[SMT-COMP] Unsat Core Track

Tjark Weber tjark.weber at it.uu.se
Mon May 18 06:39:40 EDT 2015


Matthias,

On Sun, 2015-05-17 at 15:38 +0200, Matthias Heizmann wrote:
> I want to state my enthusiasm for Tjark's suggestion to reinstate an 
> unsat core track.

Just to be clear: for 2015, we have decided to limit the scope of
SMT-COMP to the (usual) main track and application track. We are
currently adding new benchmarks in these tracks to SMT-LIB. The
competition will also feature other novelties, e.g., a parallel ranking
in addition to the usual sequential ranking -- see the rules at
http://smtcomp.sourceforge.net/2015/ for details.

I do believe that broadening the scope of SMT-COMP to again include
further tracks, e.g., an unsat core track or a proof track, would be
desirable. This will not happen for 2015 -- we decided to focus our
attention elsewhere, also because the community did not express strong
interest in such tracks. But I would encourage next year's organizing
team to revisit this issue, and perhaps recruit a volunteer who is
willing to create the necessary StarExec infrastructure.

Best,
Tjark




More information about the SMT-COMP mailing list