Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

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