SMT-COMP 2026

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2026

QF_Strings (Single Query Track)

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

Results were generated on 2026-07-25

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

Logics:

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-Noodler07225
(base +2272)		5670.086571.967225400532204080220
OSTRICH0695190423.7491289.6669513838311368206820
cvc505299141852.09142524.835299340318962334023080
cvc5-cvc5-xyz ne05287
(base -5)		135401.18136067.245287338119062346023130
Z3-GEX ne05127
(base +27)		61673.2926065.09514633041842248708980
z3-BooledASS ne04977
(base +0)		56828.9857445.194977314618312656010900
cvc5-cvc5-xyz-base n05292142944.82143614.965292339618962341023080
Z3-GEX-base n0510060009.9560651.25510032681832253309630
z3-BooledASS-base n0497756309.8356926.334977314618312656010900
Z3-Noodler-base n0495369712.5570335.384953312218312680011100
(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-Noodler07225
(base +2272)		5670.086571.967225400532204080220
OSTRICH0695190423.7491289.6669513838311368206820
cvc505299141852.09142524.835299340318962334023080
cvc5-cvc5-xyz ne05287
(base -5)		135401.18136067.245287338119062346023130
Z3-GEX ne05146
(base +46)		114236.4839865.32514633041842248708980
z3-BooledASS ne04977
(base +0)		56828.9857445.194977314618312656010900
cvc5-cvc5-xyz-base n05292142944.82143614.965292339618962341023080
Z3-GEX-base n0510060009.9560651.25510032681832253309630
z3-BooledASS-base n0497756309.8356926.334977314618312656010900
Z3-Noodler-base n0495369712.5570335.384953312218312680011100
(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-Noodler04005
(base +883)		3839.124338.20400540050153613150
OSTRICH0383879839.1780320.0638383838018236131820
cvc503403113733.03114165.4134033403061736135910
cvc5-cvc5-xyz ne03381
(base -15)		111429.21111856.1933813381063936136060
Z3-GEX ne03304
(base +36)		105986.7834732.0533043304071636132870
z3-BooledASS ne03146
(base +0)		52906.7653297.9031463146087436134680
cvc5-cvc5-xyz-base n03396114112.90114544.0233963396062436135910
Z3-GEX-base n0326857543.7557955.8132683268075236133420
z3-BooledASS-base n0314652419.9952810.9831463146087436134680
Z3-Noodler-base n0312265729.6866123.8931223122089836134880
(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-Noodler03220
(base +1389)		1830.962233.763220032206440750
OSTRICH0311310584.5610969.6031130311311344071130
cvc5-cvc5-xyz ne01906
(base +10)		23971.9724211.051906019061320440713200
cvc50189628119.0628359.421896018961330440713300
Z3-GEX ne01842
(base +10)		8249.705133.27184201842138444076100
z3-BooledASS ne01831
(base +0)		3922.224147.29183101831139544076210
cvc5-cvc5-xyz-base n0189628831.9129070.941896018961330440713300
Z3-GEX-base n018322466.202695.44183201832139444076200
z3-BooledASS-base n018313889.844115.35183101831139544076210
Z3-Noodler-base n018313982.874211.49183101831139544076210
(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-Noodler07201
(base +2531)		2819.073717.587201399632053864600
OSTRICH064039331.4810114.426403332430790123000
Z3-GEX ne04934
(base +140)		19464.718783.494934313418001566113300
cvc5048343240.593842.6248343031180326277300
cvc5-cvc5-xyz ne04830
(base +2)		3328.173924.6548303018181226277700
z3-BooledASS ne04720
(base +0)		5493.046072.704720291218081566134700
cvc5-cvc5-xyz-base n048283282.213880.7548283025180326277900
Z3-GEX-base n047945478.076075.624794297318211570126900
z3-BooledASS-base n047205464.056044.174720291318071566134700
Z3-Noodler-base n046705187.715768.744670286018101569139400
(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