SMT-COMP 2026

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2026

QF_ABV (Model Validation Track)

Competition results for the QF_ABV logic in the Model Validation Track. Chart

Results were generated on 2026-07-25

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

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24 seconds Performance (parallel)
BitwuzlaBitwuzlaBitwuzla-Bitwuzla

Sequential Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATUnsolvedAbstainedTimeoutMemout
Bitwuzla014341153.111331.89143414347010
Yices201429770.42948.701429142912000
cvc50132420083.0020249.541324132411701170
SMTInterpol0104299522.4390558.971048104839303760
z3-BooledASS ne7818
(base -579)		2013.252113.89818818623080
z3-BooledASS-base n713972111.442283.191397139744080
(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 SATUnsolvedAbstainedTimeoutMemout
Bitwuzla014341153.111331.89143414347010
Yices201429770.42948.701429142912000
cvc50132420083.0020249.541324132411701170
SMTInterpol01048106916.4597622.441048104839303760
z3-BooledASS ne7818
(base -579)		2013.252113.89818818623080
z3-BooledASS-base n713972111.442283.191397139744080
(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 SATUnsolvedAbstainedTimeoutMemout
Bitwuzla014341153.111331.89143414347010
Yices201429770.42948.701429142912000
cvc50132420083.0020249.541324132411701170
SMTInterpol01048106916.4597622.441048104839303760
z3-BooledASS ne7818
(base -579)		2013.252113.89818818623080
z3-BooledASS-base n713972111.442283.191397139744080
(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 SATUnsolvedAbstainedTimeoutMemout
Bitwuzla01427313.78491.51142714275900
Yices201423352.33529.821423142311700
cvc5011701702.751848.1111701170027100
SMTInterpol07663189.181511.857667661066500
z3-BooledASS ne7808
(base -579)		255.45354.688088086092400
z3-BooledASS-base n71387364.66535.0213871387302400
(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