// DELIBERATELY BROKEN: unfolds `evenCount` and never folds it back before the
// procedure returns. Raven's atomicity analysis rejects this too, with:
//
//   [Error] Unclosed AU token or invariant
//
// ("AU token" refers to atomic updates, a Part 5 topic -- this same message
// covers both cases, since structurally they're the same discipline: you
// borrowed a resource that only exists while briefly unfolded, and never
// gave it back.)
field count: Int

inv evenCount(c: Ref) {
  exists v: Int :: own(c.count, v) && v % 2 == 0
}

proc bumpForgetFold(c: Ref)
  requires evenCount(c)
{
  unfold evenCount(c);
  val _x := faa(c.count, 2);
}