diff --git a/jbmc/regression/jbmc-strings/literal_length/test.class b/jbmc/regression/jbmc-strings/literal_length/test.class
new file mode 100644
index 00000000000..c38f04581bc
Binary files /dev/null and b/jbmc/regression/jbmc-strings/literal_length/test.class differ
diff --git a/jbmc/regression/jbmc-strings/literal_length/test.desc b/jbmc/regression/jbmc-strings/literal_length/test.desc
new file mode 100644
index 00000000000..6dc55dbce56
--- /dev/null
+++ b/jbmc/regression/jbmc-strings/literal_length/test.desc
@@ -0,0 +1,12 @@
+CORE
+test.class
+--function test.main --trace
+^EXIT=10$
+^SIGNAL=0$
+^\[.*assertion.1\].* line 6.* FAILURE$
+abc_constarray=\{ 'a', 'b', 'c' \}
+--
+--
+Check that the string literal used in the constructor is properly concretized
+in the trace even if it is not part of the equation.
+This is necessary for test generation.
diff --git a/jbmc/regression/jbmc-strings/literal_length/test.java b/jbmc/regression/jbmc-strings/literal_length/test.java
new file mode 100644
index 00000000000..504a628a421
--- /dev/null
+++ b/jbmc/regression/jbmc-strings/literal_length/test.java
@@ -0,0 +1,8 @@
+public class test
+{
+  public static void main()
+  {
+    String x = new String("abc");
+    assert false;
+  }
+}
diff --git a/jbmc/unit/solvers/strings/string_constraint_instantiation/instantiate_not_contains.cpp b/jbmc/unit/solvers/strings/string_constraint_instantiation/instantiate_not_contains.cpp
index 253f23c5133..6f1ec9f1ca8 100644
--- a/jbmc/unit/solvers/strings/string_constraint_instantiation/instantiate_not_contains.cpp
+++ b/jbmc/unit/solvers/strings/string_constraint_instantiation/instantiate_not_contains.cpp
@@ -88,18 +88,25 @@ exprt get_data_pointer(const array_string_exprt &arr)
 
 /// Creates a `string_exprt` of the proper string type.
 /// \param [in] str: string to convert
+/// \param array_pool: pool of arrays representing strings
 /// \return corresponding `string_exprt`
-refined_string_exprt make_refined_string_exprt(const array_string_exprt &arr)
+refined_string_exprt make_refined_string_exprt(
+  const array_string_exprt &arr,
+  array_poolt &array_pool)
 {
-  return refined_string_exprt(arr.length(), get_data_pointer(arr));
+  return refined_string_exprt(
+    array_pool.get_or_create_length(arr), get_data_pointer(arr));
 }
 
 /// For a constant `string_exprt`, creates a full index set.
 /// \param [in] s: `string_exprt` to create index set for
+/// \param array_pool: pool of arrays representing strings
 /// \return the corresponding index set
