--- layout: fc_discuss_archives title: Message 28 from Frama-C-discuss on April 2013 ---
I just tried with Z3 4.2 and it works like a charm, so there must be some incompatibility with the latest and greatest Z3 which does not seem to support the -rs commandline option. -steve On Apr 9, 2013, at 10:20 AM, Stephen Siegel <siegel at UDel.Edu> wrote: > 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 >