Participants

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

Solver	Single Query Track	Incremental Track	Unsat Core Track	Model Validation Track	Proof Exhibition Track	Cloud Track	Parallel Track	Preliminary Solver ID	Final Solver ID	Seed	System Description
Bitwuzla	X	X	X	X				44483	44756	42	Bitwuzla at the SMT-COMP 2023
COLIBRI	X							44384	44384	413	COLIBRI: SMT solving with CP
OSTRICH	X							44420	44767	67223	OSTRICH Version 1.3
OpenSMT	X	X		X				44686	44750	9471002	The OpenSMT Solver in SMT-COMP 2023
Q3B	X							39062	44707	2353490582350	Q3B in SMT Competition 2023
SMT-RAT-MCSAT	X			X				44411	44765	48738	SMT-RAT 23.05
SMTInterpol	X	X	X	X	X			44719	44759	3021856368	SMTInterpol with resolution proofs
STP	X	X		X				41385	41385	16	STP 2023
UltimateEliminator+MathSAT	X	X	X					44489	44761	0	Ultimate Eliminator at SMT-COMP 2023
UltimateIntBlastingWrapper+SMTInterpol	X							44525	44760	4294967296	Ultimate IntBlastingWrapper
Vampire	X		X		X	X	X	44484	44484	6586	Vampire 4.8-SMT System Description
Yaga	X			X				44678	44678	3621199	The Yaga SMT Solver in SMT-COMP 2023
Yices2	X	X	X	X				44479 44480(inc) 44481(mv)	44479 44751(inc) 44755(mv)	0	Yices 2 in SMT-COMP 2023
YicesQS	X							39111	39111	0	YicesQS 2023, an extension of Yices for quantified satisfiability
Z3++	X			X				44702(sq) 44703(mv)	44702 44703(mv)	1	Z3++ at SMT-COMP 2023
Z3-Noodler	X							44407	44716	6590	Z3-Noodler, System description for SMT-comp 2023
Z3-Owl	X						X	44471	44715	8	Z3-Owl at SMT-COMP 2023
cvc5-NRA-LS	X			X				44469	44741 44742(mv)	99	NRA-LS at the SMT Competition 2023
cvc5-lfsc					X			44515	44736	52240	cvc5 at the SMT Competition 2023
cvc5	X	X	X	X	X	X	X	44516 44517(inc)	44737 44738(inc)	1965	cvc5 at the SMT Competition 2023
iProver	X						X	44524	44768	191937	iProver v3.8 (SMT-COMP-2023)
ismt				X				44672	44672	20230512	ISMT for SMT-COMP 2023
yices-ismt	X							44713	44713		Yices-ISMT for SMT-COMP 2023
z3-alpha	X							44485	44764	33	Z3-alpha: a reinforcement learning guided SMT solver
2018-MathSAT-incrementaln		X							19993
2019-Par4n	X							23391	23672		Par4
2019-Z3n		X						23470	23470
2020-Bitwuzlan				X				28351	28818		Bitwuzla 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-Yices2n			X					28343	28820		Yices 2 in SMT-COMP 2020
2020-z3n		X						28814	28814
2021-MathSAT5n		X							33739
2021-Yices2n	X							33007	33403		Yices 2 at SMTCOMP2021
2021-Yices2 incrementaln		X						33009	33404		Yices 2 at SMTCOMP2021
2021-Yices2 model-validationn				X				33008	33405		Yices 2 at SMTCOMP2021
2021-cvc5-incn		X						33070	33449		cvc5 at the SMT Competition 2021
2021-cvc5-ucn			X					33074	33448		cvc5 at the SMT Competition 2021
2021-z3n	X	X							33741
2022-Bitwuzlan	X	X	X	X				36798	39101		Bitwuzla at the SMT-COMP 2022
2022-MathSATn			X						41381
2022-OpenSMTn				X				39040	39040		OpenSMT in SMT-COMP 2022
2022-STP-fixedn	X								41385
2022-UltimateEliminator+MathSATn		X						36966	39121		UltimateEliminator at SMT-COMP 2022
2022-Vampiren			X			X	X	36957	39081		Vampire 4.7 for SMT-COMP 22
2022-Yices2n	X	X	X	X				33403 33404(inc) 33405(mv)	33403 33404(inc) 33405(mv)		Yices 2 in SMT-COMP 2022
2022-Z3++-fixedn	X								41324
2022-Z3++n				X				38965	38965		Z3++ at SMT-COMP 2022
2022-cvc5n	X		X					36875(sq) 36870(inc) 36872(mv) 39025(pe) 36869(uc)	39117 39114(inc)		cvc5 at the SMT Competition 2022
2022-smtinterpoln				X				39066	39093		SMTInterpol with resolution proofs
2022-z3-4.8.17n	X	X	X						41383
Bitwuzla Fixedn	X		X	X					44959		Bitwuzla at the SMT-COMP 2023
OSTRICH Fixedn	X								44976		OSTRICH Version 1.3
Q3B-pBDDn								36885	-	78549	Q3B-pBDD in SMT Competition 2023
Yices2 Fixedn		X							44947(inc)		Yices 2 in SMT-COMP 2023
Z3-Noodler Fixedn	X								44984		Z3-Noodler, System description for SMT-comp 2023
Z3-Owl Fixedn	X						X		44715		Z3-Owl at SMT-COMP 2023
iProver Fixedn	X						X		44935		iProver v3.8 (SMT-COMP-2023)
Total - competing	22	7	6	11	4	2	4
Total - non-competing	15	12	10	8	0	1	3
Total	37	19	16	19	4	3	7			756654015 (mod 230)

