Skip to content

Commit 57855b8

Browse files
author
Daniel Kroening
committed
avoid non-termination of simplify_exprt::simplify_byte_extract when given array_of
1 parent 6fd77f4 commit 57855b8

File tree

1 file changed

+5
-2
lines changed

1 file changed

+5
-2
lines changed

src/util/simplify_expr.cpp

Lines changed: 5 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1734,12 +1734,15 @@ bool simplify_exprt::simplify_byte_extract(byte_extract_exprt &expr)
17341734
return true;
17351735

17361736
if(expr.op().id()==ID_array_of &&
1737-
expr.op().op0().id()==ID_constant)
1737+
to_array_of_expr(expr.op()).op().id()==ID_constant)
17381738
{
17391739
std::string const_bits=
1740-
expr2bits(expr.op().op0(),
1740+
expr2bits(to_array_of_expr(expr.op()).op(),
17411741
byte_extract_id()==ID_byte_extract_little_endian);
17421742

1743+
if(const_bits.empty())
1744+
return true;
1745+
17431746
// double the string until we have sufficiently many bits
17441747
while(mp_integer(const_bits.size())<offset*8+el_size)
17451748
const_bits+=const_bits;

0 commit comments

Comments
 (0)