SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions

SMT-COMP 2019

Rules
Benchmarks
Tools
Specs
Participants
Results
Slides

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 (non-incremental) Challenge Track (incremental) Unsat Core Track Model Validation Track (experimental) Preliminary Solver ID Final Solver ID Seed System Description
AProVE X 1229
 1229
 896120349 AProVE
Alt-Ergo X 23333
 23530
 42 Alt-Ergo
Boolector X X X 23380
 23711
 42 Boolector
Boolector (incremental) X X 23381
 23712
 42 Boolector
COLIBRI X 23355
 23355
 614823377508390721 COLIBRI
CVC4-inc X X 23417
 23733
 439 CVC4
CVC4-mv X 23419
 23736
 439 CVC4
CVC4-uc X 23416
 23732
 439 CVC4
CVC4 X X 23420
 23737
 439 CVC4
Ctrl-Ergo X 23398
 23398
 12019 Ctrl-Ergo
MathSAT-default X X X 23373
 23680
 512 MathSAT5
MathSAT-na-ext X X X 23427
 23679
 512 MathSAT5
Minkeyrink Solver X X X X X 23392
 23720
 Minkeyrink Solver
Minkeyrink Solver MT X X X X X 23393
 23719
 Minkeyrink Solver
OpenSMT2 X 23354
 23635
 568 OpenSMT2
Par4 X 23391
 23672
 0 Par4
Poolector X X 23384
 23730
 42 Boolector
ProB X 22647
 23466
 9247 proB
Q3B X X 23405
 23686
 93629305 Q3B
SMT-RAT X 23327
 23731
 SMT-RAT
SMTInterpol X X X 23360
 23554
 983571724 SMTInterpol
SMTRAT-MCSAT X 23328
 23434
 SMT-RAT
SPASS-SATT X 23356
 23356
 73 SPASS-SATT
STP-incremental X X X X 23396
 23687
 1094795585 STP
STP-mergesat X X 23401
 23401
 1094795585 STP
STP-minisat X X 23402
 23402
 1094795585 STP
STP-mt X X X X X 23397
 23663
 1094795585 STP
STP-portfolio X X 23403
 23403
 1094795585 STP
STP-riss X X 23400
 23400
 1094795585 STP
STP X X 23321
 23321
 1094795585 STP
UltimateEliminator+MathSAT-5.5.4 X X X 23425
 23742
 0 UltimateEliminator
UltimateEliminator+SMTInterpol X X X 23426
 23743
 0 UltimateEliminator
UltimateEliminator+Yices-2.6.1 X X X 23423
 23744
 0 UltimateEliminator
Vampire X 23409
 23703
 4051 Vampire
Yices 2.6.2 X X X 23363
 23694
 255 Yices
Yices 2.6.2 CaDiCal X X 23368
 23697
 255 Yices
Yices 2.6.2 CaDiCal/SMT-LIB2 Models X 23371
 23698
 255 Yices
Yices 2.6.2 Cryptominisat X X 23369
 23699
 255 Yices
Yices 2.6.2 Cryptominisat/SMT-LIB2 Models X 23372
 23700
 255 Yices
Yices 2.6.2 Incremental X X 23364
 23695
 255 Yices
Yices 2.6.2 Model Validation X 23365
 23696
 255 Yices
Yices 2.6.2 New Bvsolver X X 23367
 23701
 255 Yices
Yices 2.6.2 New Bvsolver with SMT2 Models X 23370
 23702
 255 Yices
Yices 2.6.2 mcsat-bv X 23366
 23715
 255 Yices
veriT+raSAT+Redlog X 23399
 23399
 13 veriT+raSAT+Redlog
veriT X 23406
 23693
 7800 veriT
