diff --git a/Source/DafnyCore/Compilers/Java/Compiler-java.cs b/Source/DafnyCore/Compilers/Java/Compiler-java.cs
index 03fd4a3bd9e..1d110cd315f 100644
--- a/Source/DafnyCore/Compilers/Java/Compiler-java.cs
+++ b/Source/DafnyCore/Compilers/Java/Compiler-java.cs
@@ -1801,8 +1801,8 @@ IClassWriter CompileDatatypeBase(DatatypeDecl dt, ConcreteSyntaxTree wr) {
       foreach (var ctor in dt.Ctors.Where(ctor => !ctor.IsGhost)) {
         wr.Write($"public static{justTypeArgs} {DtT_protected} {DtCreateName(ctor)}(");
         WriteFormals("", ctor.Formals, wr);
-        var w = wr.NewBlock(")");
-        w.Write($"return new {DtCtorDeclarationName(ctor, dt.TypeArgs)}({ctor.Formals.Where(f => !f.IsGhost).Comma(FormalName)});");
+        wr.NewBlock(")")
+          .WriteLine($"return new {DtCtorDeclarationName(ctor, dt.TypeArgs)}({ctor.Formals.Where(f => !f.IsGhost).Comma(FormalName)});");
       }
 
       if (dt.IsRecordType) {
@@ -1813,7 +1813,7 @@ IClassWriter CompileDatatypeBase(DatatypeDecl dt, ConcreteSyntaxTree wr) {
         wr.Write($"public static{justTypeArgs} {DtT_protected} create_{ctor.CompileName}(");
         WriteFormals("", ctor.Formals, wr);
         wr.NewBlock(")")
-          .Write($"return create({ctor.Formals.Where(f => !f.IsGhost).Comma(FormalName)});");
+          .WriteLine($"return create({ctor.Formals.Where(f => !f.IsGhost).Comma(FormalName)});");
       }
 
       // query properties
diff --git a/Source/DafnyCore/Resolver/CallGraphBuilder.cs b/Source/DafnyCore/Resolver/CallGraphBuilder.cs
index 1122c328080..d6377bfb229 100644
--- a/Source/DafnyCore/Resolver/CallGraphBuilder.cs
+++ b/Source/DafnyCore/Resolver/CallGraphBuilder.cs
@@ -295,6 +295,9 @@ public static void AddCallGraphEdge(IASTVisitorContext callingContext, ICallable
         ModuleDefinition calleeModule = callable is SpecialFunction ? null : callable.EnclosingModule;
         if (callerModule != calleeModule) {
           // inter-module call; don't record in call graph
+          if (callingContext is ICallable context && callable is Function { EnclosingClass: TraitDecl }) {
+            callerModule.CallGraph.AddEdge(context, callable);
+          }
           return;
         }
 
diff --git a/Source/DafnyCore/Verifier/FunctionCallSubstituter.cs b/Source/DafnyCore/Verifier/FunctionCallSubstituter.cs
index be765714d9b..bea1d11dfae 100644
--- a/Source/DafnyCore/Verifier/FunctionCallSubstituter.cs
+++ b/Source/DafnyCore/Verifier/FunctionCallSubstituter.cs
@@ -1,30 +1,38 @@
 using System.Collections.Generic;
+using System.Linq;
 
 namespace Microsoft.Dafny {
   public class FunctionCallSubstituter : Substituter {
-    public readonly Function A, B;
-    public FunctionCallSubstituter(Expression receiverReplacement, Dictionary<IVariable, Expression/*!*/>/*!*/ substMap, Function a, Function b)
-      : base(receiverReplacement, substMap, new Dictionary<TypeParameter, Type>()) {
-      A = a;
-      B = b;
+    public readonly TraitDecl Tr;
+    public readonly ClassDecl Cl;
+
+    // We replace all occurrences of the trait version of the function with the class version. This is only allowed if
+    // the receiver is `this`. We underapproximate this by looking for a `ThisExpr`, which misses more complex
+    // expressions that evaluate to one.
+    public FunctionCallSubstituter(Dictionary<IVariable, Expression/*!*/>/*!*/ substMap, Dictionary<TypeParameter, Type> typeMap, TraitDecl Tr, ClassDecl Cl)
+      : base(null, substMap, typeMap) {
+      this.Tr = Tr;
+      this.Cl = Cl;
     }
+
     public override Expression Substitute(Expression expr) {
-      if (expr is FunctionCallExpr) {
-        FunctionCallExpr e = (FunctionCallExpr)expr;
-        Expression receiver = Substitute(e.Receiver);
-        List<Expression> newArgs = SubstituteExprList(e.Args);
-        FunctionCallExpr newFce = new FunctionCallExpr(expr.tok, e.Name, receiver, e.OpenParen, e.CloseParen, newArgs, e.AtLabel);
-        if (e.Function == A) {
-          newFce.Function = B;
-          newFce.Type = e.Type; // TODO: this may not work with type parameters.
+      if (expr is FunctionCallExpr e) {
+        var receiver = Substitute(e.Receiver);
+        var newArgs = SubstituteExprList(e.Args);
+        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;
         } else {
-          newFce.Function = e.Function;
-          newFce.Type = e.Type;
+          function = e.Function;
         }
-        newFce.TypeApplication_AtEnclosingClass = e.TypeApplication_AtEnclosingClass;  // resolve here
-        newFce.TypeApplication_JustFunction = e.TypeApplication_JustFunction;  // resolve here
-        newFce.IsByMethodCall = e.IsByMethodCall;
-        return newFce;
+        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_JustFunction = SubstituteTypeList(e.TypeApplication_JustFunction), // resolve here
+          IsByMethodCall = e.IsByMethodCall
+        };
       }
       return base.Substitute(expr);
     }
diff --git a/Source/DafnyCore/Verifier/Translator.ClassMembers.cs b/Source/DafnyCore/Verifier/Translator.ClassMembers.cs
index 10c96e1a5c3..fa0aee6f06b 100644
--- a/Source/DafnyCore/Verifier/Translator.ClassMembers.cs
+++ b/Source/DafnyCore/Verifier/Translator.ClassMembers.cs
@@ -173,7 +173,7 @@ void AddMethod_Top(Method m, bool isByMethod, bool includeAllMethods) {
             AddMethodImpl(m, proc, true);
           }
         }
-        if (m.OverriddenMethod != null && InVerificationScope(m)) //method has overrided a parent method
+        if (m.OverriddenMethod != null && InVerificationScope(m)) //method has overridden a parent method
         {
           var procOverrideChk = AddMethod(m, MethodTranslationKind.OverrideCheck);
           sink.AddTopLevelDeclaration(procOverrideChk);
@@ -877,8 +877,8 @@ private void AddFunctionOverrideCheckImpl(Function f) {
       }
       // the procedure itself
       var req = new List<Boogie.Requires>();
-      // free requires mh == ModuleContextHeight && fh == FunctionContextHeight;
-      req.Add(Requires(f.tok, true, etran.HeightContext(f.OverriddenFunction), null, null));
+      // free requires fh == FunctionContextHeight;
+      req.Add(Requires(f.tok, true, etran.HeightContext(f), null, null));
       if (f is TwoStateFunction) {
         // free requires prevHeap == Heap && HeapSucc(prevHeap, currHeap) && IsHeap(currHeap)
         var a0 = Boogie.Expr.Eq(prevHeap, ordinaryEtran.HeapExpr);
@@ -920,18 +920,16 @@ private void AddFunctionOverrideCheckImpl(Function f) {
       }
 
       var substMap = new Dictionary<IVariable, Expression>();
-      for (int i = 0; i < f.Formals.Count; i++) {
-        //get corresponsing formal in the class
-        var ie = new IdentifierExpr(f.Formals[i].tok, f.Formals[i].AssignUniqueName(f.IdGenerator));
-        ie.Var = f.Formals[i]; ie.Type = ie.Var.Type;
-        substMap.Add(f.OverriddenFunction.Formals[i], ie);
+      foreach (var (formal, overriddenFormal) in f.Formals.Zip(f.OverriddenFunction.Formals, Tuple.Create)) {
+        // get corresponding formal in the class
+        var ie = new IdentifierExpr(formal.tok, formal.AssignUniqueName(f.IdGenerator)) { Var = formal, Type = formal.Type };
+        substMap.Add(overriddenFormal, ie);
       }
 
       if (f.OverriddenFunction.Result != null) {
         Contract.Assert(pOut != null);
-        //get corresponsing formal in the class
-        var ie = new IdentifierExpr(pOut.tok, pOut.AssignUniqueName(f.IdGenerator));
-        ie.Var = pOut; ie.Type = ie.Var.Type;
+        //get corresponding formal in the class
+        var ie = new IdentifierExpr(pOut.tok, pOut.AssignUniqueName(f.IdGenerator)) { Var = pOut, Type = pOut.Type };
         substMap.Add(f.OverriddenFunction.Result, ie);
       }
 
@@ -947,7 +945,6 @@ private void AddFunctionOverrideCheckImpl(Function f) {
       AddFunctionOverrideSubsetChk(f, builder, etran, localVariables, substMap, typeMap);
 
       //adding assume Q; assert Post’;
-      //adding assume J.F(ins) == C.F(ins);
       AddFunctionOverrideEnsChk(f, builder, etran, substMap, typeMap, implInParams, implOutParams.Count == 0 ? null : implOutParams[0]);
 
       var stmts = builder.Collect(f.tok);
@@ -956,9 +953,9 @@ private void AddFunctionOverrideCheckImpl(Function f) {
         // emit the impl only when there are proof obligations.
         QKeyValue kv = etran.TrAttributes(f.Attributes, null);
 
-        var impl = AddImplementationWithVerboseName(f.tok, proc,
-          Util.Concat(Util.Concat(typeInParams, inParams_Heap), implInParams),
-          implOutParams, localVariables, stmts, kv);
+        AddImplementationWithVerboseName(f.tok, proc,
+            Util.Concat(Util.Concat(typeInParams, inParams_Heap), implInParams),
+            implOutParams, localVariables, stmts, kv);
       }
 
       if (InsertChecksums) {
@@ -999,7 +996,7 @@ private void AddOverrideCheckTypeArgumentInstantiations(MemberDecl member, Boogi
     ///   axiom (forall $heap: HeapType, typeArgs: Ty, this: ref, x#0: int, fuel: LayerType ::
     ///     { J.F(fuel, $heap, G(typeArgs), this, x#0), C.F(fuel, $heap, typeArgs, this, x#0) }
     ///     { J.F(fuel, $heap, G(typeArgs), this, x#0), $Is(this, C) }
-    ///     this != null && $Is(this, C)
+    ///     C.F#canCall(args) || (fh < FunctionContextHeight && this != null && $Is(this, C))
     ///     ==>
     ///     J.F(fuel, $heap, G(typeArgs), this, x#0) == C.F(fuel, $heap, typeArgs, this, x#0));
     /// (without the other usual antecedents).  Essentially, the override gives a part of the body of the
@@ -1043,19 +1040,20 @@ private Boogie.Axiom FunctionOverrideAxiom(Function f, Function overridingFuncti
       argsJF.AddRange(GetTypeArguments(f, overridingFunction).ConvertAll(TypeToTy));
       argsCF.AddRange(GetTypeArguments(overridingFunction, null).ConvertAll(TypeToTy));
 
+      var moreArgsCF = new List<Boogie.Expr>();
+      Expr layer = null;
+
       // Add the fuel argument
       if (f.IsFuelAware()) {
         Contract.Assert(overridingFunction.IsFuelAware());  // f.IsFuelAware() ==> overridingFunction.IsFuelAware()
         var fuel = new Boogie.BoundVariable(f.tok, new Boogie.TypedIdent(f.tok, "$fuel", predef.LayerType));
         forallFormals.Add(fuel);
-        var ly = new Boogie.IdentifierExpr(f.tok, fuel);
-        argsJF.Add(ly);
-        argsCF.Add(ly);
+        layer = new Boogie.IdentifierExpr(f.tok, fuel);
+        argsJF.Add(layer);
       } else if (overridingFunction.IsFuelAware()) {
         // We can't use a bound variable $fuel, because then one of the triggers won't be mentioning this $fuel.
         // Instead, we do the next best thing: use the literal $LZ.
-        var ly = new Boogie.IdentifierExpr(f.tok, "$LZ", predef.LayerType); // $LZ
-        argsCF.Add(ly);
+        layer = new Boogie.IdentifierExpr(f.tok, "$LZ", predef.LayerType); // $LZ
       }
 
       // Add heap arguments
@@ -1063,7 +1061,7 @@ private Boogie.Axiom FunctionOverrideAxiom(Function f, Function overridingFuncti
         Contract.Assert(bvPrevHeap != null);
         forallFormals.Add(bvPrevHeap);
         argsJF.Add(etran.Old.HeapExpr);
-        argsCF.Add(etran.Old.HeapExpr);
+        moreArgsCF.Add(etran.Old.HeapExpr);
       }
       if (AlwaysUseHeap || f.ReadsHeap || overridingFunction.ReadsHeap) {
         var heap = new Boogie.BoundVariable(f.tok, new Boogie.TypedIdent(f.tok, predef.HeapVarName, predef.HeapType));
@@ -1072,7 +1070,7 @@ private Boogie.Axiom FunctionOverrideAxiom(Function f, Function overridingFuncti
           argsJF.Add(new Boogie.IdentifierExpr(f.tok, heap));
         }
         if (AlwaysUseHeap || overridingFunction.ReadsHeap) {
-          argsCF.Add(new Boogie.IdentifierExpr(overridingFunction.tok, heap));
+          moreArgsCF.Add(new Boogie.IdentifierExpr(overridingFunction.tok, heap));
         }
       }
 
@@ -1082,10 +1080,12 @@ private Boogie.Axiom FunctionOverrideAxiom(Function f, Function overridingFuncti
       forallFormals.Add(bvThis);
       var bvThisExpr = new Boogie.IdentifierExpr(f.tok, bvThis);
       argsJF.Add(bvThisExpr);
-      argsCF.Add(bvThisExpr);
+      moreArgsCF.Add(bvThisExpr);
       // $Is(this, C)
       var isOfSubtype = GetWhereClause(overridingFunction.tok, bvThisExpr, thisType, f is TwoStateFunction ? etran.Old : etran, IsAllocType.NEVERALLOC);
 
+      Bpl.Expr ante = Boogie.Expr.And(ReceiverNotNull(bvThisExpr), isOfSubtype);
+
       // Add other arguments
       var typeMap = GetTypeArgumentSubstitutionMap(f, overridingFunction);
       foreach (Formal p in f.Formals) {
@@ -1094,13 +1094,26 @@ private Boogie.Axiom FunctionOverrideAxiom(Function f, Function overridingFuncti
         forallFormals.Add(bv);
         var jfArg = new Boogie.IdentifierExpr(p.tok, bv);
         argsJF.Add(ModeledAsBoxType(p.Type) ? BoxIfUnboxed(jfArg, pType) : jfArg);
-        argsCF.Add(new Boogie.IdentifierExpr(p.tok, bv));
+        moreArgsCF.Add(new Boogie.IdentifierExpr(p.tok, bv));
       }
 
-      // useViaContext: (mh != ModuleContextHeight || fh != FunctionContextHeight)
-      ModuleDefinition mod = f.EnclosingClass.EnclosingModuleDefinition;
-      Boogie.Expr useViaContext = !InVerificationScope(overridingFunction) ? (Boogie.Expr)Boogie.Expr.True :
-        Boogie.Expr.Neq(Boogie.Expr.Literal(mod.CallGraph.GetSCCRepresentativePredecessorCount(overridingFunction)), etran.FunctionContextHeight());
+      // useViaContext: fh < FunctionContextHeight
+      Boogie.Expr useViaContext = !InVerificationScope(overridingFunction)
+        ? Boogie.Expr.True
+        : Boogie.Expr.Lt(Boogie.Expr.Literal(forModule.CallGraph.GetSCCRepresentativePredecessorCount(overridingFunction)), etran.FunctionContextHeight());
+
+      // useViaCanCall: C.F#canCall(args)
+      Bpl.IdentifierExpr canCallFuncID = new Bpl.IdentifierExpr(overridingFunction.tok, overridingFunction.FullSanitizedName + "#canCall", Bpl.Type.Bool);
+      Bpl.Expr useViaCanCall = new Bpl.NAryExpr(f.tok, new Bpl.FunctionCall(canCallFuncID), Concat(argsCF, moreArgsCF));
+
+      if (layer != null) {
+        argsCF.Add(layer);
+      }
+
+      argsCF = Concat(argsCF, moreArgsCF);
+
+      // ante := useViaCanCall || (useViaContext && this != null && $Is(this, C))
+      ante = Bpl.Expr.Or(useViaCanCall, BplAnd(useViaContext, ante));
 
       Boogie.Expr funcAppl;
       {
@@ -1133,8 +1146,8 @@ private Boogie.Axiom FunctionOverrideAxiom(Function f, Function overridingFuncti
 
       // The axiom
       Boogie.Expr ax = BplForall(f.tok, new List<Boogie.TypeVariable>(), forallFormals, null, tr,
-        Boogie.Expr.Imp(Boogie.Expr.And(ReceiverNotNull(bvThisExpr), isOfSubtype), synonyms));
-      var activate = AxiomActivation(f, etran);
+        Boogie.Expr.Imp(ante, synonyms));
+      var activate = AxiomActivation(overridingFunction, etran);
       string comment = "override axiom for " + f.FullSanitizedName + " in class " + overridingFunction.EnclosingClass.FullSanitizedName;
       return new Boogie.Axiom(f.tok, Boogie.Expr.Imp(activate, ax), comment);
     }
@@ -1192,13 +1205,11 @@ private void AddMethodOverrideEnsChk(Method m, BoogieStmtListBuilder builder, Ex
         builder.Add(TrAssumeCmd(m.tok, etran.TrExpr(en.E)));
       }
       //generating trait post-conditions with class variables
+      FunctionCallSubstituter sub = null;
       foreach (var en in m.OverriddenMethod.Ens) {
-        Expression postcond = Substitute(en.E, null, substMap, typeMap);
-        bool splitHappened;  // we actually don't care
-        foreach (var s in TrSplitExpr(postcond, etran, false, out splitHappened)) {
-          if (s.IsChecked) {
-            builder.Add(Assert(m.tok, s.E, new PODesc.EnsuresStronger()));
-          }
+        sub ??= new FunctionCallSubstituter(substMap, typeMap, (TraitDecl)m.OverriddenMethod.EnclosingClass, (ClassDecl)m.EnclosingClass);
+        foreach (var s in TrSplitExpr(sub.Substitute(en.E), etran, false, out _).Where(s => s.IsChecked)) {
+          builder.Add(Assert(m.tok, s.E, new PODesc.EnsuresStronger()));
         }
       }
     }
@@ -1211,18 +1222,14 @@ private void AddMethodOverrideReqsChk(Method m, BoogieStmtListBuilder builder, E
       Contract.Requires(etran != null);
       Contract.Requires(substMap != null);
       //generating trait pre-conditions with class variables
+      FunctionCallSubstituter sub = null;
       foreach (var req in m.OverriddenMethod.Req) {
-        Expression precond = Substitute(req.E, null, substMap, typeMap);
-        builder.Add(TrAssumeCmd(m.tok, etran.TrExpr(precond)));
+        sub ??= new FunctionCallSubstituter(substMap, typeMap, (TraitDecl)m.OverriddenMethod.EnclosingClass, (ClassDecl)m.EnclosingClass);
+        builder.Add(TrAssumeCmd(m.tok, etran.TrExpr(sub.Substitute(req.E))));
       }
       //generating class pre-conditions
-      foreach (var req in m.Req) {
-        bool splitHappened;  // we actually don't care
-        foreach (var s in TrSplitExpr(req.E, etran, false, out splitHappened)) {
-          if (s.IsChecked) {
-            builder.Add(Assert(m.tok, s.E, new PODesc.RequiresWeaker()));
-          }
-        }
+      foreach (var s in m.Req.SelectMany(req => TrSplitExpr(req.E, etran, false, out _).Where(s => s.IsChecked))) {
+        builder.Add(Assert(m.tok, s.E, new PODesc.RequiresWeaker()));
       }
     }
 
@@ -1381,7 +1388,7 @@ private Boogie.Procedure AddMethod(Method m, MethodTranslationKind kind) {
       // FREE PRECONDITIONS
       if (kind == MethodTranslationKind.SpecWellformedness || kind == MethodTranslationKind.Implementation || kind == MethodTranslationKind.OverrideCheck) {  // the other cases have no need for a free precondition
         // free requires mh == ModuleContextHeight && fh == FunctionContextHeight;
-        req.Add(Requires(m.tok, true, etran.HeightContext(kind == MethodTranslationKind.OverrideCheck ? m.OverriddenMethod : m), null, null));
+        req.Add(Requires(m.tok, true, etran.HeightContext(m), null, null));
         if (m is TwoStateLemma) {
           // free requires prevHeap == Heap && HeapSucc(prevHeap, currHeap) && IsHeap(currHeap)
           var a0 = Boogie.Expr.Eq(prevHeap, ordinaryEtran.HeapExpr);
diff --git a/Source/DafnyCore/Verifier/Translator.cs b/Source/DafnyCore/Verifier/Translator.cs
index 1fb4c2f1264..169864d8561 100644
--- a/Source/DafnyCore/Verifier/Translator.cs
+++ b/Source/DafnyCore/Verifier/Translator.cs
@@ -709,6 +709,7 @@ public Bpl.IdentifierExpr TrVar(IToken tok, IVariable var) {
 
     private Bpl.Program DoTranslation(Program p, ModuleDefinition forModule) {
       program = p;
+      this.forModule = forModule;
       Type.EnableScopes();
 
       EstablishModuleScope(p.BuiltIns.SystemModule, forModule);
@@ -2050,11 +2051,10 @@ void AddFunctionConsequenceAxiom(Boogie.Function boogieFunction, Function f, Lis
       //
       // AXIOM_ACTIVATION
       // means:
-      //   mh < ModuleContextHeight ||
-      //   (mh == ModuleContextHeight && fh <= FunctionContextHeight)
+      //   fh <= FunctionContextHeight
       //
       // USE_VIA_CONTEXT
-      //   (mh != ModuleContextHeight || fh != FunctionContextHeight) &&
+      //   fh < FunctionContextHeight &&
       //   GOOD_PARAMETERS
       // where GOOD_PARAMETERS means:
       //   $IsGoodHeap($Heap) && this != null && formals-have-the-expected-types &&
@@ -2166,10 +2166,10 @@ void AddFunctionConsequenceAxiom(Boogie.Function boogieFunction, Function f, Lis
       foreach (AttributedExpression req in f.Req) {
         pre = BplAnd(pre, etran.TrExpr(req.E));
       }
-      // useViaContext: (mh != ModuleContextHeight || fh != FunctionContextHeight)
-      var mod = f.EnclosingClass.EnclosingModuleDefinition;
-      Bpl.Expr useViaContext = !InVerificationScope(f) ? Bpl.Expr.True :
-        (Bpl.Expr)Bpl.Expr.Neq(Bpl.Expr.Literal(mod.CallGraph.GetSCCRepresentativePredecessorCount(f)), etran.FunctionContextHeight());
+      // useViaContext: fh < FunctionContextHeight
+      Expr useViaContext = !(InVerificationScope(f) || (f.EnclosingClass is TraitDecl))
+        ? Bpl.Expr.True
+        : Bpl.Expr.Lt(Expr.Literal(forModule.CallGraph.GetSCCRepresentativePredecessorCount(f)), etran.FunctionContextHeight());
       // useViaCanCall: f#canCall(args)
       Bpl.IdentifierExpr canCallFuncID = new Bpl.IdentifierExpr(f.tok, f.FullSanitizedName + "#canCall", Bpl.Type.Bool);
       Bpl.Expr useViaCanCall = new Bpl.NAryExpr(f.tok, new Bpl.FunctionCall(canCallFuncID), Concat(tyargs, args));
@@ -2276,11 +2276,9 @@ Bpl.Expr AxiomActivation(Function f, ExpressionTranslator etran) {
       Contract.Requires(f != null);
       Contract.Requires(etran != null);
       Contract.Requires(VisibleInScope(f));
-      var module = f.EnclosingClass.EnclosingModuleDefinition;
-
       if (InVerificationScope(f)) {
         return
-          Bpl.Expr.Le(Bpl.Expr.Literal(module.CallGraph.GetSCCRepresentativePredecessorCount(f)), etran.FunctionContextHeight());
+          Bpl.Expr.Le(Bpl.Expr.Literal(forModule.CallGraph.GetSCCRepresentativePredecessorCount(f)), etran.FunctionContextHeight());
       } else {
         return Bpl.Expr.True;
       }
@@ -2312,15 +2310,15 @@ private Axiom GetFunctionAxiom(Function f, Expression body, List<Formal> lits) {
       //
       // AXIOM_ACTIVATION
       // for visibility==ForeignModuleOnly, means:
-      //   mh < ModuleContextHeight
+      //   true
       // for visibility==IntraModuleOnly, means:
-      //   mh == ModuleContextHeight && fh <= FunctionContextHeight
+      //   fh <= FunctionContextHeight
       //
       // USE_VIA_CONTEXT
       // for visibility==ForeignModuleOnly, means:
       //   GOOD_PARAMETERS
       // for visibility==IntraModuleOnly, means:
-      //   fh != FunctionContextHeight &&
+      //   fh < FunctionContextHeight &&
       //   GOOD_PARAMETERS
       // where GOOD_PARAMETERS means:
       //   $IsGoodHeap($Heap) && this != null && formals-have-the-expected-types &&
@@ -2525,12 +2523,11 @@ private Axiom GetFunctionAxiom(Function f, Expression body, List<Formal> lits) {
         return null;
       }
 
-      // useViaContext: (mh != ModuleContextHeight || fh != FunctionContextHeight)
+      // useViaContext: fh < FunctionContextHeight
       ModuleDefinition mod = f.EnclosingClass.EnclosingModuleDefinition;
       Bpl.Expr useViaContext = !InVerificationScope(f)
-        ? (Bpl.Expr)Bpl.Expr.True
-        : Bpl.Expr.Neq(Bpl.Expr.Literal(mod.CallGraph.GetSCCRepresentativePredecessorCount(f)),
-          etran.FunctionContextHeight());
+        ? Bpl.Expr.True
+        : Bpl.Expr.Lt(Bpl.Expr.Literal(forModule.CallGraph.GetSCCRepresentativePredecessorCount(f)), etran.FunctionContextHeight());
       // ante := (useViaContext && typeAnte && pre)
       ante = BplAnd(useViaContext, BplAnd(ante, pre));
 
@@ -3172,6 +3169,7 @@ Bpl.Expr InSeqRange(IToken tok, Bpl.Expr index, Type indexType, Bpl.Expr seq, bo
     }
 
     ModuleDefinition currentModule = null;  // the module whose members are currently being translated
+    ModuleDefinition forModule = null;  // the root module
     ICallable codeContext = null;  // the method/iterator whose implementation is currently being translated or the function whose specification is being checked for well-formedness
     Bpl.LocalVariable yieldCountVariable = null;  // non-null when an iterator body is being translated
     bool inBodyInitContext = false;  // true during the translation of the .BodyInit portion of a divided constructor body
@@ -3504,65 +3502,40 @@ private void AddFunctionOverrideEnsChk(Function f, BoogieStmtListBuilder builder
         builder.Add(TrAssumeCmd(f.tok, etran.TrExpr(en.E)));
       }
 
-      //generating assume J.F(ins) == C.F(ins)
-      Bpl.FunctionCall funcIdC = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, f.FullSanitizedName, TrType(f.ResultType)));
-      Bpl.FunctionCall funcIdT = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.OverriddenFunction.tok, f.OverriddenFunction.FullSanitizedName, TrType(f.OverriddenFunction.ResultType)));
-      List<Bpl.Expr> argsC = new List<Bpl.Expr>();
-      List<Bpl.Expr> argsT = new List<Bpl.Expr>();
-      // add type arguments
-      argsT.AddRange(GetTypeArguments(f.OverriddenFunction, f).ConvertAll(TypeToTy));
-      argsC.AddRange(GetTypeArguments(f, null).ConvertAll(TypeToTy));
-      // add fuel arguments
-      if (f.IsFuelAware()) {
-        argsC.Add(etran.layerInterCluster.GetFunctionFuel(f));
-      }
-      if (f.OverriddenFunction.IsFuelAware()) {
-        argsT.Add(etran.layerInterCluster.GetFunctionFuel(f));
-      }
-      // add heap arguments
-      if (f is TwoStateFunction) {
-        argsC.Add(etran.Old.HeapExpr);
-        argsT.Add(etran.Old.HeapExpr);
-      }
-      if (AlwaysUseHeap || f.ReadsHeap) {
-        argsC.Add(etran.HeapExpr);
-      }
-      if (AlwaysUseHeap || f.OverriddenFunction.ReadsHeap) {
-        argsT.Add(etran.HeapExpr);
-      }
-      // add "ordinary" parameters (including "this", if any)
-      var prefixCount = implInParams.Count - f.Formals.Count;
-      for (var i = 0; i < implInParams.Count; i++) {
-        Bpl.Expr cParam = new Bpl.IdentifierExpr(f.tok, implInParams[i]);
-        Bpl.Expr tParam = new Bpl.IdentifierExpr(f.OverriddenFunction.tok, implInParams[i]);
-        if (prefixCount <= i && ModeledAsBoxType(f.OverriddenFunction.Formals[i - prefixCount].Type)) {
-          tParam = BoxIfNecessary(f.tok, tParam, f.Formals[i - prefixCount].Type);
-        }
-        argsC.Add(cParam);
-        argsT.Add(tParam);
-      }
-      Bpl.Expr funcExpC = new Bpl.NAryExpr(f.tok, funcIdC, argsC);
-      Bpl.Expr funcExpT = new Bpl.NAryExpr(f.OverriddenFunction.tok, funcIdT, argsT);
-      var funcExpCPossiblyBoxed = funcExpC;
-      if (ModeledAsBoxType(f.OverriddenFunction.ResultType)) {
-        funcExpCPossiblyBoxed = BoxIfUnboxed(funcExpCPossiblyBoxed, f.ResultType);
-      }
-      builder.Add(TrAssumeCmd(f.tok, Bpl.Expr.Eq(funcExpCPossiblyBoxed, funcExpT)));
-
       //generating assume C.F(ins) == out, if a result variable was given
       if (resultVariable != null) {
+        var funcIdC = new FunctionCall(new Bpl.IdentifierExpr(f.tok, f.FullSanitizedName, TrType(f.ResultType)));
+        var argsC = new List<Bpl.Expr>();
+
+        // add type arguments
+        argsC.AddRange(GetTypeArguments(f, null).ConvertAll(TypeToTy));
+
+        // add fuel arguments
+        if (f.IsFuelAware()) {
+          argsC.Add(etran.layerInterCluster.GetFunctionFuel(f));
+        }
+
+        // add heap arguments
+        if (f is TwoStateFunction) {
+          argsC.Add(etran.Old.HeapExpr);
+        }
+        if (AlwaysUseHeap || f.ReadsHeap) {
+          argsC.Add(etran.HeapExpr);
+        }
+
+        argsC.AddRange(implInParams.Select(var => new Bpl.IdentifierExpr(f.tok, var)));
+
+        var funcExpC = new Bpl.NAryExpr(f.tok, funcIdC, argsC);
         var resultVar = new Bpl.IdentifierExpr(resultVariable.tok, resultVariable);
         builder.Add(TrAssumeCmd(f.tok, Bpl.Expr.Eq(funcExpC, resultVar)));
       }
 
       //generating trait post-conditions with class variables
+      FunctionCallSubstituter sub = null;
       foreach (var en in f.OverriddenFunction.Ens) {
-        Expression postcond = Substitute(en.E, null, substMap, typeMap);
-        bool splitHappened;  // we don't actually care
-        foreach (var s in TrSplitExpr(postcond, etran, false, out splitHappened)) {
-          if (s.IsChecked) {
-            builder.Add(Assert(f.tok, s.E, new PODesc.FunctionContractOverride(true)));
-          }
+        sub ??= new FunctionCallSubstituter(substMap, typeMap, (TraitDecl)f.OverriddenFunction.EnclosingClass, (ClassDecl)f.EnclosingClass);
+        foreach (var s in TrSplitExpr(sub.Substitute(en.E), etran, false, out _).Where(s => s.IsChecked)) {
+          builder.Add(Assert(f.tok, s.E, new PODesc.FunctionContractOverride(true)));
         }
       }
     }
@@ -3653,18 +3626,14 @@ private void AddFunctionOverrideReqsChk(Function f, BoogieStmtListBuilder builde
       Contract.Requires(etran != null);
       Contract.Requires(substMap != null);
       //generating trait pre-conditions with class variables
+      FunctionCallSubstituter sub = null;
       foreach (var req in f.OverriddenFunction.Req) {
-        Expression precond = Substitute(req.E, null, substMap, typeMap);
-        builder.Add(TrAssumeCmd(f.tok, etran.TrExpr(precond)));
+        sub ??= new FunctionCallSubstituter(substMap, typeMap, (TraitDecl)f.OverriddenFunction.EnclosingClass, (ClassDecl)f.EnclosingClass);
+        builder.Add(TrAssumeCmd(f.tok, etran.TrExpr(sub.Substitute(req.E))));
       }
       //generating class pre-conditions
-      foreach (var req in f.Req) {
-        bool splitHappened;  // we actually don't care
-        foreach (var s in TrSplitExpr(req.E, etran, false, out splitHappened)) {
-          if (s.IsChecked) {
-            builder.Add(Assert(f.tok, s.E, new PODesc.FunctionContractOverride(false)));
-          }
-        }
+      foreach (var s in f.Req.SelectMany(req => TrSplitExpr(req.E, etran, false, out _).Where(s => s.IsChecked))) {
+        builder.Add(Assert(f.tok, s.E, new PODesc.FunctionContractOverride(false)));
       }
     }
 
diff --git a/Test/concurrency/01-InnerOuter.dfy b/Test/concurrency/01-InnerOuter.dfy
index 62ac4f891f8..ce833e2bcfd 100644
--- a/Test/concurrency/01-InnerOuter.dfy
+++ b/Test/concurrency/01-InnerOuter.dfy
@@ -84,7 +84,7 @@ class Inner extends O {
     && old(data) <= data
   }
 
-  twostate lemma adm() {}
+  twostate lemma adm() requires admPre() {}
 
   constructor (ghost s: S, initial_data: int)
     requires s.i()
diff --git a/Test/concurrency/01-InnerOuter.dfy.expect b/Test/concurrency/01-InnerOuter.dfy.expect
index 5ed0d97333e..b49c1470365 100644
--- a/Test/concurrency/01-InnerOuter.dfy.expect
+++ b/Test/concurrency/01-InnerOuter.dfy.expect
@@ -1,2 +1,2 @@
 
-Dafny program verifier finished with 31 verified, 0 errors
+Dafny program verifier finished with 32 verified, 0 errors
diff --git a/Test/concurrency/02-DoubleRead.dfy b/Test/concurrency/02-DoubleRead.dfy
index 11a3a86ab27..ae119a45d8d 100644
--- a/Test/concurrency/02-DoubleRead.dfy
+++ b/Test/concurrency/02-DoubleRead.dfy
@@ -111,7 +111,7 @@ class ArcAtomicIsize extends Object {
   }
 
   // Admissibility proof
-  twostate lemma adm() {}
+  twostate lemma adm() requires admPre() {}
 
   constructor (ghost universe: Universe, initial_data: int)
     requires universe.i()
diff --git a/Test/concurrency/02-DoubleRead.dfy.expect b/Test/concurrency/02-DoubleRead.dfy.expect
index a61fd92d975..3e2e11e1866 100644
--- a/Test/concurrency/02-DoubleRead.dfy.expect
+++ b/Test/concurrency/02-DoubleRead.dfy.expect
@@ -1,2 +1,2 @@
 
-Dafny program verifier finished with 39 verified, 0 errors
+Dafny program verifier finished with 40 verified, 0 errors
diff --git a/Test/concurrency/03-SimpleCounter.dfy b/Test/concurrency/03-SimpleCounter.dfy
index d6a78609235..e0b01497246 100644
--- a/Test/concurrency/03-SimpleCounter.dfy
+++ b/Test/concurrency/03-SimpleCounter.dfy
@@ -112,7 +112,7 @@ class ArcAtomicIsize extends Object {
   }
 
   // Admissibility proof
-  twostate lemma adm() {}
+  twostate lemma adm() requires admPre() {}
 
   constructor (ghost universe: Universe, initial_data: int)
     requires universe.i()
diff --git a/Test/concurrency/03-SimpleCounter.dfy.expect b/Test/concurrency/03-SimpleCounter.dfy.expect
index bba7f9e68b7..1b45cf86b6a 100644
--- a/Test/concurrency/03-SimpleCounter.dfy.expect
+++ b/Test/concurrency/03-SimpleCounter.dfy.expect
@@ -1,2 +1,2 @@
 
-Dafny program verifier finished with 41 verified, 0 errors
+Dafny program verifier finished with 42 verified, 0 errors
diff --git a/Test/concurrency/10-SequenceInvariant.dfy b/Test/concurrency/10-SequenceInvariant.dfy
index a9bff354a68..00b90d095ff 100644
--- a/Test/concurrency/10-SequenceInvariant.dfy
+++ b/Test/concurrency/10-SequenceInvariant.dfy
@@ -256,7 +256,7 @@ class Thread extends Object {
   }
   twostate lemma baseFieldsInvMonotonicity() requires old(baseFieldsInv()) && old(universe.content) <= universe.content && unchanged(this) ensures baseFieldsInv() {}
 
-  predicate localInv() reads * {
+  predicate localInv() reads * ensures localInv() ==> objectGlobalBaseInv() {
     && objectGlobalBaseInv()
   }
   predicate inv() reads * ensures inv() ==> localInv() {
@@ -322,7 +322,7 @@ trait OwnedObject extends Object {
     assert owner in universe.content;
   }
 
-  predicate localInv() reads * {
+  predicate localInv() reads * ensures localInv() ==> objectGlobalBaseInv() {
     && objectGlobalBaseInv()
     && localUserInv()
   }
diff --git a/Test/concurrency/11-MutexGuard2.dfy b/Test/concurrency/11-MutexGuard2.dfy
index ac2aca3197a..12f8f44288c 100644
--- a/Test/concurrency/11-MutexGuard2.dfy
+++ b/Test/concurrency/11-MutexGuard2.dfy
@@ -261,7 +261,7 @@ class Thread extends Object {
   }
   twostate lemma baseFieldsInvMonotonicity() requires old(baseFieldsInv()) && old(universe.content) <= universe.content && unchanged(this) ensures baseFieldsInv() {}
 
-  predicate localInv() reads * {
+  predicate localInv() reads * ensures localInv() ==> objectGlobalBaseInv() {
     && objectGlobalBaseInv()
   }
   predicate inv() reads * ensures inv() ==> localInv() {
@@ -332,7 +332,7 @@ trait OwnedObject extends Object {
     && unchangedNonvolatileUserFields()
   }
 
-  predicate localInv() reads * {
+  predicate localInv() reads * ensures localInv() ==> objectGlobalBaseInv() {
     && objectGlobalBaseInv()
     && localUserInv()
   }
diff --git a/Test/concurrency/12-MutexLifetime-short.dfy b/Test/concurrency/12-MutexLifetime-short.dfy
index 5598fa22a50..b2f99b05827 100644
--- a/Test/concurrency/12-MutexLifetime-short.dfy
+++ b/Test/concurrency/12-MutexLifetime-short.dfy
@@ -365,7 +365,7 @@ class Thread extends Object {
   }
   twostate lemma baseFieldsInvMonotonicity() requires old(baseFieldsInv()) && old(universe.content) <= universe.content && unchanged(this) ensures baseFieldsInv() {}
 
-  predicate localInv() reads * {
+  predicate localInv() reads * ensures localInv() ==> objectGlobalBaseInv() {
     && objectGlobalBaseInv()
   }
   predicate inv() reads * ensures inv() ==> localInv() {
@@ -439,7 +439,7 @@ trait OwnedObject extends Object {
     && unchangedNonvolatileUserFields()
   }
 
-  predicate localInv() reads * {
+  predicate localInv() reads * ensures localInv() ==> objectGlobalBaseInv() {
     && objectGlobalBaseInv()
     && this in lifetime.elements
     && (lifetime.alive() ==> owner != null)
diff --git a/Test/dafny4/git-issue245.dfy b/Test/dafny4/git-issue245.dfy
index 187cef8bc42..a5458a2cd7c 100644
--- a/Test/dafny4/git-issue245.dfy
+++ b/Test/dafny4/git-issue245.dfy
@@ -37,23 +37,23 @@ class C extends T {
   { 5 + y }
 }
 
-// class D is like C, but in each case, the spec is NOT weaker than that in T
+// class D is like C, but in each case, the spec is NOT stronger than that in T
 class D extends T {
   // d does not name the result in either trait or class
   function method d(y: nat): nat
-    ensures d(y) < 20 + y  // error: specification is not weaker
+    ensures d(y) < 20 + y  // error: specification is not stronger
   { 11 + y }
   // f names the result in both trait and class
   function method f(y: nat): (result: nat)
-    ensures result < 20 + y  // error: specification is not weaker
+    ensures result < 20 + y  // error: specification is not stronger
   { 11 + y }
   // g names the result in just the class
   function method g(y: nat): (result: nat)
-    ensures result < 20 + y  // error: specification is not weaker
+    ensures result < 20 + y  // error: specification is not stronger
   { 11 + y }
   // h names the result in just the trait
   function method h(y: nat): nat
-    ensures h(y) < 20 + y  // error: specification is not weaker
+    ensures h(y) < 20 + y  // error: specification is not stronger
   { 11 + y }
 }
 
@@ -62,19 +62,19 @@ class D extends T {
 class E extends T {
   // d does not name the result in either trait or class
   function method d(y: nat): nat
-    ensures d(y) < 20 + y
+    ensures d(y) < 20 + y  // error: specification is not stronger
   { 5 + y }
   // f names the result in both trait and class
   function method f(y: nat): (result: nat)
-    ensures result < 20 + y
+    ensures result < 20 + y  // error: specification is not stronger
   { 5 + y }
   // g names the result in just the class
   function method g(y: nat): (result: nat)
-    ensures result < 20 + y
+    ensures result < 20 + y  // error: specification is not stronger
   { 5 + y }
   // h names the result in just the trait
   function method h(y: nat): nat
-    ensures h(y) < 20 + y
+    ensures h(y) < 20 + y  // error: specification is not stronger
   { 5 + y }
 }
 
diff --git a/Test/dafny4/git-issue245.dfy.expect b/Test/dafny4/git-issue245.dfy.expect
index f154a354f05..52dc0dd66b2 100644
--- a/Test/dafny4/git-issue245.dfy.expect
+++ b/Test/dafny4/git-issue245.dfy.expect
@@ -2,6 +2,10 @@ git-issue245.dfy(43,18): Error: the function must provide an equal or more detai
 git-issue245.dfy(47,18): Error: the function must provide an equal or more detailed postcondition than in its parent trait
 git-issue245.dfy(51,18): Error: the function must provide an equal or more detailed postcondition than in its parent trait
 git-issue245.dfy(55,18): Error: the function must provide an equal or more detailed postcondition than in its parent trait
+git-issue245.dfy(64,18): Error: the function must provide an equal or more detailed postcondition than in its parent trait
+git-issue245.dfy(68,18): Error: the function must provide an equal or more detailed postcondition than in its parent trait
+git-issue245.dfy(72,18): Error: the function must provide an equal or more detailed postcondition than in its parent trait
+git-issue245.dfy(76,18): Error: the function must provide an equal or more detailed postcondition than in its parent trait
 git-issue245.dfy(84,18): Error: A postcondition might not hold on this return path.
 git-issue245.dfy(85,17): Related location: This is the postcondition that might not hold.
 git-issue245.dfy(88,18): Error: A postcondition might not hold on this return path.
@@ -11,4 +15,4 @@ git-issue245.dfy(93,19): Related location: This is the postcondition that might
 git-issue245.dfy(96,18): Error: A postcondition might not hold on this return path.
 git-issue245.dfy(97,17): Related location: This is the postcondition that might not hold.
 
-Dafny program verifier finished with 28 verified, 8 errors
+Dafny program verifier finished with 24 verified, 12 errors
diff --git a/Test/git-issues/git-issue-2500.dfy b/Test/git-issues/git-issue-2500.dfy
new file mode 100644
index 00000000000..6764811860f
--- /dev/null
+++ b/Test/git-issues/git-issue-2500.dfy
@@ -0,0 +1,81 @@
+// RUN: %exits-with 4 %dafny /compile:0 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+module M {
+  trait {:termination false} Top {
+    predicate ActuallyTrue() ensures ActuallyTrue()
+  }
+  trait {:termination false} Tr extends Top {
+    predicate True(): (ret: bool) ensures ret
+    predicate True'() ensures True'()
+    predicate ActuallyTrue'() ensures ActuallyTrue()
+    predicate ActuallyTrue''() ensures var alsoThis := this; alsoThis.ActuallyTrue()
+    predicate Other(x:nat, free: Tr)
+      ensures x != 0 && free.Other(x-1, free) ==> Other(x-1, free)
+  }
+  method X(tr: Tr) requires tr.ActuallyTrue() {}
+}
+
+class Cl extends M.Tr {
+  constructor() {}
+  predicate True(): (ret: bool)
+    // Missing: ensures ret
+  { false }
+  predicate True'()
+    // Missing: ensures True'()
+  { false }
+  predicate ActuallyTrue()
+    ensures ActuallyTrue()
+  { true }
+  predicate ActuallyTrue'()
+    ensures ActuallyTrue()
+  { true }
+  predicate ActuallyTrue''()
+     // This is logically correct, but the disguised receiver in the Tr spec prevents the override check from passing.
+     ensures ActuallyTrue''()
+   { true }
+  predicate Other(x: nat, free: M.Tr)
+    // Different receiver
+    ensures x != 0 && Other(x-1, free) ==> Other(x-1, free)
+  { false }
+}
+
+method Meh(tr: M.Tr)
+  requires tr.ActuallyTrue'()
+{
+  M.X(tr);
+}
+
+module SSCinClass {
+  trait Trait {
+    predicate Even(i: nat)
+    predicate Odd(i: nat)
+      ensures i == 0 || (i % 2 == 1) == Even(i-1)
+  }
+
+  class Class extends Trait {
+    predicate Even(i: nat)
+  { i == 0 || Odd(i-1) }
+    predicate Odd(i: nat)
+      ensures i == 0 || (i % 2 == 1) == Even(i-1)
+    { i != 0 && Even(i-1) }
+  }
+}
+
+module SSCinBoth {
+  trait Trait {
+    predicate Even(i: nat)
+      ensures i == 0 || (i % 2 == 0) == Odd(i-1)
+    predicate Odd(i: nat)
+      ensures i == 0 || (i % 2 == 1) == Even(i-1)
+  }
+
+  class Class extends Trait {
+    predicate Even(i: nat)
+      ensures i == 0 || (i % 2 == 0) == Odd(i-1)
+  { i == 0 || Odd(i-1) }
+    predicate Odd(i: nat)
+      ensures i == 0 || (i % 2 == 1) == Even(i-1)
+    { i != 0 && Even(i-1) }
+  }
+}
diff --git a/Test/git-issues/git-issue-2500.dfy.expect b/Test/git-issues/git-issue-2500.dfy.expect
new file mode 100644
index 00000000000..64fcebbc922
--- /dev/null
+++ b/Test/git-issues/git-issue-2500.dfy.expect
@@ -0,0 +1,6 @@
+git-issue-2500.dfy(21,12): Error: the function must provide an equal or more detailed postcondition than in its parent trait
+git-issue-2500.dfy(24,12): Error: the function must provide an equal or more detailed postcondition than in its parent trait
+git-issue-2500.dfy(33,12): Error: the function must provide an equal or more detailed postcondition than in its parent trait
+git-issue-2500.dfy(37,12): Error: the function must provide an equal or more detailed postcondition than in its parent trait
+
+Dafny program verifier finished with 26 verified, 4 errors
diff --git a/docs/dev/news/3479.fix b/docs/dev/news/3479.fix
new file mode 100644
index 00000000000..96e3176bae2
--- /dev/null
+++ b/docs/dev/news/3479.fix
@@ -0,0 +1 @@
+To ensure that a `class` correctly implements a `trait`, we perform an override check. This check was previously faulty across `module`s, but works unconditionally now.