SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

SMT-COMP 2025

Best Overall Ranking - Parallel Track

Page generated on 2025-08-11

Winners

Sequential Performance	Parallel Performance	SAT Performance (parallel)	UNSAT Performance (parallel)	24 seconds Performance (parallel)
—	Z3-Parti-Z3pp (0.751708)	Z3-Parti-Z3pp (0.308602)	Bitwuzla (0.160051)	Z3-Parti-Z3pp (0.090967)

Parallel Performance

Division	Solver	Contribution
QF_Bitvec	STP-Parti-Bitwuzla	0.57285
QF_NonLinearIntArith	Z3-Parti-Z3pp	0.374361
QF_Bitvec	Bitwuzla	0.346539
QF_LinearRealArith	SMTS	0.225681
QF_NonLinearRealArith	Z3-Parti-Z3pp	0.217316
QF_LinearIntArith	SMTS	0.192946
QF_LinearIntArith	Z3-Parti-Z3pp	0.130189
QF_Equality_Bitvec	Bitwuzla	0.091591
QF_Equality_LinearArith	SMTS	0.089168
QF_NonLinearIntArith	Yices2	0.084889
QF_LinearRealArith	Yices2	0.078802
QF_Equality_Bitvec	Yices2	0.075695
QF_NonLinearRealArith	Yices2	0.041596
QF_Equality_LinearArith	Yices2	0.03963
QF_LinearRealArith	Z3-Parti-Z3pp	0.029842
QF_LinearIntArith	Yices2	0.003938
QF_Bitvec	Bitwuzla-32core	0
QF_Bitvec	Bitwuzla-64core	0
QF_Bitvec	STP-Parti-Bitwuzla-16core	0
QF_Bitvec	STP-Parti-Bitwuzla-32core	0
QF_Bitvec	STP-Parti-Bitwuzla-64core	0
QF_Equality_Bitvec	Bitwuzla-32core	0
QF_Equality_Bitvec	Bitwuzla-64core	0
QF_LinearRealArith	SMTS (32 cores)	0
QF_LinearRealArith	SMTS (64 cores)	0
QF_LinearRealArith	Z3-Parti-Z3pp-16core	0
QF_LinearRealArith	Z3-Parti-Z3pp-32core	0
QF_LinearRealArith	Z3-Parti-Z3pp-64core	0
QF_NonLinearIntArith	Z3-Parti-Z3pp-16core	0
QF_NonLinearIntArith	Z3-Parti-Z3pp-32core	0
QF_NonLinearIntArith	Z3-Parti-Z3pp-64core	0
QF_NonLinearRealArith	Z3-Parti-Z3pp-16core	0
QF_NonLinearRealArith	Z3-Parti-Z3pp-32core	0
QF_NonLinearRealArith	Z3-Parti-Z3pp-64core	0
QF_Equality_LinearArith	SMTS (32 cores)	0
QF_Equality_LinearArith	SMTS (64 cores)	0
QF_LinearIntArith	SMTS (32 cores)	0
QF_LinearIntArith	SMTS (64 cores)	0
QF_LinearIntArith	Z3-Parti-Z3pp-16core	0
QF_LinearIntArith	Z3-Parti-Z3pp-32core	0
QF_LinearIntArith	Z3-Parti-Z3pp-64core	0

SAT Performance

Division	Solver	Contribution
QF_NonLinearIntArith	Z3-Parti-Z3pp	0.143463
QF_Bitvec	STP-Parti-Bitwuzla	0.132801
QF_NonLinearRealArith	Z3-Parti-Z3pp	0.12224
QF_LinearIntArith	SMTS	0.119114
QF_LinearRealArith	SMTS	0.078802
QF_Bitvec	Bitwuzla	0.050291
QF_LinearRealArith	Yices2	0.037769
QF_LinearIntArith	Z3-Parti-Z3pp	0.035439
QF_Equality_LinearArith	Yices2	0.019419
QF_Equality_Bitvec	Bitwuzla	0.018924
QF_NonLinearIntArith	Yices2	0.013582
QF_NonLinearRealArith	Yices2	0.00764
QF_LinearRealArith	Z3-Parti-Z3pp	0.007461
QF_Equality_Bitvec	Yices2	0.006813
QF_LinearIntArith	Yices2	0.002215
QF_Equality_LinearArith	SMTS	0.001585
QF_Bitvec	Bitwuzla-32core	0
QF_Bitvec	Bitwuzla-64core	0
QF_Bitvec	STP-Parti-Bitwuzla-16core	0
QF_Bitvec	STP-Parti-Bitwuzla-32core	0
QF_Bitvec	STP-Parti-Bitwuzla-64core	0
QF_Equality_Bitvec	Bitwuzla-32core	0
QF_Equality_Bitvec	Bitwuzla-64core	0
QF_LinearRealArith	SMTS (32 cores)	0
QF_LinearRealArith	SMTS (64 cores)	0
QF_LinearRealArith	Z3-Parti-Z3pp-16core	0
QF_LinearRealArith	Z3-Parti-Z3pp-32core	0
QF_LinearRealArith	Z3-Parti-Z3pp-64core	0
QF_NonLinearIntArith	Z3-Parti-Z3pp-16core	0
QF_NonLinearIntArith	Z3-Parti-Z3pp-32core	0
QF_NonLinearIntArith	Z3-Parti-Z3pp-64core	0
QF_NonLinearRealArith	Z3-Parti-Z3pp-16core	0
QF_NonLinearRealArith	Z3-Parti-Z3pp-32core	0
QF_NonLinearRealArith	Z3-Parti-Z3pp-64core	0
QF_Equality_LinearArith	SMTS (32 cores)	0
QF_Equality_LinearArith	SMTS (64 cores)	0
QF_LinearIntArith	SMTS (32 cores)	0
QF_LinearIntArith	SMTS (64 cores)	0
QF_LinearIntArith	Z3-Parti-Z3pp-16core	0
QF_LinearIntArith	Z3-Parti-Z3pp-32core	0
QF_LinearIntArith	Z3-Parti-Z3pp-64core	0

