SMT-COMP 2026

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2026

QF_AUFBV (Model Validation Track)

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

Results were generated on 2026-07-25

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

Winners

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

Sequential Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATUnsolvedAbstainedTimeoutMemout
Bitwuzla0251174.751178.1325250000
Yices20212353.612356.4221214040
cvc5012447.08448.671212130130
z3-BooledASS ne05
(base -4)		1.912.5455200100
SMTInterpol04991.21914.6644210140
z3-BooledASS-base n09122.99124.1299160100
(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
Bitwuzla0251174.751178.1325250000
Yices20212353.612356.4221214040
cvc5012447.08448.671212130130
z3-BooledASS ne05
(base -4)		1.912.5455200100
SMTInterpol04991.21914.6644210140
z3-BooledASS-base n09122.99124.1299160100
(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
Bitwuzla0251174.751178.1325250000
Yices20212353.612356.4221214040
cvc5012447.08448.671212130130
z3-BooledASS ne05
(base -4)		1.912.5455200100
SMTInterpol04991.21914.6644210140
z3-BooledASS-base n09122.99124.1299160100
(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
Yices20168.4610.4216160900
Bitwuzla0155.597.46151501000
cvc501062.4763.72101001500
z3-BooledASS ne05
(base -3)		1.912.545561400
SMTInterpol025.202.212261700
z3-BooledASS-base n082.463.468821500
(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