diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp
index b528bad82dd..5a08edfe6e0 100644
--- a/src/ast/datatype_decl_plugin.cpp
+++ b/src/ast/datatype_decl_plugin.cpp
@@ -706,18 +706,20 @@ namespace datatype {
        \brief Return true if the inductive datatype is recursive.
     */
     bool util::is_recursive_core(sort* s) const {
-        obj_map<sort, status> already_found;
+        map<symbol, status, symbol_hash_proc, symbol_eq_proc> already_found;
         ptr_vector<sort> todo, subsorts;
         sort* s0 = s;
         todo.push_back(s);
         status st;
+        std::cout << "is recursive " << mk_pp(s, m) << "\n";
         while (!todo.empty()) {
             s = todo.back();
-            if (already_found.find(s, st) && st == BLACK) {
+            std::cout << "is recursive - todo " << mk_pp(s, m) << "\n";
+            if (already_found.find(datatype_name(s), st) && st == BLACK) {
                 todo.pop_back();
                 continue;
             }
-            already_found.insert(s, GRAY);
+            already_found.insert(datatype_name(s), GRAY);
             def const& d = get_def(s);
             bool can_process       = true;
             for (constructor const* c : d) {
@@ -728,9 +730,9 @@ namespace datatype {
                     get_subsorts(d, subsorts);
                     for (sort * s2 : subsorts) {
                         if (is_datatype(s2)) {
-                            if (already_found.find(s2, st)) {
+                            if (already_found.find(datatype_name(s2), st)) {
                                 // type is recursive
-                                if (st == GRAY && s0 == s2) 
+                                if (st == GRAY && datatype_name(s0) == datatype_name(s2)) 
                                     return true;
                             }
                             else {
@@ -742,7 +744,7 @@ namespace datatype {
                 }
             }
             if (can_process) {
-                already_found.insert(s, BLACK);
+                already_found.insert(datatype_name(s), BLACK);
                 todo.pop_back();
             }
         }
diff --git a/src/ast/datatype_decl_plugin.h b/src/ast/datatype_decl_plugin.h
index 68e7e3c9abe..d4d38a7570e 100644
--- a/src/ast/datatype_decl_plugin.h
+++ b/src/ast/datatype_decl_plugin.h
@@ -323,6 +323,7 @@ namespace datatype {
         bool is_covariant(ast_mark& mark, ptr_vector<sort>& subsorts, sort* s) const;
         def& get_def(symbol const& s) { return plugin().get_def(s); }        
         void get_subsorts(sort* s, ptr_vector<sort>& sorts) const;        
+        symbol datatype_name(sort* s) const { return s->get_parameter(0).get_symbol(); }
 
     public:
         util(ast_manager & m);