diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp
index fc0e5a807..be9b5f375 100644
--- a/src/ast/rewriter/bv_rewriter.cpp
+++ b/src/ast/rewriter/bv_rewriter.cpp
@@ -320,6 +320,21 @@ br_status bv_rewriter::mk_leq_core(bool is_signed, expr * a, expr * b, expr_ref
         }
     }
 
+    expr* a1, *a2, *a3, *a4, *a5, *a6;
+    // (bvsle (- x (srem x c1)) c2) -> (bvsle x (+ c1 c2 - 1))
+    // (bvsle (+ x (* -1 (srem_i x c1))) c2)
+    // pre: (and (> c1 0) (> c2 0) (= c2 % c1 0) (<= (+ c1 c2 -1) max_int))
+    if (is_signed && is_num2 && m_util.is_bv_add(a, a1, a2) &&
+        m_util.is_bv_mul(a2, a3, a4) && is_numeral(a3, r1, sz) &&
+        m_util.norm(r1, sz, is_signed).is_minus_one() &&
+        m_util.is_bv_sremi(a4, a5, a6) && is_numeral(a6, r1, sz) &&
+        (r1 = m_util.norm(r1, sz, is_signed), r1.is_pos()) &&
+        r2.is_pos() &&
+        (r2 % r1).is_zero() && r1 + r2 - rational::one() < rational::power_of_two(sz-1)) {
+        result = m_util.mk_sle(a1, m_util.mk_numeral(r1 + r2 - rational::one(), sz));
+        return BR_REWRITE2;
+    }
+
 #if 0
     if (!is_signed && m_util.is_concat(b) && to_app(b)->get_num_args() == 2 && m_util.is_zero(to_app(b)->get_arg(0))) {
         //
diff --git a/src/tactic/bv/bv_bounds_tactic.cpp b/src/tactic/bv/bv_bounds_tactic.cpp
index 5a37d166a..d9703990c 100644
--- a/src/tactic/bv/bv_bounds_tactic.cpp
+++ b/src/tactic/bv/bv_bounds_tactic.cpp
@@ -32,14 +32,16 @@ struct interval {
     // l > h: [0, h] U [l, UMAX_INT]
     rational l, h;
     unsigned sz;
+    bool tight;
 
-    explicit interval() : l(0), h(0), sz(0) {}
-    interval(const rational& l, const rational& h, unsigned sz) : l(l), h(h), sz(sz) {
+    explicit interval() : l(0), h(0), sz(0), tight(false) {}
+    interval(const rational& l, const rational& h, unsigned sz, bool tight = false) : l(l), h(h), sz(sz), tight(tight) {
         SASSERT(invariant());
     }
 
     bool invariant() const {
-        return !l.is_neg() && !h.is_neg() && l <= uMaxInt(sz) && h <= uMaxInt(sz);
+        return !l.is_neg() && !h.is_neg() && l <= uMaxInt(sz) && h <= uMaxInt(sz) &&
+               (!is_wrapped() || l != h+rational::one());
     }
 
     bool is_full() const { return l.is_zero() && h == uMaxInt(sz); }
@@ -113,13 +115,18 @@ struct interval {
                 return false;
 
             // 0 .. l.. l' ... h ... h'
-            result = interval(std::max(l, b.l), std::min(h, b.h), sz);
+            result = interval(std::max(l, b.l), std::min(h, b.h), sz, tight && b.tight);
         }
         return true;
     }
 
     /// return false if negation is empty
     bool negate(interval& result) const {
+        if (!tight) {
+            result = interval(rational::zero(), uMaxInt(sz), true);
+            return true;
+        }
+
         if (is_full())
             return false;
         if (l.is_zero()) {
@@ -152,40 +159,43 @@ class bv_bounds_simplifier : public ctx_simplify_tactic::simplifier {
 
         if (m_bv.is_bv_ule(e, lhs, rhs)) {
             if (m_bv.is_numeral(lhs, n, sz)) { // C ule x <=> x uge C
-                b = interval(n, uMaxInt(sz), sz);
+                if (m_bv.is_numeral(rhs))
+                    return false;
+                b = interval(n, uMaxInt(sz), sz, true);
                 v = rhs;
                 return true;
             }
             if (m_bv.is_numeral(rhs, n, sz)) { // x ule C
-                b = interval(rational::zero(), n, sz);
+                b = interval(rational::zero(), n, sz, true);
                 v = lhs;
                 return true;
             }
         } else if (m_bv.is_bv_sle(e, lhs, rhs)) {
             if (m_bv.is_numeral(lhs, n, sz)) { // C sle x <=> x sge C
-                b = interval(n, rational::power_of_two(sz-1) - rational::one(), sz);
+                if (m_bv.is_numeral(rhs))
+                    return false;
+                b = interval(n, rational::power_of_two(sz-1) - rational::one(), sz, true);
                 v = rhs;
                 return true;
             }
             if (m_bv.is_numeral(rhs, n, sz)) { // x sle C
-                b = interval(rational::power_of_two(sz-1), n, sz);
+                b = interval(rational::power_of_two(sz-1), n, sz, true);
                 v = lhs;
                 return true;
             }
         } else if (m.is_eq(e, lhs, rhs)) {
             if (m_bv.is_numeral(lhs, n, sz)) {
-                b = interval(n, n, sz);
+                if (m_bv.is_numeral(rhs))
+                    return false;
+                b = interval(n, n, sz, true);
                 v = rhs;
                 return true;
             }
             if (m_bv.is_numeral(rhs, n, sz)) {
-                b = interval(n, n, sz);
+                b = interval(n, n, sz, true);
                 v = lhs;
                 return true;
             }
-        } else if (m.is_not(e, lhs)) {
-            if (is_bound(lhs, v, b))
-                return b.negate(b);
         }
         return false;
     }
@@ -199,7 +209,7 @@ public:
 
     virtual ~bv_bounds_simplifier() {}
 
-    virtual void assert_expr(expr * t, bool sign) {
+    virtual bool assert_expr(expr * t, bool sign) {
         while (m.is_not(t, t)) {
             sign = !sign;
         }
@@ -207,34 +217,54 @@ public:
         interval b;
         expr* t1;
         if (is_bound(t, t1, b)) {
+            SASSERT(!m_bv.is_numeral(t1));
             if (sign)
                 VERIFY(b.negate(b));
 
             push();
             TRACE("bv", tout << (sign?"(not ":"") << mk_pp(t, m) << (sign ? ")" : "") << ": " << mk_pp(t1, m) << " in " << b << "\n";);
             interval& r = m_bound->insert_if_not_there2(t1, b)->get_data().m_value;
-            VERIFY(r.intersect(b, r));
+            return r.intersect(b, r);
         }
+        return true;
     }
 
     virtual bool simplify(expr* t, expr_ref& result) {
         expr* t1;
         interval b, ctx, intr;
         result = 0;
+        bool sign = false;
+
+        while (m.is_not(t, t)) {
+            sign = !sign;
+        }
+
         if (!is_bound(t, t1, b))
             return false;
 
-        if (m_bound->find(t1, ctx)) {
-            if (!b.intersect(ctx, intr)) {
+        if (sign && b.tight) {
+            sign = false;
+            if (!b.negate(b)) {
                 result = m.mk_false();
-            } else if (intr.l == intr.h && intr != b) {
-                result = m.mk_eq(t1, m_bv.mk_numeral(intr.l, m.get_sort(t1)));
-            } else if (ctx.implies(b)) {
-                result = m.mk_true();
+                return true;
             }
         }
 
+        if (m_bound->find(t1, ctx)) {
+            if (ctx.implies(b)) {
+                result = m.mk_true();
+            } else if (!b.intersect(ctx, intr)) {
+                result = m.mk_false();
+            } else if (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) {
+            result = m.mk_true();
+        }
+
         CTRACE("bv", result != 0, tout << mk_pp(t, m) << " " << b << " (ctx: " << ctx << ") (intr: " << intr << "): " << result << "\n";);
+        if (sign && result != 0)
+            result = m.mk_not(result);
         return result != 0;
     }
 
diff --git a/src/tactic/core/ctx_simplify_tactic.cpp b/src/tactic/core/ctx_simplify_tactic.cpp
index 95be200a8..01937eb18 100644
--- a/src/tactic/core/ctx_simplify_tactic.cpp
+++ b/src/tactic/core/ctx_simplify_tactic.cpp
@@ -34,7 +34,7 @@ class ctx_propagate_assertions : public ctx_simplify_tactic::simplifier {
 public:
     ctx_propagate_assertions(ast_manager& m);
     virtual ~ctx_propagate_assertions() {}
-    virtual void assert_expr(expr * t, bool sign);
+    virtual bool assert_expr(expr * t, bool sign);
     virtual bool simplify(expr* t, expr_ref& result);
     virtual void push();
     virtual void pop(unsigned num_scopes);
@@ -45,7 +45,7 @@ public:
 
 ctx_propagate_assertions::ctx_propagate_assertions(ast_manager& m): m(m), m_trail(m) {}
 
-void ctx_propagate_assertions::assert_expr(expr * t, bool sign) {
+bool ctx_propagate_assertions::assert_expr(expr * t, bool sign) {
     
     expr * p = t;
     while (m.is_not(t, t)) {
@@ -64,6 +64,7 @@ void ctx_propagate_assertions::assert_expr(expr * t, bool sign) {
         else if (m.is_value(lhs))
             assert_eq_val(rhs, to_app(lhs), mk_scope);
     }
+    return true;
 }
 
 void ctx_propagate_assertions::assert_eq_val(expr * t, app * val, bool mk_scope) {
@@ -307,8 +308,8 @@ struct ctx_simplify_tactic::imp {
         CASSERT("ctx_simplify_tactic", check_cache());
     }
 
-    void assert_expr(expr * t, bool sign) {
-        m_simp->assert_expr(t, sign);
+    bool assert_expr(expr * t, bool sign) {
+        return m_simp->assert_expr(t, sign);
     }
 
     bool is_cached(expr * t, expr_ref & r) {
@@ -370,6 +371,9 @@ struct ctx_simplify_tactic::imp {
             simplify(arg, new_arg);
             if (new_arg != arg)
                 modified = true;
+            if (i < num_args - 1 && !m.is_true(new_arg) && !m.is_false(new_arg) && !assert_expr(new_arg, OR))
+                new_arg = m.mk_false();
+
             if ((OR && m.is_false(new_arg)) ||
                 (!OR && m.is_true(new_arg))) {
                 modified = true;
@@ -383,8 +387,6 @@ struct ctx_simplify_tactic::imp {
                 return;
             }
             new_args.push_back(new_arg);
-            if (i < num_args - 1)
-                assert_expr(new_arg, OR);
         }
         pop(scope_level() - old_lvl);
 
@@ -398,6 +400,9 @@ struct ctx_simplify_tactic::imp {
             simplify(arg, new_arg);
             if (new_arg != arg)
                 modified = true;
+            if (i > 0 && !m.is_true(new_arg) && !m.is_false(new_arg) && !assert_expr(new_arg, OR))
+                new_arg = m.mk_false();
+
             if ((OR && m.is_false(new_arg)) ||
                 (!OR && m.is_true(new_arg))) {
                 modified = true;
@@ -411,8 +416,6 @@ struct ctx_simplify_tactic::imp {
                 return;
             }
             new_new_args.push_back(new_arg);
-            if (i > 0)
-                assert_expr(new_arg, OR);
         }
         pop(scope_level() - old_lvl);
 
@@ -448,10 +451,14 @@ struct ctx_simplify_tactic::imp {
         else {
             expr_ref new_t(m);
             expr_ref new_e(m);
-            assert_expr(new_c, false);
+            if (!assert_expr(new_c, false)) {
+                simplify(e, r);
+                cache(ite, r);
+                return;
+            }
             simplify(t, new_t);
             pop(scope_level() - old_lvl);
-            assert_expr(new_c, true);
+            VERIFY(assert_expr(new_c, true));
             simplify(e, new_e);
             pop(scope_level() - old_lvl);
             if (c == new_c && t == new_t && e == new_e) {
diff --git a/src/tactic/core/ctx_simplify_tactic.h b/src/tactic/core/ctx_simplify_tactic.h
index fccb25d3b..3c95ca554 100644
--- a/src/tactic/core/ctx_simplify_tactic.h
+++ b/src/tactic/core/ctx_simplify_tactic.h
@@ -28,7 +28,7 @@ public:
         goal_num_occurs* m_occs;
     public:
         virtual ~simplifier() {}
-        virtual void assert_expr(expr * t, bool sign) = 0;
+        virtual bool assert_expr(expr * t, bool sign) = 0;
         virtual bool simplify(expr* t, expr_ref& result) = 0;
         virtual void push() = 0;
         virtual void pop(unsigned num_scopes) = 0;