diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index 6fd518cb0..24df51845 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -5024,12 +5024,14 @@ br_status seq_rewriter::mk_re_star(expr* a, expr_ref& result) {
  * (re.range c_1 c_n) 
  */
 br_status seq_rewriter::mk_re_range(expr* lo, expr* hi, expr_ref& result) {
-    zstring s;
+    zstring slo, shi;
     unsigned len = 0;
     bool is_empty = false;
-    if (str().is_string(lo, s) && s.length() != 1) 
+    if (str().is_string(lo, slo) && slo.length() != 1) 
         is_empty = true;
-    if (str().is_string(hi, s) && s.length() != 1) 
+    if (str().is_string(hi, shi) && shi.length() != 1) 
+        is_empty = true;
+    if (slo.length() == 1 && shi.length() == 1 && slo[0] > shi[0])
         is_empty = true;
     len = min_length(lo).second;
     if (len > 1)
@@ -5246,7 +5248,17 @@ br_status seq_rewriter::reduce_re_is_empty(expr* r, expr_ref& result) {
     else if (re().is_range(r, r1, r2) && 
              str().is_string(r1, s1) && str().is_string(r2, s2) && 
              s1.length() == 1 && s2.length() == 1) {
-        result = m().mk_bool_val(s1[0] <= s2[0]);
+        result = m().mk_bool_val(s1[0] > s2[0]);
+        return BR_DONE;
+    }
+    else if (re().is_range(r, r1, r2) && 
+             str().is_string(r1, s1) && s1.length() != 1) {
+        result = m().mk_true();
+        return BR_DONE;
+    }
+    else if (re().is_range(r, r1, r2) && 
+             str().is_string(r2, s2) && s2.length() != 1) {
+        result = m().mk_true();
         return BR_DONE;
     }
     else if ((re().is_loop(r, r1, lo) ||
@@ -5307,6 +5319,7 @@ br_status seq_rewriter::mk_le_core(expr * l, expr * r, expr_ref & result) {
 }
 
 br_status seq_rewriter::mk_eq_core(expr * l, expr * r, expr_ref & result) {
+    TRACE("seq", tout << mk_pp(l, m()) << " == " << mk_pp(r, m()) << "\n");
     expr_ref_vector res(m());
     expr_ref_pair_vector new_eqs(m());
     if (m_util.is_re(l)) {