Test Jeff1

AArch64 Jeff1
{
pte_x=(valid:1,oa:phy_x);
0:X2=pte_x;
0:X1=(valid:0,oa:phy_x);
0:X3=x;
1:X2=pte_x;
1:X3=x;
y=1;
0:X8=z; 1:X8=z;
}
P0               | P1;
L0: LDR X10,[X3] | LDAR X7,[X2];
                 | MOV W4, #1  ;
MOV W7,#1        | STLR X4,[X3];
STR X1,[X2]      |             ;
exists (0:X10=1 /\ 1:X7=(oa:PA(x), valid:0) /\ ~fault(P0:L0,x))