diff --git a/src/solvers/refinement/string_refinement_util.cpp b/src/solvers/refinement/string_refinement_util.cpp index 46cb5178389..c9071509452 100644 --- a/src/solvers/refinement/string_refinement_util.cpp +++ b/src/solvers/refinement/string_refinement_util.cpp @@ -292,17 +292,19 @@ std::vector string_concatenation_builtin_functiont::eval( const std::vector &input2_value, const std::vector &args_value) const { - const std::size_t start_index = - args_value.size() > 0 && args_value[0] > 0 ? args_value[0].to_ulong() : 0; - const std::size_t end_index = args_value.size() > 1 && args_value[1] > 0 - ? args_value[1].to_ulong() - : input2_value.size(); + const auto start_index = + args_value.size() > 0 && args_value[0] > 0 ? args_value[0] : mp_integer(0); + const mp_integer input2_size(input2_value.size()); + const auto end_index = + args_value.size() > 1 + ? std::max(std::min(args_value[1], input2_size), start_index) + : input2_size; std::vector result(input1_value); result.insert( result.end(), - input2_value.begin() + start_index, - input2_value.begin() + end_index); + input2_value.begin() + numeric_cast_v(start_index), + input2_value.begin() + numeric_cast_v(end_index)); return result; }