Participants

The following solvers have been submitted to SMT-COMP 2021 or were entered as non-competing solvers by the organizers for comparison.

Solver	Single Query Track	Incremental Track	Unsat Core Track	Model Validation Track	Cloud Track	Parallel Track	Preliminary Solver ID	Final Solver ID	Seed	System Description
AProVE	X						1229	1229	170142	AProVE at SMT-COMP 2021
Bitwuzla	X	X	X	X			33006	33292	42	Bitwuzla at the SMT-COMP 2021
COLIBRI	X						32990	32990	9075420	COLIBRI
OpenSMT	X	X		X			33003	33438	13390	The OpenSMT Solver in SMT-COMP 2021
SMT-RAT-MCSAT	X						33080	33080	5650572280	SMT-RAT 21.05
SMT-RAT	X						33081	33081	9077370145	SMT-RAT 21.05
SMTInterpol-remus			X				33041	33435	1	SMTInterpol and SMTInterpol-remus
SMTInterpol	X	X	X	X			32995	33439	384076683	SMTInterpol and SMTInterpol-remus
SMTS cube-and-conquer					X		-	10	0	The OpenSMT Solver in SMT-COMP 2021
SMTS portfolio					X		-	13	0	The OpenSMT Solver in SMT-COMP 2021
STP-CMS-Cloud					X		-	14	0	STP in the SMT-COMP 2021
STP-parallel						X	-	15	0	STP in the SMT-COMP 2021
STP	X	X		X			28776	33442	2021	STP in the SMT-COMP 2021
UltimateEliminator+MathSAT	X	X	X				28804	33466	0	UltimateEliminator at SMT-COMP 2021
Vampire	X		X		X	X	33206	33458	5676	Vampire (4.6-smt)
Yices2-QS	X						33316	33422	278	Yices-QS, an extension of Yices for quantified satisfaction
Yices2	X		X				33007	33403	43874423	Yices 2 at SMTCOMP2021
Yices2 incremental		X					33009	33404	89347412	Yices 2 at SMTCOMP2021
Yices2 model-validation				X			33008	33405	13863812	Yices 2 at SMTCOMP2021
YicesLS	X			X			33317	33369	1	LS-IDL: Local Search For SMT on Integer Difference Logic
Z3str4	X						33313	33313	458751	Z3str4 String Solver: System Description
cvc5-gg					X	X	-	11	0	cvc5-gg at the SMT Competition 2021
cvc5-inc		X					33070	33449	5	cvc5 at the SMT Competition 2021
cvc5-mv				X			33069	33447	5	cvc5 at the SMT Competition 2021
cvc5-uc			X				33074	33448	5	cvc5 at the SMT Competition 2021
cvc5	X						33075	33446	5	cvc5 at the SMT Competition 2021
iProver	X						33293	33459	12281	iProver-v3.5 (SMT-COMP 2021)
mc2	X						33279	33279	750	MC2
veriT+raSAT+Redlog	X						33044	33044	54000	veriT+raSAT+Redlog at SMT-COMP 2021
veriT	X						33043	33452	6923	veriT at SMT-COMP 2021
2018-CVC4n	X							19775		CVC4 at the SMT Competition 2018
2018-MathSAT (incremental)n		X						19993
2018-Yicesn	X							19791
2018-Yices (incremental)n		X						19995
2018-Z3n	X							19792
2018-Z3 (incremental)n		X						19996
2019-CVC4-incn		X					23417	23733		CVC4 at the SMT Competition 2019
2019-CVC4n	X						23420	23737		CVC4 at the SMT Competition 2019
2019-MathSAT-defaultn	X						23373	23680		MathSAT5 (Nonlinear) at the SMT Competition 2019
2019-Par4n	X						23391	23672		Par4
2019-SMTInterpoln	X						23360	23554		SMTInterpol
2019-Yices 2.6.2n	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					23470	23470
2020-Bitwuzla-fixedn	X	X	X				29091	29091		Bitwuzla at the SMT Competition 2020
2020-Bitwuzlan	X		X	X			28351	28818		Bitwuzla at the SMT Competition 2020
2020-COLIBRIn	X						28309	28737		COLIBRI
2020-CVC4-incn		X					28466	28799		CVC4 at the SMT Competition 2020
2020-CVC4-ucn			X				28357	28800		CVC4 at the SMT Competition 2020
2020-CVC4n	X						28354	28798		CVC4 at the SMT Competition 2020
2020-MathSAT5n	X	X					28851	28851
2020-OpenSMTn	X			X			28564	28738		OpenSMT in SMT-COMP 2020
2020-SMT-RATn	X						28075	28075		SMT-RAT 20.04
2020-SMTInterpol-fixedn			X				29030	29030		SMTInterpol
2020-Vampiren	X						28324	28782		Vampire 4.5-SMT System Description
2020-Yices2-fixedn	X		X				29032	29032		Yices 2 in SMT-COMP 2020
2020-Yices2-fixed Model Validationn				X			29033	29033		Yices 2 in SMT-COMP 2020
2020-Yices2-fixed incrementaln		X					29034	29034		Yices 2 in SMT-COMP 2020
2020-Yices2n	X		X				28343	28820		Yices 2 in SMT-COMP 2020
2020-Yices2 Model Validationn				X			28464	28819		Yices 2 in SMT-COMP 2020
2020-Yices2 incrementaln		X					28344	28821		Yices 2 in SMT-COMP 2020
2020-z3n	X	X	X	X			28814	28814
Bitwuzla - fixedn		X						33809	0
COLIBRI - fixedn	X							33704	0
MathSAT5n	X	X	X	X				33739	0
OpenSMT - fixedn	X							33687	0
Par4n					X	X	-	12	0	Par4 System Description
Vampire - fixedn	X							33720	0
Z3str4 - fixedn	X							33727	0
cvc5-inc - fixedn		X						33964	0
cvc5-mv - fixedn				X				33966	0
cvc5-uc - fixedn			X					33965	0
cvc5 - fixedn	X							33963	0
iProver - fixedn	X							33670	0
iProver - fixed2n	X							33931	0
z3-mvn				X				33758	0
z3n	X	X	X					33741	0
Total - competing	19	7	7	7	5	3
Total - non-competing	29	16	10	8	1	1
Total	48	23	17	15	6	4			236518915 (mod 230)

n Non-competing.

The opening value of the NYSE Composite Index on 2021-06-15 was 16662.4235, resulting in a competition seed of 236518915 + 1666242 = 238185157.

Divisions

These are the logic divisions in which each solver is participating.

Arith

