SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

Participants
Results

Participants

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

Solver Single Query Track Preliminary Solver ID Final Solver ID Seed System Description
2018-Boolector (incremental)n 19991 Boolector at the SMT Competition 2018
2018-CVC4n X 19775 CVC4 at the SMT Competition 2018
2018-CVC4 (incremental)n 19992 CVC4 at the SMT Competition 2018
2018-CVC4 (unsat core)n 19793 CVC4 at the SMT Competition 2018
2018-MathSAT (incremental)n 19993
2018-SMTRAT-Ratn X 19783 SMT-RAT 2.2
2018-Vampiren X 19788
2018-Yicesn X 19791
2018-Yices (incremental)n 19995
2018-Yices (unsat core)n 19796
2018-Z3n X 19792
2018-Z3 (incremental)n 19996
2018-Z3 (unsat core)n 19797
2019-Boolectorn X 23380 23711 Boolector at the SMT Competition 2019
2019-CVC4-incn 23417 23733 CVC4 at the SMT Competition 2019
2019-CVC4-ucn 23416 23732 CVC4 at the SMT Competition 2019
2019-CVC4n X 23420 23737 CVC4 at the SMT Competition 2019
2019-MathSAT-defaultn X 23373 23680 MathSAT5 (Nonlinear) at the SMT Competition 2019
2019-MathSAT-na-extn 23427 23679 MathSAT5 (Nonlinear) at the SMT Competition 2019
2019-Par4n X 23391 23672 Par4
2019-Poolectorn X 23384 23730 Boolector at the SMT Competition 2019
2019-SMTInterpoln X 23360 23554 SMTInterpol
2019-SPASS-SATTn X 23356 23356 SPASS-SATT v1.1
2019-Vampiren X 23409 23703 Vampire 4.4-SMT System Description
2019-Yices 2.6.2n X 23363 23694 Yices 2 in SMT-COMP 2019
2019-Yices 2.6.2 Incrementaln 23364 23695 Yices 2 in SMT-COMP 2019
2019-Z3n X 23470 23470
AProVE X 1229 1229 31249347 AProVE at SMT-COMP 2020
Alt-Ergo X 28077 28634 42 Alt-Ergo
Bitwuzla-fixedn X 29091 29091 Bitwuzla at the SMT Competition 2020
Bitwuzla X 28351 28818 42 Bitwuzla at the SMT Competition 2020
COLIBRI X 28309 28737 101 COLIBRI
CVC4-inc 28466 28799 94305 CVC4 at the SMT Competition 2020
CVC4-mv 28356 28801 94305 CVC4 at the SMT Competition 2020
CVC4-uc 28357 28800 94305 CVC4 at the SMT Competition 2020
CVC4 X 28354 28798 94305 CVC4 at the SMT Competition 2020
LazyBV2Int X 28568 28722 670 LazyBV2Int at the SMT Competition 2020
MathSAT5-mvn 28907 28907 0
MathSAT5n X 28851 28851 0
MinkeyRink-fixedn X 28765 28765 MinkeyRink 2020.0
MinkeyRink X 23719 28838 9595959 MinkeyRink 2020.0
OpenSMT X 28564 28738 24131 OpenSMT in SMT-COMP 2020
SMT-RAT-CAlC X 28001 28001 100229226230 SMT-RAT 20.04
SMT-RAT-MCSAT X 28002 28002 110594628 SMT-RAT 20.04
SMT-RAT X 28075 28075 241141182102 SMT-RAT 20.04
SMTInterpol-fixedn X 29030 29030 SMTInterpol
SMTInterpol X 28544 28784 192843011 SMTInterpol
STP + CMS X 23663 28776 20200504 STP in the SMTCOMP 2020
STP + MergeSAT X 23401 28841 11111111 STP in the SMTCOMP 2020
UltimateEliminator+MathSAT X 28584 28846 0 UltimateEliminator
Vampire X 28324 28782 4329 Vampire 4.5-SMT System Description
Yices2-fixedn X 29032 29032 Yices 2 in SMT-COMP 2020
Yices2-fixed Model Validationn 29033 29033 Yices 2 in SMT-COMP 2020
Yices2-fixed incrementaln 29034 29034 Yices 2 in SMT-COMP 2020
Yices2 X 28343 28820 87654 Yices 2 in SMT-COMP 2020
Yices2 Model Validation 28464 28819 98765 Yices 2 in SMT-COMP 2020
Yices2 incremental 28344 28821 98765 Yices 2 in SMT-COMP 2020
Z3str4 X 28567 28721 34376255 Z3str4: A Two-Armed String Solver
veriT+raSAT+Redlog X 28339 28339 39 veriT+raSAT+Redlog at SMT-COMP 2020
veriT+viten X 28742 28742 0 veriT at SMT-COMP 2020
veriT X 28338 28741 153 veriT at SMT-COMP 2020
z3n X 28814 28814 0
Total - competing 20
Total - non-competing 22
Total 42 331171026 (mod 230)

