From 121b3b60f3dba70d6a5189233df764f422d9e1d7 Mon Sep 17 00:00:00 2001
From: Nuno Lopes <nlopes@microsoft.com>
Date: Fri, 19 Feb 2016 09:42:42 +0000
Subject: [PATCH] bv_bounds/ctx_simplify: improve handling of (ite x a b) where
 (not x) is proved to be false

---
 src/tactic/bv/bv_bounds_tactic.cpp      | 5 +++++
 src/tactic/core/ctx_simplify_tactic.cpp | 6 +++++-
 2 files changed, 10 insertions(+), 1 deletion(-)

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) {