|
17 | 17 | #include <util/expr_util.h>
|
18 | 18 | #include <util/invariant.h>
|
19 | 19 | #include <util/pointer_offset_size.h>
|
20 |
| -#include <util/range.h> |
21 | 20 | #include <util/std_expr.h>
|
22 | 21 |
|
23 | 22 | #include <analyses/dirty.h>
|
@@ -517,26 +516,9 @@ void goto_symext::phi_function(
|
517 | 516 | const statet::goto_statet &goto_state,
|
518 | 517 | statet &dest_state)
|
519 | 518 | {
|
520 |
| - auto ssa_of_current_name = |
521 |
| - [&](const std::pair<irep_idt, std::pair<ssa_exprt, unsigned>> &pair) { |
522 |
| - return pair.second.first; |
523 |
| - }; |
524 |
| - |
525 |
| - auto dest_state_names_range = |
526 |
| - make_range(dest_state.level2.current_names) |
527 |
| - .filter( |
528 |
| - [&](const std::pair<irep_idt, std::pair<ssa_exprt, unsigned>> &pair) { |
529 |
| - // We ignore the identifiers that are already in goto_state names |
530 |
| - return goto_state.level2_current_names.count(pair.first) == 0; |
531 |
| - }) |
532 |
| - .map<const ssa_exprt>(ssa_of_current_name); |
533 |
| - |
534 |
| - // go over all variables to see what changed |
535 |
| - auto all_current_names_range = make_range(goto_state.level2_current_names) |
536 |
| - .map<const ssa_exprt>(ssa_of_current_name) |
537 |
| - .concat(dest_state_names_range); |
538 |
| - |
539 |
| - if(all_current_names_range.empty()) |
| 519 | + if( |
| 520 | + goto_state.level2_current_names.empty() && |
| 521 | + dest_state.level2.current_names.empty()) |
540 | 522 | return;
|
541 | 523 |
|
542 | 524 | guardt diff_guard = goto_state.guard;
|
|
0 commit comments