SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

Biggest Lead Ranking - Incremental Track

Page generated on 2025-08-11

Winners

Winners

Parallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24 seconds Performance (parallel)
Bitwuzla--Yices2

Parallel Performance

DivisionSolverCorrect ScoreTime Score
Equality_MachineArithBitwuzla2.7716730.193079
Equalitycvc52.0783574.366691
Equality_NonLinearArithcvc51.6755054.445631
FPArithBitwuzla1.6445560.09317
QF_Equality_NonLinearArithSMTInterpol1.18819710.602028
QF_FPArithBitwuzla1.10707121.964855
Arithcvc51.08478914.738061
QF_Equality_LinearArithSMTInterpol1.0453791.165492
Equality_LinearArithcvc51.0334678.555007
Bitveccvc51.0220460.234721
QF_LinearRealArithOpenSMT1.0156581.453802
QF_LinearIntArithYices21.0156271.639626
QF_Equality_BitvecBitwuzla1.0100910.503223
QF_NonLinearIntArithZ3-Inc-Z3++1.0061830.811674
QF_Equality_Bitvec_ArithYices21.0045924.779713
QF_BitvecYices21.001920.851529
QF_EqualityYices214.199948

24 seconds Performance

DivisionSolverCorrect ScoreTime Score
QF_LinearIntArithYices2480.5360090.761368
Equalitycvc52.7966660.193835
QF_NonLinearIntArithYices22.3076921.864166
Equality_NonLinearArithcvc52.1107650.204826
QF_Equality_LinearArithYices22.048542.731351
QF_FPArithBitwuzla1.5894843.30433
FPArithBitwuzla1.3097620.35593
Bitveccvc51.1897550.610055
ArithSMTInterpol1.1392030.623148
Equality_MachineArithcvc51.1022881.462209
QF_Equality_Bitvec_ArithYices21.0732921.515629
QF_BitvecYices21.025411.11554
QF_Equality_BitvecYices21.0222051.367319
QF_Equality_NonLinearArithcvc51.0047940.57519
Equality_LinearArithSMTInterpol1.0010472.439115
QF_EqualityYices214.199948