n Non-competing.

The opening value of the NYSE Composite Index on 2023-05-30 was 15078.69, resulting in a competition seed of 756654015 + 1507869 = 758161884.

Divisions

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

Arith

Solver	Single Query Track	Incremental Track	Unsat Core Track	Proof Exhibition Track	Cloud Track	Parallel Track
SMTInterpol	LIA LRA NIA NRA	LIA LRA	LIA LRA NIA NRA	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	LIA LRA NIA NRA
YicesQS	LIA LRA NIA NRA
cvc5-lfsc				LIA LRA NIA NRA
cvc5	LIA LRA NIA NRA	LIA LRA	LIA LRA NIA NRA	LIA LRA NIA NRA	LIA LRA NIA NRA	LIA LRA NIA NRA
iProver	LIA LRA NIA NRA					LIA LRA NIA NRA
2021-cvc5-incn		LIA LRA
2021-z3n	LIA LRA NIA NRA
2022-Vampiren					LIA LRA NIA NRA	LIA LRA NIA NRA
2022-cvc5n			LIA LRA NIA NRA
iProver Fixedn	LIA LRA NIA NRA					LIA LRA NIA NRA
Total - competing	6	3	4	4	2	3
Total - non-competing	2	1	1	0	1	2
Total	8	4	5	4	3	5

Bitvec

Solver	Single Query Track	Incremental Track	Unsat Core Track	Proof Exhibition Track	Cloud Track	Parallel Track
Bitwuzla	BV	BV	BV
Q3B	BV
UltimateEliminator+MathSAT	BV	BV	BV
UltimateIntBlastingWrapper+SMTInterpol	BV
YicesQS	BV
cvc5-lfsc				BV
cvc5	BV	BV	BV	BV	BV	BV
2019-Par4n	BV
2019-Z3n		BV
2020-CVC4-ucn			BV
Bitwuzla Fixedn	BV		BV
Total - competing	6	3	3	2	1	1
Total - non-competing	2	1	2	0	0	0
Total	8	4	5	2	1	1

Equality

Solver	Single Query Track	Incremental Track	Unsat Core Track	Proof Exhibition Track	Cloud Track	Parallel Track
SMTInterpol	UF UFDT	UF	UF UFDT	UF UFDT
UltimateEliminator+MathSAT	UF UFDT	UF	UF UFDT
Vampire	UF UFDT		UF UFDT	UF UFDT	UF UFDT	UF UFDT
Yices2	UF UFDT	UF	UF UFDT
cvc5-lfsc				UF UFDT
cvc5	UF UFDT	UF	UF UFDT	UF UFDT	UF UFDT	UF UFDT
iProver	UF UFDT					UF UFDT
2020-CVC4-ucn			UF UFDT
2020-z3n		UF
2022-Vampiren			UF UFDT		UF UFDT	UF UFDT
2022-cvc5n	UF UFDT
Yices2 Fixedn		UF
iProver Fixedn	UF UFDT					UF UFDT
Total - competing	6	4	5	4	2	3
Total - non-competing	2	2	2	0	1	2
Total	8	6	7	4	3	5

Equality+LinearArith

Solver	Single Query Track	Incremental Track	Unsat Core Track	Proof Exhibition Track	Cloud Track	Parallel Track
SMTInterpol	ALIA AUFDTLIA AUFDTLIRA AUFLIA AUFLIRA UFDTLIA UFDTLIRA UFIDL UFLIA UFLRA	ALIA UFLRA	ALIA AUFDTLIA AUFDTLIRA AUFLIA AUFLIRA UFDTLIA UFDTLIRA UFIDL UFLIA 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	ALIA AUFDTLIA AUFDTLIRA AUFLIA AUFLIRA UFDTLIA UFDTLIRA UFIDL UFLIA UFLRA
cvc5-lfsc				ALIA AUFDTLIA AUFDTLIRA AUFLIA AUFLIRA UFDTLIA UFDTLIRA UFIDL UFLIA UFLRA
cvc5	ALIA AUFDTLIA AUFDTLIRA AUFLIA AUFLIRA UFDTLIA UFDTLIRA UFIDL UFLIA UFLRA	ALIA 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	ALIA AUFDTLIA AUFDTLIRA AUFLIA AUFLIRA UFDTLIA UFDTLIRA UFIDL UFLIA UFLRA
iProver	ALIA AUFDTLIA AUFDTLIRA AUFLIA AUFLIRA UFDTLIA UFDTLIRA UFIDL UFLIA UFLRA					ALIA AUFDTLIA AUFDTLIRA AUFLIA AUFLIRA UFDTLIA UFDTLIRA UFIDL UFLIA UFLRA
2021-cvc5-ucn			ALIA AUFDTLIA AUFDTLIRA AUFLIA AUFLIRA UFDTLIA UFDTLIRA UFIDL UFLIA UFLRA
2021-z3n		ALIA UFLRA
2022-Vampiren					ALIA AUFDTLIA AUFDTLIRA AUFLIA AUFLIRA UFDTLIA UFDTLIRA UFIDL UFLIA UFLRA	ALIA AUFDTLIA AUFDTLIRA AUFLIA AUFLIRA UFDTLIA UFDTLIRA UFIDL UFLIA UFLRA
2022-cvc5n	ALIA AUFDTLIA AUFDTLIRA AUFLIA AUFLIRA UFDTLIA UFDTLIRA UFIDL UFLIA UFLRA
iProver Fixedn	ALIA AUFDTLIA AUFDTLIRA AUFLIA AUFLIRA UFDTLIA UFDTLIRA UFIDL UFLIA UFLRA					ALIA AUFDTLIA AUFDTLIRA AUFLIA AUFLIRA UFDTLIA UFDTLIRA UFIDL UFLIA UFLRA
Total - competing	5	3	4	4	2	3
Total - non-competing	2	1	1	0	1	2
Total	7	4	5	4	3	5

