AArch64 POP1 "" { 0:X0=x; 0:X1=y; 1:X0=y; 2:X0=y; 2:X1=x; 0:X2=1; 0:X3=2; 1:X1=1; 2:X2=2; 2:X3=1; } P0 | P1 | P2 ; STLR W2,[X0] | STR W1,[X0] | STR W2,[X0] ; STR W3,[X0] | | DMB SY ; LDAR W4,[X0] | | LDR W3,[X1] ; LDR W5,[X1] | | ; exists (x=2 /\ y=2 /\ 0:X4=2 /\ 0:X5=1 /\ 2:X3=0)