diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index a9a290ab1..4e5e45ce7 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -696,8 +696,21 @@ app * theory_str::mk_strlen(expr * e) {
         int len = strlen(strval);
         return m_autil.mk_numeral(rational(len), true);
     } else {
-        expr * args[1] = {e};
-        return get_manager().mk_app(get_id(), OP_STRLEN, 0, 0, 1, args);
+        if (false) {
+            // use cache
+            app * lenTerm = NULL;
+            if (!length_ast_map.find(e, lenTerm)) {
+                expr * args[1] = {e};
+                lenTerm = get_manager().mk_app(get_id(), OP_STRLEN, 0, 0, 1, args);
+                length_ast_map.insert(e, lenTerm);
+                m_trail.push_back(lenTerm);
+            }
+            return lenTerm;
+        } else {
+            // always regen
+            expr * args[1] = {e};
+            return get_manager().mk_app(get_id(), OP_STRLEN, 0, 0, 1, args);
+        }
     }
 }
 
diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h
index b04e21fca..48ebf049b 100644
--- a/src/smt/theory_str.h
+++ b/src/smt/theory_str.h
@@ -287,6 +287,9 @@ namespace smt {
         // used when opt_FastValueTesterCache is true
         string_map valueTesterCache;
 
+        // cache mapping each string S to Length(S)
+        obj_map<expr, app*> length_ast_map;
+
         th_union_find m_find;
         th_trail_stack m_trail_stack;
         theory_var get_var(expr * n) const;