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			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
Q3B-pBDDn								36885	-	78549	Q3B-pBDD in SMT Competition 2023
Total - competing	22	7	6	11	4	1	3
Total - non-competing	0	0	0	0	0	0	0
Total	22	7	6	11	4	1	3			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
iProver	LIA LRA NIA NRA					LIA LRA NIA NRA
Total - competing	6	3	4	4	1	2
Total - non-competing	0	0	0	0	0	0
Total	6	3	4	4	1	2

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
Total - competing	6	3	3	2	0	0
Total - non-competing	0	0	0	0	0	0
Total	6	3	3	2	0	0

Equality

Solver	Single Query Track	Incremental Track	Unsat Core Track	Proof Exhibition Track	Cloud Track	Parallel Track
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
iProver	UF UFDT					UF UFDT
Total - competing	5	3	4	3	1	2
Total - non-competing	0	0	0	0	0	0
Total	5	3	4	3	1	2

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
iProver	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	1	2
Total - non-competing	0	0	0	0	0	0
Total	5	3	4	4	1	2

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
Total - competing	4	3	3	2	0	0
Total - non-competing	0	0	0	0	0	0
Total	4	3	3	2	0	0

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
iProver	ANIA AUFDTNIRA AUFNIA AUFNIRA UFDTNIA UFDTNIRA UFNIA					ANIA AUFDTNIRA AUFNIA AUFNIRA UFDTNIA UFDTNIRA UFNIA
Total - competing	4	3	3	3	1	2
Total - non-competing	0	0	0	0	0	0
Total	4	3	3	3	1	2

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
Total - competing	3	3	3	2	0	0
Total - non-competing	0	0	0	0	0	0
Total	3	3	3	2	0	0

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
Total - competing	6	4	3	4	2	0	1
Total - non-competing	0	0	0	0	0	0	0
Total	6	4	3	4	2	0	1

QF_Datatypes

Solver	Single Query Track	Unsat Core Track	Model Validation Track	Proof Exhibition Track	Cloud Track	Parallel Track
cvc5-lfsc				QF_DT QF_UFDT
cvc5	QF_DT QF_UFDT	QF_DT QF_UFDT	QF_DT QF_UFDT	QF_DT QF_UFDT
Total - competing	1	1	1	2	0	0
Total - non-competing	0	0	0	0	0	0
Total	1	1	1	2	0	0

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_AX QF_UF
Yices2	QF_AX QF_UF	QF_UF	QF_AX QF_UF	QF_AX QF_UF
cvc5-lfsc					QF_AX QF_UF
cvc5	QF_AX QF_UF	QF_UF	QF_AX QF_UF	QF_AX QF_UF	QF_AX QF_UF
Total - competing	3	3	2	3	2	0	0
Total - non-competing	0	0	0	0	0	0	0
Total	3	3	2	3	2	0	0

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_ABV QF_AUFBV QF_UFBV QF_UFBVDT
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_ABV QF_AUFBV QF_UFBV QF_UFBVDT
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_ABV QF_AUFBV QF_UFBV QF_UFBVDT	QF_ABV QF_AUFBV QF_UFBV QF_UFBVDT
Total - competing	5	3	3	3	2	0	0
Total - non-competing	0	0	0	0	0	0	0
Total	5	3	3	3	2	0	0

QF_Equality+Bitvec+Arith

Solver	Incremental Track
Yices2	QF_AUFBVLIA QF_AUFBVNIA QF_UFBVLIA
cvc5	QF_AUFBVLIA QF_AUFBVNIA QF_UFBVLIA
Total - competing	2
Total - non-competing	0
Total	2

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_ALIA QF_AUFLIA QF_UFDTLIA QF_UFDTLIRA 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_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
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_ALIA QF_AUFLIA QF_UFDTLIA QF_UFDTLIRA 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_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
Total - competing	4	4	3	4	3	0	0
Total - non-competing	0	0	0	0	0	0	0
Total	4	4	3	4	3	0	0

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
Total - competing	3	3	2	2	3	0	0
Total - non-competing	0	0	0	0	0	0	0
Total	3	3	2	2	3	0	0

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
Total - competing	4	2	2	2	2	0	0
Total - non-competing	0	0	0	0	0	0	0
Total	4	2	2	2	2	0	0

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
Total - competing	5	4	3	5	3	0	0
Total - non-competing	0	0	0	0	0	0	0
Total	5	4	3	5	3	0	0

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
Total - competing	5	4	3	5	3	0	0
Total - non-competing	0	0	0	0	0	0	0
Total	5	4	3	5	3	0	0

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
ismt				QF_NIA QF_NIRA
yices-ismt	QF_NIA QF_NIRA
z3-alpha	QF_NIA QF_NIRA
Total - competing	5	3	1	4	2	0	0
Total - non-competing	0	0	0	0	0	0	0
Total	5	3	1	4	2	0	0

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
z3-alpha	QF_NRA
Total - competing	6	1	5	2	0	0
Total - non-competing	0	0	0	0	0	0
Total	6	1	5	2	0	0

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
z3-alpha	QF_S QF_SLIA QF_SNIA
Total - competing	4	1	2	0	0
Total - non-competing	0	0	0	0	0
Total	4	1	2	0	0