consistency in how the Dump output stream is used

diff --git a/src/main/driver_portfolio.cpp b/src/main/driver_portfolio.cpp
index 7b0c70a8a1f3deccaafb4e347d7ee548396367b0..d17d00c5d3454fb1010a327a42e0f31d145a6c9b 100644 (file)
--- a/src/main/driver_portfolio.cpp
+++ b/src/main/driver_portfolio.cpp
@@ -275,6 +275,7 @@ int runCvc4(int argc, char *argv[], Options& options) {
     Chat.setStream(CVC4::null_os);
     Message.setStream(CVC4::null_os);
     Warning.setStream(CVC4::null_os);
+    Dump.setStream(CVC4::null_os);
   } else {
     if(options.verbosity < 2) {
       Chat.setStream(CVC4::null_os);
@@ -294,6 +295,9 @@ int runCvc4(int argc, char *argv[], Options& options) {
     Chat.getStream() << Expr::setlanguage(language);
     Message.getStream() << Expr::setlanguage(language);
     Warning.getStream() << Expr::setlanguage(language);
+    Dump.getStream() << Expr::setlanguage(options.outputLanguage)
+                     << Expr::setdepth(-1)
+                     << Expr::printtypes(false);
   }
 
   vector<Options> threadOptions;

diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index 74feebd03804f9400bc6b35d0e87509d93c7312d..f2557a30303070f1c1450594dfe55c684b0648eb 100644 (file)
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -63,18 +63,16 @@ TseitinCnfStream::TseitinCnfStream(SatSolverInterface* satSolver, Registrar* reg
 void CnfStream::assertClause(TNode node, SatClause& c) {
   Debug("cnf") << "Inserting into stream " << c << endl;
   if(Dump.isOn("clauses")) {
-    if(Message.isOn()) {
-      if(c.size() == 1) {
-        Message() << AssertCommand(BoolExpr(getNode(c[0]).toExpr())) << endl;
-      } else {
-        Assert(c.size() > 1);
-        NodeBuilder<> b(kind::OR);
-        for(int i = 0; i < c.size(); ++i) {
-          b << getNode(c[i]);
-        }
-        Node n = b;
-        Message() << AssertCommand(BoolExpr(n.toExpr())) << endl;
+    if(c.size() == 1) {
+      Dump("clauses") << AssertCommand(BoolExpr(getNode(c[0]).toExpr())) << endl;
+    } else {
+      Assert(c.size() > 1);
+      NodeBuilder<> b(kind::OR);
+      for(int i = 0; i < c.size(); ++i) {
+        b << getNode(c[i]);
       }
+      Node n = b;
+      Dump("clauses") << AssertCommand(BoolExpr(n.toExpr())) << endl;
     }
   }
   d_satSolver->addClause(c, d_removable);