From ebb7d60c75a0963eefa374af235a8f12a02d3e0b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 9 Dec 2019 07:50:57 +0300 Subject: [PATCH] fix #2792 Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/array_rewriter.cpp | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/src/ast/rewriter/array_rewriter.cpp b/src/ast/rewriter/array_rewriter.cpp index 4994ba6b1..9f7b1662f 100644 --- a/src/ast/rewriter/array_rewriter.cpp +++ b/src/ast/rewriter/array_rewriter.cpp @@ -216,7 +216,15 @@ br_status array_rewriter::mk_select_core(unsigned num_args, expr * const * args, quantifier* q = to_quantifier(args[0]); SASSERT(q->get_num_decls() == num_args - 1); var_subst subst(m()); - result = subst(q->get_expr(), num_args - 1, args + 1); + expr_ref_vector _args(m()); + var_shifter sh(m()); + for (unsigned i = 1; i < num_args; ++i) { + sh(args[i], num_args-1, result); + _args.push_back(result); + } + result = subst(q->get_expr(), _args.size(), _args.c_ptr()); + inv_var_shifter invsh(m()); + invsh(result, _args.size(), result); return BR_REWRITE_FULL; }