Module BO__BufferOverrunProofObligations.Condition