-std::set<exprt> full_index_set(const array_string_exprt &s)
+std::set<exprt>
+full_index_set(const array_string_exprt &s, array_poolt &array_pool)
 {
-  const mp_integer n = numeric_cast_v<mp_integer>(to_constant_expr(s.length()));
+  const mp_integer n = numeric_cast_v<mp_integer>(
+    to_constant_expr(to_array_type(s.type()).size()));
   std::set<exprt> ret;
   for(mp_integer i = 0; i < n; ++i)
     ret.insert(from_integer(i));
@@ -179,17 +186,20 @@ SCENARIO(
   // initialize architecture with sensible default values
   config.set_arch("none");
 
+  symbol_generatort symbol_generator;
+  array_poolt array_pool(symbol_generator);
+
   // Creating strings
   const auto ab_array = make_string_exprt("ab");
   const auto b_array = make_string_exprt("b");
   const auto a_array = make_string_exprt("a");
   const auto empty_array = make_string_exprt("");
   const auto cd_array = make_string_exprt("cd");
-  const auto ab = make_refined_string_exprt(ab_array);
-  const auto b = make_refined_string_exprt(b_array);
-  const auto a = make_refined_string_exprt(a_array);
-  const auto empty = make_refined_string_exprt(empty_array);
-  const auto cd = make_refined_string_exprt(cd_array);
+  const auto ab = make_refined_string_exprt(ab_array, array_pool);
+  const auto b = make_refined_string_exprt(b_array, array_pool);
+  const auto a = make_refined_string_exprt(a_array, array_pool);
+  const auto empty = make_refined_string_exprt(empty_array, array_pool);
+  const auto cd = make_refined_string_exprt(cd_array, array_pool);
 
   GIVEN("The not_contains axioms of String.lastIndexOf(String, Int)")
   {
@@ -247,8 +257,8 @@ SCENARIO(
     WHEN("we instantiate and simplify")
     {
       // Making index sets
-      const std::set<exprt> index_set_ab = full_index_set(ab_array);
-      const std::set<exprt> index_set_b = full_index_set(b_array);
+      const std::set<exprt> index_set_ab = full_index_set(ab_array, array_pool);
+      const std::set<exprt> index_set_b = full_index_set(b_array, array_pool);
 
       // List of new lemmas to be returned
       std::vector<exprt> lemmas;
@@ -305,7 +315,7 @@ SCENARIO(
     WHEN("we instantiate and simplify")
     {
       // Making index sets
-      const std::set<exprt> index_set_a = full_index_set(a_array);
+      const std::set<exprt> index_set_a = full_index_set(a_array, array_pool);
 
       // Instantiate the lemmas
       std::vector<exprt> lemmas = instantiate_not_contains(
@@ -355,8 +365,8 @@ SCENARIO(
     WHEN("we instantiate and simplify")
     {
       // Making index sets
-      const std::set<exprt> index_set_a = full_index_set(a_array);
-      const std::set<exprt> index_set_b = full_index_set(b_array);
+      const std::set<exprt> index_set_a = full_index_set(a_array, array_pool);
+      const std::set<exprt> index_set_b = full_index_set(b_array, array_pool);
 
       // Instantiate the lemmas
       std::vector<exprt> lemmas = instantiate_not_contains(
@@ -406,7 +416,7 @@ SCENARIO(
     WHEN("we instantiate and simplify")
     {
       // Making index sets
-      const std::set<exprt> index_set_a = full_index_set(a_array);
+      const std::set<exprt> index_set_a = full_index_set(a_array, array_pool);
       const std::set<exprt> index_set_empty = {
         generator.fresh_symbol("z", t.length_type())};
 
@@ -459,7 +469,7 @@ SCENARIO(
     WHEN("we instantiate and simplify")
     {
       // Making index sets
-      const std::set<exprt> index_set_ab = full_index_set(ab_array);
+      const std::set<exprt> index_set_ab = full_index_set(ab_array, array_pool);
 
       // Instantiate the lemmas
       std::vector<exprt> lemmas = instantiate_not_contains(
@@ -510,8 +520,8 @@ SCENARIO(
     WHEN("we instantiate and simplify")
     {
       // Making index sets
-      const std::set<exprt> index_set_ab = full_index_set(ab_array);
-      const std::set<exprt> index_set_cd = full_index_set(cd_array);
+      const std::set<exprt> index_set_ab = full_index_set(ab_array, array_pool);
+      const std::set<exprt> index_set_cd = full_index_set(cd_array, array_pool);
 
       // Instantiate the lemmas
       std::vector<exprt> lemmas = instantiate_not_contains(
diff --git a/src/solvers/strings/array_pool.cpp b/src/solvers/strings/array_pool.cpp
index 744c725be04..17891a4d90d 100644
--- a/src/solvers/strings/array_pool.cpp
+++ b/src/solvers/strings/array_pool.cpp
@@ -21,25 +21,48 @@ operator()(const irep_idt &prefix, const typet &type)
   return result;
 }
 
-exprt array_poolt::get_length(const array_string_exprt &s) const
+exprt array_poolt::get_or_create_length(const array_string_exprt &s)
 {
-  if(s.length() == infinity_exprt(s.length().type()))
+  if(const auto &if_expr = expr_try_dynamic_cast<if_exprt>((exprt)s))
   {
-    auto it = length_of_array.find(s);
-    if(it != length_of_array.end())
-      return it->second;
+    return if_exprt{
+      if_expr->cond(),
+      get_or_create_length(to_array_string_expr(if_expr->true_case())),
+      get_or_create_length(to_array_string_expr(if_expr->false_case()))};
   }
-  return s.length();
+
+  auto emplace_result =
+    length_of_array.emplace(s, symbol_exprt(s.length_type()));
+  if(emplace_result.second)
+  {
+    emplace_result.first->second =
+      fresh_symbol("string_length", s.length_type());
+  }
+
+  return emplace_result.first->second;
+}
+
+optionalt<exprt>
+array_poolt::get_length_if_exists(const array_string_exprt &s) const
+{
+  auto find_result = length_of_array.find(s);
+  if(find_result != length_of_array.end())
+    return find_result->second;
+  return {};
 }
 
 array_string_exprt
 array_poolt::fresh_string(const typet &index_type, const typet &char_type)
 {
-  symbol_exprt length = fresh_symbol("string_length", index_type);
-  array_typet array_type(char_type, length);
+  array_typet array_type{char_type, infinity_exprt(index_type)};
   symbol_exprt content = fresh_symbol("string_content", array_type);
   array_string_exprt str = to_array_string_expr(content);
-  created_strings_value.insert(str);
+  arrays_of_pointers.emplace(
+    address_of_exprt(index_exprt(str, from_integer(0, index_type))), str);
+
+  // add length to length_of_array map
+  get_or_create_length(str);
+
   return str;
 }
 
@@ -87,40 +110,73 @@ array_string_exprt array_poolt::make_char_array_for_char_pointer(
     to_array_string_expr(fresh_symbol(symbol_name, char_array_type));
   const auto insert_result =
     arrays_of_pointers.insert({char_pointer, array_sym});
+
+  // add length to length_of_array map
+  get_or_create_length(array_sym);
+
   return to_array_string_expr(insert_result.first->second);
 }
 
+/// Given an array_string_exprt, get the size of the underlying array. If that
+/// size is undefined, create a new symbol for the size.
+/// Then add an entry from `array_expr` to that size in the `length_of_array`
+/// map.
+///
+/// This function should only be used at the creation of the
+/// `array_string_exprt`s, as it is the only place where we can reliably refer
+/// to the size in the type of the array.
+static void attempt_assign_length_from_type(
+  const array_string_exprt &array_expr,
+  std::unordered_map<array_string_exprt, exprt, irep_hash> &length_of_array,
+  symbol_generatort &symbol_generator)
+{
+  DATA_INVARIANT(
+    array_expr.id() != ID_if,
+    "attempt_assign_length_from_type does not handle if exprts");
+  // This invariant seems always true, but I don't know why.
+  // If we find a case where this is violated, try calling
+  // attempt_assign_length_from_type on the true and false cases.
+  const exprt &size_from_type = to_array_type(array_expr.type()).size();
+  const exprt &size_to_assign =
+    size_from_type != infinity_exprt(size_from_type.type())
+      ? size_from_type
+      : symbol_generator("string_length", array_expr.length_type());
+
+  const auto emplace_result =
+    length_of_array.emplace(array_expr, size_to_assign);
+  INVARIANT(
+    emplace_result.second,
+    "attempt_assign_length_from_type should only be called when no entry"
+    "for the array_string_exprt exists in the length_of_array map");
+}
+
 void array_poolt::insert(
   const exprt &pointer_expr,
-  array_string_exprt &array_expr)
+  const array_string_exprt &array_expr)
 {
-  const exprt &length = array_expr.length();
-  if(length == infinity_exprt(length.type()))
-  {
-    auto pair = length_of_array.insert(
-      std::make_pair(array_expr, fresh_symbol("string_length", length.type())));
-    array_expr.length() = pair.first->second;
-  }
-
   const auto it_bool =
     arrays_of_pointers.insert(std::make_pair(pointer_expr, array_expr));
-  created_strings_value.insert(array_expr);
+
   INVARIANT(
     it_bool.second, "should not associate two arrays to the same pointer");
+
+  attempt_assign_length_from_type(array_expr, length_of_array, fresh_symbol);
 }
 
-const std::set<array_string_exprt> &array_poolt::created_strings() const
+/// Return a map mapping all array_string_exprt of the array_pool to their
+/// length.
+const std::unordered_map<array_string_exprt, exprt, irep_hash> &
+array_poolt::created_strings() const
 {
-  return created_strings_value;
+  return length_of_array;
 }
 
-const array_string_exprt &
-array_poolt::find(const exprt &pointer, const exprt &length)
+array_string_exprt array_poolt::find(const exprt &pointer, const exprt &length)
 {
   const array_typet array_type(pointer.type().subtype(), length);
   const array_string_exprt array =
     make_char_array_for_char_pointer(pointer, array_type);
-  return *created_strings_value.insert(array).first;
+  return array;
 }
 
 array_string_exprt of_argument(array_poolt &array_pool, const exprt &arg)
diff --git a/src/solvers/strings/array_pool.h b/src/solvers/strings/array_pool.h
index c23bea91016..6e6e3fd20fa 100644
--- a/src/solvers/strings/array_pool.h
+++ b/src/solvers/strings/array_pool.h
@@ -53,17 +53,31 @@ class array_poolt final
     return arrays_of_pointers;
   }
 
-  /// Associate an actual finite length to infinite arrays
+  /// Get the length of an array_string_exprt from the array_pool. If the length
+  /// does not yet exist, create a new symbol and add it to the pool.
+  ///
+  /// If the array_string_exprt is an `if` expression, the true and false parts
+  /// are handled independently (and recursively). That is, no new length symbol
+  /// is added to the pool for `if` expressions, but symbols may be added for
+  /// each of the parts.
   /// \param s: array expression representing a string
   /// \return expression for the length of `s`
-  exprt get_length(const array_string_exprt &s) const;
+  exprt get_or_create_length(const array_string_exprt &s);
 
-  void insert(const exprt &pointer_expr, array_string_exprt &array);
+  /// As opposed to get_length(), do not create a new symbol if the length
+  /// of the array_string_exprt does not have one in the array_pool, but instead
+  /// return an empty optional.
+  /// \param s: array expression representing a string
+  /// \return expression for the length of `s`, or empty optional
+  optionalt<exprt> get_length_if_exists(const array_string_exprt &s) const;
+
+  void insert(const exprt &pointer_expr, const array_string_exprt &array);
 
   /// Creates a new array if the pointer is not pointing to an array
-  const array_string_exprt &find(const exprt &pointer, const exprt &length);
+  array_string_exprt find(const exprt &pointer, const exprt &length);
 
-  const std::set<array_string_exprt> &created_strings() const;
+  const std::unordered_map<array_string_exprt, exprt, irep_hash> &
+  created_strings() const;
 
   /// Construct a string expression whose length and content are new variables
   /// \param index_type: type used to index characters of the strings
@@ -74,18 +88,19 @@ class array_poolt final
 
 private:
   /// Associate arrays to char pointers
+  /// Invariant: Each array_string_exprt in this map has a corresponding entry
+  ///            in length_of_array.
+  ///            This is enforced whenever we add an element to
+  ///            `arrays_of_pointers`, i.e. fresh_string()
+  ///            and make_char_array_for_char_pointer().
   std::unordered_map<exprt, array_string_exprt, irep_hash> arrays_of_pointers;
 
   /// Associate length to arrays of infinite size
-  std::unordered_map<array_string_exprt, symbol_exprt, irep_hash>
-    length_of_array;
+  std::unordered_map<array_string_exprt, exprt, irep_hash> length_of_array;
 
   /// Generate fresh symbols
   symbol_generatort &fresh_symbol;
 
-  /// Strings created in the pool
-  std::set<array_string_exprt> created_strings_value;
-
   array_string_exprt make_char_array_for_char_pointer(
     const exprt &char_pointer,
     const typet &char_array_type);
diff --git a/src/solvers/strings/string_builtin_function.cpp b/src/solvers/strings/string_builtin_function.cpp
index d53fe76e77e..ea08accba7d 100644
--- a/src/solvers/strings/string_builtin_function.cpp
+++ b/src/solvers/strings/string_builtin_function.cpp
@@ -25,7 +25,7 @@ string_transformation_builtin_functiont::
     const exprt &return_code,
     const std::vector<exprt> &fun_args,
     array_poolt &array_pool)
-  : string_builtin_functiont(return_code)
+  : string_builtin_functiont(return_code, array_pool)
 {
   PRECONDITION(fun_args.size() > 2);
   const auto arg1 = expr_checked_cast<struct_exprt>(fun_args[2]);
@@ -37,7 +37,7 @@ string_insertion_builtin_functiont::string_insertion_builtin_functiont(
   const exprt &return_code,
   const std::vector<exprt> &fun_args,
   array_poolt &array_pool)
-  : string_builtin_functiont(return_code)
+  : string_builtin_functiont(return_code, array_pool)
 {
   PRECONDITION(fun_args.size() > 4);
   const auto arg1 = expr_checked_cast<struct_exprt>(fun_args[2]);
@@ -53,7 +53,7 @@ string_concatenation_builtin_functiont::string_concatenation_builtin_functiont(
   const exprt &return_code,
   const std::vector<exprt> &fun_args,
   array_poolt &array_pool)
-  : string_insertion_builtin_functiont(return_code)
+  : string_insertion_builtin_functiont(return_code, array_pool)
 {
   PRECONDITION(fun_args.size() >= 4 && fun_args.size() <= 6);
   const auto arg1 = expr_checked_cast<struct_exprt>(fun_args[2]);
@@ -144,11 +144,17 @@ string_constraintst string_concatenation_builtin_functiont::constraints(
   auto pair = [&]() -> std::pair<exprt, string_constraintst> {
     if(args.size() == 0)
       return add_axioms_for_concat(
-        generator.fresh_symbol, result, input1, input2);
+        generator.fresh_symbol, result, input1, input2, array_pool);
     if(args.size() == 2)
     {
       return add_axioms_for_concat_substr(
-        generator.fresh_symbol, result, input1, input2, args[0], args[1]);
+        generator.fresh_symbol,
+        result,
+        input1,
+        input2,
+        args[0],
+        args[1],
+        array_pool);
     }
     UNREACHABLE;
   }();
@@ -159,10 +165,10 @@ string_constraintst string_concatenation_builtin_functiont::constraints(
 exprt string_concatenation_builtin_functiont::length_constraint() const
 {
   if(args.size() == 0)
-    return length_constraint_for_concat(result, input1, input2);
+    return length_constraint_for_concat(result, input1, input2, array_pool);
   if(args.size() == 2)
     return length_constraint_for_concat_substr(
-      result, input1, input2, args[0], args[1]);
+      result, input1, input2, args[0], args[1], array_pool);
   UNREACHABLE;
 }
 
@@ -201,12 +207,13 @@ string_constraintst string_concat_char_builtin_functiont::constraints(
   constraints.universal.push_back([&] {
     const symbol_exprt idx =
       generator.fresh_symbol("QA_index_concat_char", result.length_type());
-    const exprt upper_bound = zero_if_negative(input.length());
+    const exprt upper_bound =
+      zero_if_negative(array_pool.get_or_create_length(input));
     return string_constraintt(
       idx, upper_bound, equal_exprt(input[idx], result[idx]));
   }());
   constraints.existential.push_back(
-    equal_exprt(result[input.length()], character));
+    equal_exprt(result[array_pool.get_or_create_length(input)], character));
   constraints.existential.push_back(
     equal_exprt(return_code, from_integer(0, return_code.type())));
   return constraints;
@@ -214,7 +221,7 @@ string_constraintst string_concat_char_builtin_functiont::constraints(
 
 exprt string_concat_char_builtin_functiont::length_constraint() const
 {
-  return length_constraint_for_concat_char(result, input);
+  return length_constraint_for_concat_char(result, input, array_pool);
 }
 
 optionalt<exprt> string_set_char_builtin_functiont::eval(
@@ -250,14 +257,18 @@ string_constraintst string_set_char_builtin_functiont::constraints(
   constraints.existential.push_back(implies_exprt(
     and_exprt(
       binary_relation_exprt(from_integer(0, position.type()), ID_le, position),
-      binary_relation_exprt(position, ID_lt, result.length())),
+      binary_relation_exprt(
+        position, ID_lt, array_pool.get_or_create_length(result))),
     equal_exprt(result[position], character)));
   constraints.universal.push_back([&] {
     const symbol_exprt q =
       generator.fresh_symbol("QA_char_set", position.type());
     const equal_exprt a3_body(result[q], input[q]);
     return string_constraintt(
-      q, minimum(zero_if_negative(result.length()), position), a3_body);
+      q,
+      minimum(
+        zero_if_negative(array_pool.get_or_create_length(result)), position),
+      a3_body);
   }());
   constraints.universal.push_back([&] {
     const symbol_exprt q2 =
@@ -265,7 +276,10 @@ string_constraintst string_set_char_builtin_functiont::constraints(
     const plus_exprt lower_bound(position, from_integer(1, position.type()));
     const equal_exprt a4_body(result[q2], input[q2]);
     return string_constraintt(
-      q2, lower_bound, zero_if_negative(result.length()), a4_body);
+      q2,
+      lower_bound,
+      zero_if_negative(array_pool.get_or_create_length(result)),
+      a4_body);
   }());
   return constraints;
 }
@@ -273,7 +287,8 @@ string_constraintst string_set_char_builtin_functiont::constraints(
 exprt string_set_char_builtin_functiont::length_constraint() const
 {
   const exprt out_of_bounds = or_exprt(
-    binary_relation_exprt(position, ID_ge, input.length()),
+    binary_relation_exprt(
+      position, ID_ge, array_pool.get_or_create_length(input)),
     binary_relation_exprt(
       position, ID_lt, from_integer(0, input.length_type())));
   const exprt return_value = if_exprt(
@@ -281,7 +296,9 @@ exprt string_set_char_builtin_functiont::length_constraint() const
     from_integer(1, return_code.type()),
     from_integer(0, return_code.type()));
   return and_exprt(
-    equal_exprt(result.length(), input.length()),
+    equal_exprt(
+      array_pool.get_or_create_length(result),
+      array_pool.get_or_create_length(input)),
     equal_exprt(return_code, return_value));
 }
 
@@ -383,7 +400,9 @@ string_constraintst string_to_lower_case_builtin_functiont::constraints(
       return if_exprt(is_upper_case(input[idx]), converted, non_converted);
     }();
     return string_constraintt(
-      idx, zero_if_negative(result.length()), conditional_convert);
+      idx,
+      zero_if_negative(array_pool.get_or_create_length(result)),
+      conditional_convert);
   }());
   return constraints;
 }
@@ -427,7 +446,7 @@ string_constraintst string_to_upper_case_builtin_functiont::constraints(
       minus_exprt(input[idx], from_integer(0x20, char_type));
     return string_constraintt(
       idx,
-      zero_if_negative(result.length()),
+      zero_if_negative(array_pool.get_or_create_length(result)),
       equal_exprt(
         result[idx],
         if_exprt(is_lower_case(input[idx]), converted, input[idx])));
@@ -491,7 +510,7 @@ string_constraintst string_insertion_builtin_functiont::constraints(
   if(args.size() == 1)
   {
     auto pair = add_axioms_for_insert(
-      generator.fresh_symbol, result, input1, input2, args[0]);
+      generator.fresh_symbol, result, input1, input2, args[0], array_pool);
     pair.second.existential.push_back(equal_exprt(pair.first, return_code));
     return pair.second;
   }
@@ -503,7 +522,7 @@ string_constraintst string_insertion_builtin_functiont::constraints(
 exprt string_insertion_builtin_functiont::length_constraint() const
 {
   if(args.size() == 1)
-    return length_constraint_for_insert(result, input1, input2);
+    return length_constraint_for_insert(result, input1, input2, array_pool);
   if(args.size() == 3)
     UNIMPLEMENTED;
   UNREACHABLE;
@@ -518,7 +537,7 @@ string_creation_builtin_functiont::string_creation_builtin_functiont(
   const exprt &return_code,
   const std::vector<exprt> &fun_args,
   array_poolt &array_pool)
-  : string_builtin_functiont(return_code)
+  : string_builtin_functiont(return_code, array_pool)
 {
   PRECONDITION(fun_args.size() >= 3);
   result = array_pool.find(fun_args[1], fun_args[0]);
@@ -562,7 +581,7 @@ string_constraintst string_of_int_builtin_functiont::constraints(
   string_constraint_generatort &generator) const
 {
   auto pair = add_axioms_for_string_of_int_with_radix(
-    result, arg, radix, 0, generator.ns);
+    result, arg, radix, 0, generator.ns, array_pool);
   pair.second.existential.push_back(equal_exprt(pair.first, return_code));
   return pair.second;
 }
@@ -593,14 +612,15 @@ exprt string_of_int_builtin_functiont::length_constraint() const
 
   const exprt size_expr_with_sign = if_exprt(
     negative_arg, plus_exprt(size_expr, from_integer(1, type)), size_expr);
-  return equal_exprt(result.length(), size_expr_with_sign);
+  return equal_exprt(
+    array_pool.get_or_create_length(result), size_expr_with_sign);
 }
 
 string_builtin_function_with_no_evalt::string_builtin_function_with_no_evalt(
   const exprt &return_code,
   const function_application_exprt &f,
   array_poolt &array_pool)
-  : string_builtin_functiont(return_code), function_application(f)
+  : string_builtin_functiont(return_code, array_pool), function_application(f)
 {
   const std::vector<exprt> &fun_args = f.arguments();
   std::size_t i = 0;
diff --git a/src/solvers/strings/string_builtin_function.h b/src/solvers/strings/string_builtin_function.h
index bd7d1696580..271256bf302 100644
--- a/src/solvers/strings/string_builtin_function.h
+++ b/src/solvers/strings/string_builtin_function.h
@@ -64,8 +64,10 @@ class string_builtin_functiont
   string_builtin_functiont() = default;
 
 protected:
-  explicit string_builtin_functiont(exprt return_code)
-    : return_code(std::move(return_code))
+  array_poolt &array_pool;
+
+  string_builtin_functiont(exprt return_code, array_poolt &array_pool)
+    : return_code(std::move(return_code)), array_pool(array_pool)
   {
   }
 };
@@ -80,8 +82,9 @@ class string_transformation_builtin_functiont : public string_builtin_functiont
   string_transformation_builtin_functiont(
     exprt return_code,
     array_string_exprt result,
-    array_string_exprt input)
-    : string_builtin_functiont(std::move(return_code)),
+    array_string_exprt input,
+    array_poolt &array_pool)
+    : string_builtin_functiont(std::move(return_code), array_pool),
       result(std::move(result)),
       input(std::move(input))
   {
@@ -213,7 +216,9 @@ class string_to_lower_case_builtin_functiont
   exprt length_constraint() const override
   {
     return and_exprt(
-      equal_exprt(result.length(), input.length()),
+      equal_exprt(
+        array_pool.get_or_create_length(result),
+        array_pool.get_or_create_length(input)),
       equal_exprt(return_code, from_integer(0, return_code.type())));
   };
 };
@@ -235,11 +240,13 @@ class string_to_upper_case_builtin_functiont
   string_to_upper_case_builtin_functiont(
     exprt return_code,
     array_string_exprt result,
-    array_string_exprt input)
+    array_string_exprt input,
+    array_poolt &array_pool)
     : string_transformation_builtin_functiont(
         std::move(return_code),
         std::move(result),
-        std::move(input))
+        std::move(input),
+        array_pool)
   {
   }
 
@@ -262,7 +269,9 @@ class string_to_upper_case_builtin_functiont
   exprt length_constraint() const override
   {
     return and_exprt(
-      equal_exprt(result.length(), input.length()),
+      equal_exprt(
+        array_pool.get_or_create_length(result),
+        array_pool.get_or_create_length(input)),
       equal_exprt(return_code, from_integer(0, return_code.type())));
   };
 };
@@ -321,8 +330,10 @@ class string_insertion_builtin_functiont : public string_builtin_functiont
   }
 
 protected:
-  explicit string_insertion_builtin_functiont(const exprt &return_code)
-    : string_builtin_functiont(return_code)
+  explicit string_insertion_builtin_functiont(
+    const exprt &return_code,
+    array_poolt &array_pool)
+    : string_builtin_functiont(return_code, array_pool)
   {
   }
 };
diff --git a/src/solvers/strings/string_constraint_generator.h b/src/solvers/strings/string_constraint_generator.h
index 11031e0fcc0..4472b319dac 100644
--- a/src/solvers/strings/string_constraint_generator.h
+++ b/src/solvers/strings/string_constraint_generator.h
@@ -86,33 +86,38 @@ std::pair<exprt, string_constraintst> add_axioms_for_concat(
   symbol_generatort &fresh_symbol,
   const array_string_exprt &res,
   const array_string_exprt &s1,
-  const array_string_exprt &s2);
+  const array_string_exprt &s2,
+  array_poolt &array_pool);
 std::pair<exprt, string_constraintst> add_axioms_for_concat_substr(
   symbol_generatort &fresh_symbol,
   const array_string_exprt &res,
   const array_string_exprt &s1,
   const array_string_exprt &s2,
   const exprt &start_index,
-  const exprt &end_index);
+  const exprt &end_index,
+  array_poolt &array_pool);
 std::pair<exprt, string_constraintst> add_axioms_for_insert(
   symbol_generatort &fresh_symbol,
   const array_string_exprt &res,
   const array_string_exprt &s1,
   const array_string_exprt &s2,
-  const exprt &offset);
+  const exprt &offset,
+  array_poolt &array_pool);
 std::pair<exprt, string_constraintst> add_axioms_for_string_of_int_with_radix(
   const array_string_exprt &res,
   const exprt &input_int,
   const exprt &radix,
   size_t max_size,
-  const namespacet &ns);
+  const namespacet &ns,
+  array_poolt &array_pool);
 
 string_constraintst add_constraint_on_characters(
   symbol_generatort &fresh_symbol,
   const array_string_exprt &s,
   const exprt &start,
   const exprt &end,
-  const std::string &char_set);
+  const std::string &char_set,
+  array_poolt &array_pool);
 std::pair<exprt, string_constraintst> add_axioms_for_constrain_characters(
   symbol_generatort &fresh_symbol,
   const function_application_exprt &f,
@@ -186,6 +191,7 @@ std::pair<exprt, string_constraintst> add_axioms_for_concat_code_point(
 std::pair<exprt, string_constraintst> add_axioms_for_constant(
   const array_string_exprt &res,
   irep_idt sval,
+  array_poolt &array_pool,
   const exprt &guard = true_exprt());
 
 std::pair<exprt, string_constraintst> add_axioms_for_delete(
@@ -250,7 +256,8 @@ std::pair<exprt, string_constraintst> add_axioms_for_cprover_string(
   symbol_generatort &fresh_symbol,
   const array_string_exprt &res,
   const exprt &arg,
-  const exprt &guard);
+  const exprt &guard,
+  array_poolt &array_pool);
 std::pair<exprt, string_constraintst> add_axioms_from_literal(
   symbol_generatort &fresh_symbol,
   const function_application_exprt &f,
@@ -260,9 +267,12 @@ std::pair<exprt, string_constraintst> add_axioms_for_string_of_int(
   const array_string_exprt &res,
   const exprt &input_int,
   size_t max_size,
-  const namespacet &ns);
-std::pair<exprt, string_constraintst>
-add_axioms_from_int_hex(const array_string_exprt &res, const exprt &i);
+  const namespacet &ns,
+  array_poolt &array_pool);
+std::pair<exprt, string_constraintst> add_axioms_from_int_hex(
+  const array_string_exprt &res,
+  const exprt &i,
+  array_poolt &array_pool);
 std::pair<exprt, string_constraintst> add_axioms_from_int_hex(
   const function_application_exprt &f,
   array_poolt &array_pool);
@@ -273,23 +283,29 @@ std::pair<exprt, string_constraintst> add_axioms_from_long(
 std::pair<exprt, string_constraintst> add_axioms_from_bool(
   const function_application_exprt &f,
   array_poolt &array_pool);
-std::pair<exprt, string_constraintst>
-add_axioms_from_bool(const array_string_exprt &res, const exprt &i);
+std::pair<exprt, string_constraintst> add_axioms_from_bool(
+  const array_string_exprt &res,
+  const exprt &b,
+  array_poolt &array_pool);
 std::pair<exprt, string_constraintst> add_axioms_from_char(
   const function_application_exprt &f,
   array_poolt &array_pool);
-std::pair<exprt, string_constraintst>
-add_axioms_from_char(const array_string_exprt &res, const exprt &i);
+std::pair<exprt, string_constraintst> add_axioms_from_char(
+  const array_string_exprt &res,
+  const exprt &c,
+  array_poolt &array_pool);
 std::pair<exprt, string_constraintst> add_axioms_for_index_of(
   symbol_generatort &fresh_symbol,
   const array_string_exprt &str,
   const exprt &c,
-  const exprt &from_index);
+  const exprt &from_index,
+  array_poolt &array_pool);
 std::pair<exprt, string_constraintst> add_axioms_for_index_of_string(
   symbol_generatort &fresh_symbol,
   const array_string_exprt &haystack,
   const array_string_exprt &needle,
-  const exprt &from_index);
+  const exprt &from_index,
+  array_poolt &array_pool);
 std::pair<exprt, string_constraintst> add_axioms_for_index_of(
   symbol_generatort &fresh_symbol,
   const function_application_exprt &f,
@@ -298,12 +314,14 @@ std::pair<exprt, string_constraintst> add_axioms_for_last_index_of_string(
   symbol_generatort &fresh_symbol,
   const array_string_exprt &haystack,
   const array_string_exprt &needle,
-  const exprt &from_index);
+  const exprt &from_index,
+  array_poolt &array_pool);
 std::pair<exprt, string_constraintst> add_axioms_for_last_index_of(
   symbol_generatort &fresh_symbol,
   const array_string_exprt &str,
   const exprt &c,
-  const exprt &from_index);
+  const exprt &from_index,
+  array_poolt &array_pool);
 
 std::pair<exprt, string_constraintst> add_axioms_for_last_index_of(
   symbol_generatort &fresh_symbol,
@@ -328,8 +346,9 @@ std::pair<exprt, string_constraintst> add_axioms_for_string_of_float(
   const namespacet &ns);
 std::pair<exprt, string_constraintst> add_axioms_for_fractional_part(
   const array_string_exprt &res,
-  const exprt &i,
-  size_t max_size);
+  const exprt &int_expr,
+  size_t max_size,
+  array_poolt &array_pool);
 std::pair<exprt, string_constraintst> add_axioms_from_float_scientific_notation(
   symbol_generatort &fresh_symbol,
   const array_string_exprt &res,
@@ -367,7 +386,8 @@ std::pair<exprt, string_constraintst> add_axioms_for_substring(
   const array_string_exprt &res,
   const array_string_exprt &str,
   const exprt &start,
-  const exprt &end);
+  const exprt &end,
+  array_poolt &array_pool);
 std::pair<exprt, string_constraintst> add_axioms_for_substring(
   symbol_generatort &fresh_symbol,
   const function_application_exprt &f,
@@ -380,7 +400,8 @@ std::pair<exprt, string_constraintst> add_axioms_for_trim(
 
 std::pair<exprt, string_constraintst> add_axioms_for_code_point(
   const array_string_exprt &res,
-  const exprt &code_point);
+  const exprt &code_point,
+  array_poolt &array_pool);
 std::pair<exprt, string_constraintst>
 add_axioms_for_char_literal(const function_application_exprt &f);
 
@@ -412,13 +433,15 @@ string_constraintst add_axioms_for_characters_in_integer_string(
   const array_string_exprt &str,
   const std::size_t max_string_length,
   const exprt &radix,
-  const unsigned long radix_ul);
+  const unsigned long radix_ul,
+  array_poolt &array_pool);
 string_constraintst add_axioms_for_correct_number_format(
   const array_string_exprt &str,
   const exprt &radix_as_char,
   const unsigned long radix_ul,
   const std::size_t max_size,
-  const bool strict_formatting);
+  const bool strict_formatting,
+  array_poolt &array_pool);
 std::pair<exprt, string_constraintst> add_axioms_for_parse_int(
   symbol_generatort &fresh_symbol,
   const function_application_exprt &f,
@@ -460,21 +483,25 @@ exprt sum_overflows(const plus_exprt &sum);
 
 exprt length_constraint_for_concat_char(
   const array_string_exprt &res,
-  const array_string_exprt &s1);
+  const array_string_exprt &s1,
+  array_poolt &array_pool);
 exprt length_constraint_for_concat(
   const array_string_exprt &res,
   const array_string_exprt &s1,
-  const array_string_exprt &s2);
+  const array_string_exprt &s2,
+  array_poolt &array_pool);
 exprt length_constraint_for_concat_substr(
   const array_string_exprt &res,
   const array_string_exprt &s1,
   const array_string_exprt &s2,
-  const exprt &start_index,
-  const exprt &end_index);
+  const exprt &start,
+  const exprt &end,
+  array_poolt &array_pool);
 exprt length_constraint_for_insert(
   const array_string_exprt &res,
   const array_string_exprt &s1,
-  const array_string_exprt &s2);
+  const array_string_exprt &s2,
+  array_poolt &array_pool);
 
 exprt zero_if_negative(const exprt &expr);
 
diff --git a/src/solvers/strings/string_constraint_generator_code_points.cpp b/src/solvers/strings/string_constraint_generator_code_points.cpp
index dc5f3baf0a7..def8e803c2f 100644
--- a/src/solvers/strings/string_constraint_generator_code_points.cpp
+++ b/src/solvers/strings/string_constraint_generator_code_points.cpp
@@ -16,10 +16,12 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com
 /// code point to a utf-16 string
 /// \param res: array of characters corresponding to the result fo the function
 /// \param code_point: an expression representing a java code point
+/// \param array_pool: pool of arrays representing strings
 /// \return integer expression equal to zero
 std::pair<exprt, string_constraintst> add_axioms_for_code_point(
   const array_string_exprt &res,
-  const exprt &code_point)
+  const exprt &code_point,
+  array_poolt &array_pool)
 {
   string_constraintst constraints;
   const typet &char_type = res.content().type().subtype();
@@ -41,10 +43,11 @@ std::pair<exprt, string_constraintst> add_axioms_for_code_point(
   exprt hex0400 = from_integer(0x0400, type);
 
   binary_relation_exprt small(code_point, ID_lt, hex010000);
-  implies_exprt a1(small, equal_to(res.length(), 1));
+  implies_exprt a1(small, equal_to(array_pool.get_or_create_length(res), 1));
   constraints.existential.push_back(a1);
 
-  implies_exprt a2(not_exprt(small), equal_to(res.length(), 2));
+  implies_exprt a2(
+    not_exprt(small), equal_to(array_pool.get_or_create_length(res), 2));
   constraints.existential.push_back(a2);
 
   typecast_exprt code_point_as_char(code_point, char_type);
@@ -164,10 +167,10 @@ std::pair<exprt, string_constraintst> add_axioms_for_code_point_before(
   array_string_exprt str = get_string_expr(array_pool, args[0]);
   string_constraintst constraints;
 
-  const exprt &char1 =
-    str[minus_exprt(args[1], from_integer(2, str.length().type()))];
-  const exprt &char2 =
-    str[minus_exprt(args[1], from_integer(1, str.length().type()))];
+  const exprt &char1 = str[minus_exprt(
+    args[1], from_integer(2, array_pool.get_or_create_length(str).type()))];
+  const exprt &char2 = str[minus_exprt(
+    args[1], from_integer(1, array_pool.get_or_create_length(str).type()))];
   const typecast_exprt char1_as_int(char1, return_type);
   const typecast_exprt char2_as_int(char2, return_type);
 
diff --git a/src/solvers/strings/string_constraint_generator_comparison.cpp b/src/solvers/strings/string_constraint_generator_comparison.cpp
index d12b13b18dc..84f92bb4ad1 100644
--- a/src/solvers/strings/string_constraint_generator_comparison.cpp
+++ b/src/solvers/strings/string_constraint_generator_comparison.cpp
@@ -46,15 +46,18 @@ std::pair<exprt, string_constraintst> add_axioms_for_equals(
   typet index_type = s1.length_type();
 
   // Axiom 1.
-  constraints.existential.push_back(
-    implies_exprt(eq, equal_exprt(s1.length(), s2.length())));
+  constraints.existential.push_back(implies_exprt(
+    eq,
+    equal_exprt(
+      array_pool.get_or_create_length(s1),
+      array_pool.get_or_create_length(s2))));
 
   // Axiom 2.
   constraints.universal.push_back([&] {
     const symbol_exprt qvar = fresh_symbol("QA_equal", index_type);
     return string_constraintt(
       qvar,
-      zero_if_negative(s1.length()),
+      zero_if_negative(array_pool.get_or_create_length(s1)),
       implies_exprt(eq, equal_exprt(s1[qvar], s2[qvar])));
   }());
 
@@ -63,12 +66,15 @@ std::pair<exprt, string_constraintst> add_axioms_for_equals(
     const symbol_exprt witness = fresh_symbol("witness_unequal", index_type);
     const exprt zero = from_integer(0, index_type);
     const and_exprt bound_witness(
-      binary_relation_exprt(witness, ID_lt, s1.length()),
+      binary_relation_exprt(
+        witness, ID_lt, array_pool.get_or_create_length(s1)),
       binary_relation_exprt(witness, ID_ge, zero));
     const and_exprt witnessing(
       bound_witness, notequal_exprt(s1[witness], s2[witness]));
     const and_exprt diff_length(
-      notequal_exprt(s1.length(), s2.length()),
+      notequal_exprt(
+        array_pool.get_or_create_length(s1),
+        array_pool.get_or_create_length(s2)),
       equal_exprt(witness, from_integer(-1, index_type)));
     return implies_exprt(not_exprt(eq), or_exprt(diff_length, witnessing));
   }());
@@ -147,21 +153,27 @@ std::pair<exprt, string_constraintst> add_axioms_for_equals_ignore_case(
   const exprt char_Z = from_integer('Z', char_type);
   const typet index_type = s1.length_type();
 
-  const implies_exprt a1(eq, equal_exprt(s1.length(), s2.length()));
+  const implies_exprt a1(
+    eq,
+    equal_exprt(
+      array_pool.get_or_create_length(s1),
+      array_pool.get_or_create_length(s2)));
   constraints.existential.push_back(a1);
 
   const symbol_exprt qvar = fresh_symbol("QA_equal_ignore_case", index_type);
   const exprt constr2 =
     character_equals_ignore_case(s1[qvar], s2[qvar], char_a, char_A, char_Z);
   const string_constraintt a2(
-    qvar, zero_if_negative(s1.length()), implies_exprt(eq, constr2));
+    qvar,
+    zero_if_negative(array_pool.get_or_create_length(s1)),
+    implies_exprt(eq, constr2));
   constraints.universal.push_back(a2);
 
   const symbol_exprt witness =
     fresh_symbol("witness_unequal_ignore_case", index_type);
   const exprt zero = from_integer(0, witness.type());
   const and_exprt bound_witness(
-    binary_relation_exprt(witness, ID_lt, s1.length()),
+    binary_relation_exprt(witness, ID_lt, array_pool.get_or_create_length(s1)),
     binary_relation_exprt(witness, ID_ge, zero));
   const exprt witness_eq = character_equals_ignore_case(
     s1[witness], s2[witness], char_a, char_A, char_Z);
@@ -169,7 +181,9 @@ std::pair<exprt, string_constraintst> add_axioms_for_equals_ignore_case(
   const implies_exprt a3(
     not_exprt(eq),
     or_exprt(
-      notequal_exprt(s1.length(), s2.length()),
+      notequal_exprt(
+        array_pool.get_or_create_length(s1),
+        array_pool.get_or_create_length(s2)),
       and_exprt(bound_witness, witness_diff)));
   constraints.existential.push_back(a3);
 
@@ -212,13 +226,17 @@ std::pair<exprt, string_constraintst> add_axioms_for_compare_to(
   const typet &index_type = s1.length_type();
 
   const equal_exprt res_null(res, from_integer(0, return_type));
-  const implies_exprt a1(res_null, equal_exprt(s1.length(), s2.length()));
+  const implies_exprt a1(
+    res_null,
+    equal_exprt(
+      array_pool.get_or_create_length(s1),
+      array_pool.get_or_create_length(s2)));
   constraints.existential.push_back(a1);
 
   const symbol_exprt i = fresh_symbol("QA_compare_to", index_type);
   const string_constraintt a2(
     i,
-    zero_if_negative(s1.length()),
+    zero_if_negative(array_pool.get_or_create_length(s1)),
     implies_exprt(res_null, equal_exprt(s1[i], s2[i])));
   constraints.universal.push_back(a2);
 
@@ -230,20 +248,31 @@ std::pair<exprt, string_constraintst> add_axioms_for_compare_to(
   const equal_exprt ret_length_diff(
     res,
     minus_exprt(
-      typecast_exprt(s1.length(), return_type),
-      typecast_exprt(s2.length(), return_type)));
+      typecast_exprt(array_pool.get_or_create_length(s1), return_type),
+      typecast_exprt(array_pool.get_or_create_length(s2), return_type)));
   const or_exprt guard1(
     and_exprt(
-      less_than_or_equal_to(s1.length(), s2.length()),
-      greater_than(s1.length(), x)),
+      less_than_or_equal_to(
+        array_pool.get_or_create_length(s1),
+        array_pool.get_or_create_length(s2)),
+      greater_than(array_pool.get_or_create_length(s1), x)),
     and_exprt(
-      greater_or_equal_to(s1.length(), s2.length()),
-      greater_than(s2.length(), x)));
+      greater_or_equal_to(
+        array_pool.get_or_create_length(s1),
+        array_pool.get_or_create_length(s2)),
+      greater_than(array_pool.get_or_create_length(s2), x)));
   const and_exprt cond1(ret_char_diff, guard1);
   const or_exprt guard2(
-    and_exprt(greater_than(s2.length(), s1.length()), equal_to(s1.length(), x)),
     and_exprt(
-      greater_than(s1.length(), s2.length()), equal_to(s2.length(), x)));
+      greater_than(
+        array_pool.get_or_create_length(s2),
+        array_pool.get_or_create_length(s1)),
+      equal_to(array_pool.get_or_create_length(s1), x)),
+    and_exprt(
+      greater_than(
+        array_pool.get_or_create_length(s1),
+        array_pool.get_or_create_length(s2)),
+      equal_to(array_pool.get_or_create_length(s2), x)));
   const and_exprt cond2(ret_length_diff, guard2);
 
   const implies_exprt a3(
diff --git a/src/solvers/strings/string_constraint_generator_concat.cpp b/src/solvers/strings/string_constraint_generator_concat.cpp
index 1c7acc0b30b..fb4403bc456 100644
--- a/src/solvers/strings/string_constraint_generator_concat.cpp
+++ b/src/solvers/strings/string_constraint_generator_concat.cpp
@@ -34,6 +34,7 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com
 /// \param s2: an array of characters expression
 /// \param start_index: integer expression
 /// \param end_index: integer expression
+/// \param array_pool: pool of arrays representing strings
 /// \return integer expression `0`
 std::pair<exprt, string_constraintst> add_axioms_for_concat_substr(
   symbol_generatort &fresh_symbol,
@@ -41,22 +42,26 @@ std::pair<exprt, string_constraintst> add_axioms_for_concat_substr(
   const array_string_exprt &s1,
   const array_string_exprt &s2,
   const exprt &start_index,
-  const exprt &end_index)
+  const exprt &end_index,
+  array_poolt &array_pool)
 {
   string_constraintst constraints;
   const typet &index_type = start_index.type();
   const exprt start1 = maximum(start_index, from_integer(0, index_type));
-  const exprt end1 = maximum(minimum(end_index, s2.length()), start1);
+  const exprt end1 =
+    maximum(minimum(end_index, array_pool.get_or_create_length(s2)), start1);
 
   // Axiom 1.
-  constraints.existential.push_back(
-    length_constraint_for_concat_substr(res, s1, s2, start_index, end_index));
+  constraints.existential.push_back(length_constraint_for_concat_substr(
+    res, s1, s2, start_index, end_index, array_pool));
 
   // Axiom 2.
   constraints.universal.push_back([&] {
     const symbol_exprt idx = fresh_symbol("QA_index_concat", res.length_type());
     return string_constraintt(
-      idx, zero_if_negative(s1.length()), equal_exprt(s1[idx], res[idx]));
+      idx,
+      zero_if_negative(array_pool.get_or_create_length(s1)),
+      equal_exprt(s1[idx], res[idx]));
   }());
 
   // Axiom 3.
@@ -64,8 +69,11 @@ std::pair<exprt, string_constraintst> add_axioms_for_concat_substr(
     const symbol_exprt idx2 =
       fresh_symbol("QA_index_concat2", res.length_type());
     const equal_exprt res_eq(
-      res[plus_exprt(idx2, s1.length())], s2[plus_exprt(start1, idx2)]);
-    const minus_exprt upper_bound(res.length(), s1.length());
+      res[plus_exprt(idx2, array_pool.get_or_create_length(s1))],
+      s2[plus_exprt(start1, idx2)]);
+    const minus_exprt upper_bound(
+      array_pool.get_or_create_length(res),
+      array_pool.get_or_create_length(s1));
     return string_constraintt(idx2, zero_if_negative(upper_bound), res_eq);
   }());
 
