mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-12 06:00:53 +00:00
Code Activity

build

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-06-17 11:26:12 -07:00
parent 93a4939d49
commit 2138ef2ad0
1 changed files with 5 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/ast/rewriter/var_subst.cpp
View file

@ -44,8 +44,11 @@ expr_ref var_subst::operator()(expr * n, unsigned num_args, expr * const * args)
} }
if (has_quantifiers(n)) { if (has_quantifiers(n)) {
expr_safe_replace rep(m); expr_safe_replace rep(m);
for (unsigned k = 0; k < num_args; ++k) for (unsigned k = 0; k < num_args; ++k) {
rep.insert(m.mk_var(m_std_order ? num_args - k - 1 : k, args[k]->get_sort()), args[k]); expr* arg = args[k];
if (arg)
rep.insert(m.mk_var(m_std_order ? num_args - k - 1 : k, arg->get_sort()), arg);
}
rep(n, result); rep(n, result);
return result; return result;
} }