[QF_S Benchmark] seq vs nseq on ostrich suite (c3, 2026-06-06)

[github-actions[bot]]

Date: 2026-06-06 | Branch: c3 | Commit: eee5a9d
Workflow Run: #27048262889
Files benchmarked: 299 (all from tests/ostrich.zip, 5 s timeout / -T:4 internal)

---

Summary

Metric	seq	nseq
Files solved (sat/unsat)	274	261
Timeouts	18	38
Unknown	7	0
Median solve time	9 ms	9 ms
Mean solve time	29 ms	27 ms
Disagreements (sat ≠ unsat)	—	0 ✅

Both solvers agree on every file where both produce a definitive answer. seq solves 13 more files within the timeout; nseq solves 9 files that seq cannot.

---

Performance Comparison

seq-fast / nseq-slow — 26 files (seq < 2 s, nseq timed out)

Regression risk for nseq. Patterns: str.contains over concat, Parikh constraints, str.from_int/str.to_int, prefix/suffix, word equations, str.indexof with variable index, string ordering (str.<=, str.<), substr with variable length.

File	seq (ms)	nseq	seq result
contains-4.smt2	8	timeout	unsat
parikh-constraints.smt2	17	timeout	sat
prefix-suffix.smt2	11	timeout	unsat
str.from_int_6.smt2	58	timeout	sat
str.to_int_5.smt2	153	timeout	sat
str.to_int_6.smt2	115	timeout	sat
word-equation-3.smt2	102	timeout	unsat
concat_backjump_bug.smt2	57	timeout	sat
cvc_replace_28.smt2	1255	timeout	sat
prefix3.smt2	11	timeout	sat
cyclic-xy.smt2	12	timeout (10 ms)	unsat
failedProp.smt2	9	timeout (259 ms)	unsat
str-leq11.smt2	34	timeout (148 ms)	sat
str-lt.smt2	30	timeout (143 ms)	sat
str-lt2.smt2	68	timeout (189 ms)	unsat
indexof_var_sat.smt2	29	timeout (11 ms)	sat

(10 more files with similar patterns)

nseq-fast / seq-slow — 9 files (nseq < 2 s, seq timed out)

nseq advantages: non-linear word equations, deep regex nesting, integer-to-string (specific direction), large substring index.

File	seq	nseq (ms)	nseq result
str.to_int_4.smt2	timeout	9	unsat
nonlinear.smt2	timeout	18	unsat
noodles-unsat7.smt2	timeout	11	unsat
noodles-unsat3.smt2	timeout	19	unsat
noodles-unsat8.smt2	timeout	15	sat
concat-regex2.smt2	timeout	9	unsat
indexof-2.smt2	timeout	17	unsat
regexdeep.smt2	timeout	73	sat
bigSubstrIdx.smt2	timeout	280	sat

---

Correctness

✅ Zero disagreements — no file produced sat vs unsat across the two solvers.

seq returned unknown on 7 files where nseq returned sat (bug-58-replace-re.smt2, contains-7.smt2, contains-8.smt2, replace_empty_string.smt2, replace_shortest_sat.smt2, test-replace-regex3.smt2, pcp-1.smt2). These may be seq completeness gaps.

---

seq Trace Analysis (top seq-fast / nseq-slow)

Z3 statistics for representative cases

contains-4.smt2 (str.contains(y++y,z)=false when str.contains(y,z)=true): 1 conflict, 1 reduction — trivially resolved by rewrite rules. :rlimit-count 249

parikh-constraints.smt2 (nested contains/replace/substr/indexof): 41 conflicts, 160 reductions, 339 axiom additions, char2bit/Parikh encoding. Still fast despite heavy arithmetic involvement.

str.from_int_6.smt2 (integer-to-string, large case): 32 conflicts, 428 reductions, seq-int.to.str axiom ×1, heavy LP arithmetic. :rlimit-count 35643

word-equation-3.smt2 (5-variable word equation, unsat): 155 conflicts, 2859 reductions, 82 quantifier instantiations, 17 restarts. seq uses DPLL(T) + quantifiers. :rlimit-count 159895

---

To reproduce: build Z3 from c3 branch (commit eee5a9d) and run z3 smt.string_solver=seq|nseq -T:4 <file.smt2>. Benchmark suite: tests/ostrich.zip (299 files).

Generated by QF_S String Solver Benchmark · sonnet46 3.4M · ◷

• expires on Jun 13, 2026, 1:37 AM UTC

[github-actions[bot]]

This discussion has been marked as outdated by QF_S String Solver Benchmark.

A newer discussion is available at Discussion #9743.