RISCV Andy26
{
0:x7=A; 0:x8=B; 0:x9=C;
1:x8=B; 1:x9=C;
}
P0 | P1 ;
lr.w x1,0(x7) | lw x4,0(x9) ;
lw x2,0(x8) | sw x4,0(x8) ;
sc.w x3,x2,0(x7) | ;
addi x4,x3,1 | ;
sw x4,0(x9) | ;
exists
(0:x1=0 /\ 0:x2=1 /\ 0:x3=0 /\ 1:x4=1)