Allow empty arrays in convert_array

Author: romainbrenguier

src/solvers/flattening/boolbv_array.cpp

@@ -11,17 +11,16 @@ Author: Daniel Kroening, [email protected]
 
 bvt boolbvt::convert_array(const exprt &expr)
 {
-  std::size_t width=boolbv_width(expr.type());
+  const std::size_t width = boolbv_width(expr.type());
+  const exprt::operandst &operands = expr.operands();
 
-  if(width==0)
-    return conversion_failed(expr);
+  if(operands.empty() && width == 0)
+    return bvt();
 
   if(expr.type().id()==ID_array)
   {
-    assert(expr.has_operands());
-    const exprt::operandst &operands=expr.operands();
     assert(!operands.empty());
-    std::size_t op_width=width/operands.size();
+    const std::size_t op_width = width / operands.size();
 
     bvt bv;
     bv.reserve(width);