[QF_S Benchmark] seq vs nseq on 299 OSTRICH benchmarks — 2026-06-07, commit 206569c

[github-actions[bot]]

Date: 2026-06-07
Branch: c3
Commit: 206569c
Workflow Run: #27078943769
Files benchmarked: 299 (from tests/ostrich.zip; timeout 5 s per file, Z3 internal -T:4)

Note: No explicit QF_S .smt2 files were found in the c3 branch outside tests/ostrich.zip. All 299 benchmarks are from the OSTRICH string/word-equation test suite (word equations + regular constraints).

---

Summary

Metric	seq	nseq
Files solved (sat/unsat)	274 / 299 (91.6 %)	263 / 299 (87.9 %)
Timeouts	18	29
Assertion violations (crashes)	0	7
Unknown	7	0
Median solve time (solved files)	11 ms	11 ms
Mean solve time (solved files)	37 ms	31 ms
Disagreements (sat ≠ unsat)	—	0

Both solvers agree on all files where both return a definitive sat/unsat answer. ✅

---

⚠️ Critical: nseq Assertion Violations

nseq hits UNEXPECTED CODE WAS REACHED at src/smt/seq/seq_nielsen.cpp:3686 on 7 files involving str.indexof or str.substr. Exit code 114. seq handles all 7 correctly.

File	seq result	seq time (ms)
cyclic-xy.smt2	unsat	15
indexof_const_index_sat.smt2	sat	27
indexof_const_index_unsat.smt2	unsat	59
indexof_var_sat.smt2	sat	37
indexof_var_unsat.smt2	unsat	126
substr_const_len_unsat.smt2	unsat	16
substr_var_sat.smt2	sat	21

---

Performance Comparison

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

File	seq (ms)	nseq (ms)	seq result
cvc_replace_28.smt2	1630	4094	sat
concat_backjump_bug.smt2	74	4056	sat
contains-4.smt2	11	4016	unsat
str.to_int_5.smt2	195	4008	sat
parikh-constraints.smt2	21	4006	sat
prefix-suffix.smt2	10	4006	unsat
str.from_int_6.smt2	75	4006	sat
str.to_int_6.smt2	150	4006	sat
word-equation-3.smt2	126	4006	unsat
str-leq7.smt2	28	607	sat

Patterns: str.to_int/str.from_int, Parikh constraints, prefix/suffix word equations, contains, string comparison (str-leq).

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

File	seq (ms)	nseq (ms)	nseq result
str.to_int_4.smt2	4019	11	unsat
noodles-unsat7.smt2	4013	13	unsat
bigSubstrIdx.smt2	4011	370	sat
concat-regex2.smt2	4011	11	unsat
noodles-unsat3.smt2	4011	23	unsat
nonlinear.smt2	4010	22	unsat
noodles-unsat8.smt2	4009	18	sat
indexof-2.smt2	4006	19	unsat
regexdeep.smt2	4006	93	sat

Patterns: nonlinear word equations (noodles-*, nonlinear), str.to_int, concat+regex, deep regex, str.indexof.

---

Correctness

Disagreements (sat ≠ unsat): 0 — both solvers agree on every file where both return a definitive answer. ✅

nseq More Decisive (seq=unknown, nseq=sat) — 5 files

nseq returns sat on 5 files where seq gives up with unknown: bug-58-replace-re.smt2, contains-8.smt2, replace_empty_string.smt2, replace_shortest_sat.smt2, test-replace-regex3.smt2. These involve str.replace_re_all and related operations.

---

seq Trace Analysis

The -tr:seq flag is not supported in this Z3 build. No traces were collected.

---

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

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

• expires on Jun 14, 2026, 1:55 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 #9756.