Erase dead values from the value-set

This saves memory while achieving very similar behaviour as a read from a value removed from
the value-set still yields a failed object. The difference is what happens on a merge:
a merge with an explicit failed object retains it, while a merge against an empty value-set
will discard the undefined possibility. This is fine for dead variables, where on a control-
flow convergance we may safely assume we came from the path where it is not dead, but for
declarations and undefined extern variables the front-end and goto-symex must collaborate to
ensure an explicit nondet value is present.

Author: smowton

src/goto-symex/symex_dead.cpp

@@ -22,26 +22,13 @@ void goto_symext::symex_dead(statet &state)
   const code_deadt &code = instruction.get_dead();
 
   ssa_exprt ssa = state.rename_ssa<L1>(ssa_exprt{code.symbol()}, ns);
-
-  // in case of pointers, put something into the value set
-  if(code.symbol().type().id() == ID_pointer)
-  {
-    exprt rhs;
-    if(auto failed = get_failed_symbol(to_symbol_expr(code.symbol()), ns))
-      rhs = address_of_exprt(*failed, to_pointer_type(code.symbol().type()));
-    else
-      rhs=exprt(ID_invalid);
-
-    const exprt l1_rhs = state.rename<L1>(std::move(rhs), ns);
-    state.value_set.assign(ssa, l1_rhs, ns, true, false);
-  }
-
   const irep_idt &l1_identifier = ssa.get_identifier();
 
   // 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
+  // map and value-set is safe as 1) it is local to a path and 2) this instance
+  // can no longer appear
+  state.value_set.values.erase(l1_identifier);
   state.propagation.erase(l1_identifier);
   // increment the L2 index to ensure a merge on join points will propagate the
   // value for branches that are still live