[SMT-COMP] SMT-COMP 2014 milestone reached - 1/3 of job-pairs completed

David Cok dcok at grammatech.com
Thu Jun 19 16:19:56 EDT 2014


Competitors:

We have reached a milestone. After three days of computation, StarExec 
has completed 1/3 of the 339714 job-pairs planned for the competition; 
and those three days included a couple hiccups - StarExec automatically 
pausing all jobs one night, and the restart we had to do on half of the 
Heat0 divisions.

StarExec is now purring along very nicely (barring a few job-pairs that 
appear stuck), at about 50K job-pairs completed per day. At this rate 
the main track computation will be completed by sometime early next 
week. See the status at 
http://smtcomp.sourceforge.net/2014/results-toc.shtml
We have not forgotten about the application track - we'll run that after 
the main track is complete.

StarExec has generated a lot of data for individual solvers and logics 
and some of you are watching it closely.

As far as the competition goes, the leaders in individual divisions are 
some well-known tools such as CVC4, Yices2 and Boolector. But 
SMTInterpol, AProVE and veriT are leading in specific areas.

In the competition for the gold/silver medals, CVC4 had a disappointment 
when a bug causing unsoundness on one benchmark dropped it from the 
leading position. Now Yices2 is leading, with SMTInterpol in second 
place. However veriT, now in 3rd, has a lot more computation yet to do 
than SMTInterpol, across a larger number of divisions, so it has a good 
chance to catch up.

I concede that I clearly overestimated the time it would take to do the 
computation, fearing the down-side of not completing the competition 
before the SMT workshop in Vienna;  I was pessimistic about the time 
requirements for the many new benchmarks, record number of entrants, and 
a new computing platform. Also when we set the deadlines, we thought 
there would be more overlap in the various competitions on StarExec, so 
didn't anticipate having nearly 150 nodes to use. Next year's organizers 
will have better data on which to base an estimate.

- David



More information about the SMT-COMP mailing list