Heap location is added to the known-folded permission mask in fold statements even if the permission amount is zero

[Dev-XYS]

In the Viper program below, predicate P contains zero permission to x.f. When fold P(x) updates the known-folded permission mask of P, x.f is added without checking if the permission amount is strictly positive. This results in x.f, which is not actually folded in P, being stored in the known-folded permission mask and not getting havoced in the following exhale statement. This leads to an unsoundness.

field f: Int

predicate P(x: Ref)
{
    acc(x.f, 0/1)
}

method foo(x: Ref)
    requires acc(x.f) && x.f == 1
{
    fold P(x)
    exhale acc(x.f)
    inhale acc(x.f) && x.f == 2
    assert false
}

[Dev-XYS]

This also applies when the predicate body contains another predicate instance and the permission to that predicate equals 0.