1 files changed, 3 insertions, 25 deletions
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 53f128286..d951f94a7 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -1852,38 +1852,16 @@ void TheoryDatatypes::computeRelevantTerms(std::set<Node>& termSet)
   Trace("dt-cmi") << "Have " << termSet.size() << " relevant terms..."
                   << std::endl;
 
-  //also include non-singleton equivalence classes  TODO : revisit this
+  //also include non-singleton dt equivalence classes  TODO : revisit this
   eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(d_equalityEngine);
   while( !eqcs_i.isFinished() ){
     TNode r = (*eqcs_i);
-    bool addedFirst = false;
-    Node first;
-    TypeNode rtn = r.getType();
-    if (!rtn.isBoolean())
+    if (r.getType().isDatatype())
     {
       eq::EqClassIterator eqc_i = eq::EqClassIterator(r, d_equalityEngine);
       while (!eqc_i.isFinished())
       {
-        TNode n = (*eqc_i);
-        if (first.isNull())
-        {
-          first = n;
-          // always include all datatypes
-          if (rtn.isDatatype())
-          {
-            addedFirst = true;
-            termSet.insert(n);
-          }
-        }
-        else
-        {
-          if (!addedFirst)
-          {
-            addedFirst = true;
-            termSet.insert(first);
-          }
-          termSet.insert(n);
-        }
+        termSet.insert(*eqc_i);
         ++eqc_i;
       }
     }