addresses.

The operation "mem_force Γ m a" used to apply the identify function to
pricisely the object "a", even in case "a" is an "unsigned char" address
refering to an individual byte. This caused the ctree substructure of the
entire subobject to disappear and had the undesired effect that:

  mem_force Γ a m ⊑{Γ,true@Γm} m

failed to hold (i.e. unused reads cannot be removed).