Skip to content

Commit 0e9e81c

Browse files
Correct iteration in concretize_arrays_in_expression
Before it could happen that we try to increment the end iterator
1 parent a885c7e commit 0e9e81c

File tree

1 file changed

+3
-1
lines changed

1 file changed

+3
-1
lines changed

src/solvers/refinement/string_refinement.cpp

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1106,13 +1106,15 @@ static exprt negation_of_constraint(const string_constraintt &axiom)
11061106
/// \return the interpreted expression
11071107
exprt concretize_arrays_in_expression(exprt expr, std::size_t string_max_length)
11081108
{
1109-
for(auto op=expr.depth_begin(); op!=expr.depth_end(); ++op)
1109+
for(auto op=expr.depth_begin(); op!=expr.depth_end();)
11101110
{
11111111
if(op->id()==ID_with && op->type().id()==ID_array)
11121112
{
11131113
op.mutate()=fill_in_array_with_expr(*op, string_max_length);
11141114
op.next_sibling_or_parent();
11151115
}
1116+
else
1117+
++op;
11161118
}
11171119
return expr;
11181120
}

0 commit comments

Comments
 (0)