AArch64 MP+nondep+dmb.sy Com=Rf Fr { x = z ; z = 0 ; y = 0 ; 0:X1=x; 0:X4=y; 1:X1=y; 1:X3=x; } P0 | P1 ; STR X4,[X1] | LDR W0,[X1] ; LDR X2,[X1] | DMB SY ; MOV W3,#1 | LDR X4,[X3] ; STR W3,[X2] | ; exists (1:X0=1 /\ 1:X4=z /\ 0:X2=y)