2018-Boolectorn X X 19771
2018-Boolector (incremental)n X X 19991
2018-COLIBRIn X 19772
2018-CVC4n X X 19775
2018-CVC4 (incremental)n X 19992
2018-CVC4 (unsat core)n X 19793
2018-MathSAT (incremental)n X X 19993
2018-MathSAT (unsat core)n X 19827
2018-Minkeyrink MTn X X 19777
2018-SMTInterpol (unsat core)n X 19795
2018-SMTRAT-Ratn X 19783
2018-SPASS-SATTn X 19784
2018-Vampiren X 19788
2018-Yicesn X 19791
2018-Yices (incremental)n X 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
Boolector-ReasonLSn X X 23692
 Boolector-ReasonLS
CVC4-SymBreakn X 23746
 CVC4-SymBreak
CVC4-inc-fixedn X X 24474
 CVC4
STP-mergesat-fixedn X X 24232
 STP
STP-portfolio-fixedn X X 24233
 STP
Z3n X X X X X 23470
 23470
Total - competing 37 14 15 7 8 10
Total - non-competing 14 8 6 5 6 0
Total 51 22 21 12 14 10 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

Solver Single Query Track Single Query Track Single Query Track
CVC4-inc X X X
CVC4-uc X X X
CVC4 X X X
UltimateEliminator+MathSAT-5.5.4 X X X
2018-CVC4n X X X
Z3n X X X
Total - competing 4 4 4
Total - non-competing 2 2 2
Total 6 6 6

ALIA

Solver Single Query Track Single Query Track Single Query Track
Alt-Ergo X X X
CVC4-inc X X X
CVC4-uc X X X
CVC4 X X X
SMTInterpol X X X
UltimateEliminator+MathSAT-5.5.4 X X X
UltimateEliminator+SMTInterpol X X X
UltimateEliminator+Yices-2.6.1 X X X
Vampire X X X
veriT X X X
2018-Z3n X X X
2018-Z3 (incremental)n X X X
2018-Z3 (unsat core)n X X X
Z3n X X X
Total - competing 10 10 10
Total - non-competing 4 4 4
Total 14 14 14

ANIA

Solver Single Query Track
CVC4-inc X
UltimateEliminator+MathSAT-5.5.4 X
UltimateEliminator+Yices-2.6.1 X
2018-CVC4 (incremental)n X
Z3n X
Total - competing 3
Total - non-competing 2
Total 5

AUFBVDTLIA

Solver Single Query Track Single Query Track
CVC4-uc X X
CVC4 X X
2018-CVC4n X X
2018-CVC4 (unsat core)n X X
Total - competing 2 2
Total - non-competing 2 2
Total 4 4

AUFDTLIA

Solver Single Query Track Single Query Track
Alt-Ergo X X
CVC4-uc X X
CVC4 X X
Vampire X X
2018-CVC4n X X
Total - competing 4 4
Total - non-competing 1 1
Total 5 5

AUFLIA

Solver Single Query Track Single Query Track
Alt-Ergo X X
CVC4-uc X X
CVC4 X X
SMTInterpol X X
UltimateEliminator+MathSAT-5.5.4 X X
UltimateEliminator+SMTInterpol X X
UltimateEliminator+Yices-2.6.1 X X
Vampire X X
veriT X X
2018-CVC4n X X
2018-CVC4 (unsat core)n X X
CVC4-SymBreakn X X
Z3n X X
Total - competing 9 9
Total - non-competing 4 4
Total 13 13

AUFLIRA

Solver Single Query Track Single Query Track
Alt-Ergo X X
CVC4-uc X X
CVC4 X X
Par4 X X
SMTInterpol X X
UltimateEliminator+MathSAT-5.5.4 X X
UltimateEliminator+SMTInterpol X X
UltimateEliminator+Yices-2.6.1 X X
Vampire X X
veriT X X
2018-CVC4 (unsat core)n X X
2018-Z3n X X
CVC4-SymBreakn X X
Z3n X X
Total - competing 10 10
Total - non-competing 4 4
Total 14 14

AUFNIA

