SMT-COMP 2026

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2026

QF_Equality (Single Query Track)

Competition results for the QF_Equality division in the Single Query Track. Chart

Results were generated on 2026-07-25

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

Logics:

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24 seconds Performance (parallel)
Yices2Yices2Yices2Yices2Yices2

Sequential Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Yices201404246.30420.2614046097950000
cvc5-cvc5-xyz ne01404
(base +0)		1094.401266.0514046097950000
OpenSMT014041111.911286.0214046097950000
cvc5014041157.811331.3914046097950000
z3-BooledASS ne01404
(base +0)		1197.801370.0414046097950000
OpenSMT-SMTS-seq ne01404
(base +0)		1323.791483.7014046097950000
SMTInterpol013788270.243853.01137860976926010
plat-smt011021507.761643.781102467635230020
cvc5-cvc5-xyz-base n014041081.681254.3314046097950000
OpenSMT-SMTS-seq-base n014041134.441308.0814046097950000
z3-BooledASS-base n014041209.001381.8114046097950000
(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 SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Yices201404246.30420.2614046097950000
cvc5-cvc5-xyz ne01404
(base +0)		1094.401266.0514046097950000
OpenSMT014041111.911286.0214046097950000
cvc5014041157.811331.3914046097950000
z3-BooledASS ne01404
(base +0)		1197.801370.0414046097950000
OpenSMT-SMTS-seq ne01404
(base +0)		1323.791483.7014046097950000
SMTInterpol013788270.243853.01137860976926010
plat-smt011021507.761643.781102467635230020
cvc5-cvc5-xyz-base n014041081.681254.3314046097950000
OpenSMT-SMTS-seq-base n014041134.441308.0814046097950000
z3-BooledASS-base n014041209.001381.8114046097950000
(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

SAT Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Yices20609102.59178.076096090079500
z3-BooledASS ne0609
(base +0)		135.73210.106096090079500
OpenSMT0609160.97236.576096090079500
cvc5-cvc5-xyz ne0609
(base +0)		174.80249.216096090079500
cvc50609176.30251.766096090079500
OpenSMT-SMTS-seq ne0609
(base +0)		234.41306.566096090079500
SMTInterpol06091200.13561.096096090079500
plat-smt046796.45154.324674670093700
z3-BooledASS-base n0609137.38212.396096090079500
OpenSMT-SMTS-seq-base n0609164.62239.856096090079500
cvc5-cvc5-xyz-base n0609174.82249.666096090079500
(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 SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Yices20795143.71242.197950795060900
cvc5-cvc5-xyz ne0795
(base +0)		919.601016.847950795060900
OpenSMT0795950.941049.447950795060900
cvc50795981.511079.637950795060900
z3-BooledASS ne0795
(base +0)		1062.071159.957950795060900
OpenSMT-SMTS-seq ne0795
(base +0)		1089.381177.147950795060900
SMTInterpol07697070.103291.9276907692660910
plat-smt06351411.311489.456350635276720
cvc5-cvc5-xyz-base n0795906.861004.677950795060900
OpenSMT-SMTS-seq-base n0795969.821068.237950795060900
z3-BooledASS-base n07951071.621169.427950795060900
(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 SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Yices201404246.30420.2614046097950000
z3-BooledASS ne01399
(base +0)		570.40741.9713996097900500
OpenSMT01397695.39868.5813976097880700
cvc5-cvc5-xyz ne01396
(base +0)		645.11815.7413966097870800
OpenSMT-SMTS-seq ne01396
(base -1)		850.401018.9013966097870800
cvc501395639.41811.8513956097860900
SMTInterpol013666189.172840.85136660975703800
plat-smt01094415.77550.701094467627031000
z3-BooledASS-base n01399574.95747.0613996097900500
OpenSMT-SMTS-seq-base n01397708.09880.8213976097880700
cvc5-cvc5-xyz-base n01396641.18812.8513966097870800
(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