When exhaling a quantified permission, Carbon (in some cases) checks whether the exhaled fraction is strictly greater than 0. However, it should be fine to exhale 0 permission.
field f: Int
predicate P(x: Ref)
method m() {
label pre_stabilize0
exhale forall z: Ref :: acc(z.f, none) //this works
exhale (forall x: Ref:: acc(P(x), none)) //this fails
}
When exhaling a quantified permission, Carbon (in some cases) checks whether the exhaled fraction is strictly greater than 0. However, it should be fine to exhale 0 permission.