diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp b/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp
index 42d51e706..63843d31e 100644
--- a/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp
+++ b/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp
@@ -335,9 +335,6 @@ MK_PARAMETRIC_UNARY_REDUCE(reduce_sign_extend, mk_sign_extend);
             SASSERT(num == 2);
             if (butil().is_bv(args[0])) {
                 reduce_eq(args[0], args[1], result);
-                std::cout << "reduce eq: " << mk_pp(args[0], m()) << "\n" << mk_pp(args[1], m()) << "\n";
-                std::cout << mk_pp(result, m()) << "\n";
-
                 return BR_DONE;
             }
             return BR_FAILED;
diff --git a/src/tactic/tactic.cpp b/src/tactic/tactic.cpp
index 9b4f42a71..198872cf5 100644
--- a/src/tactic/tactic.cpp
+++ b/src/tactic/tactic.cpp
@@ -41,13 +41,11 @@ struct tactic_report::imp {
     goal const &    m_goal;
     stopwatch       m_watch;
     double          m_start_memory;
-    unsigned        m_start_exprs;
 
     imp(char const * id, goal const & g):
         m_id(id),
         m_goal(g),
-        m_start_memory(static_cast<double>(memory::get_allocation_size())/static_cast<double>(1024*1024)),
-        m_start_exprs(g.num_exprs()){
+        m_start_memory(static_cast<double>(memory::get_allocation_size())/static_cast<double>(1024*1024)) {
         m_watch.start();
     }
         
@@ -55,7 +53,7 @@ struct tactic_report::imp {
         m_watch.stop();
         double end_memory = static_cast<double>(memory::get_allocation_size())/static_cast<double>(1024*1024);
         verbose_stream() << "(" << m_id
-                         << " :num-exprs " << m_start_exprs << " -> " << m_goal.num_exprs()
+                         << " :num-exprs " << m_goal.num_exprs()
                          << " :num-asts " << m_goal.m().get_num_asts()
                          << " :time " << std::fixed << std::setprecision(2) << m_watch.get_seconds()
                          << " :before-memory " << std::fixed << std::setprecision(2) << m_start_memory