diff --git a/regression/cbmc-java/array2/test.class b/regression/cbmc-java/array2/test.class
new file mode 100644
index 00000000000..507d6622e5c
Binary files /dev/null and b/regression/cbmc-java/array2/test.class differ
diff --git a/regression/cbmc-java/array2/test.desc b/regression/cbmc-java/array2/test.desc
new file mode 100644
index 00000000000..6d2226bb26b
--- /dev/null
+++ b/regression/cbmc-java/array2/test.desc
@@ -0,0 +1,6 @@
+CORE
+test.class
+--function test.f --cover location
+\d+ of \d+ covered
+--
+^warning: ignoring
diff --git a/regression/cbmc-java/array2/test.java b/regression/cbmc-java/array2/test.java
new file mode 100644
index 00000000000..075017405ee
--- /dev/null
+++ b/regression/cbmc-java/array2/test.java
@@ -0,0 +1,16 @@
+public class test {
+
+  public void f(int unknown) {
+
+    int[] arr;
+    if(unknown > 0)
+      arr = new int[1];
+    else
+      arr = new int[0];
+
+    if(unknown > 0)
+      arr[0]=1;
+
+  }
+
+}
diff --git a/src/solvers/flattening/boolbv_array_of.cpp b/src/solvers/flattening/boolbv_array_of.cpp
index 09fefee64e1..2ddd2b674ad 100644
--- a/src/solvers/flattening/boolbv_array_of.cpp
+++ b/src/solvers/flattening/boolbv_array_of.cpp
@@ -25,7 +25,14 @@ bvt boolbvt::convert_array_of(const array_of_exprt &expr)
   std::size_t width=boolbv_width(array_type);
 
   if(width==0)
-    return conversion_failed(expr);
+  {
+    // A zero-length array is acceptable;
+    // an element with unknown size is not.
+    if(boolbv_width(array_type.subtype())==0)
+      return conversion_failed(expr);
+    else
+      return bvt();
+  }
 
   const exprt &array_size=array_type.size();
 
diff --git a/src/solvers/flattening/boolbv_with.cpp b/src/solvers/flattening/boolbv_with.cpp
index 56984f4efbd..c5f92806bf3 100644
--- a/src/solvers/flattening/boolbv_with.cpp
+++ b/src/solvers/flattening/boolbv_with.cpp
@@ -37,7 +37,13 @@ bvt boolbvt::convert_with(const exprt &expr)
   std::size_t width=boolbv_width(expr.type());
 
   if(width==0)
-    return conversion_failed(expr);
+  {
+    // A zero-length array is acceptable:
+    if(expr.type().id()==ID_array && boolbv_width(expr.type().subtype())!=0)
+      return bvt();
+    else
+      return conversion_failed(expr);
+  }
 
   if(bv.size()!=width)
   {