fix: Crash related to the override check for generic functions

Source/DafnyCore/Verifier/FunctionCallSubstituter.cs

@@ -19,17 +19,19 @@ public override Expression Substitute(Expression expr) {
       if (expr is FunctionCallExpr e) {
         var receiver = Substitute(e.Receiver);
         var newArgs = SubstituteExprList(e.Args);
+        var typeApplicationAtEnclosingClass = e.TypeApplication_AtEnclosingClass;
         Function function;
         if ((e.Function.EnclosingClass == Tr || Tr.InheritedMembers.Contains(e.Function)) && e.Receiver is ThisExpr && receiver is ThisExpr && Cl.Members.Find(m => m.OverriddenMember == e.Function) is { } f) {
           receiver = new ThisExpr((TopLevelDeclWithMembers)f.EnclosingClass);
           function = (Function)f;
+          typeApplicationAtEnclosingClass = receiver.Type.AsParentType(Cl).TypeArgs.ToList();
         } else {
           function = e.Function;
         }
         return new FunctionCallExpr(e.tok, e.Name, receiver, e.OpenParen, e.CloseParen, newArgs, e.AtLabel) {
           Function = function,
           Type = e.Type, // TODO: this may not work with type parameters.
-          TypeApplication_AtEnclosingClass = SubstituteTypeList(e.TypeApplication_AtEnclosingClass), // resolve here
+          TypeApplication_AtEnclosingClass = SubstituteTypeList(typeApplicationAtEnclosingClass), // resolve here
           TypeApplication_JustFunction = SubstituteTypeList(e.TypeApplication_JustFunction), // resolve here
           IsByMethodCall = e.IsByMethodCall
         };

Test/git-issues/git-issue-3691.dfy

@@ -0,0 +1,12 @@
+// RUN: %exits-with 0 %dafny /compile:0 /allocated:4 /functionSyntax:4 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+trait A {
+  predicate f()
+  method g() ensures f()
+}
+
+class B<T> extends A {
+  predicate f() { true }
+  method g() ensures f()
+}

Test/git-issues/git-issue-3691.dfy.expect

@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 2 verified, 0 errors

docs/dev/news/3692.fix

@@ -0,0 +1 @@
+Crash related to the override check for generic functions