SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Previous Competitions
SMT-LIB

SMT-COMP 2020

Rules
Benchmarks
Tools
Specs
Participants

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 Incremental Track Unsat Core Track Model Validation Track Preliminary Solver ID Final Solver ID Seed System Description
AProVE X 1229 1229 31249347 AProVE at SMT-COMP 2020
Alt-Ergo X 28077 28634 42 Alt-Ergo
Bitwuzla X X X X 28351 28818 42 Bitwuzla at the SMT Competition 2020
COLIBRI X 28309 28737 101 COLIBRI
CVC4-inc X 28466 28799 94305 CVC4 at the SMT Competition 2020
CVC4-mv X 28356 28801 94305 CVC4 at the SMT Competition 2020
CVC4-uc X 28357 28800 94305 CVC4 at the SMT Competition 2020
CVC4 X 28354 28798 94305 CVC4 at the SMT Competition 2020
LazyBV2Int X X 28568 28722 670 LazyBV2Int at the SMT Competition 2020
MathSAT5-mvn X 28907 28907 0
MathSAT5n X X X 28851 28851 0
MinkeyRink X 23719 28838 9595959 MinkeyRink 2020.0
OpenSMT X X 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 X X X X 28544 28784 192843011 SMTInterpol
STP + CMS X X X 23663 28776 20200504 STP in the SMTCOMP 2020
STP + MergeSAT X X X 23401 28841 11111111 STP in the SMTCOMP 2020
UltimateEliminator+MathSAT X X X 28584 28846 0 UltimateEliminator
Vampire X 28324 28782 4329 Vampire 4.5-SMT System Description
Yices2 X X 28343 28820 87654 Yices 2 in SMT-COMP 2020
Yices2 Model Validation X 28464 28819 98765 Yices 2 in SMT-COMP 2020
Yices2 incremental X 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 X X X 28814 28814 0
Total - competing 20 9 5 7
Total - non-competing 3 2 2 2
Total 23 11 7 9 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.

ABV

Solver Single Query Track Unsat Core Track
CVC4-uc X
CVC4 X
UltimateEliminator+MathSAT X X
z3n X X
Total - competing 2 2
Total - non-competing 1 1
Total 3 3

ABVFP

Solver Single Query Track Incremental Track Unsat Core Track
CVC4-inc X
CVC4-uc X
CVC4 X
UltimateEliminator+MathSAT X X X
Total - competing 2 2 2
Total - non-competing 0 0 0
Total 2 2 2

ABVFPLRA

Solver Single Query Track Unsat Core Track
CVC4-uc X
CVC4 X
UltimateEliminator+MathSAT X X
Total - competing 2 2
Total - non-competing 0 0
Total 2 2

ALIA

Solver Single Query Track Incremental Track Unsat Core Track
Alt-Ergo X
CVC4-inc X
CVC4-uc X
CVC4 X
SMTInterpol X X X
UltimateEliminator+MathSAT X X X
Vampire X
veriT+viten X
veriT X
z3n X X X
Total - competing 6 3 3
Total - non-competing 2 1 1
Total 8 4 4

ANIA

Solver Incremental Track
CVC4-inc X
UltimateEliminator+MathSAT X
Total - competing 2
Total - non-competing 0
Total 2

AUFBVDTLIA

Solver Single Query Track Unsat Core Track
CVC4-uc X
CVC4 X
UltimateEliminator+MathSAT X X
Total - competing 2 2
Total - non-competing 0 0
Total 2 2

AUFBVDTNIA

Solver Single Query Track Unsat Core Track
Total - competing 0 0
Total - non-competing 0 0
Total 0 0

AUFDTLIA

Solver Single Query Track Unsat Core Track
Alt-Ergo X
CVC4-uc X
CVC4 X
UltimateEliminator+MathSAT X X
Vampire X
Total - competing 4 2
Total - non-competing 0 0
Total 4 2

AUFDTLIRA

