SMT-COMP 2026

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2026

AUFBVDTNIA (Single Query Track)

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

Results were generated on 2026-07-25

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

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24 seconds Performance (parallel)
cvc5-cvc5-xyzcvc5-cvc5-xyzcvc5-cvc5-xyzcvc5-cvc5-xyzcvc5

Sequential Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc5-cvc5-xyz0280
(base +4)		607.22641.762801279200200
cvc502771382.371416.712770277230190
SMTInterpol02241601.871208.212240224760550
z3-BooledASS ne01
(base -276)		4.164.2811029901670
z3-BooledASS-base n0277409.60443.792771276230210
cvc5-cvc5-xyz-base n0276239.67273.922760276240200
(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
cvc5-cvc5-xyz0280
(base +4)		607.22641.762801279200200
cvc502771382.371416.712770277230190
SMTInterpol02241601.871208.212240224760550
z3-BooledASS ne01
(base -276)		4.164.2811029901670
z3-BooledASS-base n0277409.60443.792771276230210
cvc5-cvc5-xyz-base n0276239.67273.922760276240200
(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
z3-BooledASS ne01
(base +0)		4.164.28110029900
cvc5-cvc5-xyz01
(base +1)		90.2990.42110029900
SMTInterpol000.000.00000129910
cvc5000.000.00000129900
z3-BooledASS-base n014.214.35110029900
cvc5-cvc5-xyz-base n000.000.00000129900
(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
cvc5-cvc5-xyz0279
(base +3)		516.93551.352790279174170
cvc502771382.371416.712770277194170
SMTInterpol02241601.871208.212240224724510
z3-BooledASS ne00
(base -276)		0.000.0000029641650
cvc5-cvc5-xyz-base n0276239.67273.922760276204180
z3-BooledASS-base n0276405.39439.442760276204190
(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
cvc5027482.68116.57274027442200
cvc5-cvc5-xyz ne0266
(base -8)		81.05113.8426602661618160
SMTInterpol0194403.02183.661940194110500
z3-BooledASS ne01
(base -275)		4.164.2811012817100
z3-BooledASS-base n027694.99129.00276127502400
cvc5-cvc5-xyz-base n027486.09120.09274027442200
(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