Test J7p

AArch64 J7p
{
  pte_x=(valid:0,oa:phy_x);
  0:X2=pte_x;
  0:X1=(valid:1,oa:phy_x);
  0:X3=x;
  x=0;
  1:X3=x;

}

P0             |  P1;
STR X1,[X2]    |;
DMB SY         | LDR W4,[X3]    ;
MOV W7, #1     | MOV W7, #2     ;
               | L0:STR W7,[X3];
STR W7,[X3]    |                ;
exists (1:X4=1 /\ fault(P1:L0,x,MMU:Translation))