diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index e5e0c9cb0..2d05ee9aa 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -2783,30 +2783,29 @@ bool theory_seq::get_length(expr* e, rational& val) {
             todo.push_back(e1);
             todo.push_back(e2);
         }
-        else if (m_util.str.is_unit(c)) {
+        else if (m_util.str.is_unit(c)) 
             val += rational(1);
-        }
-        else if (m_util.str.is_empty(c)) {
+        else if (m_util.str.is_empty(c)) 
             continue;
-        }
-        else if (m_util.str.is_string(c, s)) {
+        else if (m_util.str.is_map(c, e1, e2)) 
+            todo.push_back(e2);
+        else if (m_util.str.is_mapi(c, e1, e2, c)) 
+            todo.push_back(c);
+        else if (m_util.str.is_string(c, s)) 
             val += rational(s.length());
-        }
-        else if (!has_length(c)) {
-            len = mk_len(c);
+        else
+            continue;
+        len = mk_len(c);
+        if (!has_length(c)) {
             add_axiom(mk_literal(m_autil.mk_ge(len, m_autil.mk_int(0))));
             TRACE("seq", tout << "literal has no length " << mk_pp(c, m) << "\n";);
             return false;            
         }
-        else {            
-            len = mk_len(c);
-            if (m_arith_value.get_value(len, val1) && !val1.is_neg()) {
-                val += val1;                
-            }
-            else {
-                TRACE("seq", tout << "length has not been internalized " << mk_pp(c, m) << "\n";);
-                return false;
-            }
+        else if (m_arith_value.get_value(len, val1) && !val1.is_neg()) 
+            val += val1;                
+        else {
+            TRACE("seq", tout << "length has not been internalized " << mk_pp(c, m) << "\n";);
+            return false;
         }
     }
     CTRACE("seq", !val.is_int(), tout << "length is not an integer\n";);