Test CO-IRIW

…

PPC CO-IRIW

{0:r1=x; 1:r2=x; 2:r1=x; 3:r2=x;}

 P0           | P1           | P2           | P3           ;
 li r0,1      | lwz r0,0(r2) | li r0,2      | lwz r0,0(r2) ;
 stw r0,0(r1) | lwz r1,0(r2) | stw r0,0(r1) | lwz r1,0(r2) ;

exists (not (1:r0=2 /\ (1:r1=2 /\ (3:r0=2 /\ (3:r1=2 \/ 3:r1=1) \/ 3:r0=1 /\ (3:r1=2 \/ 3:r1=1) \/ 3:r0=0 /\ (3:r1=2 \/ 3:r1=1 \/ 3:r1=0)) \/ 1:r1=1 /\ (3:r0=2 /\ (3:r1=2 \/ 3:r1=1) \/ 3:r0=1 /\ 3:r1=1 \/ 3:r0=0 /\ (3:r1=2 \/ 3:r1=1 \/ 3:r1=0))) \/ 1:r0=1 /\ (1:r1=2 /\ (3:r0=2 /\ 3:r1=2 \/ 3:r0=1 /\ (3:r1=2 \/ 3:r1=1) \/ 3:r0=0 /\ (3:r1=2 \/ 3:r1=1 \/ 3:r1=0)) \/ 1:r1=1 /\ (3:r0=2 /\ (3:r1=2 \/ 3:r1=1) \/ 3:r0=1 /\ (3:r1=2 \/ 3:r1=1) \/ 3:r0=0 /\ (3:r1=2 \/ 3:r1=1 \/ 3:r1=0))) \/ 1:r0=0 /\ (1:r1=2 /\ (3:r0=2 /\ (3:r1=2 \/ 3:r1=1) \/ 3:r0=1 /\ (3:r1=2 \/ 3:r1=1) \/ 3:r0=0 /\ (3:r1=2 \/ 3:r1=1 \/ 3:r1=0)) \/ 1:r1=1 /\ (3:r0=2 /\ (3:r1=2 \/ 3:r1=1) \/ 3:r0=1 /\ (3:r1=2 \/ 3:r1=1) \/ 3:r0=0 /\ (3:r1=2 \/ 3:r1=1 \/ 3:r1=0)) \/ 1:r1=0 /\ (3:r0=2 /\ (3:r1=2 \/ 3:r1=1) \/ 3:r0=1 /\ (3:r1=2 \/ 3:r1=1) \/ 3:r0=0 /\ (3:r1=2 \/ 3:r1=1 \/ 3:r1=0)))))