AArch64 ATOM07 { 0:X0=x; 0:X2=1; 0:X4=2; } P0 ; LDXR W1,[X0] ; STR W2,[X0] ; STXR W3,W4,[X0] ; exists (x = 2 /\ 0:X1=0 /\ 0:X3=0)