From 1d12a9c86de07feafe1261fa52b8248fe1d494ef Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Fri, 6 Oct 2017 18:19:37 +0100 Subject: [PATCH] dom_simplifier: fix dominator computation --- src/tactic/core/dom_simplify_tactic.cpp | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/src/tactic/core/dom_simplify_tactic.cpp b/src/tactic/core/dom_simplify_tactic.cpp index 99f83799b..16d8500a4 100644 --- a/src/tactic/core/dom_simplify_tactic.cpp +++ b/src/tactic/core/dom_simplify_tactic.cpp @@ -95,17 +95,17 @@ bool expr_dominators::compute_dominators() { for (unsigned i = 0; i + 1 < m_post2expr.size(); ++i) { expr * child = m_post2expr[i]; ptr_vector const& p = m_parents[child]; - SASSERT(!p.empty()); expr * new_idom = 0, *idom2 = 0; - for (unsigned j = 0; j < p.size(); ++j) { - if (!new_idom) { - m_doms.find(p[j], new_idom); - } - else if (m_doms.find(p[j], idom2)) { - new_idom = intersect(new_idom, idom2); + for (auto& pred : p) { + if (m_doms.contains(pred)) { + new_idom = !new_idom ? pred : intersect(new_idom, pred); } } - if (new_idom && (!m_doms.find(child, idom2) || idom2 != new_idom)) { + if (!new_idom) { + m_doms.insert(child, p[0]); + change = true; + } + else if (!m_doms.find(child, idom2) || idom2 != new_idom) { m_doms.insert(child, new_idom); change = true; }