SMT-COMP 2026

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2026

QF_SNIA (Single Query Track)

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

Results were generated on 2026-07-25

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

Winners

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

Sequential Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc5-cvc5-xyz ne070
(base +0)
11.2820.05707000000
Z3-Noodler ne070
(base +0)
11.5020.22707000000
cvc507011.4120.31707000000
Z3-GEX ne070
(base +0)
11.7320.50707000000
z3-BooledASS ne070
(base +0)
11.8620.54707000000
OSTRICH07012.3721.07707000000
cvc5-cvc5-xyz-base n07011.4120.17707000000
Z3-Noodler-base n07011.5320.30707000000
Z3-GEX-base n07011.7320.51707000000
z3-BooledASS-base n07012.1120.77707000000
(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 ne070
(base +0)
11.2820.05707000000
Z3-Noodler ne070
(base +0)
11.5020.22707000000
cvc507011.4120.31707000000
Z3-GEX ne070
(base +0)
11.7320.50707000000
z3-BooledASS ne070
(base +0)
11.8620.54707000000
OSTRICH07012.3721.07707000000
cvc5-cvc5-xyz-base n07011.4120.17707000000
Z3-Noodler-base n07011.5320.30707000000
Z3-GEX-base n07011.7320.51707000000
z3-BooledASS-base n07012.1120.77707000000
(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
cvc5-cvc5-xyz ne070
(base +0)
11.2820.05707000000
Z3-Noodler ne070
(base +0)
11.5020.22707000000
cvc507011.4120.31707000000
Z3-GEX ne070
(base +0)
11.7320.50707000000
z3-BooledASS ne070
(base +0)
11.8620.54707000000
OSTRICH07012.3721.07707000000
cvc5-cvc5-xyz-base n07011.4120.17707000000
Z3-Noodler-base n07011.5320.30707000000
Z3-GEX-base n07011.7320.51707000000
z3-BooledASS-base n07012.1120.77707000000
(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-xyz ne070
(base +0)
11.2820.05707000000
Z3-Noodler ne070
(base +0)
11.5020.22707000000
cvc507011.4120.31707000000
Z3-GEX ne070
(base +0)
11.7320.50707000000
z3-BooledASS ne070
(base +0)
11.8620.54707000000
OSTRICH07012.3721.07707000000
cvc5-cvc5-xyz-base n07011.4120.17707000000
Z3-Noodler-base n07011.5320.30707000000
Z3-GEX-base n07011.7320.51707000000
z3-BooledASS-base n07012.1120.77707000000
(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