SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

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_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_Equality_Bitvec Bitwuzla-32core 0
QF_Equality_Bitvec Bitwuzla-64core 0
QF_NonLinearIntArith Z3-Parti-Z3pp-16core 0
QF_NonLinearIntArith Z3-Parti-Z3pp-32core 0
QF_NonLinearIntArith 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
QF_NonLinearRealArith Z3-Parti-Z3pp-16core 0
QF_NonLinearRealArith Z3-Parti-Z3pp-32core 0
QF_NonLinearRealArith 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_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_Equality_Bitvec Bitwuzla-32core 0
QF_Equality_Bitvec Bitwuzla-64core 0
QF_NonLinearIntArith Z3-Parti-Z3pp-16core 0
QF_NonLinearIntArith Z3-Parti-Z3pp-32core 0
QF_NonLinearIntArith 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
QF_NonLinearRealArith Z3-Parti-Z3pp-16core 0
QF_NonLinearRealArith Z3-Parti-Z3pp-32core 0
QF_NonLinearRealArith 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_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_Equality_Bitvec Bitwuzla-32core 0
QF_Equality_Bitvec Bitwuzla-64core 0
QF_NonLinearIntArith Z3-Parti-Z3pp-16core 0
QF_NonLinearIntArith Z3-Parti-Z3pp-32core 0
QF_NonLinearIntArith 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
QF_NonLinearRealArith Z3-Parti-Z3pp-16core 0
QF_NonLinearRealArith Z3-Parti-Z3pp-32core 0
QF_NonLinearRealArith 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_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_Equality_Bitvec Bitwuzla-32core 0
QF_Equality_Bitvec Bitwuzla-64core 0
QF_NonLinearIntArith Z3-Parti-Z3pp-16core 0
QF_NonLinearIntArith Z3-Parti-Z3pp-32core 0
QF_NonLinearIntArith 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
QF_NonLinearRealArith Z3-Parti-Z3pp-16core 0
QF_NonLinearRealArith Z3-Parti-Z3pp-32core 0
QF_NonLinearRealArith Z3-Parti-Z3pp-64core 0