diff --git a/regression/jbmc-strings/StringConcat/Test.class b/regression/jbmc-strings/StringConcat/Test.class
new file mode 100644
index 00000000000..7600fbe19d0
Binary files /dev/null and b/regression/jbmc-strings/StringConcat/Test.class differ
diff --git a/regression/jbmc-strings/StringConcat/Test.java b/regression/jbmc-strings/StringConcat/Test.java
new file mode 100644
index 00000000000..74f91b81df0
--- /dev/null
+++ b/regression/jbmc-strings/StringConcat/Test.java
@@ -0,0 +1,315 @@
+public class Test {
+
+    public String stringDet() {
+        String s = "a";
+        s += "b";
+        s += "c";
+        s += "d";
+        s += "e";
+        s += "f";
+        s += "g";
+        s += "h";
+        s += "i";
+        s += "j";
+        s += "k";
+        s += "l";
+        s += "m";
+
+        assert(false);
+        return s;
+    }
+
+    public String stringNonDet(String arg) {
+        String s = arg;
+        s += "b";
+        s += "c";
+        s += "d";
+        s += "e";
+        s += "f";
+        s += arg;
+        s += "h";
+        s += "i";
+        s += "j";
+        s += "k";
+        s += "l";
+        s += arg;
+
+        assert(false);
+        return s;
+    }
+
+    public String bufferDet() {
+        StringBuffer s = new StringBuffer();
+        s.append("a");
+        s.append("b");
+        s.append("c");
+        s.append("d");
+        s.append("e");
+
+        s.append("a");
+        s.append("b");
+        s.append("c");
+        s.append("d");
+        s.append("e");
+
+        s.append("a");
+        s.append("b");
+        s.append("c");
+        s.append("d");
+        s.append("e");
+
+        s.append("a");
+        s.append("b");
+        s.append("c");
+        s.append("d");
+        s.append("e");
+
+        s.append("a");
+        s.append("b");
+        s.append("c");
+        s.append("d");
+        s.append("e");
+
+        s.append("a");
+        s.append("b");
+        assert(false);
+        return s.toString();
+    }
+
+    public String charBufferDet() {
+        StringBuffer s = new StringBuffer();
+        s.append('a');
+        s.append('b');
+        s.append('c');
+        s.append('d');
+        s.append('e');
+
+        s.append('a');
+        s.append('b');
+        s.append('c');
+        s.append('d');
+        s.append('e');
+
+        s.append('a');
+        s.append('b');
+        s.append('c');
+        s.append('d');
+        s.append('e');
+
+        s.append('a');
+        s.append('b');
+        s.append('c');
+        s.append('d');
+        s.append('e');
+
+        s.append('a');
+        s.append('b');
+        s.append('c');
+        s.append('d');
+        s.append('e');
+
+        s.append('a');
+        s.append('b');
+
+        assert(false);
+        return s.toString();
+    }
+
+    public String charBufferDetLoop(int width) {
+        if(width <= 5)
+            return "";
+        StringBuffer sb = new StringBuffer();
+        sb.append('+');
+        for(int i=1; i < width-1; ++i)
+            sb.append('-');
+        sb.append('+');
+        sb.append('\n');
+        sb.append('|');
+
+        sb.append(' ');
+        sb.append('c');
+        int padding = width - 2;
+        while(padding-- > 0)
+            sb.append(' ');
+
+        sb.append(' ');
+        sb.append('|');
+        sb.append('\n');
+        assert(false);
+        return sb.toString();
+    }
+
+    public String charBufferDetLoop2(int width, int height) {
+        if(width <= 0 || height <= 0)
+            return "";
+        StringBuffer sb = new StringBuffer();
+        sb.append('+');
+        for(int i=1; i < width-1; ++i)
+            sb.append('-');
+        sb.append('+');
+        sb.append('\n');
+        sb.append('|');
+
+        sb.append(' ');
+        sb.append('c');
+        int padding = width - 2;
+        while(padding-- > 0)
+            sb.append(' ');
+        sb.append(' ');
+        sb.append('|');
+        sb.append('\n');
+
+        sb.append('+');
+        for(int i=1; i<width; ++i)
+            sb.append('-');
+        sb.append('+');
+        sb.append('\n');
+
+        for(int i = 0; i < height; ++i) {
+            sb.append('|');
+            sb.append(' ');
+            sb.append('d');
+            padding = width - 3;
+            while(padding-- > 0)
+                sb.append(' ');
+            sb.append(' ');
+            sb.append('|');
+            sb.append('\n');
+        }
+
+        sb.append('+');
+        for(int i=1; i<width-1; ++i)
+            sb.append('-');
+        sb.append('+');
+        sb.append('\n');
+
+        assert(false);
+        return sb.toString();
+    }
+
+    public String bufferNonDetLoop(int width, String s) {
+        if(width <= 5 || s.length() >= width || s.length() == 0)
+            return "";
+        StringBuffer sb = new StringBuffer();
+        sb.append('+');
+        for(int i=1; i < width-1; ++i)
+            sb.append('-');
+        sb.append('+');
+        sb.append('\n');
+        sb.append('|');
+
+        sb.append(' ');
+        sb.append(s);
+        int padding = width - s.length();
+        while(padding-- > 0)
+            sb.append(' ');
+        sb.append(' ');
+        sb.append('|');
+        sb.append('\n');
+
+        assert(false);
+        return sb.toString();
+    }
+
+    public String bufferNonDetLoop2(int width, String c) {
+        if(width < 5 || c.length() > width)
+            return "";
+
+        StringBuffer sb = new StringBuffer();
+        sb.append('+');
+
+        for(int i=1; i<width-1; ++i)
+            sb.append('-');
+        sb.append('+');
+        sb.append('\n');
+        sb.append('|');
+        for(int i = 0; i < width; ++i) {
+            sb.append(' ');
+            sb.append(c);
+            int padding = width - c.length();
+            while(padding-- > 0)
+                sb.append(' ');
+            sb.append(' ');
+            sb.append('|');
+        }
+        sb.append('\n');
+
+        assert(false);
+        return sb.toString();
+    }
+
+    public String bufferNonDetLoop3(int cols, int columnWidth, String c) {
+        StringBuffer sb = new StringBuffer();
+        sb.append('-');
+        for(int i = 0; i < cols; ++i)
+            sb.append(c);
+
+        assert(false);
+        return sb.toString();
+    }
+    public String bufferNonDetLoop4(int cols, int columnWidth, String c) {
+        StringBuffer sb = new StringBuffer();
+        for(int i=1; i < columnWidth-1; ++i)
+            sb.append('-');
+        for(int i = 0; i < cols; ++i) {
+            sb.append(c);
+        }
+
+        assert(false);
+        return sb.toString();
+    }
+
+    public String bufferNonDetLoop5(int cols, int columnWidth, String c, String data[]) {
+        if(cols<1)
+            return "";
+
+        StringBuffer sb = new StringBuffer();
+        sb.append('+');
+        int totalWidth = columnWidth * cols;
+        for(int i=1; i<totalWidth-1; ++i)
+            sb.append('-');
+        sb.append('+');
+        sb.append('\n');
+        sb.append('|');
+        for(int i = 0; i < cols; ++i) {
+            sb.append(' ');
+            sb.append(c);
+            int padding = columnWidth - c.length();
+            while(padding-- > 0)
+                sb.append(' ');
+            sb.append(' ');
+            sb.append('|');
+        }
+        sb.append('\n');
+
+        sb.append('+');
+        for(int i=1; i<totalWidth-1; ++i)
+            sb.append('-');
+        sb.append('+');
+        sb.append('\n');
+
+        for(int i = 0; i < data.length; ++i) {
+            sb.append('|');
+            String d = data[i];
+            sb.append(' ');
+            sb.append(d);
+            int padding = columnWidth - d.length();
+            while(padding-- > 0)
+                sb.append(' ');
+            sb.append(' ');
+            sb.append('|');
+
+            if(i % cols == 0)
+                sb.append('\n');
+        }
+
+        sb.append('+');
+        for(int i=1; i<totalWidth-1; ++i)
+            sb.append('-');
+        sb.append('+');
+        sb.append('\n');
+
+        assert(false);
+        return sb.toString();
+    }
+}
diff --git a/regression/jbmc-strings/StringConcat/test_buffer_det.desc b/regression/jbmc-strings/StringConcat/test_buffer_det.desc
new file mode 100644
index 00000000000..5e66ea01921
--- /dev/null
+++ b/regression/jbmc-strings/StringConcat/test_buffer_det.desc
@@ -0,0 +1,11 @@
+CORE
+Test.class
+--refine-strings --string-max-length 1000 --string-max-input-length 100 --function Test.bufferDet --depth 10000  --verbosity 10
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+check_SAT: got SAT but the model is not correct
+--
+Using the string dependences information to compute the model, refinement
+should not be needed when the execution is deterministic.
diff --git a/regression/jbmc-strings/StringConcat/test_buffer_nondet_loop.desc b/regression/jbmc-strings/StringConcat/test_buffer_nondet_loop.desc
new file mode 100644
index 00000000000..85e22913994
--- /dev/null
+++ b/regression/jbmc-strings/StringConcat/test_buffer_nondet_loop.desc
@@ -0,0 +1,14 @@
+FUTURE
+Test.class
+--refine-strings --string-max-length 1000 --string-max-input-length 100 --function Test.bufferNonDetLoop --depth 10000 --unwind 5  --verbosity 10  --property "java::Test.bufferNonDetLoop:(ILjava/lang/String;)Ljava/lang/String;.assertion.1"
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+check_SAT: got SAT but the model is not correct
+--
+Using the string dependences information to compute the model, refinement
+should not be needed when the execution is deterministic.
+
+This test seems to fail with AppVeyor, we should make sure it works
+once TG-2608 is done.
diff --git a/regression/jbmc-strings/StringConcat/test_buffer_nondet_loop2.desc b/regression/jbmc-strings/StringConcat/test_buffer_nondet_loop2.desc
new file mode 100644
index 00000000000..8f2983e4c34
--- /dev/null
+++ b/regression/jbmc-strings/StringConcat/test_buffer_nondet_loop2.desc
@@ -0,0 +1,11 @@
+FUTURE
+Test.class
+--refine-strings --string-max-length 1000 --string-max-input-length 100 --function Test.bufferNonDetLoop2 --depth 10000 --unwind 5  --verbosity 10
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+check_SAT: got SAT but the model is not correct
+--
+Using the string dependences information to compute the model, refinement
+should not be needed when the execution is deterministic.
diff --git a/regression/jbmc-strings/StringConcat/test_buffer_nondet_loop3.desc b/regression/jbmc-strings/StringConcat/test_buffer_nondet_loop3.desc
new file mode 100644
index 00000000000..ac8124eb0b1
--- /dev/null
+++ b/regression/jbmc-strings/StringConcat/test_buffer_nondet_loop3.desc
@@ -0,0 +1,11 @@
+CORE
+Test.class
+--refine-strings --string-max-length 1000 --string-max-input-length 100 --function Test.bufferNonDetLoop3 --depth 10000 --unwind 5  --verbosity 10
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+check_SAT: got SAT but the model is not correct
+--
+Using the string dependences information to compute the model, refinement
+should not be needed when the execution is deterministic.
diff --git a/regression/jbmc-strings/StringConcat/test_buffer_nondet_loop4.desc b/regression/jbmc-strings/StringConcat/test_buffer_nondet_loop4.desc
new file mode 100644
index 00000000000..6d2ad2eac22
--- /dev/null
+++ b/regression/jbmc-strings/StringConcat/test_buffer_nondet_loop4.desc
@@ -0,0 +1,14 @@
+FUTURE
+Test.class
+--refine-strings --string-max-length 1000 --string-max-input-length 100 --function Test.bufferNonDetLoop4 --depth 10000 --unwind 5  --verbosity 10 --property "java::Test.bufferNonDetLoop4:(IILjava/lang/String;)Ljava/lang/String;.assertion.1"
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+check_SAT: got SAT but the model is not correct
+--
+Using the string dependences information to compute the model, refinement
+should not be needed when the execution is deterministic.
+
+This test seems to fail with AppVeyor, we should make sure it works
+once TG-2608 is done.
diff --git a/regression/jbmc-strings/StringConcat/test_buffer_nondet_loop5.desc b/regression/jbmc-strings/StringConcat/test_buffer_nondet_loop5.desc
new file mode 100644
index 00000000000..87c043ab693
--- /dev/null
+++ b/regression/jbmc-strings/StringConcat/test_buffer_nondet_loop5.desc
@@ -0,0 +1,11 @@
+FUTURE
+Test.class
+--refine-strings --string-max-length 1000 --string-max-input-length 100 --function Test.bufferNonDetLoop5 --depth 10000 --unwind 5  --verbosity 10
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+check_SAT: got SAT but the model is not correct
+--
+Using the string dependences information to compute the model, refinement
+should not be needed when the execution is deterministic.
diff --git a/regression/jbmc-strings/StringConcat/test_char_buffer_det.desc b/regression/jbmc-strings/StringConcat/test_char_buffer_det.desc
new file mode 100644
index 00000000000..8821fadda98
--- /dev/null
+++ b/regression/jbmc-strings/StringConcat/test_char_buffer_det.desc
@@ -0,0 +1,11 @@
+CORE
+Test.class
+--refine-strings --string-max-length 1000 --string-max-input-length 100 --function Test.charBufferDet --depth 10000  --verbosity 10
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+check_SAT: got SAT but the model is not correct
+--
+Using the string dependences information to compute the model, refinement
+should not be needed when the execution is deterministic.
diff --git a/regression/jbmc-strings/StringConcat/test_char_buffer_det_loop.desc b/regression/jbmc-strings/StringConcat/test_char_buffer_det_loop.desc
new file mode 100644
index 00000000000..9c3643b0770
--- /dev/null
+++ b/regression/jbmc-strings/StringConcat/test_char_buffer_det_loop.desc
@@ -0,0 +1,11 @@
+CORE
+Test.class
+--refine-strings --string-max-length 1000 --string-max-input-length 100 --function Test.charBufferDetLoop --depth 10000 --unwind 5  --verbosity 10
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+check_SAT: got SAT but the model is not correct
+--
+Using the string dependences information to compute the model, refinement
+should not be needed when the execution is deterministic.
diff --git a/regression/jbmc-strings/StringConcat/test_char_buffer_det_loop2.desc b/regression/jbmc-strings/StringConcat/test_char_buffer_det_loop2.desc
new file mode 100644
index 00000000000..eee09bad0eb
--- /dev/null
+++ b/regression/jbmc-strings/StringConcat/test_char_buffer_det_loop2.desc
@@ -0,0 +1,11 @@
+CORE
+Test.class
+--refine-strings --string-max-length 1000 --string-max-input-length 100 --function Test.charBufferDetLoop2 --depth 10000 --unwind 5  --verbosity 10
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+check_SAT: got SAT but the model is not correct
+--
+Using the string dependences information to compute the model, refinement
+should not be needed when the execution is deterministic.
diff --git a/regression/jbmc-strings/StringConcat/test_string_det.desc b/regression/jbmc-strings/StringConcat/test_string_det.desc
new file mode 100644
index 00000000000..d3a8f79fdc1
--- /dev/null
+++ b/regression/jbmc-strings/StringConcat/test_string_det.desc
@@ -0,0 +1,11 @@
+CORE
+Test.class
+--refine-strings --string-max-length 1000 --string-max-input-length 100 --function Test.stringDet --depth 10000  --verbosity 10
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+check_SAT: got SAT but the model is not correct
+--
+Using the string dependences information to compute the model, refinement
+should not be needed when the execution is deterministic.
diff --git a/regression/jbmc-strings/StringConcat/test_string_nondet.desc b/regression/jbmc-strings/StringConcat/test_string_nondet.desc
new file mode 100644
index 00000000000..14f7c8ae8d0
--- /dev/null
+++ b/regression/jbmc-strings/StringConcat/test_string_nondet.desc
@@ -0,0 +1,11 @@
+FUTURE
+Test.class
+--refine-strings --string-max-length 1000 --string-max-input-length 100 --function Test.stringNonDet --depth 10000 --unwind 5 --verbosity 10
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+check_SAT: got SAT but the model is not correct
+--
+Using the string dependences information to compute the model, refinement
+should not be needed when the execution is deterministic.
diff --git a/src/solvers/refinement/string_constraint.h b/src/solvers/refinement/string_constraint.h
index 7e804ec6e13..55aacd7f4d5 100644
--- a/src/solvers/refinement/string_constraint.h
+++ b/src/solvers/refinement/string_constraint.h
@@ -54,7 +54,7 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com
 ///      \f$f\f$ [explicitly stated, implied].
 ///
 /// \todo The fact that we follow this grammar is not enforced at the moment.
