Combining permission amounts from folded predicate and QP incompleteness

[JonasAlaif]

And another one, sorry @marcoeilers
The following program with quantified permissions and folding fails to verify in Silicon but works in Carbon:

field ref: Ref
predicate T(x: Ref) {
  acc(x.ref)
}

method foo(lft: Map[Ref, Perm], x: Ref, p: Perm)
  requires forall r: Ref :: r in lft && lft[r] >= 0/1 && lft[r] <= 1/1 && acc(T(r), lft[r])
  requires p > 0/1 && acc(x.ref, p)
{
  fold acc(T(x), p)
  assert acc(T(x), p + lft[x])
}

The strange thing is that it works without the fold:

method bar(lft: Map[Ref, Perm], x: Ref, p: Perm)
  requires forall r: Ref :: r in lft && lft[r] >= 0/1 && lft[r] <= 1/1 && acc(T(r), lft[r])
  requires p > 0/1 && acc(T(x), p) // <- get the predicate directly
{
  assert acc(T(x), p + lft[x])
}

[marcoeilers]

Everything verifies for me with master Silicon (and no options).

[JonasAlaif]

Seems that it was also fixed by #696, sorry I didn't think the two were related :P