AArch64 NT-10-addr TTHM=P0:HA Variant=precise { pte_x=(af:0); x=1; 0:X0=x; 0:X4=y; 1:X0=y; 1:X2=x; } P0 | P1 ; LDR W1,[X0] | LDR W1,[X0] ; EOR W2,W1,W1 | DMB LD ; MOV W3,#1 |L1: ; STR W3,[X4,W2,SXTW] | LDR W3,[X2] ; exists (1:X1=1 /\ 1:X3=0 /\ fault(P1:L1,x,MMU:AccessFlag))