n Non-competing.

The opening value of the NYSE Composite Index on 2020-05-27 was 11787.5646, resulting in a competition seed of 331171026 + 1178756 = 332349782.

Divisions

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

QF_BV

Solver Single Query Track
2019-Boolectorn X
2019-Poolectorn X
Bitwuzla-fixedn X
Bitwuzla X
CVC4 X
LazyBV2Int X
MathSAT5n X
MinkeyRink-fixedn X
MinkeyRink X
STP + CMS X
STP + MergeSAT X
Yices2-fixedn X
Yices2 X
z3n X
Total - competing 7
Total - non-competing 7
Total 14

QF_Equality (QF_UF, QF_AX, QF_DT)

Solver Single Query Track
2018-CVC4n X
2018-Yicesn X
2019-Par4n X
2019-Yices 2.6.2n X
Alt-Ergo X
CVC4 X
MathSAT5n X
OpenSMT X
SMTInterpol-fixedn X
SMTInterpol X
Yices2-fixedn X
Yices2 X
veriT X
z3n X
Total - competing 6
Total - non-competing 8
Total 14

QF_Equality+LinearArith (QF_ALIA, QF_AUFLIA, QF_UFLIA, QF_UFLRA, QF_UFIDL)

Solver Single Query Track
2018-Yicesn X
2019-SMTInterpoln X
2019-Yices 2.6.2n X
Alt-Ergo X
CVC4 X
MathSAT5n X
SMTInterpol-fixedn X
SMTInterpol X
Yices2-fixedn X
Yices2 X
veriT X
z3n X
Total - competing 5
Total - non-competing 7
Total 12

QF_Equality+NonLinearArith (QF_UFNRA, QF_UFNIA, QF_ANIA, QF_AUFNIA)

Solver Single Query Track
2019-CVC4n X
2019-MathSAT-defaultn X
2019-Par4n X
Alt-Ergo X
CVC4 X
MathSAT5n X
Yices2-fixedn X
Yices2 X
veriT+raSAT+Redlog X
z3n X
Total - competing 4
Total - non-competing 6
Total 10

QF_LinearIntArith (QF_LIA, QF_LIRA, QF_IDL)

Solver Single Query Track
2019-Par4n X
2019-Z3n X
CVC4 X
MathSAT5n X
SMTInterpol-fixedn X
SMTInterpol X
Yices2-fixedn X
Yices2 X
veriT X
z3n X
Total - competing 4
Total - non-competing 6
Total 10

QF_LinearRealArith (QF_LRA, QF_RDL)

Solver Single Query Track
2019-Par4n X
2019-SPASS-SATTn X
2019-Yices 2.6.2n X
CVC4 X
MathSAT5n X
OpenSMT X
SMTInterpol-fixedn X
SMTInterpol X
Yices2-fixedn X
Yices2 X
veriT X
z3n X
Total - competing 5
Total - non-competing 7
Total 12

QF_Equality+BVArith (QF_ABV, QF_UFBV, QF_AUFBV)

Solver Single Query Track
2019-Boolectorn X
2019-Par4n X
2019-Yices 2.6.2n X
Bitwuzla-fixedn X
Bitwuzla X
CVC4 X
MathSAT5n X
Yices2-fixedn X
Yices2 X
z3n X
Total - competing 3
Total - non-competing 7
Total 10

