Participants

The following solvers have been submitted to SMT-COMP 2022 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				36798	39101	42	Bitwuzla at the SMT-COMP 2022
COLIBRI	X							36854	36854	7	COLIBRI: SMT solving with CP
NRA-LS	X							36859(sq)	39120	666	NRA-LS at the SMT Competition 2022
OSTRICH	X							36797	39065	74672647	The OSTRICH String Solver
OpenSMT	X	X		X	X			39040	39040	91648253	OpenSMT in SMT-COMP 2022
Q3B-pBDD	X							36885	39086	658700	Q3B-pBDD in SMT Competition 2022
Q3B	X							36884	39062	735340574	Q3B in SMT-COMP 2022
SMT-RAT-MCSAT 22.06	X							36804	36804	5630542780	SMT-RAT 22.06
SMTS cube-and-conquer						X	X		1
SMTS portfolio						X	X		3
STP	X	X		X				38974	38974	679	STP at the SMT-COMP 2022
UltimateEliminator+MathSAT	X	X	X					36966	39121	0	UltimateEliminator at SMT-COMP 2022
Vampire	X		X			X	X	36957	39081	6284	Vampire 4.7 for SMT-COMP 22
Yices-ismt	X							36803(sq)	39056	19970805	Yices-ismt for SMT COMP 2022
Yices2	X	X	X	X				33403 33404(inc) 33405(mv)	33403 33404(inc) 33405(mv)	0	Yices 2 in SMT-COMP 2022
YicesQS	X							36836	39111	0	Yices-QS, an extension of Yices for quantified satisfiability
Z3++	X			X				38965	38965	1	Z3++ at SMT-COMP 2022
Z3++BV	X			X				38972	39106		Z3++ at SMT-COMP 2022
Z3str4	X							36977	39107	33	Z3str4, an SMT solver for the SMT-LIB theory of strings
cvc5-cloud						X	X		4
cvc5-lfsc					X			39052	39113	5	cvc5 at the SMT Competition 2022
cvc5	X	X	X	X	X			36875(sq) 36870(inc) 36872(mv) 39025(pe) 36869(uc)	39117 39114(inc)	5	cvc5 at the SMT Competition 2022
smtinterpol	X	X	X	X	X			39066	39093	945345692	SMTInterpol with resolution proofs
solsmt	X	X						39004	39077	3729	solsmt at the SMT Competition 2022
veriT+raSAT+Redlog	X							33044(sq)	33044	2039	veriT+raSAT+Redlog at SMT-COMP 2022
veriT	X				X			36975(pe) 33452(sq)	39098(pe) 33452(sq)	109	veriT at SMT-COMP 2022
2018-MathSAT-incrementaln		X							19993
2019-CVC4-incn		X						23417	23733		CVC4 at the SMT Competition 2019
2019-Par4n	X							23391	23672		Par4
2019-Z3n		X						23470	23470
2020-Bitwuzla-fixedn	X		X					29091	29091		Bitwuzla at the SMT Competition 2020
2020-Bitwuzlan	X			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-Yices2 incrementaln		X						28344	28821		Yices 2 in SMT-COMP 2020
2020-z3n		X		X				28814	28814
2021-Bitwuzlan			X					33006	33292		Bitwuzla at the SMT-COMP 2021
2021-Bitwuzla - fixedn		X							33809
2021-MathSAT5n		X	X						33739
2021-SMTInterpoln	X			X				32995	33439		SMTInterpol and SMTInterpol-remus
2021-STPn		X						28776	33442		STP in the SMT-COMP 2021
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-cvc5n	X							33075	33446		cvc5 at the SMT Competition 2021
2021-z3n	X	X	X						33741
MathSATn	X	X	X	X					41381
OpenSMT-fixedn	X								41413
STP-fixedn	X								41385
Yices-ismt-fixedn	X								41411
Z3++-fixedn	X								41324
smtinterpol-fixedn	X								41483
z3-4.8.17n	X	X	X	X					41383
Total - competing	22	8	6	8	5	4	4
Total - non-competing	15	13	9	6	0	0	0
Total	37	21	15	14	5	4	4			1055742106 (mod 230)

n Non-competing.