Equality+MachineArith

Solver	Single Query Track	Incremental Track	Unsat Core Track	Proof Exhibition Track	Cloud Track	Parallel Track
Bitwuzla	ABV ABVFP ABVFPLRA AUFBV AUFBVDTLIA AUFBVDTNIA AUFBVDTNIRA AUFBVFP AUFFPDTNIRA UFBV UFBVDT UFBVFP UFBVLIA UFFPDTNIRA	ABVFPLRA	ABV ABVFP ABVFPLRA AUFBV AUFBVDTLIA AUFBVDTNIA AUFBVDTNIRA AUFBVFP AUFFPDTNIRA UFBV UFBVDT UFBVFP UFBVLIA UFFPDTNIRA
UltimateEliminator+MathSAT	ABV ABVFP ABVFPLRA AUFBV AUFBVDTLIA AUFBVDTNIA AUFBVDTNIRA AUFBVFP AUFFPDTNIRA UFBV UFBVDT UFBVFP UFBVLIA UFFPDTNIRA	ABVFPLRA	ABV ABVFP ABVFPLRA AUFBV AUFBVDTLIA AUFBVDTNIA AUFBVDTNIRA AUFBVFP AUFFPDTNIRA UFBV UFBVDT UFBVFP UFBVLIA UFFPDTNIRA
UltimateIntBlastingWrapper+SMTInterpol	ABV ABVFP ABVFPLRA AUFBV AUFBVDTLIA AUFBVDTNIA AUFBVDTNIRA AUFBVFP AUFFPDTNIRA UFBV UFBVDT UFBVFP UFBVLIA UFFPDTNIRA
cvc5-lfsc				ABV ABVFP ABVFPLRA AUFBV AUFBVDTLIA AUFBVDTNIA AUFBVDTNIRA AUFBVFP AUFFPDTNIRA UFBV UFBVDT UFBVFP UFBVLIA UFFPDTNIRA
cvc5	ABV ABVFP ABVFPLRA AUFBV AUFBVDTLIA AUFBVDTNIA AUFBVDTNIRA AUFBVFP AUFFPDTNIRA UFBV UFBVDT UFBVFP UFBVLIA UFFPDTNIRA	ABVFPLRA	ABV ABVFP ABVFPLRA AUFBV AUFBVDTLIA AUFBVDTNIA AUFBVDTNIRA AUFBVFP AUFFPDTNIRA UFBV UFBVDT UFBVFP UFBVLIA UFFPDTNIRA	ABV ABVFP ABVFPLRA AUFBV AUFBVDTLIA AUFBVDTNIA AUFBVDTNIRA AUFBVFP AUFFPDTNIRA UFBV UFBVDT UFBVFP UFBVLIA UFFPDTNIRA	ABV ABVFP ABVFPLRA AUFBV AUFBVDTLIA AUFBVDTNIA AUFBVDTNIRA AUFBVFP AUFFPDTNIRA UFBV UFBVDT UFBVFP UFBVLIA UFFPDTNIRA	ABV ABVFP ABVFPLRA AUFBV AUFBVDTLIA AUFBVDTNIA AUFBVDTNIRA AUFBVFP AUFFPDTNIRA UFBV UFBVDT UFBVFP UFBVLIA UFFPDTNIRA
2022-UltimateEliminator+MathSATn		ABVFPLRA
2022-z3-4.8.17n	ABV ABVFP ABVFPLRA AUFBV AUFBVDTLIA AUFBVDTNIA AUFBVDTNIRA AUFBVFP AUFFPDTNIRA UFBV UFBVDT UFBVFP UFBVLIA UFFPDTNIRA		ABV ABVFP ABVFPLRA AUFBV AUFBVDTLIA AUFBVDTNIA AUFBVDTNIRA AUFBVFP AUFFPDTNIRA UFBV UFBVDT UFBVFP UFBVLIA UFFPDTNIRA
Bitwuzla Fixedn	ABV ABVFP ABVFPLRA AUFBV AUFBVDTLIA AUFBVDTNIA AUFBVDTNIRA AUFBVFP AUFFPDTNIRA UFBV UFBVDT UFBVFP UFBVLIA UFFPDTNIRA		ABV ABVFP ABVFPLRA AUFBV AUFBVDTLIA AUFBVDTNIA AUFBVDTNIRA AUFBVFP AUFFPDTNIRA UFBV UFBVDT UFBVFP UFBVLIA UFFPDTNIRA
Total - competing	4	3	3	2	1	1
Total - non-competing	2	1	2	0	0	0
Total	6	4	5	2	1	1

Equality+NonLinearArith

