SMT-COMP 2026

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2026

QF_ABV (Single Query Track)

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

Results were generated on 2026-07-25

Benchmarks: 1914
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
Bitwuzla019092430.902669.19190913275825050
bitwuzla-dandelion n01908
(base -1)		5161.335399.42190813275816060
Yices2019042995.133231.7719041326578100100
NeuroSym018682013.081804.171868132054846000
cvc5-cvc5-xyz ne01840
(base +0)		17817.1018045.3318401281559740740
cvc50183717378.4917607.2318371278559770770
SMTInterpol01446112569.50102300.06145097048046404380
z3-BooledASS ne01303
(base -586)		9988.7810149.1913038154886110240
bitwuzla-dandelion-base n019093285.783523.78190913275825050
z3-BooledASS-base n0188910166.8210400.6218891314575250250
cvc5-cvc5-xyz-base n0184017799.9218030.1318401281559740740
(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
Bitwuzla019092430.902669.19190913275825050
bitwuzla-dandelion n01908
(base -1)		5161.335399.42190813275816060
Yices2019042995.133231.7719041326578100100
NeuroSym018682013.081804.171868132054846000
cvc5-cvc5-xyz ne01840
(base +0)		17817.1018045.3318401281559740740
cvc50183717378.4917607.2318371278559770770
SMTInterpol01450117763.85107024.18145097048046404380
z3-BooledASS ne01303
(base -586)		9988.7810149.1913038154886110240
bitwuzla-dandelion-base n019093285.783523.78190913275825050
z3-BooledASS-base n0188910166.8210400.6218891314575250250
cvc5-cvc5-xyz-base n0184017799.9218030.1318401281559740740
(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
Bitwuzla013271154.811320.44132713270258520
bitwuzla-dandelion n01327
(base +0)		3478.873644.37132713270258520
Yices2013261243.531408.22132613260358530
NeuroSym013201349.091201.41132013200958500
cvc5-cvc5-xyz ne01281
(base +0)		13387.5013546.2712811281048585480
cvc50127813561.3613720.3112781278051585510
SMTInterpol097096694.8287847.5997097003595853360
z3-BooledASS ne0815
(base -499)		7601.087701.318158150514585150
bitwuzla-dandelion-base n013271886.372051.78132713270258520
z3-BooledASS-base n013147702.657865.3013141314015585150
cvc5-cvc5-xyz-base n0128113382.5413542.7912811281048585480
(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
Bitwuzla05821276.091348.7558205823132930
bitwuzla-dandelion n0581
(base -1)		1682.461755.0658105814132940
Yices205781751.601823.5557805787132970
cvc505593817.143886.925590559261329260
cvc5-cvc5-xyz ne0559
(base +0)		4429.614499.075590559261329260
NeuroSym0548663.99602.76548054837132900
z3-BooledASS ne0488
(base -87)		2387.702447.89488048897132990
SMTInterpol048021069.0419176.59480048010513291020
bitwuzla-dandelion-base n05821399.411472.0058205823132930
z3-BooledASS-base n05752464.162535.325750575101329100
cvc5-cvc5-xyz-base n05594417.384487.345590559261329260
(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
Bitwuzla018981034.641271.261898132157701600
Yices201891619.59854.381891132057102300
bitwuzla-dandelion n01870
(base -9)		780.601013.431870131755304400
NeuroSym018671933.981725.231867132054744300
cvc5017232032.712245.7617231180543019100
cvc5-cvc5-xyz ne01721
(base +1)		1992.552204.6317211178543019300
z3-BooledASS ne01277
(base -583)		465.56621.8812777964815835400
SMTInterpol011474419.202120.011147721426875900
bitwuzla-dandelion-base n01879755.16989.061879132155803500
z3-BooledASS-base n01860603.52832.871860129556505400
cvc5-cvc5-xyz-base n017201974.712188.4417201177543019400
(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