diff --git a/src/ast/simplifiers/euf_completion.cpp b/src/ast/simplifiers/euf_completion.cpp
index 3ede7024e..280b5e6bf 100644
--- a/src/ast/simplifiers/euf_completion.cpp
+++ b/src/ast/simplifiers/euf_completion.cpp
@@ -307,7 +307,7 @@ namespace euf {
             }
         };
         SASSERT(e);
-        if (num_scopes() > 0)
+        if (num_scopes() > 0 && m_canonical.size() > n->get_id())
             m_trail.push(vtrail(m_canonical, n->get_id()));
         m_canonical.setx(n->get_id(), e);
         m_epochs.setx(n->get_id(), m_epoch, 0);