2 files changed, 7 insertions, 0 deletions
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 94fc1e34c..27718b63f 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -112,6 +112,11 @@ TheoryBV::TheoryBV(context::Context* c,
 
 TheoryBV::~TheoryBV() {}
 
+std::unique_ptr<TheoryRewriter> TheoryBV::mkTheoryRewriter()
+{
+  return std::unique_ptr<TheoryRewriter>(new TheoryBVRewriter());
+}
+
 void TheoryBV::setMasterEqualityEngine(eq::EqualityEngine* eq) {
   if (options::bitblastMode() == options::BitblastMode::EAGER)
   {
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 196535a19..ff1c9245a 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -72,6 +72,8 @@ public:
 
   ~TheoryBV();
 
+  std::unique_ptr<TheoryRewriter> mkTheoryRewriter() override;
+
   void setMasterEqualityEngine(eq::EqualityEngine* eq) override;
 
   void finishInit() override;