Test V2I

AArch64 V2I
{
0:X2=pte_x;
0:X4=x;
0:X0=(oa:phy_x,valid:0);
}
P0 ;
STR X0,[X2]    ;
L0: LDR X3,[X4];
DSB ISH        ;
LSR X9,X4,#12  ;
TLBI VAAE1IS,X9;
DSB ISH        ;
L1: LDR X6,[X4];
exists ([x]=0 /\ ~fault(P0:L0,x) /\ ~fault(P0:L1,x))