--- layout: fc_discuss_archives title: Message 19 from Frama-C-discuss on April 2013 ---
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 |