SMT-COMP 2026

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2026

QF_BVFP (Single Query Track)

Competition results for the QF_BVFP logic in the Single Query Track. Chart

Results were generated on 2026-07-25

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

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 n0504
(base +0)		679.72742.635042272771010
Bitwuzla05041367.631429.855042272771010
cvc5-cvc5-xyz ne0503
(base +0)		4036.184098.535032272762020
cvc505034041.424104.125032272762020
colibri204292247.632300.59429201228760170
z3-BooledASS ne048
(base -436)		12.5818.49480484570210
COLIBRI84351464.711519.09443210233620130
bitwuzla-dandelion-base n0504776.88839.455042272771010
cvc5-cvc5-xyz-base n05034054.284117.145032272762020
z3-BooledASS-base n048413164.1713225.16484218266210200
(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 n0504
(base +0)		679.72742.635042272771010
Bitwuzla05041367.631429.855042272771010
cvc5-cvc5-xyz ne0503
(base +0)		4036.184098.535032272762020
cvc505034041.424104.125032272762020
colibri204292247.632300.59429201228760170
z3-BooledASS ne048
(base -436)		12.5818.49480484570210
COLIBRI84351464.711519.09443210233620130
bitwuzla-dandelion-base n0504776.88839.455042272771010
cvc5-cvc5-xyz-base n05034054.284117.145032272762020
z3-BooledASS-base n048413164.1713225.16484218266210200
(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
bitwuzla-dandelion n0227
(base +0)		134.32162.572272270027800
Bitwuzla0227787.72815.792272270027800
cvc5-cvc5-xyz ne0227
(base +0)		1325.211353.242272270027800
cvc502271326.121354.392272270027800
colibri202011145.201170.0020120102627820
z3-BooledASS ne00
(base -218)		0.000.0000022727870
COLIBRI8210294.30321.072182108927800
bitwuzla-dandelion-base n0227237.77265.922272270027800
cvc5-cvc5-xyz-base n02271338.711367.082272270027800
z3-BooledASS-base n02182958.342985.522182180927890
(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 n0277
(base +0)		545.40580.072770277022800
Bitwuzla0277579.91614.062770277022800
cvc5-cvc5-xyz ne0276
(base +0)		2710.972745.292760276122810
cvc502762715.302749.732760276122810
colibri202281102.431130.59228022849228150
COLIBRI02241170.071197.56224022453228130
z3-BooledASS ne048
(base -218)		12.5818.4948048229228130
bitwuzla-dandelion-base n0277539.11573.542770277022800
cvc5-cvc5-xyz-base n02762715.572750.062760276122810
z3-BooledASS-base n026610205.8410239.64266026611228100
(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
bitwuzla-dandelion n0500
(base +1)		355.79418.205002272730500
Bitwuzla0498363.11424.464982262720700
cvc5-cvc5-xyz ne0475
(base +0)		1056.431114.9847521326203000
cvc504731018.591077.3247321226103200
colibri20421276.99328.78421197224493500
z3-BooledASS ne048
(base -398)		12.5818.49480483976000
COLIBRI8430476.08529.79438209229491800
bitwuzla-dandelion-base n0499320.64382.534992262730600
cvc5-cvc5-xyz-base n04751060.921120.0347521326203000
z3-BooledASS-base n04461104.511159.6844620823805900
(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