--- layout: fc_discuss_archives title: Message 40 from Frama-C-discuss on July 2010 ---
Hello, Boris Hollas a ?crit : >> Question 3. >> ------------------ >> Finally, I have installed CVC3 and frama-c recognizes it's there (at >> lest the GUI does) but all the calls seem to break. Is this just me or >> is some special switch needed for this one. Did you run the tool "why-config" when you installed CVC3? Did it success in configuring this ATP? > > The same is true for Simplify. It seems that Alt-Ergo is the only prover > that is useful for Jessie. I dont't know if this is a bug in Boron. 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. -- Julien