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