SMT-COMP 2026

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2026

Biggest Lead Ranking - Unsat Core Track

Page generated on 2026-07-25

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24 seconds Performance (parallel)
cvc5cvc5-cvc5z3-BooledASS

Sequential Performance

DivisionSolverCorrect ScoreTime Score
Arithcvc54.031250.026
QF_Datatypescvc52.1720541.404455
QF_Equality_BitvecBitwuzla1.8244391.581737
QF_BitvecBitwuzla1.7735710.008091
Equality_MachineArithcvc51.5383450.58792
Equalitycvc51.2045690.188675
Bitveccvc51.20.091824
QF_Equality_LinearArithz3-BooledASS1.1073651.388109
QF_LinearIntArithz3-BooledASS1.080990.639272
QF_NonLinearIntArithYices21.0808033.607686
Equality_NonLinearArithz3-BooledASS1.06286111.976245
QF_NonLinearRealArithz3-BooledASS1.0570531.517052
QF_FPArithBitwuzla1.0425432.458491
FPArithBitwuzla1.049.164066
Equality_LinearArithcvc51.0380590.277291
QF_LinearRealArithOpenSMT1.034281.887944
QF_Stringsz3-BooledASS1.02451228.326802
QF_Equality_NonLinearArithSMTInterpol1.0036641.031335
QF_EqualityYices21.0025081.530585

Parallel Performance

DivisionSolverCorrect ScoreTime Score
Arithcvc54.031250.02741
QF_Datatypescvc52.1720541.404545
QF_Equality_BitvecBitwuzla1.8244391.574797
QF_BitvecBitwuzla1.7735710.008323
Equality_MachineArithcvc51.5383450.445195
Equalitycvc51.2045690.198229
Bitveccvc51.20.094865
QF_Equality_LinearArithz3-BooledASS1.1073651.386717
QF_LinearIntArithz3-BooledASS1.080990.641536
QF_NonLinearIntArithYices21.0808033.578536
Equality_NonLinearArithz3-BooledASS1.06286111.051075
QF_NonLinearRealArithz3-BooledASS1.0570531.514297
QF_FPArithBitwuzla1.0425432.319338
FPArithBitwuzla1.047.146417
Equality_LinearArithcvc51.0380590.295466
QF_LinearRealArithOpenSMT1.034281.885509
QF_Stringsz3-BooledASS1.02451225.805324
QF_Equality_NonLinearArithSMTInterpol1.0036641.24716
QF_EqualityYices21.0025081.453471

UNSAT Performance

DivisionSolverCorrect ScoreTime Score
Arithcvc54.031250.02741
QF_Datatypescvc52.1720541.404545
QF_Equality_BitvecBitwuzla1.8244391.574797
QF_BitvecBitwuzla1.7735710.008323
Equality_MachineArithcvc51.5383450.445195
Equalitycvc51.2045690.198229
Bitveccvc51.20.094865
QF_Equality_LinearArithz3-BooledASS1.1073651.386717
QF_LinearIntArithz3-BooledASS1.080990.641536
QF_NonLinearIntArithYices21.0808033.578536
Equality_NonLinearArithz3-BooledASS1.06286111.051075
QF_NonLinearRealArithz3-BooledASS1.0570531.514297
QF_FPArithBitwuzla1.0425432.319338
FPArithBitwuzla1.047.146417
Equality_LinearArithcvc51.0380590.295466
QF_LinearRealArithOpenSMT1.034281.885509
QF_Stringsz3-BooledASS1.02451225.805324
QF_Equality_NonLinearArithSMTInterpol1.0036641.24716
QF_EqualityYices21.0025081.453471

24 seconds Performance

DivisionSolverCorrect ScoreTime Score
QF_Datatypesz3-BooledASS5.3050021.2599
QF_Equality_LinearArithYices24.4381712.742631
Equality_NonLinearArithz3-BooledASS1.8555271.689837
Arithcvc51.68750.830064
Equality_MachineArithcvc51.6507272.057473
QF_NonLinearRealArithz3-BooledASS1.521580.90503
QF_BitvecBitwuzla1.4328640.160112
QF_LinearRealArithOpenSMT1.2720440.940615
QF_LinearIntArithYices21.1771821.630625
Equalitycvc51.1538690.874347
QF_FPArithBitwuzla1.1420711.172876
QF_NonLinearIntArithYices21.1328341.056365
QF_Equality_NonLinearArithSMTInterpol1.1273260.613194
BitvecBitwuzla1.0869571.024652
FPArithBitwuzla1.044.638847
QF_Stringsz3-BooledASS1.0265672.61159
QF_Equality_BitvecBitwuzla1.0176960.605819
Equality_LinearArithcvc51.0091210.750571
QF_EqualityYices21.0020831.602488