--- layout: fc_discuss_archives title: Message 148 from Frama-C-discuss on September 2013 ---
Thank you for your reply. We did the changes in the wh3.conf file. Best regards, Nanci, Rovedy, Luciana 2013/9/28 Claude Marche <Claude.Marche at inria.fr> > > Hello, > > All versions of provers below were released after the Why 0.81 release, > so we did not have the opportunity to test them. > > In general they are supported in the dev version of Why, and thus will > be supported in the next release. But there is no unique answer on > whether they are OK with 0.81 or not, see below. > > On 09/27/2013 07:21 PM, Rovedy Aparecida Busquim e Silva wrote: > > Warning: prover Z3 version 4.3.2 is not known to be supported, use it at > > your own risk! > > This one is OK with 0.81, as far as I know. > > > Warning: prover Gappa version 1.0.0 is not known to be supported, use it > at > > your own risk! > > OK too. > > > Warning: prover Coq version 8.4pl2 is not known to be supported, use it > at > > your own risk! > > should be OK too. > > > Warning: prover Alt-Ergo version 0.95.2 is not known to be supported, use > > it at your own risk! > > There is a small unintended change in the -timelimit option of Alt-Ergo > 0.95.2, that prevents Why3 to stop Alt-Ergo after the user given time > limit. This can be fixed by editing the [alt-ergo] record of the > generated why3.conf and replace the '%T' argument of why3cpulimit to '%t' > > > Warning: prover Yices version 2.1.0. is not known to be supported, use it > > at your own risk! > > Yices 2 does not support quantifiers AFAIK, so you will not get any > interesting proofs from Why3. You should stick to the last Yices 1 version > > - Claude > > _______________________________________________ > 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 > -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130930/335b1a3b/attachment.html>