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