SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

Best Overall Ranking - Unsat Core Track

Page generated on 2025-08-11

Winners

Sequential Performance Parallel Performance SAT Performance (parallel) UNSAT Performance (parallel) 24 seconds Performance (parallel)
cvc5 (27.384714) cvc5 (27.384714) — cvc5 (27.384714) cvc5 (16.674862)

Sequential Performance

Division Solver Contribution
Equality cvc5 5.575957
Equality_LinearArith cvc5 4.722485
QF_LinearRealArith OpenSMT 4.458065
QF_NonLinearRealArith Yices2 4.452778
QF_LinearRealArith OpenSMT (min-ucore) 4.183382
QF_LinearRealArith Yices2 4.102475
QF_Bitvec Bitwuzla 3.902645
QF_Equality_NonLinearArith cvc5 3.888269
QF_LinearRealArith cvc5 3.168337
QF_Equality_LinearArith Yices2 2.847879
QF_Bitvec Yices2 2.702219
QF_Equality_NonLinearArith SMTInterpol 2.651546
QF_LinearIntArith Yices2 2.44221
QF_NonLinearIntArith Yices2 2.125728
Equality_MachineArith cvc5 2.027032
QF_Equality_NonLinearArith Yices2 2.016195
QF_LinearIntArith SMTInterpol 1.992663
QF_Equality_Bitvec Bitwuzla 1.980202
QF_Equality Yices2 1.9333
Equality SMTInterpol 1.857655
Equality_LinearArith SMTInterpol 1.803076
QF_NonLinearIntArith cvc5 1.736503
QF_Equality_Bitvec Yices2 1.669337
QF_Equality SMTInterpol 1.39078
QF_Equality_Bitvec SMTInterpol 1.333546
QF_Equality cvc5 1.27828
Equality_MachineArith SMTInterpol 1.237129
QF_Bitvec cvc5 1.035971
QF_LinearIntArith cvc5 0.912855
FPArith Bitwuzla 0.790855
QF_FPArith Bitwuzla 0.776961
QF_LinearRealArith SMTInterpol 0.756944
QF_FPArith cvc5 0.730047
FPArith cvc5 0.730044
Equality_NonLinearArith cvc5 0.549281
QF_Datatypes cvc5 0.369597
QF_Bitvec SMTInterpol 0.339973
QF_Equality_Bitvec cvc5 0.325368
Arith cvc5 0.147619
QF_Equality_LinearArith cvc5 0.141041
Equality_NonLinearArith SMTInterpol 0.12738
QF_Equality_LinearArith SMTInterpol 0.068812
QF_NonLinearRealArith SMTInterpol 0.037642
QF_NonLinearRealArith cvc5 0.026467
Bitvec cvc5 0.019563
QF_Datatypes SMTInterpol 0.004414
Bitvec Bitwuzla 0.001724
QF_NonLinearIntArith SMTInterpol 0.000453
Arith SMTInterpol 0.000102
Equality_NonLinearArith UltimateEliminator+MathSAT 1e-06
Equality_MachineArith Bitwuzla 0
Bitvec SMTInterpol 0
Bitvec UltimateEliminator+MathSAT 0
FPArith UltimateEliminator+MathSAT 0
Equality_MachineArith UltimateEliminator+MathSAT 0
Equality UltimateEliminator+MathSAT 0
Arith UltimateEliminator+MathSAT -6.169867
QF_Equality OpenSMT (min-ucore) -11.490987
QF_Equality OpenSMT -11.490987
QF_Equality_LinearArith OpenSMT -12.268565
QF_Equality_LinearArith OpenSMT (min-ucore) -12.268565
Equality_LinearArith UltimateEliminator+MathSAT -12.655907
QF_LinearIntArith OpenSMT -13.551086
QF_LinearIntArith OpenSMT (min-ucore) -13.551086

Parallel Performance

