Test STRx+LDCLRptex+db

AArch64 STRx+LDCLRptex+db
TTHM=HA HD
{
pte_x=(db:0,dbm:1);
0:X2=x;
1:X4=pte_x;
}
  P0        | P1               ;
MOV W1,#1   | MOV X1,#1        ;
L0:         | LDCLR X1,X0,[X4] ; (* Clear bit 0 atomically -> invalid *)
STR W1,[X2] |                  ;

exists (1:X0=(oa:PA(x), dbm:1) /\ [PTE(x)]=(oa:PA(x), valid:0, dbm:1) /\ [x]=0 /\ fault(P0:L0,x,MMU:Translation))