Solver Single Query Track Single Query Track
Alt-Ergo X X
CVC4-uc X X
CVC4 X X
UltimateEliminator+MathSAT-5.5.4 X X
UltimateEliminator+Yices-2.6.1 X X
Vampire X X
CVC4-SymBreakn X X
Z3n X X
Total - competing 6 6
Total - non-competing 2 2
Total 8 8

AUFNIRA

Solver Single Query Track Single Query Track Single Query Track
Alt-Ergo X X X
CVC4-inc X X X
CVC4-uc X X X
CVC4 X X X
Par4 X X X
UltimateEliminator+MathSAT-5.5.4 X X X
UltimateEliminator+Yices-2.6.1 X X X
Vampire X X X
2018-CVC4n X X X
2018-CVC4 (incremental)n X X X
2018-CVC4 (unsat core)n X X X
Z3n X X X
Total - competing 8 8 8
Total - non-competing 4 4 4
Total 12 12 12

BV

Solver Single Query Track Single Query Track Single Query Track
Boolector X X X
CVC4-inc X X X
CVC4-uc X X X
CVC4 X X X
Par4 X X X
Poolector X X X
Q3B X X X
UltimateEliminator+MathSAT-5.5.4 X X X
2018-CVC4n X X X
2018-Z3 (incremental)n X X X
2018-Z3 (unsat core)n X X X
Z3n X X X
Total - competing 8 8 8
Total - non-competing 4 4 4
Total 12 12 12

BVFP

Solver Single Query Track Single Query Track Single Query Track
CVC4-inc X X X
CVC4-uc X X X
CVC4 X X X
UltimateEliminator+MathSAT-5.5.4 X X X
2018-CVC4n X X X
Z3n X X X
Total - competing 4 4 4
Total - non-competing 2 2 2
Total 6 6 6

FP

Solver Single Query Track Single Query Track
CVC4-uc X X
CVC4 X X
UltimateEliminator+MathSAT-5.5.4 X X
2018-CVC4n X X
Z3n X X
Total - competing 3 3
Total - non-competing 2 2
Total 5 5

LIA

Solver Single Query Track Single Query Track Single Query Track
CVC4-inc X X X
CVC4-uc X X X
CVC4 X X X
ProB X X X
SMTInterpol X X X
UltimateEliminator+MathSAT-5.5.4 X X X
UltimateEliminator+SMTInterpol X X X
UltimateEliminator+Yices-2.6.1 X X X
Vampire X X X
veriT X X X
2018-Z3n X X X
2018-Z3 (incremental)n X X X
2018-Z3 (unsat core)n X X X
Z3n X X X
Total - competing 10 10 10
Total - non-competing 4 4 4
Total 14 14 14

LRA

Solver Single Query Track Single Query Track Single Query Track
CVC4-inc X X X
CVC4-uc X X X
CVC4 X X X
Par4 X X X
SMTInterpol X X X
UltimateEliminator+MathSAT-5.5.4 X X X
UltimateEliminator+SMTInterpol X X X
UltimateEliminator+Yices-2.6.1 X X X
Vampire X X X
2018-CVC4 (unsat core)n X X X
2018-Z3n X X X
Z3n X X X
Total - competing 9 9 9
Total - non-competing 3 3 3
Total 12 12 12

NIA

Solver Single Query Track Single Query Track
CVC4-uc X X
CVC4 X X
ProB X X
UltimateEliminator+MathSAT-5.5.4 X X
UltimateEliminator+Yices-2.6.1 X X
Vampire X X
2018-CVC4 (unsat core)n X X
2018-Z3n X X
Z3n X X
Total - competing 6 6
Total - non-competing 3 3
Total 9 9

NRA

Solver Single Query Track Single Query Track
CVC4-uc X X
CVC4 X X
Par4 X X
UltimateEliminator+MathSAT-5.5.4 X X
UltimateEliminator+Yices-2.6.1 X X
Vampire X X
2018-Vampiren X X
2018-Z3n X X
2018-Z3 (unsat core)n X X
Z3n X X
Total - competing 6 6
Total - non-competing 4 4
Total 10 10

