diff --git a/regression/cbmc/trace_show_function_calls/test.desc b/regression/cbmc/trace_show_function_calls/test.desc
index 016a682dd8b..bf9dc380543 100644
--- a/regression/cbmc/trace_show_function_calls/test.desc
+++ b/regression/cbmc/trace_show_function_calls/test.desc
@@ -4,7 +4,7 @@ main.c
 ^EXIT=10$
 ^SIGNAL=0$
 Function call: function_to_call\(-2147483647\) \(depth 2\)
-Function return: function_to_call \(depth 1\)
+Function return from function_to_call \(depth 1\)
 Function call: function_to_call\(-2\) \(depth 2\)
 ^VERIFICATION FAILED$
 --
diff --git a/src/cbmc/symex_bmc.cpp b/src/cbmc/symex_bmc.cpp
index 077df0402a7..438b5a0c73d 100644
--- a/src/cbmc/symex_bmc.cpp
+++ b/src/cbmc/symex_bmc.cpp
@@ -65,10 +65,11 @@ void symex_bmct::symex_step(
 
   goto_symext::symex_step(get_goto_function, state);
 
-  if(record_coverage &&
-     // avoid an invalid iterator in state.source.pc
-     (!cur_pc->is_end_function() ||
-      cur_pc->function!=goto_functionst::entry_point()))
+  if(
+    record_coverage &&
+    // avoid an invalid iterator in state.source.pc
+    (!cur_pc->is_end_function() ||
+     state.source.function != goto_functionst::entry_point()))
   {
     // forward goto will effectively be covered via phi function,
     // which does not invoke symex_step; as symex_step is called
diff --git a/src/goto-programs/goto_trace.cpp b/src/goto-programs/goto_trace.cpp
index a9b797a6e3e..3d01ec6708f 100644
--- a/src/goto-programs/goto_trace.cpp
+++ b/src/goto-programs/goto_trace.cpp
@@ -83,8 +83,8 @@ void goto_trace_stept::output(
 
   if(is_assert() || is_assume() || is_goto())
     out << " (" << cond_value << ')';
-  else if(is_function_call() || is_function_return())
-    out << ' ' << function_identifier;
+  else if(is_function_call())
+    out << ' ' << called_function;
 
   if(hidden)
     out << " hidden";
@@ -344,8 +344,7 @@ void show_full_goto_trace(
         out << "  " << messaget::red << step.comment << messaget::reset << '\n';
 
         if(step.pc->is_assert())
-          out << "  " << from_expr(ns, step.pc->function, step.pc->guard)
-              << '\n';
+          out << "  " << from_expr(ns, step.function, step.pc->guard) << '\n';
 
         out << '\n';
       }
@@ -360,8 +359,7 @@ void show_full_goto_trace(
           out << "  " << step.pc->source_location << '\n';
 
         if(step.pc->is_assume())
-          out << "  " << from_expr(ns, step.pc->function, step.pc->guard)
-              << '\n';
+          out << "  " << from_expr(ns, step.function, step.pc->guard) << '\n';
 
         out << '\n';
       }
@@ -431,7 +429,8 @@ void show_full_goto_trace(
         {
           if(l_it!=step.io_args.begin())
             out << ';';
-          out << ' ' << from_expr(ns, step.pc->function, *l_it);
+
+          out << ' ' << from_expr(ns, step.function, *l_it);
 
           // the binary representation
           out << " (" << trace_numeric_value(*l_it, ns, options) << ')';
@@ -453,7 +452,8 @@ void show_full_goto_trace(
       {
         if(l_it!=step.io_args.begin())
           out << ';';
-        out << ' ' << from_expr(ns, step.pc->function, *l_it);
+
+        out << ' ' << from_expr(ns, step.function, *l_it);
 
         // the binary representation
         out << " (" << trace_numeric_value(*l_it, ns, options) << ')';
@@ -466,7 +466,7 @@ void show_full_goto_trace(
       function_depth++;
       if(options.show_function_calls)
       {
-        out << "\n#### Function call: " << step.function_identifier;
+        out << "\n#### Function call: " << step.called_function;
         out << '(';
 
         bool first = true;
@@ -477,7 +477,7 @@ void show_full_goto_trace(
           else
             out << ", ";
 
-          out << from_expr(ns, step.function_identifier, arg);
+          out << from_expr(ns, step.function, arg);
         }
 
         out << ") (depth " << function_depth << ") ####\n";
@@ -488,8 +488,8 @@ void show_full_goto_trace(
       function_depth--;
       if(options.show_function_calls)
       {
-        out << "\n#### Function return: " << step.function_identifier
-            << " (depth " << function_depth << ") ####\n";
+        out << "\n#### Function return from " << step.function << " (depth "
+            << function_depth << ") ####\n";
       }
       break;
 
@@ -561,7 +561,7 @@ void show_goto_stack_trace(
     }
     else if(step.is_function_call())
     {
-      out << "  " << step.function_identifier;
+      out << "  " << step.called_function;
       out << '(';
 
       bool first = true;
@@ -572,7 +572,7 @@ void show_goto_stack_trace(
         else
           out << ", ";
 
-        out << from_expr(ns, step.function_identifier, arg);
+        out << from_expr(ns, step.function, arg);
       }
 
       out << ')';
diff --git a/src/goto-programs/goto_trace.h b/src/goto-programs/goto_trace.h
index e82d5961881..3d5fada5c66 100644
--- a/src/goto-programs/goto_trace.h
+++ b/src/goto-programs/goto_trace.h
@@ -86,6 +86,9 @@ class goto_trace_stept
   enum class assignment_typet { STATE, ACTUAL_PARAMETER };
   assignment_typet assignment_type;
 
+  // The instruction that created this step
+  // (function calls are in the caller, function returns are in the callee)
+  irep_idt function;
   goto_programt::const_targett pc;
 
   // this transition done by given thread number
@@ -113,8 +116,8 @@ class goto_trace_stept
   io_argst io_args;
   bool formatted;
 
-  // for function call/return
-  irep_idt function_identifier;
+  // for function calls
+  irep_idt called_function;
 
   // for function call
   std::vector<exprt> function_arguments;
diff --git a/src/goto-programs/graphml_witness.cpp b/src/goto-programs/graphml_witness.cpp
index 1fcb1e603f5..b1821cfde78 100644
--- a/src/goto-programs/graphml_witness.cpp
+++ b/src/goto-programs/graphml_witness.cpp
@@ -284,8 +284,8 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace)
         {
           xmlt &val=edge.new_element("data");
           val.set_attribute("key", "assumption");
-          val.data=from_expr(ns, it->pc->function, it->full_lhs)+" = "+
-                   from_expr(ns, it->pc->function, it->full_lhs_value)+";";
+          val.data = from_expr(ns, it->function, it->full_lhs) + " = " +
+                     from_expr(ns, it->function, it->full_lhs_value) + ";";
 
           xmlt &val_s=edge.new_element("data");
           val_s.set_attribute("key", "assumption.scope");
@@ -296,10 +296,9 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace)
         {
           xmlt &val=edge.new_element("data");
           val.set_attribute("key", "sourcecode");
-          const std::string cond =
-            from_expr(ns, it->pc->function, it->cond_expr);
-          const std::string neg_cond=
-            from_expr(ns, it->pc->function, not_exprt(it->cond_expr));
+          const std::string cond = from_expr(ns, it->function, it->cond_expr);
+          const std::string neg_cond =
+            from_expr(ns, it->function, not_exprt(it->cond_expr));
           val.data="["+(it->cond_value ? cond : neg_cond)+"]";
 
           #if 0
@@ -481,7 +480,7 @@ void graphml_witnesst::operator()(const symex_target_equationt &equation)
           xmlt &val=edge.new_element("data");
           val.set_attribute("key", "sourcecode");
           const std::string cond =
-            from_expr(ns, it->source.pc->function, it->cond_expr);
+            from_expr(ns, it->source.function, it->cond_expr);
           val.data="["+cond+"]";
         }
 
diff --git a/src/goto-programs/interpreter.cpp b/src/goto-programs/interpreter.cpp
index b698bbf18aa..f00d989b2b7 100644
--- a/src/goto-programs/interpreter.cpp
+++ b/src/goto-programs/interpreter.cpp
@@ -759,7 +759,7 @@ void interpretert::execute_function_call()
   const memory_cellt &cell=memory[address];
 #endif
   const irep_idt &identifier = address_to_identifier(address);
-  trace_step.function_identifier = identifier;
+  trace_step.called_function = identifier;
 
   const goto_functionst::function_mapt::const_iterator f_it=
     goto_functions.function_map.find(identifier);
diff --git a/src/goto-programs/json_goto_trace.cpp b/src/goto-programs/json_goto_trace.cpp
index 508d8104d5e..b2710adbb57 100644
--- a/src/goto-programs/json_goto_trace.cpp
+++ b/src/goto-programs/json_goto_trace.cpp
@@ -277,10 +277,14 @@ void convert_return(
   json_call_return["internal"] = jsont::json_boolean(step.internal);
   json_call_return["thread"] = json_numbert(std::to_string(step.thread_nr));
 
-  const symbolt &symbol = ns.lookup(step.function_identifier);
+  const irep_idt &function_identifier =
+    (step.type == goto_trace_stept::typet::FUNCTION_CALL) ? step.called_function
+                                                          : step.function;
+
+  const symbolt &symbol = ns.lookup(function_identifier);
   json_objectt &json_function = json_call_return["function"].make_object();
   json_function["displayName"] = json_stringt(symbol.display_name());
-  json_function["identifier"] = json_stringt(step.function_identifier);
+  json_function["identifier"] = json_stringt(function_identifier);
   json_function["sourceLocation"] = json(symbol.location);
 
   if(!location.is_null())
diff --git a/src/goto-programs/xml_goto_trace.cpp b/src/goto-programs/xml_goto_trace.cpp
index e0850a489ac..a6c4d413050 100644
--- a/src/goto-programs/xml_goto_trace.cpp
+++ b/src/goto-programs/xml_goto_trace.cpp
@@ -139,7 +139,7 @@ void convert(
         for(const auto &arg : step.io_args)
         {
           xml_output.new_element("value").data =
-            from_expr(ns, step.pc->function, arg);
+            from_expr(ns, step.function, arg);
           xml_output.new_element("value_expression").
             new_element(xml(arg, ns));
         }
@@ -158,7 +158,7 @@ void convert(
         for(const auto &arg : step.io_args)
         {
           xml_input.new_element("value").data =
-            from_expr(ns, step.pc->function, arg);
+            from_expr(ns, step.function, arg);
           xml_input.new_element("value_expression").
             new_element(xml(arg, ns));
         }
@@ -169,23 +169,40 @@ void convert(
       break;
 
     case goto_trace_stept::typet::FUNCTION_CALL:
+    {
+      std::string tag = "function_call";
+      xmlt &xml_call_return = dest.new_element(tag);
+
+      xml_call_return.set_attribute_bool("hidden", step.hidden);
+      xml_call_return.set_attribute("thread", std::to_string(step.thread_nr));
+      xml_call_return.set_attribute("step_nr", std::to_string(step.step_nr));
+
+      const symbolt &symbol = ns.lookup(step.called_function);
+      xmlt &xml_function = xml_call_return.new_element("function");
+      xml_function.set_attribute(
+        "display_name", id2string(symbol.display_name()));
+      xml_function.set_attribute("identifier", id2string(symbol.name));
+      xml_function.new_element() = xml(symbol.location);
+
+      if(xml_location.name != "")
+        xml_call_return.new_element().swap(xml_location);
+    }
+    break;
+
     case goto_trace_stept::typet::FUNCTION_RETURN:
       {
-        std::string tag=
-          (step.type==goto_trace_stept::typet::FUNCTION_CALL)?
-          "function_call":"function_return";
+        std::string tag = "function_return";
         xmlt &xml_call_return=dest.new_element(tag);
 
         xml_call_return.set_attribute_bool("hidden", step.hidden);
         xml_call_return.set_attribute("thread", std::to_string(step.thread_nr));
         xml_call_return.set_attribute("step_nr", std::to_string(step.step_nr));
 
-        const symbolt &symbol = ns.lookup(step.function_identifier);
+        const symbolt &symbol = ns.lookup(step.function);
         xmlt &xml_function=xml_call_return.new_element("function");
         xml_function.set_attribute(
           "display_name", id2string(symbol.display_name()));
-        xml_function.set_attribute(
-          "identifier", id2string(step.function_identifier));
+        xml_function.set_attribute("identifier", id2string(step.function));
         xml_function.new_element()=xml(symbol.location);
 
         if(xml_location.name!="")
diff --git a/src/goto-symex/build_goto_trace.cpp b/src/goto-symex/build_goto_trace.cpp
index 658c589a66c..33a613b34f3 100644
--- a/src/goto-symex/build_goto_trace.cpp
+++ b/src/goto-symex/build_goto_trace.cpp
@@ -153,7 +153,7 @@ void update_internal_field(
   }
 
   // set internal field to _start function-return step
-  if(SSA_step.source.pc->function==goto_functionst::entry_point())
+  if(SSA_step.source.function == goto_functionst::entry_point())
   {
     // "__CPROVER_*" function calls in __CPROVER_start are already marked as
     // internal. Don't mark any other function calls (i.e. "main"), function
@@ -299,13 +299,14 @@ void build_goto_trace(
 
       goto_trace_step.thread_nr = SSA_step.source.thread_nr;
       goto_trace_step.pc = SSA_step.source.pc;
+      goto_trace_step.function = SSA_step.source.function;
       goto_trace_step.comment = SSA_step.comment;
       goto_trace_step.type = SSA_step.type;
       goto_trace_step.hidden = SSA_step.hidden;
       goto_trace_step.format_string = SSA_step.format_string;
       goto_trace_step.io_id = SSA_step.io_id;
       goto_trace_step.formatted = SSA_step.formatted;
-      goto_trace_step.function_identifier = SSA_step.function_identifier;
+      goto_trace_step.called_function = SSA_step.called_function;
       goto_trace_step.function_arguments = SSA_step.converted_function_arguments;
 
       for(auto &arg : goto_trace_step.function_arguments)
diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h
index 76aa8655ffe..b59552f07af 100644
--- a/src/goto-symex/goto_symex.h
+++ b/src/goto-symex/goto_symex.h
@@ -148,11 +148,13 @@ class goto_symext
   /// procedure.
   /// \param state Symex state to start with.
   /// \param goto_functions GOTO model to symex.
+  /// \param function_identifier The function with the instruction range
   /// \param first Entry point in form of a first instruction.
   /// \param limit Final instruction, which itself will not be symexed.
   virtual void symex_instruction_range(
     statet &,
     const goto_functionst &,
+    const irep_idt &function_identifier,
     goto_programt::const_targett first,
     goto_programt::const_targett limit);
 
@@ -162,11 +164,13 @@ class goto_symext
   /// procedure.
   /// \param state Symex state to start with.
   /// \param get_goto_function retrieves a function body
+  /// \param function_identifier The function with the instruction range
   /// \param first Entry point in form of a first instruction.
   /// \param limit Final instruction, which itself will not be symexed.
   virtual void symex_instruction_range(
     statet &state,
     const get_goto_functiont &get_goto_function,
+    const irep_idt &function_identifier,
     goto_programt::const_targett first,
     goto_programt::const_targett limit);
 
@@ -183,13 +187,15 @@ class goto_symext
   /// Initialise the symbolic execution and the given state with <code>pc</code>
   /// as entry point.
   /// \param state Symex state to initialise.
-  /// \param goto_functions GOTO model to symex.
+  /// \param get_goto_function producer for GOTO functions
+  /// \param function_identifier The function in which the instructions are
   /// \param pc first instruction to symex
   /// \param limit final instruction, which itself will not
   /// be symexed.
   void initialize_entry_point(
     statet &state,
     const get_goto_functiont &get_goto_function,
+    const irep_idt &function_identifier,
     goto_programt::const_targett pc,
     goto_programt::const_targett limit);
 
diff --git a/src/goto-symex/show_program.cpp b/src/goto-symex/show_program.cpp
index 13035218cb0..c054034e7f7 100644
--- a/src/goto-symex/show_program.cpp
+++ b/src/goto-symex/show_program.cpp
@@ -29,7 +29,7 @@ void show_program(const namespacet &ns, const symex_target_equationt &equation)
   {
     std::cout << "// " << step.source.pc->location_number << " ";
     std::cout << step.source.pc->source_location.as_string() << "\n";
-    const irep_idt &function = step.source.pc->function;
+    const irep_idt &function = step.source.function;
 
     if(step.is_assignment())
     {
diff --git a/src/goto-symex/symex_builtin_functions.cpp b/src/goto-symex/symex_builtin_functions.cpp
index 6d817547328..89a3ac9bcb2 100644
--- a/src/goto-symex/symex_builtin_functions.cpp
+++ b/src/goto-symex/symex_builtin_functions.cpp
@@ -55,8 +55,8 @@ void goto_symext::symex_allocate(
 
   exprt size=code.op0();
   typet object_type=nil_typet();
-  auto function_symbol = outer_symbol_table.lookup(state.source.pc->function);
-  INVARIANT(function_symbol, "function associated with instruction not found");
+  auto function_symbol = outer_symbol_table.lookup(state.source.function);
+  INVARIANT(function_symbol, "function associated with allocation not found");
   const irep_idt &mode = function_symbol->mode;
 
   // is the type given?
diff --git a/src/goto-symex/symex_dereference.cpp b/src/goto-symex/symex_dereference.cpp
index b4be01f113e..40bcf40f1ae 100644
--- a/src/goto-symex/symex_dereference.cpp
+++ b/src/goto-symex/symex_dereference.cpp
@@ -258,7 +258,7 @@ void goto_symext::dereference_rec(
 
     if(state.threads.size() == 1)
     {
-      const irep_idt &expr_function = state.source.pc->function;
+      const irep_idt &expr_function = state.source.function;
       if(!expr_function.empty())
       {
         state.get_original_name(to_check);
diff --git a/src/goto-symex/symex_function_call.cpp b/src/goto-symex/symex_function_call.cpp
index 508d48aa52f..abf85e6a514 100644
--- a/src/goto-symex/symex_function_call.cpp
+++ b/src/goto-symex/symex_function_call.cpp
@@ -267,7 +267,7 @@ void goto_symext::symex_function_call_code(
     no_body(identifier);
 
     // record the return
-    target.function_return(state.guard.as_expr(), identifier, state.source);
+    target.function_return(state.guard.as_expr(), state.source);
 
     if(call.lhs().is_not_nil())
     {
@@ -310,6 +310,7 @@ void goto_symext::symex_function_call_code(
   frame.loop_iterations[identifier].count++;
 
   state.source.is_set=true;
+  state.source.function = identifier;
   symex_transition(state, goto_function.body.instructions.begin());
 }
 
@@ -323,6 +324,7 @@ void goto_symext::pop_frame(statet &state)
 
     // restore program counter
     symex_transition(state, frame.calling_location.pc);
+    state.source.function = frame.calling_location.function;
 
     // restore L1 renaming
     state.level1.restore_from(frame.old_level1);
@@ -357,8 +359,7 @@ void goto_symext::pop_frame(statet &state)
 void goto_symext::symex_end_of_function(statet &state)
 {
   // first record the return
-  target.function_return(
-    state.guard.as_expr(), state.source.pc->function, state.source);
+  target.function_return(state.guard.as_expr(), state.source);
 
   // then get rid of the frame
   pop_frame(state);
diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp
index e0d7b39790e..df00b4c0806 100644
--- a/src/goto-symex/symex_main.cpp
+++ b/src/goto-symex/symex_main.cpp
@@ -121,12 +121,13 @@ void goto_symext::rewrite_quantifiers(exprt &expr, statet &state)
 void goto_symext::initialize_entry_point(
   statet &state,
   const get_goto_functiont &get_goto_function,
+  const irep_idt &function_identifier,
   const goto_programt::const_targett pc,
   const goto_programt::const_targett limit)
 {
   PRECONDITION(!state.threads.empty());
   PRECONDITION(!state.call_stack().empty());
-  state.source=symex_targett::sourcet(pc);
+  state.source = symex_targett::sourcet(function_identifier, pc);
   state.top().end_of_function=limit;
   state.top().calling_location.pc=state.top().end_of_function;
   state.symex_target=&target;
@@ -250,22 +251,29 @@ void goto_symext::resume_symex_from_saved_state(
 void goto_symext::symex_instruction_range(
   statet &state,
   const goto_functionst &goto_functions,
+  const irep_idt &function_identifier,
   const goto_programt::const_targett first,
   const goto_programt::const_targett limit)
 {
   symex_instruction_range(
-    state, get_function_from_goto_functions(goto_functions), first, limit);
+    state,
+    get_function_from_goto_functions(goto_functions),
+    function_identifier,
+    first,
+    limit);
 }
 
 void goto_symext::symex_instruction_range(
   statet &state,
   const get_goto_functiont &get_goto_function,
+  const irep_idt &function_identifier,
   const goto_programt::const_targett first,
   const goto_programt::const_targett limit)
 {
-  initialize_entry_point(state, get_goto_function, first, limit);
+  initialize_entry_point(
+    state, get_goto_function, function_identifier, first, limit);
   ns = namespacet(outer_symbol_table, state.symbol_table);
-  while(state.source.pc->function!=limit->function || state.source.pc!=limit)
+  while(state.source.function != limit->function || state.source.pc != limit)
     symex_threaded_step(state, get_goto_function);
 }
 
@@ -296,6 +304,7 @@ void goto_symext::symex_from_entry_point_of(
   initialize_entry_point(
     state,
     get_goto_function,
+    goto_functionst::entry_point(),
     start_function->body.instructions.begin(),
     prev(start_function->body.instructions.end()));
 
diff --git a/src/goto-symex/symex_target.h b/src/goto-symex/symex_target.h
index 82fb5f0433d..c6d7ed2da01 100644
--- a/src/goto-symex/symex_target.h
+++ b/src/goto-symex/symex_target.h
@@ -29,27 +29,26 @@ class symex_targett
   struct sourcet
   {
     unsigned thread_nr;
+    irep_idt function;
     goto_programt::const_targett pc;
     bool is_set;
 
-    sourcet():
-      thread_nr(0),
-      is_set(false)
+    sourcet() : thread_nr(0), function(irep_idt()), is_set(false)
     {
     }
 
-    explicit sourcet(
-      goto_programt::const_targett _pc):
-      thread_nr(0),
-      pc(_pc),
-      is_set(true)
+    sourcet(const irep_idt &_function, goto_programt::const_targett _pc)
+      : thread_nr(0), function(_function), pc(_pc), is_set(true)
     {
     }
 
-    explicit sourcet(const goto_programt &_goto_program):
-      thread_nr(0),
-      pc(_goto_program.instructions.begin()),
-      is_set(true)
+    explicit sourcet(
+      const irep_idt &_function,
+      const goto_programt &_goto_program)
+      : thread_nr(0),
+        function(_function),
+        pc(_goto_program.instructions.begin()),
+        is_set(true)
     {
     }
   };
@@ -111,7 +110,6 @@ class symex_targett
   // record return from a function
   virtual void function_return(
     const exprt &guard,
-    const irep_idt &function_identifier,
     const sourcet &source)=0;
 
   // just record a location
diff --git a/src/goto-symex/symex_target_equation.cpp b/src/goto-symex/symex_target_equation.cpp
index 3a6509b031a..b11d396d947 100644
--- a/src/goto-symex/symex_target_equation.cpp
+++ b/src/goto-symex/symex_target_equation.cpp
@@ -219,7 +219,7 @@ void symex_target_equationt::function_call(
   SSA_step.guard = guard;
   SSA_step.type = goto_trace_stept::typet::FUNCTION_CALL;
   SSA_step.source = source;
-  SSA_step.function_identifier = function_identifier;
+  SSA_step.called_function = function_identifier;
   SSA_step.ssa_function_arguments = ssa_function_arguments;
 
   merge_ireps(SSA_step);
@@ -228,7 +228,6 @@ void symex_target_equationt::function_call(
 /// just record a location
 void symex_target_equationt::function_return(
   const exprt &guard,
-  const irep_idt &function_identifier,
   const sourcet &source)
 {
   SSA_steps.push_back(SSA_stept());
@@ -237,7 +236,6 @@ void symex_target_equationt::function_return(
   SSA_step.guard = guard;
   SSA_step.type = goto_trace_stept::typet::FUNCTION_RETURN;
   SSA_step.source = source;
-  SSA_step.function_identifier = function_identifier;
 
   merge_ireps(SSA_step);
 }
@@ -776,10 +774,10 @@ void symex_target_equationt::SSA_stept::output(
   switch(type)
   {
   case goto_trace_stept::typet::ASSERT:
-    out << "ASSERT " << from_expr(ns, source.pc->function, cond_expr) << '\n';
+    out << "ASSERT " << from_expr(ns, source.function, cond_expr) << '\n';
     break;
   case goto_trace_stept::typet::ASSUME:
-    out << "ASSUME " << from_expr(ns, source.pc->function, cond_expr) << '\n';
+    out << "ASSUME " << from_expr(ns, source.function, cond_expr) << '\n';
     break;
   case goto_trace_stept::typet::LOCATION:
     out << "LOCATION" << '\n'; break;
@@ -790,7 +788,7 @@ void symex_target_equationt::SSA_stept::output(
 
   case goto_trace_stept::typet::DECL:
     out << "DECL" << '\n';
-    out << from_expr(ns, source.pc->function, ssa_lhs) << '\n';
+    out << from_expr(ns, source.function, ssa_lhs) << '\n';
     break;
 
   case goto_trace_stept::typet::ASSIGNMENT:
@@ -844,22 +842,22 @@ void symex_target_equationt::SSA_stept::output(
   case goto_trace_stept::typet::MEMORY_BARRIER:
     out << "MEMORY_BARRIER\n"; break;
   case goto_trace_stept::typet::GOTO:
-    out << "IF " << from_expr(ns, source.pc->function, cond_expr) << " GOTO\n";
+    out << "IF " << from_expr(ns, source.function, cond_expr) << " GOTO\n";
     break;
 
   default: UNREACHABLE;
   }
 
   if(is_assert() || is_assume() || is_assignment() || is_constraint())
-    out << from_expr(ns, source.pc->function, cond_expr) << '\n';
+    out << from_expr(ns, source.function, cond_expr) << '\n';
 
   if(is_assert() || is_constraint())
     out << comment << '\n';
 
   if(is_shared_read() || is_shared_write())
-    out << from_expr(ns, source.pc->function, ssa_lhs) << '\n';
+    out << from_expr(ns, source.function, ssa_lhs) << '\n';
 
-  out << "Guard: " << from_expr(ns, source.pc->function, guard) << '\n';
+  out << "Guard: " << from_expr(ns, source.function, guard) << '\n';
 }
 
 void symex_target_equationt::SSA_stept::output(std::ostream &out) const
diff --git a/src/goto-symex/symex_target_equation.h b/src/goto-symex/symex_target_equation.h
index 975c1e8f44a..3e7c7c1e470 100644
--- a/src/goto-symex/symex_target_equation.h
+++ b/src/goto-symex/symex_target_equation.h
@@ -81,7 +81,6 @@ class symex_target_equationt:public symex_targett
   // record return from a function
   virtual void function_return(
     const exprt &guard,
-    const irep_idt &function_identifier,
     const sourcet &source);
 
   // just record a location
@@ -231,8 +230,8 @@ class symex_target_equationt:public symex_targett
     std::list<exprt> io_args;
     std::list<exprt> converted_io_args;
 
-    // for function call/return
-    irep_idt function_identifier;
+    // for function calls: the function that is called
+    irep_idt called_function;
 
     // for function calls
     std::vector<exprt> ssa_function_arguments,