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