From d19f19c5d657fa663e7490861e59cf5f16f9a96b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 3 Jul 2026 19:50:19 -0700 Subject: [PATCH] bug fix Signed-off-by: Nikolaj Bjorner --- src/smt/seq_regex.cpp | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/smt/seq_regex.cpp b/src/smt/seq_regex.cpp index b2f038bbcf..c4005f9857 100644 --- a/src/smt/seq_regex.cpp +++ b/src/smt/seq_regex.cpp @@ -510,9 +510,10 @@ namespace smt { expr *e = ctx.bool_var2expr(lit.var()); VERIFY(str().is_in_re(e, s, r)); expr_ref_vector prefix(m); - expr *hd, *v, *tl = s; - while (str().is_concat(tl, hd, tl) && str().is_unit(hd, v) && m.is_value(v)) - prefix.push_back(v); + expr *hd, *v, *tl = s, *tl1; + while (str().is_concat(tl, hd, tl1) && str().is_unit(hd, v) && m.is_value(v)) + prefix.push_back(v), + tl = tl1; if (prefix.empty()) return false;