@@ -82,15 +90,20 @@ exprt length_constraint_for_concat_substr(
   const array_string_exprt &s1,
   const array_string_exprt &s2,
   const exprt &start,
-  const exprt &end)
+  const exprt &end,
+  array_poolt &array_pool)
 {
   PRECONDITION(res.length_type().id() == ID_signedbv);
   const exprt start1 = maximum(start, from_integer(0, start.type()));
-  const exprt end1 = maximum(minimum(end, s2.length()), start1);
-  const plus_exprt res_length(s1.length(), minus_exprt(end1, start1));
+  const exprt end1 =
+    maximum(minimum(end, array_pool.get_or_create_length(s2)), start1);
+  const plus_exprt res_length(
+    array_pool.get_or_create_length(s1), minus_exprt(end1, start1));
   const exprt overflow = sum_overflows(res_length);
   const exprt max_int = to_signedbv_type(res.length_type()).largest_expr();
-  return equal_exprt(res.length(), if_exprt(overflow, max_int, res_length));
+  return equal_exprt(
+    array_pool.get_or_create_length(res),
+    if_exprt(overflow, max_int, res_length));
 }
 
 /// Add axioms enforcing that the length of `res` is that of the concatenation
@@ -98,19 +111,27 @@ exprt length_constraint_for_concat_substr(
 exprt length_constraint_for_concat(
   const array_string_exprt &res,
   const array_string_exprt &s1,
-  const array_string_exprt &s2)
+  const array_string_exprt &s2,
+  array_poolt &array_pool)
 {
-  return equal_exprt(res.length(), plus_exprt(s1.length(), s2.length()));
+  return equal_exprt(
+    array_pool.get_or_create_length(res),
+    plus_exprt(
+      array_pool.get_or_create_length(s1),
+      array_pool.get_or_create_length(s2)));
 }
 
 /// Add axioms enforcing that the length of `res` is that of the concatenation
 /// of `s1` with
 exprt length_constraint_for_concat_char(
   const array_string_exprt &res,
-  const array_string_exprt &s1)
+  const array_string_exprt &s1,
+  array_poolt &array_pool)
 {
   return equal_exprt(
-    res.length(), plus_exprt(s1.length(), from_integer(1, s1.length_type())));
+    array_pool.get_or_create_length(res),
+    plus_exprt(
+      array_pool.get_or_create_length(s1), from_integer(1, s1.length_type())));
 }
 
 /// Add axioms enforcing that `res` is equal to the concatenation of `s1` and
@@ -121,16 +142,24 @@ exprt length_constraint_for_concat_char(
 /// \param res: string_expression corresponding to the result
 /// \param s1: the string expression to append to
 /// \param s2: the string expression to append to the first one
+/// \param array_pool: pool of arrays representing strings
 /// \return an integer expression
 std::pair<exprt, string_constraintst> add_axioms_for_concat(
   symbol_generatort &fresh_symbol,
   const array_string_exprt &res,
   const array_string_exprt &s1,
-  const array_string_exprt &s2)
+  const array_string_exprt &s2,
+  array_poolt &array_pool)
 {
   exprt index_zero = from_integer(0, s2.length_type());
   return add_axioms_for_concat_substr(
-    fresh_symbol, res, s1, s2, index_zero, s2.length());
+    fresh_symbol,
+    res,
+    s1,
+    s2,
+    index_zero,
+    array_pool.get_or_create_length(s2),
+    array_pool);
 }
 
 /// Add axioms corresponding to the StringBuilder.appendCodePoint(I) function
@@ -153,6 +182,6 @@ std::pair<exprt, string_constraintst> add_axioms_for_concat_code_point(
   const array_string_exprt code_point =
     array_pool.fresh_string(index_type, char_type);
   return combine_results(
-    add_axioms_for_code_point(code_point, f.arguments()[3]),
-    add_axioms_for_concat(fresh_symbol, res, s1, code_point));
+    add_axioms_for_code_point(code_point, f.arguments()[3], array_pool),
+    add_axioms_for_concat(fresh_symbol, res, s1, code_point, array_pool));
 }
diff --git a/src/solvers/strings/string_constraint_generator_constants.cpp b/src/solvers/strings/string_constraint_generator_constants.cpp
index 1f79f567510..6101a6be320 100644
--- a/src/solvers/strings/string_constraint_generator_constants.cpp
+++ b/src/solvers/strings/string_constraint_generator_constants.cpp
@@ -18,15 +18,17 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com
 /// equal.
 /// \param res: array of characters for the result
 /// \param sval: a string constant
+/// \param array_pool: pool of arrays representing strings
 /// \param guard: condition under which the axiom should apply, true by default
 /// \return integer expression equal to zero
 std::pair<exprt, string_constraintst> add_axioms_for_constant(
   const array_string_exprt &res,
   irep_idt sval,
+  array_poolt &array_pool,
   const exprt &guard)
 {
   string_constraintst constraints;
-  const typet &index_type = res.length().type();
+  const typet index_type = array_pool.get_or_create_length(res).type();
   const typet &char_type = res.content().type().subtype();
   std::string c_str = id2string(sval);
   std::wstring str;
@@ -50,8 +52,8 @@ std::pair<exprt, string_constraintst> add_axioms_for_constant(
 
   const exprt s_length = from_integer(str.size(), index_type);
 
-  constraints.existential.push_back(
-    implies_exprt(guard, equal_exprt(res.length(), s_length)));
+  constraints.existential.push_back(implies_exprt(
+    guard, equal_exprt(array_pool.get_or_create_length(res), s_length)));
   return {from_integer(0, get_return_code_type()), std::move(constraints)};
 }
 
@@ -75,6 +77,7 @@ add_axioms_for_empty_string(const function_application_exprt &f)
 /// \param res: string expression for the result
 /// \param arg: expression of type string typet
 /// \param guard: condition under which `res` should be equal to arg
+/// \param array_pool: pool of arrays representing strings
 /// \return 0 if constraints were added, 1 if expression could not be handled
 ///   and no constraint was added. Expression we can handle are of the form
 ///   \f$ e := "<string constant>" | (expr)? e : e \f$
@@ -82,7 +85,8 @@ std::pair<exprt, string_constraintst> add_axioms_for_cprover_string(
   symbol_generatort &fresh_symbol,
   const array_string_exprt &res,
   const exprt &arg,
-  const exprt &guard)
+  const exprt &guard,
+  array_poolt &array_pool)
 {
   if(const auto if_expr = expr_try_dynamic_cast<if_exprt>(arg))
   {
@@ -90,12 +94,13 @@ std::pair<exprt, string_constraintst> add_axioms_for_cprover_string(
     const and_exprt guard_false(guard, not_exprt(if_expr->cond()));
     return combine_results(
       add_axioms_for_cprover_string(
-        fresh_symbol, res, if_expr->true_case(), guard_true),
+        fresh_symbol, res, if_expr->true_case(), guard_true, array_pool),
       add_axioms_for_cprover_string(
-        fresh_symbol, res, if_expr->false_case(), guard_false));
+        fresh_symbol, res, if_expr->false_case(), guard_false, array_pool));
   }
   else if(const auto constant_expr = expr_try_dynamic_cast<constant_exprt>(arg))
