diff --git a/src/goto-programs/remove_function_pointers.cpp b/src/goto-programs/remove_function_pointers.cpp
index d4ab20475d5..846371c0ce7 100644
--- a/src/goto-programs/remove_function_pointers.cpp
+++ b/src/goto-programs/remove_function_pointers.cpp
@@ -44,6 +44,20 @@ class remove_function_pointerst:public messaget
 
   bool remove_function_pointers(goto_programt &goto_program);
 
+  // a set of function symbols
+  using functionst = remove_const_function_pointerst::functionst;
+
+  /// Replace a call to a dynamic function at location
+  /// target in the given goto-program by a case-split
+  /// over a given set of functions
+  /// \param goto_program The goto program that contains target
+  /// \param target location with function call with function pointer
+  /// \param functions The set of functions to consider
+  void remove_function_pointer(
+    goto_programt &goto_program,
+    goto_programt::targett target,
+    const functionst &functions);
+
 protected:
   const namespacet ns;
   symbol_tablet &symbol_table;
@@ -57,6 +71,11 @@ class remove_function_pointerst:public messaget
   // --remove-const-function-pointers instead of --remove-function-pointers
   bool only_resolve_const_fps;
 
+  /// Replace a call to a dynamic function at location
+  /// target in the given goto-program by determining
+  /// functions that have a compatible signature
+  /// \param goto_program The goto program that contains target
+  /// \param target location with function call with function pointer
   void remove_function_pointer(
     goto_programt &goto_program,
     goto_programt::targett target);
@@ -348,6 +367,19 @@ void remove_function_pointerst::remove_function_pointer(
     }
   }
 
+  remove_function_pointer(goto_program, target, functions);
+}
+
+void remove_function_pointerst::remove_function_pointer(
+  goto_programt &goto_program,
+  goto_programt::targett target,
+  const functionst &functions)
+{
+  const code_function_callt &code = to_code_function_call(target->code);
+
+  const exprt &function = code.function();
+  const exprt &pointer = to_dereference_expr(function).pointer();
+
   // the final target is a skip
   goto_programt final_skip;