Removing rewriter call in SmtEngine::addFormula().

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index e308db2696f872feb404b61479afa1ca3498c01f..ee0d9debceeee9788ec3513363c92c557d6b4988 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1900,6 +1900,8 @@ void SmtEnginePrivate::processAssertions() {
     return;
   }
 
+  // Assertions are NOT guaranteed to be rewritten by this point
+
   dumpAssertions("pre-definition-expansion", d_assertionsToPreprocess);
   {
     Chat() << "expanding definitions..." << endl;
@@ -1946,6 +1948,8 @@ void SmtEnginePrivate::processAssertions() {
   }
   dumpAssertions("post-substitution", d_assertionsToPreprocess);
 
+  // Assertions ARE guaranteed to be rewritten by this point
+
   dumpAssertions("pre-skolem-quant", d_assertionsToPreprocess);
   if( options::preSkolemQuant() ){
     //apply pre-skolemization to existential quantifiers
@@ -2075,7 +2079,8 @@ void SmtEnginePrivate::addFormula(TNode n)
   Trace("smt") << "SmtEnginePrivate::addFormula(" << n << ")" << endl;
 
   // Add the normalized formula to the queue
-  d_assertionsToPreprocess.push_back(Rewriter::rewrite(n));
+  d_assertionsToPreprocess.push_back(n);
+  //d_assertionsToPreprocess.push_back(Rewriter::rewrite(n));
 
   // If the mode of processing is incremental prepreocess and assert immediately
   if (options::simplificationMode() == SIMPLIFICATION_MODE_INCREMENTAL) {