Generated trigger by SimplifyNestedQuantifiers crashes Viper

[superaxander]

In the following program:

//@ requires \pointer(a, n, write);
void foo(int *a,  int n) {
    int half = n/2;
    int *b = a + half;
    //@ assert \pointer(b - half, half, write);
    // becomes assert (\forall* int i=0..half; Perm(b - half + i, write));
    // becomes assert (\forall* int i=0..half; Perm({:ptrAdd(ptrAdd(b, -half), i):}, write));
}

The SimplifyNestedQuantifiers pass generates a trigger for the quantifier because -half is independent of i and therefore constant. But since this computation is not lifted out of the trigger (for example into a let expression) this causes viper to crash due to the invalid trigger. Ideally the resulting quantifier looks like this:

\forall* int i = 0..half; (\let int x = ptrAdd(b, -half); Perm({:ptrAdd(x, i):}), write)