Solver	Single Query Track	Incremental Track	Unsat Core Track	Proof Exhibition Track	Cloud Track	Parallel Track
SMTInterpol		ANIA AUFNIRA UFDTNIA UFNIA UFNRA
UltimateEliminator+MathSAT	ANIA AUFDTNIRA AUFNIA AUFNIRA UFDTNIA UFDTNIRA UFNIA	ANIA AUFNIRA UFDTNIA UFNIA UFNRA	ANIA AUFDTNIRA AUFNIA AUFNIRA UFDTNIA UFDTNIRA UFNIA
Vampire	ANIA AUFDTNIRA AUFNIA AUFNIRA UFDTNIA UFDTNIRA UFNIA		ANIA AUFDTNIRA AUFNIA AUFNIRA UFDTNIA UFDTNIRA UFNIA	ANIA AUFDTNIRA AUFNIA AUFNIRA UFDTNIA UFDTNIRA UFNIA	ANIA AUFDTNIRA AUFNIA AUFNIRA UFDTNIA UFDTNIRA UFNIA	ANIA AUFDTNIRA AUFNIA AUFNIRA UFDTNIA UFDTNIRA UFNIA
cvc5-lfsc				ANIA AUFDTNIRA AUFNIA AUFNIRA UFDTNIA UFDTNIRA UFNIA
cvc5	ANIA AUFDTNIRA AUFNIA AUFNIRA UFDTNIA UFDTNIRA UFNIA	ANIA AUFNIRA UFDTNIA UFNIA UFNRA	ANIA AUFDTNIRA AUFNIA AUFNIRA UFDTNIA UFDTNIRA UFNIA	ANIA AUFDTNIRA AUFNIA AUFNIRA UFDTNIA UFDTNIRA UFNIA	ANIA AUFDTNIRA AUFNIA AUFNIRA UFDTNIA UFDTNIRA UFNIA	ANIA AUFDTNIRA AUFNIA AUFNIRA UFDTNIA UFDTNIRA UFNIA
iProver	ANIA AUFDTNIRA AUFNIA AUFNIRA UFDTNIA UFDTNIRA UFNIA					ANIA AUFDTNIRA AUFNIA AUFNIRA UFDTNIA UFDTNIRA UFNIA
2020-CVC4-ucn			ANIA AUFDTNIRA AUFNIA AUFNIRA UFDTNIA UFDTNIRA UFNIA
2022-Vampiren					ANIA AUFDTNIRA AUFNIA AUFNIRA UFDTNIA UFDTNIRA UFNIA	ANIA AUFDTNIRA AUFNIA AUFNIRA UFDTNIA UFDTNIRA UFNIA
2022-cvc5n	ANIA AUFDTNIRA AUFNIA AUFNIRA UFDTNIA UFDTNIRA UFNIA
2022-z3-4.8.17n		ANIA AUFNIRA UFDTNIA UFNIA UFNRA
iProver Fixedn	ANIA AUFDTNIRA AUFNIA AUFNIRA UFDTNIA UFDTNIRA UFNIA					ANIA AUFDTNIRA AUFNIA AUFNIRA UFDTNIA UFDTNIRA UFNIA
Total - competing	4	3	3	3	2	3
Total - non-competing	2	1	1	0	1	2
Total	6	4	4	3	3	5

FPArith

Solver	Single Query Track	Incremental Track	Unsat Core Track	Proof Exhibition Track	Cloud Track	Parallel Track
Bitwuzla	BVFP BVFPLRA FP FPLRA	BVFP BVFPLRA	BVFP BVFPLRA FP FPLRA
UltimateEliminator+MathSAT	BVFP BVFPLRA FP FPLRA	BVFP BVFPLRA	BVFP BVFPLRA FP FPLRA
cvc5-lfsc				BVFP BVFPLRA FP FPLRA
cvc5	BVFP BVFPLRA FP FPLRA	BVFP BVFPLRA	BVFP BVFPLRA FP FPLRA	BVFP BVFPLRA FP FPLRA	BVFP BVFPLRA FP FPLRA	BVFP BVFPLRA FP FPLRA
2020-CVC4-ucn			BVFP BVFPLRA FP FPLRA
2022-Bitwuzlan	BVFP BVFPLRA FP FPLRA	BVFP BVFPLRA
Bitwuzla Fixedn	BVFP BVFPLRA FP FPLRA		BVFP BVFPLRA FP FPLRA
Total - competing	3	3	3	2	1	1
Total - non-competing	2	1	2	0	0	0
Total	5	4	5	2	1	1

QF_ADT+BitVec

Solver	Model Validation Track
Bitwuzla	QF_ABV QF_AUFBV QF_UFBVDT
UltimateIntBlastingWrapper+SMTInterpol
Yices2	QF_ABV QF_AUFBV QF_UFBVDT
Z3-Owl
cvc5-lfsc
cvc5	QF_ABV QF_AUFBV QF_UFBVDT
2022-Bitwuzlan
2022-Yices2n
Bitwuzla Fixedn	QF_ABV QF_AUFBV QF_UFBVDT
Yices2 Fixedn
Z3-Owl Fixedn
Total - competing	3
Total - non-competing	1
Total	4

QF_ADT+LinArith

Solver	Model Validation Track
OpenSMT
SMTInterpol	QF_ALIA QF_AUFLIA QF_AX QF_UFDTLIA QF_UFDTLIRA
Yices2	QF_ALIA QF_AUFLIA QF_AX QF_UFDTLIA QF_UFDTLIRA
cvc5-lfsc
cvc5	QF_ALIA QF_AUFLIA QF_AX QF_UFDTLIA QF_UFDTLIRA
2020-z3n
2022-Yices2n
2022-z3-4.8.17n
Yices2 Fixedn
Total - competing	3
Total - non-competing	0
Total	3

QF_Bitvec

