[SMT-LIB] Update on SMTCOMP 2014 for the wider SMT community

[David Cok]

If you are interested in the SMTCOMP 2014 competition begin held between 
now and the SMT workshop in Vienna in mid-July:

June 1 was the deadline for preliminary versions of solvers to be 
submitted to the organizers. We have nearly all of them available on 
StarExec, with just a few problems with some solvers that have never 
been part of this infrastructure before.

Bottom line: we have 20 competing solvers from 14 teams, including 5 
solvers from teams that never participated in SMTCOMP before and others 
that have returned after an absence. See the list on 
http://smtcomp.sourceforge.net/2014/participants.shtml

Two groups that have participated in the past (Z3 and MathSAT) are not 
entering this year because their research priorities have been 
elsewhere. The organizers will include current versions of those tools 
for non-competitive comparison purposes only.

The benchmark set has also been considerably increased, with several 
thousand new benchmarks from a variety of contributors; in particular 
there are benchmarks produced by verification tools in action 
("industrial" benchmarks). We'll report a final tally later. Of note is 
that the benchmarks were recategorized into the minimal logic needed to 
express the benchmark. As a result of both the recategorization and new 
submissions, we now have benchmarks for 34 different SMT logics 
(compared to 22 in SMTEVAL 2013).

Finally, we have a parallel competition SL-SMTCOMP using a logic and 
theory that includes Separation Logic. The concrete syntax is the same 
as that used for SMTCOMP. In that inaugural competition, we have 8 
solvers from 7 teams.

With all the preliminary solvers and new benchmarks submitted , we are 
now concentrating on determining difficulty classifications for the 
benchmarks, checking benchmark correctness, running trial 
mini-competitions using the preliminary solvers, helping with solver 
problems that are being found, and planning the resources needed for the 
competition.

- David, David and Tjark