diff --git a/src/util/std_types.h b/src/util/std_types.h index 39cb1b49b94..9e84cffb3f2 100644 --- a/src/util/std_types.h +++ b/src/util/std_types.h @@ -1041,6 +1041,12 @@ class array_typet:public type_with_subtypet } }; +template <> +inline bool can_cast_type(const typet &type) +{ + return type.id() == ID_array; +} + /*! \brief Cast a generic typet to an \ref array_typet * * This is an unchecked conversion. \a type must be known to be \ref @@ -1053,7 +1059,7 @@ class array_typet:public type_with_subtypet */ inline const array_typet &to_array_type(const typet &type) { - PRECONDITION(type.id()==ID_array); + PRECONDITION(can_cast_type(type)); return static_cast(type); } @@ -1062,7 +1068,7 @@ inline const array_typet &to_array_type(const typet &type) */ inline array_typet &to_array_type(typet &type) { - PRECONDITION(type.id()==ID_array); + PRECONDITION(can_cast_type(type)); return static_cast(type); }