--- layout: fc_discuss_archives title: Message 59 from Frama-C-discuss on June 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Jessie Plugin Tutorial



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