SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Competitions by Year

SMT-COMP 2020

Rules
Benchmarks
Tools
Specs
Participants
Results
Slides

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
2018-Boolector (incremental)n X 19991
2018-CVC4n X 19775
2018-CVC4 (incremental)n X 19992
2018-CVC4 (unsat core)n X 19793
2018-MathSAT (incremental)n X 19993
2018-SMTRAT-Ratn X 19783
2018-Vampiren X 19788
2018-Yicesn X 19791
2018-Yices (incremental)n X 19995
2018-Yices (unsat core)n X 19796
2018-Z3n X 19792
2018-Z3 (incremental)n X 19996
2018-Z3 (unsat core)n X 19797
2019-Boolectorn X X 23380 23711 Boolector
2019-CVC4-incn X 23417 23733 CVC4
2019-CVC4-ucn X 23416 23732 CVC4
2019-CVC4n X 23420 23737 CVC4
2019-MathSAT-defaultn X X X 23373 23680 MathSAT5
2019-MathSAT-na-extn X X 23427 23679 MathSAT5
2019-Par4n X 23391 23672 Par4
2019-Poolectorn X 23384 23730 Boolector
2019-SMTInterpoln X 23360 23554 SMTInterpol
2019-SPASS-SATTn X 23356 23356 SPASS-SATT
2019-Vampiren X 23409 23703 Vampire
2019-Yices 2.6.2n X X 23363 23694 Yices
2019-Yices 2.6.2 Incrementaln X 23364 23695 Yices
2019-Z3n X X X 23470 23470
AProVE X 1229 1229 31249347 AProVE at SMT-COMP 2020
Alt-Ergo X 28077 28634 42 Alt-Ergo
Bitwuzla-fixedn X X X X 29091 29091 Bitwuzla at the SMT Competition 2020
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-fixedn X 28765 28765 MinkeyRink 2020.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-fixedn X X X X 29030 29030 SMTInterpol
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-fixedn X X 29032 29032 Yices 2 in SMT-COMP 2020
Yices2-fixed Model Validationn X 29033 29033 Yices 2 in SMT-COMP 2020
Yices2-fixed incrementaln X 29034 29034 Yices 2 in SMT-COMP 2020
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 22 15 13 6
Total 42 24 18 13 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
2018-CVC4n X
2019-CVC4-incn X
CVC4-inc X
CVC4-uc X
CVC4 X
UltimateEliminator+MathSAT X X X
Total - competing 2 2 2
Total - non-competing 1 1 0
Total 3 3 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
2018-Z3n X
2018-Z3 (incremental)n X
Alt-Ergo X
CVC4-inc X
CVC4-uc X
CVC4 X
SMTInterpol-fixedn X X 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 4 3 2
Total 10 6 5

ANIA

Solver Incremental Track
2018-CVC4 (incremental)n X
CVC4-inc X
UltimateEliminator+MathSAT X
Total - competing 2
Total - non-competing 1
Total 3

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
2018-CVC4n X
Alt-Ergo X
CVC4-uc X
CVC4 X
UltimateEliminator+MathSAT X X
Vampire X
Total - competing 4 2
Total - non-competing 1 0
Total 5 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
2018-CVC4n X
2018-CVC4 (unsat core)n X
Alt-Ergo X
CVC4-uc X
CVC4 X
SMTInterpol-fixedn X 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 4 3
Total 10 6

AUFLIRA

Solver Single Query Track Unsat Core Track
2018-CVC4 (unsat core)n X
2019-Par4n X
Alt-Ergo X
CVC4-uc X
CVC4 X
SMTInterpol-fixedn X 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 4 3
Total 10 6

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
2019-CVC4-incn X
2019-CVC4-ucn X
2019-Par4n X
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 2 2 2
Total 6 4 4

BV

Solver Single Query Track Incremental Track Unsat Core Track
2019-CVC4-ucn X
2019-Par4n X
2019-Z3n X
Bitwuzla-fixedn X
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 3 2 2
Total 6 4 4

