diff --git a/regression/cbmc/void_pointer3/main.c b/regression/cbmc/void_pointer3/main.c
new file mode 100644
index 00000000000..1a9ed7c6e16
--- /dev/null
+++ b/regression/cbmc/void_pointer3/main.c
@@ -0,0 +1,19 @@
+#include <stddef.h>
+
+int main()
+{
+  // make sure they are NULL objects
+  void *p=0, *q=0;
+  // with the object:offset encoding we need to make sure the address arithmetic
+  // below will only touch the offset part
+  __CPROVER_assume(sizeof(unsigned char)<sizeof(void*));
+  unsigned char o1, o2;
+  // there is ample undefined behaviour here, but the goal of this test solely
+  // is exercising CBMC's pointer subtraction encoding
+  p+=o1;
+  q+=o2;
+
+  ptrdiff_t d=p-q;
+  __CPROVER_assert(p-d==q, "");
+  return 0;
+}
diff --git a/regression/cbmc/void_pointer3/test.desc b/regression/cbmc/void_pointer3/test.desc
new file mode 100644
index 00000000000..9efefbc7362
--- /dev/null
+++ b/regression/cbmc/void_pointer3/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp
index 9cbe9309647..87b6548b689 100644
--- a/src/solvers/flattening/bv_pointers.cpp
+++ b/src/solvers/flattening/bv_pointers.cpp
@@ -412,9 +412,11 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
 
     bv=convert_bv(expr.op0());
 
-    mp_integer element_size=
-      pointer_offset_size(expr.op0().type().subtype(), ns);
-    DATA_INVARIANT(element_size>0, "object size expected to be non-zero");
+    typet pointer_sub_type=expr.op0().type().subtype();
+    if(pointer_sub_type.id()==ID_empty)
+      pointer_sub_type=char_type();
+    mp_integer element_size=pointer_offset_size(pointer_sub_type, ns);
+    DATA_INVARIANT(element_size>0, "object size expected to be positive");
 
     offset_arithmetic(bv, element_size, neg_op1);
 
@@ -469,9 +471,11 @@ bvt bv_pointerst::convert_bitvector(const exprt &expr)
 
     bvt bv=bv_utils.sub(op0, op1);
 
-    mp_integer element_size=
-      pointer_offset_size(expr.op0().type().subtype(), ns);
-    DATA_INVARIANT(element_size>0, "object size expected to be non-zero");
+    typet pointer_sub_type=expr.op0().type().subtype();
+    if(pointer_sub_type.id()==ID_empty)
+      pointer_sub_type=char_type();
+    mp_integer element_size=pointer_offset_size(pointer_sub_type, ns);
+    DATA_INVARIANT(element_size>0, "object size expected to be positive");
 
     if(element_size!=1)
     {