string_refinement::get(): get length if exists

In string_refinement::get(), we now get the length of the string from
the array_pool instead of the array type.

We use get_length_if_exists() instead of get_length(), because we want to
ignore if the length does not exist, instead of creating a new
symbol.

Author: Joel Allred

src/solvers/strings/string_refinement.cpp

@@ -1834,9 +1834,12 @@ exprt string_refinementt::get(const exprt &expr) const
     if(const auto arr_model_opt = get_array(super_get, ns, log.debug(), arr))
       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(