SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions

SMT-COMP 2017

Rules
Benchmarks
Tools
Specs
Participants
Results
Slides
Report

Participants

These solvers have been submitted to SMT-COMP 2017 or were entered as non-competing solvers by the organizers for comparison.

Solver Main Track Application Track Unsat-core Track Preliminary version solver id Final version solver id Seed System description Contact(s)
AProVE X 1229 935243 Carsten Fuhs (carsten@dcs.bbk.ac.uk)
Boolector X 11608 12020 424242 Boolector Mathias Preiner (mathias.preiner@jku.at)
Boolector+CaDiCaL X 11608 12034 0 Boolector Mathias Preiner (mathias.preiner@jku.at)
COLIBRI X 11650 12031 385141 François Bobot (francois.bobot@cea.fr)
CVC4 (Main) X 11622 12023 4261980 Clark Barrett (barrett@cs.stanford.edu)
CVC4 (Application) X 11622 12024 0 Clark Barrett (barrett@cs.stanford.edu)
CVC4 (Unsat-core) X 11622 12089 0 Clark Barrett (barrett@cs.stanford.edu)
MinkeyRink X 1234 11999 2355432 Trevor Hansen (trev_Abroad@yahoo.com)
opensmt2 X X 11630 31415 Antti Hyvärinen (antti.hyvaerinen@usi.ch)
Q3B X 8085 11954 18661329 Martin Jonas (martin.jonas@mail.muni.cz)
Redlog X 11654 11892 20170704 Redlog Haniel Barbosa (haniel.barbosa@inria.fr)
SMT-RAT X 11282 11977 4711 SMT-RAT Gereon Kremer (gereon.kremer@cs.rwth-aachen.de)
SMTInterpol X X X 11698 1953339634 SMTInterpol Jochen Hoenicke (hoenicke@informatik.uni-freiburg.de)
STP-mt X 1234 12002 433324 Trevor Hansen (trev_Abroad@yahoo.com)
STP-st X 1234 12001 734534 Trevor Hansen (trev_Abroad@yahoo.com)
Vampire X 11643 12028 3648 Vampire Giles Reger (giles.reger@manchester.ac.uk)
veriT X 11466 11989 20151003 veriT Haniel Barbosa (haniel.barbosa@inria.fr)
veriT+Redlog X 11466 12005 20170605 veriT+Redlog Haniel Barbosa (haniel.barbosa@inria.fr)
veriT+raSAT+Redlog X 11469 19061999 veriT+raSAT+Redlog Haniel Barbosa (haniel.barbosa@inria.fr)
XSat X 11647 1164700 XSat Martin Velez (marvelez@ucdavis.edu)
Yices2 (Main) X 11652 12010 11976743 Dejan Jovanović (dejan.jovanovic@sri.com)
Yices2 (Application) X 11652 12011 17735201 Dejan Jovanović (dejan.jovanovic@sri.com)
MathSAT 5.4.1 (Main)n X 11978 http://mathsat.fbk.eu/download.php?file=mathsat-5.4.1-linux-x86_64.tar.gz
MathSAT 5.4.1 (Application)n X 11979 http://mathsat.fbk.eu/download.php?file=mathsat-5.4.1-linux-x86_64.tar.gz
MathSAT 5.4.1 (Unsat-core)n X 12211 http://mathsat.fbk.eu/download.php?file=mathsat-5.4.1-linux-x86_64.tar.gz
Z3 (4.5.0)n X X X 12033 https://github.com/Z3Prover/z3/archive/z3-4.5.0.tar.gz
Total 21 6 4 1018259764 (mod 230)

n. Non-competing.

The opening value of the NYSE Composite Index on 2017-06-20 was 11801.20, resulting in a competition seed of 1018259764 + 11801 = 1018271565.

Divisions

These are the logic divisions in which each solver is participating.

Solver ABVFP1 ALIA1,2,3 ANIA2 AUFBVDTLIA1 AUFDTLIA1 AUFLIA1,3 AUFLIRA1,3 AUFNIRA1,3 BV1,3 BVFP1 FP1 LIA1,2,3 LRA1,3 NIA1,3 NRA1,3 QF_ABV1,3 QF_ABVFP1,3 QF_ALIA1,2,3 QF_ANIA1,2,3 QF_AUFBV1,3 QF_AUFLIA1,2,3 QF_AUFNIA1,3 QF_AX1,3 QF_BV1,2,3 QF_BVFP1,2,3 QF_DT1 QF_FP1,2,3 QF_IDL1,3 QF_LIA1,2,3 QF_LIRA1,3 QF_LRA1,2,3 QF_NIA1,2,3 QF_NIRA1,3 QF_NRA1,3 QF_RDL1,3 QF_UF1,3 QF_UFBV1,3 QF_UFIDL1,3 QF_UFLIA1,2,3 QF_UFLRA1,2,3 QF_UFNIA1,2,3 QF_UFNRA1,3 UF1,3 UFBV1,3 UFDT1 UFDTLIA1 UFIDL1,3 UFLIA1,3 UFLRA1,2,3 UFNIA1,3
AProVE1 X
Boolector1 X X X X X
Boolector+CaDiCaL1 X
COLIBRI1 X X
CVC4 (Main)1 X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X
CVC4 (Application)2 X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X
CVC4 (Unsat-core)3 X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X
MinkeyRink1 X
opensmt21,2 X X
Q3B1 X X
Redlog1 X X
SMT-RAT1 X X X X X X
SMTInterpol1,2,3 X X X X X X X X X X X X
STP-mt1 X
STP-st1 X
Vampire1 X X X X X X X X X X X X X X X X X
veriT1 X X X X X X X X X X X X X X X X X X
veriT+Redlog1 X X
veriT+raSAT+Redlog1 X X
XSat1 X
Yices2 (Main)1 X X X X X X X X X X X X X X X X X X X X X
Yices2 (Application)2 X X X X X X X X X X X X X X X X
MathSAT 5.4.1 (Main)1 X X X X X X X X X X X X
MathSAT 5.4.1 (Application)2 X X X X X X X X X X X X
MathSAT 5.4.1 (Unsat-core)3 X X X X X X X X X X X X
Z3 (4.5.0)1,2,3 X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X

1. Main track.
2. Application track.
3. Unsat-core track.