diff --git a/regression/cbmc/function-return-no-body1/main.c b/regression/cbmc/function-return-no-body1/main.c
new file mode 100644
index 00000000000..bf0e0685d83
--- /dev/null
+++ b/regression/cbmc/function-return-no-body1/main.c
@@ -0,0 +1,9 @@
+#include <assert.h>
+
+void no_body();
+
+void main()
+{
+  no_body();
+  assert(0);
+}
diff --git a/regression/cbmc/function-return-no-body1/test.desc b/regression/cbmc/function-return-no-body1/test.desc
new file mode 100644
index 00000000000..fffcd09289b
--- /dev/null
+++ b/regression/cbmc/function-return-no-body1/test.desc
@@ -0,0 +1,11 @@
+CORE
+main.c
+--xml-ui
+activate-multi-line-match
+EXIT=10
+SIGNAL=0
+VERIFICATION FAILED
+<function_call hidden="false" step_nr="18" thread="0">\n\s*<function display_name="no_body" identifier="no_body">
+<function_return hidden="false" step_nr="19" thread="0">\n\s*<function display_name="no_body" identifier="no_body">
+--
+^warning: ignoring
diff --git a/src/goto-programs/json_goto_trace.cpp b/src/goto-programs/json_goto_trace.cpp
index 46b761530c1..2e27f766b5d 100644
--- a/src/goto-programs/json_goto_trace.cpp
+++ b/src/goto-programs/json_goto_trace.cpp
@@ -263,9 +263,7 @@ 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 irep_idt &function_identifier =
-    (step.type == goto_trace_stept::typet::FUNCTION_CALL) ? step.called_function
-                                                          : step.function_id;
+  const irep_idt &function_identifier = step.called_function;
 
   const symbolt &symbol = ns.lookup(function_identifier);
   json_call_return["function"] =
diff --git a/src/goto-programs/xml_goto_trace.cpp b/src/goto-programs/xml_goto_trace.cpp
index 61164356bef..4af88697d0f 100644
--- a/src/goto-programs/xml_goto_trace.cpp
+++ b/src/goto-programs/xml_goto_trace.cpp
@@ -186,11 +186,11 @@ void convert(
         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_id);
+        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(step.function_id));
+        xml_function.set_attribute("identifier", id2string(symbol.name));
         xml_function.new_element()=xml(symbol.location);
 
         if(xml_location.name!="")
diff --git a/src/goto-symex/symex_function_call.cpp b/src/goto-symex/symex_function_call.cpp
index c576ea72864..a28087c2003 100644
--- a/src/goto-symex/symex_function_call.cpp
+++ b/src/goto-symex/symex_function_call.cpp
@@ -286,7 +286,8 @@ void goto_symext::symex_function_call_code(
     no_body(identifier);
 
     // record the return
-    target.function_return(state.guard.as_expr(), state.source, hidden);
+    target.function_return(
+      state.guard.as_expr(), identifier, state.source, hidden);
 
     if(call.lhs().is_not_nil())
     {
@@ -374,7 +375,8 @@ void goto_symext::symex_end_of_function(statet &state)
   const bool hidden = state.top().hidden_function;
 
   // first record the return
-  target.function_return(state.guard.as_expr(), state.source, hidden);
+  target.function_return(
+    state.guard.as_expr(), state.source.function_id, state.source, hidden);
 
   // then get rid of the frame
   pop_frame(state);
diff --git a/src/goto-symex/symex_target.h b/src/goto-symex/symex_target.h
index ca1cb755e7c..3eddaf1dd8a 100644
--- a/src/goto-symex/symex_target.h
+++ b/src/goto-symex/symex_target.h
@@ -152,11 +152,15 @@ class symex_targett
 
   /// Record return from a function.
   /// \param guard: Precondition for returning from a function
+  /// \param function_id: Name of the function from which we return
   /// \param source: Pointer to location in the input GOTO program of this
   /// \param hidden: Should this step be recorded as hidden?
   ///  function return
-  virtual void
-  function_return(const exprt &guard, const sourcet &source, bool hidden) = 0;
+  virtual void function_return(
+    const exprt &guard,
+    const irep_idt &function_id,
+    const sourcet &source,
+    bool hidden) = 0;
 
   /// Record a location.
   /// \param guard: Precondition for reaching this location
diff --git a/src/goto-symex/symex_target_equation.cpp b/src/goto-symex/symex_target_equation.cpp
index 65afe8c2794..8075528bc09 100644
--- a/src/goto-symex/symex_target_equation.cpp
+++ b/src/goto-symex/symex_target_equation.cpp
@@ -204,6 +204,7 @@ void symex_target_equationt::function_call(
 
 void symex_target_equationt::function_return(
   const exprt &guard,
+  const irep_idt &function_id,
   const sourcet &source,
   const bool hidden)
 {
@@ -211,6 +212,7 @@ void symex_target_equationt::function_return(
   SSA_stept &SSA_step=SSA_steps.back();
 
   SSA_step.guard = guard;
+  SSA_step.called_function = function_id;
   SSA_step.hidden = hidden;
 
   merge_ireps(SSA_step);
diff --git a/src/goto-symex/symex_target_equation.h b/src/goto-symex/symex_target_equation.h
index b563e980697..998a87959cd 100644
--- a/src/goto-symex/symex_target_equation.h
+++ b/src/goto-symex/symex_target_equation.h
@@ -85,8 +85,11 @@ class symex_target_equationt:public symex_targett
     bool hidden);
 
   /// \copydoc symex_targett::function_return()
-  virtual void
-  function_return(const exprt &guard, const sourcet &source, bool hidden);
+  virtual void function_return(
+    const exprt &guard,
+    const irep_idt &function_id,
+    const sourcet &source,
+    bool hidden);
 
   /// \copydoc symex_targett::location()
   virtual void location(