From fa10e510bba1647a00807a04cb7bdff73acf0dea Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Tue, 3 Apr 2018 11:53:29 -0500
Subject: [PATCH] fix(datatype): only use pointer equality for enode_tbl

---
 src/smt/smt_enode.h       | 7 -------
 src/smt/theory_datatype.h | 2 +-
 2 files changed, 1 insertion(+), 8 deletions(-)

diff --git a/src/smt/smt_enode.h b/src/smt/smt_enode.h
index ba13a31bb..df6309424 100644
--- a/src/smt/smt_enode.h
+++ b/src/smt/smt_enode.h
@@ -171,9 +171,6 @@ namespace smt {
             m_interpreted = true;
         }
 
-        inline bool equal(const enode & other) const {
-            return m_owner == other.m_owner;
-        }
 
         void del_eh(ast_manager & m, bool update_children_parent = true);
         
@@ -426,9 +423,5 @@ namespace smt {
 
 };
 
-inline bool operator==(const smt::enode & e1, const smt::enode & e2) {
-    return e1.equal(e2);
-}
-
 #endif /* SMT_ENODE_H_ */
 
diff --git a/src/smt/theory_datatype.h b/src/smt/theory_datatype.h
index fe8396fc5..4dc99f774 100644
--- a/src/smt/theory_datatype.h
+++ b/src/smt/theory_datatype.h
@@ -73,7 +73,7 @@ namespace smt {
         void sign_recognizer_conflict(enode * c, enode * r);
 
         typedef enum { ENTER, EXIT } stack_op;
-        typedef map<enode*, enode*, obj_ptr_hash<enode>, deref_eq<enode> > parent_tbl;
+        typedef map<enode*, enode*, obj_ptr_hash<enode>, ptr_eq<enode> > parent_tbl;
         typedef std::pair<stack_op, enode*> stack_entry;
 
         ptr_vector<enode>     m_to_unmark;