Stack Overflow during Counterexample Generation

[Dargones]

Dafny version

nightly-2023-08-04

Code to produce this issue

class Seq {
  var s:seq<int>
  method test(i0:nat, val0:int, i1:nat, val1:int) 
    modifies this {
    assume 0 <= i0 < i1 < |s|;
    s := s[i0 := val0];
    s := s[i1 := val1];
    assert s[0] != 0;
  }
}

Command to run and resulting output

dafny /extractCounterexample /mv:~ /proverOpt:O:model_evaluator.completion=true /proverOpt:O:model.completion=true /proverOpt:O:model.compact=false file.dfy

What happened?

Stack Overflow (at Microsoft.Dafny.LanguageServer.CounterExampleGeneration.DafnyModel.GetDafnyType(Uninterpreted))

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

Mac