SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Rules
Benchmarks
Tools
Specs
Participants
Benchmark submission
Solver submission
Previous

SMT-LIB

Participants

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

Solver Single Query Track Incremental Track Challenge Track (single query) Challenge Track (incremental) Unsat Core Track Model Validation Track Preliminary Solver ID Final Solver ID Seed System Description Solver Homepage Contact
AProVEX1229 1229 896120349 AProVE http://aprove.informatik.rwth-aachen.de/ carsten@dcs.bbk.ac.uk
Alt-ErgoX23333 23530 42 Alt-Ergo https://alt-ergo.ocamlpro.com/ albin.coquereau@ocamlpro.com
Boolector-ReasonLSnXX 23692 Boolector-ReasonLS hebing@ios.ac.cn
BoolectorXXX23380 23711 42 Boolector https://boolector.github.io preiner@cs.stanford.edu
Boolector (incremental)XX23381 23712 42 Boolector https://boolector.github.io preiner@cs.stanford.edu
COLIBRIX23355 23355 614823377508390721 COLIBRI francois.bobot@cea.fr
CVC4-SymBreaknX 23746 CVC4-SymBreak cs1150254@iitd.ac.in
CVC4-incXX23417 23733 439 CVC4 http://cvc4.cs.stanford.edu noetzli@cs.stanford.edu
CVC4-mvX23419 23736 439 CVC4 http://cvc4.cs.stanford.edu noetzli@cs.stanford.edu
CVC4-ucX23416 23732 439 CVC4 http://cvc4.cs.stanford.edu noetzli@cs.stanford.edu
CVC4XX23420 23737 439 CVC4 http://cvc4.cs.stanford.edu noetzli@cs.stanford.edu
Ctrl-ErgoX23398 23398 12019 Ctrl-Ergo https://alt-ergo.ocamlpro.com/ mohamed.iguernlala@ocamlpro.com
MathSAT-defaultXXX23373 23680 512 MathSAT5 airfan@stanford.edu
MathSAT-na-extXXX23427 23679 512 MathSAT5 airfan@stanford.edu
Minkeyrink SolverXXXXX23392 23720 Minkeyrink Solver trev_abroad@yahoo.com
Minkeyrink Solver MTXXXXX23393 23719 Minkeyrink Solver trev_abroad@yahoo.com
OpenSMT2X23354 23635 568 OpenSMT2 http://verify.inf.usi.ch/opensmt antti.hyvarinen@gmail.com
Par4X23391 23672 0 Par4 tjark.weber@it.uu.se
PoolectorXX23384 23730 42 Boolector https://boolector.github.io preiner@cs.stanford.edu
ProBX22647 23466 9247 proB http://www.prob2.de sebastian.krings@uni-duesseldorf.de
Q3BXX23405 23686 93629305 Q3B https://github.com/martinjonas/Q3B/releases/tag/smtcomp2019 martin.jonas@mail.muni.cz
SMT-RATX23327 23731 SMT-RAT https://github.com/smtrat/smtrat/wiki gereon.kremer@cs.rwth-aachen.de
SMTInterpolXXX23360 23554 983571724 SMTInterpol http://ultimate.informatik.uni-freiburg.de/smtinterpol/ hoenicke@informatik.uni-freiburg.de
SMTRAT-MCSATX23328 23434 SMT-RAT https://github.com/smtrat/smtrat/wiki gereon.kremer@cs.rwth-aachen.de
SPASS-SATTX23356 23356 73 SPASS-SATT https://www.spass-prover.org/ mbromber@mpi-inf.mpg.de
STP-incrementalXXXX23396 23687 1094795585 STP https://github.com/stp/stp soos.mate@gmail.com
STP-mergesat-fixednXX 24232 STP https://github.com/stp/stp nmanthey@conp-solutions.com
STP-mergesatXX23401 23401 1094795585 STP https://github.com/stp/stp nmanthey@conp-solutions.com
STP-minisatXX23402 23402 1094795585 STP https://github.com/stp/stp nmanthey@conp-solutions.com
STP-mtXXXXX23397 23663 1094795585 STP https://github.com/stp/stp soos.mate@gmail.com
STP-portfolio-fixednXX 24233 STP https://github.com/stp/stp nmanthey@conp-solutions.com
STP-portfolioXX23403 23403 1094795585 STP https://github.com/stp/stp nmanthey@conp-solutions.com
STP-rissXX23400 23400 1094795585 STP https://github.com/stp/stp nmanthey@conp-solutions.com
STPXX23321 23321 1094795585 STP https://github.com/stp/stp nmanthey@conp-solutions.com
UltimateEliminator+MathSAT-5.5.4XXX23425 23742 0 UltimateEliminator https://ultimate.informatik.uni-freiburg.de/ heizmann@informatik.uni-freiburg.de
UltimateEliminator+SMTInterpolXXX23426 23743 0 UltimateEliminator https://ultimate.informatik.uni-freiburg.de/ heizmann@informatik.uni-freiburg.de
UltimateEliminator+Yices-2.6.1XXX23423 23744 0 UltimateEliminator https://ultimate.informatik.uni-freiburg.de/ heizmann@informatik.uni-freiburg.de
VampireX23409 23703 4051 Vampire https://vprover.github.io giles.reger@manchester.ac.uk
Yices 2.6.2XXX23363 23694 255 Yices http://yices.csl.sri.com bruno.dutertre@sri.com
Yices 2.6.2 CaDiCalXX23368 23697 255 Yices http://yices.csl.sri.com bruno.dutertre@sri.com
Yices 2.6.2 CaDiCal/SMT-LIB2 ModelsX23371 23698 255 Yices http://yices.csl.sri.com bruno.dutertre@sri.com
Yices 2.6.2 CryptominisatXX23369 23699 255 Yices http://yices.csl.sri.com bruno.dutertre@sri.com
Yices 2.6.2 Cryptominisat/SMT-LIB2 ModelsX23372 23700 255 Yices http://yices.csl.sri.com bruno.dutertre@sri.com
Yices 2.6.2 IncrementalXX23364 23695 255 Yices http://yices.csl.sri.com bruno.dutertre@sri.com
Yices 2.6.2 Model ValidationX23365 23696 255 Yices http://yices.csl.sri.com bruno.dutertre@sri.com
Yices 2.6.2 New BvsolverXX23367 23701 255 Yices http://yices.csl.sri.com bruno.dutertre@sri.com
Yices 2.6.2 New Bvsolver with SMT2 ModelsX23370 23702 255 Yices http://yices.csl.sri.com bruno.dutertre@sri.com
Yices 2.6.2 mcsat-bvX23366 23715 255 Yices http://yices.csl.sri.com bruno.dutertre@sri.com
Z3nXXXXX23470 23470
veriT+raSAT+RedlogX23399 23399 13 veriT+raSAT+Redlog http://www.verit-solver.org hans-jorg.schurr@inria.fr
veriTX23406 23693 7800 veriT http://www.verit-solver.org hans-jorg.schurr@inria.fr
Total4216188910 912668687 (mod 230)

