Skip to content

Commit 115b214

Browse files
committed
Pointer flattening: convert typecast through cache
This is to make sure we do not convert the same expression twice, which would result in fresh variables for accesses into unbounded arrays, resulting in spurious verification failures. This was observed with --paths lifo on Pointer_array6 once alignment assumptions in value-set dereferencing are fixed.
1 parent b08632a commit 115b214

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/solvers/flattening/bv_pointers.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -732,7 +732,7 @@ bvt bv_pointerst::convert_bitvector(const exprt &expr)
732732
to_typecast_expr(expr).op().type().id() == ID_pointer)
733733
{
734734
// pointer to int
735-
bvt op0 = convert_pointer_type(to_typecast_expr(expr).op());
735+
bvt op0 = convert_bv(to_typecast_expr(expr).op());
736736

737737
// squeeze it in!
738738
std::size_t width=boolbv_width(expr.type());

0 commit comments

Comments
 (0)