Injectivity check not performed inside a magic wand

[fpoli]

I would expect both methods below to be rejected, but apparently a true --* ... magic wand is enough to escape the injectivity checks.

predicate P(x: Ref)

method m1()
    requires forall s: Set[Ref] ::
        (forall x: Ref :: x in s ==> P(x)) // As expected: Contract might not be well-formed. Receiver of P(x) might not be injective.

method m2()
    requires forall s: Set[Ref] ::
        true --* (forall x: Ref :: x in s ==> P(x)) // This should be rejected, but it's accepted