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

Author: svorenova

src/goto-instrument/nondet_static.cpp

@@ -17,6 +17,7 @@ Date: November 2011
 #include <goto-programs/goto_model.h>
 
 #include <linking/static_lifetime_init.h>
+#include <goto-programs/remove_skip.h>
 
 void nondet_static(
   const namespacet &ns,
@@ -58,11 +59,12 @@ void nondet_static(
       if(is_constant_or_has_constant_components(sym.type(), ns))
         continue;
 
-      i_it=init.insert_before(++i_it);
-      i_it->make_assignment();
-      i_it->code=code_assignt(sym, side_effect_expr_nondett(sym.type()));
-      i_it->source_location=instruction.source_location;
-      i_it->function=instruction.function;
+      const auto &ni_it=init.insert_after(i_it);
+      ni_it->make_assignment();
+      ni_it->code=code_assignt(sym, side_effect_expr_nondett(sym.type()));
+      ni_it->source_location=instruction.source_location;
+      ni_it->function=instruction.function;
+      i_it->make_skip();
     }
     else if(instruction.is_function_call())
     {
@@ -73,6 +75,7 @@ void nondet_static(
         nondet_static(ns, goto_functions, fsym.get_identifier());
     }
   }
+  remove_skip(init);
 }
 
 void nondet_static(