Solver	Single Query Track	Incremental Track	Unsat Core Track	Cloud Track	Parallel Track
SMTInterpol-remus			LIA LRA NIA NRA
SMTInterpol	LIA LRA NIA NRA	LIA LRA	LIA LRA NIA NRA
UltimateEliminator+MathSAT	LIA LRA NIA NRA	LIA LRA	LIA LRA NIA NRA
Vampire	LIA LRA NIA NRA		LIA LRA NIA NRA	LIA LRA NIA NRA	LIA LRA NIA NRA
Yices2-QS	LIA LRA NIA NRA
cvc5-gg				LIA LRA NIA NRA	LIA LRA NIA NRA
cvc5-inc		LIA LRA
cvc5-uc			LIA LRA NIA NRA
cvc5	LIA LRA NIA NRA
iProver	LIA LRA NIA NRA
veriT	LIA LRA NIA NRA
2018-Z3n	LIA LRA NIA NRA
2019-Par4n	LIA LRA NIA NRA
2020-CVC4-incn		LIA LRA
2020-CVC4-ucn			LIA LRA NIA NRA
2020-CVC4n	LIA LRA NIA NRA
2020-z3n	LIA LRA NIA NRA	LIA LRA
Par4n				LIA LRA NIA NRA	LIA LRA NIA NRA
Vampire - fixedn	LIA LRA NIA NRA
cvc5-inc - fixedn		LIA LRA
cvc5-uc - fixedn			LIA LRA NIA NRA
cvc5 - fixedn	LIA LRA NIA NRA
z3n	LIA LRA NIA NRA	LIA LRA	LIA LRA NIA NRA
Total - competing	7	3	5	2	2
Total - non-competing	7	4	3	1	1
Total	14	7	8	3	3

Bitvec

Solver	Single Query Track	Incremental Track	Unsat Core Track	Cloud Track	Parallel Track
UltimateEliminator+MathSAT	BV	BV	BV
Yices2-QS	BV
cvc5-gg				BV	BV
cvc5-inc		BV
cvc5-uc			BV
cvc5	BV
2019-Par4n	BV
2019-Z3n		BV
2020-CVC4-ucn			BV
Par4n				BV	BV
z3n	BV	BV	BV
Total - competing	3	2	2	1	1
Total - non-competing	2	2	2	1	1
Total	5	4	4	2	2

Equality

Solver	Single Query Track	Incremental Track	Unsat Core Track	Cloud Track	Parallel Track
SMTInterpol-remus			UF UFDT
SMTInterpol	UF UFDT	UF	UF UFDT
UltimateEliminator+MathSAT	UF UFDT	UF	UF UFDT
Vampire	UF UFDT		UF UFDT	UF UFDT	UF UFDT
Yices2	UF UFDT
cvc5-gg				UF UFDT	UF UFDT
cvc5-inc		UF
cvc5-uc			UF UFDT
cvc5	UF UFDT
iProver	UF UFDT
veriT	UF UFDT
2020-CVC4-ucn			UF UFDT
2020-CVC4n	UF UFDT
2020-Vampiren	UF UFDT
2020-z3n		UF
Par4n				UF UFDT	UF UFDT
Vampire - fixedn	UF UFDT
iProver - fixedn	UF UFDT
iProver - fixed2n	UF UFDT
z3n	UF UFDT	UF	UF UFDT
Total - competing	7	3	5	2	2
Total - non-competing	6	2	2	1	1
Total	13	5	7	3	3

Equality+LinearArith

Solver	Single Query Track	Incremental Track	Unsat Core Track	Cloud Track	Parallel Track
SMTInterpol-remus			ALIA AUFDTLIA AUFDTLIRA AUFLIA AUFLIRA UFDTLIA UFDTLIRA UFIDL UFLIA UFLRA
SMTInterpol	ALIA AUFDTLIA AUFDTLIRA AUFLIA AUFLIRA UFDTLIA UFDTLIRA UFIDL UFLIA UFLRA	ALIA UFLRA	ALIA AUFDTLIA AUFDTLIRA AUFLIA AUFLIRA UFDTLIA UFDTLIRA UFIDL UFLIA UFLRA
UltimateEliminator+MathSAT	ALIA AUFDTLIA AUFDTLIRA AUFLIA AUFLIRA UFDTLIA UFDTLIRA UFIDL UFLIA UFLRA	ALIA UFLRA	ALIA AUFDTLIA AUFDTLIRA AUFLIA AUFLIRA UFDTLIA UFDTLIRA UFIDL UFLIA UFLRA
Vampire	ALIA AUFDTLIA AUFDTLIRA AUFLIA AUFLIRA UFDTLIA UFDTLIRA UFIDL UFLIA UFLRA		ALIA AUFDTLIA AUFDTLIRA AUFLIA AUFLIRA UFDTLIA UFDTLIRA UFIDL UFLIA UFLRA	ALIA AUFDTLIA AUFDTLIRA AUFLIA AUFLIRA UFDTLIA UFDTLIRA UFIDL UFLIA UFLRA	ALIA AUFDTLIA AUFDTLIRA AUFLIA AUFLIRA UFDTLIA UFDTLIRA UFIDL UFLIA UFLRA
cvc5-gg				ALIA AUFDTLIA AUFDTLIRA AUFLIA AUFLIRA UFDTLIA UFDTLIRA UFIDL UFLIA UFLRA	ALIA AUFDTLIA AUFDTLIRA AUFLIA AUFLIRA UFDTLIA UFDTLIRA UFIDL UFLIA UFLRA
cvc5-inc		ALIA UFLRA
cvc5-uc			ALIA AUFDTLIA AUFDTLIRA AUFLIA AUFLIRA UFDTLIA UFDTLIRA UFIDL UFLIA UFLRA
cvc5	ALIA AUFDTLIA AUFDTLIRA AUFLIA AUFLIRA UFDTLIA UFDTLIRA UFIDL UFLIA UFLRA
iProver	ALIA AUFDTLIA AUFDTLIRA AUFLIA AUFLIRA UFDTLIA UFDTLIRA UFIDL UFLIA UFLRA
veriT	ALIA AUFDTLIA AUFDTLIRA AUFLIA AUFLIRA UFDTLIA UFDTLIRA UFIDL UFLIA UFLRA
2018-CVC4n	ALIA AUFDTLIA AUFDTLIRA AUFLIA AUFLIRA UFDTLIA UFDTLIRA UFIDL UFLIA UFLRA
2018-Z3n	ALIA AUFDTLIA AUFDTLIRA AUFLIA AUFLIRA UFDTLIA UFDTLIRA UFIDL UFLIA UFLRA
2019-CVC4n	ALIA AUFDTLIA AUFDTLIRA AUFLIA AUFLIRA UFDTLIA UFDTLIRA UFIDL UFLIA UFLRA
2019-Par4n	ALIA AUFDTLIA AUFDTLIRA AUFLIA AUFLIRA UFDTLIA UFDTLIRA UFIDL UFLIA UFLRA
2019-Z3n		ALIA UFLRA
2020-CVC4-ucn			ALIA AUFDTLIA AUFDTLIRA AUFLIA AUFLIRA UFDTLIA UFDTLIRA UFIDL UFLIA UFLRA
2020-CVC4n	ALIA AUFDTLIA AUFDTLIRA AUFLIA AUFLIRA UFDTLIA UFDTLIRA UFIDL UFLIA UFLRA
2020-Vampiren	ALIA AUFDTLIA AUFDTLIRA AUFLIA AUFLIRA UFDTLIA UFDTLIRA UFIDL UFLIA UFLRA
2020-z3n	ALIA AUFDTLIA AUFDTLIRA AUFLIA AUFLIRA UFDTLIA UFDTLIRA UFIDL UFLIA UFLRA	ALIA UFLRA	ALIA AUFDTLIA AUFDTLIRA AUFLIA AUFLIRA UFDTLIA UFDTLIRA UFIDL UFLIA UFLRA
Par4n				ALIA AUFDTLIA AUFDTLIRA AUFLIA AUFLIRA UFDTLIA UFDTLIRA UFIDL UFLIA UFLRA	ALIA AUFDTLIA AUFDTLIRA AUFLIA AUFLIRA UFDTLIA UFDTLIRA UFIDL UFLIA UFLRA
Vampire - fixedn	ALIA AUFDTLIA AUFDTLIRA AUFLIA AUFLIRA UFDTLIA UFDTLIRA UFIDL UFLIA UFLRA
cvc5-inc - fixedn		ALIA UFLRA
cvc5-uc - fixedn			ALIA AUFDTLIA AUFDTLIRA AUFLIA AUFLIRA UFDTLIA UFDTLIRA UFIDL UFLIA UFLRA
cvc5 - fixedn	ALIA AUFDTLIA AUFDTLIRA AUFLIA AUFLIRA UFDTLIA UFDTLIRA UFIDL UFLIA UFLRA
z3n	ALIA AUFDTLIA AUFDTLIRA AUFLIA AUFLIRA UFDTLIA UFDTLIRA UFIDL UFLIA UFLRA	ALIA UFLRA	ALIA AUFDTLIA AUFDTLIRA AUFLIA AUFLIRA UFDTLIA UFDTLIRA UFIDL UFLIA UFLRA
Total - competing	6	3	5	2	2
Total - non-competing	10	4	4	1	1
Total	16	7	9	3	3