The opening value of the NYSE Composite Index on 2022-07-05 was 14636.7563, resulting in a competition seed of 1055742106 + 1463675 = 1057205781.

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
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
YicesQS	LIA LRA NIA NRA
cvc5-cloud					LIA LRA NIA NRA	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
smtinterpol	LIA LRA NIA NRA	LIA LRA	LIA LRA NIA NRA	LIA LRA NIA NRA
veriT	LIA LRA NIA NRA			LIA LRA NIA NRA
2020-CVC4-ucn			LIA LRA NIA NRA
2021-cvc5-incn		LIA LRA
2021-z3n	LIA LRA NIA NRA
z3-4.8.17n	LIA LRA NIA NRA	LIA LRA	LIA LRA NIA NRA
Total - competing	6	3	4	4	2	2
Total - non-competing	2	2	2	0	0	0
Total	8	5	6	4	2	2

Bitvec

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

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
Yices2	UF UFDT
cvc5-cloud					UF UFDT	UF UFDT
cvc5-lfsc				UF UFDT
cvc5	UF UFDT	UF	UF UFDT	UF UFDT
smtinterpol	UF UFDT	UF	UF UFDT	UF UFDT
veriT	UF UFDT			UF UFDT
2020-CVC4-ucn			UF UFDT
2020-CVC4n	UF UFDT
2020-z3n		UF
z3-4.8.17n	UF UFDT	UF	UF UFDT
Total - competing	6	3	4	4	2	2
Total - non-competing	2	2	2	0	0	0
Total	8	5	6	4	2	2

Equality+LinearArith

Solver	Single Query Track	Incremental Track	Unsat Core Track	Proof Exhibition Track	Cloud Track	Parallel Track
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-cloud					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
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
veriT	ALIA AUFDTLIA AUFDTLIRA AUFLIA AUFLIRA UFDTLIA UFDTLIRA UFIDL UFLIA UFLRA			ALIA AUFDTLIA AUFDTLIRA AUFLIA AUFLIRA UFDTLIA UFDTLIRA UFIDL UFLIA UFLRA
2020-CVC4n	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
smtinterpol-fixedn	ALIA AUFDTLIA AUFDTLIRA AUFLIA AUFLIRA UFDTLIA UFDTLIRA UFIDL UFLIA UFLRA
z3-4.8.17n	ALIA AUFDTLIA AUFDTLIRA AUFLIA AUFLIRA UFDTLIA UFDTLIRA UFIDL UFLIA UFLRA	ALIA UFLRA	ALIA AUFDTLIA AUFDTLIRA AUFLIA AUFLIRA UFDTLIA UFDTLIRA UFIDL UFLIA UFLRA
Total - competing	5	3	4	4	2	2
Total - non-competing	3	2	2	0	0	0
Total	8	5	6	4	2	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 UFBVFP UFBVLIA UFFPDTNIRA	ABVFPLRA
UltimateEliminator+MathSAT	ABV ABVFP ABVFPLRA AUFBV AUFBVDTLIA AUFBVDTNIA AUFBVDTNIRA AUFBVFP AUFFPDTNIRA UFBV UFBVFP UFBVLIA UFFPDTNIRA	ABVFPLRA	ABV ABVFP ABVFPLRA AUFBV AUFBVDTLIA AUFBVDTNIA AUFBVDTNIRA AUFBVFP AUFFPDTNIRA UFBV UFBVFP UFBVLIA UFFPDTNIRA
cvc5-cloud					ABV ABVFP ABVFPLRA AUFBV AUFBVDTLIA AUFBVDTNIA AUFBVDTNIRA AUFBVFP AUFFPDTNIRA UFBV UFBVFP UFBVLIA UFFPDTNIRA	ABV ABVFP ABVFPLRA AUFBV AUFBVDTLIA AUFBVDTNIA AUFBVDTNIRA AUFBVFP AUFFPDTNIRA UFBV UFBVFP UFBVLIA UFFPDTNIRA
cvc5-lfsc				ABV ABVFP ABVFPLRA AUFBV AUFBVDTLIA AUFBVDTNIA AUFBVDTNIRA AUFBVFP AUFFPDTNIRA UFBV UFBVFP UFBVLIA UFFPDTNIRA
cvc5	ABV ABVFP ABVFPLRA AUFBV AUFBVDTLIA AUFBVDTNIA AUFBVDTNIRA AUFBVFP AUFFPDTNIRA UFBV UFBVFP UFBVLIA UFFPDTNIRA	ABVFPLRA	ABV ABVFP ABVFPLRA AUFBV AUFBVDTLIA AUFBVDTNIA AUFBVDTNIRA AUFBVFP AUFFPDTNIRA UFBV UFBVFP UFBVLIA UFFPDTNIRA	ABV ABVFP ABVFPLRA AUFBV AUFBVDTLIA AUFBVDTNIA AUFBVDTNIRA AUFBVFP AUFFPDTNIRA UFBV UFBVFP UFBVLIA UFFPDTNIRA
2021-cvc5-ucn			ABV ABVFP ABVFPLRA AUFBV AUFBVDTLIA AUFBVDTNIA AUFBVDTNIRA AUFBVFP AUFFPDTNIRA UFBV UFBVFP UFBVLIA UFFPDTNIRA
2021-cvc5n	ABV ABVFP ABVFPLRA AUFBV AUFBVDTLIA AUFBVDTNIA AUFBVDTNIRA AUFBVFP AUFFPDTNIRA UFBV UFBVFP UFBVLIA UFFPDTNIRA
z3-4.8.17n	ABV ABVFP ABVFPLRA AUFBV AUFBVDTLIA AUFBVDTNIA AUFBVDTNIRA AUFBVFP AUFFPDTNIRA UFBV UFBVFP UFBVLIA UFFPDTNIRA		ABV ABVFP ABVFPLRA AUFBV AUFBVDTLIA AUFBVDTNIA AUFBVDTNIRA AUFBVFP AUFFPDTNIRA UFBV UFBVFP UFBVLIA UFFPDTNIRA
Total - competing	3	3	2	2	1	1
Total - non-competing	2	0	2	0	0	0
Total	5	3	4	2	1	1

