SMT-COMP 2019

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Papers
Benchmark Submission
Rules
Benchmarks
Tools
Specs
Participants
Results
Slides

Previous Competitions

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 (non-incremental) Challenge Track (incremental) Unsat Core Track Model Validation Track (experimental) Preliminary Solver ID Final Solver ID Seed System Description
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
AProVE X 1229 1229 896120349 AProVE
Alt-Ergo X 23333 23530 42 Alt-Ergo
Boolector-ReasonLSn X X 23692 Boolector-ReasonLS
Boolector X X X 23380 23711 42 Boolector
Boolector (incremental) X X 23381 23712 42 Boolector
COLIBRI X 23355 23355 614823377508390721 COLIBRI
CVC4-SymBreakn X 23746 CVC4-SymBreak
CVC4-inc-fixedn X X 24474 CVC4
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-fixedn X X 24232 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-fixedn X X 24233 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
Z3n X X X X X 23470 23470
veriT+raSAT+Redlog X 23399 23399 13 veriT+raSAT+Redlog
veriT X 23406 23693 7800 veriT
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 Incremental Track Unsat Core Track
2018-CVC4n X
CVC4-inc X
CVC4-uc X
CVC4 X
UltimateEliminator+MathSAT-5.5.4 X X X
Z3n X X X
Total - competing 2 2 2
Total - non-competing 2 1 1
Total 4 3 3

ALIA

Solver Single Query Track Incremental Track Unsat Core Track
2018-Z3n X
2018-Z3 (incremental)n X
2018-Z3 (unsat core)n X
Alt-Ergo X
CVC4-inc X
CVC4-uc X
CVC4 X
SMTInterpol 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
Z3n X X X
veriT X
Total - competing 8 5 4
Total - non-competing 2 2 2
Total 10 7 6

ANIA

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

AUFBVDTLIA

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

AUFDTLIA

Solver Single Query Track Unsat Core Track
2018-CVC4n X
Alt-Ergo X
CVC4-uc X
CVC4 X
Vampire X
Total - competing 3 1
Total - non-competing 1 0
Total 4 1

AUFLIA

Solver Single Query Track Unsat Core Track
2018-CVC4n X
2018-CVC4 (unsat core)n X
Alt-Ergo X
CVC4-SymBreakn X
CVC4-uc X
CVC4 X
SMTInterpol X
UltimateEliminator+MathSAT-5.5.4 X X
UltimateEliminator+SMTInterpol X X
UltimateEliminator+Yices-2.6.1 X X
Vampire X
Z3n X X
veriT X
Total - competing 8 4
Total - non-competing 3 2
Total 11 6

AUFLIRA

Solver Single Query Track Unsat Core Track
2018-CVC4 (unsat core)n X
2018-Z3n X
Alt-Ergo X
CVC4-SymBreakn X
CVC4-uc X
CVC4 X
Par4 X
SMTInterpol X
UltimateEliminator+MathSAT-5.5.4 X X
UltimateEliminator+SMTInterpol X X
UltimateEliminator+Yices-2.6.1 X X
Vampire X
Z3n X X
veriT X
Total - competing 9 4
Total - non-competing 3 2
Total 12 6

AUFNIA

Solver Single Query Track Unsat Core Track
Alt-Ergo X
CVC4-SymBreakn X
CVC4-uc X
CVC4 X
UltimateEliminator+MathSAT-5.5.4 X X
UltimateEliminator+Yices-2.6.1 X X
Vampire X
Z3n X X
Total - competing 5 3
Total - non-competing 2 1
Total 7 4

AUFNIRA

Solver Single Query Track Incremental Track Unsat Core Track
2018-CVC4n X
2018-CVC4 (incremental)n X
2018-CVC4 (unsat core)n X
Alt-Ergo X
CVC4-inc X
CVC4-uc X
CVC4 X
Par4 X
UltimateEliminator+MathSAT-5.5.4 X X X
UltimateEliminator+Yices-2.6.1 X X X
Vampire X
Z3n X X X
Total - competing 6 3 3
Total - non-competing 2 2 2
Total 8 5 5

BV

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

BVFP

