diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp
index 6ac7393eead..b994d73b16c 100644
--- a/src/solvers/refinement/string_refinement.cpp
+++ b/src/solvers/refinement/string_refinement.cpp
@@ -757,6 +757,7 @@ decision_proceduret::resultt string_refinementt::dec_solve()
 
   // Initial try without index set
   const auto get = [this](const exprt &expr) { return this->get(expr); };
+  dependencies.clean_cache();
   const decision_proceduret::resultt res=supert::dec_solve();
   if(res==resultt::D_SATISFIABLE)
   {
@@ -804,6 +805,7 @@ decision_proceduret::resultt string_refinementt::dec_solve()
 
   while((loop_bound_--)>0)
   {
+    dependencies.clean_cache();
     const decision_proceduret::resultt res=supert::dec_solve();
 
     if(res==resultt::D_SATISFIABLE)
diff --git a/src/solvers/refinement/string_refinement_util.cpp b/src/solvers/refinement/string_refinement_util.cpp
index e55e3292a8d..6cea38e4c19 100644
--- a/src/solvers/refinement/string_refinement_util.cpp
+++ b/src/solvers/refinement/string_refinement_util.cpp
@@ -537,17 +537,36 @@ optionalt<exprt> string_dependenciest::eval(
   const array_string_exprt &s,
   const std::function<exprt(const exprt &)> &get_value) const
 {
-  const auto node = node_at(s);
-  if(node && node->dependencies.size() == 1)
+  const auto &it = node_index_pool.find(s);
+  if(it == node_index_pool.end())
+    return {};
+
+  if(eval_string_cache[it->second])
+    return eval_string_cache[it->second];
+
+  const auto node = string_nodes[it->second];
+
+  if(node.dependencies.size() == 1)
   {
-    const auto &f = get_builtin_function(node->dependencies[0]);
+    const auto &f = get_builtin_function(node.dependencies[0]);
     const auto result = f.string_result();
     if(result && *result == s)
-      return f.eval(get_value);
+    {
+      const auto value_opt = f.eval(get_value);
+      eval_string_cache[it->second] = value_opt;
+      return value_opt;
+    }
   }
   return {};
 }
 
+void string_dependenciest::clean_cache()
+{
+  eval_string_cache.resize(string_nodes.size());
+  for(auto &e : eval_string_cache)
+    e.reset();
+}
+
 bool add_node(
   string_dependenciest &dependencies,
   const equal_exprt &equation,
diff --git a/src/solvers/refinement/string_refinement_util.h b/src/solvers/refinement/string_refinement_util.h
index d23c03fb690..e8c18ad3cf6 100644
--- a/src/solvers/refinement/string_refinement_util.h
+++ b/src/solvers/refinement/string_refinement_util.h
@@ -339,10 +339,15 @@ class string_dependenciest
 
   /// Attempt to evaluate the given string from the dependencies and valuation
   /// of strings on which it depends
+  /// Warning: eval uses a cache which must be cleaned everytime the valuations
+  /// given by get_value can change.
   optionalt<exprt> eval(
     const array_string_exprt &s,
     const std::function<exprt(const exprt &)> &get_value) const;
 
+  /// Clean the cache used by `eval`
+  void clean_cache();
+
   void output_dot(std::ostream &stream) const;
 
 private:
@@ -352,6 +357,8 @@ class string_dependenciest
   /// Set of nodes representing strings
   std::vector<string_nodet> string_nodes;
 
+  mutable std::vector<optionalt<exprt>> eval_string_cache;
+
   /// Nodes describing dependencies of a string: values of the map correspond
   /// to indexes in the vector `string_nodes`.
   std::unordered_map<array_string_exprt, std::size_t, irep_hash>