SMT-COMP 2026

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2026

SMT-COMP 2026 Results - Model Validation Track

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

QF_ADT_BitVec

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

QF_ADT_LinArith

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

QF_Bitvec

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

QF_Datatypes

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

QF_Equality

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

QF_Equality_Bitvec

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

QF_Equality_LinearArith

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

QF_Equality_NonLinearArith

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

QF_FPArith

Scoring SchemeWinnerRanking
Sequential Performancecvc5cvc5, Bitwuzla, z3-BooledASS
Parallel Performancecvc5cvc5, Bitwuzla, z3-BooledASS
SAT Performancecvc5cvc5, Bitwuzla, z3-BooledASS
UNSAT Performance-
24 seconds Performancecvc5cvc5, Bitwuzla, z3-BooledASS

QF_LinearIntArith

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

QF_LinearRealArith

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

QF_NonLinearIntArith

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

QF_NonLinearRealArith

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