SMT-COMP 2026

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2026

AUFBVDTNIRA (Single Query Track)

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

Results were generated on 2026-07-25

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

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24 seconds Performance (parallel)
cvc5cvc5-cvc5cvc5

Sequential Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc5-cvc5-xyz ne0532
(base +15)		10765.9610832.57532053237203720
cvc50517839.23902.95517051738703590
SMTInterpol05026597.964338.44502050240203880
z3-BooledASS ne034
(base -475)		224.49228.653403487003980
cvc5-cvc5-xyz-base n05171060.881124.60517051738703590
z3-BooledASS-base n0509192.27254.68509050939502780
(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-xyz ne0532
(base +15)		10765.9610832.57532053237203720
cvc50517839.23902.95517051738703590
SMTInterpol05026597.964338.44502050240203880
z3-BooledASS ne034
(base -475)		224.49228.653403487003980
cvc5-cvc5-xyz-base n05171060.881124.60517051738703590
z3-BooledASS-base n0509192.27254.68509050939502780
(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-xyz ne0532
(base +15)		10765.9610832.575320532340323400
cvc50517839.23902.955170517355323520
SMTInterpol05026597.964338.445020502370323670
z3-BooledASS ne034
(base -475)		224.49228.6534034838323670
cvc5-cvc5-xyz-base n05171060.881124.605170517355323520
z3-BooledASS-base n0509192.27254.685090509363322460
(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
cvc50513132.21195.3351305132836300
cvc5-cvc5-xyz ne0507
(base -6)		136.57199.16507050726371260
SMTInterpol04702822.841169.974700470642800
z3-BooledASS ne032
(base -476)		32.2236.123203245741500
cvc5-cvc5-xyz-base n0513136.82199.9251305132836300
z3-BooledASS-base n0508165.41227.69508050810728900
(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