The code to load the high 64 bits assumed that the insn used to
load the low 64 bits zero-extended.  Enforce that.