mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

fix #2792

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-12-09 07:50:57 +03:00
parent 99a91ee116
commit ebb7d60c75
1 changed files with 9 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/ast/rewriter/array_rewriter.cpp
View file

@ -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;
}