SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

Biggest Lead Ranking - Model Validation Track

Page generated on 2025-08-11

Winners

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24 seconds Performance (parallel)
SMTInterpolSMTInterpolSMTInterpol-Yices2

Sequential Performance

DivisionSolverCorrect ScoreTime Score
QF_DatatypesSMTInterpol1.3951371.408922
QF_Equality_NonLinearArithcvc51.2517730.929269
QF_ADT_BitVecBitwuzla1.09534820.929064
QF_NonLinearIntArithYices21.07264536.175695
QF_NonLinearRealArithSMT-RAT1.0361740.473766
QF_ADT_LinArithSMTInterpol1.0144551.522788
QF_Equality_LinearArithOpenSMT1.0138891.362268
QF_LinearIntArithOpenSMT1.0108050.261748
QF_BitvecBitwuzla1.0055411.906713
QF_LinearRealArithYices21.0016921.730295
QF_FPArithcvc51.0004520.605873
QF_Equality_BitvecBitwuzla12.205669
QF_EqualityOpenSMT11.297969

Parallel Performance

DivisionSolverCorrect ScoreTime Score
QF_DatatypesSMTInterpol1.3951371.502915
QF_Equality_NonLinearArithcvc51.2517730.829817
QF_ADT_BitVecBitwuzla1.09534817.675811
QF_NonLinearIntArithYices21.07264535.517632
QF_NonLinearRealArithSMT-RAT1.0361740.479133
QF_ADT_LinArithSMTInterpol1.0144551.997009
QF_Equality_LinearArithOpenSMT1.0138891.046461
QF_LinearIntArithOpenSMT1.0108050.263454
QF_BitvecBitwuzla1.0055411.883834
QF_LinearRealArithYices21.0016921.725949
QF_FPArithcvc51.0004520.677801
QF_Equality_BitvecBitwuzla12.198479
QF_EqualityOpenSMT11.192156

SAT Performance

DivisionSolverCorrect ScoreTime Score
QF_DatatypesSMTInterpol1.3951371.502915
QF_Equality_NonLinearArithcvc51.2517730.829817
QF_ADT_BitVecBitwuzla1.09534817.675811
QF_NonLinearIntArithYices21.07264535.517632
QF_NonLinearRealArithSMT-RAT1.0361740.479133
QF_ADT_LinArithSMTInterpol1.0144551.997009
QF_Equality_LinearArithOpenSMT1.0138891.046461
QF_LinearIntArithOpenSMT1.0108050.263454
QF_BitvecBitwuzla1.0055411.883834
QF_LinearRealArithYices21.0016921.725949
QF_FPArithcvc51.0004520.677801
QF_Equality_BitvecBitwuzla12.198479
QF_EqualityOpenSMT11.192156

24 seconds Performance

DivisionSolverCorrect ScoreTime Score
QF_NonLinearIntArithYices22.171370.557579
QF_DatatypesSMTInterpol1.4795420.645562
QF_Equality_NonLinearArithcvc51.2952380.970407
QF_ADT_BitVecBitwuzla1.233123.29299
QF_LinearIntArithYices21.1896741.504684
QF_Equality_BitvecYices21.0437161.014453
QF_ADT_LinArithSMTInterpol1.0369361.049349
QF_BitvecBitwuzla1.0330790.738656
QF_LinearRealArithYices21.0308291.598645
QF_Equality_LinearArithSMTInterpol1.0133330.904105
QF_NonLinearRealArithSMT-RAT1.0119940.876962
QF_FPArithBitwuzla1.0011531.156261
QF_EqualityOpenSMT11.192156