Equality+NonLinearArith

Solver	Single Query Track	Incremental Track	Unsat Core Track	Proof Exhibition Track	Cloud Track	Parallel Track
UltimateEliminator+MathSAT	AUFDTNIRA AUFNIA AUFNIRA UFDTNIA UFDTNIRA UFNIA	ANIA AUFNIRA UFDTNIA UFNIA UFNRA	AUFDTNIRA AUFNIA AUFNIRA UFDTNIA UFDTNIRA UFNIA
Vampire	AUFDTNIRA AUFNIA AUFNIRA UFDTNIA UFDTNIRA UFNIA		AUFDTNIRA AUFNIA AUFNIRA UFDTNIA UFDTNIRA UFNIA		AUFDTNIRA AUFNIA AUFNIRA UFDTNIA UFDTNIRA UFNIA	AUFDTNIRA AUFNIA AUFNIRA UFDTNIA UFDTNIRA UFNIA
cvc5-cloud					AUFDTNIRA AUFNIA AUFNIRA UFDTNIA UFDTNIRA UFNIA	AUFDTNIRA AUFNIA AUFNIRA UFDTNIA UFDTNIRA UFNIA
cvc5-lfsc				AUFDTNIRA AUFNIA AUFNIRA UFDTNIA UFDTNIRA UFNIA
cvc5	AUFDTNIRA AUFNIA AUFNIRA UFDTNIA UFDTNIRA UFNIA	ANIA AUFNIRA UFDTNIA UFNIA UFNRA	AUFDTNIRA AUFNIA AUFNIRA UFDTNIA UFDTNIRA UFNIA	AUFDTNIRA AUFNIA AUFNIRA UFDTNIA UFDTNIRA UFNIA
smtinterpol		ANIA AUFNIRA UFDTNIA UFNIA UFNRA
2020-CVC4-ucn			AUFDTNIRA AUFNIA AUFNIRA UFDTNIA UFDTNIRA UFNIA
2020-CVC4n	AUFDTNIRA AUFNIA AUFNIRA UFDTNIA UFDTNIRA UFNIA
2020-z3n		ANIA AUFNIRA UFDTNIA UFNIA UFNRA
z3-4.8.17n	AUFDTNIRA AUFNIA AUFNIRA UFDTNIA UFDTNIRA UFNIA	ANIA AUFNIRA UFDTNIA UFNIA UFNRA	AUFDTNIRA AUFNIA AUFNIRA UFDTNIA UFDTNIRA UFNIA
Total - competing	3	3	3	2	2	2
Total - non-competing	2	2	2	0	0	0
Total	5	5	5	2	2	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
UltimateEliminator+MathSAT	BVFP BVFPLRA FP FPLRA	BVFP BVFPLRA	BVFP BVFPLRA FP FPLRA
cvc5-cloud					BVFP BVFPLRA FP FPLRA	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
2019-CVC4-incn		BVFP BVFPLRA
2020-CVC4-ucn			BVFP BVFPLRA FP FPLRA
2021-cvc5n	BVFP BVFPLRA FP FPLRA
z3-4.8.17n	BVFP BVFPLRA FP FPLRA		BVFP BVFPLRA FP FPLRA
Total - competing	3	3	2	2	1	1
Total - non-competing	2	1	2	0	0	0
Total	5	4	4	2	1	1

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
Yices2	QF_BV	QF_BV	QF_BV	QF_BV
Z3++BV	QF_BV			QF_BV
cvc5-cloud						QF_BV	QF_BV
cvc5-lfsc					QF_BV
cvc5	QF_BV	QF_BV	QF_BV	QF_BV	QF_BV
2020-Bitwuzla-fixedn	QF_BV		QF_BV
2020-Bitwuzlan				QF_BV
2021-STPn		QF_BV
MathSATn	QF_BV	QF_BV	QF_BV	QF_BV
STP-fixedn	QF_BV
z3-4.8.17n	QF_BV	QF_BV	QF_BV	QF_BV
Total - competing	5	4	3	5	2	1	1
Total - non-competing	4	3	3	3	0	0	0
Total	9	7	6	8	2	1	1

