#define SZ 1000
int a[SZ];
int b[SZ];
int index[SZ];

void loop(int *restrict a, int *restrict b, int K)
{
    int i;

    /* Original code: ii=7 due to loop carried dependency bound
       (double indirection causes pointer aliasing issues). */
    //#pragma MUST_ITERATE(SZ, SZ, )
    //for (i = 0; i < SZ; i++) {
    //     a[index[i]] += K * b[i];
    //}

    /* Unrolled loop to let the compiler know that a[index[i]]
       cannot point to the same address as a[index[i+1]] etc. */
#pragma MUST_ITERATE(SZ/4, SZ/4, )
    for (i = 0; i < SZ; i+=4) {
        int *restrict tmp1 = &a[index[i]];
        int *restrict tmp2 = &a[index[i+1]];
        int *restrict tmp3 = &a[index[i+2]];
        int *restrict tmp4 = &a[index[i+3]];
                
        *tmp1 += K * b[i];
        *tmp2 += K * b[i+1];
        *tmp3 += K * b[i+2];
        *tmp4 += K * b[i+3];
    }
}