Fix eval of insert to match string constraints

String constraints for insert are permisive with index that are negative
or exceed the length of the string so the eval method should do the
same, and in particular should not make an invariant fail.

Author: romainbrenguier

src/solvers/refinement/string_refinement_util.cpp

@@ -322,18 +322,22 @@ std::vector<mp_integer> string_insertion_builtin_functiont::eval(
   const std::vector<mp_integer> &args_value) const
 {
   PRECONDITION(args_value.size() >= 1 || args_value.size() <= 3);
-  const std::size_t &offset = numeric_cast_v<std::size_t>(args_value[0]);
-  const std::size_t &start =
-    args_value.size() > 1 ? numeric_cast_v<std::size_t>(args_value[1]) : 0;
-  const std::size_t &end = args_value.size() > 2
-                             ? numeric_cast_v<std::size_t>(args_value[2])
-                             : input2_value.size();
+  const auto offset = std::max(args_value[0], mp_integer(0));
+  const auto start = args_value.size() > 1
+                       ? std::max(args_value[1], mp_integer(0))
+                       : mp_integer(0);
+
+  const mp_integer input2_size(input2_value.size());
+  const auto end =
+    args_value.size() > 2
+      ? std::max(std::min(args_value[2], input2_size), mp_integer(0))
+      : input2_size;
 
   std::vector<mp_integer> result(input1_value);
   result.insert(
-    result.begin() + offset,
-    input2_value.begin() + start,
-    input2_value.end() + end);
+    result.begin() + numeric_cast_v<std::size_t>(offset),
+    input2_value.begin() + numeric_cast_v<std::size_t>(start),
+    input2_value.begin() + numeric_cast_v<std::size_t>(end));
   return result;
 }