mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 03:32:28 +00:00
Code Activity

fix semantics of get_concats_in_eqc and get_var_in_eqc

Browse source
This commit is contained in:
Murphy Berzish 2016-09-14 15:36:36 -04:00
parent 87d61d6d6e
commit 50353168ef
1 changed files with 2 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/smt/theory_str.cpp
View file

@ -8649,9 +8649,7 @@ void theory_str::get_concats_in_eqc(expr * n, std::set<expr*> & concats) {
if (is_concat(to_app(eqcNode))) {
concats.insert(eqcNode);
}
enode * e_eqc = ctx.get_enode(eqcNode);
eqcNode = e_eqc->get_next()->get_owner();
// eqcNode = Z3_theory_get_eqc_next(t, eqcNode);
eqcNode = get_eqc_next(eqcNode);
} while (eqcNode != n);
}
@ -8663,9 +8661,7 @@ void theory_str::get_var_in_eqc(expr * n, std::set<expr*> & varSet) {
if (variable_set.find(eqcNode) != variable_set.end()) {
varSet.insert(eqcNode);
}
enode * e_eqc = ctx.get_enode(eqcNode);
eqcNode = e_eqc->get_next()->get_owner();
// eqcNode = Z3_theory_get_eqc_next(t, eqcNode);
eqcNode = get_eqc_next(eqcNode);
} while (eqcNode != n);
}