AArch64 LDR-AF TTHM=HA { int x=1; pte_x = (af:0); 0:X2=x; } P0 ; L0: ; LDR W0,[X2] ; forall 0:X0=1 /\ pte_x=(af:1) /\ ~fault(P0:L0,x)