1 files changed, 5 insertions, 1 deletions
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index ff1c9245a..bc54a09e7 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -26,6 +26,7 @@
 #include "context/cdlist.h"
 #include "context/context.h"
 #include "theory/bv/bv_subtheory.h"
+#include "theory/bv/theory_bv_rewriter.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/theory.h"
 #include "util/hash.h"
@@ -72,7 +73,7 @@ public:
 
   ~TheoryBV();
 
-  std::unique_ptr<TheoryRewriter> mkTheoryRewriter() override;
+  TheoryRewriter* getTheoryRewriter() override { return &d_rewriter; }
 
   void setMasterEqualityEngine(eq::EqualityEngine* eq) override;
 
@@ -259,6 +260,9 @@ public:
 
   void checkForLemma(TNode node);
 
+  /** The theory rewriter for this theory. */
+  TheoryBVRewriter d_rewriter;
+
   friend class LazyBitblaster;
   friend class TLazyBitblaster;
   friend class EagerBitblaster;