--- layout: fc_discuss_archives title: Message 8 from Frama-C-discuss on August 2010 ---
Le mar. 17 ao?t 2010 13:42:28 CEST, "Kerstin Hartig" <kerstin.hartig at first.fraunhofer.de> a ?crit : > > 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. > I have the same behavior as Pascal (no proof for Equal(s,t) and 0==1 in equal_pop) for alt-ergo 0.91, Simplify 1.5.4 and Z3 2.0 (Frama-C Boron and Why 2.26). Just in case, when you ran your experiment with equal_pop, you had the ensures 0==1 commented out in the spec of pop itself, as it is in the archive, right? Otherwise, the issue lies there. Best regards, -- E tutto per oggi, a la prossima volta. Virgile