Run CoRR2 in model, using armmem

ARM CoRR2 ()
"CoRR2"
{
P0:R5=x ; P0:R1=1 ;
P1:R5=x ; P1:R2=2 ;
P2:R5=x ;
P3:R5=x ;
}
P0 |P1 |P2 |P3 ;
str R1,R5|str R2,R5|ldr R1,R5|ldr R1,R5;
| |ldr R2,R5|ldr R2,R5;
~exists
(
(P2:R1=1 /\ P2:R2=2 /\ P3:R1=2 /\ P3:R2=1) \/
(P2:R1=2 /\ P2:R2=1 /\ P3:R1=1 /\ P3:R2=2)
)