Avoid evaluting strings exceeding maximum length

Try to evaluate long strings may make the solver run out of memory just
by allocating an array of that size.

Author: romainbrenguier

src/solvers/refinement/string_refinement.cpp

@@ -2285,10 +2285,15 @@ exprt string_refinementt::get(const exprt &expr) const
     array_string_exprt &arr = to_array_string_expr(ecopy);
     arr.length() = generator.array_pool.get_length(arr);
 
-    if(
-      const auto from_dependencies =
-        dependencies.eval(arr, [&](const exprt &expr) { return get(expr); }))
-      return *from_dependencies;
+    if(const auto length = numeric_cast<std::size_t>(arr.length()))
+    {
+      if(length <= generator.max_string_length)
+      {
+        if(const auto from_dependencies =
+          dependencies.eval(arr, [&](const exprt &expr) { return get(expr); }))
+          return *from_dependencies;
+      }
+    }
 
     const auto arr_model_opt =
       get_array(super_get, ns, generator.max_string_length, debug(), arr);