From af5d989d6c53193b5af5896eadf0f07800ffe37f Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 2 Dec 2013 21:51:20 -0800
Subject: [PATCH] change verbosity level

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/opt/core_maxsat.cpp | 4 ++--
 src/opt/fu_malik.cpp    | 8 ++++----
 src/opt/maxsmt.cpp      | 1 -
 src/smt/theory_pb.cpp   | 6 +-----
 4 files changed, 7 insertions(+), 12 deletions(-)

diff --git a/src/opt/core_maxsat.cpp b/src/opt/core_maxsat.cpp
index b6da58aa0..11756c617 100644
--- a/src/opt/core_maxsat.cpp
+++ b/src/opt/core_maxsat.cpp
@@ -65,7 +65,7 @@ namespace opt {
                       for (unsigned i = 0; i < ans.size(); ++i) {
                           tout << mk_pp(ans[i].get(), m) << "\n";
                       });
-                IF_VERBOSE(0, verbose_stream() << "(maxsat.core sat with lower bound: " << ans.size() << "\n";);
+                IF_VERBOSE(1, verbose_stream() << "(maxsat.core sat with lower bound: " << ans.size() << "\n";);
                 if (ans.size() > m_answer.size()) {
                     m_answer.reset();
                     m_answer.append(ans);
@@ -92,7 +92,7 @@ namespace opt {
                     core_vars.insert(get_not(core[i]));
                     block_vars.remove(core[i]);
                 }
-                IF_VERBOSE(0, verbose_stream() << "(maxsat.core unsat (core size = " << core.size() << ")\n";);
+                IF_VERBOSE(1, verbose_stream() << "(maxsat.core unsat (core size = " << core.size() << ")\n";);
                 if (core.empty()) {
                     m_upper = m_answer.size();
                     return l_true;
diff --git a/src/opt/fu_malik.cpp b/src/opt/fu_malik.cpp
index 90420ad72..99ecdf2a5 100644
--- a/src/opt/fu_malik.cpp
+++ b/src/opt/fu_malik.cpp
@@ -149,7 +149,7 @@ namespace opt {
         }
 
         lbool step() {
-            IF_VERBOSE(0, verbose_stream() << "(opt.max_sat step " << m_soft.size() + 2 - m_upper_size << ")\n";);
+            IF_VERBOSE(1, verbose_stream() << "(opt.max_sat step " << m_soft.size() + 2 - m_upper_size << ")\n";);
             expr_ref_vector assumptions(m), block_vars(m);
             for (unsigned i = 0; i < m_soft.size(); ++i) {
                 assumptions.push_back(m.mk_not(m_aux[i].get()));
@@ -187,7 +187,7 @@ namespace opt {
                 //    ++i;
                 //}
 
-                IF_VERBOSE(0, verbose_stream() << "(opt.max_sat unsat-core of size " << core.size() << ")\n";);
+                IF_VERBOSE(1, verbose_stream() << "(opt.max_sat unsat-core of size " << core.size() << ")\n";);
             }
             else {
                 s().get_unsat_core(core);
@@ -214,7 +214,7 @@ namespace opt {
             }
             SASSERT (!block_vars.empty());
             assert_at_most_one(block_vars);
-            IF_VERBOSE(0, verbose_stream() << "(opt.max_sat # of non-blocked soft constraints: " << m_soft.size() - block_vars.size() << ")\n";);
+            IF_VERBOSE(1, verbose_stream() << "(opt.max_sat # of non-blocked soft constraints: " << m_soft.size() - block_vars.size() << ")\n";);
             return l_false;
         }
 
@@ -264,7 +264,7 @@ namespace opt {
                     m_s->assert_expr(current_solver.get_assertion(i));
                 }
                 m_use_new_bv_solver = true;
-                IF_VERBOSE(0, verbose_stream() << "Force to use the new BV solver." << std::endl;);
+                IF_VERBOSE(1, verbose_stream() << "Force to use the new BV solver." << std::endl;);
             }
         }
 
diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp
index 14233300a..c6298f2e8 100644
--- a/src/opt/maxsmt.cpp
+++ b/src/opt/maxsmt.cpp
@@ -61,7 +61,6 @@ namespace opt {
                    });
 
         DEBUG_CODE(if (is_sat == l_true) {
-                IF_VERBOSE(0, verbose_stream() << "validating assignment\n";);
                 m_s->push();
                 commit_assignment();
                 VERIFY(l_true == m_s->check_sat(0,0));
diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp
index 79db388f4..2ef202f76 100644
--- a/src/smt/theory_pb.cpp
+++ b/src/smt/theory_pb.cpp
@@ -1046,14 +1046,10 @@ namespace smt {
 
         resolve_conflict(c);
 
-#if 1
         justification* js = 0;
         ctx.mk_clause(lits.size(), lits.c_ptr(), js, CLS_AUX_LEMMA, 0);
-        IF_VERBOSE(2, ctx.display_literals_verbose(verbose_stream(), 
-                                                   lits.size(), lits.c_ptr());
+        IF_VERBOSE(2, ctx.display_literals_verbose(verbose_stream(), lits.size(), lits.c_ptr());
                    verbose_stream() << "\n";);
-        // ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
-#endif
     }
 
     void theory_pb::set_mark(bool_var v, unsigned idx) {