diff --git a/src/ast/rewriter/pb2bv_rewriter.cpp b/src/ast/rewriter/pb2bv_rewriter.cpp
index 4c8f5d665..1dd4ea6fa 100644
--- a/src/ast/rewriter/pb2bv_rewriter.cpp
+++ b/src/ast/rewriter/pb2bv_rewriter.cpp
@@ -353,7 +353,6 @@ struct pb2bv_rewriter::imp {
 
         bool mk_pb(bool full, func_decl * f, unsigned sz, expr * const* args, expr_ref & result) {
             SASSERT(f->get_family_id() == pb.get_family_id());
-            std::cout << "card: " << m_enable_card << "\n";
             if (is_or(f)) {
                 if (m_enable_card) return false;
                 result = m.mk_or(sz, args);
@@ -408,7 +407,6 @@ struct pb2bv_rewriter::imp {
         }        
 
         void enable_card(bool f) {
-            std::cout << "set " << f << "\n";
             m_enable_card = f;
             m_enable_card = true;
         }
diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp
index e2b01dd59..50464b570 100644
--- a/src/opt/maxres.cpp
+++ b/src/opt/maxres.cpp
@@ -345,6 +345,9 @@ public:
         while (is_sat == l_false) {
             core.reset();
             s().get_unsat_core(core);
+            //expr_ref_vector core1(m);
+            //core1.append(core.size(), core.c_ptr());
+            //std::cout << core1 << "\n";
             // verify_core(core);
             model_ref mdl;
             get_mus_model(mdl);
@@ -368,8 +371,7 @@ public:
                 break;
             }
             remove_soft(core, asms);
-            //is_sat = check_sat_hill_climb(asms);
-            is_sat = l_true;
+            is_sat = check_sat_hill_climb(asms);
         }
         TRACE("opt", 
               tout << "num cores: " << cores.size() << "\n";
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 44e0459f3..3aee7e8ad 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -136,7 +136,6 @@ namespace sat {
         m_user_scope_literals.reset();
         m_user_scope_literals.append(src.m_user_scope_literals);
 
-        std::cout << "copy: " << init_trail_size() << " " << src.init_trail_size() << "\n";
     }
 
     // -----------------------
@@ -1152,9 +1151,6 @@ namespace sat {
     }
 
     void solver::reinit_assumptions() {
-        if (at_search_lvl()) {
-            std::cout << " " << init_trail_size() << " " << m_trail.size() << "\n";
-        }
         if (tracking_assumptions() && at_base_lvl()) {
             TRACE("sat", tout << m_assumptions << "\n";);
             push();