From 5ab69fcdf91fb3034bf9e25f515b551124d4e747 Mon Sep 17 00:00:00 2001 From: Tim King Date: Sat, 10 Nov 2012 20:27:00 +0000 Subject: [PATCH] Removing rewriter call in SmtEngine::addFormula(). --- src/smt/smt_engine.cpp | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index e308db269..ee0d9debc 100644 --- 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) { -- 2.30.2