BVFP

Solver Single Query Track Incremental Track Unsat Core Track
2019-CVC4-incn X
2019-Z3n X
CVC4-inc X
CVC4-uc X
CVC4 X
UltimateEliminator+MathSAT X X X
Total - competing 2 2 2
Total - non-competing 1 1 0
Total 3 3 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
2019-Z3n X
CVC4-uc X
CVC4 X
UltimateEliminator+MathSAT X X
z3n X X
Total - competing 2 2
Total - non-competing 2 1
Total 4 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
2018-Z3 (incremental)n X
2018-Z3 (unsat core)n X
2019-Z3n X
CVC4-inc X
CVC4-uc X
CVC4 X
SMTInterpol-fixedn X X 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 4 3 3
Total 9 6 6

LRA

Solver Single Query Track Incremental Track Unsat Core Track
2019-Par4n X
2019-Z3n X
CVC4-inc X
CVC4-uc X
CVC4 X
SMTInterpol-fixedn X X X
SMTInterpol X X X
UltimateEliminator+MathSAT X X X
Vampire X
z3n X X X
Total - competing 4 3 3
Total - non-competing 4 2 2
Total 8 5 5

NIA

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

NRA

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

QF_ABV

Solver Single Query Track Incremental Track Unsat Core Track
2018-Boolector (incremental)n X
2019-Boolectorn X
2019-Par4n X
2019-Z3n X
Bitwuzla-fixedn X X X
Bitwuzla X X X
CVC4-inc X
CVC4-uc X
CVC4 X
MathSAT5n X X X
Yices2-fixedn X X
Yices2-fixed incrementaln X
Yices2 X X
Yices2 incremental X
z3n X X X
Total - competing 3 3 3
Total - non-competing 6 5 5
Total 9 8 8

QF_ABVFP

Solver Single Query Track Incremental Track Unsat Core Track
Bitwuzla-fixedn X X X
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 2 2 2
Total 5 4 4

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
2018-Z3 (incremental)n X
2018-Z3 (unsat core)n X
2019-Yices 2.6.2n X
Alt-Ergo X
CVC4-inc X
CVC4-uc X
CVC4 X
MathSAT5n X X X
SMTInterpol-fixedn X X X
SMTInterpol X X X
Yices2-fixedn X X
Yices2-fixed incrementaln X
Yices2 X X
Yices2 incremental X
veriT X
z3n X X X
Total - competing 5 3 3
Total - non-competing 5 5 5
Total 10 8 8

QF_ANIA

Solver Single Query Track Incremental Track Unsat Core Track
2018-CVC4 (unsat core)n X
2018-Z3 (incremental)n X
2019-CVC4n X
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 3 3 3
Total 5 4 4

QF_AUFBV

Solver Single Query Track Incremental Track Unsat Core Track
2019-Yices 2.6.2n X X
2019-Yices 2.6.2 Incrementaln X
Bitwuzla-fixedn X X X
Bitwuzla X X X
CVC4-inc X
CVC4-uc X
CVC4 X
MathSAT5n X X X
Yices2-fixedn X X
Yices2-fixed incrementaln X
Yices2 X X
Yices2 incremental X
z3n X X X
Total - competing 3 3 3
Total - non-competing 5 5 5
Total 8 8 8

QF_AUFBVLIA

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

QF_AUFBVNIA

Solver Incremental Track
2019-MathSAT-na-extn X
CVC4-inc X
MathSAT5n X
Total - competing 1
Total - non-competing 2
Total 3

QF_AUFLIA

Solver Single Query Track Incremental Track Unsat Core Track
2018-CVC4 (unsat core)n X
2018-Yices (incremental)n X
2019-Yices 2.6.2n X
Alt-Ergo X
CVC4-inc X
CVC4-uc X
CVC4 X
MathSAT5n X X X
SMTInterpol-fixedn X X X
SMTInterpol X X X
Yices2-fixedn X X
Yices2-fixed incrementaln X
Yices2 X X
Yices2 incremental X
veriT X
z3n X X X
Total - competing 5 3 3
Total - non-competing 5 5 5
Total 10 8 8

