Skip to content

Commit 199e850

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 66d9d17 commit 199e850

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
@@ -524,7 +524,9 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
524524
{
525525
return SUB::convert_byte_extract(to_byte_extract_expr(expr));
526526
}
527-
else
527+
else if(
528+
expr.id() == ID_byte_update_little_endian ||
529+
expr.id() == ID_byte_update_big_endian)
528530
{
529531
return SUB::convert_byte_update(to_byte_update_expr(expr));
530532
}

0 commit comments

Comments
 (0)