--- layout: fc_discuss_archives title: Message 36 from Frama-C-discuss on August 2012 ---
Dear Claude, At Thu, 23 Aug 2012 10:17:19 +0200, Claude Marche wrote: > > > 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. thanks for sharing this type of advice, greatly appreciated! > 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) OK, I switched. Best regards, Marko -------------- next part -------------- A non-text attachment was scrubbed... Name: not available Type: application/pgp-signature Size: 198 bytes Desc: not available URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20120823/20605b1d/attachment.pgp>