Inside of a loop after an array of booleans have been allocated, the invariant allocated(sieve) reports true however, attempting to assert the Preserved predicate on the sieve array after an assignment asserts the following error. Why does it report this error and how do I resolve it?

    twostate predicate Preserved(sieve: array<bool>, i: nat) 
        requires 2 <= i < sieve.Length
        reads sieve
    {
        i*i < sieve.Length && multiset(old(sieve[..i*i])) == multiset(sieve[..i*i])
    }

argument at index 0 for parameter ‘sieve’ could not be proved to be allocated in the two-state function’s previous state — if you add ‘new’ before the parameter declaration, like ‘new sieve: array’, arguments can refer to expressions possibly unallocated in the previous state