How to prove created-ness of variable that is reassigned in loop?

[FliegendeWurst]

I'm having trouble proving a method that is similar to the below.

import java.util.List;
import java.util.ArrayList;

public class LoopList {
    /*@ public normal_behavior
      @ ensures \result >= 0;
      @*/
    static int reassignList() {
        int iter = 0;
        List list = new ArrayList();
        list.add(new Object());
        /*@ loop_invariant
          @  list != null
          @  && \invariant_for(list)
          @  && iter >= 0
          @  && iter <= 20
          @ ;
          @ decreases 20 - iter;
          @ assignable list, iter;
          @*/
        while (!list.isEmpty() && iter < 20) {
            list = new ArrayList();
            iter++;
        }
        return iter;
    }
}

The problem is that I want to use list in the loop condition, but I can't close the Pre (isEmpty) branch. I get stuck on ==> list_0.<created>@heapAfter_add[anon({}, anon_heap_LOOP_0)]. I've tried adding list.<created> to the loop invariant, but that is a syntax error. How can I track the createdness of list in the invariant?