Skip to content

Commit 13e4931

Browse files
Use parameter instead of lookup for count
1 parent 399b687 commit 13e4931

File tree

1 file changed

+3
-6
lines changed

1 file changed

+3
-6
lines changed

src/goto-symex/symex_goto.cpp

Lines changed: 3 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -412,8 +412,7 @@ void goto_symext::phi_function(
412412
if(obj_identifier==guard_identifier)
413413
return; // just a guard, don't bother
414414

415-
if(goto_state.level2_current_count(l1_identifier)==
416-
dest_state.level2.current_count(l1_identifier))
415+
if(goto_count == dest_count)
417416
return; // not at all changed
418417

419418
// changed!
@@ -445,8 +444,7 @@ void goto_symext::phi_function(
445444
if(p_it != goto_state.propagation.end())
446445
goto_state_rhs=p_it->second;
447446
else
448-
to_ssa_expr(goto_state_rhs).set_level_2(
449-
goto_state.level2_current_count(l1_identifier));
447+
to_ssa_expr(goto_state_rhs).set_level_2(goto_count);
450448
}
451449

452450
{
@@ -455,8 +453,7 @@ void goto_symext::phi_function(
455453
if(p_it != dest_state.propagation.end())
456454
dest_state_rhs=p_it->second;
457455
else
458-
to_ssa_expr(dest_state_rhs).set_level_2(
459-
dest_state.level2.current_count(l1_identifier));
456+
to_ssa_expr(dest_state_rhs).set_level_2(dest_count);
460457
}
461458

462459
exprt rhs;

0 commit comments

Comments
 (0)