QF_Datatypes

Solver	Single Query Track	Unsat Core Track	Proof Exhibition Track	Cloud Track	Parallel Track
cvc5-cloud				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
smtinterpol	QF_DT QF_UFDT	QF_DT QF_UFDT	QF_DT QF_UFDT
2021-z3n	QF_DT QF_UFDT	QF_DT QF_UFDT
z3-4.8.17n	QF_DT QF_UFDT	QF_DT QF_UFDT
Total - competing	2	2	3	1	1
Total - non-competing	2	2	0	0	0
Total	4	4	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	QF_AX QF_UF
SMTS cube-and-conquer						QF_AX QF_UF	QF_AX QF_UF
SMTS portfolio						QF_AX QF_UF	QF_AX QF_UF
Yices2	QF_AX QF_UF	QF_UF	QF_AX QF_UF	QF_UF
cvc5-cloud						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_UF	QF_AX QF_UF
smtinterpol	QF_AX QF_UF	QF_UF	QF_AX QF_UF	QF_UF	QF_AX QF_UF
veriT	QF_AX QF_UF				QF_AX QF_UF
2021-Yices2 model-validationn				QF_UF
2021-z3n	QF_AX QF_UF	QF_UF	QF_AX QF_UF
MathSATn	QF_AX QF_UF	QF_UF	QF_AX QF_UF	QF_UF
OpenSMT-fixedn	QF_AX QF_UF
z3-4.8.17n	QF_AX QF_UF	QF_UF	QF_AX QF_UF	QF_UF
Total - competing	5	4	3	4	5	3	3
Total - non-competing	4	3	3	3	0	0	0
Total	9	7	6	7	5	3	3

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_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	QF_ABV QF_AUFBV QF_UFBV	QF_UFBV
cvc5-cloud						QF_ABV QF_AUFBV QF_UFBV	QF_ABV QF_AUFBV QF_UFBV
cvc5-lfsc					QF_ABV QF_AUFBV QF_UFBV
cvc5	QF_ABV QF_AUFBV QF_UFBV	QF_ABV QF_AUFBV QF_UFBV	QF_ABV QF_AUFBV QF_UFBV	QF_UFBV	QF_ABV QF_AUFBV QF_UFBV
2020-Bitwuzlan	QF_ABV QF_AUFBV QF_UFBV
2020-Yices2 incrementaln		QF_ABV QF_AUFBV QF_UFBV
2021-Bitwuzlan			QF_ABV QF_AUFBV QF_UFBV
2021-Yices2 model-validationn				QF_UFBV
MathSATn	QF_ABV QF_AUFBV QF_UFBV	QF_ABV QF_AUFBV QF_UFBV	QF_ABV QF_AUFBV QF_UFBV	QF_UFBV
z3-4.8.17n	QF_ABV QF_AUFBV QF_UFBV	QF_ABV QF_AUFBV QF_UFBV	QF_ABV QF_AUFBV QF_UFBV	QF_UFBV
Total - competing	3	3	3	3	2	1	1
Total - non-competing	3	3	3	3	0	0	0
Total	6	6	6	6	2	1	1

