[QF_S Benchmark] QF_S Benchmark: seq vs nseq (c3 branch, 299 files)

[github-actions[bot]]

QF_S Benchmark: seq vs nseq

Date: 2026-06-05
Branch: c3
Commit: 9de196b
Workflow Run: #27017039481
Benchmark source: tests/ostrich.zip
Files benchmarked: 299 (all files, timeout 5 s/file)

---

⚠️ Correctness Alert

1 soundness bug found: nseq returns unsat on substr_const_len_sat.smt2, which is annotated :status sat and correctly solved as sat by seq.

---

Summary

Metric	seq	nseq
Solved (sat/unsat)	274 / 299	267 / 299
Timeouts	25	31
Median solve time (solved)	8 ms	8 ms
Mean solve time (solved)	37 ms	42 ms
Disagreements (sat≠unsat)	—	1
Both agree	253	—
Only seq terminates	20	—
Only nseq terminates	14	—
Both timeout	11	—

---

seq-fast / nseq-slow (seq < 2 s, nseq timeout): 19 files

File	seq (ms)	nseq result
simple-concat-4.smt2	33	timeout
prefix3.smt2	11	timeout
concat_backjump_bug.smt2	80	timeout
cvc_replace_28.smt2	1667	timeout
contains-4.smt2	7	timeout
parikh-constraints.smt2	19	timeout
str.from_int_6.smt2	67	timeout
str.to_int_6.smt2	152	timeout
prefix-suffix.smt2	7	timeout
str.to_int_5.smt2	218	timeout
concat-regex4.smt2	3908	timeout
str-leq7.smt2	49	timeout
word-equation-3.smt2	131	timeout
str-lt.smt2	56	timeout
str-lt2.smt2	124	timeout
str-leq12.smt2	60	timeout
str-leq11.smt2	67	timeout
norn-benchmark-9f.smt2	12	timeout
failedProp.smt2	12	timeout (~226ms)

nseq-fast / seq-slow (nseq < 2 s, seq timeout): 13 files

File	nseq (ms)	seq result
str.to_int_4.smt2	12	timeout
bigSubstrIdx.smt2	417	timeout
nonlinear.smt2	24	timeout
noodles-unsat3.smt2	22	timeout
noodles-unsat7.smt2	11	timeout
concat-regex2.smt2	9	timeout
indexof-2.smt2	26	timeout
regexdeep.smt2	103	timeout
replace_empty_string.smt2	~9	unknown (fast)
replace_shortest_sat.smt2	~9	unknown (fast)
bug-58-replace-re.smt2	~9	unknown (fast)
test-replace-regex3.smt2	~7	unknown (fast)
contains-8.smt2	~9	unknown (fast)

---

Correctness: DISAGREEMENT

substr_const_len_sat.smt2 — seq=sat ✓, nseq=unsat ✗

(set-info :status sat)
(declare-fun a () String)
(declare-fun b () 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.in_re b (re.union (str.to_re "hh") (str.to_re "bb"))))
(assert (= (str.substr a i j) b))
(assert (= i 0))
(assert (= j 2))
(check-sat)

Witness: a="hhhbbb", b="hh" → str.substr("hhhbbb",0,2) = "hh". nseq fails to find this model.

Root cause hypothesis: Incorrect propagation in the str.substr + disjunctive regex handler in ZIPT. The verbose trace shows nseq cycling through assignments and exhausting all paths.

---

Both Solvers Timeout (11 files)

artur-unsat-we, artur-unsat, contains-7, nikolai-unsat, noodles-unsat, noodles-unsat2, noodles-unsat5, noodles-unsat6, noodles-unsat9, pcp-1, substring-bug2

---

Analysis

• Overall: both solvers perform well on the majority of benchmarks (253 agreements at sub-10ms median). seq has a slight edge: 274 vs 267 solved, 25 vs 31 timeouts.
• seq strengths: str.from_int/str.to_int conversions, lexicographic ordering (str-leq/str-lt), Parikh constraints, backjump-heavy concatenation problems.
• nseq strengths: nonlinear arithmetic + string combinations, deep regex (regexdeep), certain str.substr / indexof problems.
• Invalid model: noodles-unsat8.smt2 — nseq generates an invalid model (flagged by model_validate=true).
• Action items: (1) Fix soundness bug in substr_const_len_sat, (2) investigate str-leq/str-lt support in nseq, (3) investigate str.from_int/str.to_int timeouts, (4) fix invalid model in noodles-unsat8.

---

Generated by the QF_S Benchmark workflow. To reproduce: build Z3 from c3 and run python3 scripts/compare_seq_solvers.py tests/ostrich/ --z3 ./z3 --timeout 5.

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

• expires on Jun 12, 2026, 1:51 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 #9739.