Solver	Single Query Track	Incremental Track	Unsat Core Track	Model Validation Track	Proof Exhibition Track	Cloud Track	Parallel Track
Bitwuzla	QF_BV	QF_BV	QF_BV	QF_BV
STP	QF_BV	QF_BV		QF_BV
UltimateIntBlastingWrapper+SMTInterpol	QF_BV
Yices2	QF_BV	QF_BV	QF_BV	QF_BV
Z3-Owl	QF_BV						QF_BV
cvc5-lfsc					QF_BV
cvc5	QF_BV	QF_BV	QF_BV	QF_BV	QF_BV	QF_BV	QF_BV
2020-Bitwuzlan				QF_BV
2022-Bitwuzlan			QF_BV
2022-STP-fixedn	QF_BV
2022-Yices2n		QF_BV
Bitwuzla Fixedn	QF_BV		QF_BV	QF_BV
Yices2 Fixedn		QF_BV
Z3-Owl Fixedn	QF_BV						QF_BV
Total - competing	6	4	3	4	2	1	2
Total - non-competing	3	2	2	2	0	0	1
Total	9	6	5	6	2	1	3

QF_Datatypes

Solver	Single Query Track	Unsat Core Track	Model Validation Track	Proof Exhibition Track	Cloud Track	Parallel Track
SMTInterpol	QF_DT QF_UFDT	QF_DT QF_UFDT	QF_DT QF_UFDT	QF_DT QF_UFDT
cvc5-lfsc				QF_DT QF_UFDT
cvc5	QF_DT QF_UFDT	QF_DT QF_UFDT	QF_DT QF_UFDT	QF_DT QF_UFDT	QF_DT QF_UFDT	QF_DT QF_UFDT
2022-z3-4.8.17n	QF_DT QF_UFDT	QF_DT QF_UFDT
Total - competing	2	2	2	3	1	1
Total - non-competing	1	1	0	0	0	0
Total	3	3	2	3	1	1

QF_Equality

Solver	Single Query Track	Incremental Track	Unsat Core Track	Model Validation Track	Proof Exhibition Track	Cloud Track	Parallel Track
OpenSMT	QF_AX QF_UF	QF_UF		QF_UF
SMTInterpol	QF_AX QF_UF	QF_UF	QF_AX QF_UF	QF_UF	QF_AX QF_UF
Yices2	QF_AX QF_UF	QF_UF	QF_AX QF_UF	QF_UF
cvc5-lfsc					QF_AX QF_UF
cvc5	QF_AX QF_UF	QF_UF	QF_AX QF_UF	QF_UF	QF_AX QF_UF	QF_AX QF_UF	QF_AX QF_UF
2021-Yices2 model-validationn				QF_UF
2022-Yices2n	QF_AX QF_UF	QF_UF		QF_UF
2022-z3-4.8.17n			QF_AX QF_UF
Yices2 Fixedn		QF_UF
Total - competing	4	4	3	4	3	1	1
Total - non-competing	1	2	1	2	0	0	0
Total	5	6	4	6	3	1	1

QF_Equality+Bitvec

Solver	Single Query Track	Incremental Track	Unsat Core Track	Model Validation Track	Proof Exhibition Track	Cloud Track	Parallel Track
Bitwuzla	QF_ABV QF_AUFBV QF_UFBV QF_UFBVDT	QF_ABV QF_AUFBV QF_UFBV	QF_ABV QF_AUFBV QF_UFBV QF_UFBVDT	QF_UFBV
UltimateIntBlastingWrapper+SMTInterpol	QF_ABV QF_AUFBV QF_UFBV QF_UFBVDT
Yices2	QF_ABV QF_AUFBV QF_UFBV QF_UFBVDT	QF_ABV QF_AUFBV QF_UFBV	QF_ABV QF_AUFBV QF_UFBV QF_UFBVDT	QF_UFBV
Z3-Owl	QF_ABV QF_AUFBV QF_UFBV QF_UFBVDT
cvc5-lfsc					QF_ABV QF_AUFBV QF_UFBV QF_UFBVDT
cvc5	QF_ABV QF_AUFBV QF_UFBV QF_UFBVDT	QF_ABV QF_AUFBV QF_UFBV	QF_ABV QF_AUFBV QF_UFBV QF_UFBVDT	QF_UFBV	QF_ABV QF_AUFBV QF_UFBV QF_UFBVDT	QF_ABV QF_AUFBV QF_UFBV QF_UFBVDT	QF_ABV QF_AUFBV QF_UFBV QF_UFBVDT
2022-Bitwuzlan	QF_ABV QF_AUFBV QF_UFBV QF_UFBVDT		QF_ABV QF_AUFBV QF_UFBV QF_UFBVDT	QF_UFBV
2022-Yices2n		QF_ABV QF_AUFBV QF_UFBV
Bitwuzla Fixedn	QF_ABV QF_AUFBV QF_UFBV QF_UFBVDT		QF_ABV QF_AUFBV QF_UFBV QF_UFBVDT	QF_UFBV
Yices2 Fixedn		QF_ABV QF_AUFBV QF_UFBV
Z3-Owl Fixedn	QF_ABV QF_AUFBV QF_UFBV QF_UFBVDT
Total - competing	5	3	3	3	2	1	1
Total - non-competing	3	2	2	2	0	0	0
Total	8	5	5	5	2	1	1

QF_Equality+Bitvec+Arith

Solver	Incremental Track
Yices2	QF_AUFBVLIA QF_AUFBVNIA QF_UFBVLIA
cvc5	QF_AUFBVLIA QF_AUFBVNIA QF_UFBVLIA
Yices2 Fixedn	QF_AUFBVLIA QF_AUFBVNIA QF_UFBVLIA
Total - competing	2
Total - non-competing	1
Total	3