QF_AUFNIA

Solver Single Query Track Unsat Core Track
2018-Z3 (unsat core)n X
2019-MathSAT-defaultn X
Alt-Ergo X
CVC4-uc X
CVC4 X
MathSAT5n X X
z3n X X
Total - competing 2 1
Total - non-competing 3 3
Total 5 4

QF_AX

Solver Single Query Track Unsat Core Track
2018-Yicesn X
2018-Yices (unsat core)n X
2019-Yices 2.6.2n X
Alt-Ergo X
CVC4-uc X
CVC4 X
MathSAT5n X X
SMTInterpol-fixedn X X
SMTInterpol X X
Yices2-fixedn X X
Yices2 X X
z3n X X
Total - competing 4 3
Total - non-competing 6 5
Total 10 8

QF_BV

Solver Single Query Track Incremental Track Unsat Core Track Model Validation Track
2018-Yices (unsat core)n X
2019-Boolectorn X X
2019-Poolectorn X
2019-Yices 2.6.2 Incrementaln X
Bitwuzla-fixedn X X X X
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-fixedn X
MinkeyRink X
STP + CMS X X X
STP + MergeSAT X X X
Yices2-fixedn X X
Yices2-fixed Model Validationn X
Yices2-fixed incrementaln 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 7 5 5 5
Total 14 11 8 10

QF_BVFP

Solver Single Query Track Incremental Track Unsat Core Track
2019-Par4n X
Bitwuzla-fixedn X X X
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 4 3 3
Total 7 5 5

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
2018-CVC4n X
Alt-Ergo X
CVC4-uc X
CVC4 X
z3n X X
Total - competing 2 1
Total - non-competing 2 1
Total 4 2

QF_FP

Solver Single Query Track Incremental Track Unsat Core Track
2019-Par4n X
Bitwuzla-fixedn X X X
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 4 3 3
Total 7 5 5

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
2019-Par4n X
2019-Z3n X
CVC4-mv X
CVC4-uc X
CVC4 X
MathSAT5-mvn X
MathSAT5n X X
SMTInterpol-fixedn X X X
SMTInterpol X X X
Yices2-fixedn X X
Yices2-fixed Model Validationn X
Yices2 X X
Yices2 Model Validation X
veriT X
z3n X X X
Total - competing 4 3 3
Total - non-competing 6 4 4
Total 10 7 7

QF_LIA

Solver Single Query Track Incremental Track Unsat Core Track Model Validation Track
2018-Yices (incremental)n X
2019-Par4n X
2019-Yices 2.6.2n X
CVC4-inc X
CVC4-mv X
CVC4-uc X
CVC4 X
MathSAT5-mvn X
MathSAT5n X X X
SMTInterpol-fixedn X X X X
SMTInterpol X X X X
Yices2-fixedn X X
Yices2-fixed Model Validationn X
Yices2-fixed incrementaln 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 5 5 5 4
Total 9 8 8 7

QF_LIRA

Solver Single Query Track Unsat Core Track Model Validation Track
2019-Par4n X
CVC4-mv X
CVC4-uc X
CVC4 X
MathSAT5-mvn X
MathSAT5n X X
SMTInterpol-fixedn X X X
SMTInterpol X X X
Yices2-fixedn X X
Yices2-fixed Model Validationn X
Yices2 X X
Yices2 Model Validation X
z3n X X X
Total - competing 3 3 3
Total - non-competing 5 4 4
Total 8 7 7

QF_LRA