n Non-competing.

The opening value of the NYSE Composite Index on 2019-06-03 was 12888.51, resulting in a competition seed of 912668687 + 12889 = 912681576.

Divisions

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

ABVFP

SolverSingle Query TrackIncremental TrackUnsat Core Track
CVC4-incX
CVC4-ucX
CVC4X
UltimateEliminator+MathSAT-5.5.4XXX
Z3nXXX
Total333

ALIA

SolverSingle Query TrackIncremental TrackUnsat Core Track
Alt-ErgoX
CVC4-incX
CVC4-ucX
CVC4X
SMTInterpolXX
UltimateEliminator+MathSAT-5.5.4XXX
UltimateEliminator+SMTInterpolXXX
UltimateEliminator+Yices-2.6.1XXX
VampireX
Z3nXXX
veriTX
Total965

AUFBVDTLIA

SolverSingle Query TrackUnsat Core Track
CVC4-ucX
CVC4X
Total11

AUFDTLIA

SolverSingle Query TrackUnsat Core Track
Alt-ErgoX
CVC4-ucX
CVC4X
VampireX
Total31

AUFLIA

SolverSingle Query TrackUnsat Core Track
Alt-ErgoX
CVC4-SymBreaknX
CVC4-ucX
CVC4X
SMTInterpolX
UltimateEliminator+MathSAT-5.5.4XX
UltimateEliminator+SMTInterpolXX
UltimateEliminator+Yices-2.6.1XX
VampireX
Z3nXX
veriTX
Total105

