Initialize array within function

[lwli11]

Is there a reason why I can't initialize an array within a function like this? If I move the identical declaration outside to a global variable and add the requires/ensures, then it works.
 

int main()
{

        char arr[]={'1', '2', '3', '4', '5', '6', '7', '8', '9', '0', '1'};
for (int i=0; i<10; i++)
        /*@
                inv
                take x = each(u64 k; k>=0u64 && k<10u64){Owned<char>(array_shift<char>(&arr, k))};
                {&arr} unchanged;
@*/
        {
                int j=0;
        if (i>=0 && i<10){
        /*@ extract Owned<char>, (u64) i; @*/

                arr[i]=0;
        }
        }
}