SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions

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
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
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 X 28338
28741
153 veriT at SMT-COMP 2020
2018-Boolector (incremental)n X 19991
Boolector at the SMT Competition 2018
2018-CVC4n X 19775
CVC4 at the SMT Competition 2018
2018-CVC4 (incremental)n X 19992
CVC4 at the SMT Competition 2018
2018-CVC4 (unsat core)n X 19793
CVC4 at the SMT Competition 2018
2018-MathSAT (incremental)n X 19993
2018-SMTRAT-Ratn X 19783
SMT-RAT 2.2
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 at the SMT Competition 2019
2019-CVC4-incn X 23417
23733
CVC4 at the SMT Competition 2019
2019-CVC4-ucn X 23416
23732
CVC4 at the SMT Competition 2019
2019-CVC4n X 23420
23737
CVC4 at the SMT Competition 2019
2019-MathSAT-defaultn X X X 23373
23680
MathSAT5 (Nonlinear) at the SMT Competition 2019
2019-MathSAT-na-extn X X 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 X 23363
23694
Yices 2 in SMT-COMP 2019
2019-Yices 2.6.2 Incrementaln X 23364
23695
Yices 2 in SMT-COMP 2019
2019-Z3n X X X 23470
23470
Bitwuzla-fixedn X X X X 29091
29091
Bitwuzla 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
SMTInterpol-fixedn X X X X 29030
29030
SMTInterpol
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
veriT+viten X 28742
28742
0 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 Single Query Track
CVC4-uc X X
CVC4 X X
UltimateEliminator+MathSAT X X
z3n X X
Total - competing 3 3
Total - non-competing 1 1
Total 4 4

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 X X X
2018-CVC4n X X X
2019-CVC4-incn X X X
Total - competing 4 4 4
Total - non-competing 2 2 2
Total 6 6 6

ABVFPLRA

Solver Single Query Track Single Query Track
CVC4-uc X X
CVC4 X X
UltimateEliminator+MathSAT X X
Total - competing 3 3
Total - non-competing 0 0
Total 3 3

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 X X X
Vampire X X X
veriT X X X
2018-Z3n X X X
2018-Z3 (incremental)n X X X
SMTInterpol-fixedn X X X
veriT+viten X X X
z3n X X X
Total - competing 8 8 8
Total - non-competing 5 5 5
Total 13 13 13

ANIA

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

AUFBVDTLIA

Solver Single Query Track Single Query Track
CVC4-uc X X
CVC4 X X
UltimateEliminator+MathSAT X X
Total - competing 3 3
Total - non-competing 0 0
Total 3 3

AUFBVDTNIA

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

AUFDTLIA

Solver Single Query Track Single Query Track
Alt-Ergo X X
CVC4-uc X X
CVC4 X X
UltimateEliminator+MathSAT X X
Vampire X X
2018-CVC4n X X
Total - competing 5 5
Total - non-competing 1 1
Total 6 6

AUFDTLIRA

Solver Single Query Track Single Query Track
Alt-Ergo X X
CVC4-uc X X
CVC4 X X
UltimateEliminator+MathSAT X X
Vampire X X
Total - competing 5 5
Total - non-competing 0 0
Total 5 5

AUFDTNIRA

Solver Single Query Track Single Query Track
Alt-Ergo X X
CVC4-uc X X
CVC4 X X
UltimateEliminator+MathSAT X X
Vampire X X
Total - competing 5 5
Total - non-competing 0 0
Total 5 5

AUFFPDTLIRA

Solver Single Query Track Single Query Track
CVC4-uc X X
CVC4 X X
UltimateEliminator+MathSAT X X
Total - competing 3 3
Total - non-competing 0 0
Total 3 3

AUFFPDTNIRA

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

AUFLIA

Solver Single Query Track Single Query Track
Alt-Ergo X X
CVC4-uc X X
CVC4 X X
SMTInterpol X X
UltimateEliminator+MathSAT X X
Vampire X X
veriT X X
2018-CVC4n X X
2018-CVC4 (unsat core)n X X
SMTInterpol-fixedn X X
veriT+viten X X
z3n X X
Total - competing 7 7
Total - non-competing 5 5
Total 12 12

AUFLIRA

Solver Single Query Track Single Query Track
Alt-Ergo X X
CVC4-uc X X
CVC4 X X
SMTInterpol X X
UltimateEliminator+MathSAT X X
Vampire X X
veriT X X
2018-CVC4 (unsat core)n X X
2019-Par4n X X
SMTInterpol-fixedn X X
veriT+viten X X
z3n X X
Total - competing 7 7
Total - non-competing 5 5
Total 12 12

