1 files changed, 7 insertions, 40 deletions

diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp
index 3712d1914..504814e07 100644
--- a/src/smt/process_assertions.cpp
+++ b/src/smt/process_assertions.cpp
@@ -32,7 +32,6 @@
 #include "smt/dump.h"
 #include "smt/smt_engine.h"
 #include "theory/logic_info.h"
-#include "theory/quantifiers/fun_def_process.h"
 #include "theory/theory_engine.h"
 
 using namespace CVC4::preprocessing;
@@ -54,18 +53,13 @@ class ScopeCounter
 };
 
 ProcessAssertions::ProcessAssertions(SmtEngine& smt, ResourceManager& rm)
-    : d_smt(smt),
-      d_resourceManager(rm),
-      d_preprocessingPassContext(nullptr),
-      d_fmfRecFunctionsDefined(nullptr)
+    : d_smt(smt), d_resourceManager(rm), d_preprocessingPassContext(nullptr)
 {
   d_true = NodeManager::currentNM()->mkConst(true);
-  d_fmfRecFunctionsDefined = new (true) NodeList(d_smt.getUserContext());
 }
 
 ProcessAssertions::~ProcessAssertions()
 {
-  d_fmfRecFunctionsDefined->deleteSelf();
 }
 
 void ProcessAssertions::finishInit(PreprocessingPassContext* pc)
@@ -140,7 +134,11 @@ bool ProcessAssertions::apply(Assertions& as)
     unordered_map<Node, Node, NodeHashFunction> cache;
     for (size_t i = 0, nasserts = assertions.size(); i < nasserts; ++i)
     {
-      assertions.replace(i, expandDefinitions(assertions[i], cache));
+      Node expd = expandDefinitions(assertions[i], cache);
+      if (expd != assertions[i])
+      {
+        assertions.replace(i, expd);
+      }
     }
   }
   Trace("smt-proc")
@@ -247,38 +245,7 @@ bool ProcessAssertions::apply(Assertions& as)
     // to FMF
     if (options::fmfFunWellDefined())
     {
-      quantifiers::FunDefFmf fdf;
-      Assert(d_fmfRecFunctionsDefined != NULL);
-      // must carry over current definitions (in case of incremental)
-      for (context::CDList<Node>::const_iterator fit =
-               d_fmfRecFunctionsDefined->begin();
-           fit != d_fmfRecFunctionsDefined->end();
-           ++fit)
-      {
-        Node f = (*fit);
-        Assert(d_fmfRecFunctionsAbs.find(f) != d_fmfRecFunctionsAbs.end());
-        TypeNode ft = d_fmfRecFunctionsAbs[f];
-        fdf.d_sorts[f] = ft;
-        std::map<Node, std::vector<Node>>::iterator fcit =
-            d_fmfRecFunctionsConcrete.find(f);
-        Assert(fcit != d_fmfRecFunctionsConcrete.end());
-        for (const Node& fcc : fcit->second)
-        {
-          fdf.d_input_arg_inj[f].push_back(fcc);
-        }
-      }
-      fdf.simplify(assertions.ref());
-      // must store new definitions (in case of incremental)
-      for (const Node& f : fdf.d_funcs)
-      {
-        d_fmfRecFunctionsAbs[f] = fdf.d_sorts[f];
-        d_fmfRecFunctionsConcrete[f].clear();
-        for (const Node& fcc : fdf.d_input_arg_inj[f])
-        {
-          d_fmfRecFunctionsConcrete[f].push_back(fcc);
-        }
-        d_fmfRecFunctionsDefined->push_back(f);
-      }
+      d_passes["fun-def-fmf"]->apply(&assertions);
     }
   }