Skip to content

Commit 5e961cf

Browse files
committed
Array index resolution: fix use of goto_symex_statet::rename
This used to accidentally discard its argument, losing the possibility to replace an array index with its true value.
1 parent f31e9b5 commit 5e961cf

File tree

1 file changed

+2
-4
lines changed

1 file changed

+2
-4
lines changed

src/goto-symex/symex_dereference.cpp

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -237,8 +237,7 @@ void goto_symext::dereference_rec(exprt &expr, statet &state, bool write)
237237
const exprt &array_cell = to_index_expr(*expr_it).index();
238238
if(!array_cell.is_constant())
239239
{
240-
exprt constant_array_cell = array_cell;
241-
state.rename(constant_array_cell, ns);
240+
exprt constant_array_cell = state.rename(array_cell, ns).get();
242241
do_simplify(constant_array_cell);
243242
if(constant_array_cell.is_constant())
244243
{
@@ -255,8 +254,7 @@ void goto_symext::dereference_rec(exprt &expr, statet &state, bool write)
255254
const exprt &rhs = expr_it->op1();
256255
if(!rhs.is_constant())
257256
{
258-
exprt constant_rhs = rhs;
259-
state.rename(constant_rhs, ns);
257+
exprt constant_rhs = state.rename(rhs, ns).get();
260258
do_simplify(constant_rhs);
261259
if(constant_rhs.is_constant())
262260
{

0 commit comments

Comments
 (0)