SB+SC "forall (0:EAX=1 \/ 1:EAX=1)"