Solver Single Query Track Unsat Core Track
Alt-Ergo X
CVC4-uc X
CVC4 X
UltimateEliminator+MathSAT X X
Vampire X
Total - competing 4 2
Total - non-competing 0 0
Total 4 2

AUFDTNIRA

Solver Single Query Track Unsat Core Track
Alt-Ergo X
CVC4-uc X
CVC4 X
UltimateEliminator+MathSAT X X
Vampire X
Total - competing 4 2
Total - non-competing 0 0
Total 4 2

AUFFPDTLIRA

Solver Single Query Track Unsat Core Track
CVC4-uc X
CVC4 X
UltimateEliminator+MathSAT X X
Total - competing 2 2
Total - non-competing 0 0
Total 2 2

AUFFPDTNIRA

Solver Single Query Track Unsat Core Track
Total - competing 0 0
Total - non-competing 0 0
Total 0 0

AUFLIA

Solver Single Query Track Unsat Core Track
Alt-Ergo X
CVC4-uc X
CVC4 X
SMTInterpol X X
UltimateEliminator+MathSAT X X
Vampire X
veriT+viten X
veriT X
z3n X X
Total - competing 6 3
Total - non-competing 2 1
Total 8 4

AUFLIRA

Solver Single Query Track Unsat Core Track
Alt-Ergo X
CVC4-uc X
CVC4 X
SMTInterpol X X
UltimateEliminator+MathSAT X X
Vampire X
veriT+viten X
veriT X
z3n X X
Total - competing 6 3
Total - non-competing 2 1
Total 8 4

AUFNIA

Solver Single Query Track Unsat Core Track
Alt-Ergo X
CVC4-uc X
CVC4 X
UltimateEliminator+MathSAT X X
Vampire X
z3n X X
Total - competing 4 2
Total - non-competing 1 1
Total 5 3

AUFNIRA

Solver Single Query Track Incremental Track Unsat Core Track
Alt-Ergo X
CVC4-inc X
CVC4-uc X
CVC4 X
UltimateEliminator+MathSAT X X X
Vampire X
z3n X X X
Total - competing 4 2 2
Total - non-competing 1 1 1
Total 5 3 3

BV

Solver Single Query Track Incremental Track Unsat Core Track
Bitwuzla X
CVC4-inc X
CVC4-uc X
CVC4 X
UltimateEliminator+MathSAT X X X
z3n X X X
Total - competing 3 2 2
Total - non-competing 1 1 1
Total 4 3 3

BVFP

Solver Single Query Track Incremental Track Unsat Core Track
CVC4-inc X
CVC4-uc X
CVC4 X
UltimateEliminator+MathSAT X X X
Total - competing 2 2 2
Total - non-competing 0 0 0
Total 2 2 2

BVFPLRA

Solver Single Query Track Unsat Core Track
CVC4-uc X
CVC4 X
UltimateEliminator+MathSAT X X
Total - competing 2 2
Total - non-competing 0 0
Total 2 2

FP

Solver Single Query Track Unsat Core Track
CVC4-uc X
CVC4 X
UltimateEliminator+MathSAT X X
z3n X X
Total - competing 2 2
Total - non-competing 1 1
Total 3 3

FPLRA

Solver Single Query Track Unsat Core Track
CVC4-uc X
CVC4 X
UltimateEliminator+MathSAT X X
Total - competing 2 2
Total - non-competing 0 0
Total 2 2

LIA

Solver Single Query Track Incremental Track Unsat Core Track
CVC4-inc X
CVC4-uc X
CVC4 X
SMTInterpol X X X
UltimateEliminator+MathSAT X X X
Vampire X
veriT+viten X
veriT X
z3n X X X
Total - competing 5 3 3
Total - non-competing 2 1 1
Total 7 4 4

LRA

Solver Single Query Track Incremental Track Unsat Core Track
CVC4-inc X
CVC4-uc X
CVC4 X
SMTInterpol X X X
UltimateEliminator+MathSAT X X X
Vampire X
z3n X X X
Total - competing 4 3 3
Total - non-competing 1 1 1
Total 5 4 4

