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