From 433f487ff2d2dcb8d4c4427169b46e8db3b34c82 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Tue, 3 Apr 2018 18:30:09 -0500
Subject: [PATCH] fix(datatype): always use root nodes for the `parent` table

---
 src/smt/theory_datatype.cpp | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp
index fb817502b..68ebb60e6 100644
--- a/src/smt/theory_datatype.cpp
+++ b/src/smt/theory_datatype.cpp
@@ -424,7 +424,7 @@ namespace smt {
             SASSERT(d->m_constructor);
             if (app != d->m_constructor)
                 m_used_eqs.push_back(enode_pair(app, d->m_constructor));
-            bool found = m_parent.find(app, app_parent);
+            bool found = m_parent.find(app->get_root(), app_parent);
             SASSERT(found);
             app = app_parent;
         }
@@ -455,7 +455,7 @@ namespace smt {
                     }
                     // explore `arg` (with parent `app`)
                     if (m_util.is_datatype(get_manager().get_sort(arg->get_owner()))) {
-                        m_parent.insert(arg, app);
+                        m_parent.insert(arg->get_root(), app);
                         oc_push_stack(arg);
                     }
                 }