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