Dafny "вызов может нарушить условие изменения контекста"

Я новичок в Дафни. Я получаю сообщение об ошибке: call might violate context's modifies clause в строке, где Seek() вызывает Step() в следующем коде:

class Tape {
  var val : int;

  constructor() {
    this.val := 0;
  }

  method Write(x : int)
    modifies this
  {
    this.val := x;
  }
}

class Simulator {
  var tape : Tape;
  var step_num : nat;

  constructor() {
    this.tape := new Tape();
    this.step_num := 0;
  }

  method Step()
    modifies this, this.tape
    ensures this.step_num > old(this.step_num)
  {
    this.tape.Write(1);
    this.step_num := this.step_num + 1;
  }

  method Seek(target_step_num : int)
    modifies this, this.tape
  {
    while this.step_num < target_step_num {
      this.Step();
    }
  }
}

Я не понимаю, что здесь происходит, потому что я явно добавил Seek() к modifies this, this.tape.

Осматриваясь в Интернете, я вижу некоторые разговоры о «свежести», и у меня создается впечатление, что это связано с тем, что у меня есть разрешение на доступ this.tape, но я не понимаю, как это исправить. Спасибо!