SMT-COMP 2026

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2026

Biggest Lead Ranking - Model Validation Track

Page generated on 2026-07-25

Winners

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

Sequential Performance

DivisionSolverCorrect ScoreTime Score
QF_Equality_NonLinearArithcvc51.3466140.682766
QF_NonLinearIntArithYices21.06033925.70876
QF_NonLinearRealArithz3-BooledASS1.0290465.027006
QF_Datatypescvc51.0285710.54325
QF_Equality_LinearArithOpenSMT1.0197440.929613
QF_LinearIntArithYices21.0111873.176729
QF_BitvecBitwuzla1.0096152.832275
QF_LinearRealArithOpenSMT1.0068730.44842
QF_ADT_BitVecBitwuzla1.0062031.341865
QF_FPArithcvc51.002410.772672
QF_ADT_LinArithcvc51.0013070.331704
QF_Equality_BitvecBitwuzla11.521873
QF_EqualityYices211.431588

Parallel Performance

DivisionSolverCorrect ScoreTime Score
QF_Equality_NonLinearArithcvc51.3466140.60393
QF_NonLinearIntArithYices21.06033925.375563
QF_NonLinearRealArithz3-BooledASS1.0290464.784416
QF_Datatypescvc51.0285710.545883
QF_Equality_LinearArithOpenSMT1.0185610.753206
QF_LinearIntArithYices21.0111873.159849
QF_BitvecBitwuzla1.0096152.794638
QF_LinearRealArithOpenSMT1.0068730.450909
QF_ADT_BitVecBitwuzla1.0062031.316639
QF_FPArithcvc51.002410.803367
QF_ADT_LinArithcvc51.0013070.237682
QF_Equality_BitvecBitwuzla11.515837
QF_EqualityYices211.249603

SAT Performance

DivisionSolverCorrect ScoreTime Score
QF_Equality_NonLinearArithcvc51.3466140.60393
QF_NonLinearIntArithYices21.06033925.375563
QF_NonLinearRealArithz3-BooledASS1.0290464.784416
QF_Datatypescvc51.0285710.545883
QF_Equality_LinearArithOpenSMT1.0185610.753206
QF_LinearIntArithYices21.0111873.159849
QF_BitvecBitwuzla1.0096152.794638
QF_LinearRealArithOpenSMT1.0068730.450909
QF_ADT_BitVecBitwuzla1.0062031.316639
QF_FPArithcvc51.002410.803367
QF_ADT_LinArithcvc51.0013070.237682
QF_Equality_BitvecBitwuzla11.515837
QF_EqualityYices211.249603

24 seconds Performance

DivisionSolverCorrect ScoreTime Score
QF_NonLinearIntArithYices21.8512110.960626
QF_Equality_NonLinearArithcvc51.3041470.702922
QF_Datatypesz3-BooledASS1.1147192.691331
QF_LinearIntArithYices21.102751.226886
QF_BitvecBitwuzla1.0949251.63187
QF_LinearRealArithYices21.0468751.31863
QF_Equality_BitvecYices21.0311691.638289
QF_NonLinearRealArithz3-BooledASS1.0309860.688865
QF_ADT_LinArithSMTInterpol1.0230661.214955
QF_Equality_LinearArithSMTInterpol1.0109220.895077
QF_FPArithcvc51.0020940.837923
QF_ADT_BitVecBitwuzla1.0020831.082568
QF_EqualityYices211.249603