diff --git a/src/solvers/refinement/string_builtin_function.cpp b/src/solvers/refinement/string_builtin_function.cpp index 28ba76088a3..87a7c82e858 100644 --- a/src/solvers/refinement/string_builtin_function.cpp +++ b/src/solvers/refinement/string_builtin_function.cpp @@ -96,15 +96,12 @@ optionalt> eval_string( : eval_string(to_array_string_expr(ite.false_case()), get_value); } - const auto size = numeric_cast(get_value(a.length())); const exprt content = get_value(a.content()); const auto &array = expr_try_dynamic_cast(content); - if(!size || !array) + if(!array) return {}; const auto &ops = array->operands(); - INVARIANT(*size == ops.size(), "operands size should match string size"); - std::vector result; const mp_integer unknown('?'); const auto &insert = std::back_inserter(result);