-class string_constraintt: public exprt
+class string_constraintt : public exprt
 {
 public:
   // String constraints are of the form
@@ -148,9 +148,7 @@ extern inline string_constraintt &to_string_constraint(exprt &expr)
 /// \param [in] identifier: identifier for `from_expr`
 /// \param [in] expr: constraint to render
 /// \return rendered string
-inline std::string from_expr(
-  const irep_idt &identifier,
-  const string_constraintt &expr)
+inline std::string to_string(const string_constraintt &expr)
 {
   std::ostringstream out;
   out << "forall " << format(expr.univ_var()) << " in ["
@@ -160,7 +158,7 @@ inline std::string from_expr(
 }
 
 /// Constraints to encode non containement of strings.
-class string_not_contains_constraintt: public exprt
+class string_not_contains_constraintt : public exprt
 {
 public:
   // string_not contains_constraintt are formula of the form:
@@ -222,9 +220,7 @@ class string_not_contains_constraintt: public exprt
 /// \param [in] identifier: identifier for `from_expr`
 /// \param [in] expr: constraint to render
 /// \return rendered string
-inline std::string from_expr(
-  const irep_idt &identifier,
-  const string_not_contains_constraintt &expr)
+inline std::string to_string(const string_not_contains_constraintt &expr)
 {
   std::ostringstream out;
   out << "forall x in [" << format(expr.univ_lower_bound()) << ", "
diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp
index 95df34885cc..b994d73b16c 100644
--- a/src/solvers/refinement/string_refinement.cpp
+++ b/src/solvers/refinement/string_refinement.cpp
@@ -679,13 +679,14 @@ decision_proceduret::resultt string_refinementt::dec_solve()
 
 #ifdef DEBUG
   output_equations(debug(), equations, ns);
+#endif
 
-  string_dependencest dependences;
+  debug() << "dec_solve: compute dependency graph:" << eom;
   for(const equal_exprt &eq : equations)
-    add_node(dependences, eq, generator.array_pool);
+    add_node(dependencies, eq, generator.array_pool);
 
-  debug() << "dec_solve: dependence graph:" << eom;
-  dependences.output_dot(debug());
+#ifdef DEBUG
+  dependencies.output_dot(debug());
 #endif
 
   debug() << "dec_solve: Replace function applications" << eom;
@@ -756,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)
   {
@@ -803,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)
@@ -1475,17 +1478,17 @@ static void debug_check_axioms_step(
   stream << indent2 << "- axiom:\n" << indent2 << indent;
 
   if(axiom.id() == ID_string_constraint)
-    stream << format(to_string_constraint(axiom));
+    stream << to_string(to_string_constraint(axiom));
   else if(axiom.id() == ID_string_not_contains_constraint)
-    stream << format(to_string_not_contains_constraint(axiom));
+    stream << to_string(to_string_not_contains_constraint(axiom));
   else
     stream << format(axiom);
   stream << '\n' << indent2 << "- axiom_in_model:\n" << indent2 << indent;
 
   if(axiom_in_model.id() == ID_string_constraint)
-    stream << format(to_string_constraint(axiom_in_model));
+    stream << to_string(to_string_constraint(axiom_in_model));
   else if(axiom_in_model.id() == ID_string_not_contains_constraint)
-    stream << format(to_string_not_contains_constraint(axiom_in_model));
+    stream << to_string(to_string_not_contains_constraint(axiom_in_model));
   else
     stream << format(axiom_in_model);
 
@@ -1862,7 +1865,7 @@ static exprt compute_inverse_function(
   return sum_over_map(elems, f.type(), neg);
 }
 
-class find_qvar_visitort: public const_expr_visitort
+class find_qvar_visitort : public const_expr_visitort
 {
 private:
   const exprt &qvar_;
@@ -2253,6 +2256,12 @@ exprt string_refinementt::get(const exprt &expr) const
   {
     array_string_exprt &arr = to_array_string_expr(ecopy);
     arr.length() = generator.array_pool.get_length(arr);
+
+    if(
+      const auto from_dependencies =
+        dependencies.eval(arr, [&](const exprt &expr) { return get(expr); }))
+      return *from_dependencies;
+
     const auto arr_model_opt =
       get_array(super_get, ns, generator.max_string_length, debug(), arr);
     // \todo Refactor with get array in model
diff --git a/src/solvers/refinement/string_refinement.h b/src/solvers/refinement/string_refinement.h
index 7ee95f8d3a6..281f004da87 100644
--- a/src/solvers/refinement/string_refinement.h
+++ b/src/solvers/refinement/string_refinement.h
@@ -44,10 +44,11 @@ class string_refinementt final: public bv_refinementt
   };
 public:
   /// string_refinementt constructor arguments
-  struct infot:
-    public bv_refinementt::infot,
-    public string_constraint_generatort::infot,
-    public configt { };
+  struct infot : public bv_refinementt::infot,
+                 public string_constraint_generatort::infot,
+                 public configt
+  {
+  };
 
   explicit string_refinementt(const infot &);
 
@@ -84,6 +85,8 @@ class string_refinementt final: public bv_refinementt
 
   std::vector<equal_exprt> equations;
 
+  string_dependenciest dependencies;
+
   void add_lemma(const exprt &lemma, bool simplify_lemma = true);
 };
 
diff --git a/src/solvers/refinement/string_refinement_util.cpp b/src/solvers/refinement/string_refinement_util.cpp
index 06c71623ec1..236847659a0 100644
--- a/src/solvers/refinement/string_refinement_util.cpp
+++ b/src/solvers/refinement/string_refinement_util.cpp
@@ -16,8 +16,19 @@
 #include <util/expr_iterator.h>
 #include <util/graph.h>
 #include <util/magic.h>
+#include <util/make_unique.h>
 #include "string_refinement_util.h"
 
+/// Get the valuation of the string, given a valuation
+static optionalt<std::vector<mp_integer>> eval_string(
+  const array_string_exprt &a,
+  const std::function<exprt(const exprt &)> &get_value);
+
+/// Make a string from a constant array
+static array_string_exprt make_string(
+  const std::vector<mp_integer> &array,
+  const array_typet &array_type);
+
 bool is_char_type(const typet &type)
 {
   return type.id() == ID_unsignedbv &&
@@ -162,11 +173,63 @@ equation_symbol_mappingt::find_equations(const exprt &expr)
   return equations_containing[expr];
 }
 
+string_transformation_builtin_functiont::
+  string_transformation_builtin_functiont(
+    const std::vector<exprt> &fun_args,
+    array_poolt &array_pool)
+{
+  PRECONDITION(fun_args.size() > 2);
+  const auto arg1 = expr_checked_cast<struct_exprt>(fun_args[2]);
+  input = array_pool.find(arg1.op1(), arg1.op0());
+  result = array_pool.find(fun_args[1], fun_args[0]);
+  args.insert(args.end(), fun_args.begin() + 3, fun_args.end());
+}
+
+optionalt<exprt> string_transformation_builtin_functiont::eval(
+  const std::function<exprt(const exprt &)> &get_value) const
+{
+  const auto &input_value = eval_string(input, get_value);
+  if(!input_value.has_value())
+    return {};
+
+  std::vector<mp_integer> arg_values;
+  const auto &insert = std::back_inserter(arg_values);
+  const mp_integer unknown('?');
+  std::transform(
+    args.begin(), args.end(), insert, [&](const exprt &e) { // NOLINT
+      if(const auto val = numeric_cast<mp_integer>(get_value(e)))
+        return *val;
+      INVARIANT(
+        get_value(e).id() == ID_unknown,
+        "array valuation should only contain constants and unknown");
+      return unknown;
+    });
+
+  const auto result_value = eval(*input_value, arg_values);
+  const auto length = from_integer(result_value.size(), result.length().type());
+  const array_typet type(result.type().subtype(), length);
+  return make_string(result_value, type);
+}
+
 string_insertion_builtin_functiont::string_insertion_builtin_functiont(
   const std::vector<exprt> &fun_args,
   array_poolt &array_pool)
 {
-  PRECONDITION(fun_args.size() > 3);
+  PRECONDITION(fun_args.size() > 4);
+  const auto arg1 = expr_checked_cast<struct_exprt>(fun_args[2]);
+  input1 = array_pool.find(arg1.op1(), arg1.op0());
+  const auto arg2 = expr_checked_cast<struct_exprt>(fun_args[4]);
+  input2 = array_pool.find(arg2.op1(), arg2.op0());
+  result = array_pool.find(fun_args[1], fun_args[0]);
+  args.push_back(fun_args[3]);
+  args.insert(args.end(), fun_args.begin() + 5, fun_args.end());
+}
+
+string_concatenation_builtin_functiont::string_concatenation_builtin_functiont(
+  const std::vector<exprt> &fun_args,
+  array_poolt &array_pool)
+{
+  PRECONDITION(fun_args.size() >= 4 && fun_args.size() <= 6);
   const auto arg1 = expr_checked_cast<struct_exprt>(fun_args[2]);
   input1 = array_pool.find(arg1.op1(), arg1.op0());
   const auto arg2 = expr_checked_cast<struct_exprt>(fun_args[3]);
@@ -175,6 +238,129 @@ string_insertion_builtin_functiont::string_insertion_builtin_functiont(
   args.insert(args.end(), fun_args.begin() + 4, fun_args.end());
 }
 
+optionalt<std::vector<mp_integer>> eval_string(
+  const array_string_exprt &a,
+  const std::function<exprt(const exprt &)> &get_value)
+{
+  if(a.id() == ID_if)
+  {
+    const if_exprt &ite = to_if_expr(a);
+    const exprt cond = get_value(ite.cond());
+    if(!cond.is_constant())
+      return {};
+    return cond.is_true()
+             ? eval_string(to_array_string_expr(ite.true_case()), get_value)
+             : eval_string(to_array_string_expr(ite.false_case()), get_value);
+  }
+
+  const auto size = numeric_cast<std::size_t>(get_value(a.length()));
+  const exprt content = get_value(a.content());
+  const auto &array = expr_try_dynamic_cast<array_exprt>(content);
+  if(!size || !array)
+    return {};
+
+  const auto &ops = array->operands();
+  INVARIANT(*size == ops.size(), "operands size should match string size");
+
+  std::vector<mp_integer> result;
+  const mp_integer unknown('?');
+  const auto &insert = std::back_inserter(result);
+  std::transform(
+    ops.begin(), ops.end(), insert, [unknown](const exprt &e) { // NOLINT
+      if(const auto i = numeric_cast<mp_integer>(e))
+        return *i;
+      return unknown;
+    });
+  return result;
+}
+
+array_string_exprt
+make_string(const std::vector<mp_integer> &array, const array_typet &array_type)
+{
+  const typet &char_type = array_type.subtype();
+  array_exprt array_expr(array_type);
+  const auto &insert = std::back_inserter(array_expr.operands());
+  std::transform(
+    array.begin(), array.end(), insert, [&](const mp_integer &i) { // NOLINT
+      return from_integer(i, char_type);
+    });
+  return to_array_string_expr(array_expr);
+}
+
+std::vector<mp_integer> string_concatenation_builtin_functiont::eval(
+  const std::vector<mp_integer> &input1_value,
+  const std::vector<mp_integer> &input2_value,
+  const std::vector<mp_integer> &args_value) const
+{
+  const std::size_t start_index =
+    args_value.size() > 0 && args_value[0] > 0 ? args_value[0].to_ulong() : 0;
+  const std::size_t end_index = args_value.size() > 1 && args_value[1] > 0
+                                  ? args_value[1].to_ulong()
+                                  : input2_value.size();
+
+  std::vector<mp_integer> result(input1_value);
+  result.insert(
+    result.end(),
+    input2_value.begin() + start_index,
+    input2_value.begin() + end_index);
+  return result;
+}
+
+std::vector<mp_integer> string_concat_char_builtin_functiont::eval(
+  const std::vector<mp_integer> &input_value,
+  const std::vector<mp_integer> &args_value) const
+{
+  PRECONDITION(args_value.size() == 1);
+  std::vector<mp_integer> result(input_value);
+  result.push_back(args_value[0]);
+  return result;
+}
+
+std::vector<mp_integer> string_insertion_builtin_functiont::eval(
+  const std::vector<mp_integer> &input1_value,
+  const std::vector<mp_integer> &input2_value,
+  const std::vector<mp_integer> &args_value) const
+{
+  PRECONDITION(args_value.size() >= 1 || args_value.size() <= 3);
+  const std::size_t &offset = numeric_cast_v<std::size_t>(args_value[0]);
+  const std::size_t &start =
+    args_value.size() > 1 ? numeric_cast_v<std::size_t>(args_value[1]) : 0;
+  const std::size_t &end = args_value.size() > 2
+                             ? numeric_cast_v<std::size_t>(args_value[2])
+                             : input2_value.size();
+
+  std::vector<mp_integer> result(input1_value);
+  result.insert(
+    result.begin() + offset,
+    input2_value.begin() + start,
+    input2_value.end() + end);
+  return result;
+}
+
+optionalt<exprt> string_insertion_builtin_functiont::eval(
+  const std::function<exprt(const exprt &)> &get_value) const
+{
+  const auto &input1_value = eval_string(input1, get_value);
+  const auto &input2_value = eval_string(input2, get_value);
+  if(!input2_value.has_value() || !input1_value.has_value())
+    return {};
+
+  std::vector<mp_integer> arg_values;
+  const auto &insert = std::back_inserter(arg_values);
+  const mp_integer unknown('?');
+  std::transform(
+    args.begin(), args.end(), insert, [&](const exprt &e) { // NOLINT
+      if(const auto val = numeric_cast<mp_integer>(get_value(e)))
+        return *val;
+      return unknown;
+    });
+
+  const auto result_value = eval(*input1_value, *input2_value, arg_values);
+  const auto length = from_integer(result_value.size(), result.length().type());
+  const array_typet type(result.type().subtype(), length);
+  return make_string(result_value, type);
+}
+
 /// Construct a string_builtin_functiont object from a function application
 /// \return a unique pointer to the created object, this unique pointer is empty
 ///   if the function does not correspond to one of the supported
@@ -192,24 +378,37 @@ static std::unique_ptr<string_builtin_functiont> to_string_builtin_function(
       new string_insertion_builtin_functiont(fun_app.arguments(), array_pool));
 
   if(id == ID_cprover_string_concat_func)
-    return std::unique_ptr<string_builtin_functiont>(
-      new string_insertion_builtin_functiont(fun_app.arguments(), array_pool));
+    return util_make_unique<string_concatenation_builtin_functiont>(
+      fun_app.arguments(), array_pool);
+
+  if(id == ID_cprover_string_concat_char_func)
+    return util_make_unique<string_concat_char_builtin_functiont>(
+      fun_app.arguments(), array_pool);
 
   return {};
 }
 
-string_dependencest::string_nodet &
-string_dependencest::get_node(const array_string_exprt &e)
+string_dependenciest::string_nodet &
+string_dependenciest::get_node(const array_string_exprt &e)
 {
   auto entry_inserted = node_index_pool.emplace(e, string_nodes.size());
   if(!entry_inserted.second)
     return string_nodes[entry_inserted.first->second];
 
-  string_nodes.emplace_back();
+  string_nodes.emplace_back(e, entry_inserted.first->second);
   return string_nodes.back();
 }
 
-string_dependencest::builtin_function_nodet string_dependencest::make_node(
+std::unique_ptr<const string_dependenciest::string_nodet>
+string_dependenciest::node_at(const array_string_exprt &e) const
+{
+  const auto &it = node_index_pool.find(e);
+  if(it != node_index_pool.end())
+    return util_make_unique<const string_nodet>(string_nodes.at(it->second));
+  return {};
+}
+
+string_dependenciest::builtin_function_nodet string_dependenciest::make_node(
   std::unique_ptr<string_builtin_functiont> &builtin_function)
 {
   const builtin_function_nodet builtin_function_node(
@@ -219,36 +418,54 @@ string_dependencest::builtin_function_nodet string_dependencest::make_node(
   return builtin_function_node;
 }
 
-const string_builtin_functiont &string_dependencest::get_builtin_function(
+const string_builtin_functiont &string_dependenciest::get_builtin_function(
   const builtin_function_nodet &node) const
 {
   PRECONDITION(node.index < builtin_function_nodes.size());
   return *(builtin_function_nodes[node.index]);
 }
 
-const std::vector<string_dependencest::builtin_function_nodet> &
-string_dependencest::dependencies(
-  const string_dependencest::string_nodet &node) const
+const std::vector<string_dependenciest::builtin_function_nodet> &
+string_dependenciest::dependencies(
+  const string_dependenciest::string_nodet &node) const
 {
   return node.dependencies;
 }
 
-void string_dependencest::add_dependency(
+void string_dependenciest::add_dependency(
   const array_string_exprt &e,
   const builtin_function_nodet &builtin_function_node)
 {
+  if(e.id() == ID_if)
+  {
+    const auto if_expr = to_if_expr(e);
+    const auto &true_case = to_array_string_expr(if_expr.true_case());
+    const auto &false_case = to_array_string_expr(if_expr.false_case());
+    add_dependency(true_case, builtin_function_node);
+    add_dependency(false_case, builtin_function_node);
+    return;
+  }
   string_nodet &string_node = get_node(e);
   string_node.dependencies.push_back(builtin_function_node);
 }
 
-void string_dependencest::add_unknown_dependency(const array_string_exprt &e)
+void string_dependenciest::add_unknown_dependency(const array_string_exprt &e)
 {
+  if(e.id() == ID_if)
+  {
+    const auto if_expr = to_if_expr(e);
+    const auto &true_case = to_array_string_expr(if_expr.true_case());
+    const auto &false_case = to_array_string_expr(if_expr.false_case());
+    add_unknown_dependency(true_case);
+    add_unknown_dependency(false_case);
+    return;
+  }
   string_nodet &string_node = get_node(e);
   string_node.depends_on_unknown_builtin_function = true;
 }
 
 static void add_unknown_dependency_to_string_subexprs(
-  string_dependencest &dependencies,
+  string_dependenciest &dependencies,
   const function_application_exprt &fun_app,
   array_poolt &array_pool)
 {
@@ -256,11 +473,11 @@ static void add_unknown_dependency_to_string_subexprs(
   {
     std::for_each(
       expr.depth_begin(), expr.depth_end(), [&](const exprt &e) { // NOLINT
-        const auto &string_struct = expr_try_dynamic_cast<struct_exprt>(e);
-        if(string_struct && string_struct->operands().size() == 2)
+        if(is_refined_string_type(e.type()))
         {
+          const auto &string_struct = expr_checked_cast<struct_exprt>(e);
           const array_string_exprt string =
-            array_pool.find(string_struct->op1(), string_struct->op0());
+            array_pool.find(string_struct.op1(), string_struct.op0());
           dependencies.add_unknown_dependency(string);
         }
       });
@@ -268,9 +485,9 @@ static void add_unknown_dependency_to_string_subexprs(
 }
 
 static void add_dependency_to_string_subexprs(
-  string_dependencest &dependencies,
+  string_dependenciest &dependencies,
   const function_application_exprt &fun_app,
-  const string_dependencest::builtin_function_nodet &builtin_function_node,
+  const string_dependenciest::builtin_function_nodet &builtin_function_node,
   array_poolt &array_pool)
 {
   PRECONDITION(fun_app.arguments()[0].type().id() != ID_pointer);
@@ -290,65 +507,49 @@ static void add_dependency_to_string_subexprs(
       expr.depth_begin(),
       expr.depth_end(),
       [&](const exprt &e) { // NOLINT
-        if(const auto structure = expr_try_dynamic_cast<struct_exprt>(e))
+        if(is_refined_string_type(e.type()))
         {
-          const array_string_exprt string = array_pool.of_argument(*structure);
+          const auto string_struct = expr_checked_cast<struct_exprt>(e);
+          const auto string = array_pool.of_argument(string_struct);
           dependencies.add_dependency(string, builtin_function_node);
         }
       });
   }
 }
 
-string_dependencest::node_indext string_dependencest::size() const
+optionalt<exprt> string_dependenciest::eval(
+  const array_string_exprt &s,
+  const std::function<exprt(const exprt &)> &get_value) const
 {
-  return builtin_function_nodes.size() + string_nodes.size();
-}
-
-/// Convert an index of a string node in `string_nodes` to the node_indext for
-/// the same node
-static std::size_t string_index_to_node_index(const std::size_t string_index)
-{
-  return 2 * string_index + 1;
-}
-
-/// Convert an index of a builtin function node to the node_indext for
-/// the same node
-static std::size_t
-builtin_function_index_to_node_index(const std::size_t builtin_index)
-{
-  return 2 * builtin_index;
-}
-
-string_dependencest::node_indext
-string_dependencest::node_index(const builtin_function_nodet &n) const
-{
-  return builtin_function_index_to_node_index(n.index);
-}
+  const auto &it = node_index_pool.find(s);
+  if(it == node_index_pool.end())
+    return {};
 
-string_dependencest::node_indext
-string_dependencest::node_index(const array_string_exprt &s) const
-{
-  return string_index_to_node_index(node_index_pool.at(s));
-}
+  if(eval_string_cache[it->second])
+    return eval_string_cache[it->second];
 
-optionalt<string_dependencest::builtin_function_nodet>
-string_dependencest::get_builtin_function_node(node_indext i) const
-{
-  if(i % 2 == 0)
-    return builtin_function_nodet(i / 2);
+  const auto node = string_nodes[it->second];
+  const auto &f = node.result_from;
+  if(
+    f && node.dependencies.size() == 1 &&
+    !node.depends_on_unknown_builtin_function)
+  {
+    const auto value_opt = get_builtin_function(*f).eval(get_value);
+    eval_string_cache[it->second] = value_opt;
+    return value_opt;
+  }
   return {};
 }
 
-optionalt<string_dependencest::string_nodet>
-string_dependencest::get_string_node(node_indext i) const
+void string_dependenciest::clean_cache()
 {
-  if(i % 2 == 1 && i / 2 < string_nodes.size())
-    return string_nodes[i / 2];
-  return {};
+  eval_string_cache.resize(string_nodes.size());
+  for(auto &e : eval_string_cache)
+    e.reset();
 }
 
 bool add_node(
-  string_dependencest &dependencies,
+  string_dependenciest &dependencies,
   const equal_exprt &equation,
   array_poolt &array_pool)
 {
@@ -372,7 +573,11 @@ bool add_node(
   if(
     const auto &string_result =
       dependencies.get_builtin_function(builtin_function_node).string_result())
+  {
     dependencies.add_dependency(*string_result, builtin_function_node);
+    auto &node = dependencies.get_node(*string_result);
+    node.result_from = builtin_function_node;
+  }
   else
     add_dependency_to_string_subexprs(
       dependencies, *fun_app, builtin_function_node, array_pool);
@@ -380,51 +585,59 @@ bool add_node(
   return true;
 }
 
-void string_dependencest::for_each_successor(
-  const std::size_t &i,
-  const std::function<void(const std::size_t &)> &f) const
+void string_dependenciest::for_each_successor(
+  const nodet &node,
+  const std::function<void(const nodet &)> &f) const
 {
-  if(const auto &builtin_function_node = get_builtin_function_node(i))
+  if(node.kind == nodet::BUILTIN)
   {
-    const string_builtin_functiont &p =
-      get_builtin_function(*builtin_function_node);
-    std::for_each(
-      p.string_arguments().begin(),
-      p.string_arguments().end(),
-      [&](const array_string_exprt &s) { f(node_index(s)); });
+    const auto &builtin = builtin_function_nodes[node.index];
+    for(const auto &s : builtin->string_arguments())
+    {
+      if(const auto node = node_at(s))
+        f(nodet(*node));
+    }
   }
-  else if(const auto &s = get_string_node(i))
+  else if(node.kind == nodet::STRING)
   {
+    const auto &s_node = string_nodes[node.index];
     std::for_each(
-      s->dependencies.begin(),
-      s->dependencies.end(),
-      [&](const builtin_function_nodet &p) { f(node_index(p)); });
+      s_node.dependencies.begin(),
+      s_node.dependencies.end(),
+      [&](const builtin_function_nodet &p) { f(nodet(p)); });
   }
   else
     UNREACHABLE;
 }
 
-void string_dependencest::output_dot(std::ostream &stream) const
+void string_dependenciest::for_each_node(
+  const std::function<void(const nodet &)> &f) const
 {
-  const auto for_each_node =
-    [&](const std::function<void(const std::size_t &)> &f) { // NOLINT
-      for(std::size_t i = 0; i < string_nodes.size(); ++i)
-        f(string_index_to_node_index(i));
-      for(std::size_t i = 0; i < builtin_function_nodes.size(); ++i)
-        f(builtin_function_index_to_node_index(i));
-    };
-
-  const auto for_each_succ = [&](
-    const std::size_t &i,
-    const std::function<void(const std::size_t &)> &f) { // NOLINT
-    for_each_successor(i, f);
-  };
+  for(const auto string_node : string_nodes)
+    f(nodet(string_node));
+  for(std::size_t i = 0; i < builtin_function_nodes.size(); ++i)
+    f(nodet(builtin_function_nodet(i)));
+}
 
-  const auto node_to_string = [&](const std::size_t &i) { // NOLINT
-    return std::to_string(i);
+void string_dependenciest::output_dot(std::ostream &stream) const
+{
+  const auto for_each =
+    [&](const std::function<void(const nodet &)> &f) { // NOLINT
+      for_each_node(f);
+    };
+  const auto for_each_succ =
+    [&](const nodet &n, const std::function<void(const nodet &)> &f) { // NOLINT
+      for_each_successor(n, f);
+    };
+  const auto node_to_string = [&](const nodet &n) { // NOLINT
+    std::stringstream ostream;
+    if(n.kind == nodet::BUILTIN)
+      ostream << builtin_function_nodes[n.index]->name() << n.index;
+    else
+      ostream << '"' << format(string_nodes[n.index].expr) << '"';
+    return ostream.str();
   };
   stream << "digraph dependencies {\n";
-  output_dot_generic<std::size_t>(
-    stream, for_each_node, for_each_succ, node_to_string);
+  output_dot_generic<nodet>(stream, for_each, for_each_succ, node_to_string);
   stream << '}' << std::endl;
 }
diff --git a/src/solvers/refinement/string_refinement_util.h b/src/solvers/refinement/string_refinement_util.h
index 4501cd68ec3..b6e7a7880ee 100644
--- a/src/solvers/refinement/string_refinement_util.h
+++ b/src/solvers/refinement/string_refinement_util.h
@@ -145,8 +145,8 @@ class equation_symbol_mappingt
 class string_builtin_functiont
 {
 public:
-  string_builtin_functiont() = default;
   string_builtin_functiont(const string_builtin_functiont &) = delete;
+  virtual ~string_builtin_functiont() = default;
 
   virtual optionalt<array_string_exprt> string_result() const
   {
@@ -157,6 +157,14 @@ class string_builtin_functiont
   {
     return {};
   }
+
+  virtual optionalt<exprt>
+  eval(const std::function<exprt(const exprt &)> &get_value) const = 0;
+
+  virtual std::string name() const = 0;
+
+protected:
+  string_builtin_functiont() = default;
 };
 
 /// String builtin_function transforming one string into another
@@ -167,6 +175,12 @@ class string_transformation_builtin_functiont : public string_builtin_functiont
   array_string_exprt input;
   std::vector<exprt> args;
   exprt return_code;
+
+  /// Constructor from arguments of a function application
+  string_transformation_builtin_functiont(
+    const std::vector<exprt> &fun_args,
+    array_poolt &array_pool);
+
   optionalt<array_string_exprt> string_result() const override
   {
     return result;
@@ -175,6 +189,36 @@ class string_transformation_builtin_functiont : public string_builtin_functiont
   {
     return {input};
   }
+
+  /// Evaluate the result from a concrete valuation of the arguments
+  virtual std::vector<mp_integer> eval(
+    const std::vector<mp_integer> &input_value,
+    const std::vector<mp_integer> &args_value) const = 0;
+
+  optionalt<exprt>
+  eval(const std::function<exprt(const exprt &)> &get_value) const override;
+};
+
+/// Adding a character at the end of a string
+class string_concat_char_builtin_functiont
+  : public string_transformation_builtin_functiont
+{
+public:
+  string_concat_char_builtin_functiont(
+    const std::vector<exprt> &fun_args,
+    array_poolt &array_pool)
+    : string_transformation_builtin_functiont(fun_args, array_pool)
+  {
+  }
+
+  std::vector<mp_integer> eval(
+    const std::vector<mp_integer> &input_value,
+    const std::vector<mp_integer> &args_value) const override;
+
+  std::string name() const override
+  {
+    return "concat_char";
+  }
 };
 
 /// String inserting a string into another one
@@ -200,6 +244,42 @@ class string_insertion_builtin_functiont : public string_builtin_functiont
   {
     return {input1, input2};
   }
+
+  /// Evaluate the result from a concrete valuation of the arguments
+  virtual std::vector<mp_integer> eval(
+    const std::vector<mp_integer> &input1_value,
+    const std::vector<mp_integer> &input2_value,
+    const std::vector<mp_integer> &args_value) const;
+
+  optionalt<exprt>
+  eval(const std::function<exprt(const exprt &)> &get_value) const override;
+
+  std::string name() const override
+  {
+    return "insert";
+  }
+
+protected:
+  string_insertion_builtin_functiont() = default;
+};
+
+class string_concatenation_builtin_functiont final
+  : public string_insertion_builtin_functiont
+{
+public:
+  string_concatenation_builtin_functiont(
+    const std::vector<exprt> &fun_args,
+    array_poolt &array_pool);
+
+  std::vector<mp_integer> eval(
+    const std::vector<mp_integer> &input1_value,
+    const std::vector<mp_integer> &input2_value,
+    const std::vector<mp_integer> &args_value) const override;
+
+  std::string name() const override
+  {
+    return "concat";
+  }
 };
 
 /// String creation from other types
@@ -230,9 +310,9 @@ class string_test_builtin_functiont : public string_builtin_functiont
 };
 
 /// Keep track of dependencies between strings.
-/// Each string points to builtin_function calls on which it depends,
-/// each builtin_function points to the strings on which the result depend.
-class string_dependencest
+/// Each string points to the builtin_function calls on which it depends.
+/// Each builtin_function points to the strings on which the result depends.
+class string_dependenciest
 {
 public:
   /// A builtin_function node is just an index in the `builtin_function_nodes`
@@ -250,14 +330,28 @@ class string_dependencest
   class string_nodet
   {
   public:
+    // expression the node corresponds to
+    array_string_exprt expr;
+    // index in the string_nodes vector
+    std::size_t index;
+    // builtin functions on which it depends
     std::vector<builtin_function_nodet> dependencies;
-
+    // builtin function of which it is the result
+    optionalt<builtin_function_nodet> result_from;
     // In case it depends on a builtin_function we don't support yet
     bool depends_on_unknown_builtin_function = false;
+
+    explicit string_nodet(array_string_exprt e, const std::size_t index)
+      : expr(std::move(e)), index(index)
+    {
+    }
   };
 
   string_nodet &get_node(const array_string_exprt &e);
 
+  std::unique_ptr<const string_nodet>
+  node_at(const array_string_exprt &e) const;
+
   /// `builtin_function` is reset to an empty pointer after the node is created
   builtin_function_nodet
   make_node(std::unique_ptr<string_builtin_functiont> &builtin_function);
@@ -266,7 +360,9 @@ class string_dependencest
   const string_builtin_functiont &
   get_builtin_function(const builtin_function_nodet &node) const;
 
-  /// Add edge from node for `e` to node for `builtin_function`
+  /// Add edge from node for `e` to node for `builtin_function` if `e` is a
+  /// simple array expression. If it is an `if_exprt` we add the sub-expressions
+  /// that are not `if_exprt`s instead.
   void add_dependency(
     const array_string_exprt &e,
     const builtin_function_nodet &builtin_function);
@@ -274,6 +370,17 @@ class string_dependencest
   /// Mark node for `e` as depending on unknown builtin_function
   void add_unknown_dependency(const array_string_exprt &e);
 
+  /// 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:
@@ -288,38 +395,36 @@ class string_dependencest
   std::unordered_map<array_string_exprt, std::size_t, irep_hash>
     node_index_pool;
 
-  /// Common index for all nodes (both strings and builtin_functions) so that we
-  /// can reuse generic algorithms of util/graph.h
-  /// Even indexes correspond to builtin_function nodes, odd indexes to string
-  /// nodes.
-  typedef std::size_t node_indext;
-
-  /// \return total number of nodes
-  node_indext size() const;
+  class nodet
+  {
+  public:
+    enum
+    {
+      BUILTIN,
+      STRING
+    } kind;
+    std::size_t index;
 
-  /// \param n: builtin function node
-  /// \return index corresponding to builtin function node `n`
-  node_indext node_index(const builtin_function_nodet &n) const;
+    explicit nodet(const builtin_function_nodet &builtin)
+      : kind(BUILTIN), index(builtin.index)
+    {
+    }
 
-  /// \param s: array expression representing a string
-  /// \return index corresponding to an string exprt s
-  node_indext node_index(const array_string_exprt &s) const;
+    explicit nodet(const string_nodet &string_node)
+      : kind(STRING), index(string_node.index)
+    {
+    }
+  };
 
-  /// \param i: index of a node
-  /// \return corresponding node if the index corresponds to a builtin function
-  ///   node, empty optional otherwise
-  optionalt<builtin_function_nodet>
-  get_builtin_function_node(node_indext i) const;
+  mutable std::vector<optionalt<exprt>> eval_string_cache;
 
-  /// \param i: index of a node
-  /// \return corresponding node if the index corresponds to a string
-  ///   node, empty optional otherwise
-  optionalt<string_nodet> get_string_node(node_indext i) const;
+  /// Applies `f` on all nodes
+  void for_each_node(const std::function<void(const nodet &)> &f) const;
 
-  /// Applies `f` on all successors of the node with index `i`
+  /// Applies `f` on all successors of the node n
   void for_each_successor(
-    const node_indext &i,
-    const std::function<void(const node_indext &)> &f) const;
+    const nodet &i,
+    const std::function<void(const nodet &)> &f) const;
 };
 
 /// When right hand side of equation is a builtin_function add
@@ -336,7 +441,7 @@ class string_dependencest
 ///   the right hand side is not a function application
 /// \todo there should be a class with just the three functions we require here
 bool add_node(
-  string_dependencest &dependencies,
+  string_dependenciest &dependencies,
   const equal_exprt &equation,
   array_poolt &array_pool);
 
diff --git a/unit/solvers/refinement/string_refinement/dependency_graph.cpp b/unit/solvers/refinement/string_refinement/dependency_graph.cpp
index d4e9748badb..09c4b075fb0 100644
--- a/unit/solvers/refinement/string_refinement/dependency_graph.cpp
+++ b/unit/solvers/refinement/string_refinement/dependency_graph.cpp
@@ -47,7 +47,7 @@ SCENARIO("dependency_graph", "[core][solvers][refinement][string_refinement]")
 {
   GIVEN("dependency graph")
   {
-    string_dependencest dependences;
+    string_dependenciest dependences;
     refined_string_typet string_type(java_char_type(), java_int_type());
     const exprt string1 = make_string_argument("string1");
     const exprt string2 = make_string_argument("string2");
@@ -142,7 +142,7 @@ SCENARIO("dependency_graph", "[core][solvers][refinement][string_refinement]")
       THEN("string3 depends on primitive0")
       {
         const auto &node = dependences.get_node(char_array3);
-        const std::vector<string_dependencest::builtin_function_nodet>
+        const std::vector<string_dependenciest::builtin_function_nodet>
           &depends = dependences.dependencies(node);
         REQUIRE(depends.size() == 1);
         const auto &primitive0 = dependences.get_builtin_function(depends[0]);
@@ -159,7 +159,7 @@ SCENARIO("dependency_graph", "[core][solvers][refinement][string_refinement]")
       THEN("string5 depends on primitive1")
       {
         const auto &node = dependences.get_node(char_array5);
-        const std::vector<string_dependencest::builtin_function_nodet>
+        const std::vector<string_dependenciest::builtin_function_nodet>
           &depends = dependences.dependencies(node);
         REQUIRE(depends.size() == 1);
         const auto &primitive1 = dependences.get_builtin_function(depends[0]);
@@ -176,7 +176,7 @@ SCENARIO("dependency_graph", "[core][solvers][refinement][string_refinement]")
       THEN("string6 depends on primitive2")
       {
         const auto &node = dependences.get_node(char_array6);
-        const std::vector<string_dependencest::builtin_function_nodet>
+        const std::vector<string_dependenciest::builtin_function_nodet>
           &depends = dependences.dependencies(node);
         REQUIRE(depends.size() == 1);
         const auto &primitive2 = dependences.get_builtin_function(depends[0]);