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] [Why3-club] z3 failure


Le 09/10/2013 13:10, Florian Schanda a ?crit :
>>> As to Claude's comment that he has seen many VCs that Z3 could not
>>> discharge, I have seen this too, but only when using
>>> Frama-C+Jessie+Why.   When I have used Z3, CVC3, etc., by hand, it is
>>> usually the opposite -- Z3 wins.  Also Z3 wins many competitions. 
>>
>> I recommend to be very cautious when drawing conclusions from such
>> "competitions". Moreover, as far as I know, the AUFNIRA category of the
>> SMT competition was not run for several years now.
> 
> SMTCOMP is generally taken quite seriously, so I am not sure the quotes around 
> competition are warrented; but I can't speak for any other competitions (which 
> you may have had in mind).
> 
> However I can confirm that AUFNIRA has run each year SMTCOMP has been run 
> since 2009. However note that SMTCOMP was not run in 2013. You can find the 
> results for the 2012 AUFNIRA track here:
> 
>    http://www.smtexec.org/exec/?jobs=1004

You're right, my mistake, the category was run with ONE competitor.

> (Alt-Ergo should be entering here, btw!)

I'm not an author of Alt-Ergo.

Let me explain why I'm so reluctant about drawing conclusions from
competitions: the participants are tuning their tools so that they
behave the best possible on the SMTLIB benchmarks.

> It is true however that AUFNIRA desperately needs more benchmarks. I am 
> certainly trying to get some from the SPARK 2014 testsuite into smtlib.


That would be a good idea.

- Claude

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