La precondición de Dafny 0 <= tamaño < capacidad podría no cumplirse.

Soy nuevo en Dafny y trato de averiguar por qué esto no funciona. Lo que quiero hacer es insertar 2 valores en mis arreglos, priorities y values.
Tengo el siguiente código:

class Queue<V> {
    var size: int;
    ghost var capacity: int;
    var priorities: array<int>;
    var values: array<V>;

    predicate Valid()
    reads this
    {
        0 <= size <= capacity &&
        capacity == priorities.Length &&
        capacity == values.Length
    }

    constructor(aCapacity: int, defaultValue: V)
    requires aCapacity >= 0
    ensures Valid()
    {
        size := 0;
        values := new V[aCapacity](i => defaultValue);
        priorities := new int[aCapacity];
        capacity := aCapacity;
    }

    method insertValues(priority: int, value: V)
    modifies this.values, this.priorities, this
    requires Valid()
    requires 0 <= size < capacity  // aquí está el problema
    ensures Valid()
    ensures capacity == values.Length && capacity == priorities.Length
    {
        this.values[size] := value;
        this.priorities[size] := priority;
        size := size + 1;
    }
}

method Main() {
    var queue := new Queue<int>(10, 0);
    queue.insertValues(1, 10);
    queue.insertValues(2, 11);
}

Pero cuando trato de probar mi método insertValues en Main, dice que:

call may violate context's modifies clause
A precondition for this call might not hold.

Y la precondición es 0 <= size < capacity. Gracias de antemano.