allow address_of of byte_extract expressions

Author: Daniel Kroening

src/solvers/flattening/bv_pointers.cpp

@@ -158,6 +158,21 @@ bool bv_pointerst::convert_address_of_rec(
     POSTCONDITION(bv.size()==bits);
     return false;
   }
+  else if(expr.id()==ID_byte_extract_little_endian ||
+          expr.id()==ID_byte_extract_big_endian)
+  {
+    const auto &byte_extract_expr=to_byte_extract_expr(expr);
+
+    // recursive call
+    if(convert_address_of_rec(byte_extract_expr.op(), bv))
+      return true;
+
+    POSTCONDITION(bv.size()==bits);
+
+    offset_arithmetic(bv, 1, byte_extract_expr.offset());
+    POSTCONDITION(bv.size()==bits);
+    return false;
+  }
   else if(expr.id()==ID_member)
   {
     const member_exprt &member_expr=to_member_expr(expr);