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) )