--- layout: fc_discuss_archives title: Message 49 from Frama-C-discuss on May 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] question about a simple example and jessie



> 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