--- layout: fc_discuss_archives title: Message 33 from Frama-C-discuss on August 2012 ---
Generally speaking, to "debug" such a proof, I launch an interactive prover like Coq. By trying to do that proof by hand you wuold have seen the mistake. And launching on a PO is greatly greatly easier with Why3 instead of Why2 : so I'd like to suggest to try using Why3 back-end of jessie ! (which is indeed the only one which is maintained and evolves) - 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 |