Refactoring in boolbvt::convert_array_of

Author: romainbrenguier

src/solvers/flattening/boolbv_array_of.cpp

@@ -13,16 +13,11 @@ Author: Daniel Kroening, [email protected]
 
 bvt boolbvt::convert_array_of(const array_of_exprt &expr)
 {
-  if(expr.type().id()!=ID_array)
-    throw "array_of must be array-typed";
-
   const array_typet &array_type=to_array_type(expr.type());
-
   if(is_unbounded_array(array_type))
     return conversion_failed(expr);
 
-  std::size_t width=boolbv_width(array_type);
-
+  const std::size_t width = boolbv_width(array_type);
   if(width==0)
   {
     // A zero-length array is acceptable;
@@ -34,29 +29,25 @@ bvt boolbvt::convert_array_of(const array_of_exprt &expr)
   }
 
   const exprt &array_size=array_type.size();
+  const auto size = numeric_cast<mp_integer>(array_size);
 
-  mp_integer size;
-
-  if(to_integer(array_size, size))
+  if(!size)
     return conversion_failed(expr);
 
   const bvt &tmp=convert_bv(expr.op0());
 
   bvt bv;
   bv.resize(width);
-
-  if(size*tmp.size()!=width)
-    throw "convert_array_of: unexpected operand width";
+  CHECK_RETURN(*size * tmp.size() == width);
 
   std::size_t offset=0;
-
   for(mp_integer i=0; i<size; i=i+1)
   {
     for(std::size_t j=0; j<tmp.size(); j++, offset++)
       bv[offset]=tmp[j];
   }
 
-  assert(offset==bv.size());
+  INVARIANT(offset == bv.size(), "final offset should correspond to size");
 
   return bv;
 }