--- layout: fc_discuss_archives title: Message 20 from Frama-C-discuss on April 2013 ---
Cool, thanks. The only problem I have now is with Z3: HighFailure (0.00s) Prover exit status: exited with status 109 Prover output: Error: invalid command line option: -rs For usage information: z3 -h why3cpulimit time : 0.000000 s Maybe the command-line syntax for Z3 changed? I am using Z3 4.3.2 (z3-4.3.2.1ef17cbe6798-x64-osx-10.8.2) BTW, when I click on the Tools:Edit button, I get: HighFailure (0.10s) Prover exit status: exited with status 1 Prover output: emacs: standard input is not a tty -s On Apr 9, 2013, at 10:04 AM, Claude March? <Claude.Marche at inria.fr> wrote: > > You should do > > why3config --detect > > before using why3ide > > - Claude > > Le 09/04/2013 17:56, Stephen Siegel a ?crit : >> Hi all, I have Frama-C working with the Jessie plugin (thanks for help everyone), but the only prover I have managed to get working is CVC3. I have read some of the Why web pages but am a little confused about what is supported. I've installed why2 and why3, and the latest Alt-Ergo, Z3, cvc3, and Gappa. >> >> Here's my report from why2-config: >> >> prover version info invocation >> ------------------------------------------------------ >> Alt-Ergo 0.95.1 (not supported) alt-ergo >> Simplify not found >> Vampire not found >> Z3 4.3.2 (not supported) z3 -smt >> Yices not found >> CVC3 2.4.1 cvc3 -lang smt >> CVCL 2.4.1 cvc3 >> Gappa 0.17.1 (not supported) gappa >> Coq not found >> PVS not found >> VeriT not found >> Zenon not found >> ------------------------------------------------------ >> >> When I run frama-c -jessie, the why3ide shows only CVC3. Should I be looking for older versions of some of these provers that are compatible with why? >> >> >> _______________________________________________ >> Frama-c-discuss mailing list >> Frama-c-discuss at lists.gforge.inria.fr >> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss >> > > -- > Claude March? | tel: +33 1 72 92 59 69 > INRIA Saclay - ?le-de-France | > Universit? Paris-sud, Bat. 650 | http://www.lri.fr/~marche/ > F-91405 ORSAY Cedex | > > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss