--- layout: fc_discuss_archives title: Message 5 from Frama-C-discuss on November 2011 ---
Hi, From your message, I guess you mean that you are using the Why3 backend (since Vampire is not available in Why 2.30) 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 Second, when using Why3 backend, that's true that VCs are slightly different, but the most important thing is that they are not automatically split into pieces when they are conjunctions. So, when a VC is not proved, the first thing to try is the "split" button of why3 ide. See both jessie manual ("tutorial" part, http://krakatoa.lri.fr/jessie.html#htoc5) and Why3 manual (https://gforge.inria.fr/docman/view.php/2990/7635/manual.pdf, Section 1.2) If you did all that already, then further investigation is needed. I'll be happy to help but I need more details: input source if possible, and which VC you can't prove. Regards, - Claude Le 03/11/2011 09:42, Boris Hollas a ?crit : > Hello, > > I have code that verified with the previous release of Frama-C/Jessie > + Alt-Ergo + Simplify, but not with the current release, even with a > prover timeout of 5 minutes. I use Alt-Ergo, Simplify and Vampire as > back-end provers. Before I try adding more specification, are there > other options I have? Has the new why release, which I installed > together with why3, changed the way in which VC are generated? > -- > Best regards, > Boris > > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss -------------- section suivante -------------- Une pi?ce jointe HTML a ?t? nettoy?e... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20111103/e4253fea/attachment.htm>