Skip to content

Commit 9e11b41

Browse files
romainbrenguierDaniel Kroening
authored and
Daniel Kroening
committed
Replace java_int_type by tyep deduced from array
This makes the function more robust and avoid dependencies on java types.
1 parent fc67510 commit 9e11b41

File tree

1 file changed

+2
-1
lines changed

1 file changed

+2
-1
lines changed

src/solvers/refinement/string_refinement.cpp

+2-1
Original file line numberDiff line numberDiff line change
@@ -1223,6 +1223,7 @@ static exprt substitute_array_access(
12231223
&symbol_generator)
12241224
{
12251225
const typet &char_type = array_expr.type().subtype();
1226+
const typet &index_type = to_array_type(array_expr.type()).size().type();
12261227
const std::vector<exprt> &operands = array_expr.operands();
12271228

12281229
exprt result = symbol_generator("out_of_bound_access", char_type);
@@ -1231,7 +1232,7 @@ static exprt substitute_array_access(
12311232
{
12321233
// Go in reverse order so that smaller indexes appear first in the result
12331234
const std::size_t pos = operands.size() - 1 - i;
1234-
const equal_exprt equals(index, from_integer(pos, java_int_type()));
1235+
const equal_exprt equals(index, from_integer(pos, index_type));
12351236
if(operands[pos].type() != char_type)
12361237
{
12371238
INVARIANT(

0 commit comments

Comments
 (0)