Apparent unsoundness when doing nested (un)foldings with wildcards

[marcoeilers]

The following verifies but shouldn't:

predicate P(r: Ref) {
  Q(r) &&
  unfolding Q(r) in true
}

predicate Q(r: Ref) {true}

predicate R(r: Ref) {
  P(r) && unfolding P(r) in true
}

method test01(r: Ref) returns ()
  requires P(r)
{
  fold acc(R(r), wildcard)

  //:: ExpectedOutput(assert.failed:assertion.false)
  assert false
}

The problem is that constrainableARPs contains more than it should, so this is a variation of #290.

[marcoeilers]

Another instance:

predicate P2(r: Ref) {
  Q2(r) &&
  f2(r)
}

function f2(r: Ref): Bool
  requires Q2(r)
{ true }

predicate Q2(r: Ref) {true}

predicate R2(r: Ref) {
  P2(r) && unfolding P2(r) in true
}

method test02(r: Ref) returns ()
  requires P2(r)
{
  fold acc(R2(r), wildcard)

  //:: ExpectedOutput(assert.failed:assertion.false)
  assert false
}