SMT-COMP 2026

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2026

SMT-COMP 2026 Results - Unsat Core Track

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

Arith

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

Bitvec

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

Equality

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

Equality_LinearArith

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

Equality_MachineArith

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

Equality_NonLinearArith

Scoring SchemeWinnerRanking
Sequential Performancecvc5z3-BooledASS, cvc5, SMTInterpol, UltimateEliminator+MathSAT
Parallel Performancecvc5z3-BooledASS, cvc5, SMTInterpol, UltimateEliminator+MathSAT
SAT Performance-
UNSAT Performancecvc5z3-BooledASS, cvc5, SMTInterpol, UltimateEliminator+MathSAT
24 seconds Performancecvc5z3-BooledASS, cvc5, SMTInterpol, UltimateEliminator+MathSAT

FPArith

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

QF_Bitvec

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

QF_Datatypes

Scoring SchemeWinnerRanking
Sequential Performancecvc5cvc5, z3-BooledASS, SMTInterpol
Parallel Performancecvc5cvc5, z3-BooledASS, SMTInterpol
SAT Performance-
UNSAT Performancecvc5cvc5, z3-BooledASS, SMTInterpol
24 seconds PerformanceSMTInterpolz3-BooledASS, SMTInterpol, cvc5

QF_Equality

Scoring SchemeWinnerRanking
Sequential PerformanceYices2Yices2, z3-BooledASS, OpenSMT (min-ucore), OpenSMT, SMTInterpol, plat-smt, cvc5
Parallel PerformanceYices2Yices2, z3-BooledASS, OpenSMT (min-ucore), OpenSMT, SMTInterpol, plat-smt, cvc5
SAT Performance-
UNSAT PerformanceYices2Yices2, z3-BooledASS, OpenSMT (min-ucore), OpenSMT, SMTInterpol, plat-smt, cvc5
24 seconds PerformanceYices2Yices2, z3-BooledASS, OpenSMT, SMTInterpol, plat-smt, cvc5, OpenSMT (min-ucore)

QF_Equality_Bitvec

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

QF_Equality_LinearArith

Scoring SchemeWinnerRanking
Sequential PerformanceYices2z3-BooledASS, Yices2, OpenSMT, cvc5, SMTInterpol, OpenSMT (min-ucore)
Parallel PerformanceYices2z3-BooledASS, Yices2, OpenSMT, cvc5, SMTInterpol, OpenSMT (min-ucore)
SAT Performance-
UNSAT PerformanceYices2z3-BooledASS, Yices2, OpenSMT, cvc5, SMTInterpol, OpenSMT (min-ucore)
24 seconds PerformanceYices2Yices2, z3-BooledASS, cvc5, SMTInterpol, OpenSMT, OpenSMT (min-ucore)

QF_Equality_NonLinearArith

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

QF_FPArith

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

QF_LinearIntArith

Scoring SchemeWinnerRanking
Sequential PerformanceYices2z3-BooledASS, Yices2, OpenSMT, SMTInterpol, cvc5, OpenSMT (min-ucore)
Parallel PerformanceYices2z3-BooledASS, Yices2, OpenSMT, SMTInterpol, cvc5, OpenSMT (min-ucore)
SAT Performance-
UNSAT PerformanceYices2z3-BooledASS, Yices2, OpenSMT, SMTInterpol, cvc5, OpenSMT (min-ucore)
24 seconds PerformanceYices2Yices2, z3-BooledASS, OpenSMT, cvc5, OpenSMT (min-ucore), SMTInterpol

QF_LinearRealArith

Scoring SchemeWinnerRanking
Sequential PerformanceOpenSMTOpenSMT, OpenSMT (min-ucore), Yices2, cvc5, z3-BooledASS, SMTInterpol
Parallel PerformanceOpenSMTOpenSMT, OpenSMT (min-ucore), Yices2, cvc5, z3-BooledASS, SMTInterpol
SAT Performance-
UNSAT PerformanceOpenSMTOpenSMT, OpenSMT (min-ucore), Yices2, cvc5, z3-BooledASS, SMTInterpol
24 seconds PerformanceOpenSMTOpenSMT, OpenSMT (min-ucore), Yices2, cvc5, z3-BooledASS, SMTInterpol

QF_NonLinearIntArith

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

QF_NonLinearRealArith

Scoring SchemeWinnerRanking
Sequential PerformanceYices2z3-BooledASS, Yices2, cvc5, SMTInterpol
Parallel PerformanceYices2z3-BooledASS, Yices2, cvc5, SMTInterpol
SAT Performance-
UNSAT PerformanceYices2z3-BooledASS, Yices2, cvc5, SMTInterpol
24 seconds PerformanceYices2z3-BooledASS, Yices2, SMTInterpol, cvc5

QF_Strings

Scoring SchemeWinnerRanking
Sequential Performancecvc5z3-BooledASS, cvc5
Parallel Performancecvc5z3-BooledASS, cvc5
SAT Performance-
UNSAT Performancecvc5z3-BooledASS, cvc5
24 seconds Performancecvc5z3-BooledASS, cvc5