Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] command 'why-dp' failed

Hello,
     I did what you said and got those files. The contents
in runtime_equal_loop_inv_31_established_cvc3.txt are:
why --smtlib
    /home/lzh/doc/why-out/runtime_equal_loop_inv_31_established_po.why
Run
why-dp -smt-solver cvc3 -batch
    /home/lzh/doc/why-out/runtime_equal_loop_inv_31_established_po_why.smt
Run Exit [4]

Run Exit [4]

But, it finished the task if I ran the command "why-dp -smt-solver cvc3
-batch
/home/lzh/doc/why-out/runtime_equal_loop_inv_31_established_po_why.smt"
alone. So I think maybe cvc3 is not supported very well.
And by the way, is it the prover alt-ergo that you most frequently use??

Best Wishes.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20111117/73120b70/attachment.htm>