Test STRx+STCLRptex+db2

AArch64 STRx+STCLRptex+db2
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:         | STCLR X1,[X4]  ; (* Clear bit 0 atomically -> invalid *)
STR W1,[X2] |                ;

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