diff --git a/regression/cbmc/Local_out_of_scope4/main.c b/regression/cbmc/Local_out_of_scope4/main.c
new file mode 100644
index 00000000000..4117a283b4d
--- /dev/null
+++ b/regression/cbmc/Local_out_of_scope4/main.c
@@ -0,0 +1,15 @@
+int main()
+{
+  int *p = 0;
+
+  for(int i = 0; i < 3; ++i)
+  {
+    {
+      int x = 42;
+      p = &x;
+      *p = 1;
+    }
+  }
+
+  return 0;
+}
diff --git a/regression/cbmc/Local_out_of_scope4/test.desc b/regression/cbmc/Local_out_of_scope4/test.desc
new file mode 100644
index 00000000000..39c491ba8bb
--- /dev/null
+++ b/regression/cbmc/Local_out_of_scope4/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--pointer-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp
index b907cef042f..5e670922f59 100644
--- a/src/analyses/goto_check.cpp
+++ b/src/analyses/goto_check.cpp
@@ -1666,6 +1666,34 @@ void goto_checkt::goto_check(
         }
       }
     }
+    else if(i.is_decl())
+    {
+      if(enable_pointer_check)
+      {
+        assert(i.code.operands().size()==1);
+        const symbol_exprt &variable=to_symbol_expr(i.code.op0());
+
+        // is it dirty?
+        if(local_bitvector_analysis->dirty(variable))
+        {
+          // reset the dead marker
+          goto_programt::targett t=new_code.add_instruction(ASSIGN);
+          exprt address_of_expr=address_of_exprt(variable);
+          exprt lhs=ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr();
+          if(!base_type_eq(lhs.type(), address_of_expr.type(), ns))
+            address_of_expr.make_typecast(lhs.type());
+          exprt rhs=
+            if_exprt(
+              equal_exprt(lhs, address_of_expr),
+              null_pointer_exprt(to_pointer_type(address_of_expr.type())),
+              lhs,
+              lhs.type());
+          t->source_location=i.source_location;
+          t->code=code_assignt(lhs, rhs);
+          t->code.add_source_location()=i.source_location;
+        }
+      }
+    }
     else if(i.is_end_function())
     {
       if(i.function==goto_functionst::entry_point() &&
diff --git a/src/goto-symex/symex_decl.cpp b/src/goto-symex/symex_decl.cpp
index e243c46a9fe..a73875909a3 100644
--- a/src/goto-symex/symex_decl.cpp
+++ b/src/goto-symex/symex_decl.cpp
@@ -72,11 +72,8 @@ void goto_symext::symex_decl(statet &state, const symbol_exprt &expr)
   state.propagation.remove(l1_identifier);
 
   // L2 renaming
-  // inlining may yield multiple declarations of the same identifier
-  // within the same L1 context
-  if(state.level2.current_names.find(l1_identifier)==
-     state.level2.current_names.end())
-    state.level2.current_names[l1_identifier]=std::make_pair(ssa, 0);
+  state.level2.current_names.insert(
+    std::make_pair(l1_identifier, std::make_pair(ssa, 0)));
   state.level2.increase_counter(l1_identifier);
   const bool record_events=state.record_events;
   state.record_events=false;