SMT-COMP 2026

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2026

QF_UF (Incremental Track)

Competition results for the QF_UF logic in the Incremental Track. Chart

Results were generated on 2026-07-25

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

Winners

Parallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24 seconds Performance (parallel)
plat-smt--plat-smt

Parallel Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedUnsolvedAbstainedTimeoutMemout
plat-smt0985349.7049.700577000
Yices20985351.2251.220577000
cvc509853173.29173.290577000
SMTInterpol09853740.03740.030577000
OpenSMT09848447.43447.430577000
z3-BooledASS ne00
(base +0)		3.454.390577000
z3-BooledASS-base n000.000.000577000
(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 ScoreSolvedUnsolvedAbstainedTimeoutMemout
plat-smt0985349.7049.700577000
Yices20985351.2251.220577000
cvc509853173.29173.290577000
SMTInterpol09851708.31708.310576100
OpenSMT09844218.18218.180575200
z3-BooledASS ne00
(base +0)		3.454.390577000
z3-BooledASS-base n000.000.000577000
(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