diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp
index b3c6ffadf..fb817502b 100644
--- a/src/smt/theory_datatype.cpp
+++ b/src/smt/theory_datatype.cpp
@@ -393,7 +393,7 @@ namespace smt {
         for (int v = 0; v < num_vars; v++) {
             if (v == static_cast<int>(m_find.find(v))) {
                 enode * node = get_enode(v);
-                if (occurs_check(node)) {
+                if (!oc_cycle_free(node) && occurs_check(node)) {
                     // conflict was detected... 
                     // return...
                     return FC_CONTINUE;
diff --git a/src/smt/theory_datatype.h b/src/smt/theory_datatype.h
index 4dc99f774..29799910b 100644
--- a/src/smt/theory_datatype.h
+++ b/src/smt/theory_datatype.h
@@ -104,8 +104,8 @@ namespace smt {
             theory_datatype * th;
             public:
             final_check_st(theory_datatype * th) : th(th) {
-                th->m_to_unmark2.reset();
                 th->m_to_unmark.reset();
+                th->m_to_unmark2.reset();
                 th->m_used_eqs.reset();
                 th->m_stack.reset();
                 th->m_parent.reset();
@@ -115,6 +115,7 @@ namespace smt {
                 unmark_enodes2(th->m_to_unmark2.size(), th->m_to_unmark2.c_ptr());
                 th->m_to_unmark.reset();
                 th->m_to_unmark2.reset();
+                th->m_used_eqs.reset();
                 th->m_stack.reset();
                 th->m_parent.reset();
             }