diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index 0ee868c3a..25e12b4eb 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -653,6 +653,7 @@ br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& resu
     bool constantBase = m_util.str.is_string(a, s);
     bool constantPos = m_autil.is_numeral(b, pos);
     bool constantLen = m_autil.is_numeral(c, len);
+    bool lengthPos   = m_util.str.is_length(b) || m_autil.is_add(b);
 
     
     // case 1: pos<0 or len<=0
@@ -693,6 +694,42 @@ br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& resu
         return BR_DONE;
     }
 
+    // extract(a + b + c, len(a + b), s) -> extract(c, 0, s)
+    // extract(a + b + c, len(a) + len(b), s) -> extract(c, 0, s)
+    if (lengthPos) {
+        
+        m_lhs.reset();
+        expr_ref_vector lens(m()), other(m());
+        m_util.str.get_concat(a, m_lhs);
+        get_lengths(b, lens, other, pos);
+        unsigned rsz = lens.size();
+        unsigned i = 0;
+        for (; i < rsz; ++i) {
+            expr* lhs = m_lhs.get(i);
+            if (lens.contains(lhs)) {
+                lens.erase(lhs);
+            }
+            else if (m_util.str.is_unit(lhs) && pos.is_pos()) {
+                pos -= rational(1);
+            }
+            else {
+                break;
+            }
+        }
+        if (i == 0) return BR_FAILED;
+        expr_ref t1(m()), t2(m());
+        t1 = m_util.str.mk_concat(m_lhs.size() - i, m_lhs.c_ptr() + i);
+        t2 = m_autil.mk_int(pos);
+        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, m_util.str.mk_length(rhs));
+        }
+        result = m_util.str.mk_substr(t1, t2, c);
+        return BR_REWRITE2;
+    }
+
     if (!constantPos) {
         return BR_FAILED;
     }
@@ -740,6 +777,25 @@ 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) {
+    expr* arg = nullptr;
+    rational pos1;
+    if (m_autil.is_add(e)) {
+        for (expr* arg1 : *to_app(e)) {
+            get_lengths(arg1, lens, other, pos);
+        }
+    }
+    else if (m_util.str.is_length(e, arg)) {
+        lens.push_back(arg);
+    }
+    else if (m_autil.is_numeral(e, pos1)) {
+        pos += pos1;
+    }
+    else {
+        other.push_back(e);
+    }
+}
+
 bool seq_rewriter::cannot_contain_suffix(expr* a, expr* b) {
     
     if (m_util.str.is_unit(a) && m_util.str.is_unit(b) && m().are_distinct(a, b)) {
diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h
index 0cfb8639e..f527aa1a3 100644
--- a/src/ast/rewriter/seq_rewriter.h
+++ b/src/ast/rewriter/seq_rewriter.h
@@ -155,6 +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);
 
 
 public: