SMT-COMP 2026

The International Satisfiability Modulo Theories (SMT) Competition.

SMT-COMP 2026

Largest Contribution Ranking - Single Query Track

Page generated on 2026-07-25

Winners

Sequential Performance	Parallel Performance	SAT Performance (parallel)	UNSAT Performance (parallel)	24 seconds Performance (parallel)
Amaya	Amaya	UltimateEliminator+MathSAT	Xolver	Yices2

Sequential Performance

Division	Solver	Correct Score	Time Score
Arith	Amaya	0.001851	0.023112
QF_Datatypes	Z3-Z3++	0.001467	0.005159
QF_NonLinearIntArith	Xolver	0.001441	-0.013506
Equality_LinearArith	UltimateEliminator+MathSAT	0.000845	0.00108
QF_Strings	Z3-Noodler	0.000653	0.148695
QF_Equality_NonLinearArith	Yices2	0.000608	0.000576
QF_LinearIntArith	QiuQi	0.000585	0.024883
QF_NonLinearIntArith	Z3-Z3++	0.000531	0.016339
Equality_MachineArith	SMTInterpol	0.000419	0.006504
Arith	YicesQS	0.00037	0.026349
QF_Equality_LinearArith	cvc5-cvc5-xyz	0.000362	-0.000139
QF_Equality_Bitvec	SMTInterpol	0.000303	0.003929
Equality_MachineArith	cvc5-cvc5-xyz	0.00027	-0.004166
QF_LinearIntArith	Yices2	0.000251	0.029904
QF_NonLinearIntArith	Yices2	0.000228	0.00855
QF_Bitvec	Bitwuzla-MachBV	0.000213	0.013244
Equality_LinearArith	z3-BooledASS	0.000211	0.000775
QF_LinearRealArith	Yices2	0.000202	0.000214
QF_NonLinearIntArith	Z3-GEX	0.000152	-0.007514

Parallel Performance

Division	Solver	Correct Score	Time Score
Arith	Amaya	0.001851	0.022685
QF_Datatypes	Z3-Z3++	0.001448	0.005109
QF_NonLinearIntArith	Xolver	0.001441	-0.014957
Equality_LinearArith	UltimateEliminator+MathSAT	0.000845	0.001232
QF_Strings	Z3-Noodler	0.000653	0.145998
QF_Equality_NonLinearArith	Yices2	0.000608	0.000126
QF_LinearIntArith	QiuQi	0.000584	0.021034
QF_NonLinearIntArith	Z3-Z3++	0.000531	0.016625
Equality_MachineArith	SMTInterpol	0.000419	0.006681
QF_Equality_LinearArith	cvc5-cvc5-xyz	0.000362	-0.000311
Arith	YicesQS	0.000339	0.025021
QF_Equality_Bitvec	SMTInterpol	0.000303	0.006172
Equality_MachineArith	cvc5-cvc5-xyz	0.00027	-0.004176
QF_NonLinearIntArith	Yices2	0.000227	0.008685
QF_Bitvec	Bitwuzla-MachBV	0.000213	0.012973
Equality_LinearArith	z3-BooledASS	0.000211	0.000778
QF_NonLinearIntArith	Z3-GEX	0.00019	-0.001262
QF_LinearRealArith	Yices2	0.000169	0.002372
QF_LinearIntArith	Yices2	0.000167	0.027415

SAT Performance

Division	Solver	Correct Score	Time Score
Equality_LinearArith	UltimateEliminator+MathSAT	0.007145	-0.000254
Arith	Amaya	0.004472	0.020481
Equality_LinearArith	z3-BooledASS	0.001786	0.001411
QF_NonLinearIntArith	Z3-Z3++	0.000758	0.031291
QF_Equality_NonLinearArith	Yices2	0.000704	0.00082
QF_NonLinearIntArith	Xolver	0.000525	0.011276
Arith	YicesQS	0.000447	0.015211
QF_Equality_LinearArith	cvc5-cvc5-xyz	0.000433	-0.01015
QF_Strings	Z3-Noodler	0.000432	0.148866
QF_Datatypes	Z3-Z3++	0.000336	0.005453
Equality_MachineArith	SMTInterpol	0.000336	-6e-06
QF_Bitvec	Bitwuzla-MachBV	0.000326	-0.003661
QF_LinearIntArith	Yices2	0.000264	0.027174
QF_LinearIntArith	QiuQi	0.000198	0.015366
QF_LinearRealArith	Yices2	0.000187	0.003576
Equality_NonLinearArith	z3-BooledASS	0.000176	3.4e-05
Equality_NonLinearArith	SMTInterpol	0.000176	-1.7e-05
Equality_MachineArith	z3-BooledASS	0.000144	-0.001094
QF_Datatypes	SMTInterpol	0.000135	0.000433

UNSAT Performance

Division	Solver	Correct Score	Time Score
QF_NonLinearIntArith	Xolver	0.003144	-0.049648
QF_Datatypes	Z3-Z3++	0.001865	0.005001
QF_LinearIntArith	QiuQi	0.001248	0.032326
QF_Strings	Z3-Noodler	0.000929	0.109487
QF_Equality_Bitvec	SMTInterpol	0.000823	0.018398
QF_NonLinearIntArith	Yices2	0.000651	0.001494
Equality_MachineArith	SMTInterpol	0.000451	0.010317
QF_NonLinearIntArith	Z3-GEX	0.000434	-0.002483
Equality_MachineArith	cvc5-cvc5-xyz	0.000357	-0.006818
QF_Equality_NonLinearArith	Yices2	0.000291	-0.000975
QF_Equality_NonLinearArith	SMTInterpol	0.000291	-0.002397
QF_Equality_LinearArith	cvc5-cvc5-xyz	0.000272	0.00786
Arith	YicesQS	0.000263	0.033549
QF_NonLinearRealArith	Yices2	0.000239	0.00248
QF_NonLinearIntArith	Z3-alpha2	0.000217	0.009369
QF_LinearRealArith	Yices2	0.000147	0.000726
Bitvec	YicesQS	0.000145	0.000567
QF_FPArith	colibri2	0.000134	0.018701
FPArith	Bitwuzla	0.000115	-0.003534

24 seconds Performance

Division	Solver	Correct Score	Time Score
QF_LinearIntArith	Yices2	0.005758	0.034583
QF_Strings	Z3-Noodler	0.0054	0.067125
QF_Datatypes	Z3-Z3++	0.005069	-0.00798
Arith	Amaya	0.002098	-0.022686
QF_LinearIntArith	QiuQi	0.001802	-0.001484
QF_NonLinearIntArith	Z3-Z3++	0.001364	0.016234
Equality_MachineArith	SMTInterpol	0.00112	-0.003306
Arith	YicesQS	0.000939	0.01303
Equality_LinearArith	UltimateEliminator+MathSAT	0.000912	-0.000723
QF_FPArith	colibri2	0.000647	0.003579
QF_Equality_NonLinearArith	Yices2	0.000584	0.00126
QF_Equality_Bitvec	Bitwuzla	0.000515	0.002542
QF_Equality_Bitvec	SMTInterpol	0.000487	0.003907
QF_NonLinearIntArith	Yices2	0.000441	0.009029
QF_LinearRealArith	Yices2	0.00044	0.003999
QF_NonLinearRealArith	Z3-GEX	0.000409	0.003591
QF_NonLinearIntArith	Xolver	0.000401	0.005436
QF_Bitvec	SMTInterpol	0.000328	-7.5e-05
QF_NonLinearRealArith	Yices2	0.000327	0.007376