diff --git a/regression/cbmc-java/arrayread1/arrayread1.class b/regression/cbmc-java/arrayread1/arrayread1.class
new file mode 100644
index 00000000000..66779a1478b
Binary files /dev/null and b/regression/cbmc-java/arrayread1/arrayread1.class differ
diff --git a/regression/cbmc-java/arrayread1/arrayread1.java b/regression/cbmc-java/arrayread1/arrayread1.java
new file mode 100644
index 00000000000..ddf622dd5e2
--- /dev/null
+++ b/regression/cbmc-java/arrayread1/arrayread1.java
@@ -0,0 +1,14 @@
+public class arrayread1 {
+
+  static arrayread1 readback;
+
+  public static void main(int c) {
+
+    if(c!=1) return;
+    arrayread1[] a = new arrayread1[c];
+    readback=a[0];
+    assert(readback==null);
+
+  }
+
+}
diff --git a/regression/cbmc-java/arrayread1/test.desc b/regression/cbmc-java/arrayread1/test.desc
new file mode 100644
index 00000000000..f0cbf9617d2
--- /dev/null
+++ b/regression/cbmc-java/arrayread1/test.desc
@@ -0,0 +1,8 @@
+CORE
+arrayread1.class
+--unwind 3 --no-propagation
+^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 7e5714de23a..f1515f67cdd 100644
--- a/src/solvers/flattening/bv_pointers.cpp
+++ b/src/solvers/flattening/bv_pointers.cpp
@@ -296,7 +296,7 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
     const typet &op_type=ns.follow(op.type());
 
     if(op_type.id()==ID_pointer)
-      return convert_pointer_type(op);
+      return convert_bv(op);
     else if(op_type.id()==ID_signedbv ||
             op_type.id()==ID_unsignedbv ||
             op_type.id()==ID_bool ||