SMT-COMP 2026

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2026

QF_SLIA (Single Query Track)

Competition results for the QF_SLIA logic in the Single Query Track. Chart

Results were generated on 2026-07-25

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

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24 seconds Performance (parallel)
Z3-NoodlerZ3-NoodlerZ3-NoodlerZ3-NoodlerZ3-Noodler

Sequential Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Z3-Noodler05123
(base +585)		3856.884496.28512333481775230220
OSTRICH0494184505.6285122.6549413218172320502050
cvc504865132234.62132852.4148653165170028102810
cvc5-cvc5-xyz ne04839
(base -19)		128898.45129508.4148393143169630703000
Z3-GEX ne04711
(base +27)		53733.8621388.3847303038169241603750
z3-BooledASS ne04562
(base +0)		52825.8553390.5545622881168158405660
cvc5-cvc5-xyz-base n04858132873.79133488.9848583158170028802810
Z3-GEX-base n0468456730.8357319.9646843002168246204400
z3-BooledASS-base n0456252290.7952856.0045622881168158405660
Z3-Noodler-base n0453865608.4966179.2245382857168160805860
(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
Z3-Noodler05123
(base +585)		3856.884496.28512333481775230220
OSTRICH0494184505.6285122.6549413218172320502050
cvc504865132234.62132852.4148653165170028102810
cvc5-cvc5-xyz ne04839
(base -19)		128898.45129508.4148393143169630703000
Z3-GEX04730
(base +46)		106297.0435188.6147303038169241603750
z3-BooledASS ne04562
(base +0)		52825.8553390.5545622881168158405660
cvc5-cvc5-xyz-base n04858132873.79133488.9848583158170028802810
Z3-GEX-base n0468456730.8357319.9646843002168246204400
z3-BooledASS-base n0456252290.7952856.0045622881168158405660
Z3-Noodler-base n0453865608.4966179.2245382857168160805860
(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
Z3-Noodler03348
(base +491)		3457.203874.65334833480151783150
OSTRICH0321877182.3677586.3832183218014517831450
cvc503165113075.27113477.8231653165019817831980
cvc5-cvc5-xyz ne03143
(base -15)		111062.63111460.0631433143022017832130
Z3-GEX03038
(base +36)		102095.8632455.2530383038032517832870
z3-BooledASS ne02881
(base +0)		50323.9150682.2428812881048217834670
cvc5-cvc5-xyz-base n03158113469.66113871.0831583158020517831980
Z3-GEX-base n0300255695.2556073.9730023002036117833420
z3-BooledASS-base n0288149831.8850190.1328812881048217834670
Z3-Noodler-base n0285763044.5363405.5428572857050617834870
(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
Z3-Noodler01775
(base +94)		399.67621.631775017756336550
OSTRICH017237323.267536.27172301723583365580
cvc50170019159.3619374.59170001700813365810
cvc5-cvc5-xyz ne01696
(base -4)		17835.8118048.34169601696853365850
Z3-GEX ne01692
(base +10)		4201.182733.36169201692893365870
z3-BooledASS ne01681
(base +0)		2501.942708.311681016811003365980
cvc5-cvc5-xyz-base n0170019404.1319617.90170001700813365810
Z3-GEX-base n016821035.591245.99168201682993365970
z3-BooledASS-base n016812458.912665.871681016811003365980
Z3-Noodler-base n016812563.962773.681681016811003365980
(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
Z3-Noodler05114
(base +844)		1446.782084.8651143339177513100
Z3-GEX ne04589
(base +199)		19002.198496.134589290316861953800
cvc5044262579.213130.26442627971629072000
cvc5-cvc5-xyz ne04413
(base -7)		2560.073104.86441327801633073300
OSTRICH044077398.207934.83440727101697073900
z3-BooledASS ne04319
(base +0)		4892.215422.444319265616631880900
cvc5-cvc5-xyz-base n044202661.483209.30442027911629072600
Z3-GEX-base n043904854.865401.974390271416762273400
z3-BooledASS-base n043194863.215394.084319265716621880900
Z3-Noodler-base n042704606.475137.674270260516652185500
(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