1 files changed, 2 insertions, 14 deletions
diff --git a/src/smt/expand_definitions.h b/src/smt/expand_definitions.h
index d6fe8ba0d..d4e591c31 100644
--- a/src/smt/expand_definitions.h
+++ b/src/smt/expand_definitions.h
@@ -27,13 +27,8 @@ namespace cvc5 {
 
 class Env;
 class ProofNodeManager;
-class SmtEngine;
 class TConvProofGenerator;
 
-namespace preprocessing {
-class AssertionPipeline;
-}
-
 namespace smt {
 
 struct SmtEngineStatistics;
@@ -47,21 +42,17 @@ struct SmtEngineStatistics;
 class ExpandDefs
 {
  public:
-  ExpandDefs(SmtEngine& smt, Env& env, SmtEngineStatistics& stats);
+  ExpandDefs(Env& env, SmtEngineStatistics& stats);
   ~ExpandDefs();
   /**
    * Expand definitions in term n. Return the expanded form of n.
    *
    * @param n The node to expand
    * @param cache Cache of previous results
-   * @param expandOnly if true, then the expandDefinitions function of
-   * TheoryEngine is not called on subterms of n.
    * @return The expanded term.
    */
   Node expandDefinitions(
-      TNode n,
-      std::unordered_map<Node, Node, NodeHashFunction>& cache,
-      bool expandOnly = false);
+      TNode n, std::unordered_map<Node, Node, NodeHashFunction>& cache);
 
   /**
    * Set proof node manager, which signals this class to enable proofs using the
@@ -77,10 +68,7 @@ class ExpandDefs
   theory::TrustNode expandDefinitions(
       TNode n,
       std::unordered_map<Node, Node, NodeHashFunction>& cache,
-      bool expandOnly,
       TConvProofGenerator* tpg);
-  /** Reference to the SMT engine */
-  SmtEngine& d_smt;
   /** Reference to the environment. */
   Env& d_env;
   /** Reference to the SMT stats */