We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent de81183 commit 0313d1eCopy full SHA for 0313d1e
jbmc/unit/solvers/strings/string_constraint_instantiation/instantiate_not_contains.cpp
@@ -105,7 +105,8 @@ refined_string_exprt make_refined_string_exprt(
105
std::set<exprt>
106
full_index_set(const array_string_exprt &s, array_poolt &array_pool)
107
{
108
- const mp_integer n = numeric_cast_v<mp_integer>(to_constant_expr(s.length()));
+ const mp_integer n =
109
+ numeric_cast_v<mp_integer>(to_constant_expr(array_pool.get_length(s)));
110
std::set<exprt> ret;
111
for(mp_integer i = 0; i < n; ++i)
112
ret.insert(from_integer(i));
0 commit comments