AArch64 NT-10-dsb-isb+dsb 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] ; DSB SY | ; ISB | DMB LD ; MOV W3,#1 | ; STR W3,[X4] |L1: ; | LDR W3,[X2] ; exists (1:X1=1 /\ fault(P1:L1,x,MMU:AccessFlag))