Equality+MachineArith

Solver	Single Query Track	Incremental Track	Unsat Core Track	Cloud Track	Parallel Track
UltimateEliminator+MathSAT	ABV ABVFP ABVFPLRA AUFBV AUFBVDTLIA AUFBVDTNIA AUFBVFP AUFFPDTLIRA UFBV UFBVFP UFBVLIA UFFPDTLIRA UFFPDTNIRA	ABVFP	ABV ABVFP ABVFPLRA AUFBV AUFBVDTLIA AUFBVDTNIA AUFBVFP AUFFPDTLIRA UFBV UFBVFP UFBVLIA UFFPDTLIRA UFFPDTNIRA
cvc5-gg				ABV ABVFP ABVFPLRA AUFBV AUFBVDTLIA AUFBVDTNIA AUFBVFP AUFFPDTLIRA UFBV UFBVFP UFBVLIA UFFPDTLIRA UFFPDTNIRA	ABV ABVFP ABVFPLRA AUFBV AUFBVDTLIA AUFBVDTNIA AUFBVFP AUFFPDTLIRA UFBV UFBVFP UFBVLIA UFFPDTLIRA UFFPDTNIRA
cvc5-inc		ABVFP
cvc5-uc			ABV ABVFP ABVFPLRA AUFBV AUFBVDTLIA AUFBVDTNIA AUFBVFP AUFFPDTLIRA UFBV UFBVFP UFBVLIA UFFPDTLIRA UFFPDTNIRA
cvc5	ABV ABVFP ABVFPLRA AUFBV AUFBVDTLIA AUFBVDTNIA AUFBVFP AUFFPDTLIRA UFBV UFBVFP UFBVLIA UFFPDTLIRA UFFPDTNIRA
2018-Z3n	ABV ABVFP ABVFPLRA AUFBV AUFBVDTLIA AUFBVDTNIA AUFBVFP AUFFPDTLIRA UFBV UFBVFP UFBVLIA UFFPDTLIRA UFFPDTNIRA
2020-CVC4-ucn			ABV ABVFP ABVFPLRA AUFBV AUFBVDTLIA AUFBVDTNIA AUFBVFP AUFFPDTLIRA UFBV UFBVFP UFBVLIA UFFPDTLIRA UFFPDTNIRA
2020-CVC4n	ABV ABVFP ABVFPLRA AUFBV AUFBVDTLIA AUFBVDTNIA AUFBVFP AUFFPDTLIRA UFBV UFBVFP UFBVLIA UFFPDTLIRA UFFPDTNIRA
2020-z3n	ABV ABVFP ABVFPLRA AUFBV AUFBVDTLIA AUFBVDTNIA AUFBVFP AUFFPDTLIRA UFBV UFBVFP UFBVLIA UFFPDTLIRA UFFPDTNIRA
Par4n				ABV ABVFP ABVFPLRA AUFBV AUFBVDTLIA AUFBVDTNIA AUFBVFP AUFFPDTLIRA UFBV UFBVFP UFBVLIA UFFPDTLIRA UFFPDTNIRA	ABV ABVFP ABVFPLRA AUFBV AUFBVDTLIA AUFBVDTNIA AUFBVFP AUFFPDTLIRA UFBV UFBVFP UFBVLIA UFFPDTLIRA UFFPDTNIRA
cvc5-uc - fixedn			ABV ABVFP ABVFPLRA AUFBV AUFBVDTLIA AUFBVDTNIA AUFBVFP AUFFPDTLIRA UFBV UFBVFP UFBVLIA UFFPDTLIRA UFFPDTNIRA
cvc5 - fixedn	ABV ABVFP ABVFPLRA AUFBV AUFBVDTLIA AUFBVDTNIA AUFBVFP AUFFPDTLIRA UFBV UFBVFP UFBVLIA UFFPDTLIRA UFFPDTNIRA
z3n	ABV ABVFP ABVFPLRA AUFBV AUFBVDTLIA AUFBVDTNIA AUFBVFP AUFFPDTLIRA UFBV UFBVFP UFBVLIA UFFPDTLIRA UFFPDTNIRA		ABV ABVFP ABVFPLRA AUFBV AUFBVDTLIA AUFBVDTNIA AUFBVFP AUFFPDTLIRA UFBV UFBVFP UFBVLIA UFFPDTLIRA UFFPDTNIRA
Total - competing	2	2	2	1	1
Total - non-competing	5	0	3	1	1
Total	7	2	5	2	2