QF_Equality+LinearArith

Solver	Single Query Track	Incremental Track	Unsat Core Track	Model Validation Track	Proof Exhibition Track	Cloud Track	Parallel Track
OpenSMT	QF_ALIA QF_AUFLIA QF_UFDTLIA QF_UFDTLIRA QF_UFIDL QF_UFLIA QF_UFLRA	QF_ALIA QF_AUFLIA QF_UFLIA QF_UFLRA		QF_UFIDL QF_UFLIA QF_UFLRA
SMTInterpol	QF_ALIA QF_AUFLIA QF_UFDTLIA QF_UFDTLIRA QF_UFIDL QF_UFLIA QF_UFLRA	QF_ALIA QF_AUFLIA QF_UFLIA QF_UFLRA	QF_ALIA QF_AUFLIA QF_UFDTLIA QF_UFDTLIRA QF_UFIDL QF_UFLIA QF_UFLRA	QF_UFIDL QF_UFLIA QF_UFLRA	QF_ALIA QF_AUFLIA QF_UFDTLIA QF_UFDTLIRA QF_UFIDL QF_UFLIA QF_UFLRA
Yices2	QF_ALIA QF_AUFLIA QF_UFDTLIA QF_UFDTLIRA QF_UFIDL QF_UFLIA QF_UFLRA	QF_ALIA QF_AUFLIA QF_UFLIA QF_UFLRA	QF_ALIA QF_AUFLIA QF_UFDTLIA QF_UFDTLIRA QF_UFIDL QF_UFLIA QF_UFLRA	QF_UFIDL QF_UFLIA QF_UFLRA
cvc5-lfsc					QF_ALIA QF_AUFLIA QF_UFDTLIA QF_UFDTLIRA QF_UFIDL QF_UFLIA QF_UFLRA
cvc5	QF_ALIA QF_AUFLIA QF_UFDTLIA QF_UFDTLIRA QF_UFIDL QF_UFLIA QF_UFLRA	QF_ALIA QF_AUFLIA QF_UFLIA QF_UFLRA	QF_ALIA QF_AUFLIA QF_UFDTLIA QF_UFDTLIRA QF_UFIDL QF_UFLIA QF_UFLRA	QF_UFIDL QF_UFLIA QF_UFLRA	QF_ALIA QF_AUFLIA QF_UFDTLIA QF_UFDTLIRA QF_UFIDL QF_UFLIA QF_UFLRA	QF_ALIA QF_AUFLIA QF_UFDTLIA QF_UFDTLIRA QF_UFIDL QF_UFLIA QF_UFLRA	QF_ALIA QF_AUFLIA QF_UFDTLIA QF_UFDTLIRA QF_UFIDL QF_UFLIA QF_UFLRA
2020-z3n		QF_ALIA QF_AUFLIA QF_UFLIA QF_UFLRA
2022-Yices2n			QF_ALIA QF_AUFLIA QF_UFDTLIA QF_UFDTLIRA QF_UFIDL QF_UFLIA QF_UFLRA
2022-smtinterpoln				QF_UFIDL QF_UFLIA QF_UFLRA
2022-z3-4.8.17n	QF_ALIA QF_AUFLIA QF_UFDTLIA QF_UFDTLIRA QF_UFIDL QF_UFLIA QF_UFLRA
Yices2 Fixedn		QF_ALIA QF_AUFLIA QF_UFLIA QF_UFLRA
Total - competing	4	4	3	4	3	1	1
Total - non-competing	1	2	1	1	0	0	0
Total	5	6	4	5	3	1	1

QF_Equality+NonLinearArith

Solver	Single Query Track	Incremental Track	Unsat Core Track	Model Validation Track	Proof Exhibition Track	Cloud Track	Parallel Track
SMTInterpol	QF_ANIA QF_AUFNIA QF_UFDTNIA QF_UFNIA QF_UFNRA	QF_ANIA QF_UFNIA QF_UFNRA	QF_ANIA QF_AUFNIA QF_UFDTNIA QF_UFNIA QF_UFNRA		QF_ANIA QF_AUFNIA QF_UFDTNIA QF_UFNIA QF_UFNRA
Yices2	QF_ANIA QF_AUFNIA QF_UFDTNIA QF_UFNIA QF_UFNRA	QF_ANIA QF_UFNIA QF_UFNRA		QF_ANIA QF_AUFNIA QF_UFDTNIA QF_UFNIA QF_UFNRA
cvc5-lfsc					QF_ANIA QF_AUFNIA QF_UFDTNIA QF_UFNIA QF_UFNRA
cvc5	QF_ANIA QF_AUFNIA QF_UFDTNIA QF_UFNIA QF_UFNRA	QF_ANIA QF_UFNIA QF_UFNRA	QF_ANIA QF_AUFNIA QF_UFDTNIA QF_UFNIA QF_UFNRA	QF_ANIA QF_AUFNIA QF_UFDTNIA QF_UFNIA QF_UFNRA	QF_ANIA QF_AUFNIA QF_UFDTNIA QF_UFNIA QF_UFNRA	QF_ANIA QF_AUFNIA QF_UFDTNIA QF_UFNIA QF_UFNRA	QF_ANIA QF_AUFNIA QF_UFDTNIA QF_UFNIA QF_UFNRA
2020-CVC4n	QF_ANIA QF_AUFNIA QF_UFDTNIA QF_UFNIA QF_UFNRA
2021-cvc5-ucn			QF_ANIA QF_AUFNIA QF_UFDTNIA QF_UFNIA QF_UFNRA
2022-z3-4.8.17n		QF_ANIA QF_UFNIA QF_UFNRA
Yices2 Fixedn		QF_ANIA QF_UFNIA QF_UFNRA
Total - competing	3	3	2	2	3	1	1
Total - non-competing	1	2	1	0	0	0	0
Total	4	5	3	2	3	1	1

