SMT-COMP 2026

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2026

Largest Contribution 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_Datatypescvc50.002993-0.001322
QF_Equality_NonLinearArithcvc50.002846-0.000202
QF_NonLinearIntArithcvc50.002147-0.088523
QF_ADT_BitVeccvc50.002074-0.447229
QF_FPArithcvc50.0010670.008418
QF_Equality_LinearArithOpenSMT0.0009450.025069
QF_Equality_NonLinearArithSMTInterpol0.0007460.002807
QF_NonLinearIntArithYices20.0007010.040729
QF_DatatypesSMTInterpol0.0006790.003702
QF_BitvecBitwuzla0.0006740.075595
QF_LinearIntArithSMTInterpol0.000490.021347
QF_LinearIntArithYices20.000420.06514
QF_FPArithBitwuzla0.0003560.054603
QF_LinearIntArithOpenSMT0.000280.0172
QF_ADT_BitVecBitwuzla0.0002360.016726
QF_LinearRealArithYices20.0002230.016479
QF_LinearRealArithSMTInterpol0.000223-0.001344
QF_NonLinearIntArithz3-BooledASS0.0002190.003105
QF_LinearRealArithOpenSMT0.0001490.009962

Parallel Performance

DivisionSolverCorrect ScoreTime Score
QF_Datatypescvc50.002993-0.002028
QF_Equality_NonLinearArithcvc50.002846-0.000322
QF_NonLinearIntArithcvc50.002147-0.087439
QF_ADT_BitVeccvc50.002074-0.394726
QF_FPArithcvc50.0010670.007186
QF_Equality_LinearArithOpenSMT0.0008720.030978
QF_Equality_NonLinearArithSMTInterpol0.0007460.003298
QF_NonLinearIntArithYices20.0007010.040604
QF_DatatypesSMTInterpol0.0006790.00406
QF_BitvecBitwuzla0.0006740.07461
QF_LinearIntArithSMTInterpol0.000490.023874
QF_LinearIntArithYices20.000420.06095
QF_FPArithBitwuzla0.0003560.046877
QF_LinearIntArithOpenSMT0.000280.017436
QF_ADT_BitVecBitwuzla0.0002360.015852
QF_LinearRealArithYices20.0002230.016359
QF_LinearRealArithSMTInterpol0.000223-0.000408
QF_NonLinearIntArithz3-BooledASS0.0002190.003087
QF_LinearRealArithOpenSMT0.0001490.009622

SAT Performance

DivisionSolverCorrect ScoreTime Score
QF_Datatypescvc50.002993-0.002028
QF_Equality_NonLinearArithcvc50.002846-0.000322
QF_NonLinearIntArithcvc50.002147-0.087439
QF_ADT_BitVeccvc50.002074-0.394726
QF_FPArithcvc50.0010670.007186
QF_Equality_LinearArithOpenSMT0.0008720.030978
QF_Equality_NonLinearArithSMTInterpol0.0007460.003298
QF_NonLinearIntArithYices20.0007010.040604
QF_DatatypesSMTInterpol0.0006790.00406
QF_BitvecBitwuzla0.0006740.07461
QF_LinearIntArithSMTInterpol0.000490.023874
QF_LinearIntArithYices20.000420.06095
QF_FPArithBitwuzla0.0003560.046877
QF_LinearIntArithOpenSMT0.000280.017436
QF_ADT_BitVecBitwuzla0.0002360.015852
QF_LinearRealArithYices20.0002230.016359
QF_LinearRealArithSMTInterpol0.000223-0.000408
QF_NonLinearIntArithz3-BooledASS0.0002190.003087
QF_LinearRealArithOpenSMT0.0001490.009622

24 seconds Performance

DivisionSolverCorrect ScoreTime Score
QF_LinearIntArithYices20.0106330.038047
QF_NonLinearIntArithYices20.0073640.027786
QF_BitvecBitwuzla0.005750.055268
QF_Equality_NonLinearArithcvc50.00309-0.000761
QF_LinearRealArithYices20.0012130.008513
QF_Equality_NonLinearArithSMTInterpol0.0011880.000414
QF_Equality_LinearArithOpenSMT0.001117-0.022712
QF_FPArithcvc50.001070.006323
QF_ADT_BitVeccvc50.001014-0.02614
QF_Datatypescvc50.000994-0.028804
QF_DatatypesSMTInterpol0.000949-0.004088
QF_NonLinearIntArithcvc50.0006140.001377
QF_LinearIntArithOpenSMT0.0005918.3e-05
QF_LinearRealArithOpenSMT0.0005660.001135
QF_LinearIntArithSMTInterpol0.000517-0.007306
QF_Equality_BitvecBitwuzla0.00046-0.003295
QF_ADT_LinArithSMTInterpol0.000399-0.004047
QF_FPArithBitwuzla0.0003570.032111
QF_ADT_BitVecBitwuzla0.0003380.006706