From c50e6bdbb1b571d21b8143304bfb4f6da9139eb5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 30 Apr 2021 02:20:51 -0700 Subject: [PATCH] fix #5229 --- src/ast/rewriter/array_rewriter.cpp | 16 ++++++---------- 1 file changed, 6 insertions(+), 10 deletions(-) diff --git a/src/ast/rewriter/array_rewriter.cpp b/src/ast/rewriter/array_rewriter.cpp index c29bd91d7..8b1026f2e 100644 --- a/src/ast/rewriter/array_rewriter.cpp +++ b/src/ast/rewriter/array_rewriter.cpp @@ -336,8 +336,13 @@ br_status array_rewriter::mk_map_core(func_decl * f, unsigned num_args, expr * c // quantifier* lam = nullptr; for (unsigned i = 0; i < num_args; ++i) { - if (is_lambda(args[i])) { + if (is_lambda(args[i])) lam = to_quantifier(args[i]); + else if (m_util.is_const(args[i])) + continue; + else { + lam = nullptr; + break; } } if (lam) { @@ -351,15 +356,6 @@ br_status array_rewriter::mk_map_core(func_decl * f, unsigned num_args, expr * c lam = to_quantifier(a); args1.push_back(lam->get_expr()); } - else { - expr_ref_vector sel(m()); - sel.push_back(a); - unsigned n = lam->get_num_decls(); - for (unsigned i = 0; i < n; ++i) { - sel.push_back(m().mk_var(n - i - 1, lam->get_decl_sort(i))); - } - args1.push_back(m_util.mk_select(sel.size(), sel.data())); - } } result = m().mk_app(f, args1.size(), args1.data()); result = m().update_quantifier(lam, result);