diff options
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/smt_engine.cpp | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index d85f28b23..fe5628dd0 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -669,6 +669,18 @@ void SmtEnginePrivate::processAssertions() { // Simplify the assertions simplifyAssertions(); + if(Options::current()->preprocessOnly) { + if(Message.isOn()) { + // Push the formula to the Message() stream + for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) { + expr::ExprSetDepth::Scope sdScope(Message.getStream(), -1); + Message() << AssertCommand(BoolExpr(d_assertionsToCheck[i].toExpr())) << endl; + } + } + // We still call into SAT below so that we can output theory + // contributions that come from presolve(). + } + // Push the formula to SAT for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) { d_smt.d_propEngine->assertFormula(d_assertionsToCheck[i]); |