X86 X022+X023 "Fre PodWW Wse Rfi PodRR+Fre PodWW Wse Rfi PodRR Fre PodWW Wse Rfi PodRR" {} P0 | P1 | P2 | P3 ; MOV [y],$1 | MOV [x],$2 | MOV [d],$2 | MOV [c],$1 ; MOV [x],$1 | MOV EAX,[x] | MOV EAX,[d] | MOV [d],$1 ; MOV [b],$2 | MOV EBX,[y] | MOV EBX,[a] | ; MOV EAX,[b] | MOV [a],$1 | | ; MOV EBX,[c] | MOV [b],$1 | | ; forall (0:EAX=2 /\ (0:EBX=1 /\ (1:EAX=2 /\ (1:EBX=1 /\ (2:EAX=2 /\ (2:EBX=1 /\ ([b]=2 /\ ([d]=2 /\ ([x]=2 \/ [x]=1) \/ [d]=1 /\ ([x]=2 \/ [x]=1)) \/ [b]=1 /\ ([d]=2 /\ ([x]=2 \/ [x]=1) \/ [d]=1 /\ ([x]=2 \/ [x]=1))) \/ 2:EBX=0 /\ ([b]=2 /\ ([d]=2 /\ ([x]=2 \/ [x]=1) \/ [d]=1 /\ ([x]=2 \/ [x]=1)) \/ [b]=1 /\ ([d]=2 /\ ([x]=2 \/ [x]=1) \/ [d]=1 /\ ([x]=2 \/ [x]=1)))) \/ 2:EAX=1 /\ ([d]=1 /\ (2:EBX=1 /\ ([b]=2 /\ ([x]=2 \/ [x]=1) \/ [b]=1 /\ ([x]=2 \/ [x]=1)) \/ 2:EBX=0 /\ ([b]=2 /\ ([x]=2 \/ [x]=1) \/ [b]=1 /\ ([x]=2 \/ [x]=1))))) \/ 1:EBX=0 /\ ([x]=1 /\ (2:EAX=2 /\ (2:EBX=1 /\ ([b]=2 /\ ([d]=2 \/ [d]=1) \/ [b]=1 /\ ([d]=2 \/ [d]=1)) \/ 2:EBX=0 /\ ([b]=2 /\ ([d]=2 \/ [d]=1) \/ [b]=1 /\ ([d]=2 \/ [d]=1))) \/ 2:EAX=1 /\ ([d]=1 /\ (2:EBX=1 /\ ([b]=2 \/ [b]=1) \/ 2:EBX=0 /\ ([b]=2 \/ [b]=1)))))) \/ 1:EAX=1 /\ (1:EBX=1 /\ ([x]=1 /\ (2:EAX=2 /\ (2:EBX=1 /\ ([b]=2 /\ ([d]=2 \/ [d]=1) \/ [b]=1 /\ ([d]=2 \/ [d]=1)) \/ 2:EBX=0 /\ ([b]=2 /\ ([d]=2 \/ [d]=1) \/ [b]=1 /\ ([d]=2 \/ [d]=1))) \/ 2:EAX=1 /\ ([d]=1 /\ (2:EBX=1 /\ ([b]=2 \/ [b]=1) \/ 2:EBX=0 /\ ([b]=2 \/ [b]=1))))))) \/ 0:EBX=0 /\ (1:EAX=2 /\ (1:EBX=1 /\ (2:EAX=2 /\ (2:EBX=1 /\ ([b]=2 /\ ([d]=2 /\ ([x]=2 \/ [x]=1) \/ [d]=1 /\ ([x]=2 \/ [x]=1)) \/ [b]=1 /\ ([d]=2 /\ ([x]=2 \/ [x]=1) \/ [d]=1 /\ ([x]=2 \/ [x]=1))) \/ 2:EBX=0 /\ ([b]=2 /\ ([d]=1 /\ ([x]=2 \/ [x]=1)) \/ [b]=1 /\ ([d]=2 /\ ([x]=2 \/ [x]=1) \/ [d]=1 /\ ([x]=2 \/ [x]=1)))) \/ 2:EAX=1 /\ ([d]=1 /\ (2:EBX=1 /\ ([b]=2 /\ ([x]=2 \/ [x]=1) \/ [b]=1 /\ ([x]=2 \/ [x]=1)) \/ 2:EBX=0 /\ ([b]=1 /\ ([x]=2 \/ [x]=1))))) \/ 1:EBX=0 /\ ([x]=1 /\ (2:EAX=2 /\ (2:EBX=1 /\ ([b]=2 /\ ([d]=2 \/ [d]=1) \/ [b]=1 /\ ([d]=2 \/ [d]=1)) \/ 2:EBX=0 /\ ([b]=2 /\ ([d]=1) \/ [b]=1 /\ ([d]=2 \/ [d]=1))) \/ 2:EAX=1 /\ ([d]=1 /\ (2:EBX=1 /\ ([b]=2 \/ [b]=1) \/ 2:EBX=0 /\ ([b]=1)))))) \/ 1:EAX=1 /\ (1:EBX=1 /\ ([x]=1 /\ (2:EAX=2 /\ (2:EBX=1 /\ ([b]=2 /\ ([d]=2 \/ [d]=1) \/ [b]=1 /\ ([d]=2 \/ [d]=1)) \/ 2:EBX=0 /\ ([b]=2 /\ ([d]=1) \/ [b]=1 /\ ([d]=2 \/ [d]=1))) \/ 2:EAX=1 /\ ([d]=1 /\ (2:EBX=1 /\ ([b]=2 \/ [b]=1) \/ 2:EBX=0 /\ ([b]=1)))))))) \/ 0:EAX=1 /\ ([b]=1 /\ (0:EBX=1 /\ (1:EAX=2 /\ (1:EBX=1 /\ (2:EAX=2 /\ (2:EBX=1 /\ ([d]=2 /\ ([x]=2 \/ [x]=1) \/ [d]=1 /\ ([x]=2 \/ [x]=1)) \/ 2:EBX=0 /\ ([d]=2 /\ ([x]=2 \/ [x]=1) \/ [d]=1 /\ ([x]=2 \/ [x]=1))) \/ 2:EAX=1 /\ ([d]=1 /\ (2:EBX=1 /\ ([x]=2 \/ [x]=1) \/ 2:EBX=0 /\ ([x]=2 \/ [x]=1)))) \/ 1:EBX=0 /\ ([x]=1 /\ (2:EAX=2 /\ (2:EBX=1 /\ ([d]=2 \/ [d]=1) \/ 2:EBX=0 /\ ([d]=2 \/ [d]=1)) \/ 2:EAX=1 /\ ([d]=1 /\ (2:EBX=1 \/ 2:EBX=0))))) \/ 1:EAX=1 /\ (1:EBX=1 /\ ([x]=1 /\ (2:EAX=2 /\ (2:EBX=1 /\ ([d]=2 \/ [d]=1) \/ 2:EBX=0 /\ ([d]=2 \/ [d]=1)) \/ 2:EAX=1 /\ ([d]=1 /\ (2:EBX=1 \/ 2:EBX=0)))))) \/ 0:EBX=0 /\ (1:EAX=2 /\ (1:EBX=1 /\ (2:EAX=2 /\ (2:EBX=1 /\ ([d]=2 /\ ([x]=2 \/ [x]=1) \/ [d]=1 /\ ([x]=2 \/ [x]=1)) \/ 2:EBX=0 /\ ([d]=1 /\ ([x]=2 \/ [x]=1))) \/ 2:EAX=1 /\ (2:EBX=1 /\ ([d]=1 /\ ([x]=2 \/ [x]=1)))) \/ 1:EBX=0 /\ ([x]=1 /\ (2:EAX=2 /\ (2:EBX=1 /\ ([d]=2 \/ [d]=1) \/ 2:EBX=0 /\ ([d]=1)) \/ 2:EAX=1 /\ (2:EBX=1 /\ ([d]=1))))) \/ 1:EAX=1 /\ (1:EBX=1 /\ ([x]=1 /\ (2:EAX=2 /\ (2:EBX=1 /\ ([d]=2 \/ [d]=1) \/ 2:EBX=0 /\ ([d]=1)) \/ 2:EAX=1 /\ (2:EBX=1 /\ ([d]=1)))))))))