Check for recursive predicates using /all/ existing predicates.

[ionathanch]

This now passes instead of failing (lifted from silicon/0196.vpr:

predicate P(r: Ref) {forall e : Ref :: e in refs(r) ==> acc(Q(e), wildcard)}
predicate P2(r: Ref) {forall e : Ref :: e in refs(r) ==> acc(Q(e), 1/2)}
predicate R(r: Ref) {forall e : Ref :: e in refs(r) ==> acc(e.q, wildcard)}
predicate R2(r: Ref) {forall e : Ref :: e in refs(r) ==> acc(e.q, 1/2)}
predicate Q(r: Ref)
field q: Ref
function refs(r: Ref) : Set[Ref]

(See comment in #38)

[jyoo980]

Oops, should have told you I was working on this....

[jyoo980]

I'm running my local change and the error in #38 is gone, as we suspected.

[ionathanch]

Oops, should have told you I was working on this....

I probably should've asked lmao Did you have anything different?

[jyoo980]

Nope, I have the exact same diff.