QF_Equality+Bitvec+Arith

Solver	Incremental Track
cvc5	QF_AUFBVLIA QF_AUFBVNIA QF_UFBVLIA
MathSATn	QF_AUFBVLIA QF_AUFBVNIA QF_UFBVLIA
Total - competing	1
Total - non-competing	1
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_UFDTLIRA QF_UFIDL QF_UFLIA QF_UFLRA	QF_ALIA QF_AUFLIA QF_UFLIA QF_UFLRA		QF_UFIDL QF_UFLIA QF_UFLRA
SMTS cube-and-conquer						QF_ALIA QF_AUFLIA QF_UFDTLIRA QF_UFIDL QF_UFLIA QF_UFLRA	QF_ALIA QF_AUFLIA QF_UFDTLIRA QF_UFIDL QF_UFLIA QF_UFLRA
SMTS portfolio						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	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_UFLIA QF_UFLRA
cvc5-cloud						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-lfsc					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	QF_ALIA QF_AUFLIA QF_UFLIA QF_UFLRA	QF_ALIA QF_AUFLIA QF_UFDTLIRA QF_UFIDL QF_UFLIA QF_UFLRA	QF_UFIDL QF_UFLIA QF_UFLRA	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_UFLIA QF_UFLRA	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				QF_ALIA QF_AUFLIA QF_UFDTLIRA QF_UFIDL QF_UFLIA QF_UFLRA
2020-z3n		QF_ALIA QF_AUFLIA QF_UFLIA QF_UFLRA
2021-MathSAT5n			QF_ALIA QF_AUFLIA QF_UFDTLIRA QF_UFIDL QF_UFLIA QF_UFLRA
2021-SMTInterpoln	QF_ALIA QF_AUFLIA QF_UFDTLIRA QF_UFIDL QF_UFLIA QF_UFLRA			QF_UFIDL QF_UFLIA QF_UFLRA
MathSATn	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_UFLIA QF_UFLRA
z3-4.8.17n	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_UFLIA QF_UFLRA
Total - competing	5	4	3	4	4	3	3
Total - non-competing	3	3	3	3	0	0	0
Total	8	7	6	7	4	3	3

QF_Equality+NonLinearArith

