SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions

SMT-COMP 2018

Rules
Benchmarks
Tools
Specs
Participants
Results
Slides
Report

Participants

These solvers have been submitted to SMT-COMP 2018 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
Alt-Ergo-SMTComp-2018 X 16397 19737 18 Albin Coquereau (coquereau.a@gmail.com)
AProVE X 1229 3945321 Carsten Fuhs (carsten@dcs.bbk.ac.uk)
Boolector X 16381 19729 42 Boolector Mathias Preiner (mathias.preiner@gmail.com)
Boolector (application track) X 16384 19730 42 Boolector Mathias Preiner (mathias.preiner@gmail.com)
COLIBRI X 16345 19761 2187327402 COLIBRI François Bobot (francois.bobot@cea.fr)
Ctrl-Ergo X 16616 19738 16 Mohamed Iguernlala (iguer.pro@gmail.com)
CVC4-application X 16442 19756 1337 CVC4 Andres Nötzli (noetzli@stanford.edu)
CVC4-main X 16433 19757 1337 CVC4 Andres Nötzli (noetzli@stanford.edu)
CVC4-uc X 16440 19758 1337 CVC4 Andres Nötzli (noetzli@stanford.edu)
MinkeyRink 2018.1 MT X 16390 19683 24234 Trevor Hansen (trev_Abroad@yahoo.com)
MinkeyRink 2018.1 ST X 16391 19684 325559 Trevor Hansen (trev_Abroad@yahoo.com)
Q3B X 16446 19702 8027210 Martin Jonas (martin.jonas@mail.muni.cz)
SMTInterpol X X X 16351 716484617 SMTInterpol Jochen Hoenicke (hoenicke@informatik.uni-freiburg.de)
SMTRAT X 16364 19694 12345 SMTRAT Gereon Kremer (gereon.kremer@cs.rwth-aachen.de)
SMTRAT-MCSAT X 16365 19631 12345 SMTRAT Gereon Kremer (gereon.kremer@cs.rwth-aachen.de)
SPASS-SATT X 16348 19632 42 Martin Bromberger (mbromber@mpi-inf.mpg.de)
STP-CMS-mt X 16372 19624 2015 STP Norbert Manthey (nmanthey@conp-solutions.com)
STP-CMS-st X 16370 19622 5 STP Norbert Manthey (nmanthey@conp-solutions.com)
STP-Riss-st X 16371 19623 3 STP Norbert Manthey (nmanthey@conp-solutions.com)
Vampire 4.3 X 16353 19759 86 Giles Reger (giles.reger@manchester.ac.uk)
veriT X 16402 19742 60408 veriT Hans-Jörg Schurr (hans-jorg.schurr@inria.fr)
veriT+raSAT+Reduce X 16405 19733 3500782 veriT+raSAT+Reduce Hans-Jörg Schurr (hans-jorg.schurr@inria.fr)
Yices-2.6.0 (Application) X 16356 19740 258528 Bruno Dutertre (Bruno.Dutertre@sri.com)
Yices-2.6.0 (Main) X 16355 19739 256528 Bruno Dutertre (Bruno.Dutertre@sri.com)
Yices-2.6.0 (Unsat-Core) X 16358 19741 256528 Bruno Dutertre (Bruno.Dutertre@sri.com)
CVC4-experimental-idl-2n X 19728 — CVC4 Duligur Ibeling (duligur@gmail.com)
MathSAT 5.5.2 (Application)n X 17271 — http://mathsat.fbk.eu/download.php?file=mathsat-5.5.2-linux-x86_64.tar.gz
MathSAT 5.5.2 (Main)n X 17270 — http://mathsat.fbk.eu/download.php?file=mathsat-5.5.2-linux-x86_64.tar.gz
MathSAT 5.5.2 (Unsat-core)n X 19826 — http://mathsat.fbk.eu/download.php?file=mathsat-5.5.2-linux-x86_64.tar.gz
opensmt2n X 16651 19938 — Antti Hyvärinen (antti.hyvarinen@gmail.com)
Z3 (4.7.1)n X X X 16764 — https://github.com/Z3Prover/z3/releases/download/z3-4.7.1/z3-4.7.1.tar.gz
Total 24 6 5 773014439 (mod 230)

n. Non-competing.

The opening value of the NYSE Composite Index on 2018-06-11 was 12845.08, resulting in a competition seed of 773014439 + 12845 = 773027284.

Divisions

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

Solver ABVFP1 ALIA1,2,3 ANIA2 AUFBVDTLIA1,3 AUFDTLIA1 AUFLIA1,3 AUFLIRA1,3 AUFNIRA1,2,3 BV1,2,3 BVFP1 FP1 LIA1,2,3 LRA1,3 NIA1,3 NRA1,3 QF_ABV1,2,3 QF_ABVFP1,3 QF_ALIA1,2,3 QF_ANIA1,2,3 QF_AUFBV1,2,3 QF_AUFLIA1,2,3 QF_AUFNIA1,3 QF_AX1,3 QF_BV1,2,3 QF_BVFP1,2,3 QF_DT1,3 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_SLIA1 QF_UF1,3 QF_UFBV1,2,3 QF_UFIDL1,3 QF_UFLIA1,2,3 QF_UFLRA1,2,3 QF_UFNIA1,2,3 QF_UFNRA1,3 UF1,3 UFBV1,3 UFDT1,3 UFDTLIA1 UFIDL1,3 UFLIA1,3 UFLRA1,2,3 UFNIA1,3
Alt-Ergo-SMTComp-20181 X X X X
AProVE1 X
Boolector1 X X X X X
Boolector (application track)2 X X X
COLIBRI1 X X X
Ctrl-Ergo1 X X
CVC4-application2 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 X X X X X X X
CVC4-main1 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 X X X X X X X
CVC4-uc3 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 X X X X X X X
MinkeyRink 2018.1 MT1 X
MinkeyRink 2018.1 ST1 X
Q3B1 X
SMTInterpol1,2,3 X X X X X X X X X X X X
SMTRAT1 X X X X X X X X
SMTRAT-MCSAT1 X X
SPASS-SATT1 X X
STP-CMS-mt1 X
STP-CMS-st1 X
STP-Riss-st1 X
Vampire 4.31 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+raSAT+Reduce1 X X
Yices-2.6.0 (Application)2 X X X X X X X X X X X X X
Yices-2.6.0 (Main)1 X X X X X X X X X X X X X X X X X X X X X
Yices-2.6.0 (Unsat-Core)3 X X X X X X X X X X X X X X X X
CVC4-experimental-idl-21 X
MathSAT 5.5.2 (Application)2 X X X X X X X X X X
MathSAT 5.5.2 (Main)1 X X X X X X X X X X X X X X X
MathSAT 5.5.2 (Unsat-core)3 X X X X X X X X X X X X X X X
opensmt21 X X X
Z3 (4.7.1)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 X

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