diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index a90b193f9..e7ca694e8 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -4136,6 +4136,30 @@ 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;
+    unsigned len = 0;
+    rational rlen;
+    bool is_empty = false;
+    if (str().is_string(lo, s) && s.length() != 1) 
+        is_empty = true;
+    if (str().is_string(hi, s) && s.length() != 1) 
+        is_empty = true;
+    min_length(lo, len);
+    if (len > 1)
+        is_empty = true;
+    min_length(hi, len);
+    if (len > 1)
+        is_empty = true;
+    if (max_length(lo, rlen) && rlen == 0)
+        is_empty = true;
+    if (max_length(hi, rlen) && rlen == 0)
+        is_empty = true;
+    if (is_empty) {
+        sort* srt = re().mk_re(lo->get_sort());
+        result = re().mk_empty(srt);
+        return BR_DONE;
+    }
+
     return BR_FAILED;
 }
 
diff --git a/src/smt/seq_eq_solver.cpp b/src/smt/seq_eq_solver.cpp
index 465b50604..0ea878349 100644
--- a/src/smt/seq_eq_solver.cpp
+++ b/src/smt/seq_eq_solver.cpp
@@ -1067,6 +1067,8 @@ bool theory_seq::check_length_coherence() {
         if (check_length_coherence(e)) {
             return true;
         }
+        if (!ctx.e_internalized(e))
+            change = true;
         enode* n = ensure_enode(e);
         enode* r = n->get_root();
         if (r != n && has_length(r->get_expr())) {
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 3b7c462fa..4baa1f476 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -403,7 +403,10 @@ final_check_status theory_seq::final_check_eh() {
         TRACEFIN("branch_ne");
         return FC_CONTINUE;
     }
+
     if (m_unhandled_expr) {
+        TRACEFIN("give_up");
+        TRACE("seq", tout << "unhandled: " << mk_pp(m_unhandled_expr, m) << "\n";);
         return FC_GIVEUP;
     }
     if (is_solved()) {
@@ -1412,26 +1415,29 @@ bool theory_seq::internalize_atom(app* a, bool) {
 
 bool theory_seq::internalize_term(app* term) {
     m_has_seq = true;
+
+    if (m_util.str.is_in_re(term)) 
+        mk_var(ensure_enode(term->get_arg(0)));
+
+    if (m_util.str.is_length(term))
+        mk_var(ensure_enode(term->get_arg(0)));
+    
     if (ctx.e_internalized(term)) {
-        enode* e = ctx.get_enode(term);
-        mk_var(e);
+        mk_var(ctx.get_enode(term));
         return true;
-    }
+    }    
 
     if (m.is_bool(term) && 
         (m_util.str.is_in_re(term) || m_sk.is_skolem(term))) {
-        if (m_util.str.is_in_re(term)) {
-            mk_var(ensure_enode(term->get_arg(0)));
-        }
         bool_var bv = ctx.mk_bool_var(term);
         ctx.set_var_theory(bv, get_id());
         ctx.mark_as_relevant(bv);
         return true;
     }
 
-    for (auto arg : *term) {        
+    for (auto arg : *term)         
         mk_var(ensure_enode(arg));
-    }
+
     if (m.is_bool(term)) {
         bool_var bv = ctx.mk_bool_var(term);
         ctx.set_var_theory(bv, get_id());