Clarify comments in symex_dead

Try to make clearer what we can(not) remove from renaming maps. Also do small
cleanups of the code.

Author: tautschnig

src/goto-symex/symex_dead.cpp

@@ -11,8 +11,6 @@ Author: Daniel Kroening, [email protected]
 
 #include "goto_symex.h"
 
-#include <cassert>
-
 #include <util/std_expr.h>
 
 #include <pointer-analysis/add_failed_symbols.h>
@@ -23,9 +21,6 @@ void goto_symext::symex_dead(statet &state)
 
   const code_deadt &code = instruction.get_dead();
 
-  // We increase the L2 renaming to make these non-deterministic.
-  // We also prevent propagation of old values.
-
   ssa_exprt ssa = state.rename_ssa<statet::L1>(ssa_exprt{code.symbol()}, ns);
 
   // in case of pointers, put something into the value set
@@ -44,10 +39,13 @@ void goto_symext::symex_dead(statet &state)
 
   const irep_idt &l1_identifier = ssa.get_identifier();
 
-  // prevent propagation
+  // we cannot remove the object from the L1 renaming map, because L1 renaming
+  // information is not local to a path, but removing it from the propagation
+  // map is safe as 1) it is local to a path and 2) this instance can no longer
+  // appear
   state.propagation.erase(l1_identifier);
-
-  // L2 renaming
+  // increment the L2 index to ensure a merge on join points will propagate the
+  // value for branches that are still live
   auto level2_it = state.level2.current_names.find(l1_identifier);
   if(level2_it != state.level2.current_names.end())
     symex_renaming_levelt::increase_counter(level2_it);