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

[Frama-c-discuss] which provers to use



Cool, thanks.  The only problem I have now is with Z3:

HighFailure (0.00s)
Prover exit status: exited with status 109
Prover output:
Error: invalid command line option: -rs
For usage information: z3 -h
why3cpulimit time : 0.000000 s


Maybe the command-line syntax for Z3 changed? I am using Z3 4.3.2
(z3-4.3.2.1ef17cbe6798-x64-osx-10.8.2)

BTW, when I click on the Tools:Edit button, I get:

HighFailure (0.10s)
Prover exit status: exited with status 1
Prover output:
emacs: standard input is not a tty

-s

On Apr 9, 2013, at 10:04 AM, Claude March? <Claude.Marche at inria.fr> wrote:

> 
> You should do
> 
>  why3config --detect
> 
> before using why3ide
> 
> - Claude
> 
> Le 09/04/2013 17:56, Stephen Siegel a ?crit :
>> Hi all, I have Frama-C working with the Jessie plugin (thanks for help everyone), but the only prover I have managed to get working is CVC3.  I have read some of the Why web pages but am a little confused about what is supported.  I've installed why2 and why3, and the latest Alt-Ergo, Z3, cvc3, and Gappa.
>> 
>> Here's my report from why2-config:
>> 
>>     prover      version              info   invocation
>> ------------------------------------------------------
>>   Alt-Ergo       0.95.1   (not supported)   alt-ergo
>>   Simplify                      not found
>>    Vampire                      not found
>>         Z3        4.3.2   (not supported)   z3 -smt
>>      Yices                      not found
>>       CVC3        2.4.1                     cvc3 -lang smt
>>       CVCL        2.4.1                     cvc3
>>      Gappa       0.17.1   (not supported)   gappa
>>        Coq                      not found
>>        PVS                      not found
>>      VeriT                      not found
>>      Zenon                      not found
>> ------------------------------------------------------
>> 
>> When I run frama-c -jessie, the why3ide shows only CVC3.  Should I be looking for older versions of some of these provers that are compatible with why?
>> 
>> 
>> _______________________________________________
>> 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
>> 
> 
> -- 
> Claude March?                          | tel: +33 1 72 92 59 69
> INRIA Saclay - ?le-de-France           |
> Universit? Paris-sud, Bat. 650         | http://www.lri.fr/~marche/
> F-91405 ORSAY Cedex                    |
> 
> 
> _______________________________________________
> 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