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

[github-actions[bot]]

Date: 2026-06-06
Branch: c3 | Commit: eee5a9d | Z3 Version: 4.17.0
Workflow Run: #27062514353
Benchmark source: tests/ostrich.zip (c3 branch) | Files: 299 | Timeout: 5 s

---

Summary

Metric	seq	nseq
Solved (sat/unsat)	274	261
Timeouts	18	38
Unknown (incomplete)	7	0
Median solve time	11 ms	10 ms
Mean solve time	37 ms	36 ms
sat≠unsat disagreements	—	0 ✅

Both solvers agree on all cases where both return sat/unsat. seq solves 13 more files overall, but nseq handles 9 files that seq cannot. Median/mean times are nearly identical.

nseq returns 0 unknown results, while seq returns unknown on 7 files (nseq finds sat): bug-58-replace-re.smt2, contains-7/8.smt2, pcp-1.smt2, replace_empty_string.smt2, replace_shortest_sat.smt2, test-replace-regex3.smt2 -- indicating improved completeness in nseq for replace/contains.

---

Performance: seq-fast / nseq-slow (26 files)

Regression risks for nseq -- seq solves in < 2 s, nseq times out.

File	seq (ms)	nseq	seq result
contains-4.smt2	9	TO	unsat
parikh-constraints.smt2	27	TO	sat
concat_backjump_bug.smt2	83	TO	sat
prefix-suffix.smt2	10	TO	unsat
prefix3.smt2	13	TO	sat
word-equation-3.smt2	129	TO	unsat
str.to_int_5.smt2	197	TO	sat
str.to_int_6.smt2	146	TO	sat
str.from_int_6.smt2	80	TO	sat
cvc_replace_28.smt2	1652	TO	sat
indexof_var_sat.smt2	44	TO	sat
indexof_var_unsat.smt2	160	TO	unsat
indexof_const_index_sat.smt2	33	TO	sat
indexof_const_index_unsat.smt2	74	TO	unsat
failedProp.smt2	10	TO	unsat
failedProp2.smt2	11	TO	unsat
str-lt.smt2	40	TO	sat
str-lt2.smt2	90	TO	unsat
str-leq7.smt2	30	TO	sat
str-leq11.smt2	46	TO	sat
str-leq12.smt2	59	TO	sat
norn-benchmark-9f.smt2	11	TO	unsat
cyclic-xy.smt2	15	TO	unsat
simple-concat-4.smt2	13	TO	sat
substr_var_sat.smt2	21	TO	sat
substr_const_len_unsat.smt2	15	TO	unsat

Performance: nseq-fast / seq-slow (9 files)

nseq shows a performance advantage here.

File	seq	nseq (ms)	nseq result
str.to_int_4.smt2	TO	10	unsat
concat-regex2.smt2	TO	10	unsat
noodles-unsat7.smt2	TO	12	unsat
noodles-unsat8.smt2	TO	17	sat
indexof-2.smt2	TO	21	unsat
nonlinear.smt2	TO	22	unsat
noodles-unsat3.smt2	TO	23	unsat
regexdeep.smt2	TO	104	sat
bigSubstrIdx.smt2	TO	363	sat

---

Correctness

sat≠unsat disagreements: 0. Both solvers agree on all definitive results. ✅

seq returns unknown on 5 files where nseq finds sat (improved completeness in nseq):

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

---

seq Solver Traces (seq-fast/nseq-slow cases)

seq uses iterative-deepening + DPLL with string-length unfolding:

• contains-4 (9 ms, unsat): Direct unit-propagation, no unfolding needed.
• parikh-constraints (27 ms, sat): depth 2 -> length value2 2 -> sat in 41 decisions.
• concat_backjump_bug (83 ms, sat): depth 2 -> length var_9 2 -> depth 5 -> sat in 113 decisions.
• prefix-suffix (10 ms, unsat): 3 clauses, 0 conflicts -- trivially unsat.
• prefix3 (13 ms, sat): 1216 initial clauses from preprocessing; 13 decisions to sat.
• cyclic-xy (15 ms, unsat): depth 2->3, length x 4 -> unsat in 3 rounds.

nseq lacks the depth-bounded unfolding used by seq on these patterns.

---

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

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

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