diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp
index 81cf4c815..de86ef7e3 100644
--- a/src/smt/theory_pb.cpp
+++ b/src/smt/theory_pb.cpp
@@ -1436,7 +1436,7 @@ namespace smt {
             }
         }
 
-        std::cout << "zs: " << z << " nzs: " << nz << " lemmas: " << ctx.get_lemmas().size() << " trail: " << m_card_trail.size() << "\n";
+        //std::cout << "zs: " << z << " nzs: " << nz << " lemmas: " << ctx.get_lemmas().size() << " trail: " << m_card_trail.size() << "\n";
         return z*10 >= nz;
 
         m_occs.reset();
@@ -1739,7 +1739,7 @@ namespace smt {
         k.assert_expr(notB);
         lbool is_sat = k.check();
         validating = false;
-        std::cout << is_sat << "\n";
+        // std::cout << is_sat << "\n";
         if (is_sat == l_true) {
             std::cout << A << "\n";
             std::cout << B << "\n";
@@ -2010,7 +2010,6 @@ namespace smt {
                 m_coeffs[m_active_vars[i]] /= g;                
             }
             m_bound = (m_bound + g - 1) / g;
-            std::cout << "CUT " << g << "\n";
             TRACE("pb", display_resolved_lemma(tout << "cut\n"););
         }
     }
@@ -2032,7 +2031,7 @@ namespace smt {
         for (unsigned i = 0; i < m_antecedent_exprs.size(); ++i) {
             expr* a = m_antecedent_exprs[i].get();
             if (!ctx.b_internalized(a)) {
-                std::cout << "not internalized " << mk_pp(a, m) << "\n";
+                // std::cout << "not internalized " << mk_pp(a, m) << "\n";
                 return;
             }
             m_antecedents.push_back(~literal(ctx.get_bool_var(a), m_antecedent_signs[i]));
@@ -2040,7 +2039,7 @@ namespace smt {
         for (unsigned i = 0; i < m_cardinality_exprs.size(); ++i) {
             expr* a = m_cardinality_exprs[i].get();
             if (!ctx.b_internalized(a)) {
-                std::cout << "not internalized " << mk_pp(a, m) << "\n";
+                // std::cout << "not internalized " << mk_pp(a, m) << "\n";
                 return;
             }
             if (m_cardinality_signs[i]) {
diff --git a/src/test/heap.cpp b/src/test/heap.cpp
index 2c77b939e..6a5bc7b9f 100644
--- a/src/test/heap.cpp
+++ b/src/test/heap.cpp
@@ -88,7 +88,7 @@ static void tst2() {
     int_heap2 h(N);
     for (int i = 0; i < N * 10; i++) {
 
-        if (i % 1 == 0) std::cout << "i: " << i << std::endl;
+        // if (i % 1 == 0) std::cout << "i: " << i << std::endl;
         if (i % 1000 == 0) std::cout << "i: " << i << std::endl;
         int cmd = heap_rand() % 10;
         if (cmd <= 3) {
diff --git a/src/test/theory_pb.cpp b/src/test/theory_pb.cpp
index 7010b96d0..f0604df73 100644
--- a/src/test/theory_pb.cpp
+++ b/src/test/theory_pb.cpp
@@ -11,7 +11,7 @@ Copyright (c) 2015 Microsoft Corporation
 #include "smt/theory_pb.h"
 #include "ast/rewriter/th_rewriter.h"
 
-unsigned populate_literals(unsigned k, smt::literal_vector& lits) {
+static unsigned populate_literals(unsigned k, smt::literal_vector& lits) {
     ENSURE(k < (1u << lits.size()));
     unsigned t = 0;
     for (unsigned i = 0; i < lits.size(); ++i) {
@@ -84,6 +84,7 @@ private:
         }
         std::cout << "(assert " << fml << ")\n";
         ctx.assert_expr(fml);
+        std::cout << ";asserted\n";
     }
 
     
@@ -138,11 +139,8 @@ void tst_theory_pb() {
             unsigned k = populate_literals(i, lits);        
             std::cout << "k:" << k << " " << N << "\n";
             std::cout.flush();
-            TRACE("pb", tout << "k " << k << ": ";
-                  for (unsigned j = 0; j < lits.size(); ++j) {
-                      tout << lits[j] << " ";
-                  }
-                  tout << "\n";);
+            TRACE("pb", tout << "k " << k << ": " << lits << "\n";);
+
             {
                 smt::context ctx(m, params);
                 ctx.push();