Fix stack overflow

Source/DafnyLanguageServer.Test/Various/CounterExampleTest.cs

@@ -1533,6 +1533,30 @@ class C<T> {
  Assert.True(counterExamples[0].Variables.ContainsKey("b:M.C.Equal$T"));
  Assert.True(counterExamples[0].Variables.ContainsKey("this:M.C<M.C$T>"));
  }
+
+ /// <summary>
+ /// This test case would previously lead to stack overflow because of infinite recursion in GetDafnyType
+ /// </summary>
+ [Theory]
+ [MemberData(nameof(OptionSettings))]
+ public async Task GetDafnyTypeInfiniteRecursion(List<Action<DafnyOptions>> optionSettings) {
+ await SetUpOptions(optionSettings);
+ var source = @"
+ 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;
+ }
+ }
+ ".TrimStart();
+ var documentItem = CreateTestDocument(source);
+ await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken);
+ (await RequestCounterExamples(documentItem.Uri)).ToList();;
+ }
 
  public CounterExampleTest(ITestOutputHelper output) : base(output) {
  }

Source/DafnyLanguageServer/CounterExampleGeneration/DafnyModel.cs

@@ -303,6 +303,16 @@ public class DafnyModel {
  /// This method tries to extract the base type (so seq<char> instead of string)
  /// </summary>
  private Type GetDafnyType(Model.Uninterpreted element) {
+ var finalResult = UnknownType;
+ foreach (var typeElement in GetIsResults(element)) {
+ var reconstructedType = ReconstructType(typeElement);
+ if (reconstructedType is not UserDefinedType userDefinedType) {
+ return reconstructedType;
+ }
+ if (finalResult.Name.EndsWith("?") || finalResult == UnknownType) {
+ finalResult = userDefinedType;
+ }
+ }
  var seqOperation = fSeqAppend.AppWithResult(element);
  seqOperation ??= fSeqDrop.AppWithResult(element);
  seqOperation ??= fSeqTake.AppWithResult(element);
@@ -351,16 +361,6 @@ public class DafnyModel {
  if (fCharToInt.OptEval(element) != null) {
  return Type.Char;
  }
- var finalResult = UnknownType;
- foreach (var typeElement in GetIsResults(element)) {
- var reconstructedType = ReconstructType(typeElement);
- if (reconstructedType is not UserDefinedType userDefinedType) {
- return reconstructedType;
- }
- if (finalResult.Name.EndsWith("?") || finalResult == UnknownType) {
- finalResult = userDefinedType;
- }
- }
  if (finalResult != UnknownType) {
  return finalResult;
  }