diff --git a/regression/cbmc/Function_Pointer_Init_No_Candidate/main.c b/regression/cbmc/Function_Pointer_Init_No_Candidate/main.c
new file mode 100644
index 00000000000..c19c7f2dee9
--- /dev/null
+++ b/regression/cbmc/Function_Pointer_Init_No_Candidate/main.c
@@ -0,0 +1,13 @@
+#include <assert.h>
+
+typedef int (*other_function_type)(int n);
+
+void foo(other_function_type other_function)
+{
+  // returning from the function call is unreachable -> the following assertion
+  //   should succeed
+  // requesting `pointer-check` will then catch the fact that there is no valid
+  //   candidate function to call resulting in an invalid function pointer
+  //   failure
+  assert(other_function(4) > 5);
+}
diff --git a/regression/cbmc/Function_Pointer_Init_No_Candidate/test.desc b/regression/cbmc/Function_Pointer_Init_No_Candidate/test.desc
new file mode 100644
index 00000000000..fd055d8d613
--- /dev/null
+++ b/regression/cbmc/Function_Pointer_Init_No_Candidate/test.desc
@@ -0,0 +1,10 @@
+CORE
+main.c
+--function foo --pointer-check
+^\[foo.assertion.\d+\] line \d+ assertion other_function\(4\) > 5: SUCCESS$
+^\[foo.pointer_dereference.\d+\] line \d+ invalid function pointer: FAILURE$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED
+--
+^warning: ignoring
diff --git a/regression/cbmc/Function_Pointer_Init_One_Candidate/main.c b/regression/cbmc/Function_Pointer_Init_One_Candidate/main.c
new file mode 100644
index 00000000000..177a41f537c
--- /dev/null
+++ b/regression/cbmc/Function_Pointer_Init_One_Candidate/main.c
@@ -0,0 +1,22 @@
+#include <assert.h>
+
+int identity(int n)
+{
+  return n;
+}
+
+typedef int (*other_function_type)(int n);
+
+void foo(other_function_type other_function)
+{
+  // the following assertion is reachable and should fail (the only candidate is identity)
+  assert(other_function(4) == 5);
+  // the following assertion should succeed
+  assert(other_function(4) == 4);
+}
+
+int main()
+{
+  foo(&identity);
+  return 0;
+}
diff --git a/regression/cbmc/Function_Pointer_Init_One_Candidate/test.desc b/regression/cbmc/Function_Pointer_Init_One_Candidate/test.desc
new file mode 100644
index 00000000000..b0e774c5ed5
--- /dev/null
+++ b/regression/cbmc/Function_Pointer_Init_One_Candidate/test.desc
@@ -0,0 +1,10 @@
+CORE
+main.c
+--function foo
+^\[foo.assertion.\d+\] line \d+ assertion other_function\(4\) == 5: FAILURE$
+^\[foo.assertion.\d+\] line \d+ assertion other_function\(4\) == 4: SUCCESS$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED
+--
+^warning: ignoring
diff --git a/regression/cbmc/Function_Pointer_Init_Two_Candidates/main.c b/regression/cbmc/Function_Pointer_Init_Two_Candidates/main.c
new file mode 100644
index 00000000000..d9b7869bc7c
--- /dev/null
+++ b/regression/cbmc/Function_Pointer_Init_Two_Candidates/main.c
@@ -0,0 +1,27 @@
+#include <assert.h>
+
+int identity(int n)
+{
+  return n;
+}
+int increment(int n)
+{
+  return n + 1;
+}
+
+typedef int (*other_function_type)(int n);
+
+void foo(other_function_type other_function)
+{
+  // the following assertion is reachable and should fail (because of the identity case)
+  assert(other_function(4) == 5);
+  // the following assertion should succeed (satisfied by both candidates)
+  assert(other_function(4) >= 4);
+}
+
+int main()
+{
+  foo(&identity);
+  foo(&increment);
+  return 0;
+}
diff --git a/regression/cbmc/Function_Pointer_Init_Two_Candidates/test.desc b/regression/cbmc/Function_Pointer_Init_Two_Candidates/test.desc
new file mode 100644
index 00000000000..8becf23aa28
--- /dev/null
+++ b/regression/cbmc/Function_Pointer_Init_Two_Candidates/test.desc
@@ -0,0 +1,10 @@
+CORE
+main.c
+--function foo
+^\[foo.assertion.\d+\] line \d+ assertion other_function\(4\) == 5: FAILURE$
+^\[foo.assertion.\d+\] line \d+ assertion other_function\(4\) >= 4: SUCCESS$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED
+--
+^warning: ignoring
diff --git a/src/ansi-c/c_nondet_symbol_factory.cpp b/src/ansi-c/c_nondet_symbol_factory.cpp
index 5e91a9a2a73..1a0ab2c3487 100644
--- a/src/ansi-c/c_nondet_symbol_factory.cpp
+++ b/src/ansi-c/c_nondet_symbol_factory.cpp
@@ -54,6 +54,16 @@ void symbol_factoryt::gen_nondet_init(
     const pointer_typet &pointer_type=to_pointer_type(type);
     const typet &subtype = pointer_type.subtype();
 
+    if(subtype.id() == ID_code)
+    {
+      // Handle the pointer-to-code case separately:
+      // leave as nondet_ptr to allow `remove_function_pointers`
+      // to replace the pointer.
+      assignments.add(
+        code_assignt{expr, side_effect_expr_nondett{pointer_type, loc}});
+      return;
+    }
+
     if(subtype.id() == ID_struct_tag)
     {
       const irep_idt struct_tag = to_struct_tag_type(subtype).get_identifier();