diff --git a/src/tactic/bv/bv_bounds_tactic.cpp b/src/tactic/bv/bv_bounds_tactic.cpp
index 22b74db77..a279e441b 100644
--- a/src/tactic/bv/bv_bounds_tactic.cpp
+++ b/src/tactic/bv/bv_bounds_tactic.cpp
@@ -694,7 +694,8 @@ namespace {
             bool was_updated = true;
             if (b.is_full() && b.tight) {
                 r = m.mk_true();
-            } else if (m_bound.find(t1, ctx)) {
+            } 
+            else if (m_bound.find(t1, ctx)) {
                 if (ctx.implies(b)) {
                     r = m.mk_true();
                 } 
@@ -705,12 +706,15 @@ namespace {
                     r = m.mk_eq(t1, m_bv.mk_numeral(rational(intr.l, rational::ui64()),
                                                     m.get_sort(t1)));
                 }
+                else {
+                    was_updated = false;
+                }
             }
             else {
                 was_updated = false;
             }
 
-            CTRACE("bv", was_updated, tout << mk_pp(t, m) << " " << b << " (ctx: " << ctx << ") (intr: " << intr << "): " << r << "\n";);
+            TRACE("bv", tout << mk_pp(t, m) << " " << b << " (ctx: " << ctx << ") (intr: " << intr << "): " << r << "\n";);
             if (sign && was_updated)
                 r = m.mk_not(r);
         }
diff --git a/src/tactic/core/dom_simplify_tactic.cpp b/src/tactic/core/dom_simplify_tactic.cpp
index 3a6d55569..ee94c5e57 100644
--- a/src/tactic/core/dom_simplify_tactic.cpp
+++ b/src/tactic/core/dom_simplify_tactic.cpp
@@ -242,7 +242,7 @@ expr_ref dom_simplify_tactic::simplify_ite(app * ite) {
             r = new_t;
         }
         else {
-            TRACE("tactic", tout << new_c << "\n" << new_t << "\n" << new_e << "\n";);
+            TRACE("simplify", tout << new_c << "\n" << new_t << "\n" << new_e << "\n";);
             r = m.mk_ite(new_c, new_t, new_e);
         }        
     }