AUFNIA

Solver Single Query Track Single Query Track
Alt-Ergo X X
CVC4-uc X X
CVC4 X X
UltimateEliminator+MathSAT X X
Vampire X X
z3n X X
Total - competing 5 5
Total - non-competing 1 1
Total 6 6

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
UltimateEliminator+MathSAT X X X
Vampire X X X
2019-CVC4-incn X X X
2019-CVC4-ucn X X X
2019-Par4n X X X
z3n X X X
Total - competing 6 6 6
Total - non-competing 4 4 4
Total 10 10 10

BV

Solver Single Query Track Single Query Track Single Query Track
Bitwuzla X X X
CVC4-inc X X X
CVC4-uc X X X
CVC4 X X X
UltimateEliminator+MathSAT X X X
2019-CVC4-ucn X X X
2019-Par4n X X X
2019-Z3n X X X
Bitwuzla-fixedn X X X
z3n X X X
Total - competing 5 5 5
Total - non-competing 5 5 5
Total 10 10 10

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 X X X
2019-CVC4-incn X X X
2019-Z3n X X X
Total - competing 4 4 4
Total - non-competing 2 2 2
Total 6 6 6

BVFPLRA

Solver Single Query Track Single Query Track
CVC4-uc X X
CVC4 X X
UltimateEliminator+MathSAT X X
Total - competing 3 3
Total - non-competing 0 0
Total 3 3

FP

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

FPLRA

Solver Single Query Track Single Query Track
CVC4-uc X X
CVC4 X X
UltimateEliminator+MathSAT X X
Total - competing 3 3
Total - non-competing 0 0
Total 3 3

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
SMTInterpol X X X
UltimateEliminator+MathSAT X X X
Vampire X X X
veriT X X X
2018-Z3 (incremental)n X X X
2018-Z3 (unsat core)n X X X
2019-Z3n X X X
SMTInterpol-fixedn X X X
veriT+viten X X X
z3n X X X
Total - competing 7 7 7
Total - non-competing 6 6 6
Total 13 13 13

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
SMTInterpol X X X
UltimateEliminator+MathSAT X X X
Vampire X X X
2019-Par4n X X X
2019-Z3n X X X
SMTInterpol-fixedn X X X
z3n X X X
Total - competing 6 6 6
Total - non-competing 4 4 4
Total 10 10 10

NIA

Solver Single Query Track Single Query Track
CVC4-uc X X
CVC4 X X
UltimateEliminator+MathSAT X X
Vampire X X
2018-Z3n X X
z3n X X
Total - competing 4 4
Total - non-competing 2 2
Total 6 6

NRA

Solver Single Query Track Single Query Track
CVC4-uc X X
CVC4 X X
UltimateEliminator+MathSAT X X
Vampire X X
2019-Par4n X X
z3n X X
Total - competing 4 4
Total - non-competing 2 2
Total 6 6

QF_ABV

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

QF_ABVFP

Solver Single Query Track Single Query Track Single Query Track
Bitwuzla X X X
COLIBRI X X X
CVC4-inc X X X
CVC4-uc X X X
CVC4 X X X
Bitwuzla-fixedn X X X
MathSAT5n X X X
Total - competing 5 5 5
Total - non-competing 2 2 2
Total 7 7 7

QF_ABVFPLRA

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

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
Yices2 X X X
Yices2 incremental X X X
veriT X X X
2018-Z3 (incremental)n X X X
2018-Z3 (unsat core)n X X X
2019-Yices 2.6.2n X X X
MathSAT5n X X X
SMTInterpol-fixedn X X X
Yices2-fixedn X X X
Yices2-fixed incrementaln X X X
z3n X X X
Total - competing 8 8 8
Total - non-competing 8 8 8
Total 16 16 16

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
2018-CVC4 (unsat core)n X X X
2018-Z3 (incremental)n X X X
2019-CVC4n X X X
MathSAT5n X X X
z3n X X X
Total - competing 4 4 4
Total - non-competing 5 5 5
Total 9 9 9

QF_AUFBV

Solver Single Query Track Single Query Track Single Query Track
Bitwuzla X X X
CVC4-inc X X X
CVC4-uc X X X
CVC4 X X X
Yices2 X X X
Yices2 incremental X X X
2019-Yices 2.6.2n X X X
2019-Yices 2.6.2 Incrementaln X X X
Bitwuzla-fixedn X X X
MathSAT5n X X X
Yices2-fixedn X X X
Yices2-fixed incrementaln X X X
z3n X X X
Total - competing 6 6 6
Total - non-competing 7 7 7
Total 13 13 13