Equality+NonLinearArith

Solver	Single Query Track	Incremental Track	Unsat Core Track	Cloud Track	Parallel Track
SMTInterpol	AUFDTNIRA AUFFPDTNIRA AUFNIA AUFNIRA UFDTNIA UFDTNIRA UFNIA	ANIA AUFNIRA UFDTNIA UFNIA UFNRA	AUFDTNIRA AUFFPDTNIRA AUFNIA AUFNIRA UFDTNIA UFDTNIRA UFNIA
UltimateEliminator+MathSAT	AUFDTNIRA AUFFPDTNIRA AUFNIA AUFNIRA UFDTNIA UFDTNIRA UFNIA	ANIA AUFNIRA UFDTNIA UFNIA UFNRA	AUFDTNIRA AUFFPDTNIRA AUFNIA AUFNIRA UFDTNIA UFDTNIRA UFNIA
Vampire	AUFDTNIRA AUFFPDTNIRA AUFNIA AUFNIRA UFDTNIA UFDTNIRA UFNIA		AUFDTNIRA AUFFPDTNIRA AUFNIA AUFNIRA UFDTNIA UFDTNIRA UFNIA	AUFDTNIRA AUFFPDTNIRA AUFNIA AUFNIRA UFDTNIA UFDTNIRA UFNIA	AUFDTNIRA AUFFPDTNIRA AUFNIA AUFNIRA UFDTNIA UFDTNIRA UFNIA
cvc5-gg				AUFDTNIRA AUFFPDTNIRA AUFNIA AUFNIRA UFDTNIA UFDTNIRA UFNIA	AUFDTNIRA AUFFPDTNIRA AUFNIA AUFNIRA UFDTNIA UFDTNIRA UFNIA
cvc5-inc		ANIA AUFNIRA UFDTNIA UFNIA UFNRA
cvc5-uc			AUFDTNIRA AUFFPDTNIRA AUFNIA AUFNIRA UFDTNIA UFDTNIRA UFNIA
cvc5	AUFDTNIRA AUFFPDTNIRA AUFNIA AUFNIRA UFDTNIA UFDTNIRA UFNIA
iProver	AUFDTNIRA AUFFPDTNIRA AUFNIA AUFNIRA UFDTNIA UFDTNIRA UFNIA
2019-CVC4-incn		ANIA AUFNIRA UFDTNIA UFNIA UFNRA
2019-Par4n	AUFDTNIRA AUFFPDTNIRA AUFNIA AUFNIRA UFDTNIA UFDTNIRA UFNIA
2020-CVC4-incn		ANIA AUFNIRA UFDTNIA UFNIA UFNRA
2020-CVC4-ucn			AUFDTNIRA AUFFPDTNIRA AUFNIA AUFNIRA UFDTNIA UFDTNIRA UFNIA
2020-CVC4n	AUFDTNIRA AUFFPDTNIRA AUFNIA AUFNIRA UFDTNIA UFDTNIRA UFNIA
2020-Vampiren	AUFDTNIRA AUFFPDTNIRA AUFNIA AUFNIRA UFDTNIA UFDTNIRA UFNIA
2020-z3n		ANIA AUFNIRA UFDTNIA UFNIA UFNRA
Par4n				AUFDTNIRA AUFFPDTNIRA AUFNIA AUFNIRA UFDTNIA UFDTNIRA UFNIA	AUFDTNIRA AUFFPDTNIRA AUFNIA AUFNIRA UFDTNIA UFDTNIRA UFNIA
Vampire - fixedn	AUFDTNIRA AUFFPDTNIRA AUFNIA AUFNIRA UFDTNIA UFDTNIRA UFNIA
cvc5-inc - fixedn		ANIA AUFNIRA UFDTNIA UFNIA UFNRA
cvc5-uc - fixedn			AUFDTNIRA AUFFPDTNIRA AUFNIA AUFNIRA UFDTNIA UFDTNIRA UFNIA
cvc5 - fixedn	AUFDTNIRA AUFFPDTNIRA AUFNIA AUFNIRA UFDTNIA UFDTNIRA UFNIA
z3n	AUFDTNIRA AUFFPDTNIRA AUFNIA AUFNIRA UFDTNIA UFDTNIRA UFNIA	ANIA AUFNIRA UFDTNIA UFNIA UFNRA	AUFDTNIRA AUFFPDTNIRA AUFNIA AUFNIRA UFDTNIA UFDTNIRA UFNIA
Total - competing	5	3	4	2	2
Total - non-competing	6	5	3	1	1
Total	11	8	7	3	3

FPArith

Solver	Single Query Track	Incremental Track	Unsat Core Track	Cloud Track	Parallel Track
UltimateEliminator+MathSAT	BVFP BVFPLRA FP FPLRA	BVFP	BVFP BVFPLRA FP FPLRA
cvc5-gg				BVFP BVFPLRA FP FPLRA	BVFP BVFPLRA FP FPLRA
cvc5-inc		BVFP
cvc5-uc			BVFP BVFPLRA FP FPLRA
cvc5	BVFP BVFPLRA FP FPLRA
2019-CVC4-incn		BVFP
2019-Z3n	BVFP BVFPLRA FP FPLRA
2020-CVC4-ucn			BVFP BVFPLRA FP FPLRA
2020-CVC4n	BVFP BVFPLRA FP FPLRA
z3n	BVFP BVFPLRA FP FPLRA		BVFP BVFPLRA FP FPLRA
Total - competing	2	2	2	1	1
Total - non-competing	3	1	2	0	0
Total	5	3	4	1	1

QF_Bitvec

Solver	Single Query Track	Incremental Track	Unsat Core Track	Model Validation Track	Cloud Track	Parallel Track
Bitwuzla	QF_BV	QF_BV	QF_BV	QF_BV
STP-CMS-Cloud					QF_BV
STP-parallel						QF_BV
STP	QF_BV	QF_BV		QF_BV
Yices2	QF_BV		QF_BV
Yices2 incremental		QF_BV
Yices2 model-validation				QF_BV
cvc5-gg					QF_BV	QF_BV
cvc5-inc		QF_BV
cvc5-mv				QF_BV
cvc5-uc			QF_BV
cvc5	QF_BV
2020-Bitwuzla-fixedn	QF_BV		QF_BV
2020-Bitwuzlan				QF_BV
2020-Yices2-fixed incrementaln		QF_BV
MathSAT5n	QF_BV	QF_BV	QF_BV	QF_BV
Par4n					QF_BV	QF_BV
z3-mvn				QF_BV
z3n	QF_BV	QF_BV	QF_BV
Total - competing	4	4	3	4	2	2
Total - non-competing	3	3	3	3	1	1
Total	7	7	6	7	3	3

