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