SMT-COMP 2026

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2026

AUFDTNIRA (Single Query Track)

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

Results were generated on 2026-07-25

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

Winners

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

Sequential Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
z3-BooledASS ne0438
(base +1)		92.05146.04438043810701030
cvc50438675.44730.1343804381070490
cvc5-cvc5-xyz ne0438
(base +0)		681.17735.2043804381070490
SMTInterpol03421176.02594.64342034220302030
cvc5-cvc5-xyz-base n0438700.30754.3543804381070490
z3-BooledASS-base n043787.69141.11437043710801030
(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
z3-BooledASS ne0438
(base +1)		92.05146.04438043810701030
cvc50438675.44730.1343804381070490
cvc5-cvc5-xyz ne0438
(base +0)		681.17735.2043804381070490
SMTInterpol03421176.02594.64342034220302030
cvc5-cvc5-xyz-base n0438700.30754.3543804381070490
z3-BooledASS-base n043787.69141.11437043710801030
(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
z3-BooledASS0438
(base +1)		92.05146.044380438110610
cvc50438675.44730.134380438110600
cvc5-cvc5-xyz ne0438
(base +0)		681.17735.204380438110600
SMTInterpol03421176.02594.64342034297106970
cvc5-cvc5-xyz-base n0438700.30754.354380438110600
z3-BooledASS-base n043787.69141.114370437210610
(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
z3-BooledASS0438
(base +1)		92.05146.044380438310400
cvc5043794.24148.734370437575100
cvc5-cvc5-xyz ne0437
(base +0)		96.03149.894370437575100
SMTInterpol03421176.02594.643420342020300
z3-BooledASS-base n043787.69141.114370437510300
cvc5-cvc5-xyz-base n043796.40150.314370437575100
(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