AUFLIRA

SolverSingle Query TrackUnsat Core Track
Alt-ErgoX
CVC4-SymBreaknX
CVC4-ucX
CVC4X
Par4X
SMTInterpolX
UltimateEliminator+MathSAT-5.5.4XX
UltimateEliminator+SMTInterpolXX
UltimateEliminator+Yices-2.6.1XX
VampireX
Z3nXX
veriTX
Total115

AUFNIA

SolverSingle Query TrackUnsat Core Track
Alt-ErgoX
CVC4-SymBreaknX
CVC4-ucX
CVC4X
UltimateEliminator+MathSAT-5.5.4XX
UltimateEliminator+Yices-2.6.1XX
VampireX
Z3nXX
Total74

AUFNIRA

SolverSingle Query TrackIncremental TrackUnsat Core Track
Alt-ErgoX
CVC4-incX
CVC4-ucX
CVC4X
Par4X
UltimateEliminator+MathSAT-5.5.4XXX
UltimateEliminator+Yices-2.6.1XXX
VampireX
Z3nXXX
Total744

BV

SolverSingle Query TrackIncremental TrackUnsat Core Track
BoolectorX
CVC4-incX
CVC4-ucX
CVC4X
Par4X
PoolectorX
Q3BXX
UltimateEliminator+MathSAT-5.5.4XXX
Z3nXXX
Total743

BVFP

SolverSingle Query TrackIncremental TrackUnsat Core Track
CVC4-incX
CVC4-ucX
CVC4X
UltimateEliminator+MathSAT-5.5.4XXX
Z3nXXX
Total333

FP

SolverSingle Query TrackUnsat Core Track
CVC4-ucX
CVC4X
UltimateEliminator+MathSAT-5.5.4XX
Z3nXX
Total33

LIA

SolverSingle Query TrackIncremental TrackUnsat Core Track
CVC4-incX
CVC4-ucX
CVC4X
ProBX
SMTInterpolXX
UltimateEliminator+MathSAT-5.5.4XXX
UltimateEliminator+SMTInterpolXXX
UltimateEliminator+Yices-2.6.1XXX
VampireX
Z3nXXX
veriTX
Total965

LRA

SolverSingle Query TrackIncremental TrackUnsat Core Track
CVC4-incX
CVC4-ucX
CVC4X
Par4X
SMTInterpolXX
UltimateEliminator+MathSAT-5.5.4XXX
UltimateEliminator+SMTInterpolXXX
UltimateEliminator+Yices-2.6.1XXX
VampireX
Z3nXXX
Total865

NIA

SolverSingle Query TrackUnsat Core Track
CVC4-ucX
CVC4X
ProBX
UltimateEliminator+MathSAT-5.5.4XX
UltimateEliminator+Yices-2.6.1XX
VampireX
Z3nXX
Total64

NRA

SolverSingle Query TrackUnsat Core Track
CVC4-ucX
CVC4X
Par4X
UltimateEliminator+MathSAT-5.5.4XX
UltimateEliminator+Yices-2.6.1XX
VampireX
Z3nXX
Total64

QF_ABV

SolverSingle Query TrackIncremental TrackChallenge Track (single query)Challenge Track (incremental)Unsat Core Track
BoolectorXX
Boolector (incremental)XX
CVC4-incXX
CVC4-ucX
CVC4XX
Par4X
PoolectorXX
Yices 2.6.2XXX
Yices 2.6.2 IncrementalXX
Z3nXXXXX
Total64543

