Test Z3-floating

AArch64 Z3-floating
(* Z3 variant with floating read *)
{
0:X1=x; 0:X4=y; 0:X5=z;
1:X1=y; 1:X3=z;
2:X1=z; 2:X3=x;
}
 P0                  | P1          | P2          ;
 LDR W0,[X1]         | MOV W0,#1   | MOV W0,#2   ;
 EOR W2,W0,W0        | STR W0,[X1] | STR W0,[X1] ;
 LDR W3,[X4,W2,SXTW] | DMB ST      | DMB ST      ;
 LDR W6,[X5]         | MOV W2,#1   | MOV W2,#1   ;
                     | STR W2,[X3] | STR W2,[X3] ;
exists
(z=2 /\ 0:X0=1 /\ 0:X3=0 /\ 0:X6=1)