--- layout: fc_discuss_archives title: Message 43 from Frama-C-discuss on July 2010 ---
> > 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 I have similar symptoms on Mac OS X Leopard and Snow Leopard (and I did run why-config). Launching Simplify myself gives a prompt (in which I do not know what to type to check further that it is correctly installed). Pascal