diff --git a/src/tactic/bv/bv_bounds_tactic.cpp b/src/tactic/bv/bv_bounds_tactic.cpp
index d9703990c..052345df1 100644
--- a/src/tactic/bv/bv_bounds_tactic.cpp
+++ b/src/tactic/bv/bv_bounds_tactic.cpp
@@ -36,6 +36,11 @@ struct interval {
 
     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) {
+        // canonicalize full set
+        if (is_wrapped() && l == h + rational::one()) {
+            this->l = rational::zero();
+            this->h = uMaxInt(sz);
+        }
         SASSERT(invariant());
     }
 
diff --git a/src/tactic/core/ctx_simplify_tactic.cpp b/src/tactic/core/ctx_simplify_tactic.cpp
index 01937eb18..f0e0b0059 100644
--- a/src/tactic/core/ctx_simplify_tactic.cpp
+++ b/src/tactic/core/ctx_simplify_tactic.cpp
@@ -458,7 +458,11 @@ struct ctx_simplify_tactic::imp {
             }
             simplify(t, new_t);
             pop(scope_level() - old_lvl);
-            VERIFY(assert_expr(new_c, true));
+            if (!assert_expr(new_c, true)) {
+                r = new_t;
+                cache(ite, r);
+                return;
+            }
             simplify(e, new_e);
             pop(scope_level() - old_lvl);
             if (c == new_c && t == new_t && e == new_e) {