SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

Largest Contribution 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
Equality_NonLinearArith cvc5 0.040963 -0.27985
Equality_MachineArith cvc5 0.014792 0.037362
QF_Bitvec cvc5 0.00962 -0.018355
QF_Equality_LinearArith Yices2 0.008457 -0.031016
QF_Bitvec Bitwuzla 0.006496 0.035599
QF_LinearIntArith Yices2 0.003317 0.014817
Equality_MachineArith SMTInterpol 0.003293 0.010909
QF_NonLinearIntArith Yices2 0.003051 0.01194
QF_NonLinearRealArith Yices2 0.002412 -0.001241
QF_Equality_Bitvec SMTInterpol 0.002074 0.00735
QF_LinearIntArith cvc5 0.001694 -0.004415
QF_Equality_NonLinearArith cvc5 0.001614 0.001216
QF_Equality Yices2 0.001186 0.016631
QF_Equality_Bitvec Bitwuzla 0.000816 0.005459
QF_NonLinearIntArith cvc5 0.000796 -0.003885
Equality_NonLinearArith SMTInterpol 0.000723 -0.000965
QF_Equality_NonLinearArith SMTInterpol 0.000318 -0.002386
QF_Bitvec SMTInterpol 0.000313 0.011814
QF_Equality SMTInterpol 0.000265 -0.002022

Parallel Performance

Division Solver Correct Score Time Score
Equality_NonLinearArith cvc5 0.040963 -0.44462
Equality_MachineArith cvc5 0.014792 0.031907
QF_Bitvec cvc5 0.00962 -0.018419
QF_Equality_LinearArith Yices2 0.008457 -0.034579
QF_Bitvec Bitwuzla 0.006496 0.034988
QF_LinearIntArith Yices2 0.003317 0.014673
Equality_MachineArith SMTInterpol 0.003293 0.014167
QF_NonLinearIntArith Yices2 0.003051 0.011908
QF_NonLinearRealArith Yices2 0.002412 -0.001245
QF_Equality_Bitvec SMTInterpol 0.002074 0.027542
QF_LinearIntArith cvc5 0.001694 -0.004927
QF_Equality_NonLinearArith cvc5 0.001614 0.000945
QF_Equality Yices2 0.001186 0.009793
QF_Equality_Bitvec Bitwuzla 0.000816 -0.006629
QF_NonLinearIntArith cvc5 0.000796 -0.003922
Equality_NonLinearArith SMTInterpol 0.000723 -0.000496
QF_Equality_NonLinearArith SMTInterpol 0.000318 -0.001852
QF_Bitvec SMTInterpol 0.000313 0.012669
QF_Equality SMTInterpol 0.000265 -0.000707

UNSAT Performance

Division Solver Correct Score Time Score
Equality_NonLinearArith cvc5 0.040963 -0.44462
Equality_MachineArith cvc5 0.014792 0.031907
QF_Bitvec cvc5 0.00962 -0.018419
QF_Equality_LinearArith Yices2 0.008457 -0.034579
QF_Bitvec Bitwuzla 0.006496 0.034988
QF_LinearIntArith Yices2 0.003317 0.014673
Equality_MachineArith SMTInterpol 0.003293 0.014167
QF_NonLinearIntArith Yices2 0.003051 0.011908
QF_NonLinearRealArith Yices2 0.002412 -0.001245
QF_Equality_Bitvec SMTInterpol 0.002074 0.027542
QF_LinearIntArith cvc5 0.001694 -0.004927
QF_Equality_NonLinearArith cvc5 0.001614 0.000945
QF_Equality Yices2 0.001186 0.009793
QF_Equality_Bitvec Bitwuzla 0.000816 -0.006629
QF_NonLinearIntArith cvc5 0.000796 -0.003922
Equality_NonLinearArith SMTInterpol 0.000723 -0.000496
QF_Equality_NonLinearArith SMTInterpol 0.000318 -0.001852
QF_Bitvec SMTInterpol 0.000313 0.012669
QF_Equality SMTInterpol 0.000265 -0.000707

24 seconds Performance

Division Solver Correct Score Time Score
Equality_NonLinearArith cvc5 0.030222 0.039172
Equality_MachineArith cvc5 0.015778 0.032658
QF_LinearIntArith Yices2 0.009306 0.00833
QF_Equality_LinearArith Yices2 0.008333 0.002983
QF_Equality_Bitvec SMTInterpol 0.005983 0.004578
QF_NonLinearIntArith Yices2 0.005791 0.007657
Equality_MachineArith SMTInterpol 0.003106 -0.021244
QF_Equality_Bitvec cvc5 0.0025 -0.000713
QF_Bitvec Bitwuzla 0.002374 -0.005011
QF_NonLinearRealArith Yices2 0.001896 -0.0094
QF_LinearRealArith Yices2 0.001755 0.000485
Equality_NonLinearArith SMTInterpol 0.001713 -0.003482
QF_Equality_Bitvec Bitwuzla 0.001582 0.00174
QF_Equality Yices2 0.001246 0.020335
QF_Bitvec Yices2 0.00084 0.035309
QF_NonLinearIntArith cvc5 0.000823 0.001368
QF_Equality_LinearArith cvc5 0.000697 0.00053
QF_LinearRealArith OpenSMT 0.00059 0.000354
QF_Bitvec SMTInterpol 0.000436 -0.007833