QF_ABV

Solver Single Query Track Single Query Track Single Query Track Single Query Track Single Query Track
Boolector X X X X X
Boolector (incremental) X X X X X
CVC4-inc X X X X X
CVC4-uc X X X X X
CVC4 X X X X X
Par4 X X X X X
Poolector X X X X X
Yices 2.6.2 X X X X X
Yices 2.6.2 Incremental X X X X X
2018-Boolectorn X X X X X
2018-Boolector (incremental)n X X X X X
2018-Yices (unsat core)n X X X X X
Z3n X X X X X
Total - competing 9 9 9 9 9
Total - non-competing 4 4 4 4 4
Total 13 13 13 13 13

QF_ABVFP

Solver Single Query Track Single Query Track Single Query Track
CVC4-inc X X X
CVC4-uc X X X
CVC4 X X X
2018-CVC4n X X X
2018-CVC4 (unsat core)n X X X
Z3n X X X
Total - competing 3 3 3
Total - non-competing 3 3 3
Total 6 6 6

QF_ALIA

Solver Single Query Track Single Query Track Single Query Track
Alt-Ergo X X X
CVC4-inc X X X
CVC4-uc X X X
CVC4 X X X
SMTInterpol X X X
Yices 2.6.2 X X X
Yices 2.6.2 Incremental X X X
veriT X X X
2018-Yicesn X X X
2018-Z3 (incremental)n X X X
2018-Z3 (unsat core)n X X X
Z3n X X X
Total - competing 8 8 8
Total - non-competing 4 4 4
Total 12 12 12

QF_ANIA

Solver Single Query Track Single Query Track Single Query Track
Alt-Ergo X X X
CVC4-inc X X X
CVC4-uc X X X
CVC4 X X X
MathSAT-default X X X
MathSAT-na-ext X X X
2018-CVC4 (unsat core)n X X X
2018-Z3n X X X
2018-Z3 (incremental)n X X X
Z3n X X X
Total - competing 6 6 6
Total - non-competing 4 4 4
Total 10 10 10

QF_AUFBV

Solver Single Query Track Single Query Track Single Query Track Single Query Track Single Query Track
Boolector X X X X X
Boolector (incremental) X X X X X
CVC4-inc X X X X X
CVC4-uc X X X X X
CVC4 X X X X X
Poolector X X X X X
Yices 2.6.2 X X X X X
Yices 2.6.2 Incremental X X X X X
2018-CVC4n X X X X X
2018-MathSAT (unsat core)n X X X X X
2018-Yices (incremental)n X X X X X
Z3n X X X X X
Total - competing 8 8 8 8 8
Total - non-competing 4 4 4 4 4
Total 12 12 12 12 12

QF_AUFBVLIA

Solver Single Query Track
CVC4-inc X
Z3n X
Total - competing 1
Total - non-competing 1
Total 2

QF_AUFBVNIA

Solver Single Query Track
CVC4-inc X
MathSAT-default X
MathSAT-na-ext X
Z3n X
Total - competing 3
Total - non-competing 1
Total 4

QF_AUFLIA

Solver Single Query Track Single Query Track Single Query Track
Alt-Ergo X X X
CVC4-inc X X X
CVC4-uc X X X
CVC4 X X X
SMTInterpol X X X
Yices 2.6.2 X X X
Yices 2.6.2 Incremental X X X
veriT X X X
2018-CVC4 (unsat core)n X X X
2018-Yicesn X X X
2018-Yices (incremental)n X X X
Z3n X X X
Total - competing 8 8 8
Total - non-competing 4 4 4
Total 12 12 12

QF_AUFNIA

