Skip to content

Commit 84ee8e5

Browse files
committed
bv_pointerst: else case is just for byte updates
We should not treat all other expressions as byte updates. Expressions other than those handled in the if/else if chain should result in failing conversion.
1 parent 71da49a commit 84ee8e5

File tree

1 file changed

+3
-1
lines changed

1 file changed

+3
-1
lines changed

src/solvers/flattening/bv_pointers.cpp

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -508,7 +508,9 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
508508
{
509509
return SUB::convert_byte_extract(to_byte_extract_expr(expr));
510510
}
511-
else
511+
else if(
512+
expr.id() == ID_byte_update_little_endian ||
513+
expr.id() == ID_byte_update_big_endian)
512514
{
513515
return SUB::convert_byte_update(to_byte_update_expr(expr));
514516
}

0 commit comments

Comments
 (0)