return;
}
+ // Assertions are NOT guaranteed to be rewritten by this point
+
dumpAssertions("pre-definition-expansion", d_assertionsToPreprocess);
{
Chat() << "expanding definitions..." << endl;
}
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
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) {