AArch64 RelSeq03 { 0:X0=x; 1:X0=x; 2:X0=x; 2:X1=y; 3:X0=y; 3:X1=x; 0:X1=1; 1:X3=2; 1:X4=3; 3:X2=1; } P0 | P1 | P2 | P3 ; STLR W1,[X0] | LDXR W1,[X0] | LDAR W2,[X0] | STLR W2,[X0] ; | STXR W2,W3,[X0] | LDR W3,[X1] | LDAR W3,[X1] ; | STR W4,[X0] | | ; exists (x=3 /\ 1:X1=1 /\ 1:X2=0 /\ 2:X2=3 /\ 2:X3=0 /\ 3:X3=0)