better rewriting for ule

Author: NikolajBjorner

src/ast/rewriter/bv_rewriter.cpp

@@ -514,10 +514,14 @@ br_status bv_rewriter::mk_leq_core(bool is_signed, expr * a, expr * b, expr_ref
     // for r1 = r2, (bvule a (2^n - r2 - 1)) 
     // other cases r1 > r2, r1 < r2 are TBD
     if (!is_signed && is_num1 && m_util.is_bv_add(b, a1, a2) && is_numeral(a1, r2, sz)) {
-        if (r1 == r2) {
-            result = m_util.mk_ule(a2, m_util.mk_numeral(-r2 - 1, sz));
-            return BR_REWRITE1;
+        result = m_util.mk_ule(a2, m_util.mk_numeral(-r2 - 1, sz));
+        if (r1 > r2) {
+            result = m().mk_and(result, m_util.mk_ule(m_util.mk_numeral(r1-r2, sz), a2));
+        }
+        else if (r1 < r2) {
+            result = m().mk_or(result, m_util.mk_ule(m_util.mk_numeral(r1-r2, sz), a2));
         }
+        return BR_REWRITE2;
     }
 
     if (m_le_extra) {