--- layout: fc_discuss_archives title: Message 49 from Frama-C-discuss on May 2010 ---
> 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