Solver Single Query Track Single Query Track
Alt-Ergo X X
CVC4-uc X X
CVC4 X X
MathSAT-default X X
MathSAT-na-ext X X
2018-Z3n X X
2018-Z3 (unsat core)n X X
Z3n X X
Total - competing 5 5
Total - non-competing 3 3
Total 8 8

QF_AX

Solver Single Query Track Single Query Track
Alt-Ergo X X
CVC4-uc X X
CVC4 X X
SMTInterpol X X
Yices 2.6.2 X X
2018-Yicesn X X
2018-Yices (unsat core)n X X
Z3n X X
Total - competing 5 5
Total - non-competing 3 3
Total 8 8

QF_BV

Solver Single Query Track Single Query Track Single Query Track Single Query Track Single Query Track Single Query Track
Boolector X X X X X X
Boolector (incremental) X X X X X X
CVC4-inc X X X X X X
CVC4-mv X X X X X X
CVC4-uc X X X X X X
CVC4 X X X X X X
Minkeyrink Solver X X X X X X
Minkeyrink Solver MT X X X X X X
Par4 X X X X X X
Poolector X X X X X X
STP-incremental X X X X X X
STP-mergesat X X X X X X
STP-minisat X X X X X X
STP-mt X X X X X X
STP-portfolio X X X X X X
STP-riss X X X X X X
STP X X X X X X
Yices 2.6.2 X X X X X X
Yices 2.6.2 CaDiCal X X X X X X
Yices 2.6.2 CaDiCal/SMT-LIB2 Models X X X X X X
Yices 2.6.2 Cryptominisat X X X X X X
Yices 2.6.2 Cryptominisat/SMT-LIB2 Models X X X X X X
Yices 2.6.2 Incremental X X X X X X
Yices 2.6.2 Model Validation X X X X X X
Yices 2.6.2 New Bvsolver X X X X X X
Yices 2.6.2 New Bvsolver with SMT2 Models X X X X X X
Yices 2.6.2 mcsat-bv X X X X X X
2018-Boolectorn X X X X X X
2018-MathSAT (incremental)n X X X X X X
2018-Minkeyrink MTn X X X X X X
2018-Yices (unsat core)n X X X X X X
Boolector-ReasonLSn X X X X X X
CVC4-inc-fixedn X X X X X X
STP-mergesat-fixedn X X X X X X
STP-portfolio-fixedn X X X X X X
Z3n X X X X X X
Total - competing 27 27 27 27 27 27
Total - non-competing 9 9 9 9 9 9
Total 36 36 36 36 36 36

QF_BVFP

Solver Single Query Track Single Query Track Single Query Track
CVC4-inc X X X
CVC4-uc X X X
CVC4 X X X
Par4 X X X
2018-CVC4n X X X
2018-CVC4 (incremental)n X X X
2018-CVC4 (unsat core)n X X X
Z3n X X X
Total - competing 4 4 4
Total - non-competing 4 4 4
Total 8 8 8

QF_BVFPLRA

Solver Single Query Track Single Query Track
CVC4-uc X X
CVC4 X X
Z3n X X
Total - competing 2 2
Total - non-competing 1 1
Total 3 3

QF_DT

Solver Single Query Track Single Query Track
Alt-Ergo X X
CVC4-uc X X
CVC4 X X
2018-CVC4n X X
2018-CVC4 (unsat core)n X X
Total - competing 3 3
Total - non-competing 2 2
Total 5 5

QF_FP

Solver Single Query Track Single Query Track Single Query Track
COLIBRI X X X
CVC4-inc X X X
CVC4-uc X X X
CVC4 X X X
Par4 X X X
2018-COLIBRIn X X X
2018-CVC4 (unsat core)n X X X
2018-Z3 (incremental)n X X X
Z3n X X X
Total - competing 5 5 5
Total - non-competing 4 4 4
Total 9 9 9

QF_FPLRA

Solver Single Query Track Single Query Track
CVC4-uc X X
CVC4 X X
Z3n X X
Total - competing 2 2
Total - non-competing 1 1
Total 3 3

