diff --git a/src/solvers/lowering/byte_operators.cpp b/src/solvers/lowering/byte_operators.cpp index 3a5f976aac2..8bcc2554d2f 100644 --- a/src/solvers/lowering/byte_operators.cpp +++ b/src/solvers/lowering/byte_operators.cpp @@ -264,6 +264,17 @@ static exprt unpack_rec( member, little_endian, offset_bytes, max_bytes, ns, true); } } + else if(src.type().id() == ID_pointer) + { + return unpack_rec( + typecast_exprt( + src, unsignedbv_typet(to_pointer_type(src.type()).get_width())), + little_endian, + offset_bytes, + max_bytes, + ns, + unpack_byte_array); + } else if(src.type().id()!=ID_empty) { // a basic type; we turn that into extractbits while considering diff --git a/unit/solvers/lowering/byte_operators.cpp b/unit/solvers/lowering/byte_operators.cpp index fdcca2e58e7..81fe96e3bfc 100644 --- a/unit/solvers/lowering/byte_operators.cpp +++ b/unit/solvers/lowering/byte_operators.cpp @@ -124,6 +124,7 @@ SCENARIO("byte_extract_lowering", "[core][solvers][lowering][byte_extract]") signedbv_typet(24), signedbv_typet(128), // ieee_float_spect::single_precision().to_type(), + // generates the correct value, but remains wrapped in a typecast // pointer_typet(u64, 64), vector_typet(u8, size), vector_typet(u64, size),