Solver	Single Query Track	Incremental Track	Unsat Core Track	Proof Exhibition Track	Cloud Track	Parallel Track
Yices2	QF_ANIA QF_AUFNIA QF_UFNIA QF_UFNRA	QF_ANIA QF_UFNIA QF_UFNRA
cvc5-cloud					QF_ANIA QF_AUFNIA QF_UFNIA QF_UFNRA	QF_ANIA QF_AUFNIA QF_UFNIA QF_UFNRA
cvc5-lfsc				QF_ANIA QF_AUFNIA QF_UFNIA QF_UFNRA
cvc5	QF_ANIA QF_AUFNIA QF_UFNIA QF_UFNRA	QF_ANIA QF_UFNIA QF_UFNRA	QF_ANIA QF_AUFNIA QF_UFNIA QF_UFNRA	QF_ANIA QF_AUFNIA QF_UFNIA QF_UFNRA
smtinterpol	QF_ANIA QF_AUFNIA QF_UFNIA QF_UFNRA	QF_ANIA QF_UFNIA QF_UFNRA	QF_ANIA QF_AUFNIA QF_UFNIA QF_UFNRA	QF_ANIA QF_AUFNIA QF_UFNIA QF_UFNRA
veriT+raSAT+Redlog	QF_ANIA QF_AUFNIA QF_UFNIA QF_UFNRA
2020-CVC4n	QF_ANIA QF_AUFNIA QF_UFNIA QF_UFNRA
2021-cvc5-ucn			QF_ANIA QF_AUFNIA QF_UFNIA QF_UFNRA
2021-z3n		QF_ANIA QF_UFNIA QF_UFNRA
MathSATn	QF_ANIA QF_AUFNIA QF_UFNIA QF_UFNRA	QF_ANIA QF_UFNIA QF_UFNRA	QF_ANIA QF_AUFNIA QF_UFNIA QF_UFNRA
z3-4.8.17n	QF_ANIA QF_AUFNIA QF_UFNIA QF_UFNRA	QF_ANIA QF_UFNIA QF_UFNRA	QF_ANIA QF_AUFNIA QF_UFNIA QF_UFNRA
Total - competing	4	3	2	3	1	1
Total - non-competing	3	3	3	0	0	0
Total	7	6	5	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_FPLRA QF_UFFP	QF_ABVFP QF_ABVFPLRA QF_AUFBVFP QF_BVFP QF_BVFPLRA QF_FP QF_FPLRA QF_UFFP QF_UFFPDTNIRA	QF_BVFP QF_BVFPLRA QF_FP QF_FPLRA QF_UFFP
COLIBRI	QF_ABVFP QF_ABVFPLRA QF_AUFBVFP QF_BVFP QF_BVFPLRA QF_FP QF_FPLRA QF_UFFP QF_UFFPDTNIRA
cvc5-cloud						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
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_FPLRA QF_UFFP	QF_ABVFP QF_ABVFPLRA QF_AUFBVFP QF_BVFP QF_BVFPLRA QF_FP QF_FPLRA QF_UFFP QF_UFFPDTNIRA	QF_BVFP QF_BVFPLRA QF_FP QF_FPLRA QF_UFFP	QF_ABVFP QF_ABVFPLRA QF_AUFBVFP QF_BVFP QF_BVFPLRA QF_FP QF_FPLRA QF_UFFP QF_UFFPDTNIRA
2021-Bitwuzlan			QF_ABVFP QF_ABVFPLRA QF_AUFBVFP QF_BVFP QF_BVFPLRA QF_FP QF_FPLRA QF_UFFP QF_UFFPDTNIRA
2021-Bitwuzla - fixedn		QF_ABVFP QF_ABVFPLRA QF_BVFP QF_BVFPLRA QF_FP QF_FPLRA QF_UFFP
2021-cvc5n	QF_ABVFP QF_ABVFPLRA QF_AUFBVFP QF_BVFP QF_BVFPLRA QF_FP QF_FPLRA QF_UFFP QF_UFFPDTNIRA
MathSATn	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_FPLRA QF_UFFP	QF_ABVFP QF_ABVFPLRA QF_AUFBVFP QF_BVFP QF_BVFPLRA QF_FP QF_FPLRA QF_UFFP QF_UFFPDTNIRA	QF_BVFP QF_BVFPLRA QF_FP QF_FPLRA QF_UFFP
z3-4.8.17n	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_FPLRA QF_UFFP	QF_ABVFP QF_ABVFPLRA QF_AUFBVFP QF_BVFP QF_BVFPLRA QF_FP QF_FPLRA QF_UFFP QF_UFFPDTNIRA	QF_BVFP QF_BVFPLRA QF_FP QF_FPLRA QF_UFFP
Total - competing	3	2	2	2	2	1	1
Total - non-competing	3	3	3	2	0	0	0
Total	6	5	5	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	QF_IDL QF_LIA QF_LIRA
SMTS cube-and-conquer						QF_IDL QF_LIA QF_LIRA	QF_IDL QF_LIA QF_LIRA
SMTS portfolio						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-cloud						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
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
veriT	QF_IDL QF_LIA QF_LIRA				QF_IDL QF_LIA QF_LIRA
2019-Par4n	QF_IDL QF_LIA QF_LIRA
2020-z3n				QF_IDL QF_LIA QF_LIRA
2021-Yices2 incrementaln		QF_LIA
2021-cvc5-ucn			QF_IDL QF_LIA QF_LIRA
MathSATn	QF_IDL QF_LIA QF_LIRA	QF_LIA	QF_IDL QF_LIA QF_LIRA	QF_IDL QF_LIA QF_LIRA
z3-4.8.17n	QF_IDL QF_LIA QF_LIRA	QF_LIA	QF_IDL QF_LIA QF_LIRA	QF_IDL QF_LIA QF_LIRA
Total - competing	6	4	3	5	5	3	3
Total - non-competing	3	3	3	3	0	0	0
Total	9	7	6	8	5	3	3

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	QF_LRA QF_RDL
SMTS cube-and-conquer						QF_LRA QF_RDL	QF_LRA QF_RDL
SMTS portfolio						QF_LRA QF_RDL	QF_LRA QF_RDL
Yices2	QF_LRA QF_RDL	QF_LRA	QF_LRA QF_RDL	QF_LRA QF_RDL
cvc5-cloud						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
smtinterpol	QF_LRA QF_RDL	QF_LRA	QF_LRA QF_RDL	QF_LRA QF_RDL	QF_LRA QF_RDL
solsmt	QF_LRA QF_RDL	QF_LRA
veriT	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
2021-Yices2 model-validationn				QF_LRA QF_RDL
MathSATn	QF_LRA QF_RDL	QF_LRA	QF_LRA QF_RDL	QF_LRA QF_RDL
z3-4.8.17n	QF_LRA QF_RDL	QF_LRA	QF_LRA QF_RDL	QF_LRA QF_RDL
Total - competing	6	5	3	4	5	3	3
Total - non-competing	3	3	3	3	0	0	0
Total	9	8	6	7	5	3	3

