diff --git a/regression/cbmc/Function_Pointer18/main.c b/regression/cbmc/Function_Pointer18/main.c
new file mode 100644
index 00000000000..befa7b67265
--- /dev/null
+++ b/regression/cbmc/Function_Pointer18/main.c
@@ -0,0 +1,13 @@
+void (*my_ptr)();
+
+void my_f()
+{
+  asm("mfence");
+  my_ptr=my_f;
+}
+
+int main()
+{
+  void (*nondet)();
+  nondet();
+}
diff --git a/regression/cbmc/Function_Pointer18/test.desc b/regression/cbmc/Function_Pointer18/test.desc
new file mode 100644
index 00000000000..c0bbb27f448
--- /dev/null
+++ b/regression/cbmc/Function_Pointer18/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--unwind 1
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring