RISCV LR-SC-diff-loc1 { 0:x6=x; 0:x9=y; 1:x6=x; 1:x9=z; } P0 | P1 ; lr.w x5,0(x6) (* R x=0 *) | lr.w x5,0(x6) (* R x=0 *) ; ori x7,x0,1 | ori x7,x0,1 ; sc.w x8,x7,0(x9) (* W y=1 *) | sc.w x8,x7,0(x9) (* W z=1 *) ; exists (x=0 /\ y=1 /\ z=1 /\ 0:x5=0 /\ 0:x8=0 /\ 1:x5=0 /\ 1:x8=0)