QF_IDL

Solver Single Query Track Single Query Track
CVC4-uc X X
CVC4 X X
Par4 X X
ProB X X
SMTInterpol X X
Yices 2.6.2 X X
veriT X X
2018-Yicesn X X
2018-Z3 (unsat core)n X X
Z3n X X
Total - competing 7 7
Total - non-competing 3 3
Total 10 10

QF_LIA

Solver Single Query Track Single Query Track Single Query Track
CVC4-inc X X X
CVC4-uc X X X
CVC4 X X X
Ctrl-Ergo X X X
Par4 X X X
ProB X X X
SMTInterpol X X X
SPASS-SATT X X X
Yices 2.6.2 X X X
Yices 2.6.2 Incremental X X X
veriT X X X
2018-SMTInterpol (unsat core)n X X X
2018-SPASS-SATTn X X X
2018-Yices (incremental)n X X X
CVC4-SymBreakn X X X
CVC4-inc-fixedn X X X
Z3n X X X
Total - competing 11 11 11
Total - non-competing 6 6 6
Total 17 17 17

QF_LIRA

Solver Single Query Track Single Query Track
CVC4-uc X X
CVC4 X X
Par4 X X
SMTInterpol X X
Yices 2.6.2 X X
2018-Z3n X X
2018-Z3 (unsat core)n X X
Z3n X X
Total - competing 5 5
Total - non-competing 3 3
Total 8 8

QF_LRA

Solver Single Query Track Single Query Track Single Query Track
CVC4-inc X X X
CVC4-uc X X X
CVC4 X X X
Ctrl-Ergo X X X
OpenSMT2 X X X
Par4 X X X
SMTInterpol X X X
SPASS-SATT X X X
Yices 2.6.2 X X X
Yices 2.6.2 Incremental X X X
veriT X X X
2018-CVC4n X X X
2018-MathSAT (incremental)n X X X
2018-SMTInterpol (unsat core)n X X X
CVC4-SymBreakn X X X
Z3n X X X
Total - competing 11 11 11
Total - non-competing 5 5 5
Total 16 16 16

QF_NIA

Solver Single Query Track Single Query Track Single Query Track
AProVE X X X
CVC4-inc X X X
CVC4-uc X X X
CVC4 X X X
MathSAT-default X X X
MathSAT-na-ext X X X
Par4 X X X
ProB X X X
SMT-RAT X X X
Yices 2.6.2 X X X
Yices 2.6.2 Incremental X X X
2018-CVC4n X X X
2018-CVC4 (incremental)n X X X
2018-Z3 (unsat core)n X X X
CVC4-SymBreakn X X X
Z3n X X X
Total - competing 11 11 11
Total - non-competing 5 5 5
Total 16 16 16

QF_NIRA

Solver Single Query Track Single Query Track
CVC4-uc X X
CVC4 X X
MathSAT-default X X
MathSAT-na-ext X X
SMT-RAT X X
Yices 2.6.2 X X
2018-SMTRAT-Ratn X X
2018-Z3 (unsat core)n X X
Z3n X X
Total - competing 6 6
Total - non-competing 3 3
Total 9 9

QF_NRA

Solver Single Query Track Single Query Track
CVC4-uc X X
CVC4 X X
MathSAT-default X X
MathSAT-na-ext X X
Par4 X X
SMT-RAT X X
SMTRAT-MCSAT X X
Yices 2.6.2 X X
veriT+raSAT+Redlog X X
2018-CVC4 (unsat core)n X X
2018-Z3n X X
CVC4-SymBreakn X X
Z3n X X
Total - competing 9 9
Total - non-competing 4 4
Total 13 13

QF_RDL

Solver Single Query Track Single Query Track
CVC4-uc X X
CVC4 X X
SMTInterpol X X
Yices 2.6.2 X X
veriT X X
2018-Yicesn X X
2018-Z3 (unsat core)n X X
Z3n X X
Total - competing 5 5
Total - non-competing 3 3
Total 8 8

