Refactoring in boolbvt::convert_array

Author: romainbrenguier

src/solvers/flattening/arrays.cpp

@@ -34,7 +34,7 @@ void arrayst::record_array_index(const index_exprt &index)
   // we are not allowed to put the index directly in the
   //   entry for the root of the equivalence class
   //   because this map is accessed during building the error trace
-  std::size_t number=arrays.number(index.array());
+  const std::size_t number = arrays.number(index.array());
   index_map[number].insert(index.index());
   update_indices.insert(number);
 }
@@ -45,14 +45,9 @@ literalt arrayst::record_array_equality(
   const exprt &op0=equality.op0();
   const exprt &op1=equality.op1();
 
-  // check types
-  if(!base_type_eq(op0.type(), op1.type(), ns))
-  {
-    prop.error() << equality.pretty() << messaget::eom;
-    DATA_INVARIANT(
-      false,
-      "record_array_equality got equality without matching types");
-  }
+  DATA_INVARIANT(
+    base_type_eq(op0.type(), op1.type(), ns),
+    "record_array_equality should get matching types");
 
   DATA_INVARIANT(
     ns.follow(op0.type()).id()==ID_array,

src/solvers/flattening/boolbv_array.cpp

@@ -6,39 +6,30 @@ Author: Daniel Kroening, [email protected]
 
 \*******************************************************************/
 
-
 #include "boolbv.h"
 
 bvt boolbvt::convert_array(const exprt &expr)
 {
-  std::size_t width=boolbv_width(expr.type());
-
+  const std::size_t width = boolbv_width(expr.type());
   if(width==0)
     return conversion_failed(expr);
 
   if(expr.type().id()==ID_array)
   {
-    assert(expr.has_operands());
+    INVARIANT(expr.has_operands(), "array should have 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);
 
-    forall_expr(it, operands)
+    for(const exprt &op : operands)
     {
-      const bvt &tmp=convert_bv(*it);
-
-      if(tmp.size()!=op_width)
-        throw "convert_array: unexpected operand width";
-
-      forall_literals(it2, tmp)
-        bv.push_back(*it2);
+      const bvt &tmp = convert_bv(op);
+      CHECK_RETURN(tmp.size() == op_width);
+      bv.insert(bv.end(), tmp.begin(), tmp.end());
     }
 
     return bv;
   }
-
   return conversion_failed(expr);
 }