QF_ABVFP

SolverSingle Query TrackIncremental TrackUnsat Core Track
CVC4-incX
CVC4-ucX
CVC4X
Z3nXXX
Total222

QF_ALIA

SolverSingle Query TrackIncremental TrackUnsat Core Track
Alt-ErgoX
CVC4-incX
CVC4-ucX
CVC4X
SMTInterpolXXX
Yices 2.6.2XX
Yices 2.6.2 IncrementalX
Z3nXXX
veriTX
Total644

QF_ANIA

SolverSingle Query TrackIncremental TrackUnsat Core Track
Alt-ErgoX
CVC4-incX
CVC4-ucX
CVC4X
MathSAT-defaultXXX
MathSAT-na-extXXX
Z3nXXX
Total544

QF_AUFBV

SolverSingle Query TrackIncremental TrackChallenge Track (single query)Challenge Track (incremental)Unsat Core Track
BoolectorXX
Boolector (incremental)XX
CVC4-incXX
CVC4-ucX
CVC4XX
PoolectorXX
Yices 2.6.2XXX
Yices 2.6.2 IncrementalXX
Z3nXXXXX
Total54543

QF_AUFLIA

SolverSingle Query TrackIncremental TrackUnsat Core Track
Alt-ErgoX
CVC4-incX
CVC4-ucX
CVC4X
SMTInterpolXXX
Yices 2.6.2XX
Yices 2.6.2 IncrementalX
Z3nXXX
veriTX
Total644

QF_AUFNIA

SolverSingle Query TrackUnsat Core Track
Alt-ErgoX
CVC4-ucX
CVC4X
MathSAT-defaultXX
MathSAT-na-extXX
Z3nXX
Total54

QF_AX

SolverSingle Query TrackUnsat Core Track
Alt-ErgoX
CVC4-ucX
CVC4X
SMTInterpolXX
Yices 2.6.2XX
Z3nXX
Total54

QF_BV

SolverSingle Query TrackIncremental TrackChallenge Track (single query)Challenge Track (incremental)Unsat Core TrackModel Validation Track
Boolector-ReasonLSnXX
BoolectorXXX
Boolector (incremental)XX
CVC4-incXX
CVC4-mvX
CVC4-ucX
CVC4XX
Minkeyrink SolverXXXXX
Minkeyrink Solver MTXXXXX
Par4X
PoolectorXX
STP-incrementalXXXX
STP-mergesat-fixednXX
STP-mergesatXX
STP-minisatXX
STP-mtXXXXX
STP-portfolio-fixednXX
STP-portfolioXX
STP-rissXX
STPXX
Yices 2.6.2XXX
Yices 2.6.2 CaDiCalXX
Yices 2.6.2 CaDiCal/SMT-LIB2 ModelsX
Yices 2.6.2 CryptominisatXX
Yices 2.6.2 Cryptominisat/SMT-LIB2 ModelsX
Yices 2.6.2 IncrementalXX
Yices 2.6.2 Model ValidationX
Yices 2.6.2 New BvsolverXX
Yices 2.6.2 New Bvsolver with SMT2 ModelsX
Yices 2.6.2 mcsat-bvX
Z3nXXXXX
Total229188310

QF_BVFP

SolverSingle Query TrackIncremental TrackUnsat Core Track
CVC4-incX
CVC4-ucX
CVC4X
Par4X
Z3nXXX
Total322

QF_BVFPLRA

SolverSingle Query TrackUnsat Core Track
CVC4-ucX
CVC4X
Z3nXX
Total22

QF_DT

SolverSingle Query TrackUnsat Core Track
Alt-ErgoX
CVC4-ucX
CVC4X
Total21

QF_FP

SolverSingle Query TrackIncremental TrackUnsat Core Track
COLIBRIX
CVC4-incX
CVC4-ucX
CVC4X
Par4X
Z3nXXX
Total422

QF_FPLRA

