From 0c312061114a7e83cc147a799bcf556cfcfe6245 Mon Sep 17 00:00:00 2001
From: Fabio Madge <fmadge@amazon.com>
Date: Mon, 12 Jun 2023 22:27:42 +0200
Subject: [PATCH] fix: Missing substitution in the subset check of the function
 override check (#4060)

Fixes #4056.
---
 Source/DafnyCore/Verifier/Translator.cs   |  4 +++-
 Test/git-issues/git-issue-4056.dfy        | 17 +++++++++++++++++
 Test/git-issues/git-issue-4056.dfy.expect |  2 ++
 docs/dev/news/4056.fix                    |  1 +
 4 files changed, 23 insertions(+), 1 deletion(-)
 create mode 100644 Test/git-issues/git-issue-4056.dfy
 create mode 100644 Test/git-issues/git-issue-4056.dfy.expect
 create mode 100644 docs/dev/news/4056.fix

diff --git a/Source/DafnyCore/Verifier/Translator.cs b/Source/DafnyCore/Verifier/Translator.cs
index 4b3c6ec2163..d8a2b74ec14 100644
--- a/Source/DafnyCore/Verifier/Translator.cs
+++ b/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);
       }
diff --git a/Test/git-issues/git-issue-4056.dfy b/Test/git-issues/git-issue-4056.dfy
new file mode 100644
index 00000000000..842e0e6e1ad
--- /dev/null
+++ b/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)
+  { {} }
+}
diff --git a/Test/git-issues/git-issue-4056.dfy.expect b/Test/git-issues/git-issue-4056.dfy.expect
new file mode 100644
index 00000000000..00a51f822da
--- /dev/null
+++ b/Test/git-issues/git-issue-4056.dfy.expect
@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 3 verified, 0 errors
diff --git a/docs/dev/news/4056.fix b/docs/dev/news/4056.fix
new file mode 100644
index 00000000000..83e5f005d1f
--- /dev/null
+++ b/docs/dev/news/4056.fix
@@ -0,0 +1 @@
+Regression in the subset check of the function override check