We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 4cca831 commit 71983b3Copy full SHA for 71983b3
src/solvers/refinement/string_builtin_function.cpp
@@ -96,15 +96,12 @@ optionalt<std::vector<mp_integer>> eval_string(
96
: eval_string(to_array_string_expr(ite.false_case()), get_value);
97
}
98
99
- const auto size = numeric_cast<std::size_t>(get_value(a.length()));
100
const exprt content = get_value(a.content());
101
const auto &array = expr_try_dynamic_cast<array_exprt>(content);
102
- if(!size || !array)
+ if(!array)
103
return {};
104
105
const auto &ops = array->operands();
106
- INVARIANT(*size == ops.size(), "operands size should match string size");
107
-
108
std::vector<mp_integer> result;
109
const mp_integer unknown('?');
110
const auto &insert = std::back_inserter(result);
0 commit comments