diff --git a/src/tactic/core/dom_simplify_tactic.cpp b/src/tactic/core/dom_simplify_tactic.cpp
index 60207e823..830d44c7a 100644
--- a/src/tactic/core/dom_simplify_tactic.cpp
+++ b/src/tactic/core/dom_simplify_tactic.cpp
@@ -100,33 +100,19 @@ bool expr_dominators::compute_dominators() {
         for (unsigned i = 0; i + 1 < m_post2expr.size(); ++i) {
             expr * child = m_post2expr[i];
             ptr_vector<expr> const& p = m_parents[child];
-            SASSERT(!p.empty());
-            if (p.size() == 1) {
-                if (!m_doms.contains(child)) {
-                    m_doms.insert(child, p[0]);
-                    change = true;
-                }                
+            expr * new_idom = 0, *idom2 = 0;
+            for (auto& pred : p) {
+                if (m_doms.contains(pred)) {
+                    new_idom = !new_idom ? pred : intersect(new_idom, pred);
+                }
             }
-            else {
-                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);
-                    }
-                }
-                if (!new_idom) {
-                    m_doms.insert(child, p[0]);
-                    TRACE("simplify", tout << expr_ref(child, m) << " |-> " << expr_ref(p[0], m) << "\n";);
-                    change = true;
-                } 
-                else if (!m_doms.find(child, idom2) || idom2 != new_idom) {
-                    m_doms.insert(child, new_idom);
-                    TRACE("simplify", tout << expr_ref(child, m) << " |-> " << expr_ref(new_idom, m) << "\n";);
-                    change = true;
-                }
+            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;
             }
         }
         iterations *= 2;