(Test Generation) stack overflow during test generation related to self-referencing objects

[Dargones]

Dafny version

4.0.0

Code to produce this issue

module M {

    class LoopingList {

        var next:LoopingList;
        var value:int;

        constructor() {
            value := 0;
            next := this;
        }

        method getValue() returns (value:int) {
            return this.value;
        }
    }
}

Command to run and resulting output

dotnet ~/RiderProjects/dafny/Binaries/Dafny.dll generate-tests Block example.dfy

Program terminates with a stack overflow, the following trace causing infinite recursion:


DafnyTestGeneration.TestMethod.GetClassTypeInstance
DafnyTestGeneration.TestMethod.GetDefaultValue
DafnyTestGeneration.TestMethod.GetFieldValue

### What happened?

Field `next` is irrelevant for a counterexample used by test generation and so test generation must figure out by itself the value of this field. It should assign the field of the object to the object itself, producing the test below:

```Dafny
method {:test} test0() {
  var loopingList0 : M.LoopingList := getFreshMLoopingList();
  loopingList0.next := loopingList0;
  loopingList0.value := 12;
  var r0 := loopingList0.getValue();
}

method {:synthesize} getFreshMLoopingList() returns (o:M.LoopingList) ensures fresh(o)

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

Linux