Resolution slowdown

[MikaelMayer]

Dafny version

latest-nightly

Code to produce this issue

First, start with the following code in VSCode in an untitled document, with verification on change enabled.

class ResizeableArray<T> {
  var entries: array<T>
  var length: nat
  function capacity(): nat { entries.Length }
  constructor() ensures Valid() {
    entries := new T[0];
    length := 0;
  }
  predicate Valid() {
    length <= entries.Length
  }
  method Push(t: T) requires Valid() ensures Valid() modifies this`entries, this.entries {
    if length == entries.Length {
      var newCapacity := if entries.Length == 0 then 1 else entries.Length * 2;
      var oldLength := entries.Length;
      entries := new T[newCapacity](i requires 0 <= i < newCapacity reads entries[i] => 
        if i < oldLength then entries[i] else t);
    } else {
      entries[length] := t;
    }
    length := length + 1;
  }
}

Command to run and resulting output

Then, transform it as follow:
- Remove '[i]' from 'reads entries[i]' and wait
- Just before the assignment entries = new T[newCapacity];, add 'var oldEntries := entries[..];' and wait. Sometimes this step is extremely slow to resolve, sometimes not.
- Remove ' reads entries' alltogether
- In the callback of the array constructor, change 'entries' to 'oldEntries'
- Change 'modifies this`entries' into 'modifies this'
- Add 'reads this' to the 'Valid()' predicate
- Add 'reads this' to the 'Capacity()' function

The resulting code should be:

class ResizeableArray<T> {
  var entries: array<T>
  var length: nat
  function capacity(): nat reads this { entries.Length }
  constructor() ensures Valid() {
    entries := new T[0];
    length := 0;
  }
  predicate Valid() reads this {
    length <= entries.Length
  }
  method Push(t: T) requires Valid() ensures Valid() modifies this, this.entries {
    if length == entries.Length {
      var newCapacity := if entries.Length == 0 then 1 else entries.Length * 2;
      var oldLength := entries.Length;
      var oldEntries := entries[..];
      entries := new T[newCapacity](i requires 0 <= i < newCapacity => 
        if i < oldLength then oldEntries[i] else t);
    } else {
      entries[length] := t;
    }
    length := length + 1;
  }
}

What happened?

The first time I tried doing that, It hanged a lot (there were no other Dafny files), and the last step took easily a minute while it was stuck in "Parsing failed" when there were no parsing errors.
I could not reproduce it despite doing these exact steps again and again. Logging in for reference.

What type of operating system are you experiencing the problem on?

Windows

[keyboardDrummer]

I could not reproduce it despite doing these exact steps again and again. Logging in for reference.

That's a shame. I would love to look into any performance issue, if there is a reproduction

[keyboardDrummer]

Closing since there doesn't seem to be even a complicated way of reproducing this