--- layout: fc_discuss_archives title: Message 29 from Frama-C-discuss on August 2012 ---
With the combination of Why3 0.73 and Why 2.31 that were released last July, there is a bug that prevents Why3 from running if the Coq prover is *not* installed. This can be fixed by editing the file WHYLIB/why3/why3.conf (typically WHYLIB = /usr/local/lib/why) and removing the [prover coq] section (3 lines) - Claude -- 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 |