[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