Consistency errors with triggers

[JLedelay]

The following input:

class C {
    final Object[] arr;

    /*@
        inline resource common() =
            arr != null ** 
            Perm(arr[*], 1\2) **
            (\forall int i = 0 .. arr.length; 
                (\forall int j = 0 .. arr.length; i != j ==>
                    arr[i] != arr[j]));
    @*/

    //@ requires common();
    void m() {

    }
}

Gives the following output:

[INFO] Starting verification
[WARN] The binder '(\forall int i; true; (i\memberof{0 .. this.arr.length}) ==> (\forall int j; true; (j\memberof{0 .. this.arr.length}) && i != j ==> this.arr[i] != this.arr[j]))' contains no triggers
The silver AST delivered to viper is not valid:
 - Consistency error: Variable i is not mentioned in one or more triggers. (Test.java-13-18;unique_id=302)
 - Consistency error: Variable i is not mentioned in one or more triggers. (Test.java-13-18;unique_id=390)

Note that no triggers were specified in the source file. If any triggers are added, these errors don't go away.