Solver Single Query Track Incremental Track Unsat Core Track Model Validation Track
2018-MathSAT (incremental)n X
2019-Par4n X
2019-SPASS-SATTn X
2019-Yices 2.6.2n X
CVC4-inc X
CVC4-mv X
CVC4-uc X
CVC4 X
MathSAT5-mvn X
MathSAT5n X X X
OpenSMT X X X
SMTInterpol-fixedn X X X X
SMTInterpol X X X X
Yices2-fixedn X X
Yices2-fixed Model Validationn X
Yices2-fixed incrementaln 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 6 5 5 4
Total 11 9 8 8

QF_NIA

Solver Single Query Track Incremental Track Unsat Core Track
2019-MathSAT-defaultn X X
2019-Par4n X
AProVE X
CVC4-inc X
CVC4-uc X
CVC4 X
MathSAT5n X X X
SMT-RAT X
Yices2-fixedn X
Yices2-fixed incrementaln X
Yices2 X
Yices2 incremental X
z3n X X X
Total - competing 4 2 1
Total - non-competing 4 4 3
Total 8 6 4

QF_NIRA

Solver Single Query Track Unsat Core Track
2018-SMTRAT-Ratn X
2019-MathSAT-na-extn X
CVC4-uc X
CVC4 X
MathSAT5n X X
SMT-RAT X
Yices2-fixedn X
Yices2 X
z3n X X
Total - competing 3 1
Total - non-competing 4 3
Total 7 4

QF_NRA

Solver Single Query Track Unsat Core Track
2018-CVC4 (unsat core)n X
2019-Par4n X
CVC4-uc X
CVC4 X
MathSAT5n X X
SMT-RAT-CAlC X
SMT-RAT-MCSAT X
Yices2-fixedn X
Yices2 X
veriT+raSAT+Redlog X
z3n X X
Total - competing 5 1
Total - non-competing 4 3
Total 9 4

QF_RDL

Solver Single Query Track Unsat Core Track Model Validation Track
2019-Yices 2.6.2n X
CVC4-mv X
CVC4-uc X
CVC4 X
MathSAT5-mvn X
MathSAT5n X X
SMTInterpol-fixedn X X X
SMTInterpol X X X
Yices2-fixedn X X
Yices2-fixed Model Validationn X
Yices2 X X
Yices2 Model Validation X
veriT X
z3n X X X
Total - competing 4 3 3
Total - non-competing 5 4 4
Total 9 7 7

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
2019-Par4n X
2019-Yices 2.6.2n X X
2019-Yices 2.6.2 Incrementaln X
Alt-Ergo X
CVC4-inc X
CVC4-uc X
CVC4 X
MathSAT5n X X X
OpenSMT X X
SMTInterpol-fixedn X X X
SMTInterpol X X X
Yices2-fixedn X X
Yices2-fixed incrementaln X
Yices2 X X
Yices2 incremental X
veriT X
z3n X X X
Total - competing 6 4 3
Total - non-competing 6 5 5
Total 12 9 8

QF_UFBV

Solver Single Query Track Incremental Track Unsat Core Track
2018-Boolector (incremental)n X
2018-Z3 (unsat core)n X
2019-Yices 2.6.2n X
Bitwuzla-fixedn X X X
Bitwuzla X X X
CVC4-inc X
CVC4-uc X
CVC4 X
MathSAT5n X X X
Yices2-fixedn X X
Yices2-fixed incrementaln X
Yices2 X X
Yices2 incremental X
z3n X X X
Total - competing 3 3 3
Total - non-competing 5 5 5
Total 8 8 8

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-fixedn X X X
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 2 2 2
Total 5 4 4

QF_UFIDL

Solver Single Query Track Unsat Core Track
2018-Yices (unsat core)n X
2019-Yices 2.6.2n X X
CVC4-uc X
CVC4 X
MathSAT5n X X
SMTInterpol-fixedn X X
SMTInterpol X X
Yices2-fixedn X X
Yices2 X X
veriT X
z3n X X
Total - competing 4 3
Total - non-competing 5 6
Total 9 9

QF_UFLIA

