--- layout: fc_discuss_archives title: Message 48 from Frama-C-discuss on May 2010 ---
> Maybe the prover cannot prove the invariant is wrong, but cannot > prove it right either. Previously I meant, as one possible explanation for the post-condition being proved as well as its negation, for the invariant to be equivalent to the logical formula "false", that is, to be self-contradictory (I should have mentioned the possibility that the invariant contradicts the loop's exit condition, which is another possibility). This is different from having the wrong invariant, which can prevent establishing the invariant, or prevent proving a post-condition that should hold, or allow to prove a post-condition that does not hold, but which should never, as far as I reckon, allow to prove both a post-condition and its negation. Now that I think about it, the invariants on the slides I referenced earlier do not look like they are contradictory, although it is always hard to be sure that they are the right invariants. >> Could you clarify what the diagnostic of each of alt-ergo and CVC3 is >> > > Where can I find this? Is this in the jessie log file? If I run CVC3 and Alt > Ergo back to back, does it include both results in the log file? 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. Pascal