--- layout: fc_discuss_archives title: Message 21 from Frama-C-discuss on October 2013 ---
[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                    |