--- layout: fc_discuss_archives title: Message 50 from Frama-C-discuss on May 2010 ---
Hi, Are you using Frama-C Beryllium with CVC3? Or is it Boron version? Kalyan On Sat, May 15, 2010 at 2:01 AM, Naghmeh Ghafari <naghmeh.ghafari at cslabs.com > wrote: > > I was only asking whether alt-ergo and CVC3 were both proving the >> post-condition, and whether they were both proving its negation. >> If they are, we should look in a bug in Frama-C/Jessie/Why. If only >> one of them is proving the property and its negation, we'll start >> by suspecting a bug in that theorem prover. If you are using >> Why's graphical interface, that would be the contents of the >> row that corresponds to the post-condition. >> > > Yes, they are both proving the post condition and its negation. > > cheers, > naghmeh > > > > _______________________________________________ > 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 > -- -- Kalyan KRISHNAMANI http://www.tcs.tifr.res.in/~kalyan -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20100515/ae9a9274/attachment.htm>