NIA

Solver Single Query Track Unsat Core Track
CVC4-uc X
CVC4 X
UltimateEliminator+MathSAT X X
Vampire X
z3n X X
Total - competing 3 2
Total - non-competing 1 1
Total 4 3

NRA

Solver Single Query Track Unsat Core Track
CVC4-uc X
CVC4 X
UltimateEliminator+MathSAT X X
Vampire X
z3n X X
Total - competing 3 2
Total - non-competing 1 1
Total 4 3

QF_ABV

Solver Single Query Track Incremental Track Unsat Core Track
Bitwuzla X X X
CVC4-inc X
CVC4-uc X
CVC4 X
MathSAT5n X X X
Yices2 X X
Yices2 incremental X
z3n X X X
Total - competing 3 3 3
Total - non-competing 2 2 2
Total 5 5 5

QF_ABVFP

Solver Single Query Track Incremental Track Unsat Core Track
Bitwuzla X X X
COLIBRI X
CVC4-inc X
CVC4-uc X
CVC4 X
MathSAT5n X X X
Total - competing 3 2 2
Total - non-competing 1 1 1
Total 4 3 3

QF_ABVFPLRA

Solver Single Query Track Unsat Core Track
COLIBRI X
CVC4-uc X
CVC4 X
MathSAT5n X X
Total - competing 2 1
Total - non-competing 1 1
Total 3 2

QF_ALIA

Solver Single Query Track Incremental Track Unsat Core Track
Alt-Ergo X
CVC4-inc X
CVC4-uc X
CVC4 X
MathSAT5n X X X
SMTInterpol X X X
Yices2 X X
Yices2 incremental X
veriT X
z3n X X X
Total - competing 5 3 3
Total - non-competing 2 2 2
Total 7 5 5

QF_ANIA

Solver Single Query Track Incremental Track Unsat Core Track
Alt-Ergo X
CVC4-inc X
CVC4-uc X
CVC4 X
MathSAT5n X X X
z3n X X X
Total - competing 2 1 1
Total - non-competing 2 2 2
Total 4 3 3

QF_AUFBV

Solver Single Query Track Incremental Track Unsat Core Track
Bitwuzla X X X
CVC4-inc X
CVC4-uc X
CVC4 X
MathSAT5n X X X
Yices2 X X
Yices2 incremental X
z3n X X X
Total - competing 3 3 3
Total - non-competing 2 2 2
Total 5 5 5

QF_AUFBVLIA

Solver Incremental Track
CVC4-inc X
MathSAT5n X
Total - competing 1
Total - non-competing 1
Total 2

QF_AUFBVNIA

Solver Incremental Track
CVC4-inc X
MathSAT5n X
Total - competing 1
Total - non-competing 1
Total 2

QF_AUFLIA

Solver Single Query Track Incremental Track Unsat Core Track
Alt-Ergo X
CVC4-inc X
CVC4-uc X
CVC4 X
MathSAT5n X X X
SMTInterpol X X X
Yices2 X X
Yices2 incremental X
veriT X
z3n X X X
Total - competing 5 3 3
Total - non-competing 2 2 2
Total 7 5 5

QF_AUFNIA

Solver Single Query Track Unsat Core Track
Alt-Ergo X
CVC4-uc X
CVC4 X
MathSAT5n X X
z3n X X
Total - competing 2 1
Total - non-competing 2 2
Total 4 3

QF_AX

Solver Single Query Track Unsat Core Track
Alt-Ergo X
CVC4-uc X
CVC4 X
MathSAT5n X X
SMTInterpol X X
Yices2 X X
z3n X X
Total - competing 4 3
Total - non-competing 2 2
Total 6 5

QF_BV

Solver Single Query Track Incremental Track Unsat Core Track Model Validation Track
Bitwuzla X X X X
CVC4-inc X
CVC4-mv X
CVC4-uc X
CVC4 X
LazyBV2Int X X
MathSAT5-mvn X
MathSAT5n X X X
MinkeyRink X
STP + CMS X X X
STP + MergeSAT X X X
Yices2 X X
Yices2 Model Validation X
Yices2 incremental X
z3n X X X X
Total - competing 7 6 3 5
Total - non-competing 2 2 2 2
Total 9 8 5 7

