--- layout: fc_discuss_archives title: Message 35 from Frama-C-discuss on May 2014 ---
Hello, Le 27/05/2014 10:36, Christophe Garion a ?crit : > z3 4.3.1 via why3 seems to prove all the assertions under Neon, so it > may be an Alt-Ergo problem. External provers are not supposed to be equivalent, so this is non-sense to say that there is a problem with a prover X if it does not prove something that is proved by a prover Y. This is the reason why using several external provers is recommended, - 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 |