--- layout: fc_discuss_archives title: Message 28 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



I just tried with Z3 4.2 and it works like a charm, so there must be some incompatibility with the latest and greatest Z3 which does not seem to support the -rs commandline option.
-steve

On Apr 9, 2013, at 10:20 AM, Stephen Siegel <siegel at UDel.Edu> wrote:

> 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
>