diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp index 8ec1ec841ea..833ca000f81 100644 --- a/src/solvers/flattening/bv_pointers.cpp +++ b/src/solvers/flattening/bv_pointers.cpp @@ -441,6 +441,12 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr) { return SUB::convert_byte_extract(to_byte_extract_expr(expr)); } + else if( + expr.id() == ID_byte_update_little_endian || + expr.id() == ID_byte_update_big_endian) + { + throw "byte-wise updates of pointers are unsupported"; + } return conversion_failed(expr); }