QF_AUFBVLIA

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

QF_AUFBVNIA

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

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
Yices2 X X X
Yices2 incremental X X X
veriT X X X
2018-CVC4 (unsat core)n X X X
2018-Yices (incremental)n X X X
2019-Yices 2.6.2n X X X
MathSAT5n X X X
SMTInterpol-fixedn X X X
Yices2-fixedn X X X
Yices2-fixed incrementaln X X X
z3n X X X
Total - competing 8 8 8
Total - non-competing 8 8 8
Total 16 16 16

QF_AUFNIA

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

QF_AX

Solver Single Query Track Single Query Track
Alt-Ergo X X
CVC4-uc X X
CVC4 X X
SMTInterpol X X
Yices2 X X
2018-Yicesn X X
2018-Yices (unsat core)n X X
2019-Yices 2.6.2n X X
MathSAT5n X X
SMTInterpol-fixedn X X
Yices2-fixedn X X
z3n X X
Total - competing 5 5
Total - non-competing 7 7
Total 12 12

QF_BV

Solver Single Query Track Single Query Track Single Query Track Single Query Track
Bitwuzla X X X X
CVC4-inc X X X X
CVC4-mv X X X X
CVC4-uc X X X X
CVC4 X X X X
LazyBV2Int X X X X
MinkeyRink X X X X
STP + CMS X X X X
STP + MergeSAT X X X X
Yices2 X X X X
Yices2 Model Validation X X X X
Yices2 incremental X X X X
2018-Yices (unsat core)n X X X X
2019-Boolectorn X X X X
2019-Poolectorn X X X X
2019-Yices 2.6.2 Incrementaln X X X X
Bitwuzla-fixedn X X X X
MathSAT5-mvn X X X X
MathSAT5n X X X X
MinkeyRink-fixedn X X X X
Yices2-fixedn X X X X
Yices2-fixed Model Validationn X X X X
Yices2-fixed incrementaln X X X X
z3n X X X X
Total - competing 12 12 12 12
Total - non-competing 12 12 12 12
Total 24 24 24 24

QF_BVFP

Solver Single Query Track Single Query Track Single Query Track
Bitwuzla X X X
COLIBRI X X X
CVC4-inc X X X
CVC4-uc X X X
CVC4 X X X
2019-Par4n X X X
Bitwuzla-fixedn X X X
MathSAT5n X X X
z3n X X X
Total - competing 5 5 5
Total - non-competing 4 4 4
Total 9 9 9

QF_BVFPLRA

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

QF_DT

Solver Single Query Track Single Query Track
Alt-Ergo X X
CVC4-uc X X
CVC4 X X
2018-CVC4n X X
z3n 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
Bitwuzla X X X
COLIBRI X X X
CVC4-inc X X X
CVC4-uc X X X
CVC4 X X X
2019-Par4n X X X
Bitwuzla-fixedn X X X
MathSAT5n 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
COLIBRI X X
CVC4-uc X X
CVC4 X X
MathSAT5n X X
z3n X X
Total - competing 3 3
Total - non-competing 2 2
Total 5 5

QF_IDL

Solver Single Query Track Single Query Track Single Query Track
CVC4-mv X X X
CVC4-uc X X X
CVC4 X X X
SMTInterpol X X X
Yices2 X X X
Yices2 Model Validation X X X
veriT X X X
2019-Par4n X X X
2019-Z3n X X X
MathSAT5-mvn X X X
MathSAT5n X X X
SMTInterpol-fixedn X X X
Yices2-fixedn X X X
Yices2-fixed Model Validationn X X X
z3n X X X
Total - competing 7 7 7
Total - non-competing 8 8 8
Total 15 15 15

QF_LIA

Solver Single Query Track Single Query Track Single Query Track Single Query Track
CVC4-inc X X X X
CVC4-mv X X X X
CVC4-uc X X X X
CVC4 X X X X
SMTInterpol X X X X
Yices2 X X X X
Yices2 Model Validation X X X X
Yices2 incremental X X X X
veriT X X X X
2018-Yices (incremental)n X X X X
2019-Par4n X X X X
2019-Yices 2.6.2n X X X X
MathSAT5-mvn X X X X
MathSAT5n X X X X
SMTInterpol-fixedn X X X X
Yices2-fixedn X X X X
Yices2-fixed Model Validationn X X X X
Yices2-fixed incrementaln X X X X
z3n X X X X
Total - competing 9 9 9 9
Total - non-competing 10 10 10 10
Total 19 19 19 19

