SMT-COMP 2026

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2026

UFDT (Single Query Track)

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

Results were generated on 2026-07-25

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

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24 seconds Performance (parallel)
cvc5cvc5cvc5cvc5cvc5

Sequential Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc5-cvc5-xyz ne0253
(base +0)		35759.6535793.652536019346004600
cvc5025336827.4436861.692536019346004600
z3-BooledASS ne0107
(base +0)		1179.621192.8810789960605190
SMTInterpol028812.85613.862812768506340
cvc5-cvc5-xyz-base n025336823.9736858.332536019346004600
z3-BooledASS-base n01071333.371346.5410789960604950
(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 ne0253
(base +0)		35759.6535793.652536019346004600
cvc5025336827.4436861.692536019346004600
z3-BooledASS ne0107
(base +0)		1179.621192.8810789960605190
SMTInterpol028812.85613.862812768506340
cvc5-cvc5-xyz-base n025336823.9736858.332536019346004600
z3-BooledASS-base n01071333.371346.5410789960604950
(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 ne060
(base +0)		28802.2028812.1060600165210
cvc506028807.7828817.5560600165210
z3-BooledASS ne08
(base +0)		1.792.8188053652350
SMTInterpol010.880.5911060652420
cvc5-cvc5-xyz-base n06028803.9128813.8360600165210
z3-BooledASS-base n081.632.6388053652350
(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 ne0193
(base +0)		6957.456981.551930193651460
cvc501938019.658044.151930193651460
z3-BooledASS ne099
(base +0)		1177.831190.0799099100514910
SMTInterpol027811.98613.28270271725141680
cvc5-cvc5-xyz-base n01938020.068044.501930193651460
z3-BooledASS-base n0991331.741343.9199099100514850
(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 ne0151
(base +3)		145.43163.911511150056200
cvc50148122.42140.651481147056500
z3-BooledASS ne0104
(base +0)		38.1150.85104896660300
SMTInterpol023182.5181.80231222766300
cvc5-cvc5-xyz-base n0148124.13142.281481147056500
z3-BooledASS-base n010438.1550.84104896560400
(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