Skip to content

Commit daff1d1

Browse files
author
svorenova
committed
Make nondet-static replace lines in CPROVER_init
Instead of keeping both the original line that sets the value of a variable and the new line that nondet initializes it, we only keep the new one
1 parent b62bf01 commit daff1d1

File tree

1 file changed

+3
-3
lines changed

1 file changed

+3
-3
lines changed

src/goto-instrument/nondet_static.cpp

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -58,11 +58,11 @@ void nondet_static(
5858
if(is_constant_or_has_constant_components(sym.type(), ns))
5959
continue;
6060

61-
i_it=init.insert_before(++i_it);
61+
const goto_programt::instructiont original_instruction = instruction;
6262
i_it->make_assignment();
6363
i_it->code=code_assignt(sym, side_effect_expr_nondett(sym.type()));
64-
i_it->source_location=instruction.source_location;
65-
i_it->function=instruction.function;
64+
i_it->source_location = original_instruction.source_location;
65+
i_it->function = original_instruction.function;
6666
}
6767
else if(instruction.is_function_call())
6868
{

0 commit comments

Comments
 (0)