diff --git a/regression/cbmc/Function_Pointer19/main.c b/regression/cbmc/Function_Pointer19/main.c
new file mode 100644
index 00000000000..278fcbe1127
--- /dev/null
+++ b/regression/cbmc/Function_Pointer19/main.c
@@ -0,0 +1,51 @@
+#include <assert.h>
+
+struct PtrWrapperInner
+{
+  int *value;
+};
+
+struct PtrWrapper
+{
+  int *value;
+  struct PtrWrapperInner inner;
+};
+
+struct AltPtrWrapperInner
+{
+  int *value;
+};
+
+struct AltPtrWrapper
+{
+  unsigned int *value;
+  // A) Doesn't work
+  struct AltPtrWrapperInner inner;
+  // B) Works
+  // struct PtrWrapperInner inner;
+};
+
+void fn(struct PtrWrapper wrapper)
+{
+  assert(*wrapper.value == 10);
+  assert(*wrapper.inner.value == 10);
+}
+
+int main()
+{
+  int ret = 10;
+  int *ptr = &ret;
+
+  struct AltPtrWrapper alt;
+  alt.inner.value = ptr;
+  alt.value = ptr;
+
+  // Casting the structure itself works.
+  struct PtrWrapper wrapper = *(struct PtrWrapper *)&alt;
+  assert(*wrapper.value == 10);
+  assert(*wrapper.inner.value == 10);
+
+  // This only works if there is one level of casting.
+  int (*alias)(struct AltPtrWrapper) = (int (*)(struct AltPtrWrapper))fn;
+  alias(alt);
+}
diff --git a/regression/cbmc/Function_Pointer19/test.desc b/regression/cbmc/Function_Pointer19/test.desc
new file mode 100644
index 00000000000..278f468e130
--- /dev/null
+++ b/regression/cbmc/Function_Pointer19/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
diff --git a/regression/cbmc/Linking7/member-name-mismatch.desc b/regression/cbmc/Linking7/member-name-mismatch.desc
index da68dba90a0..603d759e8d8 100644
--- a/regression/cbmc/Linking7/member-name-mismatch.desc
+++ b/regression/cbmc/Linking7/member-name-mismatch.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 module2.c
 ^EXIT=10$
diff --git a/regression/cbmc/Linking7/test.desc b/regression/cbmc/Linking7/test.desc
index 315426f8aae..7e8989049b8 100644
--- a/regression/cbmc/Linking7/test.desc
+++ b/regression/cbmc/Linking7/test.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 module.c
 ^EXIT=10$
diff --git a/src/goto-programs/remove_function_pointers.cpp b/src/goto-programs/remove_function_pointers.cpp
index a0bcdd80db9..5d1f373ec57 100644
--- a/src/goto-programs/remove_function_pointers.cpp
+++ b/src/goto-programs/remove_function_pointers.cpp
@@ -11,6 +11,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "remove_function_pointers.h"
 
+#include <util/arith_tools.h>
+#include <util/byte_operators.h>
 #include <util/c_types.h>
 #include <util/fresh_symbol.h>
 #include <util/invariant.h>
@@ -195,8 +197,10 @@ static void fix_argument_types(code_function_callt &function_call)
     {
       if(call_arguments[i].type() != function_parameters[i].type())
       {
-        call_arguments[i] =
-          typecast_exprt(call_arguments[i], function_parameters[i].type());
+        call_arguments[i] = make_byte_extract(
+          call_arguments[i],
+          from_integer(0, c_index_type()),
+          function_parameters[i].type());
       }
     }
   }
@@ -235,8 +239,10 @@ static void fix_return_type(
   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()))));
+  dest.add(goto_programt::make_assignment(code_assignt(
+    old_lhs,
+    make_byte_extract(
+      tmp_symbol_expr, from_integer(0, c_index_type()), old_lhs.type()))));
 }
 
 void remove_function_pointerst::remove_function_pointer(