Division Solver Contribution
Equality cvc5 5.575957
Equality_LinearArith cvc5 4.722485
QF_LinearRealArith OpenSMT 4.458065
QF_NonLinearRealArith Yices2 4.452778
QF_LinearRealArith OpenSMT (min-ucore) 4.183382
QF_LinearRealArith Yices2 4.102475
QF_Bitvec Bitwuzla 3.902645
QF_Equality_NonLinearArith cvc5 3.888269
QF_LinearRealArith cvc5 3.168337
QF_Equality_LinearArith Yices2 2.847879
QF_Bitvec Yices2 2.702219
QF_Equality_NonLinearArith SMTInterpol 2.651546
QF_LinearIntArith Yices2 2.44221
QF_NonLinearIntArith Yices2 2.125728
Equality_MachineArith cvc5 2.027032
QF_Equality_NonLinearArith Yices2 2.016195
QF_LinearIntArith SMTInterpol 1.992663
QF_Equality_Bitvec Bitwuzla 1.980202
QF_Equality Yices2 1.9333
Equality SMTInterpol 1.860678
Equality_LinearArith SMTInterpol 1.80644
QF_NonLinearIntArith cvc5 1.736503
QF_Equality_Bitvec Yices2 1.669337
QF_Equality SMTInterpol 1.39078
QF_Equality_Bitvec SMTInterpol 1.333546
QF_Equality cvc5 1.27828
Equality_MachineArith SMTInterpol 1.237129
QF_Bitvec cvc5 1.035971
QF_LinearIntArith cvc5 0.912855
FPArith Bitwuzla 0.790855
QF_FPArith Bitwuzla 0.776961
QF_LinearRealArith SMTInterpol 0.760784
QF_FPArith cvc5 0.730047
FPArith cvc5 0.730044
Equality_NonLinearArith cvc5 0.549281
QF_Datatypes cvc5 0.369597
QF_Bitvec SMTInterpol 0.341689
QF_Equality_Bitvec cvc5 0.325368
Arith cvc5 0.147619
QF_Equality_LinearArith cvc5 0.141041
Equality_NonLinearArith SMTInterpol 0.12738
QF_Equality_LinearArith SMTInterpol 0.068812
QF_NonLinearRealArith SMTInterpol 0.037642
QF_NonLinearRealArith cvc5 0.026467
Bitvec cvc5 0.019563
QF_Datatypes SMTInterpol 0.004414
Bitvec Bitwuzla 0.001724
QF_NonLinearIntArith SMTInterpol 0.000453
Arith SMTInterpol 0.000102
Equality_NonLinearArith UltimateEliminator+MathSAT 1e-06
Equality_MachineArith Bitwuzla 0
Bitvec SMTInterpol 0
Bitvec UltimateEliminator+MathSAT 0
FPArith UltimateEliminator+MathSAT 0
Equality_MachineArith UltimateEliminator+MathSAT 0
Equality UltimateEliminator+MathSAT 0
Arith UltimateEliminator+MathSAT -6.169867
QF_Equality OpenSMT (min-ucore) -11.490987
QF_Equality OpenSMT -11.490987
QF_Equality_LinearArith OpenSMT -12.268565
QF_Equality_LinearArith OpenSMT (min-ucore) -12.268565
Equality_LinearArith UltimateEliminator+MathSAT -12.655907
QF_LinearIntArith OpenSMT -13.551086
QF_LinearIntArith OpenSMT (min-ucore) -13.551086

UNSAT Performance

Division Solver Contribution
Equality cvc5 5.575957
Equality_LinearArith cvc5 4.722485
QF_LinearRealArith OpenSMT 4.458065
QF_NonLinearRealArith Yices2 4.452778
QF_LinearRealArith OpenSMT (min-ucore) 4.183382
QF_LinearRealArith Yices2 4.102475
QF_Bitvec Bitwuzla 3.902645
QF_Equality_NonLinearArith cvc5 3.888269
QF_LinearRealArith cvc5 3.168337
QF_Equality_LinearArith Yices2 2.847879
QF_Bitvec Yices2 2.702219
QF_Equality_NonLinearArith SMTInterpol 2.651546
QF_LinearIntArith Yices2 2.44221
QF_NonLinearIntArith Yices2 2.125728
Equality_MachineArith cvc5 2.027032
QF_Equality_NonLinearArith Yices2 2.016195
QF_LinearIntArith SMTInterpol 1.992663
QF_Equality_Bitvec Bitwuzla 1.980202
QF_Equality Yices2 1.9333
Equality SMTInterpol 1.860678
Equality_LinearArith SMTInterpol 1.80644
QF_NonLinearIntArith cvc5 1.736503
QF_Equality_Bitvec Yices2 1.669337
QF_Equality SMTInterpol 1.39078
QF_Equality_Bitvec SMTInterpol 1.333546
QF_Equality cvc5 1.27828
Equality_MachineArith SMTInterpol 1.237129
QF_Bitvec cvc5 1.035971
QF_LinearIntArith cvc5 0.912855
FPArith Bitwuzla 0.790855
QF_FPArith Bitwuzla 0.776961
QF_LinearRealArith SMTInterpol 0.760784
QF_FPArith cvc5 0.730047
FPArith cvc5 0.730044
Equality_NonLinearArith cvc5 0.549281
QF_Datatypes cvc5 0.369597
QF_Bitvec SMTInterpol 0.341689
QF_Equality_Bitvec cvc5 0.325368
Arith cvc5 0.147619
QF_Equality_LinearArith cvc5 0.141041
Equality_NonLinearArith SMTInterpol 0.12738
QF_Equality_LinearArith SMTInterpol 0.068812
QF_NonLinearRealArith SMTInterpol 0.037642
QF_NonLinearRealArith cvc5 0.026467
Bitvec cvc5 0.019563
QF_Datatypes SMTInterpol 0.004414
Bitvec Bitwuzla 0.001724
QF_NonLinearIntArith SMTInterpol 0.000453
Arith SMTInterpol 0.000102
Equality_NonLinearArith UltimateEliminator+MathSAT 1e-06
Equality_MachineArith Bitwuzla 0
Bitvec SMTInterpol 0
Bitvec UltimateEliminator+MathSAT 0
FPArith UltimateEliminator+MathSAT 0
Equality_MachineArith UltimateEliminator+MathSAT 0
Equality UltimateEliminator+MathSAT 0
Arith UltimateEliminator+MathSAT -6.169867
QF_Equality OpenSMT (min-ucore) -11.490987
QF_Equality OpenSMT -11.490987
QF_Equality_LinearArith OpenSMT -12.268565
QF_Equality_LinearArith OpenSMT (min-ucore) -12.268565
Equality_LinearArith UltimateEliminator+MathSAT -12.655907
QF_LinearIntArith OpenSMT -13.551086
QF_LinearIntArith OpenSMT (min-ucore) -13.551086

