Skip to content

Commit 728a231

Browse files
author
Daniel Kroening
committed
array_of_exprt has array_typet type
1 parent 09bcb5a commit 728a231

File tree

2 files changed

+11
-1
lines changed

2 files changed

+11
-1
lines changed

src/solvers/flattening/boolbv_array_of.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,7 @@ bvt boolbvt::convert_array_of(const array_of_exprt &expr)
1818
DATA_INVARIANT(
1919
expr.type().id() == ID_array, "array_of expression shall have array type");
2020

21-
const array_typet &array_type=to_array_type(expr.type());
21+
const array_typet &array_type = expr.type();
2222

2323
if(is_unbounded_array(array_type))
2424
return conversion_failed(expr);

src/util/std_expr.h

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1590,6 +1590,16 @@ class array_of_exprt:public unary_exprt
15901590
{
15911591
}
15921592

1593+
const array_typet &type() const
1594+
{
1595+
return static_cast<const array_typet &>(unary_exprt::type());
1596+
}
1597+
1598+
array_typet &type()
1599+
{
1600+
return static_cast<array_typet &>(unary_exprt::type());
1601+
}
1602+
15931603
exprt &what()
15941604
{
15951605
return op0();

0 commit comments

Comments
 (0)