diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index 5f024dead..c7cbff04e 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -41,6 +41,7 @@ theory_str::theory_str(ast_manager & m):
 		opt_DeferEQCConsistencyCheck(false),
 		opt_CheckVariableScope(true),
 		opt_UseFastLengthTesterCache(true),
+		opt_UseFastValueTesterCache(true),
         /* Internal setup */
         search_started(false),
         m_autil(m),
@@ -7967,6 +7968,7 @@ expr * theory_str::gen_val_options(expr * freeVar, expr * len_indicator, expr *
 	ptr_vector<expr> andList;
 
 	for (long long i = l; i < h; i++) {
+		// TODO can we share the val_indicator constants with the length tester cache?
 		orList.push_back(m.mk_eq(val_indicator, m_strutil.mk_string(longlong_to_string(i).c_str()) ));
 		if (opt_AggressiveValueTesting) {
 		    literal l = mk_eq(val_indicator, m_strutil.mk_string(longlong_to_string(i).c_str()), false);
@@ -7975,7 +7977,16 @@ expr * theory_str::gen_val_options(expr * freeVar, expr * len_indicator, expr *
 		}
 
 		std::string aStr = gen_val_string(len, options[i - l]);
-		expr * strAst = m_strutil.mk_string(aStr);
+		expr * strAst;
+		if (opt_UseFastValueTesterCache) {
+			if (!valueTesterCache.find(aStr, strAst)) {
+				strAst = m_strutil.mk_string(aStr);
+				valueTesterCache.insert(aStr, strAst);
+				m_trail.push_back(strAst);
+			}
+		} else {
+			strAst = m_strutil.mk_string(aStr);
+		}
 		andList.push_back(m.mk_eq(orList[orList.size() - 1], m.mk_eq(freeVar, strAst)));
 	}
 	if (!coverAll) {
diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h
index 9b41c583b..b04e21fca 100644
--- a/src/smt/theory_str.h
+++ b/src/smt/theory_str.h
@@ -89,6 +89,12 @@ namespace smt {
         typedef union_find<theory_str> th_union_find;
 
         typedef map<rational, expr*, obj_hash<rational>, default_eq<rational> > rational_map;
+        struct str_hash_proc {
+            unsigned operator()(std::string const & s) const {
+            	return string_hash(s.c_str(), static_cast<unsigned>(s.length()), 17);
+            }
+        };
+        typedef map<std::string, expr*, str_hash_proc, default_eq<std::string> > string_map;
 
     protected:
         // Some options that control how the solver operates.
@@ -176,6 +182,13 @@ namespace smt {
          */
         bool opt_UseFastLengthTesterCache;
 
+        /*
+         * If UseFastValueTesterCache is set to true,
+         * value 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_UseFastValueTesterCache;
+
         bool search_started;
         arith_util m_autil;
         str_util m_strutil;
@@ -271,6 +284,8 @@ namespace smt {
 
         // used when opt_FastLengthTesterCache is true
         rational_map lengthTesterCache;
+        // used when opt_FastValueTesterCache is true
+        string_map valueTesterCache;
 
         th_union_find m_find;
         th_trail_stack m_trail_stack;