From baeaa84bdea22d16edb4c6eb3e8c36f7c01f98e8 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 25 Jun 2026 20:26:35 -0700 Subject: [PATCH] have it create string ranges Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.cpp | 11 ++++------- 1 file changed, 4 insertions(+), 7 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index dcb2a30fcc..71ad42efb0 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -4132,12 +4132,8 @@ br_status seq_rewriter::mk_re_range(expr* lo, expr* hi, expr_ref& result) { if (max_length(hi) == std::make_pair(true, rational(0))) is_empty = true; if (!is_empty) { - if (str().is_string(lo, slo)) { - if (slo.length() != 1) - is_empty = true; - else - clo = slo[0]; - } + if (str().is_string(lo, slo) && slo.length() == 1) + clo = slo[0]; else if (str().is_unit(lo, lo1) && m_util.is_const_char(lo1, clo)) ; else @@ -4159,8 +4155,9 @@ br_status seq_rewriter::mk_re_range(expr* lo, expr* hi, expr_ref& result) { if (clo > chi) is_empty = true; // Singleton: re.range "a" "a" → str.to_re "a" + verbose_stream() << "mk_re_range: " << clo << " " << chi << " is_empty: " << is_empty << "\n"; if (clo == chi) { - result = re().mk_to_re(str().mk_string(slo)); + result = re().mk_to_re(str().mk_string(zstring(clo))); return BR_DONE; }