Skip to content

Commit b778bea

Browse files
committed
byte_update against a pointer shouldn't be fatal
This can happen in inaccessible code, so it doesn't seem necessary to kill the whole process
1 parent d48e840 commit b778bea

File tree

1 file changed

+0
-10
lines changed

1 file changed

+0
-10
lines changed

src/solvers/flattening/bv_pointers.cpp

Lines changed: 0 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -451,16 +451,6 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
451451
{
452452
return SUB::convert_byte_extract(to_byte_extract_expr(expr));
453453
}
454-
else
455-
{
456-
INVARIANT(
457-
expr.id() != ID_byte_update_little_endian,
458-
"byte-wise pointer updates are unsupported");
459-
460-
INVARIANT(
461-
expr.id() != ID_byte_update_big_endian,
462-
"byte-wise pointer updates are unsupported");
463-
}
464454

465455
return conversion_failed(expr);
466456
}

0 commit comments

Comments
 (0)