Test 2+2WNExpExp+NExpNExp+DMBST+DMBST

AArch64 2+2WNExpExp+NExpNExp+DMBST+DMBST
TTHM=HD
{
int z;
0:X2=x; 1:X4=pte_x;
0:X3=y; 1:X6=pte_y; 
1:X5=(oa:phy_z,db:0,dbm:1);
1:X7=(oa:phy_y,db:0,dbm:1);
pte_x=(oa:phy_x,db:0,dbm:1);
pte_y=(oa:phy_y,db:1,dbm:1);
}
P0          | P1         ;
MOV X8,#1   | STR X5,[X4]; 
STR X8,[X3] | DMB ST     ;
            | STR X7,[X6];
DMB ST      |            ;
MOV X9,#1   |            ;
STR X9,[X2] |            ;
exists ([PTE(x)]=(oa:PA(z), dbm:1, db:0) /\ [PTE(y)]=(oa:PA(y), dbm:1) /\ [x]=1 /\ [y]=1)