SMT-COMP 2026

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2026

QF_ADT_BitVec (Model Validation Track)

Competition results for the QF_ADT_BitVec division in the Model Validation Track. Chart

Results were generated on 2026-07-25

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

Logics:

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
Bitwuzla014592327.872510.031459145974710
Yices2014503124.023305.1214501450164740
cvc50138028984.6029159.321380138013301330
SMTInterpol01046100513.6491473.641052105246104170
z3-BooledASS ne7852
(base -578)		11601.6311707.568528526610360
z3-BooledASS-base n714309624.379800.9814301430830400
(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
Bitwuzla014592327.872510.031459145974710
Yices2014503124.023305.1214501450164740
cvc50138028984.6029159.321380138013301330
SMTInterpol01052107907.6698537.111052105246104170
z3-BooledASS ne7852
(base -578)		11601.6311707.568528526610360
z3-BooledASS-base n714309624.379800.9814301430830400
(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
Bitwuzla014592327.872510.031459145974710
Yices2014503124.023305.1214501450164740
cvc50138028984.6029159.321380138013301330
SMTInterpol01052107907.6698537.111052105246104170
z3-BooledASS ne7852
(base -578)		11601.6311707.568528526610360
z3-BooledASS-base n714309624.379800.9814301430830400
(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
Bitwuzla01442319.37498.961442144256600
Yices201439360.79540.2514391439116300
cvc5012011932.442081.6612011201031200
SMTInterpol07683194.381514.067687682472100
z3-BooledASS ne7822
(base -581)		294.33395.368228226157600
z3-BooledASS-base n71403384.34556.6914031403327800
(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