[QF_S Benchmark] QF_S Benchmark: seq vs nseq — c3 branch (2026-06-10)

[github-actions[bot]]

Date: 2026-06-10 Branch: c3 Commit: 89a2ac1
Workflow Run: #27246388375
Benchmark source: tests/ostrich.zip (shipped in the c3 branch)
Files benchmarked: 299 (all files, timeout 5 s per file, Z3 internal timeout 4 s)

---

Summary

Metric	seq	nseq
Files solved (sat/unsat)	274	275
Timeouts	18	23
Unknown	7	1
Median solve time (solved files)	10 ms	11 ms
Mean solve time (solved files)	36 ms	37 ms
Disagreements (sat≠unsat)	—	0

Both solvers are extremely close in aggregate performance. nseq solves 1 more file than seq; seq has 5 fewer timeouts. The difference is within noise.

---

Performance Comparison

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

Potential regression risk for nseq:

File	seq (ms)	nseq (ms)	seq result
indexof.smt2	30	4113	sat
concat_backjump_bug.smt2	79	4057	sat
contains-4.smt2	10	4014	unsat
parikh-constraints.smt2	20	4011	sat
str.to_int_6.smt2	148	4009	sat
prefix-suffix.smt2	10	4008	unsat
str.to_int_5.smt2	193	4008	sat
str-lt.smt2	39	4006	sat
str-lt2.smt2	55	4006	unsat
str.from_int_6.smt2	53	4006	sat
word-equation-3.smt2	132	4006	unsat

Pattern: str.to_int/str.from_int conversions, string ordering (str-lt*), indexof, Parikh constraints, prefix/suffix/contains all challenge nseq.

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

nseq performance advantages:

File	seq (ms)	nseq (ms)	nseq result
str.to_int_4.smt2	4019	11	unsat
bigSubstrIdx.smt2	4014	362	sat
nonlinear.smt2	4013	23	unsat
noodles-unsat3.smt2	4013	23	unsat
noodles-unsat7.smt2	4013	14	unsat
noodles-unsat8.smt2	4011	20	sat
concat-regex2.smt2	4008	11	unsat
indexof-2.smt2	4006	19	unsat
regexdeep.smt2	4006	97	sat

Pattern: nonlinear string constraints (nonlinear.smt2, noodles-*), deep regex (regexdeep.smt2, concat-regex2.smt2), large substring indexing (bigSubstrIdx.smt2). The ZIPT-based nseq shows clear wins on complex regex and nonlinear string arithmetic.

---

Correctness

Disagreements (seq=sat vs nseq=unsat or vice versa): 0 ✅

Both solvers agree on all cases where both produce a definitive answer.

Near-disagreements (unknown vs sat/unsat)

File	seq result	nseq result
bug-58-replace-re.smt2	unknown	sat
contains-8.smt2	unknown	sat
replace_empty_string.smt2	unknown	sat
replace_shortest_sat.smt2	unknown	sat
test-replace-regex3.smt2	unknown	sat
pcp-1.smt2	unknown	timeout
contains-7.smt2	unknown	timeout

In all unknown vs sat cases, nseq provides the definitive answer — suggesting nseq handles incomplete rewrite cases better than seq.

---

seq Trace Analysis

Trace collection via -tr:seq is not supported in the Release build (option not recognized). A Debug build with tracing enabled would be needed for deeper analysis.

Top seq-fast/nseq-slow benchmark descriptions:

• indexof.smt2: str.indexof x0 "===" 0 with > n 0 — indexof with positive start
• concat_backjump_bug.smt2: QF_SLIA, CEGAR string model checking (Norn benchmark)
• contains-4.smt2: str.contains on doubled string, (= x (str.++ y y))
• prefix-suffix.smt2: Proves prefix+suffix implies equality (UNSAT)
• parikh-constraints.smt2: Parikh image constraints over string variables

---

Generated by the QF_S Benchmark workflow. To reproduce: build Z3 from c3 and run z3 smt.string_solver=seq|nseq -T:4 <file.smt2>. Full CSV available on request.

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

• expires on Jun 17, 2026, 1:50 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 #9809.