2 files changed, 8 insertions, 0 deletions
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 8986e6894..2c748f188 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -19,6 +19,7 @@
 
 #include "options/smt_options.h"
 #include "smt/smt_statistics_registry.h"
+#include "theory/arith/arith_rewriter.h"
 #include "theory/arith/infer_bounds.h"
 #include "theory/arith/theory_arith_private.h"
 #include "theory/ext_theory.h"
@@ -53,6 +54,11 @@ TheoryArith::~TheoryArith(){
   delete d_internal;
 }
 
+std::unique_ptr<TheoryRewriter> TheoryArith::mkTheoryRewriter()
+{
+  return std::unique_ptr<TheoryRewriter>(new ArithRewriter());
+}
+
 void TheoryArith::preRegisterTerm(TNode n){
   d_internal->preRegisterTerm(n);
 }
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index b39ab961f..92892d2ae 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -51,6 +51,8 @@ public:
               Valuation valuation, const LogicInfo& logicInfo);
   virtual ~TheoryArith();
 
+  std::unique_ptr<TheoryRewriter> mkTheoryRewriter() override;
+
   /**
    * Does non-context dependent setup for a node connected to a theory.
    */