Lower byte_{extract,update} when pointers are involved

This is in preparation of the flattened bit width of pointers not
necessarily matching the width claimed by the front-end.

Author: tautschnig

src/solvers/flattening/boolbv_byte_extract.cpp

@@ -38,8 +38,12 @@ bvt map_bv(const bv_endianness_mapt &map, const bvt &src)
 bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr)
 {
   // array logic does not handle byte operators, thus lower when operating on
-  // unbounded arrays
-  if(is_unbounded_array(expr.op().type()))
+  // unbounded arrays; similarly, byte extracts over pointers are not to be
+  // handled here
+  if(
+    is_unbounded_array(expr.op().type()) ||
+    has_subtype(expr.type(), ID_pointer, ns) ||
+    has_subtype(expr.op().type(), ID_pointer, ns))
   {
     return convert_bv(lower_byte_extract(expr, ns));
   }

src/solvers/flattening/boolbv_byte_update.cpp

@@ -20,10 +20,13 @@ Author: Daniel Kroening, [email protected]
 bvt boolbvt::convert_byte_update(const byte_update_exprt &expr)
 {
   // if we update (from) an unbounded array, lower the expression as the array
-  // logic does not handle byte operators
+  // logic does not handle byte operators; similarly, data types that contain
+  // pointers must not be handled here
   if(
     is_unbounded_array(expr.op().type()) ||
-    is_unbounded_array(expr.value().type()))
+    is_unbounded_array(expr.value().type()) ||
+    has_subtype(expr.value().type(), ID_pointer, ns) ||
+    has_subtype(expr.op0().type(), ID_pointer, ns))
   {
     return convert_bv(lower_byte_update(expr, ns));
   }