Test 2+2W+TLBI+VaToInv+01

AArch64 2+2W+TLBI+VaToInv+01
Variant=fatal
{
int x=1;
int y=1;
0:X1=(oa:phy_x,valid:0);
0:X2=pte_x;
0:X8=y;

1:X1=(oa:phy_y,valid:0);
1:X2=pte_y;
1:X8=x;

}
  P0             | P1              ;
 STR X1,[X2]     | STR X1,[X2]     ;
 LSR X9,X8,#12   | LSR X9,X8,#12   ;
 TLBI VAAE1IS,X9 | TLBI VAAE1IS,X9 ;
 DSB ISH         | DSB ISH         ;
 ISB             | ISB             ;
 LDR W4,[X8]     | LDR W4,[X8]     ;

exists (0:X4=1 /\ 1:X4=1 /\ ~fault(P0,y) /\ ~fault(P1,x))