SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

Largest Contribution Ranking - Model Validation Track

Page generated on 2025-08-11

Winners

Winners

Sequential Performance Parallel Performance SAT Performance (parallel) UNSAT Performance (parallel) 24 seconds Performance (parallel)
Yices2 Yices2 Yices2 - Yices2

Sequential Performance

Division Solver Correct Score Time Score
QF_NonLinearIntArith Yices2 0.010645 0.07692
QF_ADT_BitVec Bitwuzla 0.005676 0.093672
QF_NonLinearIntArith cvc5 0.00489 -0.376271
QF_NonLinearRealArith SMT-RAT 0.001619 0.012491
QF_LinearIntArith OpenSMT 0.001442 0.011649
QF_LinearIntArith Yices2 0.00102 0.073495
QF_LinearIntArith SMTInterpol 0.000821 -0.009001
QF_LinearIntArith cvc5 0.000746 0.029471
QF_NonLinearRealArith cvc5 0.000723 0.019901
QF_Bitvec Bitwuzla 0.000457 0.074115
QF_Equality_LinearArith OpenSMT 0.000402 0.013239
QF_Bitvec Yices2 0.000168 0.039288
QF_Equality_LinearArith SMTInterpol 0.000134 0.007096
QF_ADT_BitVec cvc5 5.5e-05 0.028876
QF_LinearRealArith Yices2 5.1e-05 0.008336
QF_LinearRealArith OpenSMT 5.1e-05 0.005579
QF_Equality_Bitvec Bitwuzla 4.1e-05 0.006252
QF_NonLinearRealArith SMTInterpol 2.7e-05 -0.002319
QF_LinearRealArith SMTInterpol 2.6e-05 6.8e-05

Parallel Performance

Division Solver Correct Score Time Score
QF_NonLinearIntArith Yices2 0.010645 0.076878
QF_ADT_BitVec Bitwuzla 0.005657 0.093065
QF_NonLinearIntArith cvc5 0.00489 -0.369607
QF_NonLinearRealArith SMT-RAT 0.001619 0.012394
QF_LinearIntArith OpenSMT 0.001442 0.011463
QF_LinearIntArith Yices2 0.00102 0.069615
QF_LinearIntArith SMTInterpol 0.000821 -0.006172
QF_LinearIntArith cvc5 0.000746 0.029469
QF_NonLinearRealArith cvc5 0.000723 0.019832
QF_Bitvec Bitwuzla 0.000457 0.072539
QF_Equality_LinearArith OpenSMT 0.000402 0.01316
QF_Bitvec Yices2 0.000168 0.038192
QF_Equality_LinearArith SMTInterpol 0.000134 0.008104
QF_ADT_BitVec cvc5 5.5e-05 0.024148
QF_LinearRealArith Yices2 5.1e-05 0.008231
QF_LinearRealArith OpenSMT 5.1e-05 0.005451
QF_Equality_Bitvec Bitwuzla 4.1e-05 0.006306
QF_NonLinearRealArith SMTInterpol 2.7e-05 -0.001488
QF_LinearRealArith SMTInterpol 2.6e-05 0.000224

SAT Performance

Division Solver Correct Score Time Score
QF_NonLinearIntArith Yices2 0.010645 0.076878
QF_ADT_BitVec Bitwuzla 0.005657 0.093065
QF_NonLinearIntArith cvc5 0.00489 -0.369607
QF_NonLinearRealArith SMT-RAT 0.001619 0.012394
QF_LinearIntArith OpenSMT 0.001442 0.011463
QF_LinearIntArith Yices2 0.00102 0.069615
QF_LinearIntArith SMTInterpol 0.000821 -0.006172
QF_LinearIntArith cvc5 0.000746 0.029469
QF_NonLinearRealArith cvc5 0.000723 0.019832
QF_Bitvec Bitwuzla 0.000457 0.072539
QF_Equality_LinearArith OpenSMT 0.000402 0.01316
QF_Bitvec Yices2 0.000168 0.038192
QF_Equality_LinearArith SMTInterpol 0.000134 0.008104
QF_ADT_BitVec cvc5 5.5e-05 0.024148
QF_LinearRealArith Yices2 5.1e-05 0.008231
QF_LinearRealArith OpenSMT 5.1e-05 0.005451
QF_Equality_Bitvec Bitwuzla 4.1e-05 0.006306
QF_NonLinearRealArith SMTInterpol 2.7e-05 -0.001488
QF_LinearRealArith SMTInterpol 2.6e-05 0.000224

24 seconds Performance

Division Solver Correct Score Time Score
QF_NonLinearIntArith Yices2 0.049027 -0.059794
QF_ADT_BitVec Bitwuzla 0.018028 0.066877
QF_LinearIntArith Yices2 0.01427 0.042706
QF_Bitvec Bitwuzla 0.004886 0.020794
QF_LinearIntArith cvc5 0.002227 -0.00205
QF_NonLinearRealArith SMT-RAT 0.001738 -0.002897
QF_LinearIntArith OpenSMT 0.001632 -0.004751
QF_NonLinearRealArith cvc5 0.001428 0.000542
QF_NonLinearIntArith cvc5 0.001167 0.006425
QF_Equality_Bitvec Bitwuzla 0.000855 -0.0022
QF_Bitvec Yices2 0.000831 0.049541
QF_Equality_Bitvec Yices2 0.000624 0.000167
QF_LinearRealArith Yices2 0.000474 0.004921
QF_LinearIntArith SMTInterpol 0.000466 -0.003219
QF_Equality_LinearArith SMTInterpol 0.000417 -0.002471
QF_Bitvec cvc5 0.000391 -9.7e-05
QF_LinearRealArith OpenSMT 0.000362 -0.002374
QF_Equality_LinearArith OpenSMT 0.000361 -0.001531
QF_ADT_BitVec cvc5 0.00013 -0.001637