From dee8a9f308f06b78a89ca829a5f4a6ca928e18a6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 23 Sep 2019 02:56:31 -0700 Subject: [PATCH] remove more unsound rewrites #2575 Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.cpp | 10 ++-------- 1 file changed, 2 insertions(+), 8 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 29a326426..4cac29a85 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -1828,14 +1828,8 @@ br_status seq_rewriter::mk_re_loop(func_decl* f, unsigned num_args, expr* const* result = m_util.re.mk_loop(args[0], f->get_parameter(1).get_int(), f->get_parameter(1).get_int()); return BR_REWRITE1; } - // (loop (loop a lo hi) lo2) = (loop lo*lo2) - if (m_util.re.is_loop(args[0], a, lo, hi) && f->get_num_parameters() == 1) { - result = m_util.re.mk_loop(a, f->get_parameter(0).get_int() * lo); - return BR_REWRITE1; - } - // (loop (loop a lo) lo2 ..) = (loop lo*lo2) - if (m_util.re.is_loop(args[0], a, lo)) { - SASSERT(f->get_num_parameters() >= 1); + // (loop (loop a lo) lo2) = (loop lo*lo2) + if (m_util.re.is_loop(args[0], a, lo) && f->get_num_parameters() == 1) { result = m_util.re.mk_loop(a, f->get_parameter(0).get_int() * lo); return BR_REWRITE1; }