X86 X015+X016-F "Fre PodWW Rfi PodRR Fre PodWR Fre Rfi PodRR+Fre PodWR Fre PodWR Fre Rfi PodRR" {} P0 | P1 | P2 ; MOV [b],$1 | MOV [y],$1 | MOV [z],$1 ; MOV [a],$1 | MOV [d],$1 | MOV [c],$1 ; MOV [x],$1 | MFENCE | MOV EAX,[z] ; MFENCE | MOV EAX,[z] | MFENCE ; MOV ECX,[c] | MOV EBX,[b] | MOV EBX,[a] ; MOV EAX,[x] | | MOV ECX,[c] ; MOV EBX,[y] | | MOV EDX,[d] ; forall (0:EAX=1 /\ 2:EAX=1 /\ 2:ECX=1 /\ (0:EBX=1 /\ (0:ECX=1 /\ (1:EAX=1 /\ (1:EBX=1 /\ (2:EBX=1 /\ (2:EDX=1 \/ 2:EDX=0) \/ 2:EBX=0 /\ (2:EDX=1 \/ 2:EDX=0)) \/ 1:EBX=0 /\ (2:EBX=1 /\ 2:EDX=1 \/ 2:EBX=0 /\ (2:EDX=1 \/ 2:EDX=0))) \/ 1:EAX=0 /\ 2:EDX=1 /\ (1:EBX=1 /\ (2:EBX=1 \/ 2:EBX=0) \/ 1:EBX=0 /\ (2:EBX=1 \/ 2:EBX=0))) \/ 0:ECX=0 /\ 2:EBX=1 /\ (1:EAX=1 /\ (1:EBX=1 /\ (2:EDX=1 \/ 2:EDX=0) \/ 1:EBX=0 /\ 2:EDX=1) \/ 1:EAX=0 /\ 2:EDX=1 /\ (1:EBX=1 \/ 1:EBX=0))) \/ 0:EBX=0 /\ 1:EBX=1 /\ (0:ECX=1 /\ 1:EAX=1 /\ (2:EBX=1 /\ (2:EDX=1 \/ 2:EDX=0) \/ 2:EBX=0 /\ (2:EDX=1 \/ 2:EDX=0)) \/ 0:ECX=0 /\ 2:EBX=1 /\ (1:EAX=1 /\ (2:EDX=1 \/ 2:EDX=0) \/ 1:EAX=0 /\ 2:EDX=1))))