SMT-COMP 2026

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2026

QF_LIA (Unsat Core Track)

Competition results for the QF_LIA logic in the Unsat Core Track. Chart

Results were generated on 2026-07-25

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

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24 seconds Performance (parallel)
Yices2Yices2-Yices2Yices2

Sequential Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved UNSATUnsolvedAbstainedTimeoutMemout
z3-BooledASS ne02290703
(base +0)		3239.073310.455805808080
Yices2022695141903.871976.475805808080
OpenSMT019768141596.581669.215795799090
SMTInterpol016001249252.398223.99570570180160
OpenSMT (min-ucore)014862248477.518548.66563563250250
cvc5012422351049.141115.70534534540540
z3-BooledASS-base n022907033231.083302.515805808080
(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 UNSATUnsolvedAbstainedTimeoutMemout
z3-BooledASS ne02290703
(base +0)		3239.073310.455805808080
Yices2022695141903.871976.475805808080
OpenSMT019768141596.581669.215795799090
SMTInterpol016001249252.398223.99570570180160
OpenSMT (min-ucore)014862248477.518548.66563563250250
cvc5012422351049.141115.70534534540540
z3-BooledASS-base n022907033231.083302.515805808080
(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 UNSATUnsolvedAbstainedTimeoutMemout
z3-BooledASS ne02290703
(base +0)		3239.073310.455805808080
Yices2022695141903.871976.475805808080
OpenSMT019768141596.581669.215795799090
SMTInterpol016001249252.398223.99570570180160
OpenSMT (min-ucore)014862248477.518548.66563563250250
cvc5012422351049.141115.70534534540540
z3-BooledASS-base n022907033231.083302.515805808080
(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 UNSATUnsolvedAbstainedTimeoutMemout
Yices202101931214.45285.8957257201600
z3-BooledASS ne01766194
(base +0)		384.75454.5856956901900
OpenSMT01386616305.90376.7456656602200
cvc501242205279.00344.8552952905900
OpenSMT (min-ucore)01093155375.21442.1453653605200
SMTInterpol0818279990.71540.9754154104700
z3-BooledASS-base n01766194385.00454.8556956901900
(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