SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

Biggest Lead Ranking - Parallel Track

Page generated on 2025-08-11

Winners

Winners

Sequential Performance Parallel Performance SAT Performance (parallel) UNSAT Performance (parallel) 24 seconds Performance (parallel)
- Z3-Parti-Z3pp Z3-Parti-Z3pp SMTS Z3-Parti-Z3pp

Parallel Performance

Division Solver Correct Score Time Score
QF_NonLinearRealArith Z3-Parti-Z3pp 2.125 0.01221
QF_NonLinearIntArith Z3-Parti-Z3pp 2 0.479565
QF_LinearRealArith SMTS 1.642857 1.013739
QF_Equality_LinearArith SMTS 1.454545 0.723263
QF_Bitvec STP-Parti-Bitwuzla 1.272727 0.522612
QF_LinearIntArith SMTS 1.208333 1.464977
QF_Equality_Bitvec Bitwuzla 1.090909 1.328785

SAT Performance

Division Solver Correct Score Time Score
QF_NonLinearRealArith Z3-Parti-Z3pp 3.25 0.004461
QF_NonLinearIntArith Z3-Parti-Z3pp 2.8 0.296723
QF_Equality_LinearArith Yices2 2.666667 0.086862
QF_LinearIntArith SMTS 1.769231 0.59306
QF_Bitvec STP-Parti-Bitwuzla 1.555556 0.398285
QF_Equality_Bitvec Bitwuzla 1.5 0.250215
QF_LinearRealArith SMTS 1.4 1.158349

UNSAT Performance

Division Solver Correct Score Time Score
QF_Equality_LinearArith SMTS 3.5 0.151856
QF_LinearRealArith SMTS 2 0.70265
QF_LinearIntArith Z3-Parti-Z3pp 1.714286 0.306078
QF_NonLinearIntArith Z3-Parti-Z3pp 1.285714 0.858253
QF_Equality_Bitvec Yices2 1.142857 0.280482
QF_Bitvec STP-Parti-Bitwuzla 1.071429 0.758541
QF_NonLinearRealArith Yices2 1 39.560568

24 seconds Performance

Division Solver Correct Score Time Score
QF_NonLinearIntArith Z3-Parti-Z3pp 3.333333 0.356843
QF_Equality_Bitvec Bitwuzla 2.5 0.159304
QF_LinearIntArith SMTS 2 0.677416
QF_LinearRealArith SMTS 2 0.052302
QF_Equality_LinearArith Yices2 2 0.042071
QF_Bitvec Bitwuzla 1.666667 0.393272
QF_NonLinearRealArith Yices2 1.166667 1.136855