Solver Single Query Track Incremental Track Unsat Core Track
2018-CVC4n X
CVC4-inc X
CVC4-uc X
CVC4 X
UltimateEliminator+MathSAT-5.5.4 X X X
Z3n X X X
Total - competing 2 2 2
Total - non-competing 2 1 1
Total 4 3 3

FP

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

LIA

Solver Single Query Track Incremental Track Unsat Core Track
2018-Z3n X
2018-Z3 (incremental)n X
2018-Z3 (unsat core)n X
CVC4-inc X
CVC4-uc X
CVC4 X
ProB X
SMTInterpol 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
Z3n X X X
veriT X
Total - competing 8 5 4
Total - non-competing 2 2 2
Total 10 7 6

LRA

Solver Single Query Track Incremental Track Unsat Core Track
2018-CVC4 (unsat core)n X
2018-Z3n X
CVC4-inc X
CVC4-uc X
CVC4 X
Par4 X
SMTInterpol 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
Z3n X X X
Total - competing 7 5 4
Total - non-competing 2 1 2
Total 9 6 6

NIA

Solver Single Query Track Unsat Core Track
2018-CVC4 (unsat core)n X
2018-Z3n X
CVC4-uc X
CVC4 X
ProB X
UltimateEliminator+MathSAT-5.5.4 X X
UltimateEliminator+Yices-2.6.1 X X
Vampire X
Z3n X X
Total - competing 5 3
Total - non-competing 2 2
Total 7 5

NRA

Solver Single Query Track Unsat Core Track
2018-Vampiren X
2018-Z3n X
2018-Z3 (unsat core)n X
CVC4-uc X
CVC4 X
Par4 X
UltimateEliminator+MathSAT-5.5.4 X X
UltimateEliminator+Yices-2.6.1 X X
Vampire X
Z3n X X
Total - competing 5 3
Total - non-competing 3 2
Total 8 5

QF_ABV

Solver Single Query Track Incremental Track Challenge Track (non-incremental) Challenge Track (incremental) Unsat Core Track
2018-Boolectorn X X
2018-Boolector (incremental)n X X
2018-Yices (unsat core)n X
Boolector X X
Boolector (incremental) X X
CVC4-inc X X
CVC4-uc X
CVC4 X X
Par4 X
Poolector X X
Yices 2.6.2 X X X
Yices 2.6.2 Incremental X X
Z3n X X X X X
Total - competing 5 3 4 3 2
Total - non-competing 2 2 2 2 2
Total 7 5 6 5 4

QF_ABVFP

Solver Single Query Track Incremental Track Unsat Core Track
2018-CVC4n X
2018-CVC4 (unsat core)n X
CVC4-inc X
CVC4-uc X
CVC4 X
Z3n X X X
Total - competing 1 1 1
Total - non-competing 2 1 2
Total 3 2 3

QF_ALIA

Solver Single Query Track Incremental Track Unsat Core Track
2018-Yicesn X
2018-Z3 (incremental)n X
2018-Z3 (unsat core)n X
Alt-Ergo X
CVC4-inc X
CVC4-uc X
CVC4 X
SMTInterpol X X X
Yices 2.6.2 X X
Yices 2.6.2 Incremental X
Z3n X X X
veriT 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
2018-CVC4 (unsat core)n X
2018-Z3n X
2018-Z3 (incremental)n X
Alt-Ergo X
CVC4-inc X
CVC4-uc X
CVC4 X
MathSAT-default X X X
MathSAT-na-ext X X X
Z3n X X X
Total - competing 4 3 3
Total - non-competing 2 2 2
Total 6 5 5

QF_AUFBV

Solver Single Query Track Incremental Track Challenge Track (non-incremental) Challenge Track (incremental) Unsat Core Track
2018-CVC4n X X
2018-MathSAT (unsat core)n X
2018-Yices (incremental)n X X
Boolector X X
Boolector (incremental) X X
CVC4-inc X X
CVC4-uc X
CVC4 X X
Poolector X X
Yices 2.6.2 X X X
Yices 2.6.2 Incremental X X
Z3n X X X X X
Total - competing 4 3 4 3 2
Total - non-competing 2 2 2 2 2
Total 6 5 6 5 4

QF_AUFBVLIA

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

QF_AUFBVNIA

