--- layout: fc_discuss_archives title: Message 47 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



> - 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