1 files changed, 5 insertions, 1 deletions
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index d1f912d95..34cf6c424 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -27,6 +27,7 @@
 #include "context/cdqueue.h"
 #include "theory/arrays/array_info.h"
 #include "theory/arrays/array_proof_reconstruction.h"
+#include "theory/arrays/theory_arrays_rewriter.h"
 #include "theory/theory.h"
 #include "theory/uf/equality_engine.h"
 #include "util/statistics_registry.h"
@@ -144,7 +145,7 @@ class TheoryArrays : public Theory {
                std::string name = "");
   ~TheoryArrays();
 
-  std::unique_ptr<TheoryRewriter> mkTheoryRewriter() override;
+  TheoryRewriter* getTheoryRewriter() override { return &d_rewriter; }
 
   void setMasterEqualityEngine(eq::EqualityEngine* eq) override;
 
@@ -177,6 +178,9 @@ class TheoryArrays : public Theory {
   bool ppDisequal(TNode a, TNode b);
   Node solveWrite(TNode term, bool solve1, bool solve2, bool ppCheck);
 
+  /** The theory rewriter for this theory. */
+  TheoryArraysRewriter d_rewriter;
+
  public:
   PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override;
   Node ppRewrite(TNode atom) override;