SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

Biggest Lead Ranking - Unsat Core Track

Page generated on 2025-08-11

Winners

Winners

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

Sequential Performance

Division Solver Correct Score Time Score
Arith cvc5 33.375 0.001466
QF_NonLinearRealArith Yices2 10.87564 0.001603
QF_Datatypes cvc5 9.150435 0.333423
QF_Equality_LinearArith Yices2 4.493513 0.227272
Bitvec cvc5 3.25 0.115493
Equality_NonLinearArith cvc5 2.076565 0.180614
Equality cvc5 1.732514 3.405705
Equality_LinearArith cvc5 1.618371 1.872232
Equality_MachineArith cvc5 1.280037 1.127433
QF_Equality_NonLinearArith cvc5 1.210954 0.761002
QF_Bitvec Bitwuzla 1.201764 0.508413
QF_Equality Yices2 1.179017 8.192068
QF_LinearIntArith Yices2 1.107069 1.675866
QF_NonLinearIntArith Yices2 1.106406 3.344723
QF_Equality_Bitvec Bitwuzla 1.089137 4.925647
FPArith Bitwuzla 1.04 6.025612
QF_LinearRealArith OpenSMT 1.032308 2.428354
QF_FPArith Bitwuzla 1.03163 2.122405

Parallel Performance

Division Solver Correct Score Time Score
Arith cvc5 33.375 0.001266
QF_NonLinearRealArith Yices2 10.87564 0.000647
QF_Datatypes cvc5 9.150435 0.177871
QF_Equality_LinearArith Yices2 4.493513 0.229122
Bitvec cvc5 3.25 0.117468
Equality_NonLinearArith cvc5 2.076565 0.122326
Equality cvc5 1.731106 2.704698
Equality_LinearArith cvc5 1.616864 1.512142
Equality_MachineArith cvc5 1.280037 0.820552
QF_Equality_NonLinearArith cvc5 1.210954 0.623924
QF_Bitvec Bitwuzla 1.201764 0.510576
QF_Equality Yices2 1.179017 3.333792
QF_LinearIntArith Yices2 1.107069 1.422869
QF_NonLinearIntArith Yices2 1.106406 3.320464
QF_Equality_Bitvec Bitwuzla 1.089137 4.860473
FPArith Bitwuzla 1.04 4.855741
QF_LinearRealArith OpenSMT 1.032308 2.423808
QF_FPArith Bitwuzla 1.03163 1.944569

UNSAT Performance

Division Solver Correct Score Time Score
Arith cvc5 33.375 0.001266
QF_NonLinearRealArith Yices2 10.87564 0.000647
QF_Datatypes cvc5 9.150435 0.177871
QF_Equality_LinearArith Yices2 4.493513 0.229122
Bitvec cvc5 3.25 0.117468
Equality_NonLinearArith cvc5 2.076565 0.122326
Equality cvc5 1.731106 2.704698
Equality_LinearArith cvc5 1.616864 1.512142
Equality_MachineArith cvc5 1.280037 0.820552
QF_Equality_NonLinearArith cvc5 1.210954 0.623924
QF_Bitvec Bitwuzla 1.201764 0.510576
QF_Equality Yices2 1.179017 3.333792
QF_LinearIntArith Yices2 1.107069 1.422869
QF_NonLinearIntArith Yices2 1.106406 3.320464
QF_Equality_Bitvec Bitwuzla 1.089137 4.860473
FPArith Bitwuzla 1.04 4.855741
QF_LinearRealArith OpenSMT 1.032308 2.423808
QF_FPArith Bitwuzla 1.03163 1.944569

24 seconds Performance

Division Solver Correct Score Time Score
Arith cvc5 15.375 0.172157
QF_Datatypes SMTInterpol 4.667961 0.865089
QF_Equality_LinearArith Yices2 3.981314 1.349514
QF_NonLinearRealArith Yices2 3.569858 0.008459
Bitvec cvc5 2.35 0.301727
QF_LinearIntArith Yices2 1.981649 1.232029
Equality cvc5 1.904338 2.901647
Equality_LinearArith cvc5 1.597744 2.005157
Equality_NonLinearArith cvc5 1.592545 1.600613
Equality_MachineArith cvc5 1.316041 3.245535
QF_NonLinearIntArith Yices2 1.268892 1.268057
QF_Equality Yices2 1.211404 7.070112
QF_Equality_Bitvec Bitwuzla 1.114902 0.478257
QF_LinearRealArith Yices2 1.077908 1.53046
QF_FPArith Bitwuzla 1.043047 1.019561
FPArith Bitwuzla 1.04 4.855741
QF_Equality_NonLinearArith Yices2 1.032575 1.277959
QF_Bitvec Bitwuzla 1.010423 0.536561