QF_S

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

QF_SLIA

Solver Single Query Track Single Query Track
CVC4-uc X X
CVC4 X X
2018-CVC4n X X
Total - competing 2 2
Total - non-competing 1 1
Total 3 3

QF_UF

Solver Single Query Track Single Query Track Single Query Track
Alt-Ergo X X X
CVC4-inc X X X
CVC4-uc X X X
CVC4 X X X
OpenSMT2 X X X
Par4 X X X
SMTInterpol X X X
Yices 2.6.2 X X X
Yices 2.6.2 Incremental X X X
veriT X X X
2018-CVC4 (unsat core)n X X X
2018-Yicesn X X X
Z3n X X X
Total - competing 10 10 10
Total - non-competing 3 3 3
Total 13 13 13

QF_UFBV

Solver Single Query Track Single Query Track Single Query Track
Boolector X X X
Boolector (incremental) X X X
CVC4-inc X X X
CVC4-uc X X X
CVC4 X X X
Poolector X X X
Yices 2.6.2 X X X
Yices 2.6.2 Incremental X X X
2018-Boolectorn X X X
2018-Boolector (incremental)n X X X
2018-Z3 (unsat core)n X X X
Z3n X X X
Total - competing 8 8 8
Total - non-competing 4 4 4
Total 12 12 12

QF_UFBVLIA

Solver Single Query Track
CVC4-inc X
Z3n X
Total - competing 1
Total - non-competing 1
Total 2

QF_UFIDL

Solver Single Query Track Single Query Track
CVC4-uc X X
CVC4 X X
SMTInterpol X X
Yices 2.6.2 X X
veriT X X
2018-Yicesn X X
2018-Yices (unsat core)n X X
Z3n X X
Total - competing 5 5
Total - non-competing 3 3
Total 8 8

QF_UFLIA

Solver Single Query Track Single Query Track Single Query Track
Alt-Ergo X X X
CVC4-inc X X X
CVC4-uc X X X
CVC4 X X X
SMTInterpol X X X
Yices 2.6.2 X X X
Yices 2.6.2 Incremental X X X
veriT X X X
2018-Yicesn X X X
2018-Z3 (incremental)n X X X
2018-Z3 (unsat core)n X X X
Z3n X X X
Total - competing 8 8 8
Total - non-competing 4 4 4
Total 12 12 12

QF_UFLRA

Solver Single Query Track Single Query Track Single Query Track
Alt-Ergo X X X
CVC4-inc X X X
CVC4-uc X X X
CVC4 X X X
SMTInterpol X X X
Yices 2.6.2 X X X
Yices 2.6.2 Incremental X X X
veriT X X X
2018-MathSAT (unsat core)n X X X
2018-Yicesn X X X
2018-Z3 (incremental)n X X X
Z3n X X X
Total - competing 8 8 8
Total - non-competing 4 4 4
Total 12 12 12

QF_UFNIA

Solver Single Query Track Single Query Track Single Query Track
Alt-Ergo X X X
CVC4-inc X X X
CVC4-uc X X X
CVC4 X X X
MathSAT-default X X X
MathSAT-na-ext X X X
Yices 2.6.2 X X X
Yices 2.6.2 Incremental X X X
2018-Yicesn X X X
2018-Z3 (incremental)n X X X
2018-Z3 (unsat core)n X X X
Z3n X X X
Total - competing 8 8 8
Total - non-competing 4 4 4
Total 12 12 12

QF_UFNRA

Solver Single Query Track Single Query Track
Alt-Ergo X X
CVC4-uc X X
CVC4 X X
MathSAT-default X X
MathSAT-na-ext X X
Par4 X X
Yices 2.6.2 X X
veriT+raSAT+Redlog X X
2018-Yicesn X X
2018-Z3 (unsat core)n X X
Z3n X X
Total - competing 8 8
Total - non-competing 3 3
Total 11 11

