--- layout: fc_discuss_archives title: Message 32 from Frama-C-discuss on October 2010 ---
On 10/11/2010 04:17 PM, Boris Hollas wrote: > Hi, > > I just tried to verify some of my programs with Jessie and simplify. > Although why found simplify, all VCs fail. I see the "tool problem" > icon. > > I compiled everything from the Boron 20100401 distribution on Ubuntu 10 > and installed simplify separately. Does why need special switches > for ./configure? > > > prover version info invocation > ------------------------------------------------------ > Alt-Ergo 0.92 (not supported) alt-ergo > Simplify 1.5.4 simplify > Z3 not found > Yices not found > CVC3 not found > CVCL not found > Gappa not found > Coq not found > PVS not found > ------------------------------------------------------ > > The prover Simplify should work. Please also consider adding more of them: for me Z3 and CVC3 regularly prove VCs that cannot be proved with Alt-Ergo or Simplify When the "tools" icon shows up for a prover, please select Proof/Debug mode in the menu and replay the same proof by double-clicking on it. Debug info should print on the standard error, so that you can figure out what is the problem. Apart from that, I confirm that the time limit setting of Gwhy should be stored permanently between sessions, so you have a specific problem with that, e.g. the ~/.gwhyrc, or the equivalent under MSWindows, is not writeable. - Claude -- Claude March? | tel: +33 1 72 92 59 69 INRIA Saclay - ?le-de-France | mobile: +33 6 33 14 57 93 Parc Orsay Universit? | fax: +33 1 74 85 42 29 4, rue Jacques Monod - B?timent N | http://www.lri.fr/~marche/ F-91893 ORSAY Cedex |