-    return add_axioms_for_constant(res, constant_expr->get_value(), guard);
+    return add_axioms_for_constant(
+      res, constant_expr->get_value(), array_pool, guard);
   else
     return {from_integer(1, get_return_code_type()), {}};
 }
@@ -119,5 +124,5 @@ std::pair<exprt, string_constraintst> add_axioms_from_literal(
   PRECONDITION(args.size() == 3); // Bad args to string literal?
   const array_string_exprt res = array_pool.find(args[1], args[0]);
   return add_axioms_for_cprover_string(
-    fresh_symbol, res, args[2], true_exprt());
+    fresh_symbol, res, args[2], true_exprt(), array_pool);
 }
diff --git a/src/solvers/strings/string_constraint_generator_float.cpp b/src/solvers/strings/string_constraint_generator_float.cpp
index 723d69168cd..7f207e25212 100644
--- a/src/solvers/strings/string_constraint_generator_float.cpp
+++ b/src/solvers/strings/string_constraint_generator_float.cpp
@@ -223,8 +223,8 @@ std::pair<exprt, string_constraintst> add_axioms_for_string_of_float(
   const mod_exprt fractional_part(shifted, max_non_exponent_notation);
   const array_string_exprt fractional_part_str =
     array_pool.fresh_string(index_type, char_type);
-  auto result1 =
-    add_axioms_for_fractional_part(fractional_part_str, fractional_part, 6);
+  auto result1 = add_axioms_for_fractional_part(
+    fractional_part_str, fractional_part, 6, array_pool);
 
   // The axiom added to convert to integer should always be satisfiable even
   // when the preconditions are not satisfied.
@@ -234,11 +234,11 @@ std::pair<exprt, string_constraintst> add_axioms_for_string_of_float(
   // part of the float.
   const array_string_exprt integer_part_str =
     array_pool.fresh_string(index_type, char_type);
-  auto result2 =
-    add_axioms_for_string_of_int(integer_part_str, integer_part, 8, ns);
+  auto result2 = add_axioms_for_string_of_int(
+    integer_part_str, integer_part, 8, ns, array_pool);
 
   auto result3 = add_axioms_for_concat(
-    fresh_symbol, res, integer_part_str, fractional_part_str);
+    fresh_symbol, res, integer_part_str, fractional_part_str, array_pool);
   merge(result3.second, std::move(result1.second));
   merge(result3.second, std::move(result2.second));
 
@@ -253,11 +253,13 @@ std::pair<exprt, string_constraintst> add_axioms_for_string_of_float(
 /// \param int_expr: an integer expression
 /// \param max_size: a maximal size for the string, this includes the
 ///   potential minus sign and therefore should be greater than 2
+/// \param array_pool: pool of arrays representing strings
 /// \return code 0 on success
 std::pair<exprt, string_constraintst> add_axioms_for_fractional_part(
   const array_string_exprt &res,
   const exprt &int_expr,
-  size_t max_size)
+  size_t max_size,
+  array_poolt &array_pool)
 {
   PRECONDITION(int_expr.type().id() == ID_signedbv);
   PRECONDITION(max_size >= 2);
@@ -279,7 +281,8 @@ std::pair<exprt, string_constraintst> add_axioms_for_fractional_part(
   // a3 : int_expr = sum_j 10^j (j < |res| ? res[j] - '0' : 0)
 
   const and_exprt a1(
-    greater_than(res.length(), 1), less_than_or_equal_to(res.length(), max));
+    greater_than(array_pool.get_or_create_length(res), 1),
+    less_than_or_equal_to(array_pool.get_or_create_length(res), max));
   constraints.existential.push_back(a1);
 
   equal_exprt starts_with_dot(res[0], from_integer('.', char_type));
@@ -292,7 +295,9 @@ std::pair<exprt, string_constraintst> add_axioms_for_fractional_part(
   {
     // after_end is |res| <= j
     binary_relation_exprt after_end(
-      res.length(), ID_le, from_integer(j, res.length_type()));
+      array_pool.get_or_create_length(res),
+      ID_le,
+      from_integer(j, res.length_type()));
     mult_exprt ten_sum(sum, ten);
 
     // sum = 10 * sum + after_end ? 0 : (res[j]-'0')
@@ -311,7 +316,9 @@ std::pair<exprt, string_constraintst> add_axioms_for_fractional_part(
     if(j > 1)
     {
       not_exprt no_trailing_zero(and_exprt(
-        equal_exprt(res.length(), from_integer(j + 1, res.length_type())),
+        equal_exprt(
+          array_pool.get_or_create_length(res),
+          from_integer(j + 1, res.length_type())),
         equal_exprt(res[j], zero_char)));
       digit_constraints.push_back(no_trailing_zero);
     }
@@ -462,7 +469,7 @@ std::pair<exprt, string_constraintst> add_axioms_from_float_scientific_notation(
   array_string_exprt string_expr_integer_part =
     array_pool.fresh_string(index_type, char_type);
   auto result1 = add_axioms_for_string_of_int(
-    string_expr_integer_part, dec_significand_int, 3, ns);
+    string_expr_integer_part, dec_significand_int, 3, ns, array_pool);
   minus_exprt fractional_part(
     dec_significand, floatbv_of_int_expr(dec_significand_int, float_spec));
 
@@ -482,7 +489,7 @@ std::pair<exprt, string_constraintst> add_axioms_from_float_scientific_notation(
   array_string_exprt string_fractional_part =
     array_pool.fresh_string(index_type, char_type);
   auto result2 = add_axioms_for_fractional_part(
-    string_fractional_part, fractional_part_shifted, 6);
+    string_fractional_part, fractional_part_shifted, 6, array_pool);
 
   // string_expr_with_fractional_part =
   //   concat(string_with_do, string_fractional_part)
@@ -492,29 +499,31 @@ std::pair<exprt, string_constraintst> add_axioms_from_float_scientific_notation(
     fresh_symbol,
     string_expr_with_fractional_part,
     string_expr_integer_part,
-    string_fractional_part);
+    string_fractional_part,
+    array_pool);
 
   // string_expr_with_E = concat(string_fraction, string_lit_E)
   const array_string_exprt stringE =
     array_pool.fresh_string(index_type, char_type);
-  auto result4 = add_axioms_for_constant(stringE, "E");
+  auto result4 = add_axioms_for_constant(stringE, "E", array_pool);
   const array_string_exprt string_expr_with_E =
     array_pool.fresh_string(index_type, char_type);
   auto result5 = add_axioms_for_concat(
     fresh_symbol,
     string_expr_with_E,
     string_expr_with_fractional_part,
-    stringE);
+    stringE,
+    array_pool);
 
   // exponent_string = string_of_int(decimal_exponent)
   const array_string_exprt exponent_string =
     array_pool.fresh_string(index_type, char_type);
-  auto result6 =
-    add_axioms_for_string_of_int(exponent_string, decimal_exponent, 3, ns);
+  auto result6 = add_axioms_for_string_of_int(
+    exponent_string, decimal_exponent, 3, ns, array_pool);
 
   // string_expr = concat(string_expr_with_E, exponent_string)
   auto result7 = add_axioms_for_concat(
-    fresh_symbol, res, string_expr_with_E, exponent_string);
+    fresh_symbol, res, string_expr_with_E, exponent_string, array_pool);
 
   const exprt return_code = maximum(
     result1.first,
diff --git a/src/solvers/strings/string_constraint_generator_format.cpp b/src/solvers/strings/string_constraint_generator_format.cpp
index a8c67b4858b..c3bb5b6aaf3 100644
--- a/src/solvers/strings/string_constraint_generator_format.cpp
+++ b/src/solvers/strings/string_constraint_generator_format.cpp
@@ -108,7 +108,7 @@ class format_elementt
     TEXT
   } format_typet;
 
-  explicit format_elementt(format_typet _type) : type(_type)
+  explicit format_elementt(format_typet _type) : type(_type), fstring("")
   {
   }
 
@@ -116,7 +116,7 @@ class format_elementt
   {
   }
 
-  explicit format_elementt(format_specifiert fs) : type(SPECIFIER)
+  explicit format_elementt(format_specifiert fs) : type(SPECIFIER), fstring("")
   {
     fspec.push_back(fs);
   }
@@ -186,6 +186,11 @@ static bool check_format_string(std::string s)
 }
 #endif
 
+static exprt format_arg_from_string(
+  const array_string_exprt &string,
+  const irep_idt &id,
+  array_poolt &array_pool);
+
 /// Helper function for parsing format strings.
 /// This follows the implementation in openJDK of the java.util.Formatter class:
 /// http://hg.openjdk.java.net/jdk7/jdk7/jdk/file/9b8c96f96a0f/src/share/classes/java/util/Formatter.java#l2660
@@ -205,8 +210,7 @@ static format_specifiert format_specifier_of_match(std::smatch &m)
   if(tT == "T")
     flag.push_back(format_specifiert::DATE_TIME_UPPER);
 
-  INVARIANT(
-    m[6].str().length() == 1, "format conversion should be one character");
+  INVARIANT(m[6].length() == 1, "format conversion should be one character");
   char conversion = m[6].str()[0];
 
   return format_specifiert(index, flag, width, precision, dt, conversion);
@@ -242,10 +246,11 @@ static std::vector<format_elementt> parse_format_string(std::string s)
 }
 
 /// Expression which is true when the string is equal to the literal "null"
