SMT-COMP 2026

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2026

UFLIA (Unsat Core Track)

Competition results for the UFLIA logic in the Unsat Core Track. Chart

Results were generated on 2026-07-25

Benchmarks: 1172
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 UNSATUnsolvedAbstainedTimeoutMemout
cvc502851935828.165973.14116611666050
z3-BooledASS ne0262126
(base +473)		3364.153497.9610851085870790
SMTInterpol01659459359.817352.7572672644604300
UltimateEliminator+MathSAT01200251.33209.9611111161010
z3-BooledASS-base n02616532660.592794.2410821082900770
(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 UNSATUnsolvedAbstainedTimeoutMemout
cvc502851935828.165973.14116611666050
z3-BooledASS ne0262126
(base +473)		3364.153497.9610851085870790
SMTInterpol016622111174.978242.6072672644604300
UltimateEliminator+MathSAT01200251.33209.9611111161010
z3-BooledASS-base n02616532660.592794.2410821082900770
(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 UNSATUnsolvedAbstainedTimeoutMemout
cvc502851935828.165973.14116611666050
z3-BooledASS ne0262126
(base +473)		3364.153497.9610851085870790
SMTInterpol016622111174.978242.6072672644604300
UltimateEliminator+MathSAT01200251.33209.9611111161010
z3-BooledASS-base n02616532660.592794.2410821082900770
(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 UNSATUnsolvedAbstainedTimeoutMemout
cvc50277018774.83915.661136113603600
z3-BooledASS ne0260398
(base +286)		357.03489.491078107839100
SMTInterpol01616202126.081016.02693693347600
UltimateEliminator+MathSAT061158.5727.3010101156600
z3-BooledASS-base n0260112380.04512.681076107629400
(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