--- layout: fc_discuss_archives title: Message 24 from Frama-C-discuss on November 2011 ---
Hi, Suggestion: you should use -wp-out <dir> option of WP to keep all generated files in <dir>. Then, have a look at <dir>/ runtime_equal_loop_inv_146_established_po_why.txt which is the log of all operations runs by WP on this goal, as indicated in the WP manual. You also have this log available from the GUI (-wp-out <dir> is not necessary in this case) in the 'WP Proof Obligations' panel. Probably, Cvc3 have failed in some way... Indeed, we use Cvc3 very rarely ! L. Le 12 nov. 11 ? 02:20, ??? a ?crit : > Hi, > When wp plugin is loaded in program to prove some properties, > frama-c raised an error: > > [wp] user error: command 'why-dp' failed. > > and the description is: > > [wp] [Cvc3] Goal runtime_equal_loop_inv_146_preserved : > Valid > [wp] user error: command 'why-dp' failed. > why-dp -smt-solver cvc3 -batch > /tmp/wp33b87e.dir/ > runtime_equal_loop_inv_146_established_po_why.smt > [wp] [Cvc3] Goal runtime_equal_loop_inv_146_established : > Unknown > > Is that because of it has forked too many threads(4?) or the memory > or CPU is not enough? > > Best Regards to You. > Henry > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss