From 195a0486aaaf0fd7c7a680d8e38b4db02d675f96 Mon Sep 17 00:00:00 2001 From: Margus Veanes Date: Thu, 2 Jul 2026 17:32:49 +0300 Subject: [PATCH] tests(wordeq-ladder): add minimal nseq spurious-unsat reproducer Distilled companion to d5-two-var-square.smt2: x.x in (Sigma* "a" Sigma*) with |x|=1 is sat (x="a"), but smt.string_solver=nseq returns unsat. Trigger = regex membership over a str.++ of variable terms + an exact length (str.len = k, or a word equation forcing lengths); default/seq/z3str3 are correct. nseq is a c3-branch-only solver; master is unaffected. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- .../nseq-bug-len-coupling-min.smt2 | 23 +++++++++++++++++++ 1 file changed, 23 insertions(+) create mode 100644 tests/wordeq-ladder/nseq-bug-len-coupling-min.smt2 diff --git a/tests/wordeq-ladder/nseq-bug-len-coupling-min.smt2 b/tests/wordeq-ladder/nseq-bug-len-coupling-min.smt2 new file mode 100644 index 0000000000..482b2bf92b --- /dev/null +++ b/tests/wordeq-ladder/nseq-bug-len-coupling-min.smt2 @@ -0,0 +1,23 @@ +; nseq-bug-len-coupling-min MINIMAL SOUNDNESS REPRODUCER (nseq returns spurious unsat) +; Companion to d5-two-var-square.smt2 (which triggers the same bug via a word equation). +; Membership: x.x in (Sigma* "a" Sigma*) with |x| = 1 +; Expected: sat (x="a" -> "aa" contains "a", and |x|=1) +; z3 file.smt2 -> sat (correct) +; z3 smt.string_solver=nseq file.smt2 -> unsat (WRONG; c3-branch nseq solver only, master unaffected) +; Trigger = regex membership over a str.++ of variable terms + an EXACT length (str.len = k, +; or a word equation that forces lengths). Inequalities (>=) or no length coupling are fine; +; default / seq / z3str3 are all correct. Same class as the L2-04 length/Parikh coupling bug. + +(set-logic QF_SLIA) +(set-info :smt-lib-version 2.6) +(set-info :status sat) +(set-info :category "crafted") +(set-info :source |Minimal reproducer for an nseq (smt.string_solver=nseq, c3 branch) spurious-unsat soundness bug, distilled from the lookaround membership benchmarks (resharp-node data/lookarounds.json, IPv6 exactly-one-"::" query). Companion to d5-two-var-square.smt2.|) +(declare-fun x () String) + +; x.x must contain "a" and |x| = 1 +(assert (str.in_re (str.++ x x) + (re.++ (re.* re.allchar) (re.++ (str.to_re "a") (re.* re.allchar))))) +(assert (= (str.len x) 1)) + +(check-sat)