SMT-COMP 2026

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2026

SMT-COMP 2026 Results - Incremental Track

Summary of all competition results for the Incremental Track.
Results are given ranked by performance for each scoring scheme (best solver is given as left-most solver).

Arith

Scoring SchemeWinnerRanking
Parallel Performancecvc5cvc5, SMTInterpol, UltimateEliminator+MathSAT, z3-BooledASS
SAT Performance-
UNSAT Performance-
24 seconds PerformanceSMTInterpolSMTInterpol, cvc5, UltimateEliminator+MathSAT, z3-BooledASS

Bitvec

Scoring SchemeWinnerRanking
Parallel Performancecvc5Bitwuzla-fixed, cvc5, SMTInterpol, UltimateEliminator+MathSAT, z3-BooledASS, Bitwuzla
SAT Performance-
UNSAT Performance-
24 seconds Performancecvc5cvc5, Bitwuzla-fixed, SMTInterpol, UltimateEliminator+MathSAT, z3-BooledASS, Bitwuzla

Equality

Scoring SchemeWinnerRanking
Parallel Performancecvc5cvc5, SMTInterpol, z3-BooledASS, UltimateEliminator+MathSAT
SAT Performance-
UNSAT Performance-
24 seconds Performancecvc5cvc5, SMTInterpol, z3-BooledASS, UltimateEliminator+MathSAT

Equality_LinearArith

Scoring SchemeWinnerRanking
Parallel Performancecvc5cvc5, SMTInterpol, UltimateEliminator+MathSAT, z3-BooledASS
SAT Performance-
UNSAT Performance-
24 seconds Performancecvc5cvc5, SMTInterpol, UltimateEliminator+MathSAT, z3-BooledASS

Equality_MachineArith

Scoring SchemeWinnerRanking
Parallel PerformanceBitwuzlaBitwuzla-fixed, Bitwuzla, cvc5, UltimateEliminator+MathSAT, z3-BooledASS
SAT Performance-
UNSAT Performance-
24 seconds Performancecvc5cvc5, UltimateEliminator+MathSAT, Bitwuzla, Bitwuzla-fixed, z3-BooledASS

Equality_NonLinearArith

Scoring SchemeWinnerRanking
Parallel Performancecvc5cvc5, SMTInterpol, UltimateEliminator+MathSAT, z3-BooledASS
SAT Performance-
UNSAT Performance-
24 seconds Performancecvc5cvc5, SMTInterpol, UltimateEliminator+MathSAT, z3-BooledASS

FPArith

Scoring SchemeWinnerRanking
Parallel PerformanceBitwuzlaBitwuzla, Bitwuzla-fixed, cvc5, UltimateEliminator+MathSAT, z3-BooledASS
SAT Performance-
UNSAT Performance-
24 seconds Performancecvc5cvc5, Bitwuzla-fixed, Bitwuzla, UltimateEliminator+MathSAT, z3-BooledASS

QF_Bitvec

Scoring SchemeWinnerRanking
Parallel PerformanceBitwuzlaBitwuzla, Yices2, cvc5, SMTInterpol, z3-BooledASS
SAT Performance-
UNSAT Performance-
24 seconds PerformanceYices2Yices2, Bitwuzla, cvc5, SMTInterpol, z3-BooledASS

QF_Equality

Scoring SchemeWinnerRanking
Parallel Performanceplat-smtplat-smt, Yices2, cvc5, SMTInterpol, OpenSMT, z3-BooledASS
SAT Performance-
UNSAT Performance-
24 seconds Performanceplat-smtplat-smt, Yices2, cvc5, SMTInterpol, OpenSMT, z3-BooledASS

QF_Equality_Bitvec

Scoring SchemeWinnerRanking
Parallel PerformanceBitwuzlaBitwuzla, Yices2, cvc5, SMTInterpol, z3-BooledASS
SAT Performance-
UNSAT Performance-
24 seconds PerformanceYices2Yices2, Bitwuzla, cvc5, SMTInterpol, z3-BooledASS

QF_Equality_Bitvec_Arith

Scoring SchemeWinnerRanking
Parallel PerformanceYices2Yices2, SMTInterpol, cvc5, z3-BooledASS
SAT Performance-
UNSAT Performance-
24 seconds PerformanceYices2Yices2, cvc5, SMTInterpol, z3-BooledASS

QF_Equality_LinearArith

Scoring SchemeWinnerRanking
Parallel Performancecvc5cvc5, SMTInterpol, Yices2, OpenSMT, z3-BooledASS
SAT Performance-
UNSAT Performance-
24 seconds PerformanceYices2Yices2, cvc5, SMTInterpol, OpenSMT, z3-BooledASS

QF_Equality_NonLinearArith

Scoring SchemeWinnerRanking
Parallel PerformanceSMTInterpolSMTInterpol, cvc5, Yices2, z3-BooledASS
SAT Performance-
UNSAT Performance-
24 seconds PerformanceSMTInterpolSMTInterpol, cvc5, Yices2, z3-BooledASS

QF_FPArith

Scoring SchemeWinnerRanking
Parallel PerformanceBitwuzlaBitwuzla, cvc5, z3-BooledASS
SAT Performance-
UNSAT Performance-
24 seconds PerformanceBitwuzlaBitwuzla, cvc5, z3-BooledASS

QF_LinearIntArith

Scoring SchemeWinnerRanking
Parallel PerformanceYices2Yices2, SMTInterpol, cvc5, OpenSMT, z3-BooledASS
SAT Performance-
UNSAT Performance-
24 seconds PerformanceYices2Yices2, OpenSMT, cvc5, SMTInterpol, z3-BooledASS

QF_LinearRealArith

Scoring SchemeWinnerRanking
Parallel PerformanceOpenSMTOpenSMT, Yices2, cvc5, SMTInterpol, z3-BooledASS
SAT Performance-
UNSAT Performance-
24 seconds Performance-z3-BooledASS

QF_NonLinearIntArith

Scoring SchemeWinnerRanking
Parallel PerformanceSMTInterpolSMTInterpol, cvc5, Yices2, z3-BooledASS
SAT Performance-
UNSAT Performance-
24 seconds PerformanceYices2Yices2, SMTInterpol, cvc5, z3-BooledASS