diff --git a/src/tactic/bv/bv_bounds_tactic.cpp b/src/tactic/bv/bv_bounds_tactic.cpp
index 317c17f12..381802ac5 100644
--- a/src/tactic/bv/bv_bounds_tactic.cpp
+++ b/src/tactic/bv/bv_bounds_tactic.cpp
@@ -262,7 +262,7 @@ public:
                 result = m.mk_true();
             } else if (!b.intersect(ctx, intr)) {
                 result = m.mk_false();
-            } else if (intr.l == intr.h) {
+            } else if (false && intr.l == intr.h) {
                 result = m.mk_eq(t1, m_bv.mk_numeral(intr.l, m.get_sort(t1)));
             }
         } else if (b.is_full() && b.tight) {
diff --git a/src/tactic/core/ctx_simplify_tactic.cpp b/src/tactic/core/ctx_simplify_tactic.cpp
index 3bcadb03d..2847e403f 100644
--- a/src/tactic/core/ctx_simplify_tactic.cpp
+++ b/src/tactic/core/ctx_simplify_tactic.cpp
@@ -529,6 +529,37 @@ struct ctx_simplify_tactic::imp {
         return sz;
     }
 
+    void process_goal(goal & g) {
+        SASSERT(scope_level() == 0);
+        // go forwards
+        unsigned old_lvl = scope_level();
+        unsigned sz = g.size();
+        expr_ref r(m);
+        for (unsigned i = 0; !g.inconsistent() && i < sz; ++i) {
+            m_depth = 0;            
+            simplify(g.form(i), r);
+            if (i < sz - 1 && !m.is_true(r) && !m.is_false(r) && !g.dep(i) && !assert_expr(r, false)) {
+                r = m.mk_false();
+            }
+            g.update(i, r, 0, g.dep(i));
+        }
+        pop(scope_level() - old_lvl);
+
+        // go backwards
+        sz = g.size();
+        for (unsigned i = sz; !g.inconsistent() && i > 0; ) {
+            m_depth = 0;
+            --i;
+            simplify(g.form(i), r);
+            if (i > 0 && !m.is_true(r) && !m.is_false(r) && !g.dep(i) && !assert_expr(r, false)) {
+                r = m.mk_false();
+            }
+            g.update(i, r, 0, g.dep(i));
+        }
+        pop(scope_level() - old_lvl);
+        SASSERT(scope_level() == 0);
+    }
+
     void process(expr * s, expr_ref & r) {
         TRACE("ctx_simplify_tactic", tout << "simplifying:\n" << mk_ismt2_pp(s, m) << "\n";);
         SASSERT(scope_level() == 0);
@@ -546,24 +577,22 @@ struct ctx_simplify_tactic::imp {
 
     void operator()(goal & g) {
         SASSERT(g.is_well_sorted());
-        bool proofs_enabled = g.proofs_enabled();
         m_occs.reset();
         m_occs(g);
         m_num_steps = 0;
-        expr_ref r(m);
-        proof * new_pr = 0;
         tactic_report report("ctx-simplify", g);
-        unsigned sz = g.size();
-        for (unsigned i = 0; i < sz; i++) {
-            if (g.inconsistent())
-                return;
-            expr * t = g.form(i);
-            process(t, r);
-            if (proofs_enabled) {
-                proof * pr = g.pr(i);
-                new_pr     = m.mk_modus_ponens(pr, m.mk_rewrite_star(t, r, 0, 0)); // TODO :-)
+        if (g.proofs_enabled()) {
+            expr_ref r(m);
+            unsigned sz = g.size();
+            for (unsigned i = 0; !g.inconsistent() && i < sz; ++i) {
+                expr * t = g.form(i);
+                process(t, r);
+                proof* new_pr = m.mk_modus_ponens(g.pr(i), m.mk_rewrite_star(t, r, 0, 0)); // TODO :-)
+                g.update(i, r, new_pr, g.dep(i));
             }
-            g.update(i, r, new_pr, g.dep(i));
+        }
+        else {
+            process_goal(g);
         }
         IF_VERBOSE(TACTIC_VERBOSITY_LVL, verbose_stream() << "(ctx-simplify :num-steps " << m_num_steps << ")\n";);
         SASSERT(g.is_well_sorted());