Cleanup invariants in remove_vector

Author: hannes-steffenhagen-diffblue

src/goto-programs/remove_vector.cpp

@@ -82,13 +82,16 @@ static void remove_vector(exprt &expr)
        expr.id()==ID_mod  || expr.id()==ID_bitxor ||
        expr.id()==ID_bitand || expr.id()==ID_bitor)
     {
+      // FIXME plus, mult, bitxor, bitor and bitand are not binary operators
+      //       normally. It is unclear why is it safe to assume that they are
+      //       in this context
+      auto const &binary_expr = to_binary_expr(expr);
       remove_vector(expr.type());
       array_typet array_type=to_array_type(expr.type());
 
       mp_integer dimension;
       to_integer(array_type.size(), dimension);
 
-      assert(expr.operands().size()==2);
       const typet subtype=array_type.subtype();
       // do component-wise:
       // x+y -> vector(x[0]+y[0],x[1]+y[1],...)
@@ -99,22 +102,23 @@ static void remove_vector(exprt &expr)
       {
         exprt index=from_integer(i, array_type.size().type());
 
-        array_expr.operands()[i]=
-          binary_exprt(index_exprt(expr.op0(), index, subtype), expr.id(),
-                       index_exprt(expr.op1(), index, subtype));
+        array_expr.operands()[i] = binary_exprt(
+          index_exprt(binary_expr.op0(), index, subtype),
+          binary_expr.id(),
+          index_exprt(binary_expr.op1(), index, subtype));
       }
 
       expr=array_expr;
     }
     else if(expr.id()==ID_unary_minus || expr.id()==ID_bitnot)
     {
+      auto const &unary_expr = to_unary_expr(expr);
       remove_vector(expr.type());
       array_typet array_type=to_array_type(expr.type());
 
       mp_integer dimension;
       to_integer(array_type.size(), dimension);
 
-      assert(expr.operands().size()==1);
       const typet subtype=array_type.subtype();
       // do component-wise:
       // -x -> vector(-x[0],-x[1],...)
@@ -125,8 +129,8 @@ static void remove_vector(exprt &expr)
       {
         exprt index=from_integer(i, array_type.size().type());
 
-        array_expr.operands()[i]=
-          unary_exprt(expr.id(), index_exprt(expr.op0(), index, subtype));
+        array_expr.operands()[i] = unary_exprt(
+          unary_expr.id(), index_exprt(unary_expr.op0(), index, subtype));
       }
 
       expr=array_expr;