QF_Equality

Solver	Single Query Track	Incremental Track	Unsat Core Track	Model Validation Track	Cloud Track	Parallel Track
OpenSMT	QF_AX QF_DT QF_UF QF_UFDT	QF_UF		QF_UF
SMTInterpol-remus			QF_AX QF_DT QF_UF QF_UFDT
SMTInterpol	QF_AX QF_DT QF_UF QF_UFDT	QF_UF	QF_AX QF_DT QF_UF QF_UFDT	QF_UF
SMTS cube-and-conquer					QF_AX QF_DT QF_UF QF_UFDT
SMTS portfolio					QF_AX QF_DT QF_UF QF_UFDT
Yices2	QF_AX QF_DT QF_UF QF_UFDT		QF_AX QF_DT QF_UF QF_UFDT
Yices2 incremental		QF_UF
Yices2 model-validation				QF_UF
cvc5-gg					QF_AX QF_DT QF_UF QF_UFDT	QF_AX QF_DT QF_UF QF_UFDT
cvc5-inc		QF_UF
cvc5-mv				QF_UF
cvc5-uc			QF_AX QF_DT QF_UF QF_UFDT
cvc5	QF_AX QF_DT QF_UF QF_UFDT
veriT	QF_AX QF_DT QF_UF QF_UFDT
2019-Par4n	QF_AX QF_DT QF_UF QF_UFDT
2019-Yices 2.6.2 Incrementaln		QF_UF
2020-SMTInterpol-fixedn			QF_AX QF_DT QF_UF QF_UFDT
2020-Yices2-fixedn	QF_AX QF_DT QF_UF QF_UFDT		QF_AX QF_DT QF_UF QF_UFDT
2020-Yices2n	QF_AX QF_DT QF_UF QF_UFDT
2020-z3n	QF_AX QF_DT QF_UF QF_UFDT
MathSAT5n	QF_AX QF_DT QF_UF QF_UFDT	QF_UF	QF_AX QF_DT QF_UF QF_UFDT	QF_UF
Par4n					QF_AX QF_DT QF_UF QF_UFDT	QF_AX QF_DT QF_UF QF_UFDT
z3-mvn				QF_UF
z3n	QF_AX QF_DT QF_UF QF_UFDT	QF_UF	QF_AX QF_DT QF_UF QF_UFDT
Total - competing	5	4	4	4	3	1
Total - non-competing	6	3	4	2	1	1
Total	11	7	8	6	4	2

QF_Equality+Bitvec

Solver	Single Query Track	Incremental Track	Unsat Core Track	Model Validation Track	Cloud Track	Parallel Track
Bitwuzla	QF_ABV QF_AUFBV QF_UFBV	QF_ABV QF_AUFBV QF_UFBV	QF_ABV QF_AUFBV QF_UFBV	QF_UFBV
Yices2	QF_ABV QF_AUFBV QF_UFBV		QF_ABV QF_AUFBV QF_UFBV
Yices2 incremental		QF_ABV QF_AUFBV QF_UFBV
Yices2 model-validation				QF_UFBV
cvc5-gg					QF_ABV QF_AUFBV QF_UFBV	QF_ABV QF_AUFBV QF_UFBV
cvc5-inc		QF_ABV QF_AUFBV QF_UFBV
cvc5-mv				QF_UFBV
cvc5-uc			QF_ABV QF_AUFBV QF_UFBV
cvc5	QF_ABV QF_AUFBV QF_UFBV
2020-Bitwuzla-fixedn		QF_ABV QF_AUFBV QF_UFBV
2020-Bitwuzlan	QF_ABV QF_AUFBV QF_UFBV
2020-Yices2-fixedn	QF_ABV QF_AUFBV QF_UFBV
2020-Yices2n	QF_ABV QF_AUFBV QF_UFBV		QF_ABV QF_AUFBV QF_UFBV
2020-Yices2 incrementaln		QF_ABV QF_AUFBV QF_UFBV
2020-z3n			QF_ABV QF_AUFBV QF_UFBV
MathSAT5n	QF_ABV QF_AUFBV QF_UFBV	QF_ABV QF_AUFBV QF_UFBV	QF_ABV QF_AUFBV QF_UFBV	QF_UFBV
Par4n					QF_ABV QF_AUFBV QF_UFBV	QF_ABV QF_AUFBV QF_UFBV
z3-mvn				QF_UFBV
z3n	QF_ABV QF_AUFBV QF_UFBV	QF_ABV QF_AUFBV QF_UFBV	QF_ABV QF_AUFBV QF_UFBV
Total - competing	3	3	3	3	1	1
Total - non-competing	5	4	4	2	1	1
Total	8	7	7	5	2	2

QF_Equality+Bitvec+Arith

Solver	Incremental Track
cvc5-inc	QF_AUFBVLIA QF_AUFBVNIA QF_UFBVLIA
MathSAT5n	QF_AUFBVLIA QF_AUFBVNIA QF_UFBVLIA
cvc5-inc - fixedn	QF_AUFBVLIA QF_AUFBVNIA QF_UFBVLIA
Total - competing	1
Total - non-competing	2
Total	3

QF_Equality+LinearArith

