diff --git a/regression/cbmc/Function_Pointer18/main.c b/regression/cbmc/Function_Pointer18/main.c
new file mode 100644
index 00000000000..3720f5806c6
--- /dev/null
+++ b/regression/cbmc/Function_Pointer18/main.c
@@ -0,0 +1,34 @@
+// f is set to 0 -> does not point to either f1 or f2
+#include <assert.h>
+
+typedef int (*f_ptr)(int);
+
+extern f_ptr f;
+
+int f1(int j);
+int f2(int i);
+
+int f1(int j)
+{
+  f = &f2;
+  return 1;
+}
+int f2(int i)
+{
+  assert(0);
+  return 2;
+}
+
+f_ptr f = 0;
+
+int main()
+{
+  int x = 0;
+
+  x = f(x);
+  assert(x == 1);
+  x = f(x);
+  assert(x == 2);
+
+  return 0;
+}
diff --git a/regression/cbmc/Function_Pointer18/test.desc b/regression/cbmc/Function_Pointer18/test.desc
new file mode 100644
index 00000000000..e255c4accf3
--- /dev/null
+++ b/regression/cbmc/Function_Pointer18/test.desc
@@ -0,0 +1,11 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+\[f2.assertion.1\] line [0-9]+ assertion 0: SUCCESS
+\[main.assertion.1\] line [0-9]+ assertion x == 1: SUCCESS
+\[main.assertion.2\] line [0-9]+ assertion x == 2: SUCCESS
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/src/goto-programs/remove_function_pointers.cpp b/src/goto-programs/remove_function_pointers.cpp
index 8f5bb55e277..3c579f386b1 100644
--- a/src/goto-programs/remove_function_pointers.cpp
+++ b/src/goto-programs/remove_function_pointers.cpp
@@ -416,6 +416,7 @@ void remove_function_pointerst::remove_function_pointer(
     t->source_location.set_property_class("pointer dereference");
     t->source_location.set_comment("invalid function pointer");
   }
+  new_code_gotos.add(goto_programt::make_assumption(false_exprt()));
 
   goto_programt new_code;