consistency in how the Dump output stream is used

1 files changed, 9 insertions, 11 deletions

diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index 74feebd03..f2557a303 100644
--- 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);