--- layout: fc_discuss_archives title: Message 47 from Frama-C-discuss on May 2010 ---
> - one of the invariants is false, and your CVC3 is correctly using it > to prove both the post-condition and its negation. > This is highly probable, as I get 'timeouts' and 'unknown' for some invariants. Maybe the prover cannot prove the invariant is wrong, but cannot prove it right either. > 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? thanks, naghmeh