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

[github-actions[bot]]

Date: 2026-06-10
Branch: c3
Commit: dbb3f70
Workflow Run: #27279442767
Files benchmarked: 299 (from tests/ostrich.zip, timeout 5 s/file, Z3 internal timeout 4 s)

Note: The c3 branch contains no standalone QF_S .smt2 files in the workspace tree. Benchmarks were sourced from tests/ostrich.zip (299 string/sequence theory files covering concat, replace, indexOf, regex, substrings, Parikh constraints, and more).

---

Summary

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

Both solvers achieve near-identical median performance (10 ms). nseq has a lower mean (30 ms vs 36 ms) but slightly more timeouts (23 vs 18), suggesting nseq is faster on the problems it solves but has coverage gaps on specific benchmark categories.

---

Performance Comparison

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

File	seq (ms)	nseq result
indexof.smt2	32	timeout (4083 ms)
concat_backjump_bug.smt2	70	timeout (4053 ms)
contains-4.smt2	8	timeout (4011 ms)
parikh-constraints.smt2	20	timeout (4011 ms)
str-lt.smt2	39	timeout (4011 ms)
str.to_int_5.smt2	211	timeout (4008 ms)
str.to_int_6.smt2	165	timeout (4008 ms)
word-equation-3.smt2	131	timeout (4008 ms)
prefix-suffix.smt2	9	timeout (4006 ms)
str.from_int_6.smt2	52	timeout (4006 ms)
str-lt2.smt2	55	timeout (4005 ms)

Affected categories: indexOf with variable indices, Parikh constraints, lexicographic ordering (str-lt), str.to_int/str.from_int with constraints, word equations, prefix/suffix with negation.

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

File	seq result	nseq (ms)
str.to_int_4.smt2	timeout (4019 ms)	10
bigSubstrIdx.smt2	timeout (4011 ms)	359
noodles-unsat3.smt2	timeout (4011 ms)	22
noodles-unsat7.smt2	timeout (4011 ms)	12
nonlinear.smt2	timeout (4010 ms)	22
noodles-unsat8.smt2	timeout (4008 ms)	14
concat-regex2.smt2	timeout (4006 ms)	10
indexof-2.smt2	timeout (4006 ms)	17
regexdeep.smt2	timeout (4006 ms)	118

nseq excels at: nonlinear word equations (noodles-*, nonlinear.smt2), deep regex (regexdeep.smt2, concat-regex2.smt2), large substring index queries, and certain str.to_int / indexOf in negative contexts.

---

Correctness

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

Both solvers are in full agreement on all benchmarks where both produce a definitive answer. No soundness issues detected.

---

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

The seq solver uses an iterative depth/length-increase strategy:

• smt.seq :increase-depth N — widens string unfolding depth to N
• smt.seq :increase-length var N — widens length bound for variable var

concat_backjump_bug.smt2 (seq=70 ms, nseq=timeout):

(smt.seq :increase-depth 2) → 7 decisions, 13 clauses
(smt.seq :increase-length var_8 2) → 26 decisions, 250 clauses
(smt.seq :increase-depth 5) → sat

indexof.smt2 (seq=32 ms, nseq=timeout):

(smt.seq :increase-depth 2,3,5) → sat (65 decisions, 350 clauses)

parikh-constraints.smt2 (seq=20 ms, nseq=timeout):

(smt.seq :increase-depth 2) → (smt.seq :increase-length value2 2) → sat

contains-4.smt2, prefix-suffix.smt2: Solved immediately (no depth/length iterations).

Interpretation: seq's bounded unfolding finds solutions at shallow depth for these cases. nseq (ZIPT-based) appears to have higher setup overhead for symbolic transducer encodings, making it slower even on shallow instances.

---

Generated by the QF_S Benchmark workflow. Reproduce: build Z3 from the c3 branch and run z3 smt.string_solver=seq|nseq -T:4 <file.smt2>. Benchmark suite: tests/ostrich.zip.

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

• expires on Jun 17, 2026, 2:15 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 #9818.