Solver Single Query Track Incremental Track Unsat Core Track
2018-Yicesn X
2018-Z3 (incremental)n X
2019-Yices 2.6.2n X
Alt-Ergo X
CVC4-inc X
CVC4-uc X
CVC4 X
MathSAT5n X X X
SMTInterpol-fixedn X X X
SMTInterpol X X X
Yices2-fixedn X X
Yices2-fixed incrementaln X
Yices2 X X
Yices2 incremental X
veriT X
z3n X X X
Total - competing 5 3 3
Total - non-competing 5 5 5
Total 10 8 8

QF_UFLRA

Solver Single Query Track Incremental Track Unsat Core Track
2019-SMTInterpoln X
2019-Z3n X X
Alt-Ergo X
CVC4-inc X
CVC4-uc X
CVC4 X
MathSAT5n X X X
SMTInterpol-fixedn X X X
SMTInterpol X X X
Yices2-fixedn X X
Yices2-fixed incrementaln X
Yices2 X X
Yices2 incremental X
veriT X
z3n X X X
Total - competing 5 3 3
Total - non-competing 5 5 5
Total 10 8 8

QF_UFNIA

Solver Single Query Track Incremental Track Unsat Core Track
2018-Z3 (unsat core)n X
2019-CVC4n X
2019-MathSAT-defaultn X
Alt-Ergo X
CVC4-inc X
CVC4-uc X
CVC4 X
MathSAT5n X X X
Yices2-fixedn X
Yices2-fixed incrementaln X
Yices2 X
Yices2 incremental X
z3n X X X
Total - competing 3 2 1
Total - non-competing 4 4 3
Total 7 6 4

QF_UFNRA

Solver Single Query Track Unsat Core Track
2018-Z3 (unsat core)n X
2019-Par4n X
Alt-Ergo X
CVC4-uc X
CVC4 X
MathSAT5n X X
Yices2-fixedn X
Yices2 X
veriT+raSAT+Redlog X
z3n X X
Total - competing 4 1
Total - non-competing 4 3
Total 8 4

UF

Solver Single Query Track Incremental Track Unsat Core Track
2018-CVC4 (unsat core)n X
2018-Vampiren X
2019-CVC4n X
Alt-Ergo X
CVC4-inc X
CVC4-uc X
CVC4 X
SMTInterpol-fixedn X X 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 5 2 3
Total 11 5 6

UFBV

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

UFDT

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

UFDTLIA

Solver Single Query Track Unsat Core Track
2019-CVC4n X
Alt-Ergo X
CVC4-uc X
CVC4 X
UltimateEliminator+MathSAT X X
Vampire X
Total - competing 4 2
Total - non-competing 1 0
Total 5 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
2019-Vampiren X
Alt-Ergo X
CVC4-uc X
CVC4 X
UltimateEliminator+MathSAT X X
Vampire X
Total - competing 4 2
Total - non-competing 1 0
Total 5 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
2018-CVC4 (unsat core)n X
2019-CVC4-ucn X
2019-Par4n X
CVC4-uc X
CVC4 X
SMTInterpol-fixedn X 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 4 4
Total 9 7

UFLIA

Solver Single Query Track Unsat Core Track
2018-CVC4 (unsat core)n X
2019-Par4n X
Alt-Ergo X
CVC4-uc X
CVC4 X
SMTInterpol-fixedn X 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 4 3
Total 10 6

UFLRA

Solver Single Query Track Incremental Track Unsat Core Track
2018-Z3n X
2018-Z3 (unsat core)n X
2019-Z3n X
Alt-Ergo X
CVC4-inc X
CVC4-uc X
CVC4 X
SMTInterpol-fixedn X X 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 4 3 3
Total 10 6 6

UFNIA

Solver Single Query Track Incremental Track Unsat Core Track
2018-CVC4 (unsat core)n X
2018-Vampiren X
2019-Par4n X
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 3 1 2
Total 7 3 4

UFNRA

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