Smol bugs

[ionathanch]

Propagating none permission fails verification

field x: Int
field y: Ref

predicate P(this: Ref) {
  acc(this.y) && acc(this.y.x)
}

method test(this: Ref)
  requires acc(P(this), none) {}

expands to

method test(this: Ref)
  requires acc(this.y, write * none) && acc(this.y.x, write * none) {}

which doesn't pass verification.

Assertions delayed by predicates no longer delayed

predicate bad(b: Bool) {b}

method lazy()
  requires bad(false)
{
  assert false
}

should not pass verification, but it expands to the following, which does:

method lazy()
  requires false
{
  assert false
}