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>
