diff --git a/src/ast/rewriter/pb_rewriter_def.h b/src/ast/rewriter/pb_rewriter_def.h
index 7e2a13779..3c60babce 100644
--- a/src/ast/rewriter/pb_rewriter_def.h
+++ b/src/ast/rewriter/pb_rewriter_def.h
@@ -247,7 +247,7 @@ lbool pb_rewriter_util<PBU>::normalize(typename PBU::args_t& args, typename PBU:
     // example: k = 5, min = 3, max = 4: 5/3 -> 2   5/4 -> 1, n = 2
     // replace all coefficients by 1, and k by 2.
     //
-    if (false && !k.is_one()) {
+    if (!k.is_one()) {
         PBU::numeral min = args[0].second, max = args[0].second;
         for (unsigned i = 1; i < args.size(); ++i) {
             if (args[i].second < min) min = args[i].second;
diff --git a/src/math/simplex/simplex.h b/src/math/simplex/simplex.h
index 0ea3bebf0..1370d4bae 100644
--- a/src/math/simplex/simplex.h
+++ b/src/math/simplex/simplex.h
@@ -59,9 +59,11 @@ namespace simplex {
 
         struct stats {
             unsigned m_num_pivots;
+            unsigned m_num_infeasible;
+            unsigned m_num_checks;
             stats() { reset(); }
             void reset() {
-                memset(this, sizeof(*this), 0);
+                memset(this, 0, sizeof(*this));
             }
         };
 
diff --git a/src/math/simplex/simplex_def.h b/src/math/simplex/simplex_def.h
index ab416e042..fa6cdf234 100644
--- a/src/math/simplex/simplex_def.h
+++ b/src/math/simplex/simplex_def.h
@@ -250,6 +250,7 @@ namespace simplex {
 
     template<typename Ext>
     lbool simplex<Ext>::make_feasible() {
+        ++m_stats.m_num_checks;
         m_left_basis.reset();
         m_infeasible_var = null_var;
         unsigned num_iterations = 0;
@@ -266,6 +267,7 @@ namespace simplex {
             if (!make_var_feasible(v)) {
                 m_to_patch.insert(v);
                 m_infeasible_var = v;
+                ++m_stats.m_num_infeasible;
                 return l_false;
             }
             ++num_iterations;
@@ -873,6 +875,8 @@ namespace simplex {
     void simplex<Ext>::collect_statistics(::statistics & st) const {
         M.collect_statistics(st);
         st.update("simplex num pivots", m_stats.m_num_pivots);
+        st.update("simplex num infeasible", m_stats.m_num_infeasible);
+        st.update("simplex num checks", m_stats.m_num_checks);
     }
         
 
diff --git a/src/math/simplex/sparse_matrix.h b/src/math/simplex/sparse_matrix.h
index b711c91af..e4cb33f07 100644
--- a/src/math/simplex/sparse_matrix.h
+++ b/src/math/simplex/sparse_matrix.h
@@ -44,7 +44,7 @@ namespace simplex {
             unsigned m_add_rows;
             stats() { reset(); }
             void reset() {
-                memset(this, sizeof(*this), 0);
+                memset(this, 0, sizeof(*this));
             }
         };
 
diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp
index bc21ed243..191481ae4 100644
--- a/src/smt/theory_pb.cpp
+++ b/src/smt/theory_pb.cpp
@@ -546,12 +546,10 @@ namespace smt {
                         mpq_inf zero(mpq(0),mpq(0)), one(mpq(1),mpq(0));
                         switch(ctx.get_assignment(rep.lit(i))) {
                         case l_true:
-                            std::cout << "true\n";
                             VERIFY(update_bound(v, literal(v), true, one));
                             m_simplex.set_lower(v, one);
                             break;
                         case l_false:
-                            std::cout << "false\n";
                             VERIFY(update_bound(v, ~literal(v), false, zero));
                             m_simplex.set_upper(v, zero);
                             break;