SMT-COMP 2026

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2026

AUFLIA (Unsat Core Track)

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

Results were generated on 2026-07-25

Benchmarks: 649
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
cvc50209554265.914345.79639639100100
z3-BooledASS ne017491
(base -120)		2938.663013.35602602470470
SMTInterpol0146819421.917348.355335331160850
UltimateEliminator+MathSAT024677.1934.201616633000
z3-BooledASS-base n0176112263.152337.57604604450450
(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
cvc50209554265.914345.79639639100100
z3-BooledASS ne017491
(base -120)		2938.663013.35602602470470
SMTInterpol0146819421.917348.355335331160850
UltimateEliminator+MathSAT024677.1934.201616633000
z3-BooledASS-base n0176112263.152337.57604604450450
(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
cvc50209554265.914345.79639639100100
z3-BooledASS ne017491
(base -120)		2938.663013.35602602470470
SMTInterpol0146819421.917348.355335331160850
UltimateEliminator+MathSAT024677.1934.201616633000
z3-BooledASS-base n0176112263.152337.57604604450450
(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
cvc5017854144.25218.2859459405500
z3-BooledASS ne016721
(base -66)		214.71287.9859359305600
SMTInterpol0134551639.92794.54502502314400
UltimateEliminator+MathSAT024677.1934.201616632100
z3-BooledASS-base n016787194.24267.1959459405500
(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