diff options
Diffstat (limited to 'src/smt/smt_engine.cpp')
-rw-r--r-- | src/smt/smt_engine.cpp | 7 |
1 files changed, 6 insertions, 1 deletions
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) { |