1 files changed, 19 insertions, 12 deletions
diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp
index bff5e36cd..04c39c897 100644
--- a/src/theory/rep_set.cpp
+++ b/src/theory/rep_set.cpp
@@ -43,12 +43,8 @@ bool RepSet::hasRep(TypeNode tn, Node n) const
 
 unsigned RepSet::getNumRepresentatives(TypeNode tn) const
 {
-  std::map< TypeNode, std::vector< Node > >::const_iterator it = d_type_reps.find( tn );
-  if( it!=d_type_reps.end() ){
-    return it->second.size();
-  }else{
-    return 0;
-  }
+  const std::vector<Node>* reps = getTypeRepsOrNull(tn);
+  return (reps != nullptr) ? reps->size() : 0;
 }
 
 Node RepSet::getRepresentative(TypeNode tn, unsigned i) const
@@ -60,14 +56,18 @@ Node RepSet::getRepresentative(TypeNode tn, unsigned i) const
   return it->second[i];
 }
 
-void RepSet::getRepresentatives(TypeNode tn, std::vector<Node>& reps) const
+const std::vector<Node>* RepSet::getTypeRepsOrNull(TypeNode tn) const
 {
-  std::map<TypeNode, std::vector<Node> >::const_iterator it =
-      d_type_reps.find(tn);
-  Assert(it != d_type_reps.end());
-  reps.insert(reps.end(), it->second.begin(), it->second.end());
+  auto it = d_type_reps.find(tn);
+  if (it == d_type_reps.end())
+  {
+    return nullptr;
+  }
+  return &(it->second);
 }
 
+namespace {
+
 bool containsStoreAll(Node n, std::unordered_set<Node, NodeHashFunction>& cache)
 {
   if( std::find( cache.begin(), cache.end(), n )==cache.end() ){
@@ -85,6 +85,8 @@ bool containsStoreAll(Node n, std::unordered_set<Node, NodeHashFunction>& cache)
   return false;
 }
 
+}  // namespace
+
 void RepSet::add( TypeNode tn, Node n ){
   //for now, do not add array constants FIXME
   if( tn.isArray() ){
@@ -264,7 +266,12 @@ bool RepSetIterator::initialize()
       if (d_rs->hasType(tn))
       {
         d_enum_type.push_back( ENUM_DEFAULT );
-        d_rs->getRepresentatives(tn, d_domain_elements[v]);
+        if (const auto* type_reps = d_rs->getTypeRepsOrNull(tn))
+        {
+          std::vector<Node>& v_domain_elements = d_domain_elements[v];
+          v_domain_elements.insert(v_domain_elements.end(),
+                                   type_reps->begin(), type_reps->end());
+        }
       }else{
         Assert( d_incomplete );
         return false;