--- layout: fc_discuss_archives title: Message 25 from Frama-C-discuss on November 2011 ---
[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>