diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp b/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp
index 63843d31e..42d51e706 100644
--- a/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp
+++ b/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp
@@ -335,6 +335,9 @@ 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/smt/smt_context.cpp b/src/smt/smt_context.cpp
index d86b2da77..f68df30ab 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -2872,7 +2872,7 @@ namespace smt {
                 // mark_as_relevant(l); <<< not needed
                 // internalize_assertion marked l as relevant.
                 SASSERT(is_relevant(l));
-                TRACE("assumptions", tout << mk_pp(curr_assumption, m_manager) << "\n";);
+                TRACE("assumptions", tout << l << ":" << mk_pp(curr_assumption, m_manager) << "\n";);
                 if (m_manager.proofs_enabled())
                     assign(l, mk_justification(justification_proof_wrapper(*this, pr)));
                 else
@@ -2907,6 +2907,7 @@ namespace smt {
             literal l = *it;
             TRACE("unsat_core_bug", tout << "answer literal: " << l << "\n";);
             SASSERT(get_bdata(l.var()).m_assumption);
+            if (!m_literal2assumption.contains(l.index())) l.neg();
             SASSERT(m_literal2assumption.contains(l.index()));
             expr * a = m_literal2assumption[l.index()];
             if (!already_found_assumptions.contains(a)) {
diff --git a/src/tactic/arith/card2bv_tactic.cpp b/src/tactic/arith/card2bv_tactic.cpp
index 5f9f28898..e5f699eaa 100644
--- a/src/tactic/arith/card2bv_tactic.cpp
+++ b/src/tactic/arith/card2bv_tactic.cpp
@@ -221,6 +221,7 @@ namespace pb {
         default:
             UNREACHABLE();
         }
+        TRACE("card2bv", tout << result << "\n";);
     }
 
     struct argc_t {
@@ -268,6 +269,8 @@ namespace pb {
                 SASSERT(argcs[i].m_coeff >= argcs[i+1].m_coeff);
             }
             );
+        result = m.mk_app(f, sz, args);
+        TRACE("card2bv", tout << result << "\n";);
         argc_cache cache;
         expr_ref_vector trail(m);
         vector<rational> todo_k;
@@ -277,7 +280,7 @@ namespace pb {
         decl_kind kind = f->get_decl_kind();
         argc_entry entry1;
         while (!todo_i.empty()) {
-
+            SASSERT(todo_i.size() == todo_k.size());
             if (cache.size() > max_clauses) {
                 return BR_FAILED;
             }
@@ -307,13 +310,17 @@ namespace pb {
                     break;
                 case OP_AT_LEAST_K:
                 case OP_PB_GE:
-                    if (coeff < k) {
+                    if (k.is_zero()) {
+                        entry.m_value = m.mk_true();
+                    }
+                    else if (coeff < k) {
                         entry.m_value = m.mk_false();
                     }
                     else if (coeff.is_zero()) {
                         entry.m_value = m.mk_true();
                     }
                     else {
+                        SASSERT(coeff >= k && k.is_pos());
                         entry.m_value = arg;
                     }
                     break;
@@ -345,7 +352,7 @@ namespace pb {
                 todo_k.push_back(k);
             }
             entry.m_k -= coeff;
-            if (kind != OP_PB_EQ && entry.m_k.is_neg()) {
+            if (kind != OP_PB_EQ && !entry.m_k.is_pos()) {
                 switch (kind) {
                 case OP_AT_MOST_K:
                 case OP_PB_LE:
@@ -379,6 +386,7 @@ namespace pb {
         argc_entry entry(0, pb.get_k(f));
         VERIFY(cache.find(entry, entry));
         result = entry.m_value;
+        TRACE("card2bv", tout << result << "\n";);
         return BR_DONE;
     }
 
diff --git a/src/tactic/tactic.cpp b/src/tactic/tactic.cpp
index 198872cf5..9b4f42a71 100644
--- a/src/tactic/tactic.cpp
+++ b/src/tactic/tactic.cpp
@@ -41,11 +41,13 @@ 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_memory(static_cast<double>(memory::get_allocation_size())/static_cast<double>(1024*1024)),
+        m_start_exprs(g.num_exprs()){
         m_watch.start();
     }
         
@@ -53,7 +55,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_goal.num_exprs()
+                         << " :num-exprs " << m_start_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