--- layout: fc_discuss_archives title: Message 148 from Frama-C-discuss on September 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Provers versions



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>