Don't warn on array_of_expr with zero length

These result from array_set instructions, which when targeting
variable-length arrays can end up targeting zero-sized arrays.

Author: smowton

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();
 

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)
   {