SMT-COMP 2026

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2026

QF_UF (Single Query Track)

Competition results for the QF_UF logic in the Single Query Track. Chart

Results were generated on 2026-07-25

Benchmarks: 1104
Time Limit: 1200 seconds
Memory Limit: 30720 GB

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24 seconds Performance (parallel)
Yices2Yices2Yices2Yices2Yices2

Sequential Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Yices201104200.33337.1011044676370000
OpenSMT01104979.661116.5411044676370000
cvc5-cvc5-xyz ne01104
(base +0)		994.901129.7211044676370000
cvc5011041057.301193.5711044676370000
OpenSMT-SMTS-seq ne01104
(base +0)		1136.331262.5111044676370000
z3-BooledASS ne01104
(base +0)		1141.201276.7011044676370000
plat-smt011021507.761643.7811024676352020
SMTInterpol010787685.943560.53107846761126010
cvc5-cvc5-xyz-base n01104982.581118.0911044676370000
OpenSMT-SMTS-seq-base n011041000.561137.1711044676370000
z3-BooledASS-base n011041152.091288.0711044676370000
(base +/- n): for derived solvers: increment over base solver
ne: not eligible for winning as it does not substantially improve over the base solver (at least 10 % improvement in PAR2 score) n: non-competing solver

Parallel Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Yices201104200.33337.1011044676370000
OpenSMT01104979.661116.5411044676370000
cvc5-cvc5-xyz ne01104
(base +0)		994.901129.7211044676370000
cvc5011041057.301193.5711044676370000
OpenSMT-SMTS-seq ne01104
(base +0)		1136.331262.5111044676370000
z3-BooledASS ne01104
(base +0)		1141.201276.7011044676370000
plat-smt011021507.761643.7811024676352020
SMTInterpol010787685.943560.53107846761126010
cvc5-cvc5-xyz-base n01104982.581118.0911044676370000
OpenSMT-SMTS-seq-base n011041000.561137.1711044676370000
z3-BooledASS-base n011041152.091288.0711044676370000
(base +/- n): for derived solvers: increment over base solver
ne: not eligible for winning as it does not substantially improve over the base solver (at least 10 % improvement in PAR2 score) n: non-competing solver

SAT Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Yices2046781.39139.324674670063700
plat-smt046796.45154.324674670063700
z3-BooledASS ne0467
(base +0)		111.24168.264674670063700
OpenSMT0467129.02186.954674670063700
cvc5-cvc5-xyz ne0467
(base +0)		148.64205.564674670063700
cvc50467149.88207.624674670063700
OpenSMT-SMTS-seq ne0467
(base +0)		186.47242.224674670063700
SMTInterpol04671072.71478.764674670063700
z3-BooledASS-base n0467112.88170.484674670063700
OpenSMT-SMTS-seq-base n0467132.52190.244674670063700
cvc5-cvc5-xyz-base n0467148.59205.824674670063700
(base +/- n): for derived solvers: increment over base solver
ne: not eligible for winning as it does not substantially improve over the base solver (at least 10 % improvement in PAR2 score) n: non-competing solver

UNSAT Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Yices20637118.95197.786370637046700
cvc5-cvc5-xyz ne0637
(base +0)		846.26924.156370637046700
OpenSMT0637850.65929.596370637046700
cvc50637907.43985.966370637046700
OpenSMT-SMTS-seq ne0637
(base +0)		949.861020.296370637046700
z3-BooledASS ne0637
(base +0)		1029.961108.436370637046700
plat-smt06351411.311489.456350635246720
SMTInterpol06116613.223081.7761106112646710
cvc5-cvc5-xyz-base n0637833.99912.276370637046700
OpenSMT-SMTS-seq-base n0637868.04946.936370637046700
z3-BooledASS-base n06371039.211117.586370637046700
(base +/- n): for derived solvers: increment over base solver
ne: not eligible for winning as it does not substantially improve over the base solver (at least 10 % improvement in PAR2 score) n: non-competing solver

24 seconds Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Yices201104200.33337.1011044676370000
z3-BooledASS ne01099
(base +0)		513.81648.6310994676320500
OpenSMT01097563.14699.1010974676300700
OpenSMT-SMTS-seq ne01097
(base +0)		702.18836.3910974676300700
cvc5-cvc5-xyz ne01096
(base +0)		545.61679.4110964676290800
cvc501095538.90674.0310954676280900
plat-smt01094415.77550.70109446762701000
SMTInterpol010665604.872548.38106646759903800
z3-BooledASS-base n01099518.03653.3210994676320500
OpenSMT-SMTS-seq-base n01097574.21709.9110974676300700
cvc5-cvc5-xyz-base n01096542.09676.6110964676290800
(base +/- n): for derived solvers: increment over base solver
ne: not eligible for winning as it does not substantially improve over the base solver (at least 10 % improvement in PAR2 score) n: non-competing solver