merge from symmetry branch

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]);