SMT-COMP 2026

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2026

AUFDTLIRA (Single Query Track)

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

Results were generated on 2026-07-25

Benchmarks: 1344
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
cvc501194591.00738.5211940119415001470
cvc5-cvc5-xyz ne01193
(base -1)		610.78758.7211930119315101480
z3-BooledASS ne01189
(base +2)		408.22554.1311890118915501220
SMTInterpol0100410496.386893.9310050100533902820
cvc5-cvc5-xyz-base n01194597.76745.8111940119415001470
z3-BooledASS-base n01187276.33421.8311870118715701250
(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
cvc501194591.00738.5211940119415001470
cvc5-cvc5-xyz ne01193
(base -1)		610.78758.7211930119315101480
z3-BooledASS ne01189
(base +2)		408.22554.1311890118915501220
SMTInterpol0100511701.097478.4710050100533902820
cvc5-cvc5-xyz-base n01194597.76745.8111940119415001470
z3-BooledASS-base n01187276.33421.8311870118715701250
(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
cvc501194591.00738.52119401194114910
cvc5-cvc5-xyz ne01193
(base -1)		610.78758.72119301193214920
z3-BooledASS01189
(base +2)		408.22554.13118901189614930
SMTInterpol0100511701.097478.471005010051901491660
cvc5-cvc5-xyz-base n01194597.76745.81119401194114910
z3-BooledASS-base n01187276.33421.83118701187814940
(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
cvc501190243.02390.02119001190015400
cvc5-cvc5-xyz ne01190
(base +0)		246.60394.13119001190015400
z3-BooledASS ne01187
(base +1)		235.83381.461187011873112600
SMTInterpol09803356.281615.1898009803832600
cvc5-cvc5-xyz-base n01190247.83395.34119001190015400
z3-BooledASS-base n01186237.47382.841186011862912900
(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