I'm new to Dafny. I'm getting the error: `call might violate context's modifies clause` on the line where `Seek()` calls `Step()` in the following code:

```
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();
    }
  }
}

```

I don't understand what's going on here because I explicitly annotated `Seek()` with `modifies this, this.tape`.

Looking around online I see some talk about "freshness" and I get the impression that this has to do with ensuring that I have permission to access `this.tape`, but I don't understand how to fix it. Thanks!