SMT-COMP 2026

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2026

QF_Equality (Unsat Core Track)

Competition results for the QF_Equality division in the Unsat Core Track. Chart

Results were generated on 2026-07-25

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

Logics:

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24 seconds Performance (parallel)
Yices2Yices2-Yices2Yices2

Sequential Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved UNSATUnsolvedAbstainedTimeoutMemout
Yices20137097754.37879.90101410140000
z3-BooledASS ne0136754
(base +0)		1155.151279.36101410140000
OpenSMT (min-ucore)010568342358.9942472.5188888812601260
OpenSMT0984051029.391155.50101410140000
SMTInterpol0944576715.713097.04100510059000
plat-smt0931812017.352117.64811811120210
cvc50797112130.822254.93101410140000
z3-BooledASS-base n01367541155.331279.78101410140000
(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
Yices20137097754.37879.90101410140000
z3-BooledASS ne0136754
(base +0)		1155.151279.36101410140000
OpenSMT (min-ucore)010568342358.9942472.5188888812601260
OpenSMT0984051029.391155.50101410140000
SMTInterpol0944576715.713097.04100510059000
plat-smt0931812017.352117.64811811120210
cvc50797112130.822254.93101410140000
z3-BooledASS-base n01367541155.331279.78101410140000
(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
Yices20137097754.37879.90101410140000
z3-BooledASS ne0136754
(base +0)		1155.151279.36101410140000
OpenSMT (min-ucore)010568342358.9942472.5188888812601260
OpenSMT0984051029.391155.50101410140000
SMTInterpol0944576715.713097.04100510059000
plat-smt0931812017.352117.64811811120210
cvc50797112130.822254.93101410140000
z3-BooledASS-base n01367541155.331279.78101410140000
(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
Yices20132770287.17411.55100510050900
z3-BooledASS ne0132494
(base +0)		537.03660.10100510050900
OpenSMT098403650.67775.72100610060800
SMTInterpol0901336184.582791.0999899801600
plat-smt084658398.76497.51800800021400
cvc5074709630.85753.551004100401000
OpenSMT (min-ucore)0523881469.791545.92615615039900
z3-BooledASS-base n0132494538.28661.55100510050900
(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