--- layout: fc_discuss_archives title: Message 59 from Frama-C-discuss on June 2009 ---
Hi, I tried to repeat some of the exercieses, which are contained in the Jessie Plugin Tutorial, however, I was not able to obtain the same results. In many cases, for which the tutorial claims that certain SMT solvers can provide a possitive answer I was only obtaining a qustion mark. In particular non of the SMT solvers I used was able to demonstrate the lemma about mean value: /*@ lemma mean : \forall integer x, y; x <= y ==> x <= (x+y)/2 <= y; */ My question is what is the reason of such a situation. If it depends on the version of solvers what versions should I use to obtain similar results: My configuration is: - Linux - Frama C Lithium Dec 2008 - Alt-Ergo 0.8 - Simplify 1.5.5 (also tried 1.5.4) - Yices 1.0.21 (also tried 1.0.17) <--- this was the solver which in the tutarial is claimed to be very powerful, but in my case did not seem so - CVC3 1.5 - Z3 1.3 -------------- next part -------------- An HTML attachment was scrubbed... URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090619/6e6d945d/attachment.htm