SMT-COMP 2026

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2026

ALIA (Unsat Core Track)

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

Results were generated on 2026-07-25

Benchmarks: 154
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
cvc508156849.846867.13135135190140
SMTInterpol06653909.722905.78108108460260
z3-BooledASS ne066
(base -20)
1133.991135.871414140010
UltimateEliminator+MathSAT0527.9212.6266148000
z3-BooledASS-base n0863.265.4718181360770
(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
cvc508156849.846867.13135135190140
SMTInterpol06725755.163685.59108108460260
z3-BooledASS ne066
(base -20)
1133.991135.871414140010
UltimateEliminator+MathSAT0527.9212.6266148000
z3-BooledASS-base n0863.265.4718181360770
(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
cvc508156849.846867.13135135190140
SMTInterpol06725755.163685.59108108460260
z3-BooledASS ne066
(base -20)
1133.991135.871414140010
UltimateEliminator+MathSAT0527.9212.6266148000
z3-BooledASS-base n0863.265.4718181360770
(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
cvc5073781.9095.7611211224000
SMTInterpol0538397.95292.798989115400
z3-BooledASS ne066
(base -20)
2.353.951313137400
UltimateEliminator+MathSAT0527.9212.6266148000
z3-BooledASS-base n0863.265.471818577900
(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