5 files changed, 17 insertions, 8 deletions
diff --git a/src/theory/quantifiers/quantifiers_preprocess.cpp b/src/theory/quantifiers/quantifiers_preprocess.cpp
index aa9674bda..321ad1717 100644
--- a/src/theory/quantifiers/quantifiers_preprocess.cpp
+++ b/src/theory/quantifiers/quantifiers_preprocess.cpp
@@ -77,7 +77,7 @@ Node QuantifiersPreprocess::computePrenexAgg(
     std::unordered_set<Node> argsSet;
     std::unordered_set<Node> nargsSet;
     Node q;
-    QuantifiersRewriter qrew(options());
+    QuantifiersRewriter qrew(d_env.getRewriter(), options());
     Node nn = qrew.computePrenex(q, n, argsSet, nargsSet, true, true);
     Assert(n != nn || argsSet.empty());
     Assert(n != nn || nargsSet.empty());
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 10c0a315b..a66a2021d 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -90,7 +90,10 @@ std::ostream& operator<<(std::ostream& out, RewriteStep s)
   return out;
 }
 
-QuantifiersRewriter::QuantifiersRewriter(const Options& opts) : d_opts(opts) {}
+QuantifiersRewriter::QuantifiersRewriter(Rewriter* r, const Options& opts)
+    : d_rewriter(r), d_opts(opts)
+{
+}
 
 bool QuantifiersRewriter::isLiteral( Node n ){
   switch( n.getKind() ){
@@ -550,7 +553,8 @@ Node QuantifiersRewriter::computeProcessTerms2(
   return ret;
 }
 
-Node QuantifiersRewriter::computeExtendedRewrite(Node q, const QAttributes& qa)
+Node QuantifiersRewriter::computeExtendedRewrite(TNode q,
+                                                 const QAttributes& qa) const
 {
   // do not apply to recursive functions
   if (qa.isFunDef())
@@ -559,7 +563,7 @@ Node QuantifiersRewriter::computeExtendedRewrite(Node q, const QAttributes& qa)
   }
   Node body = q[1];
   // apply extended rewriter
-  Node bodyr = Rewriter::callExtendedRewrite(body);
+  Node bodyr = d_rewriter->extendedRewrite(body);
   if (body != bodyr)
   {
     std::vector<Node> children;
diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h
index 8b3cbb522..d1e02b75d 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.h
+++ b/src/theory/quantifiers/quantifiers_rewriter.h
@@ -26,6 +26,9 @@ namespace cvc5 {
 class Options;
 
 namespace theory {
+
+class Rewriter;
+
 namespace quantifiers {
 
 struct QAttributes;
@@ -63,7 +66,7 @@ std::ostream& operator<<(std::ostream& out, RewriteStep s);
 class QuantifiersRewriter : public TheoryRewriter
 {
  public:
-  QuantifiersRewriter(const Options& opts);
+  QuantifiersRewriter(Rewriter* r, const Options& opts);
   /** Pre-rewrite n */
   RewriteResponse preRewrite(TNode in) override;
   /** Post-rewrite n */
@@ -295,7 +298,7 @@ class QuantifiersRewriter : public TheoryRewriter
    * This returns the result of applying the extended rewriter on the body
    * of quantified formula q with attributes qa.
    */
-  static Node computeExtendedRewrite(Node q, const QAttributes& qa);
+  Node computeExtendedRewrite(TNode q, const QAttributes& qa) const;
   //------------------------------------- end extended rewrite
   /**
    * Return true if we should do operation computeOption on quantified formula
@@ -308,6 +311,8 @@ class QuantifiersRewriter : public TheoryRewriter
   Node computeOperation(Node q,
                         RewriteStep computeOption,
                         QAttributes& qa) const;
+  /** Pointer to rewriter, used for computeExtendedRewrite above */
+  Rewriter* d_rewriter;
   /** Reference to the options */
   const Options& d_opts;
 }; /* class QuantifiersRewriter */
diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
index bcd6ea561..10e70d76a 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
@@ -508,7 +508,7 @@ bool CegSingleInv::solveTrivial(Node q)
 
     std::vector<Node> varsTmp;
     std::vector<Node> subsTmp;
-    QuantifiersRewriter qrew(options());
+    QuantifiersRewriter qrew(d_env.getRewriter(), options());
     qrew.getVarElim(body, args, varsTmp, subsTmp);
     // if we eliminated a variable, update body and reprocess
     if (!varsTmp.empty())
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index 03e647947..d726d6db9 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -34,7 +34,7 @@ TheoryQuantifiers::TheoryQuantifiers(Env& env,
                                      OutputChannel& out,
                                      Valuation valuation)
     : Theory(THEORY_QUANTIFIERS, env, out, valuation),
-      d_rewriter(env.getOptions()),
+      d_rewriter(env.getRewriter(), options()),
       d_qstate(env, valuation, logicInfo()),
       d_qreg(env),
       d_treg(env, d_qstate, d_qreg),