Solver	Single Query Track	Incremental Track	Unsat Core Track	Model Validation Track	Cloud Track	Parallel Track
SMTInterpol-remus			QF_ALIA QF_AUFLIA QF_UFDTLIRA QF_UFIDL QF_UFLIA QF_UFLRA
SMTInterpol	QF_ALIA QF_AUFLIA QF_UFDTLIRA QF_UFIDL QF_UFLIA QF_UFLRA	QF_ALIA QF_AUFLIA QF_UFLIA QF_UFLRA	QF_ALIA QF_AUFLIA QF_UFDTLIRA QF_UFIDL QF_UFLIA QF_UFLRA	QF_UFIDL QF_UFLRA QF_UFLIA
Yices2	QF_ALIA QF_AUFLIA QF_UFDTLIRA QF_UFIDL QF_UFLIA QF_UFLRA		QF_ALIA QF_AUFLIA QF_UFDTLIRA QF_UFIDL QF_UFLIA QF_UFLRA
Yices2 incremental		QF_ALIA QF_AUFLIA QF_UFLIA QF_UFLRA
Yices2 model-validation				QF_UFIDL QF_UFLRA QF_UFLIA
cvc5-gg					QF_ALIA QF_AUFLIA QF_UFDTLIRA QF_UFIDL QF_UFLIA QF_UFLRA	QF_ALIA QF_AUFLIA QF_UFDTLIRA QF_UFIDL QF_UFLIA QF_UFLRA
cvc5-inc		QF_ALIA QF_AUFLIA QF_UFLIA QF_UFLRA
cvc5-mv				QF_UFIDL QF_UFLRA QF_UFLIA
cvc5-uc			QF_ALIA QF_AUFLIA QF_UFDTLIRA QF_UFIDL QF_UFLIA QF_UFLRA
cvc5	QF_ALIA QF_AUFLIA QF_UFDTLIRA QF_UFIDL QF_UFLIA QF_UFLRA
mc2	QF_ALIA QF_AUFLIA QF_UFDTLIRA QF_UFIDL QF_UFLIA QF_UFLRA
veriT	QF_ALIA QF_AUFLIA QF_UFDTLIRA QF_UFIDL QF_UFLIA QF_UFLRA
2018-Yicesn	QF_ALIA QF_AUFLIA QF_UFDTLIRA QF_UFIDL QF_UFLIA QF_UFLRA
2018-Yices (incremental)n		QF_ALIA QF_AUFLIA QF_UFLIA QF_UFLRA
2018-Z3 (incremental)n		QF_ALIA QF_AUFLIA QF_UFLIA QF_UFLRA
2019-SMTInterpoln	QF_ALIA QF_AUFLIA QF_UFDTLIRA QF_UFIDL QF_UFLIA QF_UFLRA
2019-Yices 2.6.2n	QF_ALIA QF_AUFLIA QF_UFDTLIRA QF_UFIDL QF_UFLIA QF_UFLRA
2020-CVC4-ucn			QF_ALIA QF_AUFLIA QF_UFDTLIRA QF_UFIDL QF_UFLIA QF_UFLRA
2020-Yices2-fixedn			QF_ALIA QF_AUFLIA QF_UFDTLIRA QF_UFIDL QF_UFLIA QF_UFLRA
2020-z3n		QF_ALIA QF_AUFLIA QF_UFLIA QF_UFLRA	QF_ALIA QF_AUFLIA QF_UFDTLIRA QF_UFIDL QF_UFLIA QF_UFLRA
MathSAT5n	QF_ALIA QF_AUFLIA QF_UFDTLIRA QF_UFIDL QF_UFLIA QF_UFLRA	QF_ALIA QF_AUFLIA QF_UFLIA QF_UFLRA	QF_ALIA QF_AUFLIA QF_UFDTLIRA QF_UFIDL QF_UFLIA QF_UFLRA	QF_UFIDL QF_UFLRA QF_UFLIA
cvc5-inc - fixedn		QF_ALIA QF_AUFLIA QF_UFLIA QF_UFLRA
cvc5-mv - fixedn				QF_UFIDL QF_UFLRA QF_UFLIA
cvc5-uc - fixedn			QF_ALIA QF_AUFLIA QF_UFDTLIRA QF_UFIDL QF_UFLIA QF_UFLRA
cvc5 - fixedn	QF_ALIA QF_AUFLIA QF_UFDTLIRA QF_UFIDL QF_UFLIA QF_UFLRA
z3-mvn				QF_UFIDL QF_UFLRA QF_UFLIA
z3n	QF_ALIA QF_AUFLIA QF_UFDTLIRA QF_UFIDL QF_UFLIA QF_UFLRA	QF_ALIA QF_AUFLIA QF_UFLIA QF_UFLRA	QF_ALIA QF_AUFLIA QF_UFDTLIRA QF_UFIDL QF_UFLIA QF_UFLRA
Total - competing	5	3	4	3	1	1
Total - non-competing	6	6	6	3	0	0
Total	11	9	10	6	1	1

QF_Equality+NonLinearArith

Solver	Single Query Track	Incremental Track	Unsat Core Track	Cloud Track	Parallel Track
SMTInterpol		QF_ANIA QF_UFNIA QF_UFNRA
Yices2	QF_ANIA QF_AUFNIA QF_UFNIA QF_UFNRA		QF_ANIA QF_AUFNIA QF_UFNIA QF_UFNRA
Yices2 incremental		QF_ANIA QF_UFNIA QF_UFNRA
cvc5-gg				QF_ANIA QF_AUFNIA QF_UFNIA QF_UFNRA	QF_ANIA QF_AUFNIA QF_UFNIA QF_UFNRA
cvc5-inc		QF_ANIA QF_UFNIA QF_UFNRA
cvc5-uc			QF_ANIA QF_AUFNIA QF_UFNIA QF_UFNRA
cvc5	QF_ANIA QF_AUFNIA QF_UFNIA QF_UFNRA
veriT+raSAT+Redlog	QF_ANIA QF_AUFNIA QF_UFNIA QF_UFNRA
2019-CVC4n	QF_ANIA QF_AUFNIA QF_UFNIA QF_UFNRA
2019-MathSAT-defaultn	QF_ANIA QF_AUFNIA QF_UFNIA QF_UFNRA
2019-Par4n	QF_ANIA QF_AUFNIA QF_UFNIA QF_UFNRA
2020-CVC4n	QF_ANIA QF_AUFNIA QF_UFNIA QF_UFNRA
2020-MathSAT5n		QF_ANIA QF_UFNIA QF_UFNRA
MathSAT5n	QF_ANIA QF_AUFNIA QF_UFNIA QF_UFNRA	QF_ANIA QF_UFNIA QF_UFNRA	QF_ANIA QF_AUFNIA QF_UFNIA QF_UFNRA
Par4n				QF_ANIA QF_AUFNIA QF_UFNIA QF_UFNRA	QF_ANIA QF_AUFNIA QF_UFNIA QF_UFNRA
cvc5-inc - fixedn		QF_ANIA QF_UFNIA QF_UFNRA
cvc5-uc - fixedn			QF_ANIA QF_AUFNIA QF_UFNIA QF_UFNRA
cvc5 - fixedn	QF_ANIA QF_AUFNIA QF_UFNIA QF_UFNRA
z3n	QF_ANIA QF_AUFNIA QF_UFNIA QF_UFNRA	QF_ANIA QF_UFNIA QF_UFNRA	QF_ANIA QF_AUFNIA QF_UFNIA QF_UFNRA
Total - competing	3	3	2	1	1
Total - non-competing	7	4	3	1	1
Total	10	7	5	2	2

QF_FPArith