QF_NonLinearIntArith

Solver	Single Query Track	Incremental Track	Unsat Core Track	Proof Exhibition Track	Cloud Track	Parallel Track
Yices-ismt	QF_NIA QF_NIRA
Yices2	QF_NIA QF_NIRA	QF_NIA
Z3++	QF_NIA QF_NIRA
cvc5-cloud					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
smtinterpol		QF_NIA
2019-Par4n	QF_NIA QF_NIRA
2021-MathSAT5n		QF_NIA
2021-z3n			QF_NIA QF_NIRA
MathSATn	QF_NIA QF_NIRA	QF_NIA	QF_NIA QF_NIRA
Yices-ismt-fixedn	QF_NIA QF_NIRA
Z3++-fixedn	QF_NIA QF_NIRA
z3-4.8.17n	QF_NIA QF_NIRA	QF_NIA	QF_NIA QF_NIRA
Total - competing	4	3	1	2	1	1
Total - non-competing	5	3	3	0	0	0
Total	9	6	4	2	1	1

QF_NonLinearRealArith

Solver	Single Query Track	Unsat Core Track	Proof Exhibition Track	Cloud Track	Parallel Track
NRA-LS	QF_NRA
SMT-RAT-MCSAT 22.06	QF_NRA
Yices2	QF_NRA
Z3++	QF_NRA
cvc5-cloud				QF_NRA	QF_NRA
cvc5-lfsc			QF_NRA
cvc5	QF_NRA	QF_NRA	QF_NRA
veriT+raSAT+Redlog	QF_NRA
2019-Par4n	QF_NRA
2021-cvc5-ucn		QF_NRA
MathSATn	QF_NRA	QF_NRA
Z3++-fixedn	QF_NRA
z3-4.8.17n	QF_NRA	QF_NRA
Total - competing	6	1	2	1	1
Total - non-competing	4	3	0	0	0
Total	10	4	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
Z3str4	QF_S QF_SLIA QF_SNIA
cvc5-cloud				QF_S QF_SLIA QF_SNIA	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
2020-CVC4n	QF_S QF_SLIA QF_SNIA
z3-4.8.17n	QF_S QF_SLIA QF_SNIA	QF_S QF_SLIA QF_SNIA
Total - competing	3	1	2	1	1
Total - non-competing	2	1	0	0	0
Total	5	2	2	1	1