QF_LIRA

Solver Single Query Track Single Query Track Single Query Track
CVC4-mv X X X
CVC4-uc X X X
CVC4 X X X
SMTInterpol X X X
Yices2 X X X
Yices2 Model Validation X X X
2019-Par4n X X X
MathSAT5-mvn X X X
MathSAT5n X X X
SMTInterpol-fixedn X X X
Yices2-fixedn X X X
Yices2-fixed Model Validationn X X X
z3n X X X
Total - competing 6 6 6
Total - non-competing 7 7 7
Total 13 13 13

QF_LRA

Solver Single Query Track Single Query Track Single Query Track Single Query Track
CVC4-inc X X X X
CVC4-mv X X X X
CVC4-uc X X X X
CVC4 X X X X
OpenSMT X X X X
SMTInterpol X X X X
Yices2 X X X X
Yices2 Model Validation X X X X
Yices2 incremental X X X X
veriT X X X X
2018-MathSAT (incremental)n X X X X
2019-Par4n X X X X
2019-SPASS-SATTn X X X X
2019-Yices 2.6.2n X X X X
MathSAT5-mvn X X X X
MathSAT5n X X X X
SMTInterpol-fixedn X X X X
Yices2-fixedn X X X X
Yices2-fixed Model Validationn X X X X
Yices2-fixed incrementaln X X X X
z3n X X X X
Total - competing 10 10 10 10
Total - non-competing 11 11 11 11
Total 21 21 21 21

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
SMT-RAT X X X
Yices2 X X X
Yices2 incremental X X X
2019-MathSAT-defaultn X X X
2019-Par4n X X X
MathSAT5n X X X
Yices2-fixedn X X X
Yices2-fixed incrementaln X X X
z3n X X X
Total - competing 7 7 7
Total - non-competing 6 6 6
Total 13 13 13

QF_NIRA

Solver Single Query Track Single Query Track
CVC4-uc X X
CVC4 X X
SMT-RAT X X
Yices2 X X
2018-SMTRAT-Ratn X X
2019-MathSAT-na-extn X X
MathSAT5n X X
Yices2-fixedn X X
z3n X X
Total - competing 4 4
Total - non-competing 5 5
Total 9 9

QF_NRA

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

QF_RDL

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

QF_S

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

QF_SLIA

Solver Single Query Track Single Query Track
CVC4-uc X X
CVC4 X X
Z3str4 X X
Total - competing 3 3
Total - non-competing 0 0
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
OpenSMT X X X
SMTInterpol X X X
Yices2 X X X
Yices2 incremental X X X
veriT X X X
2019-Par4n X X X
2019-Yices 2.6.2n X X X
2019-Yices 2.6.2 Incrementaln X X X
MathSAT5n X X X
SMTInterpol-fixedn X X X
Yices2-fixedn X X X
Yices2-fixed incrementaln X X X
z3n X X X
Total - competing 9 9 9
Total - non-competing 8 8 8
Total 17 17 17

QF_UFBV

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

QF_UFBVLIA

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

QF_UFFP

Solver Single Query Track Single Query Track Single Query Track
Bitwuzla X X X
COLIBRI X X X
CVC4-inc X X X
CVC4-uc X X X
CVC4 X X X
Bitwuzla-fixedn X X X
MathSAT5n X X X
Total - competing 5 5 5
Total - non-competing 2 2 2
Total 7 7 7

QF_UFIDL

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

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
Yices2 X X X
Yices2 incremental X X X
veriT X X X
2018-Yicesn X X X
2018-Z3 (incremental)n X X X
2019-Yices 2.6.2n X X X
MathSAT5n X X X
SMTInterpol-fixedn X X X
Yices2-fixedn X X X
Yices2-fixed incrementaln X X X
z3n X X X
Total - competing 8 8 8
Total - non-competing 8 8 8
Total 16 16 16

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
Yices2 X X X
Yices2 incremental X X X
veriT X X X
2019-SMTInterpoln X X X
2019-Z3n X X X
MathSAT5n X X X
SMTInterpol-fixedn X X X
Yices2-fixedn X X X
Yices2-fixed incrementaln X X X
z3n X X X
Total - competing 8 8 8
Total - non-competing 7 7 7
Total 15 15 15

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
Yices2 X X X
Yices2 incremental X X X
2018-Z3 (unsat core)n X X X
2019-CVC4n X X X
2019-MathSAT-defaultn X X X
MathSAT5n X X X
Yices2-fixedn X X X
Yices2-fixed incrementaln X X X
z3n X X X
Total - competing 6 6 6
Total - non-competing 7 7 7
Total 13 13 13

