array_of_exprt has array_typet type

Author: Daniel Kroening

src/solvers/flattening/boolbv_array_of.cpp

@@ -18,7 +18,7 @@ bvt boolbvt::convert_array_of(const array_of_exprt &expr)
   DATA_INVARIANT(
     expr.type().id() == ID_array, "array_of expression shall have array type");
 
-  const array_typet &array_type=to_array_type(expr.type());
+  const array_typet &array_type = expr.type();
 
   if(is_unbounded_array(array_type))
     return conversion_failed(expr);

src/util/std_expr.h

@@ -1616,6 +1616,16 @@ class array_of_exprt:public unary_exprt
   {
   }
 
+  const array_typet &type() const
+  {
+    return static_cast<const array_typet &>(unary_exprt::type());
+  }
+
+  array_typet &type()
+  {
+    return static_cast<array_typet &>(unary_exprt::type());
+  }
+
   exprt &what()
   {
     return op0();