2 files changed, 28 insertions, 17 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;
diff --git a/src/theory/rep_set.h b/src/theory/rep_set.h
index 5b75fa943..a75918b5a 100644
--- a/src/theory/rep_set.h
+++ b/src/theory/rep_set.h
@@ -57,9 +57,9 @@ class QuantifiersEngine;
  * finite types.
  */
 class RepSet {
-public:
+ public:
   RepSet(){}
-  ~RepSet(){}
+
   /** map from types to the list of representatives
    * TODO : as part of #1199, encapsulate this
    */
@@ -67,15 +67,19 @@ public:
   /** clear the set */
   void clear();
   /** does this set have representatives of type tn? */
-  bool hasType( TypeNode tn ) const { return d_type_reps.find( tn )!=d_type_reps.end(); }
+  bool hasType(TypeNode tn) const { return d_type_reps.count(tn) > 0; }
   /** does this set have representative n of type tn? */
   bool hasRep(TypeNode tn, Node n) const;
   /** get the number of representatives for type */
   unsigned getNumRepresentatives(TypeNode tn) const;
   /** get representative at index */
   Node getRepresentative(TypeNode tn, unsigned i) const;
-  /** get representatives of type tn, appends them to reps */
-  void getRepresentatives(TypeNode tn, std::vector<Node>& reps) const;
+  /**
+   * Returns the representatives of a type for a `type_node` if one exists.
+   * Otherwise, returns nullptr.
+   */
+  const std::vector<Node>* getTypeRepsOrNull(TypeNode type_node) const;
+
   /** add representative n for type tn, where n has type tn */
   void add( TypeNode tn, Node n );
   /** returns index in d_type_reps for node n */