Verifying D programs

[roxanaRA]

Hello,

I am working on a project to verify D programs and I am using Smack.
I created a template for loop invariants in D and I wanted to use Smack with it. The following is an example:

mixin template LoopInvariant() {
    void call_invariant(T...)(T params) {

        static if (params.length == 3) {
            for(int k = params[0]; k < params[1]; k++)
                        params[2](k);
        }
    }
}

int getMaxIndex(int[] array, int n) {
    int i = 0;
    int index = 0;

    while (i < n) {

        /* I want to replace this with my template  
        for(int k = 0; k < i; k++) {
            __VERIFIER_assert(array[k] <= array[index]); 
        }*/
        
        mixin LoopInvariant!();
        call_invariant(0, i, ((int k) => __VERIFIER_assert(array[k] <= array[index])));

        if (array[i] > array[index])
            index = i;
        i = i + 1;

    }

    return index;
}

The code with the for loop worked fine with Smack.
I want to replace the commented for loop with my template.
This construction worked in D with D assert at runtime, however when I try it with Smack and __VERIFIER_assert the assert is always false.

Regarding this problem, I tried an easier example:

void foo() {
int index = 12345;

mixin LoopInvariant!();
call_invariant(0, 1, ((int k) => __VERIFIER_assert(k < index)));
}

Looking at the Boogie code I found out that the index variable outside the lambda call and the index variable inside the lambda function are in different memories locations.
In D, at runtime, the index from the lambda function can be inferred as the one from outside it. I was wondering if this inference can be added into Smack?

Thank you