[QF_S Benchmark] seq vs nseq on 299 ostrich benchmarks — c3 branch (2026-06-07)

[github-actions[bot]]

Date: 2026-06-07
Branch: c3 · Commit: 206569c · Z3 version: 4.17.0
Workflow Run: #27092906519
Files benchmarked: 299 (from tests/ostrich.zip; 5 s shell timeout, 4 s Z3 timeout)

---

Summary

Metric	seq	nseq
Files solved (sat/unsat)	274	263
Timeouts	18	36
unknown (gave up)	5	0
Median solve time (solved files)	11 ms	11 ms
Mean solve time (solved files)	37 ms	33 ms
Disagreements (sat≠unsat)	—	0 ✅

seq solves 11 more files overall; both solvers are equally fast on the benchmark median. nseq has 2× more timeouts but zero soundness disagreements.

---

Performance Comparison

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

File	seq (ms)	nseq result
cvc_replace_28.smt2	1626	timeout
concat_backjump_bug.smt2	74	timeout
contains-4.smt2	9	timeout
str.from_int_6.smt2	76	timeout
parikh-constraints.smt2	22	timeout
prefix-suffix.smt2	10	timeout
str.to_int_5.smt2	195	timeout
str.to_int_6.smt2	147	timeout
word-equation-3.smt2	129	timeout
str-leq7.smt2	28	timeout
str-lt.smt2	53	timeout
str-leq11/12.smt2	41–51	timeout
failedProp.smt2	11	timeout
norn-benchmark-9f.smt2	11	timeout
indexof_var_sat/unsat.smt2	44–137	timeout
cyclic-xy.smt2	16	timeout
(+8 more)		timeout

Patterns: nseq has coverage gaps in str.to_int/str.from_int, string ordering (str-leq/str-lt), Parikh constraints, and indexof/substr with variable indices.

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

File	nseq (ms)	seq result
str.to_int_4.smt2	11	timeout
noodles-unsat3.smt2	24	timeout
noodles-unsat7.smt2	13	timeout
nonlinear.smt2	25	timeout
concat-regex2.smt2	11	timeout
indexof-2.smt2	19	timeout
noodles-unsat8.smt2	18	timeout
regexdeep.smt2	100	timeout
bigSubstrIdx.smt2	369	timeout

Patterns: nseq (ZIPT) excels on nonlinear word equations, complex regex membership, and certain int-to-string conversions.

---

Correctness

Zero sat/unsat disagreements across all 299 files. ✅

seq returned unknown on 5 files where nseq said sat:
bug-58-replace-re, contains-8, replace_empty_string, replace_shortest_sat, test-replace-regex3 — all involve replace/contains with regex patterns.

---

seq Trace Analysis

Verbose traces (-v:3) on top seq-fast/nseq-slow cases show seq using bounded depth/length search:

concat_backjump_bug: (smt.seq :increase-depth 2) → (smt.seq :increase-length var_9 2) → sat (74ms)
cyclic-xy:           (smt.seq :increase-depth 2) → (smt.seq :increase-length x 4)    → unsat (16ms)

nseq's ZIPT graph-propagation handles nonlinear cases better (nonlinear.smt2: unsat in 25ms vs seq timeout), but lacks seq's backjump optimization for simpler bounded problems.

---

Raw Data (interesting cases)

Click to expand CSV rows for seq/nseq divergences

file,seq_result,seq_time_ms,nseq_result,nseq_time_ms
bigSubstrIdx.smt2,timeout,4013,sat,369
concat-regex2.smt2,timeout,4008,unsat,11
concat-regex4.smt2,sat,3730,timeout,4030
concat_backjump_bug.smt2,sat,74,timeout,4054
contains-4.smt2,unsat,9,timeout,4013
cvc_replace_28.smt2,sat,1626,timeout,4097
cyclic-xy.smt2,unsat,16,timeout,12
failedProp.smt2,unsat,11,timeout,178
failedProp2.smt2,unsat,12,timeout,169
indexof-2.smt2,timeout,4008,unsat,19
indexof_const_index_sat.smt2,sat,28,timeout,13
indexof_const_index_unsat.smt2,unsat,70,timeout,17
indexof_var_sat.smt2,sat,44,timeout,14
indexof_var_unsat.smt2,unsat,137,timeout,14
nonlinear.smt2,timeout,4010,unsat,25
noodles-unsat3.smt2,timeout,4014,unsat,24
noodles-unsat7.smt2,timeout,4011,unsat,13
noodles-unsat8.smt2,timeout,4008,sat,18
norn-benchmark-9f.smt2,unsat,11,timeout,175
parikh-constraints.smt2,sat,22,timeout,4006
prefix-suffix.smt2,unsat,10,timeout,4006
regexdeep.smt2,timeout,4006,sat,100
str-leq7.smt2,sat,28,timeout,633
str-leq11.smt2,sat,51,timeout,197
str-leq12.smt2,sat,41,timeout,198
str-lt.smt2,sat,53,timeout,202
str-lt2.smt2,unsat,57,timeout,197
str.from_int_6.smt2,sat,76,timeout,4009
str.to_int_4.smt2,timeout,4019,unsat,11
str.to_int_5.smt2,sat,195,timeout,4006
str.to_int_6.smt2,sat,147,timeout,4006
substr_const_len_unsat.smt2,unsat,15,timeout,13
substr_var_sat.smt2,sat,21,timeout,13
word-equation-3.smt2,unsat,129,timeout,4006

---

To reproduce: build Z3 from c3 and run z3 smt.string_solver=seq|nseq -T:10 <file.smt2>. Files from tests/ostrich.zip.

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

• expires on Jun 14, 2026, 1:17 PM UTC

[github-actions[bot]]

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

A newer discussion is available at Discussion #9760.