X86 X022-A "Fre PodWW Wse Rfi PodRR" {} P0 | P1 ; MOV [y],$1 | MOV %atom,$2 ; MOV [x],$1 | XCHG [x],%atom ; | MOV EAX,[x] ; | MOV EBX,[y] ; forall (1:EAX=2 /\ (1:EBX=1 /\ (x=2 \/ x=1) \/ 1:EBX=0 /\ x=1) \/ 1:EAX=1 /\ 1:EBX=1 /\ x=1)