SMT-COMP 2026

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2026

SMT-COMP 2026 Results - Parallel Track

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

QF_Bitvec

Scoring SchemeWinnerRanking
Sequential Performance-
Parallel PerformanceBitwuzllobBitwuzllob, Bitwuzla-BV_Parti
SAT PerformanceBitwuzllobBitwuzllob, Bitwuzla-BV_Parti
UNSAT PerformanceBitwuzllobBitwuzllob, Bitwuzla-BV_Parti
24 seconds PerformanceBitwuzllobBitwuzllob

QF_Equality_LinearArith

Scoring SchemeWinnerRanking
Sequential Performance-
Parallel Performancez3-parallelz3-parallel, OpenSMT-SMTS
SAT Performancez3-parallelz3-parallel, OpenSMT-SMTS
UNSAT Performancez3-parallelz3-parallel, OpenSMT-SMTS
24 seconds Performance-

QF_LinearIntArith

Scoring SchemeWinnerRanking
Sequential Performance-
Parallel PerformanceOpenSMT-SMTSOpenSMT-SMTS, z3-parallel, QiuQi
SAT PerformanceOpenSMT-SMTSOpenSMT-SMTS, z3-parallel, QiuQi
UNSAT Performancez3-parallelz3-parallel, QiuQi, OpenSMT-SMTS
24 seconds PerformanceOpenSMT-SMTSOpenSMT-SMTS, QiuQi

QF_LinearRealArith

Scoring SchemeWinnerRanking
Sequential Performance-
Parallel Performancez3-parallelOpenSMT-SMTS, z3-parallel
SAT PerformanceOpenSMT-SMTSOpenSMT-SMTS, z3-parallel
UNSAT Performancez3-parallelOpenSMT-SMTS, z3-parallel
24 seconds PerformanceOpenSMT-SMTSOpenSMT-SMTS

QF_NonLinearIntArith

Scoring SchemeWinnerRanking
Sequential Performance-
Parallel PerformanceYices2Yices2, z3-parallel
SAT PerformanceYices2Yices2, z3-parallel
UNSAT Performancez3-parallelz3-parallel, Yices2
24 seconds PerformanceYices2Yices2, z3-parallel

QF_NonLinearRealArith

Scoring SchemeWinnerRanking
Sequential Performance-
Parallel PerformanceYices2Yices2, z3-parallel
SAT PerformanceYices2Yices2, z3-parallel
UNSAT PerformanceYices2Yices2, z3-parallel
24 seconds PerformanceYices2Yices2, z3-parallel