24 seconds Performance

Division Solver Contribution
Equality cvc5 5.017413
Equality_LinearArith cvc5 4.295946
QF_Bitvec Bitwuzla 2.647555
QF_Bitvec Yices2 2.593216
QF_LinearRealArith Yices2 2.136636
QF_LinearIntArith Yices2 2.069325
QF_NonLinearIntArith Yices2 1.939141
QF_Equality_NonLinearArith Yices2 1.907774
QF_LinearRealArith OpenSMT 1.838936
QF_Equality_NonLinearArith SMTInterpol 1.7893
Equality_MachineArith cvc5 1.784752
QF_Equality Yices2 1.748876
Equality_LinearArith SMTInterpol 1.682844
QF_Equality_Bitvec Bitwuzla 1.463705
Equality SMTInterpol 1.383537
QF_NonLinearIntArith cvc5 1.204346
QF_Equality SMTInterpol 1.191736
QF_Equality_Bitvec Yices2 1.177553
QF_Equality cvc5 1.123166
QF_Equality_Bitvec SMTInterpol 1.050389
Equality_MachineArith SMTInterpol 1.030475
QF_LinearRealArith OpenSMT (min-ucore) 0.987252
FPArith Bitwuzla 0.790855
FPArith cvc5 0.730044
QF_FPArith Bitwuzla 0.724263
QF_FPArith cvc5 0.665714
QF_LinearIntArith cvc5 0.526957
QF_NonLinearRealArith Yices2 0.479749
QF_LinearIntArith SMTInterpol 0.444536
QF_Equality_NonLinearArith cvc5 0.375218
Equality_NonLinearArith cvc5 0.27829
QF_LinearRealArith cvc5 0.235488
QF_Bitvec cvc5 0.19226
QF_Equality_Bitvec cvc5 0.175485
Equality_NonLinearArith SMTInterpol 0.109727
QF_Equality_LinearArith Yices2 0.074576
QF_Bitvec SMTInterpol 0.059579
QF_LinearRealArith SMTInterpol 0.057633
QF_NonLinearRealArith SMTInterpol 0.037642
Arith cvc5 0.031053
QF_NonLinearRealArith cvc5 0.02392
Bitvec cvc5 0.010107
QF_Equality_LinearArith cvc5 0.004705
Bitvec Bitwuzla 0.001724
QF_Equality_LinearArith SMTInterpol 0.000659
QF_NonLinearIntArith SMTInterpol 0.000439
Arith SMTInterpol 0.000102
QF_Datatypes SMTInterpol 1e-06
Equality_NonLinearArith UltimateEliminator+MathSAT 1e-06
Equality_MachineArith Bitwuzla 0
QF_Datatypes cvc5 0
Bitvec SMTInterpol 0
Bitvec UltimateEliminator+MathSAT 0
FPArith UltimateEliminator+MathSAT 0
Equality_MachineArith UltimateEliminator+MathSAT 0
Equality UltimateEliminator+MathSAT 0
Arith UltimateEliminator+MathSAT -6.169867
QF_Equality OpenSMT (min-ucore) -11.490987
QF_Equality OpenSMT -11.490987
QF_Equality_LinearArith OpenSMT (min-ucore) -12.268565
QF_Equality_LinearArith OpenSMT -12.268565
Equality_LinearArith UltimateEliminator+MathSAT -12.655907
QF_LinearIntArith OpenSMT (min-ucore) -13.551086
QF_LinearIntArith OpenSMT -13.551086