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 PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24 seconds Performance (parallel)
cvc5cvc5-cvc5cvc5

Sequential Performance

DivisionSolverCorrect ScoreTime Score
Equality_NonLinearArithcvc50.040963-0.27985
Equality_MachineArithcvc50.0147920.037362
QF_Bitveccvc50.00962-0.018355
QF_Equality_LinearArithYices20.008457-0.031016
QF_BitvecBitwuzla0.0064960.035599
QF_LinearIntArithYices20.0033170.014817
Equality_MachineArithSMTInterpol0.0032930.010909
QF_NonLinearIntArithYices20.0030510.01194
QF_NonLinearRealArithYices20.002412-0.001241
QF_Equality_BitvecSMTInterpol0.0020740.00735
QF_LinearIntArithcvc50.001694-0.004415
QF_Equality_NonLinearArithcvc50.0016140.001216
QF_EqualityYices20.0011860.016631
QF_Equality_BitvecBitwuzla0.0008160.005459
QF_NonLinearIntArithcvc50.000796-0.003885
Equality_NonLinearArithSMTInterpol0.000723-0.000965
QF_Equality_NonLinearArithSMTInterpol0.000318-0.002386
QF_BitvecSMTInterpol0.0003130.011814
QF_EqualitySMTInterpol0.000265-0.002022

Parallel Performance

DivisionSolverCorrect ScoreTime Score
Equality_NonLinearArithcvc50.040963-0.44462
Equality_MachineArithcvc50.0147920.031907
QF_Bitveccvc50.00962-0.018419
QF_Equality_LinearArithYices20.008457-0.034579
QF_BitvecBitwuzla0.0064960.034988
QF_LinearIntArithYices20.0033170.014673
Equality_MachineArithSMTInterpol0.0032930.014167
QF_NonLinearIntArithYices20.0030510.011908
QF_NonLinearRealArithYices20.002412-0.001245
QF_Equality_BitvecSMTInterpol0.0020740.027542
QF_LinearIntArithcvc50.001694-0.004927
QF_Equality_NonLinearArithcvc50.0016140.000945
QF_EqualityYices20.0011860.009793
QF_Equality_BitvecBitwuzla0.000816-0.006629
QF_NonLinearIntArithcvc50.000796-0.003922
Equality_NonLinearArithSMTInterpol0.000723-0.000496
QF_Equality_NonLinearArithSMTInterpol0.000318-0.001852
QF_BitvecSMTInterpol0.0003130.012669
QF_EqualitySMTInterpol0.000265-0.000707

UNSAT Performance

DivisionSolverCorrect ScoreTime Score
Equality_NonLinearArithcvc50.040963-0.44462
Equality_MachineArithcvc50.0147920.031907
QF_Bitveccvc50.00962-0.018419
QF_Equality_LinearArithYices20.008457-0.034579
QF_BitvecBitwuzla0.0064960.034988
QF_LinearIntArithYices20.0033170.014673
Equality_MachineArithSMTInterpol0.0032930.014167
QF_NonLinearIntArithYices20.0030510.011908
QF_NonLinearRealArithYices20.002412-0.001245
QF_Equality_BitvecSMTInterpol0.0020740.027542
QF_LinearIntArithcvc50.001694-0.004927
QF_Equality_NonLinearArithcvc50.0016140.000945
QF_EqualityYices20.0011860.009793
QF_Equality_BitvecBitwuzla0.000816-0.006629
QF_NonLinearIntArithcvc50.000796-0.003922
Equality_NonLinearArithSMTInterpol0.000723-0.000496
QF_Equality_NonLinearArithSMTInterpol0.000318-0.001852
QF_BitvecSMTInterpol0.0003130.012669
QF_EqualitySMTInterpol0.000265-0.000707

24 seconds Performance

DivisionSolverCorrect ScoreTime Score
Equality_NonLinearArithcvc50.0302220.039172
Equality_MachineArithcvc50.0157780.032658
QF_LinearIntArithYices20.0093060.00833
QF_Equality_LinearArithYices20.0083330.002983
QF_Equality_BitvecSMTInterpol0.0059830.004578
QF_NonLinearIntArithYices20.0057910.007657
Equality_MachineArithSMTInterpol0.003106-0.021244
QF_Equality_Bitveccvc50.0025-0.000713
QF_BitvecBitwuzla0.002374-0.005011
QF_NonLinearRealArithYices20.001896-0.0094
QF_LinearRealArithYices20.0017550.000485
Equality_NonLinearArithSMTInterpol0.001713-0.003482
QF_Equality_BitvecBitwuzla0.0015820.00174
QF_EqualityYices20.0012460.020335
QF_BitvecYices20.000840.035309
QF_NonLinearIntArithcvc50.0008230.001368
QF_Equality_LinearArithcvc50.0006970.00053
QF_LinearRealArithOpenSMT0.000590.000354
QF_BitvecSMTInterpol0.000436-0.007833