-static exprt is_null(const array_string_exprt &string)
+static exprt is_null(const array_string_exprt &string, array_poolt &array_pool)
 {
   return and_exprt{
-    equal_exprt{string.length(), from_integer(4, string.length_type())},
+    equal_exprt{array_pool.get_or_create_length(string),
+                from_integer(4, string.length_type())},
     and_exprt{equal_exprt{string[0], from_integer('n', string[0].type())},
               equal_exprt{string[1], from_integer('u', string[0].type())},
               equal_exprt{string[2], from_integer('l', string[0].type())},
@@ -259,8 +264,7 @@ static exprt is_null(const array_string_exprt &string)
 /// on the format specifier.
 /// \param fresh_symbol: generator of fresh symbols
 /// \param fs: a format specifier
-/// \param get_arg: a function returning the possible value of the argument to
-///   format given their type.
+/// \param string_arg: format string from argument
 /// \param index_type: type for indexes in strings
 /// \param char_type: type of characters
 /// \param array_pool: pool of arrays representing strings
@@ -271,7 +275,7 @@ static std::pair<array_string_exprt, string_constraintst>
 add_axioms_for_format_specifier(
   symbol_generatort &fresh_symbol,
   const format_specifiert &fs,
-  const std::function<exprt(const irep_idt &)> &get_arg,
+  const array_string_exprt &string_arg,
   const typet &index_type,
   const typet &char_type,
   array_poolt &array_pool,
@@ -284,33 +288,50 @@ add_axioms_for_format_specifier(
   switch(fs.conversion)
   {
   case format_specifiert::DECIMAL_INTEGER:
-    return_code = add_axioms_for_string_of_int(res, get_arg(ID_int), 0, ns);
+    return_code = add_axioms_for_string_of_int(
+      res,
+      format_arg_from_string(string_arg, ID_int, array_pool),
+      0,
+      ns,
+      array_pool);
     return {res, std::move(return_code.second)};
   case format_specifiert::HEXADECIMAL_INTEGER:
     return_code = add_axioms_for_string_of_int_with_radix(
-      res, get_arg(ID_int), from_integer(16, index_type), 16, ns);
+      res,
+      format_arg_from_string(string_arg, ID_int, array_pool),
+      from_integer(16, index_type),
+      16,
+      ns,
+      array_pool);
     return {res, std::move(return_code.second)};
   case format_specifiert::SCIENTIFIC:
     return_code = add_axioms_from_float_scientific_notation(
-        fresh_symbol, res, get_arg(ID_float), array_pool, ns);
+      fresh_symbol,
+      res,
+      format_arg_from_string(string_arg, ID_float, array_pool),
+      array_pool,
+      ns);
     return {res, std::move(return_code.second)};
   case format_specifiert::DECIMAL_FLOAT:
     return_code = add_axioms_for_string_of_float(
-        fresh_symbol, res, get_arg(ID_float), array_pool, ns);
+      fresh_symbol,
+      res,
+      format_arg_from_string(string_arg, ID_float, array_pool),
+      array_pool,
+      ns);
     return {res, std::move(return_code.second)};
   case format_specifiert::CHARACTER:
   {
-    exprt arg_string = get_arg(ID_char);
+    exprt arg_string = format_arg_from_string(string_arg, ID_char, array_pool);
     array_string_exprt &string_expr = to_array_string_expr(arg_string);
     // In the case the arg is null, the result will be equal to "null" and
     // and otherwise we just take the 4th character of the string.
-    const exprt is_null_literal = is_null(string_expr);
-    constraints.existential.push_back(equal_exprt{
-      res.length(),
-      if_exprt{
-        is_null_literal,
-        from_integer(4, index_type),
-        from_integer(1, index_type)}});
+    const exprt is_null_literal = is_null(string_expr, array_pool);
+    constraints.existential.push_back(
+      equal_exprt{array_pool.get_or_create_length(res),
+                  if_exprt{is_null_literal,
+                           from_integer(4, index_type),
+                           from_integer(1, index_type)}});
     constraints.existential.push_back(implies_exprt{
       is_null_literal,
       and_exprt{
@@ -324,23 +345,31 @@ add_axioms_for_format_specifier(
     return {res, constraints};
   }
   case format_specifiert::BOOLEAN:
-    return_code = add_axioms_from_bool(res, get_arg(ID_boolean));
+    return_code = add_axioms_from_bool(
+      res,
+      format_arg_from_string(string_arg, ID_boolean, array_pool),
+      array_pool);
     return {res, std::move(return_code.second)};
   case format_specifiert::STRING:
   {
-    const exprt arg_string = get_arg("string_expr");
+    const exprt arg_string = string_arg;
     const array_string_exprt string_expr = to_array_string_expr(arg_string);
     return {std::move(string_expr), {}};
   }
   case format_specifiert::HASHCODE:
-    return_code = add_axioms_for_string_of_int(res, get_arg("hashcode"), 0, ns);
+    return_code = add_axioms_for_string_of_int(
+      res,
+      format_arg_from_string(string_arg, "hashcode", array_pool),
+      0,
+      ns,
+      array_pool);
     return {res, std::move(return_code.second)};
   case format_specifiert::LINE_SEPARATOR:
     // TODO: the constant should depend on the system: System.lineSeparator()
-    return_code = add_axioms_for_constant(res, "\n");
+    return_code = add_axioms_for_constant(res, "\n", array_pool);
     return {res, std::move(return_code.second)};
   case format_specifiert::PERCENT_SIGN:
-    return_code = add_axioms_for_constant(res, "%");
+    return_code = add_axioms_for_constant(res, "%", array_pool);
     return {res, std::move(return_code.second)};
   case format_specifiert::SCIENTIFIC_UPPER:
   case format_specifiert::GENERAL_UPPER:
@@ -356,7 +385,7 @@ add_axioms_for_format_specifier(
     auto format_specifier_result = add_axioms_for_format_specifier(
       fresh_symbol,
       fs_lower,
-      get_arg,
+      string_arg,
       index_type,
       char_type,
       array_pool,
@@ -366,7 +395,7 @@ add_axioms_for_format_specifier(
     const exprt return_code_upper_case =
       fresh_symbol("return_code_upper_case", get_return_code_type());
     const string_to_upper_case_builtin_functiont upper_case_function(
-      return_code_upper_case, res, format_specifier_result.first);
+      return_code_upper_case, res, format_specifier_result.first, array_pool);
     auto upper_case_constraints = upper_case_function.constraints(fresh_symbol);
     merge(upper_case_constraints, std::move(format_specifier_result.second));
     return {res, std::move(upper_case_constraints)};
@@ -392,7 +421,9 @@ add_axioms_for_format_specifier(
 /// \p id should be one of: string_expr, int, char, boolean, float.
 /// The primitive values are expected to all be encoded using 4 characters.
 static exprt format_arg_from_string(
-  const array_string_exprt &string, const irep_idt &id)
+  const array_string_exprt &string,
+  const irep_idt &id,
+  array_poolt &array_pool)
 {
   if(id == "string_expr")
     return string;
@@ -420,13 +451,14 @@ static exprt format_arg_from_string(
   {
     // We assume the string has length exactly 4, if it is "null" return false
     // and otherwise ignore the first 3 and return (bool)string.content[3]
-    return if_exprt{
-      is_null(string), false_exprt{}, typecast_exprt{string[3], bool_typet()}};
+    return if_exprt{is_null(string, array_pool),
+                    false_exprt{},
+                    typecast_exprt{string[3], bool_typet()}};
   }
   if(id == ID_float)
   {
     // Deserialize an int and cast to float
-    const exprt as_int = format_arg_from_string(string, ID_int);
+    const exprt as_int = format_arg_from_string(string, ID_int, array_pool);
     return typecast_exprt{as_int, floatbv_typet{}};
   }
   UNHANDLED_CASE;
@@ -458,13 +490,13 @@ std::pair<exprt, string_constraintst> add_axioms_for_format(
   const typet &char_type = res.content().type().subtype();
   const typet &index_type = res.length_type();
 
+  array_string_exprt string_arg;
+
   for(const format_elementt &fe : format_strings)
   {
     if(fe.is_format_specifier())
     {
       const format_specifiert &fs = fe.get_format_specifier();
-      std::function<exprt(const irep_idt &)> get_arg =
-          [](const irep_idt &) -> exprt { UNREACHABLE; };
 
       if(
         fs.conversion != format_specifiert::PERCENT_SIGN &&
@@ -492,16 +524,13 @@ std::pair<exprt, string_constraintst> add_axioms_for_format(
         INVARIANT(
           is_refined_string_type(arg.type()),
           "arguments of format should be strings");
-        const array_string_exprt string_arg = get_string_expr(array_pool, arg);
-        get_arg = [string_arg](const irep_idt &id) {
-          return format_arg_from_string(string_arg, id);
-        };
+        string_arg = get_string_expr(array_pool, arg);
       }
 
       auto result = add_axioms_for_format_specifier(
         fresh_symbol,
         fs,
-        get_arg,
+        string_arg,
         index_type,
         char_type,
         array_pool,
@@ -514,8 +543,8 @@ std::pair<exprt, string_constraintst> add_axioms_for_format(
     {
       const array_string_exprt str =
         array_pool.fresh_string(index_type, char_type);
-      auto result =
-        add_axioms_for_constant(str, fe.get_format_text().get_content());
+      auto result = add_axioms_for_constant(
+        str, fe.get_format_text().get_content(), array_pool);
       merge(constraints, result.second);
       intermediary_strings.push_back(str);
     }
@@ -525,8 +554,8 @@ std::pair<exprt, string_constraintst> add_axioms_for_format(
 
   if(intermediary_strings.empty())
   {
-    constraints.existential.push_back(
-      equal_exprt(res.length(), from_integer(0, index_type)));
+    constraints.existential.push_back(equal_exprt(
+      array_pool.get_or_create_length(res), from_integer(0, index_type)));
     return {return_code, constraints};
   }
 
@@ -536,7 +565,12 @@ std::pair<exprt, string_constraintst> add_axioms_for_format(
   {
     // Copy the first string
     auto result = add_axioms_for_substring(
-      fresh_symbol, res, str, from_integer(0, index_type), str.length());
+      fresh_symbol,
+      res,
+      str,
+      from_integer(0, index_type),
+      array_pool.get_or_create_length(str),
+      array_pool);
     merge(constraints, std::move(result.second));
     return {result.first, std::move(constraints)};
   }
@@ -547,14 +581,15 @@ std::pair<exprt, string_constraintst> add_axioms_for_format(
     const array_string_exprt &intermediary = intermediary_strings[i];
     const array_string_exprt fresh =
       array_pool.fresh_string(index_type, char_type);
-    auto result = add_axioms_for_concat(fresh_symbol, fresh, str, intermediary);
+    auto result =
+      add_axioms_for_concat(fresh_symbol, fresh, str, intermediary, array_pool);
     return_code = maximum(return_code, result.first);
     merge(constraints, std::move(result.second));
     str = fresh;
   }
 
-  auto result =
-    add_axioms_for_concat(fresh_symbol, res, str, intermediary_strings.back());
+  auto result = add_axioms_for_concat(
+    fresh_symbol, res, str, intermediary_strings.back(), array_pool);
   merge(constraints, std::move(result.second));
   return {maximum(result.first, return_code), std::move(constraints)};
 }
@@ -604,10 +639,12 @@ std::pair<exprt, string_constraintst> add_axioms_for_format(
     array_pool.find(f.arguments()[1], f.arguments()[0]);
   const array_string_exprt s1 = get_string_expr(array_pool, f.arguments()[2]);
 
-  if(s1.length().id() == ID_constant && s1.content().id() == ID_array)
+  if(
+    array_pool.get_or_create_length(s1).id() == ID_constant &&
+    s1.content().id() == ID_array)
   {
-    const auto length =
-      numeric_cast_v<std::size_t>(to_constant_expr(s1.length()));
+    const auto length = numeric_cast_v<std::size_t>(
+      to_constant_expr(array_pool.get_or_create_length(s1)));
     std::string s =
       utf16_constant_array_to_java(to_array_expr(s1.content()), length);
     // List of arguments after s
diff --git a/src/solvers/strings/string_constraint_generator_indexof.cpp b/src/solvers/strings/string_constraint_generator_indexof.cpp
index 56b04d8c049..8f37d5e2f1f 100644
--- a/src/solvers/strings/string_constraint_generator_indexof.cpp
+++ b/src/solvers/strings/string_constraint_generator_indexof.cpp
@@ -34,12 +34,14 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com
 /// \param str: an array of characters expression
 /// \param c: a character expression
 /// \param from_index: an integer expression
+/// \param array_pool: pool of arrays representing strings
 /// \return integer expression `index`
 std::pair<exprt, string_constraintst> add_axioms_for_index_of(
   symbol_generatort &fresh_symbol,
   const array_string_exprt &str,
   const exprt &c,
-  const exprt &from_index)
+  const exprt &from_index,
+  array_poolt &array_pool)
 {
   string_constraintst constraints;
   const typet &index_type = str.length_type();
@@ -49,7 +51,7 @@ std::pair<exprt, string_constraintst> add_axioms_for_index_of(
   exprt minus1 = from_integer(-1, index_type);
   and_exprt a1(
     binary_relation_exprt(index, ID_ge, minus1),
-    binary_relation_exprt(index, ID_lt, str.length()));
+    binary_relation_exprt(index, ID_lt, array_pool.get_or_create_length(str)));
   constraints.existential.push_back(a1);
 
   equal_exprt a2(not_exprt(contains), equal_exprt(index, minus1));
@@ -76,7 +78,7 @@ std::pair<exprt, string_constraintst> add_axioms_for_index_of(
   string_constraintt a5(
     m,
     lower_bound,
-    zero_if_negative(str.length()),
+    zero_if_negative(array_pool.get_or_create_length(str)),
     implies_exprt(not_exprt(contains), not_exprt(equal_exprt(str[m], c))));
   constraints.universal.push_back(a5);
 
@@ -106,13 +108,15 @@ std::pair<exprt, string_constraintst> add_axioms_for_index_of(
 /// \param haystack: an array of character expression
 /// \param needle: an array of character expression
 /// \param from_index: an integer expression
+/// \param array_pool: pool of arrays representing strings
 /// \return integer expression `index` representing the first index of `needle`
 ///   in `haystack`
 std::pair<exprt, string_constraintst> add_axioms_for_index_of_string(
   symbol_generatort &fresh_symbol,
   const array_string_exprt &haystack,
   const array_string_exprt &needle,
-  const exprt &from_index)
+  const exprt &from_index,
+  array_poolt &array_pool)
 {
   string_constraintst constraints;
   const typet &index_type = haystack.length_type();
@@ -124,7 +128,11 @@ std::pair<exprt, string_constraintst> add_axioms_for_index_of_string(
     and_exprt(
       binary_relation_exprt(from_index, ID_le, offset),
       binary_relation_exprt(
-        offset, ID_le, minus_exprt(haystack.length(), needle.length()))));
+        offset,
+        ID_le,
+        minus_exprt(
+          array_pool.get_or_create_length(haystack),
+          array_pool.get_or_create_length(needle)))));
   constraints.existential.push_back(a1);
 
   equal_exprt a2(
@@ -134,36 +142,40 @@ std::pair<exprt, string_constraintst> add_axioms_for_index_of_string(
   symbol_exprt qvar = fresh_symbol("QA_index_of_string", index_type);
   string_constraintt a3(
     qvar,
-    zero_if_negative(needle.length()),
+    zero_if_negative(array_pool.get_or_create_length(needle)),
     implies_exprt(
       contains, equal_exprt(haystack[plus_exprt(qvar, offset)], needle[qvar])));
   constraints.universal.push_back(a3);
 
   // string_not contains_constraintt are formulas of the form:
   // forall x in [lb,ub[. p(x) => exists y in [lb,ub[. s1[x+y] != s2[y]
-  const string_not_contains_constraintt a4 = {from_index,
-                                              offset,
-                                              contains,
-                                              from_integer(0, index_type),
-                                              needle.length(),
-                                              haystack,
-                                              needle};
+  const string_not_contains_constraintt a4 = {
+    from_index,
+    offset,
+    contains,
+    from_integer(0, index_type),
+    array_pool.get_or_create_length(needle),
+    haystack,
+    needle};
   constraints.not_contains.push_back(a4);
 
   const string_not_contains_constraintt a5 = {
     from_index,
     plus_exprt( // Add 1 for inclusive upper bound.
-      minus_exprt(haystack.length(), needle.length()),
+      minus_exprt(
+        array_pool.get_or_create_length(haystack),
+        array_pool.get_or_create_length(needle)),
       from_integer(1, index_type)),
     not_exprt(contains),
     from_integer(0, index_type),
-    needle.length(),
+    array_pool.get_or_create_length(needle),
     haystack,
     needle};
   constraints.not_contains.push_back(a5);
 
   const implies_exprt a6(
-    equal_exprt(needle.length(), from_integer(0, index_type)),
+    equal_exprt(
+      array_pool.get_or_create_length(needle), from_integer(0, index_type)),
     equal_exprt(offset, from_index));
   constraints.existential.push_back(a6);
 
@@ -199,13 +211,15 @@ std::pair<exprt, string_constraintst> add_axioms_for_index_of_string(
 /// \param haystack: an array of characters expression
 /// \param needle: an array of characters expression
 /// \param from_index: integer expression
+/// \param array_pool: pool of arrays representing strings
 /// \return integer expression `index` representing the last index of `needle`
 ///         in `haystack` before or at `from_index`, or -1 if there is none
 std::pair<exprt, string_constraintst> add_axioms_for_last_index_of_string(
   symbol_generatort &fresh_symbol,
   const array_string_exprt &haystack,
   const array_string_exprt &needle,
-  const exprt &from_index)
+  const exprt &from_index,
+  array_poolt &array_pool)
 {
   string_constraintst constraints;
   const typet &index_type = haystack.length_type();
@@ -217,7 +231,11 @@ std::pair<exprt, string_constraintst> add_axioms_for_last_index_of_string(
     and_exprt(
       binary_relation_exprt(from_integer(-1, index_type), ID_le, offset),
       binary_relation_exprt(
-        offset, ID_le, minus_exprt(haystack.length(), needle.length())),
+        offset,
+        ID_le,
+        minus_exprt(
+          array_pool.get_or_create_length(haystack),
+          array_pool.get_or_create_length(needle))),
       binary_relation_exprt(offset, ID_le, from_index)));
   constraints.existential.push_back(a1);
 
@@ -228,11 +246,15 @@ std::pair<exprt, string_constraintst> add_axioms_for_last_index_of_string(
   symbol_exprt qvar = fresh_symbol("QA_index_of_string", index_type);
   equal_exprt constr3(haystack[plus_exprt(qvar, offset)], needle[qvar]);
   const string_constraintt a3(
-    qvar, zero_if_negative(needle.length()), implies_exprt(contains, constr3));
+    qvar,
+    zero_if_negative(array_pool.get_or_create_length(needle)),
+    implies_exprt(contains, constr3));
   constraints.universal.push_back(a3);
 
   // end_index is min(from_index, |str| - |substring|)
-  minus_exprt length_diff(haystack.length(), needle.length());
+  minus_exprt length_diff(
+    array_pool.get_or_create_length(haystack),
+    array_pool.get_or_create_length(needle));
   if_exprt end_index(
     binary_relation_exprt(from_index, ID_le, length_diff),
     from_index,
@@ -243,7 +265,7 @@ std::pair<exprt, string_constraintst> add_axioms_for_last_index_of_string(
     plus_exprt(end_index, from_integer(1, index_type)),
     contains,
     from_integer(0, index_type),
-    needle.length(),
+    array_pool.get_or_create_length(needle),
     haystack,
     needle};
   constraints.not_contains.push_back(a4);
@@ -253,13 +275,14 @@ std::pair<exprt, string_constraintst> add_axioms_for_last_index_of_string(
     plus_exprt(end_index, from_integer(1, index_type)),
     not_exprt(contains),
     from_integer(0, index_type),
-    needle.length(),
+    array_pool.get_or_create_length(needle),
     haystack,
     needle};
   constraints.not_contains.push_back(a5);
 
   const implies_exprt a6(
-    equal_exprt(needle.length(), from_integer(0, index_type)),
+    equal_exprt(
+      array_pool.get_or_create_length(needle), from_integer(0, index_type)),
     equal_exprt(offset, from_index));
   constraints.existential.push_back(a6);
 
@@ -270,9 +293,9 @@ std::pair<exprt, string_constraintst> add_axioms_for_last_index_of_string(
 ///
 /// If the target is a character:
 // NOLINTNEXTLINE
-/// \copybrief add_axioms_for_index_of(symbol_generatort &fresh_symbol, const array_string_exprt&,const exprt&,const exprt&)
+/// \copybrief add_axioms_for_index_of(symbol_generatort &fresh_symbol, const array_string_exprt&,const exprt&,const exprt&, array_poolt &)
 // NOLINTNEXTLINE
-/// \link add_axioms_for_index_of(symbol_generatort &fresh_symbol, const array_string_exprt&,const exprt&,const exprt&)
+/// \link add_axioms_for_index_of(symbol_generatort &fresh_symbol, const array_string_exprt&,const exprt&,const exprt&, array_poolt &)
 /// (More...) \endlink
 ///
 /// If the target is a refined_string:
@@ -304,7 +327,7 @@ std::pair<exprt, string_constraintst> add_axioms_for_index_of(
   if(c.type().id() == ID_unsignedbv || c.type().id() == ID_signedbv)
   {
     return add_axioms_for_index_of(
-      fresh_symbol, str, typecast_exprt(c, char_type), from_index);
+      fresh_symbol, str, typecast_exprt(c, char_type), from_index, array_pool);
   }
   else
   {
@@ -314,7 +337,8 @@ std::pair<exprt, string_constraintst> add_axioms_for_index_of(
         "c can only be a (un)signedbv or a refined "
         "string and the (un)signedbv case is already handled"));
     array_string_exprt sub = get_string_expr(array_pool, c);
-    return add_axioms_for_index_of_string(fresh_symbol, str, sub, from_index);
+    return add_axioms_for_index_of_string(
+      fresh_symbol, str, sub, from_index, array_pool);
   }
 }
 
@@ -340,13 +364,15 @@ std::pair<exprt, string_constraintst> add_axioms_for_index_of(
 /// \param str: an array of characters expression
 /// \param c: a character expression
 /// \param from_index: an integer expression
+/// \param array_pool: pool of arrays representing strings
 /// \return integer expression `index` representing the last index of `needle`
 ///   in `haystack` before or at `from_index`, or `-1` if there is none
 std::pair<exprt, string_constraintst> add_axioms_for_last_index_of(
   symbol_generatort &fresh_symbol,
   const array_string_exprt &str,
   const exprt &c,
-  const exprt &from_index)
+  const exprt &from_index,
+  array_poolt &array_pool)
 {
   string_constraintst constraints;
   const typet &index_type = str.length_type();
@@ -357,7 +383,7 @@ std::pair<exprt, string_constraintst> add_axioms_for_last_index_of(
   const and_exprt a1(
     binary_relation_exprt(index, ID_ge, minus1),
     binary_relation_exprt(index, ID_le, from_index),
-    binary_relation_exprt(index, ID_lt, str.length()));
+    binary_relation_exprt(index, ID_lt, array_pool.get_or_create_length(str)));
   constraints.existential.push_back(a1);
 
   const notequal_exprt a2(contains, equal_exprt(index, minus1));
@@ -369,9 +395,10 @@ std::pair<exprt, string_constraintst> add_axioms_for_last_index_of(
   const exprt index1 = from_integer(1, index_type);
   const plus_exprt from_index_plus_one(from_index, index1);
   const if_exprt end_index(
-    binary_relation_exprt(from_index_plus_one, ID_le, str.length()),
+    binary_relation_exprt(
+      from_index_plus_one, ID_le, array_pool.get_or_create_length(str)),
     from_index_plus_one,
-    str.length());
+    array_pool.get_or_create_length(str));
 
   const symbol_exprt n = fresh_symbol("QA_last_index_of1", index_type);
   const string_constraintt a4(
@@ -395,9 +422,9 @@ std::pair<exprt, string_constraintst> add_axioms_for_last_index_of(
 ///
 /// If the target is a character:
 // NOLINTNEXTLINE
-/// \copybrief add_axioms_for_last_index_of(symbol_generatort &fresh_symbol, const array_string_exprt&,const exprt&,const exprt&)
+/// \copybrief add_axioms_for_last_index_of(symbol_generatort &fresh_symbol, const array_string_exprt&,const exprt&,const exprt&, array_poolt &)
 // NOLINTNEXTLINE
-/// \link add_axioms_for_last_index_of(symbol_generatort &fresh_symbol, const array_string_exprt&,const exprt&,const exprt&)
+/// \link add_axioms_for_last_index_of(symbol_generatort &fresh_symbol, const array_string_exprt&,const exprt&,const exprt&, array_poolt &)
 ///   (More...) \endlink
 ///
 /// If the target is a refined_string:
@@ -424,17 +451,18 @@ std::pair<exprt, string_constraintst> add_axioms_for_last_index_of(
   const typet &char_type = str.content().type().subtype();
   PRECONDITION(f.type() == index_type);
 
-  const exprt from_index = args.size() == 2 ? str.length() : args[2];
+  const exprt from_index =
+    args.size() == 2 ? array_pool.get_or_create_length(str) : args[2];
 
   if(c.type().id() == ID_unsignedbv || c.type().id() == ID_signedbv)
   {
     return add_axioms_for_last_index_of(
-      fresh_symbol, str, typecast_exprt(c, char_type), from_index);
+      fresh_symbol, str, typecast_exprt(c, char_type), from_index, array_pool);
   }
   else
   {
     const array_string_exprt sub = get_string_expr(array_pool, c);
     return add_axioms_for_last_index_of_string(
-      fresh_symbol, str, sub, from_index);
+      fresh_symbol, str, sub, from_index, array_pool);
   }
 }
diff --git a/src/solvers/strings/string_constraint_generator_insert.cpp b/src/solvers/strings/string_constraint_generator_insert.cpp
index 3df28acbc3d..6615481c20a 100644
--- a/src/solvers/strings/string_constraint_generator_insert.cpp
+++ b/src/solvers/strings/string_constraint_generator_insert.cpp
@@ -29,6 +29,7 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com
 /// \param s1: array of characters expression
 /// \param s2: array of characters expression
 /// \param offset: integer expression
+/// \param array_pool: pool of arrays representing strings
 /// \return an expression expression which is different from zero if there is
 ///   an exception to signal
 std::pair<exprt, string_constraintst> add_axioms_for_insert(
@@ -36,17 +37,20 @@ std::pair<exprt, string_constraintst> add_axioms_for_insert(
   const array_string_exprt &res,
   const array_string_exprt &s1,
   const array_string_exprt &s2,
-  const exprt &offset)
+  const exprt &offset,
+  array_poolt &array_pool)
 {
   PRECONDITION(offset.type() == s1.length_type());
 
   string_constraintst constraints;
   const typet &index_type = s1.length_type();
-  const exprt offset1 =
-    maximum(from_integer(0, index_type), minimum(s1.length(), offset));
+  const exprt offset1 = maximum(
+    from_integer(0, index_type),
+    minimum(array_pool.get_or_create_length(s1), offset));
 
   // Axiom 1.
-  constraints.existential.push_back(length_constraint_for_insert(res, s1, s2));
+  constraints.existential.push_back(
+    length_constraint_for_insert(res, s1, s2, array_pool));
 
   // Axiom 2.
   constraints.universal.push_back([&] { // NOLINT
@@ -59,7 +63,7 @@ std::pair<exprt, string_constraintst> add_axioms_for_insert(
     const symbol_exprt i = fresh_symbol("QA_insert2", index_type);
     return string_constraintt(
       i,
-      zero_if_negative(s2.length()),
+      zero_if_negative(array_pool.get_or_create_length(s2)),
       equal_exprt(res[plus_exprt(i, offset1)], s2[i]));
   }());
 
@@ -69,8 +73,9 @@ std::pair<exprt, string_constraintst> add_axioms_for_insert(
     return string_constraintt(
       i,
       offset1,
-      zero_if_negative(s1.length()),
-      equal_exprt(res[plus_exprt(i, s2.length())], s1[i]));
+      zero_if_negative(array_pool.get_or_create_length(s1)),
+      equal_exprt(
+        res[plus_exprt(i, array_pool.get_or_create_length(s2))], s1[i]));
   }());
 
   return {from_integer(0, get_return_code_type()), std::move(constraints)};
@@ -81,17 +86,22 @@ std::pair<exprt, string_constraintst> add_axioms_for_insert(
 exprt length_constraint_for_insert(
   const array_string_exprt &res,
   const array_string_exprt &s1,
-  const array_string_exprt &s2)
+  const array_string_exprt &s2,
+  array_poolt &array_pool)
 {
-  return equal_exprt(res.length(), plus_exprt(s1.length(), s2.length()));
+  return equal_exprt(
+    array_pool.get_or_create_length(res),
+    plus_exprt(
+      array_pool.get_or_create_length(s1),
+      array_pool.get_or_create_length(s2)));
 }
 
 /// Insertion of a string in another at a specific index
 ///
 // NOLINTNEXTLINE
-/// \copybrief add_axioms_for_insert(symbol_generatort &fresh_symbol, const array_string_exprt &, const array_string_exprt &, const array_string_exprt &, const exprt &)
+/// \copybrief add_axioms_for_insert(symbol_generatort &fresh_symbol, const array_string_exprt &, const array_string_exprt &, const array_string_exprt &, const exprt &, array_poolt &)
 // NOLINTNEXTLINE
-/// \link add_axioms_for_insert(symbol_generatort &fresh_symbol, const array_string_exprt&,const array_string_exprt&,const array_string_exprt&,const exprt&)
+/// \link add_axioms_for_insert(symbol_generatort &fresh_symbol, const array_string_exprt&,const array_string_exprt&,const array_string_exprt&,const exprt&,array_poolt &)
 ///   (More...) \endlink
 ///
 /// If `start` and `end` arguments are given then `substring(s2, start, end)`
@@ -122,12 +132,14 @@ std::pair<exprt, string_constraintst> add_axioms_for_insert(
     const array_string_exprt substring =
       array_pool.fresh_string(index_type, char_type);
     return combine_results(
-      add_axioms_for_substring(fresh_symbol, substring, s2, start, end),
-      add_axioms_for_insert(fresh_symbol, res, s1, substring, offset));
+      add_axioms_for_substring(
+        fresh_symbol, substring, s2, start, end, array_pool),
+      add_axioms_for_insert(
+        fresh_symbol, res, s1, substring, offset, array_pool));
   }
   else // 5 arguments
   {
-    return add_axioms_for_insert(fresh_symbol, res, s1, s2, offset);
+    return add_axioms_for_insert(fresh_symbol, res, s1, s2, offset, array_pool);
   }
 }
 
@@ -155,8 +167,8 @@ std::pair<exprt, string_constraintst> add_axioms_for_insert_int(
   const typet &char_type = s1.content().type().subtype();
   const array_string_exprt s2 = array_pool.fresh_string(index_type, char_type);
   return combine_results(
-    add_axioms_for_string_of_int(s2, f.arguments()[4], 0, ns),
-    add_axioms_for_insert(fresh_symbol, res, s1, s2, offset));
+    add_axioms_for_string_of_int(s2, f.arguments()[4], 0, ns, array_pool),
+    add_axioms_for_insert(fresh_symbol, res, s1, s2, offset, array_pool));
 }
 
 /// add axioms corresponding to the StringBuilder.insert(Z) java function
@@ -181,8 +193,8 @@ std::pair<exprt, string_constraintst> add_axioms_for_insert_bool(
   const typet &char_type = s1.content().type().subtype();
   const array_string_exprt s2 = array_pool.fresh_string(index_type, char_type);
   return combine_results(
-    add_axioms_from_bool(s2, f.arguments()[4]),
-    add_axioms_for_insert(fresh_symbol, res, s1, s2, offset));
+    add_axioms_from_bool(s2, f.arguments()[4], array_pool),
+    add_axioms_for_insert(fresh_symbol, res, s1, s2, offset, array_pool));
 }
 
 /// Add axioms corresponding to the StringBuilder.insert(C) java function
@@ -206,8 +218,8 @@ std::pair<exprt, string_constraintst> add_axioms_for_insert_char(
   const typet &char_type = s1.content().type().subtype();
   const array_string_exprt s2 = array_pool.fresh_string(index_type, char_type);
   return combine_results(
-    add_axioms_from_char(s2, f.arguments()[4]),
-    add_axioms_for_insert(fresh_symbol, res, s1, s2, offset));
+    add_axioms_from_char(s2, f.arguments()[4], array_pool),
+    add_axioms_for_insert(fresh_symbol, res, s1, s2, offset, array_pool));
 }
 
 /// add axioms corresponding to the StringBuilder.insert(D) java function
@@ -236,7 +248,7 @@ std::pair<exprt, string_constraintst> add_axioms_for_insert_double(
   return combine_results(
     add_axioms_for_string_of_float(
       fresh_symbol, s2, f.arguments()[4], array_pool, ns),
-    add_axioms_for_insert(fresh_symbol, res, s1, s2, offset));
+    add_axioms_for_insert(fresh_symbol, res, s1, s2, offset, array_pool));
 }
 
 /// Add axioms corresponding to the StringBuilder.insert(F) java function
diff --git a/src/solvers/strings/string_constraint_generator_main.cpp b/src/solvers/strings/string_constraint_generator_main.cpp
index ae184de1f5d..93cbe3a6ebb 100644
--- a/src/solvers/strings/string_constraint_generator_main.cpp
+++ b/src/solvers/strings/string_constraint_generator_main.cpp
@@ -85,7 +85,7 @@ exprt string_constraint_generatort::associate_length_to_array(
   array_string_exprt array_expr = to_array_string_expr(f.arguments()[0]);
   const exprt &new_length = f.arguments()[1];
 
-  const auto &length = array_pool.get_length(array_expr);
+  const auto &length = array_pool.get_or_create_length(array_expr);
   constraints.existential.push_back(equal_exprt(length, new_length));
   return from_integer(0, f.type());
 }
@@ -125,6 +125,7 @@ void merge(string_constraintst &result, string_constraintst other)
 /// \param char_set: a string of the form "<low_char>-<high_char>" where
 ///   `<low_char>` and `<high_char>` are two characters, which represents the
 ///   set of characters that are between `low_char` and `high_char`.
+/// \param array_pool: pool of arrays representing strings
 /// \return a string expression that is linked to the argument through axioms
 ///   that are added to the list
 string_constraintst add_constraint_on_characters(
@@ -132,7 +133,8 @@ string_constraintst add_constraint_on_characters(
   const array_string_exprt &s,
   const exprt &start,
   const exprt &end,
-  const std::string &char_set)
+  const std::string &char_set,
+  array_poolt &array_pool)
 {
   // Parse char_set
   PRECONDITION(char_set.length() == 3);
@@ -177,9 +179,10 @@ std::pair<exprt, string_constraintst> add_axioms_for_constrain_characters(
   const irep_idt &char_set_string = to_constant_expr(args[2]).get_value();
   const exprt &start =
     args.size() >= 4 ? args[3] : from_integer(0, s.length_type());
-  const exprt &end = args.size() >= 5 ? args[4] : s.length();
+  const exprt &end =
+    args.size() >= 5 ? args[4] : array_pool.get_or_create_length(s);
   auto constraints = add_constraint_on_characters(
-    fresh_symbol, s, start, end, char_set_string.c_str());
+    fresh_symbol, s, start, end, char_set_string.c_str(), array_pool);
   return {from_integer(0, get_return_code_type()), std::move(constraints)};
 }
 
@@ -339,9 +342,10 @@ std::pair<exprt, string_constraintst> add_axioms_for_copy(
   const array_string_exprt str = get_string_expr(array_pool, args[2]);
   const typet &index_type = str.length_type();
   const exprt offset = args.size() == 3 ? from_integer(0, index_type) : args[3];
-  const exprt count = args.size() == 3 ? str.length() : args[4];
+  const exprt count =
+    args.size() == 3 ? array_pool.get_or_create_length(str) : args[4];
   return add_axioms_for_substring(
-    fresh_symbol, res, str, offset, plus_exprt(offset, count));
+    fresh_symbol, res, str, offset, plus_exprt(offset, count), array_pool);
 }
 
 /// Length of a string
@@ -356,7 +360,7 @@ std::pair<exprt, string_constraintst> add_axioms_for_length(
 {
   PRECONDITION(f.arguments().size() == 1);
   const array_string_exprt str = get_string_expr(array_pool, f.arguments()[0]);
-  return {str.length(), {}};
+  return {array_pool.get_or_create_length(str), {}};
 }
 
 /// \param x: an expression
diff --git a/src/solvers/strings/string_constraint_generator_testing.cpp b/src/solvers/strings/string_constraint_generator_testing.cpp
index 68f991e30c4..1be420293ce 100644
--- a/src/solvers/strings/string_constraint_generator_testing.cpp
+++ b/src/solvers/strings/string_constraint_generator_testing.cpp
@@ -34,21 +34,25 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com
 /// \param prefix: an array of characters
 /// \param str: an array of characters
 /// \param offset: an integer
+/// \param array_pool: pool of arrays representing strings
 /// \return Boolean expression `isprefix`
 std::pair<exprt, string_constraintst> add_axioms_for_is_prefix(
   symbol_generatort &fresh_symbol,
   const array_string_exprt &prefix,
   const array_string_exprt &str,
-  const exprt &offset)
+  const exprt &offset,
+  array_poolt &array_pool)
 {
   string_constraintst constraints;
   const symbol_exprt isprefix = fresh_symbol("isprefix");
   const typet &index_type = str.length_type();
   const exprt offset_within_bounds = and_exprt(
     binary_relation_exprt(offset, ID_ge, from_integer(0, offset.type())),
-    binary_relation_exprt(offset, ID_le, str.length()),
+    binary_relation_exprt(offset, ID_le, array_pool.get_or_create_length(str)),
     binary_relation_exprt(
-      minus_exprt(str.length(), offset), ID_ge, prefix.length()));
+      minus_exprt(array_pool.get_or_create_length(str), offset),
+      ID_ge,
+      array_pool.get_or_create_length(prefix)));
 
   // Axiom 1.
   constraints.existential.push_back(
@@ -60,7 +64,10 @@ std::pair<exprt, string_constraintst> add_axioms_for_is_prefix(
     const exprt body = implies_exprt(
       isprefix, equal_exprt(str[plus_exprt(qvar, offset)], prefix[qvar]));
     return string_constraintt(
-      qvar, maximum(from_integer(0, index_type), prefix.length()), body);
+      qvar,
+      maximum(
+        from_integer(0, index_type), array_pool.get_or_create_length(prefix)),
+      body);
   }());
 
   // Axiom 3.
@@ -68,12 +75,13 @@ std::pair<exprt, string_constraintst> add_axioms_for_is_prefix(
     const exprt witness = fresh_symbol("witness_not_isprefix", index_type);
     const exprt strings_differ_at_witness = and_exprt(
       is_positive(witness),
-      greater_than(prefix.length(), witness),
+      greater_than(array_pool.get_or_create_length(prefix), witness),
       notequal_exprt(str[plus_exprt(witness, offset)], prefix[witness]));
     const exprt s1_does_not_start_with_s0 = or_exprt(
       not_exprt(offset_within_bounds),
-      not_exprt(
-        greater_or_equal_to(str.length(), plus_exprt(prefix.length(), offset))),
+      not_exprt(greater_or_equal_to(
+        array_pool.get_or_create_length(str),
+        plus_exprt(array_pool.get_or_create_length(prefix), offset))),
       strings_differ_at_witness);
     return implies_exprt(not_exprt(isprefix), s1_does_not_start_with_s0);
   }());
@@ -113,7 +121,8 @@ std::pair<exprt, string_constraintst> add_axioms_for_is_prefix(
     get_string_expr(array_pool, args[swap_arguments ? 0u : 1u]);
   const exprt offset =
     args.size() == 2 ? from_integer(0, s0.length_type()) : args[2];
-  auto pair = add_axioms_for_is_prefix(fresh_symbol, s0, s1, offset);
+  auto pair =
+    add_axioms_for_is_prefix(fresh_symbol, s0, s1, offset, array_pool);
   return {typecast_exprt(pair.first, f.type()), std::move(pair.second)};
 }
 
@@ -139,8 +148,9 @@ std::pair<exprt, string_constraintst> add_axioms_for_is_empty(
   symbol_exprt is_empty = fresh_symbol("is_empty");
   array_string_exprt s0 = get_string_expr(array_pool, f.arguments()[0]);
   string_constraintst constraints;
-  constraints.existential = {implies_exprt(is_empty, equal_to(s0.length(), 0)),
-                             implies_exprt(equal_to(s0.length(), 0), is_empty)};
+  constraints.existential = {
+    implies_exprt(is_empty, equal_to(array_pool.get_or_create_length(s0), 0)),
+    implies_exprt(equal_to(array_pool.get_or_create_length(s0), 0), is_empty)};
   return {typecast_exprt(is_empty, f.type()), std::move(constraints)};
 }
 
@@ -187,26 +197,42 @@ std::pair<exprt, string_constraintst> add_axioms_for_is_suffix(
     get_string_expr(array_pool, args[swap_arguments ? 0u : 1u]);
   const typet &index_type = s0.length_type();
 
-  implies_exprt a1(issuffix, greater_or_equal_to(s1.length(), s0.length()));
+  implies_exprt a1(
+    issuffix,
+    greater_or_equal_to(
+      array_pool.get_or_create_length(s1),
+      array_pool.get_or_create_length(s0)));
   constraints.existential.push_back(a1);
 
   symbol_exprt qvar = fresh_symbol("QA_suffix", index_type);
-  const plus_exprt qvar_shifted(qvar, minus_exprt(s1.length(), s0.length()));
+  const plus_exprt qvar_shifted(
+    qvar,
+    minus_exprt(
+      array_pool.get_or_create_length(s1),
+      array_pool.get_or_create_length(s0)));
   string_constraintt a2(
     qvar,
-    zero_if_negative(s0.length()),
+    zero_if_negative(array_pool.get_or_create_length(s0)),
     implies_exprt(issuffix, equal_exprt(s0[qvar], s1[qvar_shifted])));
   constraints.universal.push_back(a2);
 
   symbol_exprt witness = fresh_symbol("witness_not_suffix", index_type);
-  const plus_exprt shifted(witness, minus_exprt(s1.length(), s0.length()));
+  const plus_exprt shifted(
+    witness,
+    minus_exprt(
+      array_pool.get_or_create_length(s1),
+      array_pool.get_or_create_length(s0)));
   or_exprt constr3(
     and_exprt(
-      greater_than(s0.length(), s1.length()),
+      greater_than(
+        array_pool.get_or_create_length(s0),
+        array_pool.get_or_create_length(s1)),
       equal_exprt(witness, from_integer(-1, index_type))),
     and_exprt(
       notequal_exprt(s0[witness], s1[shifted]),
-      and_exprt(greater_than(s0.length(), witness), is_positive(witness))));
+      and_exprt(
+        greater_than(array_pool.get_or_create_length(s0), witness),
+        is_positive(witness))));
   implies_exprt a3(not_exprt(issuffix), constr3);
 
   constraints.existential.push_back(a3);
@@ -248,10 +274,14 @@ std::pair<exprt, string_constraintst> add_axioms_for_contains(
   const symbol_exprt startpos = fresh_symbol("startpos_contains", index_type);
 
   const implies_exprt a1(
-    contains, greater_or_equal_to(s0.length(), s1.length()));
+    contains,
+    greater_or_equal_to(
+      array_pool.get_or_create_length(s0),
+      array_pool.get_or_create_length(s1)));
   constraints.existential.push_back(a1);
 
-  minus_exprt length_diff(s0.length(), s1.length());
+  minus_exprt length_diff(
+    array_pool.get_or_create_length(s0), array_pool.get_or_create_length(s1));
   and_exprt bounds(
     is_positive(startpos), binary_relation_exprt(startpos, ID_le, length_diff));
   implies_exprt a2(contains, bounds);
@@ -265,7 +295,7 @@ std::pair<exprt, string_constraintst> add_axioms_for_contains(
   const plus_exprt qvar_shifted(qvar, startpos);
   string_constraintt a4(
     qvar,
-    zero_if_negative(s1.length()),
+    zero_if_negative(array_pool.get_or_create_length(s1)),
     implies_exprt(contains, equal_exprt(s1[qvar], s0[qvar_shifted])));
   constraints.universal.push_back(a4);
 
@@ -273,9 +303,12 @@ std::pair<exprt, string_constraintst> add_axioms_for_contains(
     from_integer(0, index_type),
     plus_exprt(from_integer(1, index_type), length_diff),
     and_exprt(
-      not_exprt(contains), greater_or_equal_to(s0.length(), s1.length())),
+      not_exprt(contains),
+      greater_or_equal_to(
+        array_pool.get_or_create_length(s0),
+        array_pool.get_or_create_length(s1))),
     from_integer(0, index_type),
-    s1.length(),
+    array_pool.get_or_create_length(s1),
     s0,
     s1};
   constraints.not_contains.push_back(a5);
diff --git a/src/solvers/strings/string_constraint_generator_transformation.cpp b/src/solvers/strings/string_constraint_generator_transformation.cpp
index aaa04a8a0b1..92ee1e7e639 100644
--- a/src/solvers/strings/string_constraint_generator_transformation.cpp
+++ b/src/solvers/strings/string_constraint_generator_transformation.cpp
@@ -54,20 +54,21 @@ std::pair<exprt, string_constraintst> add_axioms_for_set_length(
   // a2 : forall i< min(|s1|, k) .res[i] = s1[i]
   // a3 : forall |s1| <= i < |res|. res[i] = 0
 
-  constraints.existential.push_back(equal_to(res.length(), k));
+  constraints.existential.push_back(
+    equal_to(array_pool.get_or_create_length(res), k));
 
   const symbol_exprt idx = fresh_symbol("QA_index_set_length", index_type);
   const string_constraintt a2(
     idx,
-    zero_if_negative(minimum(s1.length(), k)),
+    zero_if_negative(minimum(array_pool.get_or_create_length(s1), k)),
     equal_exprt(s1[idx], res[idx]));
   constraints.universal.push_back(a2);
 
   symbol_exprt idx2 = fresh_symbol("QA_index_set_length2", index_type);
   string_constraintt a3(
     idx2,
-    zero_if_negative(s1.length()),
-    zero_if_negative(res.length()),
+    zero_if_negative(array_pool.get_or_create_length(s1)),
+    zero_if_negative(array_pool.get_or_create_length(res)),
     equal_exprt(res[idx2], from_integer(0, char_type)));
   constraints.universal.push_back(a3);
 
@@ -77,9 +78,9 @@ std::pair<exprt, string_constraintst> add_axioms_for_set_length(
 /// Substring of a string between two indices
 ///
 // NOLINTNEXTLINE
-/// \copybrief add_axioms_for_substring(symbol_generatort &fresh_symbol, const array_string_exprt &res, const array_string_exprt &str, const exprt &start, const exprt &end)
+/// \copybrief add_axioms_for_substring(symbol_generatort &fresh_symbol, const array_string_exprt &res, const array_string_exprt &str, const exprt &start, const exprt &end, array_poolt &)
 // NOLINTNEXTLINE
-/// \link string_constraint_generatort::add_axioms_for_substring(symbol_generatort &fresh_symbol, const array_string_exprt &res, const array_string_exprt &str, const exprt &start, const exprt &end)
+/// \link string_constraint_generatort::add_axioms_for_substring(symbol_generatort &fresh_symbol, const array_string_exprt &res, const array_string_exprt &str, const exprt &start, const exprt &end, array_poolt &)
 ///   (More...) \endlink
 /// \warning The specification may not be correct for the case where the string
 /// is shorter than the end index
@@ -102,8 +103,9 @@ std::pair<exprt, string_constraintst> add_axioms_for_substring(
   const array_string_exprt str = get_string_expr(array_pool, args[2]);
   const array_string_exprt res = array_pool.find(args[1], args[0]);
   const exprt &i = args[3];
-  const exprt j = args.size() == 5 ? args[4] : str.length();
-  return add_axioms_for_substring(fresh_symbol, res, str, i, j);
+  const exprt j =
+    args.size() == 5 ? args[4] : array_pool.get_or_create_length(str);
+  return add_axioms_for_substring(fresh_symbol, res, str, i, j, array_pool);
 }
 
 /// Add axioms ensuring that `res` corresponds to the substring of `str`
@@ -120,13 +122,15 @@ std::pair<exprt, string_constraintst> add_axioms_for_substring(
 /// \param str: array of characters expression
 /// \param start: integer expression
 /// \param end: integer expression
+/// \param array_pool: pool of arrays representing strings
 /// \return integer expression equal to zero
 std::pair<exprt, string_constraintst> add_axioms_for_substring(
   symbol_generatort &fresh_symbol,
   const array_string_exprt &res,
   const array_string_exprt &str,
   const exprt &start,
-  const exprt &end)
+  const exprt &end,
+  array_poolt &array_pool)
 {
   const typet &index_type = str.length_type();
   PRECONDITION(start.type() == index_type);
@@ -134,18 +138,19 @@ std::pair<exprt, string_constraintst> add_axioms_for_substring(
 
   string_constraintst constraints;
   const exprt start1 = maximum(start, from_integer(0, start.type()));
-  const exprt end1 = maximum(minimum(end, str.length()), start1);
+  const exprt end1 =
+    maximum(minimum(end, array_pool.get_or_create_length(str)), start1);
 
   // Axiom 1.
-  constraints.existential.push_back(
-    equal_exprt(res.length(), minus_exprt(end1, start1)));
+  constraints.existential.push_back(equal_exprt(
+    array_pool.get_or_create_length(res), minus_exprt(end1, start1)));
 
   // Axiom 2.
   constraints.universal.push_back([&] {
     const symbol_exprt idx = fresh_symbol("QA_index_substring", index_type);
     return string_constraintt(
       idx,
-      zero_if_negative(res.length()),
+      zero_if_negative(array_pool.get_or_create_length(res)),
       equal_exprt(res[idx], str[plus_exprt(start1, idx)]));
   }());
 
@@ -196,20 +201,23 @@ std::pair<exprt, string_constraintst> add_axioms_for_trim(
   const exprt space_char = from_integer(' ', char_type);
 
   // Axiom 1.
-  constraints.existential.push_back(
-    greater_or_equal_to(str.length(), plus_exprt(idx, res.length())));
+  constraints.existential.push_back(greater_or_equal_to(
+    array_pool.get_or_create_length(str),
+    plus_exprt(idx, array_pool.get_or_create_length(res))));
 
   binary_relation_exprt a2(idx, ID_ge, from_integer(0, index_type));
   constraints.existential.push_back(a2);
 
-  const exprt a3 = greater_or_equal_to(str.length(), idx);
+  const exprt a3 =
+    greater_or_equal_to(array_pool.get_or_create_length(str), idx);
   constraints.existential.push_back(a3);
 
-  const exprt a4 =
-    greater_or_equal_to(res.length(), from_integer(0, index_type));
+  const exprt a4 = greater_or_equal_to(
+    array_pool.get_or_create_length(res), from_integer(0, index_type));
   constraints.existential.push_back(a4);
 
-  const exprt a5 = less_than_or_equal_to(res.length(), str.length());
+  const exprt a5 = less_than_or_equal_to(
+    array_pool.get_or_create_length(res), array_pool.get_or_create_length(str));
   constraints.existential.push_back(a5);
 
   symbol_exprt n = fresh_symbol("QA_index_trim", index_type);
@@ -220,25 +228,33 @@ std::pair<exprt, string_constraintst> add_axioms_for_trim(
   // Axiom 7.
   constraints.universal.push_back([&] {
     const symbol_exprt n2 = fresh_symbol("QA_index_trim2", index_type);
-    const minus_exprt bound(minus_exprt(str.length(), idx), res.length());
+    const minus_exprt bound(
+      minus_exprt(array_pool.get_or_create_length(str), idx),
+      array_pool.get_or_create_length(res));
     const binary_relation_exprt eqn2(
-      str[plus_exprt(idx, plus_exprt(res.length(), n2))], ID_le, space_char);
+      str[plus_exprt(
+        idx, plus_exprt(array_pool.get_or_create_length(res), n2))],
+      ID_le,
+      space_char);
     return string_constraintt(n2, zero_if_negative(bound), eqn2);
   }());
 
   symbol_exprt n3 = fresh_symbol("QA_index_trim3", index_type);
   equal_exprt eqn3(res[n3], str[plus_exprt(n3, idx)]);
-  string_constraintt a8(n3, zero_if_negative(res.length()), eqn3);
+  string_constraintt a8(
+    n3, zero_if_negative(array_pool.get_or_create_length(res)), eqn3);
   constraints.universal.push_back(a8);
 
   // Axiom 9.
   constraints.existential.push_back([&] {
     const plus_exprt index_before(
-      idx, minus_exprt(res.length(), from_integer(1, index_type)));
+      idx,
+      minus_exprt(
+        array_pool.get_or_create_length(res), from_integer(1, index_type)));
     const binary_relation_exprt no_space_before(
       str[index_before], ID_gt, space_char);
     return or_exprt(
-      equal_exprt(idx, str.length()),
+      equal_exprt(idx, array_pool.get_or_create_length(str)),
       and_exprt(
         binary_relation_exprt(str[idx], ID_gt, space_char), no_space_before));
   }());
@@ -254,11 +270,13 @@ std::pair<exprt, string_constraintst> add_axioms_for_trim(
 /// \param get_string_expr: Function that yields an array_string_exprt
 ///   corresponding to either `expr1` or `expr2`, for the case where they are
 ///   not primitive chars.
+/// \param array_pool: pool of arrays representing strings
 /// \return Optional pair of two expressions
 static optionalt<std::pair<exprt, exprt>> to_char_pair(
   exprt expr1,
   exprt expr2,
-  std::function<array_string_exprt(const exprt &)> get_string_expr)
+  std::function<array_string_exprt(const exprt &)> get_string_expr,
+  array_poolt &array_pool)
 {
   if(
     (expr1.type().id() == ID_unsignedbv || expr1.type().id() == ID_char) &&
@@ -266,8 +284,10 @@ static optionalt<std::pair<exprt, exprt>> to_char_pair(
     return std::make_pair(expr1, expr2);
   const auto expr1_str = get_string_expr(expr1);
   const auto expr2_str = get_string_expr(expr2);
-  const auto expr1_length = numeric_cast<std::size_t>(expr1_str.length());
-  const auto expr2_length = numeric_cast<std::size_t>(expr2_str.length());
+  const auto expr1_length =
+    numeric_cast<std::size_t>(array_pool.get_or_create_length(expr1_str));
+  const auto expr2_length =
+    numeric_cast<std::size_t>(array_pool.get_or_create_length(expr2_str));
   if(expr1_length && expr2_length && *expr1_length == 1 && *expr2_length == 1)
     return std::make_pair(exprt(expr1_str[0]), exprt(expr2_str[0]));
   return {};
@@ -304,15 +324,18 @@ std::pair<exprt, string_constraintst> add_axioms_for_replace(
   array_string_exprt str = get_string_expr(array_pool, f.arguments()[2]);
   array_string_exprt res = array_pool.find(f.arguments()[1], f.arguments()[0]);
   if(
-    const auto maybe_chars =
-      to_char_pair(f.arguments()[3], f.arguments()[4], [&](const exprt &e) {
-        return get_string_expr(array_pool, e);
-      }))
+    const auto maybe_chars = to_char_pair(
+      f.arguments()[3],
+      f.arguments()[4],
+      [&](const exprt &e) { return get_string_expr(array_pool, e); },
+      array_pool))
   {
     const auto old_char = maybe_chars->first;
     const auto new_char = maybe_chars->second;
 
-    constraints.existential.push_back(equal_exprt(res.length(), str.length()));
+    constraints.existential.push_back(equal_exprt(
+      array_pool.get_or_create_length(res),
+      array_pool.get_or_create_length(str)));
 
     symbol_exprt qvar = fresh_symbol("QA_replace", str.length_type());
     implies_exprt case1(
@@ -321,7 +344,9 @@ std::pair<exprt, string_constraintst> add_axioms_for_replace(
       not_exprt(equal_exprt(str[qvar], old_char)),
       equal_exprt(res[qvar], str[qvar]));
     string_constraintt a2(
-      qvar, zero_if_negative(res.length()), and_exprt(case1, case2));
+      qvar,
+      zero_if_negative(array_pool.get_or_create_length(res)),
+      and_exprt(case1, case2));
     constraints.universal.push_back(a2);
     return {from_integer(0, f.type()), std::move(constraints)};
   }
@@ -387,10 +412,21 @@ std::pair<exprt, string_constraintst> add_axioms_for_delete(
     array_pool.fresh_string(index_type, char_type);
   return combine_results(
     add_axioms_for_substring(
-      fresh_symbol, sub1, str, from_integer(0, str.length_type()), start),
+      fresh_symbol,
+      sub1,
+      str,
+      from_integer(0, str.length_type()),
+      start,
+      array_pool),
     combine_results(
-      add_axioms_for_substring(fresh_symbol, sub2, str, end, str.length()),
-      add_axioms_for_concat(fresh_symbol, res, sub1, sub2)));
+      add_axioms_for_substring(
+        fresh_symbol,
+        sub2,
+        str,
+        end,
+        array_pool.get_or_create_length(str),
+        array_pool),
+      add_axioms_for_concat(fresh_symbol, res, sub1, sub2, array_pool)));
 }
 
 /// Remove a portion of a string
diff --git a/src/solvers/strings/string_constraint_generator_valueof.cpp b/src/solvers/strings/string_constraint_generator_valueof.cpp
index 2c99717629e..ff55d56e57b 100644
--- a/src/solvers/strings/string_constraint_generator_valueof.cpp
+++ b/src/solvers/strings/string_constraint_generator_valueof.cpp
@@ -53,9 +53,10 @@ std::pair<exprt, string_constraintst> add_axioms_from_long(
     array_pool.find(f.arguments()[1], f.arguments()[0]);
   if(f.arguments().size() == 4)
     return add_axioms_for_string_of_int_with_radix(
-      res, f.arguments()[2], f.arguments()[3], 0, ns);
+      res, f.arguments()[2], f.arguments()[3], 0, ns, array_pool);
   else
-    return add_axioms_for_string_of_int(res, f.arguments()[2], 0, ns);
+    return add_axioms_for_string_of_int(
+      res, f.arguments()[2], 0, ns, array_pool);
 }
 
 /// Add axioms corresponding to the String.valueOf(Z) java function.
@@ -71,7 +72,7 @@ std::pair<exprt, string_constraintst> add_axioms_from_bool(
   PRECONDITION(f.arguments().size() == 3);
   const array_string_exprt res =
     array_pool.find(f.arguments()[1], f.arguments()[0]);
-  return add_axioms_from_bool(res, f.arguments()[2]);
+  return add_axioms_from_bool(res, f.arguments()[2], array_pool);
 }
 
 /// Add axioms stating that the returned string equals "true" when the Boolean
@@ -79,10 +80,13 @@ std::pair<exprt, string_constraintst> add_axioms_from_bool(
 /// \deprecated This is Java specific and should be implemented in Java instead
 /// \param res: string expression for the result
 /// \param b: Boolean expression
+/// \param array_pool: pool of arrays representing strings
 /// \return code 0 on success
 DEPRECATED(SINCE(2017, 10, 5, "Java specific, should be implemented in Java"))
-std::pair<exprt, string_constraintst>
-add_axioms_from_bool(const array_string_exprt &res, const exprt &b)
+std::pair<exprt, string_constraintst> add_axioms_from_bool(
+  const array_string_exprt &res,
+  const exprt &b,
+  array_poolt &array_pool)
 {
   const typet &char_type = res.content().type().subtype();
   PRECONDITION(b.type() == bool_typet() || b.type().id() == ID_c_bool);
@@ -96,7 +100,8 @@ add_axioms_from_bool(const array_string_exprt &res, const exprt &b)
   // a4 : forall i < |"false"|. !eq => res[i]="false"[i]
 
   std::string str_true = "true";
-  const implies_exprt a1(eq, equal_to(res.length(), str_true.length()));
+  const implies_exprt a1(
+    eq, equal_to(array_pool.get_or_create_length(res), str_true.length()));
   constraints.existential.push_back(a1);
 
   for(std::size_t i = 0; i < str_true.length(); i++)
@@ -108,7 +113,8 @@ add_axioms_from_bool(const array_string_exprt &res, const exprt &b)
 
   std::string str_false = "false";
   const implies_exprt a3(
-    not_exprt(eq), equal_to(res.length(), str_false.length()));
+    not_exprt(eq),
+    equal_to(array_pool.get_or_create_length(res), str_false.length()));
   constraints.existential.push_back(a3);
 
   for(std::size_t i = 0; i < str_false.length(); i++)
@@ -129,16 +135,18 @@ add_axioms_from_bool(const array_string_exprt &res, const exprt &b)
 /// \param max_size: a maximal size for the string representation (default 0,
 ///   which is interpreted to mean "as large as is needed for this type")
 /// \param ns: namespace
+/// \param array_pool: pool of arrays representing strings
 /// \return code 0 on success
 std::pair<exprt, string_constraintst> add_axioms_for_string_of_int(
   const array_string_exprt &res,
   const exprt &input_int,
   size_t max_size,
-  const namespacet &ns)
+  const namespacet &ns,
+  array_poolt &array_pool)
 {
   const constant_exprt radix = from_integer(10, input_int.type());
   return add_axioms_for_string_of_int_with_radix(
-    res, input_int, radix, max_size, ns);
+    res, input_int, radix, max_size, ns, array_pool);
 }
 
 /// Add axioms enforcing that the string corresponds to the result
@@ -150,13 +158,15 @@ std::pair<exprt, string_constraintst> add_axioms_for_string_of_int(
 /// \param max_size: a maximal size for the string representation (default 0,
 ///   which is interpreted to mean "as large as is needed for this type")
 /// \param ns: namespace
+/// \param array_pool: pool of arrays representing strings
 /// \return code 0 on success
 std::pair<exprt, string_constraintst> add_axioms_for_string_of_int_with_radix(
   const array_string_exprt &res,
   const exprt &input_int,
   const exprt &radix,
   size_t max_size,
-  const namespacet &ns)
+  const namespacet &ns,
+  array_poolt &array_pool)
 {
   PRECONDITION(max_size < std::numeric_limits<size_t>::max());
   const typet &type = input_int.type();
@@ -179,7 +189,7 @@ std::pair<exprt, string_constraintst> add_axioms_for_string_of_int_with_radix(
   const bool strict_formatting = true;
 
   auto result1 = add_axioms_for_correct_number_format(
-    res, radix_as_char, radix_ul, max_size, strict_formatting);
+    res, radix_as_char, radix_ul, max_size, strict_formatting, array_pool);
   auto result2 = add_axioms_for_characters_in_integer_string(
     input_int,
     type,
@@ -187,7 +197,8 @@ std::pair<exprt, string_constraintst> add_axioms_for_string_of_int_with_radix(
     res,
     max_size,
     radix_input_type,
-    radix_ul);
+    radix_ul,
+    array_pool);
   merge(result2, std::move(result1));
   return {from_integer(0, get_return_code_type()), std::move(result2)};
 }
@@ -212,10 +223,13 @@ static exprt int_of_hex_char(const exprt &chr)
 /// \deprecated use add_axioms_from_int_with_radix instead
 /// \param res: string expression for the result
 /// \param i: an integer argument
+/// \param array_pool: pool of arrays representing strings
 /// \return code 0 on success
 DEPRECATED(SINCE(2017, 10, 5, "use add_axioms_for_string_of_int_with_radix"))
-std::pair<exprt, string_constraintst>
-add_axioms_from_int_hex(const array_string_exprt &res, const exprt &i)
+std::pair<exprt, string_constraintst> add_axioms_from_int_hex(
+  const array_string_exprt &res,
+  const exprt &i,
+  array_poolt &array_pool)
 {
   const typet &type = i.type();
   PRECONDITION(type.id() == ID_signedbv);
@@ -231,8 +245,8 @@ add_axioms_from_int_hex(const array_string_exprt &res, const exprt &i)
 
   size_t max_size = 8;
   constraints.existential.push_back(and_exprt(
-    greater_than(res.length(), 0),
-    less_than_or_equal_to(res.length(), max_size)));
+    greater_than(array_pool.get_or_create_length(res), 0),
+    less_than_or_equal_to(array_pool.get_or_create_length(res), max_size)));
 
   for(size_t size = 1; size <= max_size; size++)
   {
@@ -255,7 +269,8 @@ add_axioms_from_int_hex(const array_string_exprt &res, const exprt &i)
       all_numbers = and_exprt(all_numbers, is_number);
     }
 
-    const equal_exprt premise = equal_to(res.length(), size);
+    const equal_exprt premise =
+      equal_to(array_pool.get_or_create_length(res), size);
     constraints.existential.push_back(
       implies_exprt(premise, and_exprt(equal_exprt(i, sum), all_numbers)));
 
@@ -278,15 +293,15 @@ std::pair<exprt, string_constraintst> add_axioms_from_int_hex(
   PRECONDITION(f.arguments().size() == 3);
   const array_string_exprt res =
     array_pool.find(f.arguments()[1], f.arguments()[0]);
-  return add_axioms_from_int_hex(res, f.arguments()[2]);
+  return add_axioms_from_int_hex(res, f.arguments()[2], array_pool);
 }
 
 /// Conversion from char to string
 ///
 // NOLINTNEXTLINE
-/// \copybrief add_axioms_from_char(const array_string_exprt &res, const exprt &c)
+/// \copybrief add_axioms_from_char(const array_string_exprt &res, const exprt &c, array_poolt &)
 // NOLINTNEXTLINE
-/// \link add_axioms_from_char(const array_string_exprt &res, const exprt &c)
+/// \link add_axioms_from_char(const array_string_exprt &res, const exprt &c, array_poolt &)
 ///   (More...) \endlink
 /// \param f: function application with arguments integer `|res|`, character
 ///   pointer `&res[0]` and character `c`
@@ -299,7 +314,7 @@ std::pair<exprt, string_constraintst> add_axioms_from_char(
   PRECONDITION(f.arguments().size() == 3);
   const array_string_exprt res =
     array_pool.find(f.arguments()[1], f.arguments()[0]);
-  return add_axioms_from_char(res, f.arguments()[2]);
+  return add_axioms_from_char(res, f.arguments()[2], array_pool);
 }
 
 /// Add axiom stating that string `res` has length 1 and the character
@@ -308,13 +323,16 @@ std::pair<exprt, string_constraintst> add_axioms_from_char(
 /// This axiom is: \f$ |{\tt res}| = 1 \land {\tt res}[0] = {\tt c} \f$.
 /// \param res: array of characters expression
 /// \param c: character expression
+/// \param array_pool: pool of arrays representing strings
 /// \return code 0 on success
-std::pair<exprt, string_constraintst>
-add_axioms_from_char(const array_string_exprt &res, const exprt &c)
+std::pair<exprt, string_constraintst> add_axioms_from_char(
+  const array_string_exprt &res,
+  const exprt &c,
+  array_poolt &array_pool)
 {
   string_constraintst constraints;
-  constraints.existential = {
-    and_exprt(equal_exprt(res[0], c), equal_to(res.length(), 1))};
+  constraints.existential = {and_exprt(
+    equal_exprt(res[0], c), equal_to(array_pool.get_or_create_length(res), 1))};
   return {from_integer(0, get_return_code_type()), std::move(constraints)};
 }
 
@@ -328,12 +346,14 @@ add_axioms_from_char(const array_string_exprt &res, const exprt &c)
 /// \param max_size: maximum number of characters
 /// \param strict_formatting: if true, don't allow a leading plus, redundant
 ///   zeros or upper case letters
+/// \param array_pool: pool of arrays representing strings
 string_constraintst add_axioms_for_correct_number_format(
   const array_string_exprt &str,
   const exprt &radix_as_char,
   const unsigned long radix_ul,
   const std::size_t max_size,
-  const bool strict_formatting)
+  const bool strict_formatting,
+  array_poolt &array_pool)
 {
   string_constraintst constraints;
   const typet &char_type = str.content().type().subtype();
@@ -346,8 +366,8 @@ string_constraintst add_axioms_for_correct_number_format(
     is_digit_with_radix(chr, strict_formatting, radix_as_char, radix_ul);
 
   // |str| > 0
-  const exprt non_empty =
-    greater_or_equal_to(str.length(), from_integer(1, index_type));
+  const exprt non_empty = greater_or_equal_to(
+    array_pool.get_or_create_length(str), from_integer(1, index_type));
   constraints.existential.push_back(non_empty);
 
   if(strict_formatting)
@@ -367,21 +387,24 @@ string_constraintst add_axioms_for_correct_number_format(
   // str[0]='+' or '-' ==> |str| > 1
   const implies_exprt contains_digit(
     or_exprt(starts_with_minus, starts_with_plus),
-    greater_or_equal_to(str.length(), from_integer(2, index_type)));
+    greater_or_equal_to(
+      array_pool.get_or_create_length(str), from_integer(2, index_type)));
   constraints.existential.push_back(contains_digit);
 
   // |str| <= max_size
   constraints.existential.push_back(
-    less_than_or_equal_to(str.length(), max_size));
+    less_than_or_equal_to(array_pool.get_or_create_length(str), max_size));
 
   // forall 1 <= i < |str| . is_digit_with_radix(str[i], radix)
   // We unfold the above because we know that it will be used for all i up to
-  // str.length(), and str.length() <= max_size
+  // |str|, and |str| <= max_size.
   for(std::size_t index = 1; index < max_size; ++index)
   {
     /// index < length => is_digit_with_radix(str[index], radix)
     const implies_exprt character_at_index_is_digit(
-      greater_or_equal_to(str.length(), from_integer(index + 1, index_type)),
+      greater_or_equal_to(
+        array_pool.get_or_create_length(str),
+        from_integer(index + 1, index_type)),
       is_digit_with_radix(
         str[index], strict_formatting, radix_as_char, radix_ul));
     constraints.existential.push_back(character_at_index_is_digit);
@@ -394,7 +417,8 @@ string_constraintst add_axioms_for_correct_number_format(
     // no_leading_zero : str[0] = '0' => |str| = 1
     const implies_exprt no_leading_zero(
       equal_exprt(chr, zero_char),
-      equal_to(str.length(), from_integer(1, index_type)));
+      equal_to(
+        array_pool.get_or_create_length(str), from_integer(1, index_type)));
     constraints.existential.push_back(no_leading_zero);
 
     // no_leading_zero_after_minus : str[0]='-' => str[1]!='0'
@@ -417,6 +441,7 @@ string_constraintst add_axioms_for_correct_number_format(
 /// \param radix: the radix, with the same type as input_int
 /// \param radix_ul: the radix as an unsigned long, or 0 if that can't be
 ///   determined
+/// \param array_pool: pool of arrays representing strings
 string_constraintst add_axioms_for_characters_in_integer_string(
   const exprt &input_int,
   const typet &type,
@@ -424,7 +449,8 @@ string_constraintst add_axioms_for_characters_in_integer_string(
   const array_string_exprt &str,
   const std::size_t max_string_length,
   const exprt &radix,
-  const unsigned long radix_ul)
+  const unsigned long radix_ul,
+  array_poolt &array_pool)
 {
   string_constraintst constraints;
   const typet &char_type = str.content().type().subtype();
@@ -439,8 +465,9 @@ string_constraintst add_axioms_for_characters_in_integer_string(
   /// Deal with size==1 case separately. There are axioms from
   /// add_axioms_for_correct_number_format which say that the string must
   /// contain at least one digit, so we don't have to worry about "+" or "-".
-  constraints.existential.push_back(
-    implies_exprt(equal_to(str.length(), 1), equal_exprt(input_int, sum)));
+  constraints.existential.push_back(implies_exprt(
+    equal_to(array_pool.get_or_create_length(str), 1),
+    equal_exprt(input_int, sum)));
 
   for(size_t size = 2; size <= max_string_length; size++)
   {
@@ -478,7 +505,8 @@ string_constraintst add_axioms_for_characters_in_integer_string(
     }
     sum = new_sum;
 
-    const equal_exprt premise = equal_to(str.length(), size);
+    const equal_exprt premise =
+      equal_to(array_pool.get_or_create_length(str), size);
 
     if(!digit_constraints.empty())
     {
@@ -541,7 +569,12 @@ std::pair<exprt, string_constraintst> add_axioms_for_parse_int(
   /// \note the only thing stopping us from taking longer strings with many
   /// leading zeros is the axioms for correct number format
   auto constraints1 = add_axioms_for_correct_number_format(
-    str, radix_as_char, radix_ul, max_string_length, strict_formatting);
+    str,
+    radix_as_char,
+    radix_ul,
+    max_string_length,
+    strict_formatting,
+    array_pool);
 
   auto constraints2 = add_axioms_for_characters_in_integer_string(
     input_int,
@@ -550,7 +583,8 @@ std::pair<exprt, string_constraintst> add_axioms_for_parse_int(
     str,
     max_string_length,
     radix,
-    radix_ul);
+    radix_ul,
+    array_pool);
   merge(constraints2, std::move(constraints1));
 
   return {input_int, std::move(constraints2)};
diff --git a/src/solvers/strings/string_refinement.cpp b/src/solvers/strings/string_refinement.cpp
index fd2db24e300..8753c7f59a8 100644
--- a/src/solvers/strings/string_refinement.cpp
+++ b/src/solvers/strings/string_refinement.cpp
@@ -107,7 +107,8 @@ static optionalt<exprt> get_array(
   const std::function<exprt(const exprt &)> &super_get,
   const namespacet &ns,
   messaget::mstreamt &stream,
-  const array_string_exprt &arr);
+  const array_string_exprt &arr,
+  const array_poolt &array_pool);
 
 static exprt substitute_array_access(
   const index_exprt &index_expr,
@@ -740,10 +741,11 @@ decision_proceduret::resultt string_refinementt::dec_solve()
     add_lemma(lemma);
 
   // All generated strings should have non-negative length
-  for(const auto &string : generator.array_pool.created_strings())
+  for(const auto &pair : generator.array_pool.created_strings())
   {
-    add_lemma(greater_or_equal_to(
-      string.length(), from_integer(0, string.length_type())));
+    exprt length = generator.array_pool.get_or_create_length(pair.first);
+    add_lemma(
+      binary_relation_exprt{length, ID_ge, from_integer(0, length.type())});
   }
 
   // Initial try without index set
@@ -949,59 +951,102 @@ void string_refinementt::add_lemma(
   prop.l_set_to_true(convert(simple_lemma));
 }
 
-/// Get a model of an array and put it in a certain form.
-/// If the model is incomplete or if it is too big, return no value.
+/// Get a model of the size of the input string.
+/// First ask the solver for a size value. If the solver has no value, get the
+/// size directly from the type. This is the case for string literals that are
+/// not part of the decision procedure (e.g. literals in return values).
+/// If the size value is not a constant or not a valid integer (size_t),
+/// return no value.
 /// \param super_get: function returning the valuation of an expression
 ///   in a model
 /// \param ns: namespace
 /// \param stream: output stream for warning messages
 /// \param arr: expression of type array representing a string
-/// \return an optional array expression or array_of_exprt
-static optionalt<exprt> get_array(
+/// \param array_pool: pool of arrays representing strings
+/// \return an optional expression representing the size of the array that can
+///         be cast to size_t
+static optionalt<exprt> get_valid_array_size(
   const std::function<exprt(const exprt &)> &super_get,
   const namespacet &ns,
   messaget::mstreamt &stream,
-  const array_string_exprt &arr)
+  const array_string_exprt &arr,
+  const array_poolt &array_pool)
 {
-  const exprt &size = arr.length();
-  exprt arr_val = simplify_expr(adjust_if_recursive(super_get(arr), ns), ns);
-  exprt size_val = super_get(size);
-  size_val = simplify_expr(size_val, ns);
-  const typet char_type = arr.type().subtype();
-  const typet &index_type = size.type();
-  const array_typet empty_ret_type(char_type, from_integer(0, index_type));
-  const array_of_exprt empty_ret(from_integer(0, char_type), empty_ret_type);
-
-  if(size_val.id() != ID_constant)
+  const auto &size_from_pool = array_pool.get_length_if_exists(arr);
+  exprt size_val;
+  if(size_from_pool.has_value())
   {
-    stream << "(sr::get_array) string of unknown size: " << format(size_val)
-           << messaget::eom;
-    return {};
+    const exprt size = size_from_pool.value();
+    size_val = simplify_expr(super_get(size), ns);
+    if(size_val.id() != ID_constant)
+    {
+      stream << "(sr::get_valid_array_size) string of unknown size: "
+             << format(size_val) << messaget::eom;
+      return {};
+    }
   }
+  else if(to_array_type(arr.type()).size().id() == ID_constant)
+    size_val = simplify_expr(to_array_type(arr.type()).size(), ns);
+  else
+    return {};
 
   auto n_opt = numeric_cast<std::size_t>(size_val);
   if(!n_opt)
   {
-    stream << "(sr::get_array) size is not valid" << messaget::eom;
+    stream << "(sr::get_valid_array_size) size is not valid" << messaget::eom;
     return {};
   }
-  std::size_t n = *n_opt;
+
+  return size_val;
+}
+
+/// Get a model of an array and put it in a certain form.
+/// If the model is incomplete or if it is too big, return no value.
+/// \param super_get: function returning the valuation of an expression
+///   in a model
+/// \param ns: namespace
+/// \param stream: output stream for warning messages
+/// \param arr: expression of type array representing a string
+/// \param array_pool: pool of arrays representing strings
+/// \return an optional array expression or array_of_exprt
+static optionalt<exprt> get_array(
+  const std::function<exprt(const exprt &)> &super_get,
+  const namespacet &ns,
+  messaget::mstreamt &stream,
+  const array_string_exprt &arr,
+  const array_poolt &array_pool)
+{
+  const auto size =
+    get_valid_array_size(super_get, ns, stream, arr, array_pool);
+  if(!size.has_value())
+  {
+    return {};
+  }
+
+  const size_t n = numeric_cast<std::size_t>(size.value()).value();
 
   if(n > MAX_CONCRETE_STRING_SIZE)
   {
-    stream << "(sr::get_array) long string (size " << format(arr.length())
+    stream << "(sr::get_valid_array_size) long string (size "
            << " = " << n << ") " << format(arr) << messaget::eom;
-    stream << "(sr::get_array) consider reducing max-nondet-string-length so "
+    stream << "(sr::get_valid_array_size) consider reducing "
+              "max-nondet-string-length so "
               "that no string exceeds "
            << MAX_CONCRETE_STRING_SIZE
            << " in length and "
               "make sure all functions returning strings are loaded"
            << messaget::eom;
-    stream << "(sr::get_array) this can also happen on invalid object access"
+    stream << "(sr::get_valid_array_size) this can also happen on invalid "
+              "object access"
            << messaget::eom;
     return nil_exprt();
   }
 
+  const exprt arr_val =
+    simplify_expr(adjust_if_recursive(super_get(arr), ns), ns);
+  const typet char_type = arr.type().subtype();
+  const typet &index_type = size.value().type();
+
   if(
     const auto &array = interval_sparse_arrayt::of_expr(
       arr_val, from_integer(CHARACTER_FOR_UNKNOWN, char_type)))
@@ -1029,17 +1074,19 @@ static std::string string_of_array(const array_exprt &arr)
 /// \param ns: namespace
 /// \param stream: output stream
 /// \param arr: array expression
+/// \param array_pool: pool of arrays representing strings
 /// \return expression corresponding to `arr` in the model
 static exprt get_char_array_and_concretize(
   const std::function<exprt(const exprt &)> &super_get,
   const namespacet &ns,
   messaget::mstreamt &stream,
-  const array_string_exprt &arr)
+  const array_string_exprt &arr,
+  array_poolt &array_pool)
 {
   stream << "- " << format(arr) << ":\n";
   stream << std::string(4, ' ') << "- type: " << format(arr.type())
          << messaget::eom;
-  const auto arr_model_opt = get_array(super_get, ns, stream, arr);
+  const auto arr_model_opt = get_array(super_get, ns, stream, arr, array_pool);
   if(arr_model_opt)
   {
     stream << std::string(4, ' ') << "- char_array: " << format(*arr_model_opt)
@@ -1050,8 +1097,8 @@ static exprt get_char_array_and_concretize(
     stream << std::string(4, ' ')
            << "- simplified_char_array: " << format(simple) << messaget::eom;
     if(
-      const auto concretized_array =
-        get_array(super_get, ns, stream, to_array_string_expr(simple)))
+      const auto concretized_array = get_array(
+        super_get, ns, stream, to_array_string_expr(simple), array_pool))
     {
       stream << std::string(4, ' ')
              << "- concretized_char_array: " << format(*concretized_array)
@@ -1082,14 +1129,15 @@ void debug_model(
   messaget::mstreamt &stream,
   const namespacet &ns,
   const std::function<exprt(const exprt &)> &super_get,
-  const std::vector<symbol_exprt> &symbols)
+  const std::vector<symbol_exprt> &symbols,
+  array_poolt &array_pool)
 {
   stream << "debug_model:" << '\n';
   for(const auto &pointer_array : generator.array_pool.get_arrays_of_pointers())
   {
     const auto arr = pointer_array.second;
     const exprt model =
-      get_char_array_and_concretize(super_get, ns, stream, arr);
+      get_char_array_and_concretize(super_get, ns, stream, arr, array_pool);
 
     stream << "- " << format(arr) << ":\n"
            << "  - pointer: " << format(pointer_array.first) << "\n"
@@ -1334,7 +1382,12 @@ static std::pair<bool, std::vector<exprt>> check_axioms(
 
 #ifdef DEBUG
   debug_model(
-    generator, stream, ns, get, generator.fresh_symbol.created_symbols);
+    generator,
+    stream,
+    ns,
+    get,
+    generator.fresh_symbol.created_symbols,
+    generator.array_pool);
 #endif
 
   // Maps from indexes of violated universal axiom to a witness of violation
@@ -1826,19 +1879,23 @@ exprt string_refinementt::get(const exprt &expr) const
   if(is_char_array_type(ecopy.type(), ns))
   {
     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;
 
-    if(const auto arr_model_opt = get_array(super_get, ns, log.debug(), arr))
+    if(
+      const auto arr_model_opt =
+        get_array(super_get, ns, log.debug(), arr, generator.array_pool))
       return *arr_model_opt;
 
-    if(generator.array_pool.created_strings().count(arr))
+    if(
+      const auto &length_from_pool =
+        generator.array_pool.get_length_if_exists(arr))
     {
-      const exprt length = super_get(arr.length());
+      const exprt length = super_get(length_from_pool.value());
+
       if(const auto n = numeric_cast<std::size_t>(length))
       {
         const interval_sparse_arrayt sparse_array(
diff --git a/src/util/string_expr.h b/src/util/string_expr.h
index 789c95010f9..cba42355423 100644
--- a/src/util/string_expr.h
+++ b/src/util/string_expr.h
@@ -66,16 +66,6 @@ inline equal_exprt equal_to(const exprt &lhs, mp_integer i)
 class array_string_exprt : public exprt
 {
 public:
-  exprt &length()
-  {
-    return to_array_type(type()).size();
-  }
-
-  const exprt &length() const
-  {
-    return to_array_type(type()).size();
-  }
-
   const typet &length_type() const
   {
     return to_array_type(type()).size().type();