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

[Frama-c-discuss] Provers versions



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