diff --git a/src/solvers/flattening/boolbv_array_of.cpp b/src/solvers/flattening/boolbv_array_of.cpp index 89a71dba486..458430a3805 100644 --- a/src/solvers/flattening/boolbv_array_of.cpp +++ b/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); diff --git a/src/util/std_expr.h b/src/util/std_expr.h index e2d1ff13e57..05250e5b58f 100644 --- a/src/util/std_expr.h +++ b/src/util/std_expr.h @@ -1585,14 +1585,19 @@ inline index_exprt &to_index_expr(exprt &expr) class array_of_exprt:public unary_exprt { public: - DEPRECATED(SINCE(2018, 9, 21, "use array_of_exprt(what, type) instead")) - array_of_exprt():unary_exprt(ID_array_of) + explicit array_of_exprt(exprt _what, array_typet _type) + : unary_exprt(ID_array_of, std::move(_what), std::move(_type)) { } - explicit array_of_exprt(exprt _what, array_typet _type) - : unary_exprt(ID_array_of, std::move(_what), std::move(_type)) + const array_typet &type() const + { + return static_cast(unary_exprt::type()); + } + + array_typet &type() { + return static_cast(unary_exprt::type()); } exprt &what()