[SMT-COMP] Unsat Core Track

[Matthias Heizmann]

Hi all,

I want to state my enthusiasm for Tjark's suggestion to reinstate an 
unsat core track.

On Sunday 08 February 2015 16:18:21 Tjark Weber wrote:
> We might reinstate additional tracks, e.g., for unsat core extraction and
> proof-producing solvers.

In the latest Competition on Software Verification (SV-COMP) our tool Ultimate 
Automizer used unsatisfiable cores obtained from an SMT solver to compute 
sequences of state assertions along traces. 
Hence, we would be very happy if the SMT-COMP will encourage SMT solvers to 
support unsatisfiable cores.

We submitted two sets of benchmarks for an unsatisfiable core track
http://www.informatik.uni-freiburg.de/~heizmann/2015smtcomp/UltimateAutomizer-UnsatCoreTrack.tar.xz
http://www.informatik.uni-freiburg.de/~heizmann/2015smtcomp/UltimateBuchiAutomizer-UnsatCoreTrack.tar.xz
that use various logics (QF_LIA,QF_NIA, QF_ALIA, QF_AUFLIA, QF_AUFNIA).
Please note that these benchmarks have not yet been accepted. But I already 
shared some of them with developers of solvers and in order to give no team 
an advantage I want to share them with all of you as soon as possible.

In case you are a developer of an SMT solver: if you tell the organizers that 
you are willing to participate in an unsat core track you are doing us a 
great favor.


Best,
Matthias
-------------- next part --------------
An embedded message was scrubbed...
From: Tjark Weber <tjark.weber at it.uu.se>
Subject: [SMT-COMP] SMT-COMP 2015: Call for Comments, Benchmarks, Solvers
Date: Sun, 08 Feb 2015 16:18:21 +0100
Size: 9498
URL: </pipermail/smt-comp/attachments/20150517/21690667/attachment.mht>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 819 bytes
Desc: This is a digitally signed message part.
URL: </pipermail/smt-comp/attachments/20150517/21690667/attachment.asc>