Solver Incremental 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 Incremental Track Unsat Core Track
2018-CVC4 (unsat core)n X
2018-Yicesn X
2018-Yices (incremental)n X
Alt-Ergo X
CVC4-inc X
CVC4-uc X
CVC4 X
SMTInterpol X X X
Yices 2.6.2 X X
Yices 2.6.2 Incremental X
Z3n X X X
veriT 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
2018-Z3n X
2018-Z3 (unsat core)n X
Alt-Ergo X
CVC4-uc X
CVC4 X
MathSAT-default X X
MathSAT-na-ext X X
Z3n X X
Total - competing 4 3
Total - non-competing 2 2
Total 6 5

QF_AX

Solver Single Query Track Unsat Core Track
2018-Yicesn X
2018-Yices (unsat core)n X
Alt-Ergo X
CVC4-uc X
CVC4 X
SMTInterpol X X
Yices 2.6.2 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 Challenge Track (non-incremental) Challenge Track (incremental) Unsat Core Track Model Validation Track (experimental)
2018-Boolectorn X X
2018-MathSAT (incremental)n X X
2018-Minkeyrink MTn X X
2018-Yices (unsat core)n X
Boolector-ReasonLSn X X
Boolector X X X
Boolector (incremental) X X
CVC4-inc-fixedn X X
CVC4-inc X X
CVC4-mv X
CVC4-uc X
CVC4 X X
Minkeyrink Solver X X X X X
Minkeyrink Solver MT X X X X X
Par4 X
Poolector X X
STP-incremental X X X X
STP-mergesat-fixedn X X
STP-mergesat X X
STP-minisat X X
STP-mt X X X X X
STP-portfolio-fixedn X X
STP-portfolio X X
STP-riss X X
STP X X
Yices 2.6.2 X X X
Yices 2.6.2 CaDiCal X X
Yices 2.6.2 CaDiCal/SMT-LIB2 Models X
Yices 2.6.2 Cryptominisat X X
Yices 2.6.2 Cryptominisat/SMT-LIB2 Models X
Yices 2.6.2 Incremental X X
Yices 2.6.2 Model Validation X
Yices 2.6.2 New Bvsolver X X
Yices 2.6.2 New Bvsolver with SMT2 Models X
Yices 2.6.2 mcsat-bv X
Z3n X X X X X
Total - competing 18 7 15 7 2 10
Total - non-competing 6 4 5 3 2 0
Total 24 11 20 10 4 10

QF_BVFP

Solver Single Query Track Incremental Track Unsat Core Track
2018-CVC4n X
2018-CVC4 (incremental)n X
2018-CVC4 (unsat core)n X
CVC4-inc X
CVC4-uc X
CVC4 X
Par4 X
Z3n X X X
Total - competing 2 1 1
Total - non-competing 2 2 2
Total 4 3 3

QF_BVFPLRA

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

QF_DT

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

QF_FP

Solver Single Query Track Incremental Track Unsat Core Track
2018-COLIBRIn X
2018-CVC4 (unsat core)n X
2018-Z3 (incremental)n X
COLIBRI X
CVC4-inc X
CVC4-uc X
CVC4 X
Par4 X
Z3n X X X
Total - competing 3 1 1
Total - non-competing 2 2 2
Total 5 3 3

QF_FPLRA

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

QF_IDL

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

QF_LIA

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

QF_LIRA

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

QF_LRA

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

QF_NIA

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

QF_NIRA

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

QF_NRA

Solver Single Query Track Unsat Core Track
2018-CVC4 (unsat core)n X
2018-Z3n X
CVC4-SymBreakn X
CVC4-uc X
CVC4 X
MathSAT-default X X
MathSAT-na-ext X X
Par4 X
SMT-RAT X
SMTRAT-MCSAT X
Yices 2.6.2 X
Z3n X X
veriT+raSAT+Redlog X
Total - competing 8 3
Total - non-competing 3 2
Total 11 5

QF_RDL

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

QF_S

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

QF_SLIA

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

QF_UF

Solver Single Query Track Incremental Track Unsat Core Track
2018-CVC4 (unsat core)n X
2018-Yicesn X
Alt-Ergo X
CVC4-inc X
CVC4-uc X
CVC4 X
OpenSMT2 X
Par4 X
SMTInterpol X X X
Yices 2.6.2 X X
Yices 2.6.2 Incremental X
Z3n X X X
veriT X
Total - competing 7 3 3
Total - non-competing 2 1 2
Total 9 4 5