QF_FPArith

Solver	Single Query Track	Incremental Track	Unsat Core Track	Model Validation Track	Proof Exhibition Track	Cloud Track	Parallel Track
Bitwuzla	QF_ABVFP QF_ABVFPLRA QF_AUFBVFP QF_BVFP QF_BVFPLRA QF_FP QF_FPLRA QF_UFFP QF_UFFPDTNIRA	QF_ABVFP QF_ABVFPLRA QF_BVFP QF_BVFPLRA QF_FP QF_UFFP	QF_ABVFP QF_ABVFPLRA QF_AUFBVFP QF_BVFP QF_BVFPLRA QF_FP QF_FPLRA QF_UFFP QF_UFFPDTNIRA	QF_ABVFP QF_ABVFPLRA QF_AUFBVFP QF_BVFP QF_BVFPLRA QF_FP QF_FPLRA QF_UFFP QF_UFFPDTNIRA
COLIBRI	QF_ABVFP QF_ABVFPLRA QF_AUFBVFP QF_BVFP QF_BVFPLRA QF_FP QF_FPLRA QF_UFFP QF_UFFPDTNIRA
Z3-Owl	QF_ABVFP QF_ABVFPLRA QF_AUFBVFP QF_BVFP QF_BVFPLRA QF_FP QF_FPLRA QF_UFFP QF_UFFPDTNIRA
cvc5-lfsc					QF_ABVFP QF_ABVFPLRA QF_AUFBVFP QF_BVFP QF_BVFPLRA QF_FP QF_FPLRA QF_UFFP QF_UFFPDTNIRA
cvc5	QF_ABVFP QF_ABVFPLRA QF_AUFBVFP QF_BVFP QF_BVFPLRA QF_FP QF_FPLRA QF_UFFP QF_UFFPDTNIRA	QF_ABVFP QF_ABVFPLRA QF_BVFP QF_BVFPLRA QF_FP QF_UFFP	QF_ABVFP QF_ABVFPLRA QF_AUFBVFP QF_BVFP QF_BVFPLRA QF_FP QF_FPLRA QF_UFFP QF_UFFPDTNIRA	QF_ABVFP QF_ABVFPLRA QF_AUFBVFP QF_BVFP QF_BVFPLRA QF_FP QF_FPLRA QF_UFFP QF_UFFPDTNIRA	QF_ABVFP QF_ABVFPLRA QF_AUFBVFP QF_BVFP QF_BVFPLRA QF_FP QF_FPLRA QF_UFFP QF_UFFPDTNIRA	QF_ABVFP QF_ABVFPLRA QF_AUFBVFP QF_BVFP QF_BVFPLRA QF_FP QF_FPLRA QF_UFFP QF_UFFPDTNIRA	QF_ABVFP QF_ABVFPLRA QF_AUFBVFP QF_BVFP QF_BVFPLRA QF_FP QF_FPLRA QF_UFFP QF_UFFPDTNIRA
2022-Bitwuzlan	QF_ABVFP QF_ABVFPLRA QF_AUFBVFP QF_BVFP QF_BVFPLRA QF_FP QF_FPLRA QF_UFFP QF_UFFPDTNIRA	QF_ABVFP QF_ABVFPLRA QF_BVFP QF_BVFPLRA QF_FP QF_UFFP		QF_ABVFP QF_ABVFPLRA QF_AUFBVFP QF_BVFP QF_BVFPLRA QF_FP QF_FPLRA QF_UFFP QF_UFFPDTNIRA
2022-z3-4.8.17n			QF_ABVFP QF_ABVFPLRA QF_AUFBVFP QF_BVFP QF_BVFPLRA QF_FP QF_FPLRA QF_UFFP QF_UFFPDTNIRA
Bitwuzla Fixedn	QF_ABVFP QF_ABVFPLRA QF_AUFBVFP QF_BVFP QF_BVFPLRA QF_FP QF_FPLRA QF_UFFP QF_UFFPDTNIRA		QF_ABVFP QF_ABVFPLRA QF_AUFBVFP QF_BVFP QF_BVFPLRA QF_FP QF_FPLRA QF_UFFP QF_UFFPDTNIRA	QF_ABVFP QF_ABVFPLRA QF_AUFBVFP QF_BVFP QF_BVFPLRA QF_FP QF_FPLRA QF_UFFP QF_UFFPDTNIRA
Z3-Owl Fixedn	QF_ABVFP QF_ABVFPLRA QF_AUFBVFP QF_BVFP QF_BVFPLRA QF_FP QF_FPLRA QF_UFFP QF_UFFPDTNIRA
Total - competing	4	2	2	2	2	1	1
Total - non-competing	3	1	2	2	0	0	0
Total	7	3	4	4	2	1	1

QF_LinearIntArith

