diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp
index e1c09e469..c096c1a30 100644
--- a/src/ast/rewriter/arith_rewriter.cpp
+++ b/src/ast/rewriter/arith_rewriter.cpp
@@ -624,16 +624,16 @@ br_status arith_rewriter::mk_le_ge_eq_core(expr * arg1, expr * arg2, op_kind kin
         switch (kind) {
         case LE: 
             result = m_util.mk_lt(t, m_util.mk_numeral(a2+1, false)); 
-            return BR_DONE;
+            return BR_REWRITE1;
         case GE: 
             result = m_util.mk_ge(t, m_util.mk_numeral(a2, false)); 
             return BR_REWRITE1;
         case EQ: 
             result = m_util.mk_ge(t, m_util.mk_numeral(a2, false));
             result = m().mk_and(m_util.mk_lt(t, m_util.mk_numeral(a2+1, false)), result);
-            return BR_DONE;
+            return BR_REWRITE3;
         }        
-    } 
+    }
     if ((m_arith_lhs || m_arith_ineq_lhs) && is_numeral(arg2, a2) && is_neg_poly(arg1, new_arg1)) {
         a2.neg();
         new_arg2 = m_util.mk_numeral(a2, m_util.is_int(new_arg1));
diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index 88e9fde32..1e053fe1b 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -824,6 +824,7 @@ br_status seq_rewriter::mk_seq_length(expr* a, expr_ref& result) {
         result = m_autil.mk_add(es.size(), es.c_ptr());
         return BR_REWRITE2;
     }
+#if 0
     expr* s = nullptr, *offset = nullptr, *length = nullptr;
     if (str().is_extract(a, s, offset, length)) {
         expr_ref len_s(str().mk_length(s), m());
@@ -837,11 +838,12 @@ br_status seq_rewriter::mk_seq_length(expr* a, expr_ref& result) {
         result = m().mk_ite(m_autil.mk_gt(m_autil.mk_add(offset, length), len_s),
                             m_autil.mk_sub(len_s, offset),
                             result);
-        result = m().mk_ite(m().mk_or(m_autil.mk_ge(offset, len_s), m_autil.mk_le(length, zero), m_autil.mk_lt(offset, zero)),
+        result = m().mk_ite(m().mk_or(m_autil.mk_le(len_s, offset), m_autil.mk_le(length, zero), m_autil.mk_lt(offset, zero)),
                             zero,
                             result);
         return BR_REWRITE_FULL;
     }
+#endif
     return BR_FAILED;
 }
 
@@ -3810,7 +3812,7 @@ br_status seq_rewriter::mk_eq_core(expr * l, expr * r, expr_ref & result) {
     }
     bool changed = false;
     if (reduce_eq_empty(l, r, result)) 
-        return BR_REWRITE3;
+        return BR_REWRITE_FULL;
 
     if (!reduce_eq(l, r, new_eqs, changed)) {
         result = m().mk_false();
@@ -4220,7 +4222,7 @@ bool seq_rewriter::reduce_eq_empty(expr* l, expr* r, expr_ref& result) {
         fmls.push_back(m_autil.mk_lt(offset, m_autil.mk_int(0)));
         fmls.push_back(m().mk_eq(s, l));
         fmls.push_back(m_autil.mk_lt(len, m_autil.mk_int(0)));
-        fmls.push_back(m_autil.mk_ge(offset, len_s));
+        fmls.push_back(m_autil.mk_le(len_s, offset));
         result = m().mk_or(fmls);
         return true;
     }