Injectivity check for quantified predicates missing

[mschwerhoff]

Consider the following program:

predicate p(a: Ref, b: Ref)

method m(x: Ref, s: Set[Ref], t: Seq[Ref]) {
  exhale forall a: Int, b: Ref :: b in s && 0 <= a && a < |t| ==> p(t[a], b) // might not be injective
}

The QP assertion may not be injective in the predicate arguments (which Silicon reports), but Carbon only reports potentially insufficient permissions.