Error condition statically unreachable, schematic, reached

[bobismijnnaam]

The following program:

class Channels {
  int a;

  inline resource fields() = Perm(a, 1);
}

ensures \result != null && \result.length == N;
ensures (\forall* int tid = 0 .. N; Perm(\result[tid], write) ** \result[tid].fields());
Channels[] veymontChannelInit(int N) {
  inhale false;
}

requires N >= 1;
void main(int N) {
  Channels[] channels = veymontChannelInit(N);

  par (int tid = 0 .. N) 
  requires Perm(channels[tid], write) ** channels[tid].fields();
  {

  }
}

When executed gives the following unexpected error:

$ ~/Workbench/Tools/vercors_dev/bin/vct rr.pvl --backend-option --assumeInjectivityOnInhale
[581/623] vercors.buildInfo.resources
[INFO] Starting verification
[WARN] The binder `(\forall* int tid; tid \in {0 .. N_2030433136} ==> (\let Channels_1583364970 self = \result[tid]; Perm(self.a_2141871959, 1)))` contains no triggers
[WARN] The binder `(\forall* int tid; tid \in {0 .. N_265219} ==> (\let Channels_1583364970 self = channels_58514318[tid]; Perm(self.a_2141871959, 1)))` contains no triggers
An error condition was reached, which should be statically unreachable. schematic. Inner failure:
 > ======================================
 > At rr.pvl:17:3:
 > --------------------------------------
 >    15    Channels[] channels = veymontChannelInit(N);
 >    16
 >         [-------------------------
 >    17    par (int tid = 0 .. N)
 >    18    requires Perm(channels[tid], write) ** channels[tid].fields();
 >    19    {
 >    20
 >    21    }
 >        ---]
 >    22  }
 >    23
 > --------------------------------------
 > There may be insufficient permission to access this field here. (https://utwente.nl/vercors#perm)
 > ======================================

It seems to originate from the following forperm expression, which is from the encoding of the par block:

      label beforeFrame
      excBeforeLoop := exc
      flatten1 := true
      once := flatten1
      while (once)
        invariant exc == excBeforeLoop
        invariant once ==>
          acc(aloc(opt_get1(channels), tid1).ref, write) &&
          (let self ==
            (aloc(opt_get1(channels), tid1).ref) in
            acc(self.a, 1 * write)) &&
          [(forperm obj: Ref [obj.a] :: obj.a == old[beforeFrame](obj.a)) &&
          (forperm
            obj: Ref [obj.ref] :: obj.ref == old[beforeFrame](obj.ref)),
          true]