fix: Missing substitution in the subset check of the function overrid…

…e check (#4060)

Fixes #4056.

Source/DafnyCore/Verifier/Translator.cs

@@ -3682,8 +3682,10 @@ private void AddFunctionOverrideSubsetChk(Function func, BoogieStmtListBuilder b
       Dictionary<TypeParameter, Type> typeMap) {
       //getting framePrime
       List<FrameExpression> traitFrameExps = new List<FrameExpression>();
+      FunctionCallSubstituter sub = null;
       foreach (var e in func.OverriddenFunction.Reads) {
-        var newE = Substitute(e.E, null, substMap, typeMap);
+        sub ??= new FunctionCallSubstituter(substMap, typeMap, (TraitDecl)func.OverriddenFunction.EnclosingClass, (ClassLikeDecl)func.EnclosingClass);
+        var newE = sub.Substitute(e.E);
         FrameExpression fe = new FrameExpression(e.tok, newE, e.FieldName);
         traitFrameExps.Add(fe);
       }

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

@@ -0,0 +1,17 @@
+// RUN: %baredafny verify %args %s > %t
+// RUN: %diff "%s.expect" "%t"
+
+trait ADT {
+  ghost function ReprFamily(n: nat): set<object>
+    decreases n
+    ensures n > 0 ==> ReprFamily(n) >= ReprFamily(n-1)
+    reads this, if n == 0 then {} else ReprFamily(n-1)
+}
+
+class P extends ADT {
+  ghost function ReprFamily(n: nat): set<object>
+    decreases n
+    ensures n > 0 ==> ReprFamily(n) >= ReprFamily(n-1)
+    reads this, if n == 0 then {} else ReprFamily(n-1)
+  { {} }
+}

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

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

docs/dev/news/4056.fix

@@ -0,0 +1 @@
+Regression in the subset check of the function override check