Specification on codatatype function triggers wrong encoding

[MikaelMayer]

Dafny version

latest-nightly

Code to produce this issue

// A heap is an infinite stream of heap fields
  codatatype Heap = HeapElem(alloc: bool, tail: Heap)
  {
    predicate AllFalse() {
      !alloc && tail.AllFalse()
    }
    static function Init(): Heap
      ensures Init().AllFalse()
    {
      HeapElem(false, Init())
    }
  }
  method {:test} Test() {
    var h := Heap.Init();
  }

Command to run and resulting output

SHIFT+F5 to run the tests in VSCode.

Test: Stack overflow.
Repeat 19261 times:
--------------------------------
   at _module.Heap.Init()
--------------------------------
   at _module.__default.Test()

What happened?

Init() was compiled like a regular method. If I remove the specification, it works.

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

Windows