SMT-COMP 2026

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2026

QF_Equality_Bitvec (Single Query Track)

Competition results for the QF_Equality_Bitvec division in the Single Query Track. Chart

Results were generated on 2026-07-25

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

Logics:

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24 seconds Performance (parallel)
BitwuzlaBitwuzlaBitwuzlaBitwuzlaBitwuzla

Sequential Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
bitwuzla-dandelion n02486
(base +8)		25284.5825597.48248615659215576550
Bitwuzla0247920690.8521003.44247915659146276620
Yices20242348332.9548638.0524231553870118761180
cvc5-cvc5-xyz ne02373
(base -1)		145961.51146272.152373151685724402440
cvc502371146315.33146627.752371151485724602460
NeuroSym018682013.081804.17186813205484670300
SMTInterpol01829140251.91123934.921834107476078306270
z3-BooledASS ne01646
(base -692)		46341.6946547.89164698566197102690
bitwuzla-dandelion-base n0247821211.2121522.65247815639156376630
cvc5-cvc5-xyz-base n02374147049.79147364.242374151785724302430
z3-BooledASS-base n0233859785.6760079.692338152381527902770
(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 SATSolved UNSATUnsolvedAbstainedTimeoutMemout
bitwuzla-dandelion n02486
(base +8)		25284.5825597.48248615659215576550
Bitwuzla0247920690.8521003.44247915659146276620
Yices20242348332.9548638.0524231553870118761180
cvc5-cvc5-xyz ne02373
(base -1)		145961.51146272.152373151685724402440
cvc502371146315.33146627.752371151485724602460
NeuroSym018682013.081804.17186813205484670300
SMTInterpol01834146666.19129836.271834107476078306270
z3-BooledASS ne01646
(base -692)		46341.6946547.89164698566197102690
bitwuzla-dandelion-base n0247821211.2121522.65247815639156376630
cvc5-cvc5-xyz-base n02374147049.79147364.242374151785724302430
z3-BooledASS-base n0233859785.6760079.692338152381527902770
(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 SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Bitwuzla0156511064.8311261.931565156502105020
bitwuzla-dandelion n01565
(base +2)		14465.9514662.721565156502105020
Yices20155317251.6817446.03155315530141050140
cvc5-cvc5-xyz ne01516
(base -1)		45028.4745220.10151615160991002990
cvc50151445865.8646058.2615141514010110021010
NeuroSym013201349.091201.411320132009128800
SMTInterpol01074115823.54104699.8410741074054110024210
z3-BooledASS ne0985
(base -538)		26381.4126504.4098598506301002860
bitwuzla-dandelion-base n0156311174.5811370.841563156304105040
z3-BooledASS-base n0152326567.2626757.59152315230921002900
cvc5-cvc5-xyz-base n0151745582.8045776.21151715170981002980
(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 SATSolved UNSATUnsolvedAbstainedTimeoutMemout
bitwuzla-dandelion n0921
(base +6)		10818.6310934.769210921221674220
Bitwuzla09149626.039741.529140914291674290
Yices2087031081.2731192.018700870731674730
cvc50857100449.48100569.498570857911669910
cvc5-cvc5-xyz ne0857
(base +0)		100933.05101052.058570857911669910
SMTInterpol076030842.6525136.43760076018816691770
z3-BooledASS ne0661
(base -154)		19960.2820043.49661066128716691290
NeuroSym0548663.99602.76548054837203200
bitwuzla-dandelion-base n091510036.6310151.829150915281674280
cvc5-cvc5-xyz-base n0857101466.99101588.048570857911669910
z3-BooledASS-base n081533218.4133322.10815081513316691330
(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 SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Bitwuzla022873765.904051.4922871463824033000
bitwuzla-dandelion n02287
(base -11)		4349.904635.3222871458829033000
Yices2022613002.943283.7522611481780035600
cvc5018912939.883173.7418911296595072600
cvc5-cvc5-xyz ne01887
(base +0)		2853.853086.3218871292595073000
NeuroSym018671933.981725.23186713205474470600
z3-BooledASS ne01507
(base -631)		1494.411679.12150791858963547500
SMTInterpol0144010736.704786.43144077067069110800
bitwuzla-dandelion-base n022983991.464278.0422981467831031900
z3-BooledASS-base n021381874.242137.7521381445693047900
cvc5-cvc5-xyz-base n018872852.573087.0218871292595073000
(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