diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index b9cb5f8d7..eb6337e5a 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -699,9 +699,11 @@ br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& resu
     if (lengthPos) {
         
         m_lhs.reset();
-        expr_ref_vector lens(m()), other(m());
+        expr_ref_vector lens(m());
         m_util.str.get_concat(a, m_lhs);
-        get_lengths(b, lens, other, pos);
+        if (!get_lengths(b, lens, pos)) {
+            return BR_FAILED;
+        }
         unsigned rsz = lens.size();
         unsigned i = 0;
         for (; i < m_lhs.size(); ++i) {
@@ -728,9 +730,6 @@ br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& resu
         for (expr* rhs : lens) {
             t2 = m_autil.mk_add(t2, m_util.str.mk_length(rhs));
         }
-        for (expr* rhs : other) {
-            t2 = m_autil.mk_add(t2, rhs);
-        }
         result = m_util.str.mk_substr(t1, t2, c);
         return BR_REWRITE2;
     }
@@ -782,12 +781,12 @@ br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& resu
     return BR_REWRITE3;
 }
 
-void seq_rewriter::get_lengths(expr* e, expr_ref_vector& lens, expr_ref_vector& other, rational& pos) {
+bool seq_rewriter::get_lengths(expr* e, expr_ref_vector& lens, rational& pos) {
     expr* arg = nullptr;
     rational pos1;
     if (m_autil.is_add(e)) {
         for (expr* arg1 : *to_app(e)) {
-            get_lengths(arg1, lens, other, pos);
+            if (!get_lengths(arg1, lens, pos)) return false;
         }
     }
     else if (m_util.str.is_length(e, arg)) {
@@ -797,8 +796,9 @@ void seq_rewriter::get_lengths(expr* e, expr_ref_vector& lens, expr_ref_vector&
         pos += pos1;
     }
     else {
-        other.push_back(e);
+        return false;
     }
+    return true;
 }
 
 bool seq_rewriter::cannot_contain_suffix(expr* a, expr* b) {
diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h
index f527aa1a3..13c93b3ca 100644
--- a/src/ast/rewriter/seq_rewriter.h
+++ b/src/ast/rewriter/seq_rewriter.h
@@ -155,7 +155,7 @@ class seq_rewriter {
     bool is_sequence(eautomaton& aut, expr_ref_vector& seq);
     bool is_epsilon(expr* e) const;
     void split_units(expr_ref_vector& lhs, expr_ref_vector& rhs);
-    void get_lengths(expr* e, expr_ref_vector& lens, expr_ref_vector& other, rational& pos);
+    bool get_lengths(expr* e, expr_ref_vector& lens, rational& pos);
 
 
 public:    
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index c005a859c..ede98c783 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -4746,6 +4746,9 @@ void theory_seq::add_itos_length_axiom(expr* len) {
     literal n_ge_100hi = mk_literal(m_autil.mk_ge(n, m_autil.mk_numeral(ten*ten*hi, true)));
     
     add_axiom(~n_ge_10hi, len_ge);
+    add_axiom(n_ge_10hi, ~len_ge);
+
+    add_axiom(n_ge_100hi, len_le);
     add_axiom(~n_ge_100hi, ~len_le);
 }