diff --git a/regression/goto-instrument/value-set-fi-fp-removal/test.c b/regression/goto-instrument/value-set-fi-fp-removal/test.c
new file mode 100644
index 00000000000..ce8b1b1af08
--- /dev/null
+++ b/regression/goto-instrument/value-set-fi-fp-removal/test.c
@@ -0,0 +1,20 @@
+#include <assert.h>
+
+typedef void (*fp_t)();
+
+void f()
+{
+}
+
+void g()
+{
+}
+
+int main(void)
+{
+  fp_t fp = f;
+  fp();
+
+  // this would fool an analysis that looks for functions whose address is taken
+  fp_t other_fp = g;
+}
diff --git a/regression/goto-instrument/value-set-fi-fp-removal/test.desc b/regression/goto-instrument/value-set-fi-fp-removal/test.desc
new file mode 100644
index 00000000000..5de3977d7aa
--- /dev/null
+++ b/regression/goto-instrument/value-set-fi-fp-removal/test.desc
@@ -0,0 +1,12 @@
+CORE
+test.c
+--value-set-fi-fp-removal
+^EXIT=0$
+^SIGNAL=0$
+^  function: f$
+--
+^  function: g$
+--
+This test checks that the value-set-fi-based function pointer removal
+precisely identifies the function to call for a particular function pointer
+call.
diff --git a/regression/goto-instrument/value-set-fi-fp-removal2/test.c b/regression/goto-instrument/value-set-fi-fp-removal2/test.c
new file mode 100644
index 00000000000..0aad1b22e69
--- /dev/null
+++ b/regression/goto-instrument/value-set-fi-fp-removal2/test.c
@@ -0,0 +1,27 @@
+
+typedef void (*fp_t)(int, int);
+
+void add(int a, int b)
+{
+}
+void subtract(int a, int b)
+{
+}
+void multiply(int a, int b)
+{
+}
+
+int main()
+{
+  // fun_ptr_arr is an array of function pointers
+  void (*fun_ptr_arr[])(int, int) = {add, subtract, add};
+
+  // Multiply should not be added into the value set
+  fp_t other_fp = multiply;
+  void (*fun_ptr_arr2[])(int, int) = {multiply, subtract, add};
+
+  // the fp removal over-approximates and assumes this could be any pointer in the array
+  (*fun_ptr_arr[0])(1, 1);
+
+  return 0;
+}
diff --git a/regression/goto-instrument/value-set-fi-fp-removal2/test.desc b/regression/goto-instrument/value-set-fi-fp-removal2/test.desc
new file mode 100644
index 00000000000..382f1d52a0c
--- /dev/null
+++ b/regression/goto-instrument/value-set-fi-fp-removal2/test.desc
@@ -0,0 +1,13 @@
+CORE
+test.c
+--value-set-fi-fp-removal
+^EXIT=0$
+^SIGNAL=0$
+^  function: add$
+^  function: subtract$
+--
+^  function: multiply$
+--
+This test checks that the value-set-fi-based function pointer removal
+precisely identifies the function to call for a particular function pointer
+call.
diff --git a/regression/goto-instrument/value-set-fi-fp-removal3/test.c b/regression/goto-instrument/value-set-fi-fp-removal3/test.c
new file mode 100644
index 00000000000..2d4d897a252
--- /dev/null
+++ b/regression/goto-instrument/value-set-fi-fp-removal3/test.c
@@ -0,0 +1,32 @@
+typedef void (*fp_t)(int, int);
+
+void add(int a, int b)
+{
+}
+void subtract(int a, int b)
+{
+}
+void multiply(int a, int b)
+{
+}
+
+int main()
+{
+  // fun_ptr_arr is an array of function pointers
+  struct my_struct
+  {
+    fp_t first_pointer;
+    fp_t second_pointer;
+  } struct1;
+
+  struct1.first_pointer = add;
+
+  // Multiply and subtract should not be added into the value set
+  fp_t other_fp = multiply;
+  struct1.second_pointer = subtract;
+
+  // this pointer can only be "add"
+  struct1.first_pointer(1, 1);
+
+  return 0;
+}
diff --git a/regression/goto-instrument/value-set-fi-fp-removal3/test.desc b/regression/goto-instrument/value-set-fi-fp-removal3/test.desc
new file mode 100644
index 00000000000..de947f49fc7
--- /dev/null
+++ b/regression/goto-instrument/value-set-fi-fp-removal3/test.desc
@@ -0,0 +1,13 @@
+CORE
+test.c
+--value-set-fi-fp-removal
+^EXIT=0$
+^SIGNAL=0$
+^  function: add$
+--
+^  function: multiply$
+^  function: subtract$
+--
+This test checks that the value-set-fi-based function pointer removal
+precisely identifies the function to call for a particular function pointer
+call.
diff --git a/regression/goto-instrument/value-set-fi-fp-removal4/test.c b/regression/goto-instrument/value-set-fi-fp-removal4/test.c
new file mode 100644
index 00000000000..b99e6c73e8e
--- /dev/null
+++ b/regression/goto-instrument/value-set-fi-fp-removal4/test.c
@@ -0,0 +1,21 @@
+#include <assert.h>
+
+typedef void (*fp_t)();
+
+void f()
+{
+}
+
+void g()
+{
+}
+
+int main(void)
+{
+  // the value set for fp is empty, defaults to standard function pointer removal behaviour
+  fp_t other_fp = g;
+  other_fp = f;
+
+  fp_t fp;
+  fp();
+}
diff --git a/regression/goto-instrument/value-set-fi-fp-removal4/test.desc b/regression/goto-instrument/value-set-fi-fp-removal4/test.desc
new file mode 100644
index 00000000000..95cc354a7a2
--- /dev/null
+++ b/regression/goto-instrument/value-set-fi-fp-removal4/test.desc
@@ -0,0 +1,10 @@
+CORE
+test.c
+--value-set-fi-fp-removal
+^EXIT=0$
+^SIGNAL=0$
+^file test.c line 20 function main: replacing function pointer by 2 possible targets$
+--
+This test checks that the value-set-fi-based function pointer removal
+precisely identifies the function to call for a particular function pointer
+call.
diff --git a/regression/goto-instrument/value-set-fi-fp-removal5/test.c b/regression/goto-instrument/value-set-fi-fp-removal5/test.c
new file mode 100644
index 00000000000..05e3a5ab1c3
--- /dev/null
+++ b/regression/goto-instrument/value-set-fi-fp-removal5/test.c
@@ -0,0 +1,20 @@
+#include <assert.h>
+
+typedef void (*fp_t)();
+
+void f(int x)
+{
+}
+
+void g(int y)
+{
+}
+
+int main(void)
+{
+  // the value set is empty, defaults to standard function pointer removal behaviour
+  fp_t other_fp = g;
+
+  fp_t fp;
+  fp();
+}
diff --git a/regression/goto-instrument/value-set-fi-fp-removal5/test.desc b/regression/goto-instrument/value-set-fi-fp-removal5/test.desc
new file mode 100644
index 00000000000..637e25cc835
--- /dev/null
+++ b/regression/goto-instrument/value-set-fi-fp-removal5/test.desc
@@ -0,0 +1,10 @@
+CORE
+test.c
+--value-set-fi-fp-removal
+^EXIT=0$
+^SIGNAL=0$
+^file test.c line 19 function main: replacing function pointer by 0 possible targets$
+--
+This test checks that the value-set-fi-based function pointer removal
+precisely identifies the function to call for a particular function pointer
+call.
diff --git a/regression/goto-instrument/value-set-fi-fp-removal6/test.c b/regression/goto-instrument/value-set-fi-fp-removal6/test.c
new file mode 100644
index 00000000000..2d2990bd1ca
--- /dev/null
+++ b/regression/goto-instrument/value-set-fi-fp-removal6/test.c
@@ -0,0 +1,19 @@
+#include <assert.h>
+
+typedef void (*fp_t)(void);
+
+void f()
+{
+}
+
+void g()
+{
+}
+
+int main(void)
+{
+  fp_t fp = f;
+  fp_t decoy_fp = g;
+  fp_t *ptr_to_func_ptr = &fp; // a pointer to a function pointer
+  (*ptr_to_func_ptr)();
+}
diff --git a/regression/goto-instrument/value-set-fi-fp-removal6/test.desc b/regression/goto-instrument/value-set-fi-fp-removal6/test.desc
new file mode 100644
index 00000000000..5de3977d7aa
--- /dev/null
+++ b/regression/goto-instrument/value-set-fi-fp-removal6/test.desc
@@ -0,0 +1,12 @@
+CORE
+test.c
+--value-set-fi-fp-removal
+^EXIT=0$
+^SIGNAL=0$
+^  function: f$
+--
+^  function: g$
+--
+This test checks that the value-set-fi-based function pointer removal
+precisely identifies the function to call for a particular function pointer
+call.
diff --git a/src/goto-instrument/Makefile b/src/goto-instrument/Makefile
index 00cb2a9db98..8cd5b3936b9 100644
--- a/src/goto-instrument/Makefile
+++ b/src/goto-instrument/Makefile
@@ -67,6 +67,7 @@ SRC = accelerate/accelerate.cpp \
       uninitialized.cpp \
       unwind.cpp \
       unwindset.cpp \
