SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

Best Overall Ranking - Model Validation Track

Page generated on 2025-08-11

Winners

Sequential Performance Parallel Performance SAT Performance (parallel) UNSAT Performance (parallel) 24 seconds Performance (parallel)
cvc5 (31.577255) cvc5 (31.577255) cvc5 (31.577255) — cvc5 (25.834537)

Sequential Performance

Division Solver Contribution
QF_FPArith cvc5 4.381439
QF_FPArith Bitwuzla 4.377482
QF_Bitvec Bitwuzla 3.871608
QF_Bitvec Yices2 3.829056
QF_Bitvec cvc5 3.761461
QF_ADT_BitVec Bitwuzla 3.687547
QF_LinearIntArith OpenSMT 3.234384
QF_Equality SMTInterpol 3.196176
QF_Equality cvc5 3.196176
QF_Equality OpenSMT 3.196176
QF_Equality Yices2 3.192109
QF_LinearIntArith Yices2 3.165592
QF_ADT_BitVec cvc5 3.073389
QF_NonLinearIntArith Yices2 3.05528
QF_Datatypes SMTInterpol 2.933059
QF_ADT_LinArith SMTInterpol 2.880141
QF_Equality_LinearArith OpenSMT 2.844885
QF_ADT_LinArith cvc5 2.798545
QF_Equality_LinearArith SMTInterpol 2.767389
QF_Equality_LinearArith cvc5 2.729042
QF_NonLinearIntArith cvc5 2.655395
QF_Equality_Bitvec Yices2 2.6542
QF_Equality_Bitvec Bitwuzla 2.6542
QF_LinearRealArith Yices2 2.646431
QF_LinearRealArith OpenSMT 2.637483
QF_LinearIntArith SMTInterpol 2.58352
QF_Equality_LinearArith Yices2 2.516797
QF_LinearRealArith SMTInterpol 2.275342
QF_LinearIntArith cvc5 2.241202
QF_ADT_BitVec SMTInterpol 2.038939
QF_NonLinearRealArith SMT-RAT 1.95052
QF_NonLinearRealArith cvc5 1.816643
QF_LinearRealArith cvc5 1.680844
QF_Datatypes cvc5 1.506261
QF_Equality_NonLinearArith cvc5 1.46993
QF_Equality_Bitvec SMTInterpol 1.162252
QF_Equality_NonLinearArith SMTInterpol 0.936751
QF_Bitvec SMTInterpol 0.873149
QF_Equality_Bitvec cvc5 0.266928
QF_NonLinearRealArith SMTInterpol 7.5e-05
QF_NonLinearIntArith SMTInterpol 0
QF_Equality_NonLinearArith Yices2 -5.353387
QF_NonLinearRealArith Yices2 -6.887152

Parallel Performance

Division Solver Contribution
QF_FPArith cvc5 4.381439
QF_FPArith Bitwuzla 4.377482
QF_Bitvec Bitwuzla 3.871608
QF_Bitvec Yices2 3.829056
QF_Bitvec cvc5 3.761461
QF_ADT_BitVec Bitwuzla 3.687547
QF_LinearIntArith OpenSMT 3.234384
QF_Equality SMTInterpol 3.196176
QF_Equality cvc5 3.196176
QF_Equality OpenSMT 3.196176
QF_Equality Yices2 3.192109
QF_LinearIntArith Yices2 3.165592
QF_ADT_BitVec cvc5 3.073389
QF_NonLinearIntArith Yices2 3.05528
QF_Datatypes SMTInterpol 2.933059
QF_ADT_LinArith SMTInterpol 2.880141
QF_Equality_LinearArith OpenSMT 2.844885
QF_ADT_LinArith cvc5 2.798545
QF_Equality_LinearArith SMTInterpol 2.767389
QF_Equality_LinearArith cvc5 2.729042
QF_NonLinearIntArith cvc5 2.655395
QF_Equality_Bitvec Yices2 2.6542
QF_Equality_Bitvec Bitwuzla 2.6542
QF_LinearRealArith Yices2 2.646431
QF_LinearRealArith OpenSMT 2.637483
QF_LinearIntArith SMTInterpol 2.586043
QF_Equality_LinearArith Yices2 2.516797
QF_LinearRealArith SMTInterpol 2.275342
QF_LinearIntArith cvc5 2.241202
QF_ADT_BitVec SMTInterpol 2.051551
QF_NonLinearRealArith SMT-RAT 1.95052
QF_NonLinearRealArith cvc5 1.816643
QF_LinearRealArith cvc5 1.680844
QF_Datatypes cvc5 1.506261
QF_Equality_NonLinearArith cvc5 1.46993
QF_Equality_Bitvec SMTInterpol 1.162252
QF_Equality_NonLinearArith SMTInterpol 0.936751
QF_Bitvec SMTInterpol 0.877206
QF_Equality_Bitvec cvc5 0.266928
QF_NonLinearRealArith SMTInterpol 7.5e-05
QF_NonLinearIntArith SMTInterpol 0
QF_Equality_NonLinearArith Yices2 -5.353387
QF_NonLinearRealArith Yices2 -6.887152

