SMT-COMP 2026

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2026

QF_UFBV (Model Validation Track)

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

Results were generated on 2026-07-25

Benchmarks: 437
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
Bitwuzla04375027.485083.654374370000
Yices204377651.707706.504374370000
SMTInterpol031823756.3418731.613183181190450
z3-BooledASS ne0270
(base -122)		1891.911925.072702701670280
cvc501996473.036498.7419919923802380
z3-BooledASS-base n03926779.266828.05392392450270
(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
Bitwuzla04375027.485083.654374370000
Yices204377651.707706.504374370000
SMTInterpol031823756.3418731.613183181190450
z3-BooledASS ne0270
(base -122)		1891.911925.072702701670280
cvc501996473.036498.7419919923802380
z3-BooledASS-base n03926779.266828.05392392450270
(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
Bitwuzla04375027.485083.654374370000
Yices204377651.707706.504374370000
SMTInterpol031823756.3418731.613183181190450
z3-BooledASS ne0270
(base -122)		1891.911925.072702701670280
cvc501996473.036498.7419919923802380
z3-BooledASS-base n03926779.266828.05392392450270
(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
Yices20396468.19517.2139639604100
Bitwuzla0384799.15847.9838438405300
z3-BooledASS ne0263
(base -107)		265.55297.682632631165800
SMTInterpol02324289.771733.702322321519000
cvc50172132.61153.92172172026500
z3-BooledASS-base n0370622.92668.29370370125500
(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