QF_BVFP

Solver Single Query Track Incremental Track Unsat Core Track
Bitwuzla X X X
COLIBRI X
CVC4-inc X
CVC4-uc X
CVC4 X
MathSAT5n X X X
z3n X X X
Total - competing 3 2 2
Total - non-competing 2 2 2
Total 5 4 4

QF_BVFPLRA

Solver Single Query Track Unsat Core Track
COLIBRI X
CVC4-uc X
CVC4 X
MathSAT5n X X
Total - competing 2 1
Total - non-competing 1 1
Total 3 2

QF_DT

Solver Single Query Track Unsat Core Track
Alt-Ergo X
CVC4-uc X
CVC4 X
z3n X X
Total - competing 2 1
Total - non-competing 1 1
Total 3 2

QF_FP

Solver Single Query Track Incremental Track Unsat Core Track
Bitwuzla X X X
COLIBRI X
CVC4-inc X
CVC4-uc X
CVC4 X
MathSAT5n X X X
z3n X X X
Total - competing 3 2 2
Total - non-competing 2 2 2
Total 5 4 4

QF_FPLRA

Solver Single Query Track Unsat Core Track
COLIBRI X
CVC4-uc X
CVC4 X
MathSAT5n X X
z3n X X
Total - competing 2 1
Total - non-competing 2 2
Total 4 3

QF_IDL

Solver Single Query Track Unsat Core Track Model Validation Track
CVC4-mv X
CVC4-uc X
CVC4 X
MathSAT5-mvn X
MathSAT5n X X
SMTInterpol X X X
Yices2 X X
Yices2 Model Validation X
veriT X
z3n X X X
Total - competing 4 3 3
Total - non-competing 2 2 2
Total 6 5 5

QF_LIA

Solver Single Query Track Incremental Track Unsat Core Track Model Validation Track
CVC4-inc X
CVC4-mv X
CVC4-uc X
CVC4 X
MathSAT5-mvn X
MathSAT5n X X X
SMTInterpol X X X X
Yices2 X X
Yices2 Model Validation X
Yices2 incremental X
veriT X
z3n X X X X
Total - competing 4 3 3 3
Total - non-competing 2 2 2 2
Total 6 5 5 5

QF_LIRA

Solver Single Query Track Unsat Core Track Model Validation Track
CVC4-mv X
CVC4-uc X
CVC4 X
MathSAT5-mvn X
MathSAT5n X X
SMTInterpol X X X
Yices2 X X
Yices2 Model Validation X
z3n X X X
Total - competing 3 3 3
Total - non-competing 2 2 2
Total 5 5 5

QF_LRA

Solver Single Query Track Incremental Track Unsat Core Track Model Validation Track
CVC4-inc X
CVC4-mv X
CVC4-uc X
CVC4 X
MathSAT5-mvn X
MathSAT5n X X X
OpenSMT X X X
SMTInterpol X X X X
Yices2 X X
Yices2 Model Validation X
Yices2 incremental X
veriT X
z3n X X X X
Total - competing 5 4 3 4
Total - non-competing 2 2 2 2
Total 7 6 5 6

QF_NIA

Solver Single Query Track Incremental Track Unsat Core Track
AProVE X
CVC4-inc X
CVC4-uc X
CVC4 X
MathSAT5n X X X
SMT-RAT X
Yices2 X
Yices2 incremental X
z3n X X X
Total - competing 4 2 1
Total - non-competing 2 2 2
Total 6 4 3

QF_NIRA

Solver Single Query Track Unsat Core Track
CVC4-uc X
CVC4 X
MathSAT5n X X
SMT-RAT X
Yices2 X
z3n X X
Total - competing 3 1
Total - non-competing 2 2
Total 5 3

