AArch64 NT-33-dmbld+dsb2 TTHM=P1:HA { int x=1; int y; int z=2; pte_x=(af:0); 0:X2=y; 0:X6=pte_x; 0:X9=(oa:phy_z,af:0); 1:X2=y; 1:X4=x; } P0 | P1 ; LDR X7,[X6] | LDR W0,[X2] ; STR X9,[X6] | DSB SY ; LDR X5,[X6] |L0: ; DMB LD | LDR W1,[X4] ; MOV W0,#1 | ; STR W0,[X2] | ; exists (0:X7=(oa:PA(x)) /\ 1:X0=1 /\ 1:X1=1) \/ (0:X7=(oa:PA(x)) /\ 1:X0=1 /\ 1:X1=2) \/ (0:X7=(oa:PA(x), af:0) /\ 1:X0=1 /\ 1:X1=1)