RISCV SWAP-LR-SC+FULL { 0:x5=x; 1:x5=x; } P0 | P1 ; ori x6,x0,1 | ori x6,x0,2 ; lr.w x7,0(x5) | lr.w x7,0(x5) ; sc.w x8,x6,0(x5) | sc.w x8,x6,0(x5) ; forall (x=1 /\ 1:x7=0 /\ 0:x7=2) \/ (0:x7=0 /\ x=2 /\ 1:x7=1) \/ (not (0:x8 = 0) \/ not (1:x8 = 0))