3 files changed, 9 insertions, 3 deletions
diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp
index 0b9e6d934..f4b265d98 100644
--- a/src/theory/sets/theory_sets.cpp
+++ b/src/theory/sets/theory_sets.cpp
@@ -46,9 +46,9 @@ TheorySets::~TheorySets()
   // Do not move me to the header. See explanation in the constructor.
 }
 
-std::unique_ptr<TheoryRewriter> TheorySets::mkTheoryRewriter()
+TheoryRewriter* TheorySets::getTheoryRewriter()
 {
-  return std::unique_ptr<TheoryRewriter>(new TheorySetsRewriter());
+  return d_internal->getTheoryRewriter();
 }
 
 void TheorySets::finishInit()
diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h
index a55a22600..5fc1a61a3 100644
--- a/src/theory/sets/theory_sets.h
+++ b/src/theory/sets/theory_sets.h
@@ -42,7 +42,7 @@ class TheorySets : public Theory
              const LogicInfo& logicInfo);
   ~TheorySets() override;
 
-  std::unique_ptr<TheoryRewriter> mkTheoryRewriter() override;
+  TheoryRewriter* getTheoryRewriter() override;
 
   /** finish initialization */
   void finishInit() override;
diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h
index 5ef8c4825..ab9071793 100644
--- a/src/theory/sets/theory_sets_private.h
+++ b/src/theory/sets/theory_sets_private.h
@@ -26,6 +26,7 @@
 #include "theory/sets/inference_manager.h"
 #include "theory/sets/solver_state.h"
 #include "theory/sets/theory_sets_rels.h"
+#include "theory/sets/theory_sets_rewriter.h"
 #include "theory/theory.h"
 #include "theory/uf/equality_engine.h"
 
@@ -161,6 +162,8 @@ class TheorySetsPrivate {
 
   ~TheorySetsPrivate();
 
+  TheoryRewriter* getTheoryRewriter() { return &d_rewriter; }
+
   void setMasterEqualityEngine(eq::EqualityEngine* eq);
 
   void addSharedTerm(TNode);
@@ -279,6 +282,9 @@ class TheorySetsPrivate {
    * involving cardinality constraints is asserted to this theory.
    */
   bool d_card_enabled;
+
+  /** The theory rewriter for this theory. */
+  TheorySetsRewriter d_rewriter;
 };/* class TheorySetsPrivate */