diff --git a/src/ast/simplifiers/elim_unconstrained.cpp b/src/ast/simplifiers/elim_unconstrained.cpp index a6acd7260..b3f833a78 100644 --- a/src/ast/simplifiers/elim_unconstrained.cpp +++ b/src/ast/simplifiers/elim_unconstrained.cpp @@ -199,6 +199,8 @@ void elim_unconstrained::freeze(expr* t) { return; if (m_nodes.size() <= t->get_id()) return; + if (m_nodes.size() <= root(t)) + return; node& n = get_node(t); if (!n.m_term) return;