>>4
Oh right, I think I've got it. You have an S that randomly returns 0 or 1. Then wp(S, x=0 /\ x=1) = true, since it always happens regardless of initial state. But wp(S, x=0) and wp(S, x=1) will both be false since there's no initial state that will always satisfy the post-condition.