2 files changed, 1 insertions, 10 deletions
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 212a99a8e..03746c9b2 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -91,15 +91,11 @@ PropEngine::~PropEngine() {
   delete d_satSolver;
 }
 
-void PropEngine::processAssertionsStart() {
-  d_theoryEngine->preprocessStart();
-}
-
 void PropEngine::assertFormula(TNode node) {
   Assert(!d_inCheckSat, "Sat solver in solve()!");
   Debug("prop") << "assertFormula(" << node << ")" << endl;
   // Assert as non-removable
-  d_cnfStream->convertAndAssert(d_theoryEngine->preprocess(node), false, false);
+  d_cnfStream->convertAndAssert(node, false, false);
 }
 
 void PropEngine::assertLemma(TNode node, bool negated, bool removable) {
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index 3d114db3a..9e49cf3f1 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -174,11 +174,6 @@ public:
   void shutdown() { }
 
   /**
-   * Signal that a new round of assertions is ready so we can notify the theory engine
-   */
-  void processAssertionsStart();
-
-  /**
    * Converts the given formula to CNF and assert the CNF to the SAT solver.
    * The formula is asserted permanently for the current context.
    * @param node the formula to assert