From 3a90de1cbe280c98046f6191d3ad2ee933346e52 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 24 Jul 2019 10:09:34 -0700 Subject: [PATCH] fix #2419 Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/array_rewriter.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ast/rewriter/array_rewriter.cpp b/src/ast/rewriter/array_rewriter.cpp index 311d849a7..5d2325d33 100644 --- a/src/ast/rewriter/array_rewriter.cpp +++ b/src/ast/rewriter/array_rewriter.cpp @@ -306,7 +306,7 @@ br_status array_rewriter::mk_map_core(func_decl * f, unsigned num_args, expr * c 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.append(num_indices, store_expr->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()); }