[SMT-LIB] Updates on SMTCOMP 2014

[David Cok]

1) The competition website has been updated to include a participants 
page, where details of those participating (so far, mostly, intending to 
participate) in the competition are listed. This will be updated as we 
receive official submissions: 
http://smtcomp.sourceforge.net/2014/participants.shtml

2) Solver authors: Reminder - the preliminary deadline is *June 1*. (The 
final deadline is June 15.) Upload your solver to StarExec and send the 
organizers an email stating
- the StarExec solver id
- whether you are participating in the main track or application track 
or both (may be different solver ids)
- the logics in which you are participating (see the note below on 
benchmarks)
- a random seed
- a solver description (can be submitted later)
- who to contact if there are problems.
As soon as we can we will be running trials on the solvers and 
benchmarks. While we are not a testing service, we will report to the 
contact any problems (e.g., crashes, anonymous results, failures to run, 
...) we happen to discover during the run up to the final submission 
deadline.

3) Benchmarks. We (+ Clark Barrett) have received and curated many new 
benchmarks. In particular, some logics have benchmarks that did not 
before and we will run competitions in those divisions. See the list of 
logics on the participants page: 
http://smtcomp.sourceforge.net/2014/participants.shtml. The new logics 
are: BV, UFBV, QF_ABV, QF_UFNIA . We will make the new benchmark 
subspace public as soon as we finish the last few benchmarks sets, with 
the goal being this coming weekend. The following task will be creating 
the subset and difficulty ratings from which the competition benchmark 
set will be selected.

4) Rules. A final update to the rules will be in place by this coming 
weekend.

5) Separation Logic. A subcommunity researching SMT solvers for 
Separation Logic is holding an SL-SMTCOMP, with several solvers and a 
set of benchmarks in SMTLIBv2 format. The SMTCOMP organizing committee 
will run this competition as a demonstration alongside the regular 
SMTCOMP. Over the next year, we expect the SL community and the SMTLIB 
coordinators to settle on an appropriate theory, logics, benchmarks and 
relationship to classic SMTLIB.

- David
for the organizers