+      value_set_fi_fp_removal.cpp \
       wmm/abstract_event.cpp \
       wmm/cycle_collection.cpp \
       wmm/data_dp.cpp \
diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp
index 9a3d00a69b4..7733e4f0750 100644
--- a/src/goto-instrument/goto_instrument_parse_options.cpp
+++ b/src/goto-instrument/goto_instrument_parse_options.cpp
@@ -54,6 +54,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <pointer-analysis/goto_program_dereference.h>
 #include <pointer-analysis/show_value_sets.h>
 #include <pointer-analysis/value_set_analysis.h>
+#include <pointer-analysis/value_set_analysis_fi.h>
 
 #include <analyses/call_graph.h>
 #include <analyses/constant_propagator.h>
@@ -111,6 +112,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "undefined_functions.h"
 #include "uninitialized.h"
 #include "unwind.h"
+#include "value_set_fi_fp_removal.h"
 #include "wmm/weak_memory.h"
 
 /// invoke main modules
@@ -1198,6 +1200,12 @@ void goto_instrument_parse_optionst::instrument_goto_program()
         exit(CPROVER_EXIT_USAGE_ERROR);
   }
 
+  if(cmdline.isset("value-set-fi-fp-removal"))
+  {
+    value_set_fi_fp_removal(goto_model, ui_message_handler);
+    do_indirect_call_and_rtti_removal();
+  }
+
   // replace function pointers, if explicitly requested
   if(cmdline.isset("remove-function-pointers"))
   {
@@ -1867,6 +1875,9 @@ void goto_instrument_parse_optionst::help()
     " --no-caching                 disable caching of intermediate results during transitive function inlining\n" // NOLINT(*)
     " --log <file>                 log in json format which code segments were inlined, use with --function-inline\n" // NOLINT(*)
     " --remove-function-pointers   replace function pointers by case statement over function calls\n" // NOLINT(*)
+    " --value-set-fi-fp-removal    build flow-insensitive value set and replace function pointers by a case statement\n" // NOLINT(*)
+    "                              over the possible assignments. If the set of possible assignments is empty the function pointer\n" // NOLINT(*)
+    "                              is removed using the standard remove-function-pointers pass. \n" // NOLINT(*)
     HELP_RESTRICT_FUNCTION_POINTER
     HELP_REMOVE_CALLS_NO_BODY
     HELP_REMOVE_CONST_FUNCTION_POINTERS
diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h
index a9858a30c4a..353b8a1e8f1 100644
--- a/src/goto-instrument/goto_instrument_parse_options.h
+++ b/src/goto-instrument/goto_instrument_parse_options.h
@@ -83,6 +83,7 @@ Author: Daniel Kroening, kroening@kroening.com
   "(full-slice)(reachability-slice)(slice-global-inits)" \
   "(fp-reachability-slice):" \
   "(inline)(partial-inline)(function-inline):(log):(no-caching)" \
+  "(value-set-fi-fp-removal)" \
   OPT_REMOVE_CONST_FUNCTION_POINTERS \
   "(print-internal-representation)" \
   "(remove-function-pointers)" \
diff --git a/src/goto-instrument/value_set_fi_fp_removal.cpp b/src/goto-instrument/value_set_fi_fp_removal.cpp
new file mode 100644
index 00000000000..f7b05375dbd
--- /dev/null
+++ b/src/goto-instrument/value_set_fi_fp_removal.cpp
@@ -0,0 +1,247 @@
+/*******************************************************************\
+
+Module: value_set_fi_Fp_removal
+
+Author: Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+#include "value_set_fi_fp_removal.h"
+
+#include <goto-programs/goto_model.h>
+#include <goto-programs/remove_function_pointers.h>
+
+#include <pointer-analysis/value_set_analysis_fi.h>
+
+#include <util/base_type.h>
+#include <util/c_types.h>
+#include <util/expanding_vector.h>
+#include <util/fresh_symbol.h>
+#include <util/message.h>
+#include <util/namespace.h>
+#include <util/std_code.h>
+#include <util/union_find.h>
+
+#ifdef USE_STD_STRING
+#  include <util/dstring.h>
+#endif
+
+void fix_argument_types(
+  code_function_callt &function_call,
+  const namespacet &ns)
+{
+  const code_typet &code_type =
+    to_code_type(ns.follow(function_call.function().type()));
+
+  const code_typet::parameterst &function_parameters = code_type.parameters();
+
+  code_function_callt::argumentst &call_arguments = function_call.arguments();
+
+  for(std::size_t i = 0; i < function_parameters.size(); i++)
+  {
+    // casting pointers might result in more arguments than function parameters
+    if(i < call_arguments.size())
+    {
+      call_arguments[i] = typecast_exprt::conditional_cast(
+        call_arguments[i], function_parameters[i].type());
+    }
+  }
+}
+
+void fix_return_type(
+  code_function_callt &function_call,
+  goto_programt &dest,
+  goto_modelt &goto_model)
+{
+  // are we returning anything at all?
+  if(function_call.lhs().is_nil())
+    return;
+
+  const namespacet ns(goto_model.symbol_table);
+
+  const code_typet &code_type =
+    to_code_type(ns.follow(function_call.function().type()));
+
+  // type already ok?
+  if(function_call.lhs().type() == code_type.return_type())
+    return;
+
+  const symbolt &function_symbol =
+    ns.lookup(to_symbol_expr(function_call.function()).get_identifier());
+
+  symbolt &tmp_symbol = get_fresh_aux_symbol(
+    code_type.return_type(),
+    id2string(function_call.source_location().get_function()),
+    "tmp_return_val_" + id2string(function_symbol.base_name),
+    function_call.source_location(),
+    function_symbol.mode,
+    goto_model.symbol_table);
+
+  const symbol_exprt tmp_symbol_expr = tmp_symbol.symbol_expr();
+
+  exprt old_lhs = function_call.lhs();
+  function_call.lhs() = tmp_symbol_expr;
+
+  dest.add(goto_programt::make_assignment(
+    code_assignt(old_lhs, typecast_exprt(tmp_symbol_expr, old_lhs.type()))));
+}
+
+void remove_function_pointer(
+  goto_programt &goto_program,
+  goto_programt::targett target,
+  const std::set<symbol_exprt> &functions,
+  goto_modelt &goto_model)
+{
+  const code_function_callt &code = to_code_function_call(target->code);
+
+  const exprt &function = code.function();
+  PRECONDITION(function.id() == ID_dereference);
+
+  // this better have the right type
+  code_typet call_type = to_code_type(function.type());
+
+  // refine the type in case the forward declaration was incomplete
+  if(call_type.has_ellipsis() && call_type.parameters().empty())
+  {
+    call_type.remove_ellipsis();
+    forall_expr(it, code.arguments())
+      call_type.parameters().push_back(code_typet::parametert(it->type()));
+  }
+
+  const exprt &pointer = to_dereference_expr(function).pointer();
+
+  // the final target is a skip
+  goto_programt final_skip;
+
+  goto_programt::targett t_final = final_skip.add_instruction();
+  t_final->make_skip();
+
+  // build the calls and gotos
+
+  goto_programt new_code_calls;
+  goto_programt new_code_gotos;
+
+  for(const auto &fun : functions)
+  {
+    // call function
+    goto_programt::targett t1 = new_code_calls.add_instruction();
+    t1->make_function_call(code);
+    to_code_function_call(t1->code).function() = fun;
+
+    // the signature of the function might not match precisely
+    const namespacet ns(goto_model.symbol_table);
+    fix_argument_types(to_code_function_call(t1->code), ns);
+    fix_return_type(
+      to_code_function_call(t1->code), new_code_calls, goto_model);
+
+    // goto final
+    goto_programt::targett t3 = new_code_calls.add_instruction();
+    t3->make_goto(t_final, true_exprt());
+
+    // goto to call
+    address_of_exprt address_of(fun, pointer_type(fun.type()));
+
+    goto_programt::targett t4 = new_code_gotos.add_instruction();
+    t4->make_goto(
+      t1,
+      equal_exprt(
+        pointer, typecast_exprt::conditional_cast(address_of, pointer.type())));
+  }
+
+  goto_programt::targett t = new_code_gotos.add_instruction();
+  t->make_assertion(false_exprt());
+  t->source_location.set_property_class("pointer dereference");
+  t->source_location.set_comment("invalid function pointer");
+
+  goto_programt new_code;
+
+  // patch them all together
+  new_code.destructive_append(new_code_gotos);
+  new_code.destructive_append(new_code_calls);
+  new_code.destructive_append(final_skip);
+
+  // set locations
+  for(auto &instruction : new_code.instructions)
+  {
+    irep_idt property_class = instruction.source_location.get_property_class();
+    irep_idt comment = instruction.source_location.get_comment();
+    instruction.source_location = target->source_location;
+    if(!property_class.empty())
+      instruction.source_location.set_property_class(property_class);
+    if(!comment.empty())
+      instruction.source_location.set_comment(comment);
+  }
+
+  goto_programt::targett next_target = target;
+  next_target++;
+
+  goto_program.destructive_insert(next_target, new_code);
+
+  // We preserve the original dereferencing to possibly catch
+  // further pointer-related errors.
+  code_expressiont code_expression(function);
+  code_expression.add_source_location() = function.source_location();
+  target->code.swap(code_expression);
+  target->type = OTHER;
+}
+
+void value_set_fi_fp_removal(
+  goto_modelt &goto_model,
+  message_handlert &message_handler)
+{
+  messaget message(message_handler);
+  message.status() << "Doing FI value set analysis" << messaget::eom;
+
+  const namespacet ns(goto_model.symbol_table);
+  value_set_analysis_fit value_sets(ns);
+  value_sets(goto_model.goto_functions);
+
+  message.status() << "Instrumenting" << messaget::eom;
+
+  // now replace aliases by addresses
+  for(auto &f : goto_model.goto_functions.function_map)
+  {
+    for(auto target = f.second.body.instructions.begin();
+        target != f.second.body.instructions.end();
+        target++)
+    {
+      if(target->is_function_call())
+      {
+        const auto &call = to_code_function_call(target->code);
+        if(call.function().id() == ID_dereference)
+        {
+          message.status() << "CALL at " << target->source_location << ":"
+                           << messaget::eom;
+
+          const auto &pointer = to_dereference_expr(call.function()).pointer();
+          std::list<exprt> addresses;
+          value_sets.get_values(f.first, target, pointer, addresses);
+
+          std::set<symbol_exprt> functions;
+
+          for(const auto &address : addresses)
+          {
+            // is this a plain function address?
+            // strip leading '&'
+            if(address.id() == ID_object_descriptor)
+            {
+              const auto &od = to_object_descriptor_expr(address);
+              const auto &object = od.object();
+              if(object.type().id() == ID_code && object.id() == ID_symbol)
+                functions.insert(to_symbol_expr(object));
+            }
+          }
+
+          for(const auto &f : functions)
+            message.status()
+              << "  function: " << f.get_identifier() << messaget::eom;
+
+          if(functions.size() > 0)
+            remove_function_pointer(
+              f.second.body, target, functions, goto_model);
+        }
+      }
+    }
+  }
+  goto_model.goto_functions.update();
+}
diff --git a/src/goto-instrument/value_set_fi_fp_removal.h b/src/goto-instrument/value_set_fi_fp_removal.h
new file mode 100644
index 00000000000..a2427267971
--- /dev/null
+++ b/src/goto-instrument/value_set_fi_fp_removal.h
@@ -0,0 +1,28 @@
+/*******************************************************************\
+
+Module: value_set_fi_Fp_removal
+
+Author: Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+/// \file
+/// flow insensitive value set function pointer removal
+
+#ifndef CPROVER_GOTO_INSTRUMENT_VALUE_SET_FI_FP_REMOVAL_H
+#define CPROVER_GOTO_INSTRUMENT_VALUE_SET_FI_FP_REMOVAL_H
+
+class goto_modelt;
+class message_handlert;
+/// Builds the flow-insensitive value set for all function pointers
+/// and replaces function pointers with a non-deterministic switch
+/// between this set. If the set is empty, the function pointer is
+/// not removed. Thus remove_function_pointers should be run after this to
+// guarantee removal of all function pointers.
+/// \param goto_model: goto model to be modified
+/// \param message_handler: message handler for status output
+void value_set_fi_fp_removal(
+  goto_modelt &goto_model,
+  message_handlert &message_handler);
+
+#endif // CPROVER_GOTO_INSTRUMENT_VALUE_SET_FI_FP_REMOVAL_H