diff --git a/src/solvers/Makefile b/src/solvers/Makefile
index 293d0419361..1e1f84b5f02 100644
--- a/src/solvers/Makefile
+++ b/src/solvers/Makefile
@@ -179,6 +179,7 @@ SRC = $(BOOLEFORCE_SRC) \
       refinement/bv_refinement_loop.cpp \
       refinement/refine_arithmetic.cpp \
       refinement/refine_arrays.cpp \
+      refinement/string_builtin_function.cpp \
       refinement/string_refinement.cpp \
       refinement/string_refinement_util.cpp \
       refinement/string_constraint_generator_code_points.cpp \
diff --git a/src/solvers/refinement/string_builtin_function.cpp b/src/solvers/refinement/string_builtin_function.cpp
new file mode 100644
index 00000000000..045a85a1c8e
--- /dev/null
+++ b/src/solvers/refinement/string_builtin_function.cpp
@@ -0,0 +1,209 @@
+/// Module: String solver
+/// Author: Diffblue Ltd.
+
+#include "string_builtin_function.h"
+
+#include <algorithm>
+#include "string_constraint_generator.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);
+
+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() > 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]);
+  input2 = array_pool.find(arg2.op1(), arg2.op0());
+  result = array_pool.find(fun_args[1], fun_args[0]);
+  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 exprt content = get_value(a.content());
+  const auto &array = expr_try_dynamic_cast<array_exprt>(content);
+  if(!array)
+    return {};
+
+  const auto &ops = array->operands();
+  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 auto start_index =
+    args_value.size() > 0 && args_value[0] > 0 ? args_value[0] : mp_integer(0);
+  const mp_integer input2_size(input2_value.size());
+  const auto end_index =
+    args_value.size() > 1
+      ? std::max(std::min(args_value[1], input2_size), start_index)
+      : input2_size;
+
+  std::vector<mp_integer> result(input1_value);
+  result.insert(
+    result.end(),
+    input2_value.begin() + numeric_cast_v<std::size_t>(start_index),
+    input2_value.begin() + numeric_cast_v<std::size_t>(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 auto offset = std::min(
+    std::max(args_value[0], mp_integer(0)), mp_integer(input1_value.size()));
+  const auto start = args_value.size() > 1
+                       ? std::max(args_value[1], mp_integer(0))
+                       : mp_integer(0);
+
+  const mp_integer input2_size(input2_value.size());
+  const auto end =
+    args_value.size() > 2
+      ? std::max(std::min(args_value[2], input2_size), mp_integer(0))
+      : input2_size;
+
+  std::vector<mp_integer> result(input1_value);
+  result.insert(
+    result.begin() + numeric_cast_v<std::size_t>(offset),
+    input2_value.begin() + numeric_cast_v<std::size_t>(start),
+    input2_value.begin() + numeric_cast_v<std::size_t>(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);
+}
diff --git a/src/solvers/refinement/string_builtin_function.h b/src/solvers/refinement/string_builtin_function.h
new file mode 100644
index 00000000000..3ebdd6dc8f3
--- /dev/null
+++ b/src/solvers/refinement/string_builtin_function.h
@@ -0,0 +1,200 @@
+/// Module: String solver
+/// Author: Diffblue Ltd.
+
+#ifndef CPROVER_SOLVERS_REFINEMENT_STRING_BUILTIN_FUNCTION_H
+#define CPROVER_SOLVERS_REFINEMENT_STRING_BUILTIN_FUNCTION_H
+
+#include <vector>
+#include <util/optional.h>
+#include <util/string_expr.h>
+
+class array_poolt;
+
+/// Base class for string functions that are built in the solver
+class string_builtin_functiont
+{
+public:
+  string_builtin_functiont(const string_builtin_functiont &) = delete;
+  virtual ~string_builtin_functiont() = default;
+
+  virtual optionalt<array_string_exprt> string_result() const
+  {
+    return {};
+  }
+
+  virtual std::vector<array_string_exprt> string_arguments() const
+  {
+    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
+class string_transformation_builtin_functiont : public string_builtin_functiont
+{
+public:
+  array_string_exprt result;
+  array_string_exprt input;
+  std::vector<exprt> args;
+  exprt return_code;
+
+  /// Constructor from arguments of a function application.
+  /// The arguments in `fun_args` should be in order:
+  /// an integer `result.length`, a character pointer `&result[0]`,
+  /// a string `arg1` of type refined_string_typet, and potentially some
+  /// arguments of primitive types.
+  string_transformation_builtin_functiont(
+    const std::vector<exprt> &fun_args,
+    array_poolt &array_pool);
+
+  optionalt<array_string_exprt> string_result() const override
+  {
+    return result;
+  }
+  std::vector<array_string_exprt> string_arguments() const override
+  {
+    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:
+  /// Constructor from arguments of a function application.
+  /// The arguments in `fun_args` should be in order:
+  /// an integer `result.length`, a character pointer `&result[0]`,
+  /// a string `arg1` of type refined_string_typet, and a character.
+  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
+class string_insertion_builtin_functiont : public string_builtin_functiont
+{
+public:
+  array_string_exprt result;
+  array_string_exprt input1;
+  array_string_exprt input2;
+  std::vector<exprt> args;
+  exprt return_code;
+
+  /// Constructor from arguments of a function application.
+  /// The arguments in `fun_args` should be in order:
+  /// an integer `result.length`, a character pointer `&result[0]`,
+  /// a string `arg1` of type refined_string_typet,
+  /// a string `arg2` of type refined_string_typet,
+  /// and potentially some arguments of primitive types.
+  string_insertion_builtin_functiont(
+    const std::vector<exprt> &fun_args,
+    array_poolt &array_pool);
+
+  optionalt<array_string_exprt> string_result() const override
+  {
+    return result;
+  }
+  std::vector<array_string_exprt> string_arguments() const override
+  {
+    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:
+  /// Constructor from arguments of a function application.
+  /// The arguments in `fun_args` should be in order:
+  /// an integer `result.length`, a character pointer `&result[0]`,
+  /// a string `arg1` of type refined_string_typet,
+  /// a string `arg2` of type refined_string_typet,
+  /// optionally followed by an integer `start` and an integer `end`.
+  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
+class string_creation_builtin_functiont : public string_builtin_functiont
+{
+public:
+  array_string_exprt result;
+  std::vector<exprt> args;
+  exprt return_code;
+
+  optionalt<array_string_exprt> string_result() const override
+  {
+    return result;
+  }
+};
+
+/// String test
+class string_test_builtin_functiont : public string_builtin_functiont
+{
+public:
+  exprt result;
+  std::vector<array_string_exprt> under_test;
+  std::vector<exprt> args;
+  std::vector<array_string_exprt> string_arguments() const override
+  {
+    return under_test;
+  }
+};
+
+#endif // CPROVER_SOLVERS_REFINEMENT_STRING_BUILTIN_FUNCTION_H
diff --git a/src/solvers/refinement/string_refinement_util.cpp b/src/solvers/refinement/string_refinement_util.cpp
index c9071509452..7da97d672c7 100644
--- a/src/solvers/refinement/string_refinement_util.cpp
+++ b/src/solvers/refinement/string_refinement_util.cpp
@@ -19,16 +19,6 @@
 #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 &&
@@ -173,200 +163,6 @@ 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() > 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]);
-  input2 = array_pool.find(arg2.op1(), arg2.op0());
-  result = array_pool.find(fun_args[1], fun_args[0]);
-  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 auto start_index =
-    args_value.size() > 0 && args_value[0] > 0 ? args_value[0] : mp_integer(0);
-  const mp_integer input2_size(input2_value.size());
-  const auto end_index =
-    args_value.size() > 1
-      ? std::max(std::min(args_value[1], input2_size), start_index)
-      : input2_size;
-
-  std::vector<mp_integer> result(input1_value);
-  result.insert(
-    result.end(),
-    input2_value.begin() + numeric_cast_v<std::size_t>(start_index),
-    input2_value.begin() + numeric_cast_v<std::size_t>(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 auto offset = std::max(args_value[0], mp_integer(0));
-  const auto start = args_value.size() > 1
-                       ? std::max(args_value[1], mp_integer(0))
-                       : mp_integer(0);
-
-  const mp_integer input2_size(input2_value.size());
-  const auto end =
-    args_value.size() > 2
-      ? std::max(std::min(args_value[2], input2_size), mp_integer(0))
-      : input2_size;
-
-  std::vector<mp_integer> result(input1_value);
-  result.insert(
-    result.begin() + numeric_cast_v<std::size_t>(offset),
-    input2_value.begin() + numeric_cast_v<std::size_t>(start),
-    input2_value.begin() + numeric_cast_v<std::size_t>(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
@@ -600,8 +396,21 @@ void string_dependenciest::for_each_successor(
     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));
+      std::vector<std::reference_wrapper<const exprt>> stack({s});
+      while(!stack.empty())
+      {
+        const auto current = stack.back();
+        stack.pop_back();
+        if(const auto if_expr = expr_try_dynamic_cast<if_exprt>(current.get()))
+        {
+          stack.emplace_back(if_expr->true_case());
+          stack.emplace_back(if_expr->false_case());
+        }
+        else if(const auto node = node_at(to_array_string_expr(current)))
+          f(nodet(*node));
+        else
+          UNREACHABLE;
+      }
     }
   }
   else if(node.kind == nodet::STRING)
diff --git a/src/solvers/refinement/string_refinement_util.h b/src/solvers/refinement/string_refinement_util.h
index b6e7a7880ee..f4a0e219adb 100644
--- a/src/solvers/refinement/string_refinement_util.h
+++ b/src/solvers/refinement/string_refinement_util.h
@@ -9,6 +9,7 @@
 #ifndef CPROVER_SOLVERS_REFINEMENT_STRING_REFINEMENT_UTIL_H
 #define CPROVER_SOLVERS_REFINEMENT_STRING_REFINEMENT_UTIL_H
 
+#include "string_builtin_function.h"
 #include "string_constraint.h"
 #include "string_constraint_generator.h"
 
@@ -141,173 +142,6 @@ class equation_symbol_mappingt
   std::unordered_map<std::size_t, std::vector<exprt>> strings_in_equation;
 };
 
-/// Base class for string functions that are built in the solver
-class string_builtin_functiont
-{
-public:
-  string_builtin_functiont(const string_builtin_functiont &) = delete;
-  virtual ~string_builtin_functiont() = default;
-
-  virtual optionalt<array_string_exprt> string_result() const
-  {
-    return {};
-  }
-
-  virtual std::vector<array_string_exprt> string_arguments() const
-  {
-    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
-class string_transformation_builtin_functiont : public string_builtin_functiont
-{
-public:
-  array_string_exprt result;
-  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;
-  }
-  std::vector<array_string_exprt> string_arguments() const override
-  {
-    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
-class string_insertion_builtin_functiont : public string_builtin_functiont
-{
-public:
-  array_string_exprt result;
-  array_string_exprt input1;
-  array_string_exprt input2;
-  std::vector<exprt> args;
-  exprt return_code;
-
-  /// Constructor from arguments of a function application
-  string_insertion_builtin_functiont(
-    const std::vector<exprt> &fun_args,
-    array_poolt &array_pool);
-
-  optionalt<array_string_exprt> string_result() const override
-  {
-    return result;
-  }
-  std::vector<array_string_exprt> string_arguments() const override
-  {
-    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
-class string_creation_builtin_functiont : public string_builtin_functiont
-{
-public:
-  array_string_exprt result;
-  std::vector<exprt> args;
-  exprt return_code;
-
-  optionalt<array_string_exprt> string_result() const override
-  {
-    return result;
-  }
-};
-
-/// String test
-class string_test_builtin_functiont : public string_builtin_functiont
-{
-public:
-  exprt result;
-  std::vector<array_string_exprt> under_test;
-  std::vector<exprt> args;
-  std::vector<array_string_exprt> string_arguments() const override
-  {
-    return under_test;
-  }
-};
 
 /// Keep track of dependencies between strings.
 /// Each string points to the builtin_function calls on which it depends.