Test CO-W+RR+fri-dmb

Executions for behaviour: "0:R0=2 ; 0:R2=0 ; x=1"

Executions for behaviour: "0:R0=2 ; 0:R2=0 ; x=2"

Executions for behaviour: "0:R0=2 ; 0:R2=1 ; x=2"

ARM CO-W+RR+fri-dmb
"Fri DMBsWR Fre Rfe"
Prefetch=
Com=Fr Rf
Orig=Fri DMBsWR Fre Rfe
{
%x0=x;
%x1=x;
}
 P0           | P1           ;
 LDR R0,[%x0] | MOV R0,#2    ;
 MOV R1,#1    | STR R0,[%x1] ;
 STR R1,[%x0] |              ;
 DMB          |              ;
 LDR R2,[%x0] |              ;
exists 0:R0=2 /\ (0:R2=0 /\ (x=1 \/ x=2) \/ 0:R2=1 /\ x=2)