Solver	Single Query Track	Incremental Track	Unsat Core Track	Cloud Track	Parallel Track
Bitwuzla	QF_ABVFP QF_ABVFPLRA QF_AUFBVFP QF_BVFP QF_BVFPLRA QF_FP QF_FPLRA QF_UFFP QF_UFFPDTLIRA	QF_ABVFP QF_BVFP QF_FP QF_UFFP	QF_ABVFP QF_ABVFPLRA QF_AUFBVFP QF_BVFP QF_BVFPLRA QF_FP QF_FPLRA QF_UFFP QF_UFFPDTLIRA
COLIBRI	QF_ABVFP QF_ABVFPLRA QF_AUFBVFP QF_BVFP QF_BVFPLRA QF_FP QF_FPLRA QF_UFFP QF_UFFPDTLIRA
cvc5-gg				QF_ABVFP QF_ABVFPLRA QF_AUFBVFP QF_BVFP QF_BVFPLRA QF_FP QF_FPLRA QF_UFFP QF_UFFPDTLIRA	QF_ABVFP QF_ABVFPLRA QF_AUFBVFP QF_BVFP QF_BVFPLRA QF_FP QF_FPLRA QF_UFFP QF_UFFPDTLIRA
cvc5-inc		QF_ABVFP QF_BVFP QF_FP QF_UFFP
cvc5-uc			QF_ABVFP QF_ABVFPLRA QF_AUFBVFP QF_BVFP QF_BVFPLRA QF_FP QF_FPLRA QF_UFFP QF_UFFPDTLIRA
cvc5	QF_ABVFP QF_ABVFPLRA QF_AUFBVFP QF_BVFP QF_BVFPLRA QF_FP QF_FPLRA QF_UFFP QF_UFFPDTLIRA
2020-Bitwuzla-fixedn	QF_ABVFP QF_ABVFPLRA QF_AUFBVFP QF_BVFP QF_BVFPLRA QF_FP QF_FPLRA QF_UFFP QF_UFFPDTLIRA	QF_ABVFP QF_BVFP QF_FP QF_UFFP	QF_ABVFP QF_ABVFPLRA QF_AUFBVFP QF_BVFP QF_BVFPLRA QF_FP QF_FPLRA QF_UFFP QF_UFFPDTLIRA
2020-Bitwuzlan	QF_ABVFP QF_ABVFPLRA QF_AUFBVFP QF_BVFP QF_BVFPLRA QF_FP QF_FPLRA QF_UFFP QF_UFFPDTLIRA		QF_ABVFP QF_ABVFPLRA QF_AUFBVFP QF_BVFP QF_BVFPLRA QF_FP QF_FPLRA QF_UFFP QF_UFFPDTLIRA
2020-COLIBRIn	QF_ABVFP QF_ABVFPLRA QF_AUFBVFP QF_BVFP QF_BVFPLRA QF_FP QF_FPLRA QF_UFFP QF_UFFPDTLIRA
2020-CVC4-incn		QF_ABVFP QF_BVFP QF_FP QF_UFFP
2020-CVC4n	QF_ABVFP QF_ABVFPLRA QF_AUFBVFP QF_BVFP QF_BVFPLRA QF_FP QF_FPLRA QF_UFFP QF_UFFPDTLIRA
2020-MathSAT5n	QF_ABVFP QF_ABVFPLRA QF_AUFBVFP QF_BVFP QF_BVFPLRA QF_FP QF_FPLRA QF_UFFP QF_UFFPDTLIRA
Bitwuzla - fixedn		QF_ABVFP QF_BVFP QF_FP QF_UFFP
COLIBRI - fixedn	QF_ABVFP QF_ABVFPLRA QF_AUFBVFP QF_BVFP QF_BVFPLRA QF_FP QF_FPLRA QF_UFFP QF_UFFPDTLIRA
MathSAT5n	QF_ABVFP QF_ABVFPLRA QF_AUFBVFP QF_BVFP QF_BVFPLRA QF_FP QF_FPLRA QF_UFFP QF_UFFPDTLIRA	QF_ABVFP QF_BVFP QF_FP QF_UFFP	QF_ABVFP QF_ABVFPLRA QF_AUFBVFP QF_BVFP QF_BVFPLRA QF_FP QF_FPLRA QF_UFFP QF_UFFPDTLIRA
Par4n				QF_ABVFP QF_ABVFPLRA QF_AUFBVFP QF_BVFP QF_BVFPLRA QF_FP QF_FPLRA QF_UFFP QF_UFFPDTLIRA	QF_ABVFP QF_ABVFPLRA QF_AUFBVFP QF_BVFP QF_BVFPLRA QF_FP QF_FPLRA QF_UFFP QF_UFFPDTLIRA
cvc5-uc - fixedn			QF_ABVFP QF_ABVFPLRA QF_AUFBVFP QF_BVFP QF_BVFPLRA QF_FP QF_FPLRA QF_UFFP QF_UFFPDTLIRA
cvc5 - fixedn	QF_ABVFP QF_ABVFPLRA QF_AUFBVFP QF_BVFP QF_BVFPLRA QF_FP QF_FPLRA QF_UFFP QF_UFFPDTLIRA
z3n	QF_ABVFP QF_ABVFPLRA QF_AUFBVFP QF_BVFP QF_BVFPLRA QF_FP QF_FPLRA QF_UFFP QF_UFFPDTLIRA	QF_ABVFP QF_BVFP QF_FP QF_UFFP	QF_ABVFP QF_ABVFPLRA QF_AUFBVFP QF_BVFP QF_BVFPLRA QF_FP QF_FPLRA QF_UFFP QF_UFFPDTLIRA
Total - competing	3	2	2	1	1
Total - non-competing	9	5	5	1	1
Total	12	7	7	2	2

QF_LinearIntArith

