SMT-COMP 2026

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2026

AUFBVFPDTNIRA (Single Query Track)

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

Results were generated on 2026-07-25

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

Winners

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

Sequential Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc5-cvc5-xyz ne060
(base +0)
56.4863.8560060570570
cvc506099.31106.756006057000
z3-BooledASS ne00
(base -53)
0.000.0000011701130
cvc5-cvc5-xyz-base n060101.26108.676006057000
z3-BooledASS-base n0539.6316.1553053640640
(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 ne060
(base +0)
56.4863.8560060570570
cvc506099.31106.756006057000
z3-BooledASS ne00
(base -53)
0.000.0000011701130
cvc5-cvc5-xyz-base n060101.26108.676006057000
z3-BooledASS-base n0539.6316.1553053640640
(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-xyz060
(base +0)
56.4863.856006005700
cvc506099.31106.756006005700
z3-BooledASS ne00
(base -53)
0.000.000006057560
cvc5-cvc5-xyz-base n060101.26108.676006005700
z3-BooledASS-base n0539.6316.155305375770
(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
cvc5-cvc5-xyz059
(base +1)
22.2329.475905905800
cvc505812.8920.085805854500
z3-BooledASS ne00
(base -53)
0.000.00000411300
cvc5-cvc5-xyz-base n05813.1020.245805854500
z3-BooledASS-base n0539.6316.155305306400
(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