{ [P0_r0]=0;[P1_r0]=0;[x]=0;[y]=0;
  uint64_t %P0_P0_r0=P0_r0;uint64_t %P0_x=x;uint64_t %P0_y=y;
  uint64_t %P1_P1_r0=P1_r0;uint64_t %P1_x=x;uint64_t %P1_y=y }

  P0                    |  P1                    ;
   MOV W10,#1           |   MOV W10,#1           ;
   LDR W8,[X%P0_x]      |   LDR W8,[X%P1_y]      ;
   CBZ W8, label1       |   CBZ W8, label2       ;
label1:                 | label2:                ;
   STR W10,[X%P0_y]     |   STR W10,[X%P1_x]     ;
   STR W8,[X%P0_P0_r0]  |   STR W8,[X%P1_P1_r0]  ;

exists (P0_r0=1 /\ P1_r0=1)