--- layout: fc_discuss_archives title: Message 42 from Frama-C-discuss on July 2010 ---
On Thu, 2010-07-22 at 09:57 +0200, Julien Signoles wrote: > That's not true. Many users discharge proof obligations using either > Simplify, Z3, CVC3 or Alt-Ergo. Gappa is also useful for verifying > floating-points code. > > By the way, for many examples, using several ATPs is the only way to > automatically discharge the whole generated proof obligations. I have a program that generates ~200 VC. Most of them are proved by Alt-Ergo, but none of them by Simplify. I see the "tool problem" icon on each VC. I ran why-config and it detected Simplify. I was able to use Simplify with previous versions of Frama-C/Jessie. Maybe there's a bug in the toolchain or the makefile. I use Boron on Ubuntu 10. prover version info invocation ------------------------------------------------------ Alt-Ergo 0.91 (not supported) alt-ergo Simplify 1.5.4 simplify -- Regards, Boris