--- layout: fc_discuss_archives title: Message 8 from Frama-C-discuss on November 2011 ---
On Thu, 2011-11-03 at 13:11 +0100, Claude Marche wrote: > From your message, I guess you mean that you are using the Why3 > backend (since Vampire is not available in Why 2.30) yes, I had that problem with why3. However, Vampire also works with the why2-gui. > First of all, you may want to check that your proofs still work with > the former Why 2.30 back-end, using frama-c -jessie -jessie-atp=gui indeed, with the why2 back-end, the code verifies as before. -- Best regards, Boris