mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-07 19:51:22 +00:00
Code Activity

dom_simplify_tactic: micro opt

Browse source
This commit is contained in:
Nuno Lopes 2017-10-05 08:53:12 +01:00
parent f1eb53761a
commit 110d558ee4
1 changed files with 2 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/tactic/core/dom_simplify_tactic.cpp
View file

@ -225,9 +225,8 @@ expr_ref dom_simplify_tactic::simplify(expr * e0) {
} }
else { else {
expr_dominators::tree_t const& t = m_dominators.get_tree(); expr_dominators::tree_t const& t = m_dominators.get_tree();
if (t.contains(e)) { if (auto children = t.find_core(e)) {
ptr_vector<expr> const& children = t[e]; for (expr * child : children->get_data().m_value) {
for (expr * child : children) {
simplify(child); simplify(child);
} }
} }