QF_NRA

Solver Single Query Track Unsat Core Track
CVC4-uc X
CVC4 X
MathSAT5n X X
SMT-RAT-CAlC X
SMT-RAT-MCSAT X
Yices2 X
veriT+raSAT+Redlog X
z3n X X
Total - competing 5 1
Total - non-competing 2 2
Total 7 3

QF_RDL

Solver Single Query Track Unsat Core Track Model Validation Track
CVC4-mv X
CVC4-uc X
CVC4 X
MathSAT5-mvn X
MathSAT5n X X
SMTInterpol X X X
Yices2 X X
Yices2 Model Validation X
veriT X
z3n X X X
Total - competing 4 3 3
Total - non-competing 2 2 2
Total 6 5 5

QF_S

Solver Single Query Track Unsat Core Track
CVC4-uc X
CVC4 X
Z3str4 X
Total - competing 2 1
Total - non-competing 0 0
Total 2 1

QF_SLIA

Solver Single Query Track Unsat Core Track
CVC4-uc X
CVC4 X
Z3str4 X
Total - competing 2 1
Total - non-competing 0 0
Total 2 1

QF_UF

Solver Single Query Track Incremental Track Unsat Core Track
Alt-Ergo X
CVC4-inc X
CVC4-uc X
CVC4 X
MathSAT5n X X X
OpenSMT X X
SMTInterpol X X X
Yices2 X X
Yices2 incremental X
veriT X
z3n X X X
Total - competing 6 4 3
Total - non-competing 2 2 2
Total 8 6 5

QF_UFBV

Solver Single Query Track Incremental Track Unsat Core Track
Bitwuzla X X X
CVC4-inc X
CVC4-uc X
CVC4 X
MathSAT5n X X X
Yices2 X X
Yices2 incremental X
z3n X X X
Total - competing 3 3 3
Total - non-competing 2 2 2
Total 5 5 5

QF_UFBVLIA

Solver Incremental Track
CVC4-inc X
MathSAT5n X
Total - competing 1
Total - non-competing 1
Total 2

QF_UFFP

Solver Single Query Track Incremental Track Unsat Core Track
Bitwuzla X X X
COLIBRI X
CVC4-inc X
CVC4-uc X
CVC4 X
MathSAT5n X X X
Total - competing 3 2 2
Total - non-competing 1 1 1
Total 4 3 3

QF_UFIDL

Solver Single Query Track Unsat Core Track
CVC4-uc X
CVC4 X
MathSAT5n X X
SMTInterpol X X
Yices2 X X
veriT X
z3n X X
Total - competing 4 3
Total - non-competing 2 2
Total 6 5

QF_UFLIA

Solver Single Query Track Incremental Track Unsat Core Track
Alt-Ergo X
CVC4-inc X
CVC4-uc X
CVC4 X
MathSAT5n X X X
SMTInterpol X X X
Yices2 X X
Yices2 incremental X
veriT X
z3n X X X
Total - competing 5 3 3
Total - non-competing 2 2 2
Total 7 5 5

QF_UFLRA

Solver Single Query Track Incremental Track Unsat Core Track
Alt-Ergo X
CVC4-inc X
CVC4-uc X
CVC4 X
MathSAT5n X X X
SMTInterpol X X X
Yices2 X X
Yices2 incremental X
veriT X
z3n X X X
Total - competing 5 3 3
Total - non-competing 2 2 2
Total 7 5 5

QF_UFNIA

Solver Single Query Track Incremental Track Unsat Core Track
Alt-Ergo X
CVC4-inc X
CVC4-uc X
CVC4 X
MathSAT5n X X X
Yices2 X
Yices2 incremental X
z3n X X X
Total - competing 3 2 1
Total - non-competing 2 2 2
Total 5 4 3

QF_UFNRA

Solver Single Query Track Unsat Core Track
Alt-Ergo X
CVC4-uc X
CVC4 X
MathSAT5n X X
Yices2 X
veriT+raSAT+Redlog X
z3n X X
Total - competing 4 1
Total - non-competing 2 2
Total 6 3