QF_FPArith (QF_FP, QF_UFFP, QF_FPLRA, QF_BVFP, QF_ABVFP, QF_BVFPLRA, QF_ABVFPLRA)

Solver Single Query Track
2019-Par4n X
Bitwuzla-fixedn X
Bitwuzla X
COLIBRI X
CVC4 X
MathSAT5n X
z3n X
Total - competing 3
Total - non-competing 4
Total 7

QF_NonLinearIntArith (QF_NIA, QF_NIRA)

Solver Single Query Track
2018-SMTRAT-Ratn X
2019-Par4n X
AProVE X
CVC4 X
MathSAT5n X
SMT-RAT X
Yices2-fixedn X
Yices2 X
z3n X
Total - competing 4
Total - non-competing 5
Total 9

QF_NRA

Solver Single Query Track
2019-Par4n X
CVC4 X
MathSAT5n X
SMT-RAT-CAlC X
SMT-RAT-MCSAT X
Yices2-fixedn X
Yices2 X
veriT+raSAT+Redlog X
z3n X
Total - competing 5
Total - non-competing 4
Total 9

QF_Strings (QF_S, QF_SLIA)

Solver Single Query Track
CVC4 X
Z3str4 X
Total - competing 2
Total - non-competing 0
Total 2

BV

Solver Single Query Track
2019-Par4n X
Bitwuzla-fixedn X
Bitwuzla X
CVC4 X
UltimateEliminator+MathSAT X
z3n X
Total - competing 3
Total - non-competing 3
Total 6

Arith (LRA, LIA, NIA, NRA)

Solver Single Query Track
2018-Z3n X
2019-Par4n X
2019-Z3n X
CVC4 X
SMTInterpol-fixedn X
SMTInterpol X
UltimateEliminator+MathSAT X
Vampire X
veriT+viten X
veriT X
z3n X
Total - competing 5
Total - non-competing 6
Total 11

Equality (UF, UFDT)

Solver Single Query Track
2018-Vampiren X
2019-CVC4n X
Alt-Ergo X
CVC4 X
SMTInterpol-fixedn X
SMTInterpol X
UltimateEliminator+MathSAT X
Vampire X
veriT+viten X
veriT X
z3n X
Total - competing 6
Total - non-competing 5
Total 11

Equality+LinearArith (ALIA, AUFLIA, UFLIA, UFIDL, AUFLIRA, UFLRA, UFDTLIA, UFDTLIRA, AUFDTLIA, AUFDTLIRA)

Solver Single Query Track
2018-CVC4n X
2018-Z3n X
2019-CVC4n X
2019-Par4n X
Alt-Ergo X
CVC4 X
SMTInterpol-fixedn X
SMTInterpol X
UltimateEliminator+MathSAT X
Vampire X
veriT+viten X
veriT X
z3n X
Total - competing 6
Total - non-competing 7
Total 13

Equality+NonLinearArith (AUFDTNIRA, UFDTNIA, UFDTNIRA, AUFNIA, AUFNIRA, UFNIA)

Solver Single Query Track
2018-Vampiren X
2019-Par4n X
2019-Vampiren X
Alt-Ergo X
CVC4 X
UltimateEliminator+MathSAT X
Vampire X
z3n X
Total - competing 4
Total - non-competing 4
Total 8

Equality+MachineArith (AUFFPDTLIRA, UFFPDTLIRA, UFFPDTNIRA, ABVFP, ABVFPLRA, UFBV, AUFBVDTLIA)

Solver Single Query Track
2018-CVC4n X
2018-Z3n X
2019-Par4n X
CVC4 X
UltimateEliminator+MathSAT X
z3n X
Total - competing 2
Total - non-competing 4
Total 6

FPArith (BVFP, FP, BVFPLRA, FPLRA)

Solver Single Query Track
2019-Z3n X
CVC4 X
UltimateEliminator+MathSAT X
z3n X
Total - competing 2
Total - non-competing 2
Total 4