[SMT-LIB] SMT COMP/EVAL in 2013

[David Cok]

To everyone interested in SMT evaluations and competitions:

After input and discussion since last summer's SMT competition 
(SMT-COMP'12 at IJCAR in Manchester: 
http://smtcomp.sourceforge.net/2012/ ), the SMT Steering committee has 
decided to change the format of the competition in 2013. The SMT 
competition has been useful to both participants and observers, but has 
now been running for 8 years in more or less the same format. 
Accordingly, in 2013 we will conduct an evaluation (SMT-EVAL) of a 
different nature, in large part yet to be determined. It is expected to 
be a study of some aspect of the state of the art of solver capability, 
conducted over a longer period of time. It will not have the real-time 
focus that the competition did. There will be a report on progress at 
the SMT workshop at SAT in July. We will engage solver providers and 
those interested in using solvers for applications.

A side-benefit of SMT-EVAL as envisioned rather than the traditional 
SMT-COMP is to be able to exercise the new (still in development) 
Star-Exec competition framework without the deadline pressure of a 
real-time competition.

The SMT-EVAL team consists of Aaron Stump, Tjark Weber, and David Cok. 
For the moment, we will continue to use the SMT-COMP mailing list for 
discussions of purpose and progress, and for relevant communications 
with solver authors and benchmark providers. (So if you are interested 
in further discussion and receive smt-lib communications but not 
smt-comp, please subscribe to smt-comp at cs.nyu.edu)

More information (and requests) to come,

David Cok
(chair of SMT-COMP'12 organizing committee)