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

[github-actions[bot]]

Date: 2026-06-12
Branch: c3
Commit: f126b60
Workflow Run: #27388126663
Files benchmarked: 299 (from tests/ostrich.zip, timeout 5 s per file, Z3 internal timeout 4 s)
Z3 version: 4.17.0 — build hash f126b603690007f08707515917a7737081a1c809

---

Summary

Metric	seq	nseq
Files solved (sat/unsat)	274	275
Timeouts	18	23
Median solve time (solved files)	10 ms	10 ms
Mean solve time (solved files)	44 ms	26 ms
Disagreements (sat≠unsat)	—	1 ⚠️

Both solvers perform similarly on this benchmark set, with identical median times (10 ms). The nseq solver has a lower mean time (26 ms vs 44 ms), suggesting it handles many cases slightly faster. However, nseq has 5 more timeouts (23 vs 18), and one critical correctness disagreement was detected.

---

⚠️ Correctness Disagreement

1 file where seq says sat but nseq says unsat (potential bug in nseq)

File	seq	nseq	Expected
indexof_const_index_sat.smt2	sat	unsat ❌	sat

The seq solver correctly returns sat with model a = "bhhh" (indexof "bhhh" for "hhh" starting at 0 is 1). The nseq solver incorrectly returns unsat and emits repetitive ZIPT trace output before concluding — indicating a bug in nseq's handling of str.indexof with a constant start position.

(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))

---

Performance Comparison

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

File	seq (ms)	nseq	seq result
parikh-constraints.smt2	20	timeout	sat
concat_backjump_bug.smt2	72	timeout	sat
word-equation-3.smt2	120	timeout	unsat
contains-4.smt2	9	timeout	unsat
str-leq5.smt2	66	timeout	sat
str-lt.smt2	70	timeout	sat
str.to_int_5.smt2	185	timeout	sat
str.to_int_6.smt2	156	timeout	sat
prefix-suffix.smt2	10	timeout	unsat
str.from_int_6.smt2	54	timeout	sat

Patterns: nseq lacks efficient support for str.<=/str.< ordering, str.to_int/str.from_int, and simple prefix/suffix/contains reasoning.

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

File	seq	nseq (ms)	nseq result
str.to_int_4.smt2	timeout	10	unsat
concat-regex2.smt2	timeout	10	unsat
noodles-unsat3.smt2	timeout	23	unsat
nonlinear.smt2	timeout	22	unsat
indexof-2.smt2	timeout	61	unsat
regexdeep.smt2	timeout	123	sat
bigSubstrIdx.smt2	timeout	353	sat

Patterns: nseq excels at nonlinear constraints, deep regex, and Parikh-image unsat proofs.

---

seq Trace Analysis

The -tr:seq trace option is not available in this build. Formula-level analysis of top seq-fast/nseq-slow cases:

• contains-4.smt2 (9 ms): UNSAT — str.contains y z, x = y++y, not str.contains x z. Trivially UNSAT by monotonicity. nseq exhausts its 4 s budget.
• prefix-suffix.smt2 (10 ms): UNSAT — proves prefixof(a,b) ∧ suffixof(b,a) ⟹ a=b. seq has direct lemmas; nseq does not.
• parikh-constraints.smt2 (20 ms): Composition of str.contains, str.replace, str.substr, str.indexof. nseq cannot efficiently handle this chain.
• str-leq5.smt2 (66 ms): str.len x = 4 and str.<= x "cba". nseq lacks lexicographic order reasoning.
• concat_backjump_bug.smt2 (72 ms): QF_SLIA with 13 variables, multiple regex intersections. seq uses Nielsen backjumping; nseq ZIPT loops.

---

Raw Data

First 50 entries of benchmark-results.csv

file,seq_result,seq_time_ms,nseq_result,nseq_time_ms
03_track_1.smt2,unsat,9,unsat,8
03_track_10.smt2,unsat,8,unsat,8
03_track_11.smt2,unsat,12,unsat,11
1234.corecstrs.readable.smt2,sat,13,sat,12
adt.smt2,sat,10,sat,11
adt2.smt2,sat,10,sat,11
all-quantifiers.smt2,unsat,12,unsat,13
artur-unsat-common-prefix.smt2,unsat,10,unsat,12
artur-unsat-we.smt2,timeout,4006,timeout,4030
artur-unsat.smt2,timeout,4010,timeout,4033
bigSubstrIdx.smt2,timeout,4013,sat,353
brackets-regex.smt2,sat,8,sat,8
bug-56-replace-bug2.smt2,sat,11,sat,14
bug-58-replace-re.smt2,unknown,10,sat,11
chars.smt2,sat,9,sat,9
chars2.smt2,sat,10,sat,10
chars3.smt2,sat,11,sat,11
concat-001.smt2,sat,16,sat,11
concat-002.smt2,sat,9,sat,9
concat-003.smt2,sat,9,sat,8
concat-004-unsat.smt2,unsat,8,unsat,8
concat-005-unsat.smt2,unsat,8,unsat,8
concat-006.smt2,sat,9,sat,10
concat-007.smt2,sat,9,sat,9
concat-008.smt2,sat,9,sat,9
concat-009.smt2,sat,9,sat,9
concat-010.smt2,sat,9,sat,9
concat-empty.smt2,unsat,8,unsat,8
concat-regex.smt2,sat,14,sat,13
concat-regex2.smt2,timeout,4011,unsat,10
concat-regex3.smt2,sat,23,sat,18
concat-regex4.smt2,sat,3800,timeout,4027
concat.smt2,sat,19,sat,13
concat2.smt2,sat,9,sat,9
concat_backjump_bug.smt2,sat,72,timeout,4053
concat_sat.smt2,sat,12,sat,10
concat_unsat.smt2,unsat,9,unsat,10
contains-1.smt2,sat,11,sat,11
contains-2.smt2,sat,10,sat,10
contains-3.smt2,unsat,8,unsat,8
contains-4.smt2,unsat,9,timeout,4013
contains-5.smt2,sat,10,sat,11
contains-6.smt2,sat,10,sat,11
contains-7.smt2,unknown,19,timeout,4016
contains-8.smt2,unknown,11,sat,11
cvc_replace_185.smt2,unsat,9,unsat,9
cvc_replace_28.smt2,sat,3589,sat,226
cvc_replace_4062.smt2,sat,55,sat,1675
cyclic-xy.smt2,unsat,15,unsat,17
indexof_const_index_sat.smt2,sat,26,unsat,85

---

Generated by the QF_S Benchmark workflow. To reproduce: check out the c3 branch, build Z3 in Release mode, and run z3 smt.string_solver=seq|nseq -T:4 <file.smt2> on files from tests/ostrich.zip.

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

• expires on Jun 19, 2026, 1:53 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 #9841.