X86 SB+SB-BIS-A "Rfi PodRR Fre PodWR Fre+Rfi PodRR Fre PodWW Wse" {} P0 | P1 ; MOV %atom,$1 | MOV %atom,$2 ; XCHG [a],%atom | XCHG [b],%atom ; MOV %atom,$1 | MOV %atom,$1 ; XCHG [y],%atom | XCHG [x],%atom ; MOV %atom,$1 | MOV EBX,[b] ; XCHG [b],%atom | MOV ECX,[a] ; MOV EAX,[y] | MOV EAX,[y] ; MOV EBX,[x] | ; exists (0:EAX=1 /\ 0:EBX=0 /\ 1:EAX=0 \/ b=2 /\ 1:EBX=2 /\ 1:ECX=0)