SMT-COMP 2026

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2026

Biggest Lead Ranking - Incremental Track

Page generated on 2026-07-25

Winners

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

Parallel Performance

DivisionSolverCorrect ScoreTime Score
QF_NonLinearIntArithSMTInterpol2.5684294.230919
Equalitycvc51.9034241.797439
Equality_NonLinearArithcvc51.286622.231934
QF_Equality_NonLinearArithSMTInterpol1.22243913.35192
QF_LinearRealArithOpenSMT1.1191772.203736
QF_FPArithBitwuzla1.08845131.165822
Arithcvc51.08478914.994224
BitvecBitwuzla-fixed1.0844224.545172
Equality_LinearArithcvc51.0612514.146281
QF_LinearIntArithYices21.0199241.669193
QF_Equality_LinearArithcvc51.013641.011613
QF_Equality_BitvecBitwuzla1.0101810.506665
QF_Equality_Bitvec_ArithYices21.00236613.213426
QF_BitvecBitwuzla1.0008271.157644
QF_Equalityplat-smt11.030058
Equality_MachineArithBitwuzla-fixed11.016415
FPArithBitwuzla11.00235

24 seconds Performance

DivisionSolverCorrect ScoreTime Score
QF_LinearIntArithYices2508.786380.811839
QF_NonLinearIntArithYices27.0019042.007371
Equalitycvc52.6144280.333275
Equality_NonLinearArithcvc52.0533570.386993
QF_Equality_LinearArithYices21.7481611.954662
FPArithcvc51.5963442.046933
Equality_LinearArithcvc51.4804120.723728
QF_Equality_NonLinearArithSMTInterpol1.4641261.818749
QF_BitvecYices21.1938631.538568
ArithSMTInterpol1.1392330.572234
Bitveccvc51.1234021.329651
Equality_MachineArithcvc51.1022881.802669
QF_Equality_Bitvec_ArithYices21.0962411.693323
QF_FPArithBitwuzla1.0944862.51413
QF_Equality_BitvecYices21.0666671.838203
QF_Equalityplat-smt11.030058