mirror of
https://github.com/Z3Prover/z3
synced 2026-08-07 14:32:06 +00:00
195a0486aa
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> |
||
|---|---|---|
| .. | ||
| d0-copy.smt2 | ||
| d1-square.smt2 | ||
| d2-tag-complement.smt2 | ||
| d3-block-end-2var.smt2 | ||
| d4a-mid-empty.smt2 | ||
| d4b-mid-ab.smt2 | ||
| d4c-mid-a-unsat.smt2 | ||
| d4d-mid-b-unsat.smt2 | ||
| d5-two-var-square.smt2 | ||
| d6-user-seed-unsat.smt2 | ||
| d7-cube.smt2 | ||
| d8-counting.smt2 | ||
| d9-commutation-unsat.smt2 | ||
| nseq-bug-len-coupling-min.smt2 | ||