Solver	Single Query Track	Incremental Track	Unsat Core Track	Model Validation Track	Proof Exhibition Track	Cloud Track	Parallel Track
OpenSMT	QF_IDL QF_LIA QF_LIRA	QF_LIA		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	QF_IDL QF_LIA QF_LIRA
Yices2	QF_IDL QF_LIA QF_LIRA	QF_LIA	QF_IDL QF_LIA QF_LIRA	QF_IDL QF_LIA QF_LIRA
Z3++	QF_IDL QF_LIA QF_LIRA			QF_IDL QF_LIA QF_LIRA
cvc5-lfsc					QF_IDL QF_LIA QF_LIRA
cvc5	QF_IDL QF_LIA QF_LIRA	QF_LIA	QF_IDL QF_LIA QF_LIRA	QF_IDL QF_LIA QF_LIRA	QF_IDL QF_LIA QF_LIRA	QF_IDL QF_LIA QF_LIRA	QF_IDL QF_LIA QF_LIRA
2019-Par4n	QF_IDL QF_LIA QF_LIRA
2021-Yices2 incrementaln		QF_LIA
2022-MathSATn			QF_IDL QF_LIA QF_LIRA
2022-Z3++n				QF_IDL QF_LIA QF_LIRA
Yices2 Fixedn		QF_LIA
Total - competing	5	4	3	5	3	1	1
Total - non-competing	1	2	1	1	0	0	0
Total	6	6	4	6	3	1	1

QF_LinearRealArith

Solver	Single Query Track	Incremental Track	Unsat Core Track	Model Validation Track	Proof Exhibition Track	Cloud Track	Parallel Track
OpenSMT	QF_LRA QF_RDL	QF_LRA		QF_LRA QF_RDL
SMTInterpol	QF_LRA QF_RDL	QF_LRA	QF_LRA QF_RDL	QF_LRA QF_RDL	QF_LRA QF_RDL
Yaga	QF_LRA QF_RDL			QF_LRA QF_RDL
Yices2	QF_LRA QF_RDL	QF_LRA	QF_LRA QF_RDL	QF_LRA QF_RDL
cvc5-lfsc					QF_LRA QF_RDL
cvc5	QF_LRA QF_RDL	QF_LRA	QF_LRA QF_RDL	QF_LRA QF_RDL	QF_LRA QF_RDL	QF_LRA QF_RDL	QF_LRA QF_RDL
2018-MathSAT-incrementaln		QF_LRA
2020-Yices2n			QF_LRA QF_RDL
2021-Yices2n	QF_LRA QF_RDL
2022-OpenSMTn				QF_LRA QF_RDL
2022-Yices2n	QF_LRA QF_RDL
Yices2 Fixedn		QF_LRA
Total - competing	5	4	3	5	3	1	1
Total - non-competing	2	2	1	1	0	0	0
Total	7	6	4	6	3	1	1

QF_NonLinearIntArith

Solver	Single Query Track	Incremental Track	Unsat Core Track	Model Validation Track	Proof Exhibition Track	Cloud Track	Parallel Track
SMTInterpol		QF_NIA
Yices2	QF_NIA QF_NIRA	QF_NIA		QF_NIA QF_NIRA
Z3++	QF_NIA QF_NIRA			QF_NIA QF_NIRA
cvc5-lfsc					QF_NIA QF_NIRA
cvc5	QF_NIA QF_NIRA	QF_NIA	QF_NIA QF_NIRA	QF_NIA QF_NIRA	QF_NIA QF_NIRA	QF_NIA QF_NIRA	QF_NIA QF_NIRA
ismt				QF_NIA QF_NIRA
yices-ismt	QF_NIA QF_NIRA
z3-alpha	QF_NIA QF_NIRA
2021-MathSAT5n		QF_NIA
2022-Z3++-fixedn	QF_NIA QF_NIRA
Yices2 Fixedn		QF_NIA
Total - competing	5	3	1	4	2	1	1
Total - non-competing	1	2	0	0	0	0	0
Total	6	5	1	4	2	1	1

QF_NonLinearRealArith

Solver	Single Query Track	Unsat Core Track	Model Validation Track	Proof Exhibition Track	Cloud Track	Parallel Track
SMT-RAT-MCSAT	QF_NRA		QF_NRA
Yices2	QF_NRA		QF_NRA
Z3++	QF_NRA		QF_NRA
cvc5-NRA-LS	QF_NRA		QF_NRA
cvc5-lfsc				QF_NRA
cvc5	QF_NRA	QF_NRA	QF_NRA	QF_NRA	QF_NRA	QF_NRA
z3-alpha	QF_NRA
2019-Par4n	QF_NRA
2022-Z3++-fixedn	QF_NRA
Total - competing	6	1	5	2	1	1
Total - non-competing	2	0	0	0	0	0
Total	8	1	5	2	1	1

QF_Strings

Solver	Single Query Track	Unsat Core Track	Proof Exhibition Track	Cloud Track	Parallel Track
OSTRICH	QF_S QF_SLIA QF_SNIA
Z3-Noodler	QF_S QF_SLIA QF_SNIA
cvc5-lfsc			QF_S QF_SLIA QF_SNIA
cvc5	QF_S QF_SLIA QF_SNIA	QF_S QF_SLIA QF_SNIA	QF_S QF_SLIA QF_SNIA	QF_S QF_SLIA QF_SNIA	QF_S QF_SLIA QF_SNIA
z3-alpha	QF_S QF_SLIA QF_SNIA
2022-cvc5n	QF_S QF_SLIA QF_SNIA
OSTRICH Fixedn	QF_S QF_SLIA QF_SNIA
Z3-Noodler Fixedn	QF_S QF_SLIA QF_SNIA
Total - competing	4	1	2	1	1
Total - non-competing	3	0	0	0	0
Total	7	1	2	1	1