int A:mo (B b, int i) {
  guard = pc ⊔ level(b) ⊔ obj_level(b) = ⊥;
}