diff --git a/src/tactic/arith/bound_manager.cpp b/src/tactic/arith/bound_manager.cpp
index abde88a19..1ed3265e2 100644
--- a/src/tactic/arith/bound_manager.cpp
+++ b/src/tactic/arith/bound_manager.cpp
@@ -244,6 +244,8 @@ bool bound_manager::is_disjunctive_bound(expr * f, expr_dependency * d) {
 }
 
 void bound_manager::operator()(goal const & g) {
+    if (g.proofs_enabled())
+        return;
     unsigned sz = g.size();
     for (unsigned i = 0; i < sz; i++) {
         operator()(g.form(i), g.dep(i));
diff --git a/src/tactic/arith/normalize_bounds_tactic.cpp b/src/tactic/arith/normalize_bounds_tactic.cpp
index 807881503..daaa9bc3c 100644
--- a/src/tactic/arith/normalize_bounds_tactic.cpp
+++ b/src/tactic/arith/normalize_bounds_tactic.cpp
@@ -84,7 +84,7 @@ class normalize_bounds_tactic : public tactic {
             bool produce_proofs = in->proofs_enabled();
             tactic_report report("normalize-bounds", *in);
             
-            m_bm(*in);
+            m_bm(*in);            
             
             if (!has_lowers()) {
                 result.push_back(in.get());
@@ -119,11 +119,14 @@ class normalize_bounds_tactic : public tactic {
             
             m_rw.set_substitution(&subst);
             expr_ref   new_curr(m);
-            proof_ref  new_pr(m);
-            unsigned size = in->size();
-            for (unsigned idx = 0; !in->inconsistent() && idx < size; idx++) {
+            
+            for (unsigned idx = 0; !in->inconsistent() && idx < in->size(); idx++) {
                 expr * curr = in->form(idx);
+                proof_ref  new_pr(m);
                 m_rw(curr, new_curr, new_pr);
+                std::cout << new_curr << "\n";
+                std::cout << new_pr << "\n";
+                std::cout << expr_ref(in->pr(idx), m) << "\n";
                 if (produce_proofs) {
                     proof * pr = in->pr(idx);
                     new_pr     = m.mk_modus_ponens(pr, new_pr);