SolverSingle Query TrackUnsat Core Track
CVC4-ucX
CVC4X
Z3nXX
Total22

QF_IDL

SolverSingle Query TrackUnsat Core Track
CVC4-ucX
CVC4X
Par4X
ProBX
SMTInterpolXX
Yices 2.6.2XX
Z3nXX
veriTX
Total74

QF_LIA

SolverSingle Query TrackIncremental TrackUnsat Core Track
CVC4-SymBreaknX
CVC4-incX
CVC4-ucX
CVC4X
Ctrl-ErgoX
Par4X
ProBX
SMTInterpolXXX
SPASS-SATTX
Yices 2.6.2XX
Yices 2.6.2 IncrementalX
Z3nXXX
veriTX
Total1044

QF_LIRA

SolverSingle Query TrackUnsat Core Track
CVC4-ucX
CVC4X
Par4X
SMTInterpolXX
Yices 2.6.2XX
Z3nXX
Total54

QF_LRA

SolverSingle Query TrackIncremental TrackUnsat Core Track
CVC4-SymBreaknX
CVC4-incX
CVC4-ucX
CVC4X
Ctrl-ErgoX
OpenSMT2X
Par4X
SMTInterpolXXX
SPASS-SATTX
Yices 2.6.2XX
Yices 2.6.2 IncrementalX
Z3nXXX
veriTX
Total1044

QF_NIA

SolverSingle Query TrackIncremental TrackUnsat Core Track
AProVEX
CVC4-SymBreaknX
CVC4-incX
CVC4-ucX
CVC4X
MathSAT-defaultXXX
MathSAT-na-extXXX
Par4X
ProBX
SMT-RATX
Yices 2.6.2X
Yices 2.6.2 IncrementalX
Z3nXXX
Total1054

QF_NIRA

SolverSingle Query TrackUnsat Core Track
CVC4-ucX
CVC4X
MathSAT-defaultXX
MathSAT-na-extXX
SMT-RATX
Yices 2.6.2X
Z3nXX
Total64

QF_NRA

SolverSingle Query TrackUnsat Core Track
CVC4-SymBreaknX
CVC4-ucX
CVC4X
MathSAT-defaultXX
MathSAT-na-extXX
Par4X
SMT-RATX
SMTRAT-MCSATX
Yices 2.6.2X
Z3nXX
veriT+raSAT+RedlogX
Total104

QF_RDL

SolverSingle Query TrackUnsat Core Track
CVC4-ucX
CVC4X
SMTInterpolXX
Yices 2.6.2XX
Z3nXX
veriTX
Total54

QF_S

SolverSingle Query TrackUnsat Core Track
CVC4-ucX
CVC4X
Total11

QF_SLIA

SolverSingle Query TrackUnsat Core Track
CVC4-ucX
CVC4X
Total11

QF_UF

SolverSingle Query TrackIncremental TrackUnsat Core Track
Alt-ErgoX
CVC4-incX
CVC4-ucX
CVC4X
OpenSMT2X
Par4X
SMTInterpolXXX
Yices 2.6.2XX
Yices 2.6.2 IncrementalX
Z3nXXX
veriTX
Total844

QF_UFBV

SolverSingle Query TrackIncremental TrackUnsat Core Track
BoolectorX
Boolector (incremental)X
CVC4-incX
CVC4-ucX
CVC4X
PoolectorX
Yices 2.6.2XX
Yices 2.6.2 IncrementalX
Z3nXXX
Total543

QF_UFIDL

SolverSingle Query TrackUnsat Core Track
CVC4-ucX
CVC4X
SMTInterpolXX
Yices 2.6.2XX
Z3nXX
veriTX
Total54

QF_UFLIA

SolverSingle Query TrackIncremental TrackUnsat Core Track
Alt-ErgoX
CVC4-incX
CVC4-ucX
CVC4X
SMTInterpolXXX
Yices 2.6.2XX
Yices 2.6.2 IncrementalX
Z3nXXX
veriTX
Total644