UF

Solver Single Query Track Incremental Track Unsat Core Track
Alt-Ergo X
CVC4-inc X
CVC4-uc X
CVC4 X
SMTInterpol X X X
UltimateEliminator+MathSAT X X X
Vampire X
veriT+viten X
veriT X
z3n X X X
Total - competing 6 3 3
Total - non-competing 2 1 1
Total 8 4 4

UFBV

Solver Single Query Track Unsat Core Track
CVC4-uc X
CVC4 X
UltimateEliminator+MathSAT X X
z3n X X
Total - competing 2 2
Total - non-competing 1 1
Total 3 3

UFDT

Solver Single Query Track Unsat Core Track
Alt-Ergo X
CVC4-uc X
CVC4 X
UltimateEliminator+MathSAT X X
Vampire X
Total - competing 4 2
Total - non-competing 0 0
Total 4 2

UFDTLIA

Solver Single Query Track Unsat Core Track
Alt-Ergo X
CVC4-uc X
CVC4 X
UltimateEliminator+MathSAT X X
Vampire X
Total - competing 4 2
Total - non-competing 0 0
Total 4 2

UFDTLIRA

Solver Single Query Track Unsat Core Track
Alt-Ergo X
CVC4-uc X
CVC4 X
UltimateEliminator+MathSAT X X
Vampire X
Total - competing 4 2
Total - non-competing 0 0
Total 4 2

UFDTNIA

Solver Single Query Track Unsat Core Track
Alt-Ergo X
CVC4-uc X
CVC4 X
UltimateEliminator+MathSAT X X
Vampire X
Total - competing 4 2
Total - non-competing 0 0
Total 4 2

UFDTNIRA

Solver Single Query Track Unsat Core Track
Alt-Ergo X
CVC4-uc X
CVC4 X
UltimateEliminator+MathSAT X X
Vampire X
Total - competing 4 2
Total - non-competing 0 0
Total 4 2

UFFPDTLIRA

Solver Single Query Track Unsat Core Track
CVC4-uc X
CVC4 X
UltimateEliminator+MathSAT X X
Total - competing 2 2
Total - non-competing 0 0
Total 2 2

UFFPDTNIRA

Solver Single Query Track Unsat Core Track
CVC4-uc X
CVC4 X
UltimateEliminator+MathSAT X X
Total - competing 2 2
Total - non-competing 0 0
Total 2 2

UFIDL

Solver Single Query Track Unsat Core Track
CVC4-uc X
CVC4 X
SMTInterpol X X
UltimateEliminator+MathSAT X X
Vampire X
veriT+viten X
veriT X
z3n X X
Total - competing 5 3
Total - non-competing 2 1
Total 7 4

UFLIA

Solver Single Query Track Unsat Core Track
Alt-Ergo X
CVC4-uc X
CVC4 X
SMTInterpol X X
UltimateEliminator+MathSAT X X
Vampire X
veriT+viten X
veriT X
z3n X X
Total - competing 6 3
Total - non-competing 2 1
Total 8 4

UFLRA

Solver Single Query Track Incremental Track Unsat Core Track
Alt-Ergo X
CVC4-inc X
CVC4-uc X
CVC4 X
SMTInterpol X X X
UltimateEliminator+MathSAT X X X
Vampire X
veriT+viten X
veriT X
z3n X X X
Total - competing 6 3 3
Total - non-competing 2 1 1
Total 8 4 4

UFNIA

Solver Single Query Track Incremental Track Unsat Core Track
Alt-Ergo X
CVC4-inc X
CVC4-uc X
CVC4 X
UltimateEliminator+MathSAT X X X
Vampire X
z3n X X X
Total - competing 4 2 2
Total - non-competing 1 1 1
Total 5 3 3

UFNRA

Solver Incremental Track
CVC4-inc X
UltimateEliminator+MathSAT X
z3n X
Total - competing 2
Total - non-competing 1
Total 3