[QF_S Benchmark] QF_S Benchmark: seq vs nseq — OSTRICH suite (299 files, 5s timeout)

[github-actions[bot]]

Date: 2026-06-09 | Branch: c3 | Commit: ad17fe7 | Run: #27177227977
Benchmark source: tests/ostrich.zip | Files: 299 | Timeout: 5 s wall-clock / 4 s Z3 internal | Build: Release -O3

---

Summary

Metric	seq	nseq
Files solved (sat/unsat)	274	263
Genuine timeouts	18	29
Crashes (UNREACHABLE assertion)	0	7
unknown returned	7	0
Median solve time (solved files)	11 ms	11 ms
Mean solve time (solved files)	38 ms	35 ms
Disagreements (sat≠unsat)	—	0 ✅

---

🚨 Crashes — nseq Assertion Violations

Seven benchmark files trigger UNREACHABLE() at src/smt/seq/seq_nielsen.cpp:3686 with nseq. All 7 are solved correctly by seq.

File	seq	seq ms	nseq	Trigger
cyclic-xy.smt2	unsat	15	crash	cyclic word eq xy=yx + regex
indexof_const_index_sat.smt2	sat	34	crash	str.indexof const index
indexof_const_index_unsat.smt2	unsat	83	crash	str.indexof const index (unsat)
indexof_var_sat.smt2	sat	48	crash	str.indexof variable index
indexof_var_unsat.smt2	unsat	155	crash	str.indexof variable index (unsat)
substr_const_len_unsat.smt2	unsat	16	crash	str.substr const length
substr_var_sat.smt2	sat	22	crash	str.substr variable index/length

Crash location: UNREACHABLE() at seq_nielsen.cpp:3686 — sigma-pair decomposition in the ZIPT engine when handling str.indexof/str.substr constraints not yet fully supported.

Minimal reproducer:

(declare-fun a () String)
(declare-fun i () Int)(declare-fun j () Int)
(assert (str.in_re a (re.union (str.to_re "hhhbbb") (str.to_re "bhhh"))))
(assert (= (str.indexof a "hhh" j) i))
(assert (= i 1))(assert (= j 0))
(check-sat)

Run: z3 smt.string_solver=nseq <file>

---

Performance Comparison

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

File	seq ms	nseq ms	seq	nseq
cvc_replace_28.smt2	1786	4086	sat	timeout
concat_backjump_bug.smt2	81	4050	sat	timeout
contains-4.smt2	10	4013	unsat	timeout
str.from_int_6.smt2	82	4009	sat	timeout
parikh-constraints.smt2	22	4006	sat	timeout
prefix-suffix.smt2	10	4006	unsat	timeout
str.to_int_5.smt2	210	4006	sat	timeout
str.to_int_6.smt2	163	4006	sat	timeout
word-equation-3.smt2	134	4006	unsat	timeout
str-leq7.smt2	43	730	sat	timeout

Other seq-fast/nseq-slow: concat-regex4, str-lt, str-lt2, str-leq11, str-leq12, failedProp, failedProp2, norn-benchmark-9f, plus the 6 crash files above.

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

File	seq ms	nseq ms	seq	nseq
str.to_int_4.smt2	4019	11	timeout	unsat
bigSubstrIdx.smt2	4011	388	timeout	sat
nonlinear.smt2	4011	23	timeout	unsat
noodles-unsat3.smt2	4011	24	timeout	unsat
noodles-unsat7.smt2	4011	16	timeout	unsat
concat-regex2.smt2	4008	12	timeout	unsat
indexof-2.smt2	4008	20	timeout	unsat
noodles-unsat8.smt2	4008	18	timeout	sat
regexdeep.smt2	4006	101	timeout	sat

---

Completeness: seq unknown → nseq sat (5 files)

nseq is strictly more complete for these str.replace/regex operations:

File	seq	nseq
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

---

Correctness

Disagreements (sat≠unsat between solvers): 0 ✅

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

---

seq Trace Notes (seq-fast cases)

• contains-4.smt2 (10ms unsat): seq's rewriter fires str.contains monotonicity under concatenation immediately. nseq misses this simplification (4013ms timeout).
• prefix-suffix.smt2 (10ms unsat): seq recognises the prefix/suffix algebraic identity directly. nseq times out (4006ms).
• parikh-constraints.smt2 (22ms sat): seq uses iterative depth/length bounds (increase-depth 2, increase-length 2). nseq lacks Parikh image reasoning (4006ms timeout).
• concat_backjump_bug.smt2 (81ms sat): seq solves via bounded model checking at depth 5 with regex intersection. nseq times out (4050ms).

---

To reproduce: build Z3 from c3 branch (-DCMAKE_BUILD_TYPE=Release) and run z3 smt.string_solver=seq|nseq -T:4 <file.smt2>. Benchmarks from tests/ostrich.zip.

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

• expires on Jun 16, 2026, 1:45 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 #9793.