--- layout: fc_discuss_archives title: Message 7 from Frama-C-discuss on August 2010 ---
Hello, > Could you specify which automated prover(s) prove the false > post-condition of equal_pop? When I run "frama-c-Jessie -jessie > equal_pop.c" with Boron I get timeouts from alt-ergo 0.91 for "0==1" > and for "Equal(s,t)". It is Simplify that proves the false one in this example. The other provers return a time-out. (But by running these kind of experiments I also saw Alt-Ergo prove such a false postcondition in an analogue example of a Queue.) Thanks for the other hint, I'm going to try what you suggested. Regards, Kerstin -------------- next part -------------- A non-text attachment was scrubbed... Name: not available Type: application/ms-tnef Size: 2951 bytes Desc: not available URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20100817/244cb892/attachment.bin>