SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

Largest Contribution Ranking - Single Query Track

Page generated on 2025-08-11

Winners

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24 seconds Performance (parallel)
cvc5cvc5cvc5Z3-Noodler-Mochacvc5

Sequential Performance

DivisionSolverCorrect ScoreTime Score
Equality_LinearArithcvc50.0088990.024368
Equality_NonLinearArithcvc50.0073420.001827
Equality_MachineArithcvc50.004893-0.018558
QF_StringsZ3-Noodler-Mocha0.0032310.136272
Equalitycvc50.001958-0.007166
Equality_MachineArithBitwuzla0.001070.000391
QF_NonLinearIntArithz3siri0.000982-0.002856
QF_NonLinearIntArithZ3-alpha0.000931-0.002136
QF_NonLinearIntArithYices20.0005550.025284
Equality_LinearArithUltimateEliminator+MathSAT0.0004060.000401
Equality_MachineArithSMTInterpol0.0003160.001883
Equality_LinearArithiProver v3.9.30.0003080.001316
QF_NonLinearIntArithcvc50.000307-0.009183
QF_Equality_Bitveccvc50.0003-0.01066
QF_BitvecYices20.0002820.011208
Bitveccvc50.000277-0.002451
QF_Equality_BitvecSMTInterpol0.0002730.00398
FPArithBitwuzla0.000270.001647
Equality_NonLinearArithiProver v3.9.30.00027-0.001329

Parallel Performance

DivisionSolverCorrect ScoreTime Score
Equality_LinearArithcvc50.0075270.024634
Equality_NonLinearArithcvc50.0060110.008065
Equality_MachineArithcvc50.004893-0.024345
QF_StringsZ3-Noodler-Mocha0.0032310.063843
Equalitycvc50.001784-0.009147
QF_NonLinearIntArithZ3-alpha0.0011160.011004
Equality_MachineArithBitwuzla0.001070.000375
QF_NonLinearIntArithz3siri0.000946-0.006788
QF_NonLinearIntArithYices20.0005450.020941
Equality_NonLinearArithiProver v3.9.30.000418-0.000524
Equality_LinearArithUltimateEliminator+MathSAT0.0004050.000409
Equality_LinearArithiProver v3.9.30.0003940.000214
Equality_MachineArithSMTInterpol0.0003160.001982
QF_Equality_Bitveccvc50.0003-0.011816
QF_BitvecYices20.0002820.010929
Bitveccvc50.000277-0.002437
QF_Equality_BitvecSMTInterpol0.0002730.00775
FPArithBitwuzla0.000270.001629
QF_NonLinearIntArithcvc50.000264-0.012915

SAT Performance

DivisionSolverCorrect ScoreTime Score
Equality_LinearArithcvc50.031831-6.952655
Equality_NonLinearArithcvc50.008722-0.05279
Equality_MachineArithcvc50.007711-0.163741
Equality_LinearArithUltimateEliminator+MathSAT0.005299-0.000178
Equalitycvc50.002924-0.107743
Equality_MachineArithBitwuzla0.002326-0.000213
QF_NonLinearIntArithZ3-alpha0.0015280.017928
FPArithBitwuzla0.0005480.002635
QF_NonLinearIntArithYices20.0004620.023635
QF_Equality_Bitveccvc50.000406-0.029073
QF_BitvecYices20.0004010.013518
QF_NonLinearIntArithcvc50.000385-0.021993
QF_Equality_LinearArithSMTInterpol0.000290.000514
Equality_MachineArithSMTInterpol0.000279-2e-06
QF_Equality_NonLinearArithYices20.0002580.000909
QF_BitvecBitwuzla0.0002410.007282
QF_LinearIntArithOpenSMT0.0002320.000792
ArithYicesQS0.0001810.009289
Bitveccvc50.00017-0.002375

UNSAT Performance

DivisionSolverCorrect ScoreTime Score
QF_StringsZ3-Noodler-Mocha0.0091620.181973
Equality_NonLinearArithcvc50.0056960.009231
Equality_LinearArithcvc50.0055590.029079
Equality_MachineArithcvc50.003982-0.007288
QF_NonLinearIntArithz3siri0.002634-0.036338
Equalitycvc50.0013180.002436
QF_Equality_BitvecSMTInterpol0.0007820.010791
QF_NonLinearIntArithYices20.0007090.015437
Equality_MachineArithBitwuzla0.0006650.000919
Equality_NonLinearArithiProver v3.9.30.000466-0.00058
Equality_LinearArithiProver v3.9.30.0004260.000322
Equality_MachineArithSMTInterpol0.0003270.00349
Bitveccvc50.000312-0.002466
QF_NonLinearIntArithZ3-alpha0.000304-0.005745
QF_LinearIntArithcvc50.0002890.010459
QF_FPArithBitwuzla0.0002740.005922
ArithYicesQS0.0002490.009961
QF_BitvecBitwuzla-MachBV0.0002480.02524
QF_Equality_BitvecBitwuzla0.0002270.016445

24 seconds Performance

DivisionSolverCorrect ScoreTime Score
Equality_LinearArithcvc50.0118680.025679
Equality_NonLinearArithcvc50.0080580.009695
QF_LinearIntArithYices20.0049130.026228
Equality_MachineArithcvc50.0040550.004711
QF_StringsZ3-Noodler-Mocha0.0034660.069201
QF_NonLinearIntArithYices20.0026370.018382
Equalitycvc50.001760.00256
QF_NonLinearIntArithZ3-alpha0.00130.007156
Equality_MachineArithBitwuzla0.001205-0.003526
EqualityiProver v3.9.30.001062-0.00318
Equality_NonLinearArithiProver v3.9.30.000858-0.003647
QF_BitvecYices20.0007720.030449
Equality_MachineArithSMTInterpol0.000765-0.001486
QF_Equality_BitvecBitwuzla0.0006890.000266
Equality_LinearArithiProver v3.9.30.000586-0.003413
QF_FPArithBitwuzla0.0005290.003022
ArithYicesQS0.0005060.006592
QF_NonLinearIntArithz3siri0.0004760.004767
QF_Equality_NonLinearArithYices20.000448-0.000458