1 files changed, 8 insertions, 5 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 7881449dd..4f3b1b5d6 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -110,6 +110,7 @@ using namespace CVC4::smt;
 using namespace CVC4::prop;
 using namespace CVC4::context;
 using namespace CVC4::theory;
+using namespace CVC4::preproc;
 
 namespace CVC4 {
 namespace smt {
@@ -3630,6 +3631,11 @@ void SmtEnginePrivate::processAssertions() {
  }
 
   if( d_smt.d_logic.isQuantified() ){
+/*    preproc::QuantifiedPass pass(d_resourceManager, d_smt.d_theoryEngine,
+     d_smt.d_fmfRecFunctionsDefined, d_smt.d_fmfRecFunctionsAbs,
+     d_smt.d_fmfRecFunctionsConcrete);
+    pass.apply(&d_assertions);*/
+ 
     Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-quant-preprocess" << std::endl;
 
     dumpAssertions("pre-skolem-quant", d_assertions);
@@ -3655,6 +3661,7 @@ void SmtEnginePrivate::processAssertions() {
       qm.finalizeDefinitions();
     }
 
+
     //fmf-fun : assume admissible functions, applying preprocessing reduction to FMF
     if( options::fmfFunWellDefined() ){
       quantifiers::FunDefFmf fdf;
@@ -3685,11 +3692,7 @@ void SmtEnginePrivate::processAssertions() {
       }
     }
     Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-quant-preprocess" << std::endl;
-  /*  preproc::QuantifiedPass pass(d_resourceManager, d_smt.d_theoryEngine,
-     d_smt.d_fmfRecFunctionsDefined, d_smt.d_fmfRecFunctionsAbs,
-     d_smt.d_fmfRecFunctionsConcrete);
-    pass.apply(&d_assertions);*/
- }
+}
 
   if( options::sortInference() || options::ufssFairnessMonotone() ){
     //sort inference technique