QF_UFNRA

Solver Single Query Track Single Query Track
Alt-Ergo X X
CVC4-uc X X
CVC4 X X
Yices2 X X
veriT+raSAT+Redlog X X
2018-Z3 (unsat core)n X X
2019-Par4n X X
MathSAT5n X X
Yices2-fixedn X X
z3n X X
Total - competing 5 5
Total - non-competing 5 5
Total 10 10

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
SMTInterpol X X X
UltimateEliminator+MathSAT X X X
Vampire X X X
veriT X X X
2018-CVC4 (unsat core)n X X X
2018-Vampiren X X X
2019-CVC4n X X X
SMTInterpol-fixedn X X X
veriT+viten X X X
z3n X X X
Total - competing 8 8 8
Total - non-competing 6 6 6
Total 14 14 14

UFBV

Solver Single Query Track Single Query Track
CVC4-uc X X
CVC4 X X
UltimateEliminator+MathSAT X X
2018-Z3n X X
2019-Par4n X X
z3n X X
Total - competing 3 3
Total - non-competing 3 3
Total 6 6

UFDT

Solver Single Query Track Single Query Track
Alt-Ergo X X
CVC4-uc X X
CVC4 X X
UltimateEliminator+MathSAT X X
Vampire X X
2019-CVC4n X X
Total - competing 5 5
Total - non-competing 1 1
Total 6 6

UFDTLIA

Solver Single Query Track Single Query Track
Alt-Ergo X X
CVC4-uc X X
CVC4 X X
UltimateEliminator+MathSAT X X
Vampire X X
2019-CVC4n X X
Total - competing 5 5
Total - non-competing 1 1
Total 6 6

UFDTLIRA

Solver Single Query Track Single Query Track
Alt-Ergo X X
CVC4-uc X X
CVC4 X X
UltimateEliminator+MathSAT X X
Vampire X X
Total - competing 5 5
Total - non-competing 0 0
Total 5 5

UFDTNIA

Solver Single Query Track Single Query Track
Alt-Ergo X X
CVC4-uc X X
CVC4 X X
UltimateEliminator+MathSAT X X
Vampire X X
2019-Vampiren X X
Total - competing 5 5
Total - non-competing 1 1
Total 6 6

UFDTNIRA

Solver Single Query Track Single Query Track
Alt-Ergo X X
CVC4-uc X X
CVC4 X X
UltimateEliminator+MathSAT X X
Vampire X X
Total - competing 5 5
Total - non-competing 0 0
Total 5 5

UFFPDTLIRA

Solver Single Query Track Single Query Track
CVC4-uc X X
CVC4 X X
UltimateEliminator+MathSAT X X
Total - competing 3 3
Total - non-competing 0 0
Total 3 3

UFFPDTNIRA

Solver Single Query Track Single Query Track
CVC4-uc X X
CVC4 X X
UltimateEliminator+MathSAT X X
Total - competing 3 3
Total - non-competing 0 0
Total 3 3

UFIDL

Solver Single Query Track Single Query Track
CVC4-uc X X
CVC4 X X
SMTInterpol X X
UltimateEliminator+MathSAT X X
Vampire X X
veriT X X
2018-CVC4 (unsat core)n X X
2019-CVC4-ucn X X
2019-Par4n X X
SMTInterpol-fixedn X X
veriT+viten X X
z3n X X
Total - competing 6 6
Total - non-competing 6 6
Total 12 12

UFLIA

Solver Single Query Track Single Query Track
Alt-Ergo X X
CVC4-uc X X
CVC4 X X
SMTInterpol X X
UltimateEliminator+MathSAT X X
Vampire X X
veriT X X
2018-CVC4 (unsat core)n X X
2019-Par4n X X
SMTInterpol-fixedn X X
veriT+viten X X
z3n X X
Total - competing 7 7
Total - non-competing 5 5
Total 12 12

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 X X X
Vampire X X X
veriT X X X
2018-Z3n X X X
2018-Z3 (unsat core)n X X X
2019-Z3n X X X
SMTInterpol-fixedn X X X
veriT+viten X X X
z3n X X X
Total - competing 8 8 8
Total - non-competing 6 6 6
Total 14 14 14

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
UltimateEliminator+MathSAT X X X
Vampire X X X
2018-CVC4 (unsat core)n X X X
2018-Vampiren X X X
2019-Par4n X X X
z3n X X X
Total - competing 6 6 6
Total - non-competing 4 4 4
Total 10 10 10

UFNRA

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