Flattening: support index expressions over zero bitwidth arrays

There is not really anything wrong in having empty bitvectors, which we
otherwise already support (as of e021eef).

Author: tautschnig

src/solvers/flattening/boolbv_index.cpp

@@ -36,9 +36,6 @@ bvt boolbvt::convert_index(const index_exprt &expr)
 
     std::size_t width=boolbv_width(expr.type());
 
-    if(width==0)
-      return conversion_failed(expr);
-
     // see if the array size is constant
 
     if(is_unbounded_array(array_type))
@@ -290,9 +287,6 @@ bvt boolbvt::convert_index(
 
   std::size_t width = boolbv_width(array_type.element_type());
 
-  if(width==0)
-    return conversion_failed(array);
-
   // TODO: If the underlying array can use one of the
   // improvements given above then it may be better to use
   // the array theory for short chains of updates and then