From e51b5fd99c10319584230d13e57f9bbe6e0fbd18 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 3 Mar 2019 13:10:11 -0800 Subject: [PATCH] fix t154 regression Signed-off-by: Nikolaj Bjorner --- src/ast/array_decl_plugin.cpp | 1 + src/ast/rewriter/array_rewriter.cpp | 12 +++++++++--- 2 files changed, 10 insertions(+), 3 deletions(-) diff --git a/src/ast/array_decl_plugin.cpp b/src/ast/array_decl_plugin.cpp index 7975a4d61..396f93973 100644 --- a/src/ast/array_decl_plugin.cpp +++ b/src/ast/array_decl_plugin.cpp @@ -127,6 +127,7 @@ func_decl * array_decl_plugin::mk_const(sort * s, unsigned arity, sort * const * return nullptr; } if (!m_manager->compatible_sorts(get_array_range(s), domain[0])) { + SASSERT(false); m_manager->raise_exception("invalid const array definition, sort mismatch between array range and argument"); return nullptr; } diff --git a/src/ast/rewriter/array_rewriter.cpp b/src/ast/rewriter/array_rewriter.cpp index 8ff6dd654..f5798dede 100644 --- a/src/ast/rewriter/array_rewriter.cpp +++ b/src/ast/rewriter/array_rewriter.cpp @@ -270,15 +270,21 @@ br_status array_rewriter::mk_map_core(func_decl * f, unsigned num_args, expr * c values.push_back(to_app(a)->get_arg(num_indices+1)); } } - ptr_buffer new_args; - new_args.push_back(m_util.mk_map(f, arrays.size(), arrays.c_ptr())); if (store_expr) { + ptr_buffer new_args; + new_args.push_back(m_util.mk_map(f, arrays.size(), arrays.c_ptr())); new_args.append(num_indices, to_app(args[0])->get_args() + 1); new_args.push_back(m().mk_app(f, values.size(), values.c_ptr())); result = m().mk_app(get_fid(), OP_STORE, new_args.size(), new_args.c_ptr()); } else { - result = m_util.mk_const_array(m().get_sort(args[0]), new_args.back()); + expr_ref value(m().mk_app(f, values.size(), values.c_ptr()), m()); + sort* s0 = m().get_sort(args[0]); + unsigned sz = get_array_arity(s0); + ptr_vector domain; + for (unsigned i = 0; i < sz; ++i) domain.push_back(get_array_domain(s0, i)); + sort_ref s(m_util.mk_array_sort(sz, domain.c_ptr(), m().get_sort(value)), m()); + result = m_util.mk_const_array(s, value); } return BR_REWRITE2; }