diff --git a/regression/cbmc/member1/main.c b/regression/cbmc/member1/main.c
new file mode 100644
index 00000000000..0dcf92d958d
--- /dev/null
+++ b/regression/cbmc/member1/main.c
@@ -0,0 +1,19 @@
+struct B
+{
+  int bi;
+  int *c;
+};
+
+struct A
+{
+  int ai;
+  struct B b;
+};
+
+int main()
+{
+  struct A *a;
+  if((&a->b)->c == 0)
+    return 1;
+  return 0;
+}
diff --git a/regression/cbmc/member1/test.desc b/regression/cbmc/member1/test.desc
new file mode 100644
index 00000000000..22feeb5e857
--- /dev/null
+++ b/regression/cbmc/member1/test.desc
@@ -0,0 +1,9 @@
+CORE
+main.c
+--pointer-check
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
+add/sub with mixed types
diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp
index 2933f680e8e..6fd2cfcfdc0 100644
--- a/src/analyses/goto_check.cpp
+++ b/src/analyses/goto_check.cpp
@@ -1414,7 +1414,10 @@ void goto_checkt::check_rec(const exprt &expr, guardt &guard, bool address)
           deref.pointer(), pointer_type(char_type()));
 
       const exprt new_address = typecast_exprt(
-        plus_exprt(char_pointer, member_offset), char_pointer.type());
+        plus_exprt(
+          char_pointer,
+          typecast_exprt::conditional_cast(member_offset, pointer_diff_type())),
+        char_pointer.type());
 
       const exprt new_address_casted =
         typecast_exprt::conditional_cast(new_address, new_pointer_type);