Skip to content

Commit 39ed961

Browse files
author
Joel Allred
committed
Unit test: get constant length directly from array
We require a constant value in this case and querying the array pool gives us a symbol.
1 parent de81183 commit 39ed961

File tree

1 file changed

+2
-1
lines changed

1 file changed

+2
-1
lines changed

jbmc/unit/solvers/strings/string_constraint_instantiation/instantiate_not_contains.cpp

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -105,7 +105,8 @@ refined_string_exprt make_refined_string_exprt(
105105
std::set<exprt>
106106
full_index_set(const array_string_exprt &s, array_poolt &array_pool)
107107
{
108-
const mp_integer n = numeric_cast_v<mp_integer>(to_constant_expr(s.length()));
108+
const mp_integer n = numeric_cast_v<mp_integer>(
109+
to_constant_expr(to_array_type(s.type()).size()));
109110
std::set<exprt> ret;
110111
for(mp_integer i = 0; i < n; ++i)
111112
ret.insert(from_integer(i));

0 commit comments

Comments
 (0)