QF_UFBV

Solver Single Query Track Incremental Track Unsat Core Track
2018-Boolectorn X
2018-Boolector (incremental)n X
2018-Z3 (unsat core)n X
Boolector X
Boolector (incremental) X
CVC4-inc X
CVC4-uc X
CVC4 X
Poolector X
Yices 2.6.2 X X
Yices 2.6.2 Incremental X
Z3n X X X
Total - competing 4 3 2
Total - non-competing 2 2 2
Total 6 5 4

QF_UFBVLIA

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

QF_UFIDL

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

QF_UFLIA

Solver Single Query Track Incremental Track Unsat Core Track
2018-Yicesn X
2018-Z3 (incremental)n X
2018-Z3 (unsat core)n X
Alt-Ergo X
CVC4-inc X
CVC4-uc X
CVC4 X
SMTInterpol X X X
Yices 2.6.2 X X
Yices 2.6.2 Incremental X
Z3n X X X
veriT 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
2018-MathSAT (unsat core)n X
2018-Yicesn X
2018-Z3 (incremental)n X
Alt-Ergo X
CVC4-inc X
CVC4-uc X
CVC4 X
SMTInterpol X X X
Yices 2.6.2 X X
Yices 2.6.2 Incremental X
Z3n X X X
veriT 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
2018-Yicesn X
2018-Z3 (incremental)n X
2018-Z3 (unsat core)n X
Alt-Ergo X
CVC4-inc X
CVC4-uc X
CVC4 X
MathSAT-default X X X
MathSAT-na-ext X X X
Yices 2.6.2 X
Yices 2.6.2 Incremental X
Z3n X X X
Total - competing 5 4 3
Total - non-competing 2 2 2
Total 7 6 5

QF_UFNRA

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

UF

Solver Single Query Track Unsat Core Track
2018-CVC4n X
2018-CVC4 (unsat core)n X
2018-Vampiren X
Alt-Ergo X
CVC4-uc X
CVC4 X
Par4 X
SMTInterpol X
UltimateEliminator+MathSAT-5.5.4 X X
UltimateEliminator+SMTInterpol X X
UltimateEliminator+Yices-2.6.1 X X
Vampire X
Z3n X X
veriT X
Total - competing 9 4
Total - non-competing 3 2
Total 12 6

UFBV

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

UFDT

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

UFDTLIA

Solver Single Query Track Unsat Core Track
2018-CVC4n X
Alt-Ergo X
CVC4-uc X
CVC4 X
Vampire X
Total - competing 3 1
Total - non-competing 1 0
Total 4 1

UFDTNIA

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

UFIDL

Solver Single Query Track Unsat Core Track
2018-CVC4 (unsat core)n X
2018-Z3n X
CVC4-uc X
CVC4 X
Par4 X
SMTInterpol X
UltimateEliminator+MathSAT-5.5.4 X X
UltimateEliminator+SMTInterpol X X
UltimateEliminator+Yices-2.6.1 X X
Vampire X
Z3n X X
veriT X
Total - competing 8 4
Total - non-competing 2 2
Total 10 6

UFLIA

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

UFLRA

Solver Single Query Track Incremental Track Unsat Core Track
2018-Z3n X
2018-Z3 (incremental)n X
2018-Z3 (unsat core)n X
Alt-Ergo X
CVC4-inc X
CVC4-uc X
CVC4 X
SMTInterpol 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
Z3n X X X
veriT X
Total - competing 8 5 4
Total - non-competing 2 2 2
Total 10 7 6

UFNIA

Solver Single Query Track Unsat Core Track
2018-CVC4 (unsat core)n X
2018-Vampiren X
2018-Z3n X
Alt-Ergo X
CVC4-SymBreakn X
CVC4-uc X
CVC4 X
Par4 X
UltimateEliminator+MathSAT-5.5.4 X X
UltimateEliminator+Yices-2.6.1 X X
Vampire X
Z3n X X
Total - competing 6 3
Total - non-competing 4 2
Total 10 5