UF

Solver Single Query Track Single Query Track
Alt-Ergo X X
CVC4-uc X X
CVC4 X X
Par4 X X
SMTInterpol X X
UltimateEliminator+MathSAT-5.5.4 X X
UltimateEliminator+SMTInterpol X X
UltimateEliminator+Yices-2.6.1 X X
Vampire X X
veriT X X
2018-CVC4n X X
2018-CVC4 (unsat core)n X X
2018-Vampiren X X
Z3n X X
Total - competing 10 10
Total - non-competing 4 4
Total 14 14

UFBV

Solver Single Query Track Single Query Track
CVC4-uc X X
CVC4 X X
Par4 X X
UltimateEliminator+MathSAT-5.5.4 X X
2018-CVC4 (unsat core)n X X
2018-Z3n X X
Z3n X X
Total - competing 4 4
Total - non-competing 3 3
Total 7 7

UFDT

Solver Single Query Track Single Query Track
Alt-Ergo X X
CVC4-uc X X
CVC4 X X
Vampire X X
2018-CVC4n X X
2018-CVC4 (unsat core)n X X
Total - competing 4 4
Total - non-competing 2 2
Total 6 6

UFDTLIA

Solver Single Query Track Single Query Track
Alt-Ergo X X
CVC4-uc X X
CVC4 X X
Vampire X X
2018-CVC4n X X
Total - competing 4 4
Total - non-competing 1 1
Total 5 5

UFDTNIA

Solver Single Query Track Single Query Track
Alt-Ergo X X
CVC4-uc X X
CVC4 X X
Vampire X X
Total - competing 4 4
Total - non-competing 0 0
Total 4 4

UFIDL

Solver Single Query Track Single Query Track
CVC4-uc X X
CVC4 X X
Par4 X X
SMTInterpol X X
UltimateEliminator+MathSAT-5.5.4 X X
UltimateEliminator+SMTInterpol X X
UltimateEliminator+Yices-2.6.1 X X
Vampire X X
veriT X X
2018-CVC4 (unsat core)n X X
2018-Z3n X X
Z3n X X
Total - competing 9 9
Total - non-competing 3 3
Total 12 12

UFLIA

Solver Single Query Track Single Query Track
Alt-Ergo X X
CVC4-uc X X
CVC4 X X
Par4 X X
SMTInterpol X X
UltimateEliminator+MathSAT-5.5.4 X X
UltimateEliminator+SMTInterpol X X
UltimateEliminator+Yices-2.6.1 X X
Vampire X X
veriT X X
2018-CVC4n X X
2018-CVC4 (unsat core)n X X
Z3n X X
Total - competing 10 10
Total - non-competing 3 3
Total 13 13

UFLRA

Solver Single Query Track Single Query Track Single Query Track
Alt-Ergo X X X
CVC4-inc X X X
CVC4-uc X X X
CVC4 X X X
SMTInterpol X X X
UltimateEliminator+MathSAT-5.5.4 X X X
UltimateEliminator+SMTInterpol X X X
UltimateEliminator+Yices-2.6.1 X X X
Vampire X X X
veriT X X X
2018-Z3n X X X
2018-Z3 (incremental)n X X X
2018-Z3 (unsat core)n X X X
Z3n X X X
Total - competing 10 10 10
Total - non-competing 4 4 4
Total 14 14 14

UFNIA

Solver Single Query Track Single Query Track
Alt-Ergo X X
CVC4-uc X X
CVC4 X X
Par4 X X
UltimateEliminator+MathSAT-5.5.4 X X
UltimateEliminator+Yices-2.6.1 X X
Vampire X X
2018-CVC4 (unsat core)n X X
2018-Vampiren X X
2018-Z3n X X
CVC4-SymBreakn X X
Z3n X X
Total - competing 7 7
Total - non-competing 5 5
Total 12 12