From 0ee79182d4e0cc4613cd58baa26988b496015411 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 11 Apr 2020 14:09:09 -0700 Subject: [PATCH] fix #3911 Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.cpp | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 2ef7ea69d..d6ee47b50 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -1892,10 +1892,15 @@ br_status seq_rewriter::mk_re_loop(func_decl* f, unsigned num_args, expr* const* case 1: np = f->get_num_parameters(); lo2 = np > 0 ? f->get_parameter(0).get_int() : 0; - hi2 = np > 1 ? f->get_parameter(1).get_int() : 0; + hi2 = np > 1 ? f->get_parameter(1).get_int() : lo2; + // (loop a 0 0) = "" if (np == 2 && lo2 > hi2) { - result = m_util.re.mk_loop(args[0], lo2, lo2); - return BR_REWRITE1; + result = m_util.re.mk_empty(m().get_sort(args[0])); + return BR_DONE; + } + if (np == 2 && hi2 == 0) { + result = m_util.re.mk_to_re(m_util.str.mk_empty(m_util.re.to_seq(m().get_sort(args[0])))); + return BR_DONE; } // (loop (loop a lo) lo2) = (loop lo*lo2) if (m_util.re.is_loop(args[0], a, lo) && np == 1) { @@ -1907,11 +1912,6 @@ br_status seq_rewriter::mk_re_loop(func_decl* f, unsigned num_args, expr* const* result = m_util.re.mk_loop(a, lo2 * lo, hi2 * hi); return BR_REWRITE1; } - // (loop a 0 0) = "" - if (np == 2 && hi2 == 0) { - result = m_util.re.mk_to_re(m_util.str.mk_empty(m_util.re.to_seq(m().get_sort(args[0])))); - return BR_DONE; - } // (loop a 1 1) = a if (np == 2 && lo2 == 1 && hi2 == 1) { result = args[0];