UNSAT Performance

Division	Solver	Contribution
QF_Bitvec	STP-Parti-Bitwuzla	0.154017
QF_Bitvec	Bitwuzla	0.132801
QF_Equality_LinearArith	SMTS	0.066975
QF_NonLinearIntArith	Z3-Parti-Z3pp	0.054329
QF_LinearRealArith	SMTS	0.037769
QF_Equality_Bitvec	Yices2	0.03709
QF_NonLinearIntArith	Yices2	0.03056
QF_LinearIntArith	Z3-Parti-Z3pp	0.029779
QF_Equality_Bitvec	Bitwuzla	0.02725
QF_NonLinearRealArith	Z3-Parti-Z3pp	0.013582
QF_NonLinearRealArith	Yices2	0.013582
QF_LinearIntArith	SMTS	0.00886
QF_LinearRealArith	Z3-Parti-Z3pp	0.007461
QF_LinearRealArith	Yices2	0.007461
QF_Equality_LinearArith	Yices2	0.003567
QF_LinearIntArith	Yices2	0.000246
QF_Bitvec	Bitwuzla-32core	0
QF_Bitvec	Bitwuzla-64core	0
QF_Bitvec	STP-Parti-Bitwuzla-16core	0
QF_Bitvec	STP-Parti-Bitwuzla-32core	0
QF_Bitvec	STP-Parti-Bitwuzla-64core	0
QF_Equality_Bitvec	Bitwuzla-32core	0
QF_Equality_Bitvec	Bitwuzla-64core	0
QF_LinearRealArith	SMTS (32 cores)	0
QF_LinearRealArith	SMTS (64 cores)	0
QF_LinearRealArith	Z3-Parti-Z3pp-16core	0
QF_LinearRealArith	Z3-Parti-Z3pp-32core	0
QF_LinearRealArith	Z3-Parti-Z3pp-64core	0
QF_NonLinearIntArith	Z3-Parti-Z3pp-16core	0
QF_NonLinearIntArith	Z3-Parti-Z3pp-32core	0
QF_NonLinearIntArith	Z3-Parti-Z3pp-64core	0
QF_NonLinearRealArith	Z3-Parti-Z3pp-16core	0
QF_NonLinearRealArith	Z3-Parti-Z3pp-32core	0
QF_NonLinearRealArith	Z3-Parti-Z3pp-64core	0
QF_Equality_LinearArith	SMTS (32 cores)	0
QF_Equality_LinearArith	SMTS (64 cores)	0
QF_LinearIntArith	SMTS (32 cores)	0
QF_LinearIntArith	SMTS (64 cores)	0
QF_LinearIntArith	Z3-Parti-Z3pp-16core	0
QF_LinearIntArith	Z3-Parti-Z3pp-32core	0
QF_LinearIntArith	Z3-Parti-Z3pp-64core	0

24 seconds Performance

Division	Solver	Contribution
QF_NonLinearIntArith	Z3-Parti-Z3pp	0.06876
QF_NonLinearRealArith	Yices2	0.03056
QF_NonLinearRealArith	Z3-Parti-Z3pp	0.021222
QF_Bitvec	Bitwuzla	0.012573
QF_Equality_Bitvec	Bitwuzla	0.012111
QF_LinearIntArith	SMTS	0.006153
QF_NonLinearIntArith	Yices2	0.003396
QF_Bitvec	STP-Parti-Bitwuzla	0.003143
QF_LinearIntArith	Z3-Parti-Z3pp	0.000984
QF_Equality_Bitvec	Yices2	0.000757
QF_LinearRealArith	SMTS	0.000466
QF_Equality_LinearArith	Yices2	0.000396
QF_Bitvec	Bitwuzla-32core	0
QF_Bitvec	Bitwuzla-64core	0
QF_Bitvec	STP-Parti-Bitwuzla-16core	0
QF_Bitvec	STP-Parti-Bitwuzla-32core	0
QF_Bitvec	STP-Parti-Bitwuzla-64core	0
QF_Equality_Bitvec	Bitwuzla-32core	0
QF_Equality_Bitvec	Bitwuzla-64core	0
QF_LinearRealArith	SMTS (32 cores)	0
QF_LinearRealArith	SMTS (64 cores)	0
QF_LinearRealArith	Z3-Parti-Z3pp-16core	0
QF_LinearRealArith	Z3-Parti-Z3pp-32core	0
QF_LinearRealArith	Z3-Parti-Z3pp-64core	0
QF_NonLinearIntArith	Z3-Parti-Z3pp-16core	0
QF_NonLinearIntArith	Z3-Parti-Z3pp-32core	0
QF_NonLinearIntArith	Z3-Parti-Z3pp-64core	0
QF_NonLinearRealArith	Z3-Parti-Z3pp-16core	0
QF_NonLinearRealArith	Z3-Parti-Z3pp-32core	0
QF_NonLinearRealArith	Z3-Parti-Z3pp-64core	0
QF_Equality_LinearArith	SMTS (32 cores)	0
QF_Equality_LinearArith	SMTS (64 cores)	0
QF_LinearIntArith	SMTS (32 cores)	0
QF_LinearIntArith	SMTS (64 cores)	0
QF_LinearIntArith	Z3-Parti-Z3pp-16core	0
QF_LinearIntArith	Z3-Parti-Z3pp-32core	0
QF_LinearIntArith	Z3-Parti-Z3pp-64core	0