QF_UFLRA

SolverSingle Query TrackIncremental TrackUnsat Core Track
Alt-ErgoX
CVC4-incX
CVC4-ucX
CVC4X
SMTInterpolXXX
Yices 2.6.2XX
Yices 2.6.2 IncrementalX
Z3nXXX
veriTX
Total644

QF_UFNIA

SolverSingle Query TrackIncremental TrackUnsat Core Track
Alt-ErgoX
CVC4-incX
CVC4-ucX
CVC4X
MathSAT-defaultXXX
MathSAT-na-extXXX
Yices 2.6.2X
Yices 2.6.2 IncrementalX
Z3nXXX
Total654

QF_UFNRA

SolverSingle Query TrackUnsat Core Track
Alt-ErgoX
CVC4-ucX
CVC4X
MathSAT-defaultXX
MathSAT-na-extXX
Par4X
Yices 2.6.2X
Z3nXX
veriT+raSAT+RedlogX
Total84

UF

SolverSingle Query TrackUnsat Core Track
Alt-ErgoX
CVC4-ucX
CVC4X
Par4X
SMTInterpolX
UltimateEliminator+MathSAT-5.5.4XX
UltimateEliminator+SMTInterpolXX
UltimateEliminator+Yices-2.6.1XX
VampireX
Z3nXX
veriTX
Total105

UFBV

SolverSingle Query TrackUnsat Core Track
CVC4-ucX
CVC4X
Par4X
UltimateEliminator+MathSAT-5.5.4XX
Z3nXX
Total43

UFDT

SolverSingle Query TrackUnsat Core Track
Alt-ErgoX
CVC4-ucX
CVC4X
VampireX
Total31

UFDTLIA

SolverSingle Query TrackUnsat Core Track
Alt-ErgoX
CVC4-ucX
CVC4X
VampireX
Total31

UFDTNIA

SolverSingle Query TrackUnsat Core Track
Alt-ErgoX
CVC4-ucX
CVC4X
VampireX
Total31

UFIDL

SolverSingle Query TrackUnsat Core Track
CVC4-ucX
CVC4X
Par4X
SMTInterpolX
UltimateEliminator+MathSAT-5.5.4XX
UltimateEliminator+SMTInterpolXX
UltimateEliminator+Yices-2.6.1XX
VampireX
Z3nXX
veriTX
Total95

UFLIA

SolverSingle Query TrackUnsat Core Track
Alt-ErgoX
CVC4-ucX
CVC4X
Par4X
SMTInterpolX
UltimateEliminator+MathSAT-5.5.4XX
UltimateEliminator+SMTInterpolXX
UltimateEliminator+Yices-2.6.1XX
VampireX
Z3nXX
veriTX
Total105

UFLRA

SolverSingle Query TrackIncremental TrackUnsat Core Track
Alt-ErgoX
CVC4-incX
CVC4-ucX
CVC4X
SMTInterpolXX
UltimateEliminator+MathSAT-5.5.4XXX
UltimateEliminator+SMTInterpolXXX
UltimateEliminator+Yices-2.6.1XXX
VampireX
Z3nXXX
veriTX
Total965

UFNIA

SolverSingle Query TrackUnsat Core Track
Alt-ErgoX
CVC4-SymBreaknX
CVC4-ucX
CVC4X
Par4X
UltimateEliminator+MathSAT-5.5.4XX
UltimateEliminator+Yices-2.6.1XX
VampireX
Z3nXX
Total84

ANIA

SolverIncremental Track
CVC4-incX
UltimateEliminator+MathSAT-5.5.4X
UltimateEliminator+Yices-2.6.1X
Z3nX
Total4

QF_AUFBVLIA

SolverIncremental Track
CVC4-incX
Z3nX
Total2

QF_AUFBVNIA

SolverIncremental Track
CVC4-incX
MathSAT-defaultX
MathSAT-na-extX
Z3nX
Total4

QF_UFBVLIA

SolverIncremental Track
CVC4-incX
Z3nX
Total2