diff --git a/src/goto-instrument/aggressive_slicer.cpp b/src/goto-instrument/aggressive_slicer.cpp
index 7cf71a96d12..3e047c6285c 100644
--- a/src/goto-instrument/aggressive_slicer.cpp
+++ b/src/goto-instrument/aggressive_slicer.cpp
@@ -46,8 +46,8 @@ void aggressive_slicert::get_all_functions_containing_properties()
       for(const auto &ins : fct.second.body.instructions)
         if(ins.is_assert())
         {
-          if(functions_to_keep.insert(ins.function).second)
-            note_functions_to_keep(ins.function);
+          if(functions_to_keep.insert(fct.first).second)
+            note_functions_to_keep(fct.first);
         }
     }
   }
diff --git a/src/goto-instrument/full_slicer.cpp b/src/goto-instrument/full_slicer.cpp
index 7a256867830..192de05efbe 100644
--- a/src/goto-instrument/full_slicer.cpp
+++ b/src/goto-instrument/full_slicer.cpp
@@ -38,8 +38,8 @@ void full_slicert::add_function_calls(
   queuet &queue,
   const goto_functionst &goto_functions)
 {
-  goto_functionst::function_mapt::const_iterator f_it=
-    goto_functions.function_map.find(node.PC->function);
+  goto_functionst::function_mapt::const_iterator f_it =
+    goto_functions.function_map.find(node.function_id);
   assert(f_it!=goto_functions.function_map.end());
 
   assert(!f_it->second.body.instructions.empty());
@@ -148,7 +148,7 @@ void full_slicert::add_jumps(
       continue;
     }
 
-    const irep_idt id=j.PC->function;
+    const irep_idt &id = j.function_id;
     const cfg_post_dominatorst &pd=post_dominators.at(id);
 
     cfg_post_dominatorst::cfgt::entry_mapt::const_iterator e=
@@ -182,7 +182,7 @@ void full_slicert::add_jumps(
 
         if(cfg[entry->second].node_required)
         {
-          const irep_idt id2=(*d_it)->function;
+          const irep_idt &id2 = cfg[entry->second].function_id;
           INVARIANT(id==id2,
                     "goto/jump expected to be within a single function");
 
@@ -288,6 +288,11 @@ void full_slicert::operator()(
 {
   // build the CFG data structure
   cfg(goto_functions);
+  forall_goto_functions(f_it, goto_functions)
+  {
+    forall_goto_program_instructions(i_it, f_it->second.body)
+      cfg[cfg.entry_map[i_it]].function_id = f_it->first;
+  }
 
   // fill queue with according to slicing criterion
   queuet queue;
@@ -301,7 +306,7 @@ void full_slicert::operator()(
       e_it!=cfg.entry_map.end();
       e_it++)
   {
-    if(criterion(e_it->first))
+    if(criterion(cfg[e_it->second].function_id, e_it->first))
       add_to_queue(queue, e_it->second, e_it->first);
     else if(implicit(e_it->first))
       add_to_queue(queue, e_it->second, e_it->first);
diff --git a/src/goto-instrument/full_slicer.h b/src/goto-instrument/full_slicer.h
index deb522d060f..d087b273a22 100644
--- a/src/goto-instrument/full_slicer.h
+++ b/src/goto-instrument/full_slicer.h
@@ -33,7 +33,9 @@ class slicing_criteriont
 {
 public:
   virtual ~slicing_criteriont();
-  virtual bool operator()(goto_programt::const_targett) const = 0;
+  virtual bool operator()(
+    const irep_idt &function_id,
+    goto_programt::const_targett) const = 0;
 };
 
 void full_slicer(
diff --git a/src/goto-instrument/full_slicer_class.h b/src/goto-instrument/full_slicer_class.h
index ccd60107f00..b5b9485f459 100644
--- a/src/goto-instrument/full_slicer_class.h
+++ b/src/goto-instrument/full_slicer_class.h
@@ -51,6 +51,7 @@ class full_slicert
     }
 
     bool node_required;
+    irep_idt function_id;
 #ifdef DEBUG_FULL_SLICERT
     std::set<unsigned> required_by;
 #endif
@@ -109,7 +110,8 @@ class full_slicert
 class assert_criteriont:public slicing_criteriont
 {
 public:
-  virtual bool operator()(goto_programt::const_targett target) const
+  virtual bool
+  operator()(const irep_idt &, goto_programt::const_targett target) const
   {
     return target->is_assert();
   }
@@ -123,9 +125,10 @@ class in_function_criteriont : public slicing_criteriont
   {
   }
 
-  virtual bool operator()(goto_programt::const_targett target) const
+  virtual bool
+  operator()(const irep_idt &function_id, goto_programt::const_targett) const
   {
-    return target->function == target_function;
+    return function_id == target_function;
   }
 
 protected:
@@ -141,7 +144,8 @@ class properties_criteriont:public slicing_criteriont
   {
   }
 
-  virtual bool operator()(goto_programt::const_targett target) const
+  virtual bool
+  operator()(const irep_idt &, goto_programt::const_targett target) const
   {
     if(!target->is_assert())
       return false;
diff --git a/src/goto-instrument/reachability_slicer.cpp b/src/goto-instrument/reachability_slicer.cpp
index 73e8c3a2198..4441b9e831b 100644
--- a/src/goto-instrument/reachability_slicer.cpp
+++ b/src/goto-instrument/reachability_slicer.cpp
@@ -40,20 +40,27 @@ reachability_slicert::get_sources(
   std::vector<cfgt::node_indext> sources;
   for(const auto &e_it : cfg.entry_map)
   {
-    if(criterion(e_it.first) || is_threaded(e_it.first))
+    if(
+      criterion(cfg[e_it.second].function_id, e_it.first) ||
+      is_threaded(e_it.first))
       sources.push_back(e_it.second);
   }
 
   return sources;
 }
 
-static bool is_same_target(
+bool reachability_slicert::is_same_target(
   goto_programt::const_targett it1,
-  goto_programt::const_targett it2)
+  goto_programt::const_targett it2) const
 {
   // Avoid comparing iterators belonging to different functions, and therefore
   // different std::lists.
-  return it1->function == it2->function && it1 == it2;
+  cfgt::entry_mapt::const_iterator it1_entry = cfg.entry_map.find(it1);
+  cfgt::entry_mapt::const_iterator it2_entry = cfg.entry_map.find(it2);
+  return it1_entry != cfg.entry_map.end() && it2_entry != cfg.entry_map.end() &&
+         cfg[it1_entry->second].function_id ==
+           cfg[it2_entry->second].function_id &&
+         it1 == it2;
 }
 
 /// Perform backward depth-first search of the control-flow graph of the
diff --git a/src/goto-instrument/reachability_slicer_class.h b/src/goto-instrument/reachability_slicer_class.h
index 34a706fc59c..70ff29c7e98 100644
--- a/src/goto-instrument/reachability_slicer_class.h
+++ b/src/goto-instrument/reachability_slicer_class.h
@@ -28,6 +28,12 @@ class reachability_slicert
     bool include_forward_reachability)
   {
     cfg(goto_functions);
+    forall_goto_functions(f_it, goto_functions)
+    {
+      forall_goto_program_instructions(i_it, f_it->second.body)
+        cfg[cfg.entry_map[i_it]].function_id = f_it->first;
+    }
+
     is_threadedt is_threaded(goto_functions);
     fixedpoint_to_assertions(is_threaded, criterion);
     if(include_forward_reachability)
@@ -42,10 +48,15 @@ class reachability_slicert
     {
     }
 
+    irep_idt function_id;
     bool reaches_assertion;
     bool reachable_from_assertion;
   };
 
+  bool is_same_target(
+    goto_programt::const_targett it1,
+    goto_programt::const_targett it2) const;
+
   typedef cfg_baset<slicer_entryt> cfgt;
   cfgt cfg;