mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-11 17:46:20 +00:00
Code Activity

tests(wordeq-ladder): add minimal nseq spurious-unsat reproducer

Browse source 
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>
This commit is contained in:
Margus Veanes 2026-07-02 17:32:49 +03:00
parent 0b9b6b5869
commit 195a0486aa
1 changed files with 23 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

23
tests/wordeq-ladder/nseq-bug-len-coupling-min.smt2 Normal file
View file

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