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

renamed variable to avoid clashes

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-05-24 14:37:43 +01:00
parent 9717161bb8
commit c4610e0423
1 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/muz/transforms/dl_mk_quantifier_abstraction.cpp
View file

@ -97,7 +97,7 @@ namespace datalog {
TRACE("dl", tout << mk_pp(body, m) << "\n";);
// 2. replace bound variables by constants.
expr_ref_vector consts(m), bound(m), free(m);
expr_ref_vector consts(m), bound(m), _free(m);
svector<symbol> names;
ptr_vector<sort> bound_sorts;
for (unsigned i = 0; i < sorts.size(); ++i) {
@ -110,7 +110,7 @@ namespace datalog {
bound_sorts.push_back(s);
}
else {
free.push_back(consts.back());
_free.push_back(consts.back());
}
}
rep(body);
@ -123,8 +123,8 @@ namespace datalog {
TRACE("dl", tout << mk_pp(body, m) << "\n";);
// 4. replace remaining constants by variables.
for (unsigned i = 0; i < free.size(); ++i) {
rep.insert(free[i].get(), m.mk_var(i, m.get_sort(free[i].get())));
for (unsigned i = 0; i < _free.size(); ++i) {
rep.insert(_free[i].get(), m.mk_var(i, m.get_sort(_free[i].get())));
}
rep(body);
g->set_else(body);