Solver	Single Query Track	Incremental Track	Unsat Core Track	Model Validation Track	Cloud Track	Parallel Track
OpenSMT	QF_IDL QF_LIA QF_LIRA	QF_LIA		QF_IDL QF_LIA QF_LIRA
SMTInterpol-remus			QF_IDL QF_LIA QF_LIRA
SMTInterpol	QF_IDL QF_LIA QF_LIRA	QF_LIA	QF_IDL QF_LIA QF_LIRA	QF_IDL QF_LIA QF_LIRA
SMTS cube-and-conquer					QF_IDL QF_LIA QF_LIRA
SMTS portfolio					QF_IDL QF_LIA QF_LIRA
Yices2	QF_IDL QF_LIA QF_LIRA		QF_IDL QF_LIA QF_LIRA
Yices2 incremental		QF_LIA
Yices2 model-validation				QF_IDL QF_LIA QF_LIRA
YicesLS	QF_IDL QF_LIA QF_LIRA			QF_IDL QF_LIA QF_LIRA
cvc5-gg					QF_IDL QF_LIA QF_LIRA	QF_IDL QF_LIA QF_LIRA
cvc5-inc		QF_LIA
cvc5-mv				QF_IDL QF_LIA QF_LIRA
cvc5-uc			QF_IDL QF_LIA QF_LIRA
cvc5	QF_IDL QF_LIA QF_LIRA
veriT	QF_IDL QF_LIA QF_LIRA
2019-Par4n	QF_IDL QF_LIA QF_LIRA
2020-Yices2-fixedn			QF_IDL QF_LIA QF_LIRA
2020-Yices2-fixed Model Validationn				QF_IDL QF_LIA QF_LIRA
2020-Yices2-fixed incrementaln		QF_LIA
2020-Yices2 Model Validationn				QF_IDL QF_LIA QF_LIRA
2020-z3n				QF_IDL QF_LIA QF_LIRA
MathSAT5n	QF_IDL QF_LIA QF_LIRA	QF_LIA	QF_IDL QF_LIA QF_LIRA	QF_IDL QF_LIA QF_LIRA
OpenSMT - fixedn	QF_IDL QF_LIA QF_LIRA
Par4n					QF_IDL QF_LIA QF_LIRA	QF_IDL QF_LIA QF_LIRA
cvc5-inc - fixedn		QF_LIA
cvc5-mv - fixedn				QF_IDL QF_LIA QF_LIRA
cvc5-uc - fixedn			QF_IDL QF_LIA QF_LIRA
cvc5 - fixedn	QF_IDL QF_LIA QF_LIRA
z3-mvn				QF_IDL QF_LIA QF_LIRA
z3n	QF_IDL QF_LIA QF_LIRA	QF_LIA	QF_IDL QF_LIA QF_LIRA
Total - competing	6	4	4	5	3	1
Total - non-competing	5	4	4	6	1	1
Total	11	8	8	11	4	2

QF_LinearRealArith

Solver	Single Query Track	Incremental Track	Unsat Core Track	Model Validation Track	Cloud Track	Parallel Track
OpenSMT	QF_LRA QF_RDL	QF_LRA		QF_RDL QF_LRA
SMTInterpol-remus			QF_LRA QF_RDL
SMTInterpol	QF_LRA QF_RDL	QF_LRA	QF_LRA QF_RDL	QF_RDL QF_LRA
SMTS cube-and-conquer					QF_LRA QF_RDL
SMTS portfolio					QF_LRA QF_RDL
Yices2	QF_LRA QF_RDL		QF_LRA QF_RDL
Yices2 incremental		QF_LRA
Yices2 model-validation				QF_RDL QF_LRA
cvc5-gg					QF_LRA QF_RDL	QF_LRA QF_RDL
cvc5-inc		QF_LRA
cvc5-mv				QF_RDL QF_LRA
cvc5-uc			QF_LRA QF_RDL
cvc5	QF_LRA QF_RDL
mc2	QF_LRA QF_RDL
veriT	QF_LRA QF_RDL
2018-MathSAT (incremental)n		QF_LRA
2019-Par4n	QF_LRA QF_RDL
2019-Yices 2.6.2n	QF_LRA QF_RDL
2020-OpenSMTn	QF_LRA QF_RDL			QF_RDL QF_LRA
2020-Yices2-fixed Model Validationn				QF_RDL QF_LRA
2020-Yices2n			QF_LRA QF_RDL
MathSAT5n	QF_LRA QF_RDL	QF_LRA	QF_LRA QF_RDL	QF_RDL QF_LRA
Par4n					QF_LRA QF_RDL	QF_LRA QF_RDL
z3-mvn				QF_RDL QF_LRA
z3n	QF_LRA QF_RDL	QF_LRA	QF_LRA QF_RDL
Total - competing	6	4	4	4	3	1
Total - non-competing	5	3	3	4	1	1
Total	11	7	7	8	4	2

QF_NonLinearIntArith

Solver	Single Query Track	Incremental Track	Unsat Core Track	Cloud Track	Parallel Track
AProVE	QF_NIA QF_NIRA
SMT-RAT	QF_NIA QF_NIRA
SMTInterpol		QF_NIA
Yices2	QF_NIA QF_NIRA		QF_NIA QF_NIRA
Yices2 incremental		QF_NIA
cvc5-gg				QF_NIA QF_NIRA	QF_NIA QF_NIRA
cvc5-inc		QF_NIA
cvc5-uc			QF_NIA QF_NIRA
cvc5	QF_NIA QF_NIRA
2019-Par4n	QF_NIA QF_NIRA
2020-MathSAT5n		QF_NIA
2020-SMT-RATn	QF_NIA QF_NIRA
MathSAT5n	QF_NIA QF_NIRA	QF_NIA	QF_NIA QF_NIRA
Par4n				QF_NIA QF_NIRA	QF_NIA QF_NIRA
cvc5-inc - fixedn		QF_NIA
cvc5-uc - fixedn			QF_NIA QF_NIRA
cvc5 - fixedn	QF_NIA QF_NIRA
z3n	QF_NIA QF_NIRA	QF_NIA	QF_NIA QF_NIRA
Total - competing	4	3	2	1	1
Total - non-competing	5	4	3	1	1
Total	9	7	5	2	2

QF_NonLinearRealArith

Solver	Single Query Track	Unsat Core Track	Cloud Track	Parallel Track
SMT-RAT-MCSAT	QF_NRA
Yices2	QF_NRA	QF_NRA
cvc5-gg			QF_NRA	QF_NRA
cvc5-uc		QF_NRA
cvc5	QF_NRA
veriT+raSAT+Redlog	QF_NRA
2019-Par4n	QF_NRA
MathSAT5n	QF_NRA	QF_NRA
Par4n			QF_NRA	QF_NRA
z3n	QF_NRA	QF_NRA
Total - competing	4	2	1	1
Total - non-competing	3	2	1	1
Total	7	4	2	2

QF_Strings

Solver	Single Query Track	Unsat Core Track	Cloud Track	Parallel Track
Z3str4	QF_S QF_SLIA QF_SNIA
cvc5-gg			QF_S QF_SLIA QF_SNIA	QF_S QF_SLIA QF_SNIA
cvc5-uc		QF_S QF_SLIA QF_SNIA
cvc5	QF_S QF_SLIA QF_SNIA
2020-CVC4n	QF_S QF_SLIA QF_SNIA
Z3str4 - fixedn	QF_S QF_SLIA QF_SNIA
cvc5-uc - fixedn		QF_S QF_SLIA QF_SNIA
cvc5 - fixedn	QF_S QF_SLIA QF_SNIA
z3n	QF_S QF_SLIA QF_SNIA
Total - competing	2	1	1	1
Total - non-competing	4	1	0	0
Total	6	2	1	1