SAT Performance

Division Solver Contribution
QF_FPArith cvc5 4.381439
QF_FPArith Bitwuzla 4.377482
QF_Bitvec Bitwuzla 3.871608
QF_Bitvec Yices2 3.829056
QF_Bitvec cvc5 3.761461
QF_ADT_BitVec Bitwuzla 3.687547
QF_LinearIntArith OpenSMT 3.234384
QF_Equality SMTInterpol 3.196176
QF_Equality cvc5 3.196176
QF_Equality OpenSMT 3.196176
QF_Equality Yices2 3.192109
QF_LinearIntArith Yices2 3.165592
QF_ADT_BitVec cvc5 3.073389
QF_NonLinearIntArith Yices2 3.05528
QF_Datatypes SMTInterpol 2.933059
QF_ADT_LinArith SMTInterpol 2.880141
QF_Equality_LinearArith OpenSMT 2.844885
QF_ADT_LinArith cvc5 2.798545
QF_Equality_LinearArith SMTInterpol 2.767389
QF_Equality_LinearArith cvc5 2.729042
QF_NonLinearIntArith cvc5 2.655395
QF_Equality_Bitvec Yices2 2.6542
QF_Equality_Bitvec Bitwuzla 2.6542
QF_LinearRealArith Yices2 2.646431
QF_LinearRealArith OpenSMT 2.637483
QF_LinearIntArith SMTInterpol 2.586043
QF_Equality_LinearArith Yices2 2.516797
QF_LinearRealArith SMTInterpol 2.275342
QF_LinearIntArith cvc5 2.241202
QF_ADT_BitVec SMTInterpol 2.051551
QF_NonLinearRealArith SMT-RAT 1.95052
QF_NonLinearRealArith cvc5 1.816643
QF_LinearRealArith cvc5 1.680844
QF_Datatypes cvc5 1.506261
QF_Equality_NonLinearArith cvc5 1.46993
QF_Equality_Bitvec SMTInterpol 1.162252
QF_Equality_NonLinearArith SMTInterpol 0.936751
QF_Bitvec SMTInterpol 0.877206
QF_Equality_Bitvec cvc5 0.266928
QF_NonLinearRealArith SMTInterpol 7.5e-05
QF_NonLinearIntArith SMTInterpol 0
QF_Equality_NonLinearArith Yices2 -5.353387
QF_NonLinearRealArith Yices2 -6.887152

24 seconds Performance

Division Solver Contribution
QF_FPArith Bitwuzla 4.369573
QF_FPArith cvc5 4.359518
QF_Bitvec Bitwuzla 3.710231
QF_ADT_BitVec Bitwuzla 3.656565
QF_Bitvec Yices2 3.476403
QF_Equality SMTInterpol 3.196176
QF_Equality cvc5 3.196176
QF_Equality OpenSMT 3.196176
QF_Equality Yices2 3.192109
QF_Bitvec cvc5 3.069453
QF_LinearIntArith Yices2 2.857875
QF_Datatypes SMTInterpol 2.844232
QF_NonLinearIntArith Yices2 2.797245
QF_ADT_LinArith SMTInterpol 2.776494
QF_Equality_LinearArith SMTInterpol 2.590726
QF_ADT_LinArith cvc5 2.581967
QF_Equality_LinearArith OpenSMT 2.522917
QF_ADT_BitVec cvc5 2.404494
QF_Equality_LinearArith Yices2 2.289749
QF_Equality_LinearArith cvc5 2.249095
QF_LinearRealArith Yices2 2.160569
QF_LinearRealArith OpenSMT 2.033036
QF_LinearIntArith OpenSMT 2.019059
QF_NonLinearRealArith SMT-RAT 1.829275
QF_NonLinearRealArith cvc5 1.78615
QF_LinearIntArith SMTInterpol 1.779075
QF_Equality_Bitvec Yices2 1.722112
QF_LinearIntArith cvc5 1.697337
QF_Equality_Bitvec Bitwuzla 1.58051
QF_LinearRealArith cvc5 1.520693
QF_LinearRealArith SMTInterpol 1.433719
QF_Datatypes cvc5 1.298614
QF_ADT_BitVec SMTInterpol 1.093625
QF_Equality_NonLinearArith cvc5 0.871265
QF_Equality_Bitvec SMTInterpol 0.622132
QF_NonLinearIntArith cvc5 0.593067
QF_Bitvec SMTInterpol 0.581227
QF_Equality_NonLinearArith SMTInterpol 0.518208
QF_Equality_Bitvec cvc5 0.206709
QF_NonLinearRealArith SMTInterpol 2.2e-05
QF_NonLinearIntArith SMTInterpol 0
QF_Equality_NonLinearArith Yices2 -5.353387
QF_NonLinearRealArith Yices2 -6.887152