diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index 1050e4a66..45b715247 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -40,6 +40,7 @@ theory_str::theory_str(ast_manager & m):
 		opt_DisableIntegerTheoryIntegration(false),
 		opt_DeferEQCConsistencyCheck(false),
 		opt_CheckVariableScope(true),
+		opt_UseFastLengthTesterCache(true),
         /* Internal setup */
         search_started(false),
         m_autil(m),
@@ -8536,9 +8537,25 @@ expr * theory_str::gen_len_test_options(expr * freeVar, expr * indicator, int tr
 	);
 
 	for (int i = l; i < h; ++i) {
-	    std::string i_str = int_to_string(i);
-	    expr_ref str_indicator(m_strutil.mk_string(i_str), m);
-		expr_ref or_expr(ctx.mk_eq_atom(indicator, str_indicator), m); // ARGUMENT 2 IS BOGUS! WRONG SORT
+	    expr_ref str_indicator(m);
+	    if (opt_UseFastLengthTesterCache) {
+	        rational ri(i);
+	        expr * lookup_val;
+	        if(lengthTesterCache.find(ri, lookup_val)) {
+	            str_indicator = expr_ref(lookup_val, m);
+	        } else {
+	            // no match; create and insert
+	            std::string i_str = int_to_string(i);
+                expr_ref new_val(m_strutil.mk_string(i_str), m);
+                lengthTesterCache.insert(ri, new_val);
+                m_trail.push_back(new_val);
+                str_indicator = expr_ref(new_val, m);
+	        }
+	    } else {
+	        std::string i_str = int_to_string(i);
+	        expr_ref str_indicator(m_strutil.mk_string(i_str), m);
+	    }
+		expr_ref or_expr(ctx.mk_eq_atom(indicator, str_indicator), m);
 		orList.push_back(or_expr);
 
 		if (opt_AggressiveLengthTesting) {
@@ -8551,6 +8568,7 @@ expr * theory_str::gen_len_test_options(expr * freeVar, expr * indicator, int tr
 		andList.push_back(and_expr);
 	}
 
+	// TODO cache mk_string("more")
 	orList.push_back(m.mk_eq(indicator, m_strutil.mk_string("more")));
 	if (opt_AggressiveLengthTesting) {
 	    literal l = mk_eq(indicator, m_strutil.mk_string("more"), false);
diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h
index 43552f31a..9b41c583b 100644
--- a/src/smt/theory_str.h
+++ b/src/smt/theory_str.h
@@ -88,6 +88,8 @@ namespace smt {
         typedef trail_stack<theory_str> th_trail_stack;
         typedef union_find<theory_str> th_union_find;
 
+        typedef map<rational, expr*, obj_hash<rational>, default_eq<rational> > rational_map;
+
     protected:
         // Some options that control how the solver operates.
 
@@ -167,6 +169,13 @@ namespace smt {
          */
         bool opt_CheckVariableScope;
 
+        /*
+         * If UseFastLengthTesterCache is set to true,
+         * length tester terms will not be generated from scratch each time they are needed,
+         * but will be saved in a map and looked up.
+         */
+        bool opt_UseFastLengthTesterCache;
+
         bool search_started;
         arith_util m_autil;
         str_util m_strutil;
@@ -260,6 +269,9 @@ namespace smt {
 
         obj_pair_map<expr, expr, expr*> concat_astNode_map;
 
+        // used when opt_FastLengthTesterCache is true
+        rational_map lengthTesterCache;
+
         th_union_find m_find;
         th_trail_stack m_trail_stack;
         theory_var get_var(expr * n) const;