From 040b54cc3b4bf18553b18495bed673032249bced Mon Sep 17 00:00:00 2001
From: Remy Willems <rwillems@amazon.com>
Date: Thu, 4 Jul 2024 11:19:28 +0200
Subject: [PATCH] Refactor codebase in preparation for hide PR (#5594)

Factors out the refactoring parts of
https://github.com/dafny-lang/dafny/pull/5562

### Description
- Extracted methods into separate files
- Extracted code into separate methods

### How has this been tested?
- Pure refactoring, no additional tests needed

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
---
 .../AST/Grammar/Printer/Printer.Statement.cs  |  34 +-
 .../AST/Statements/Verification/RevealStmt.cs |  47 ++
 .../PreType/PreTypeResolve.Expressions.cs     |   6 +-
 .../PreType/PreTypeResolve.Statements.cs      |  83 +---
 .../Resolver/PreType/PreTypeResolve.cs        |  18 +-
 .../Resolver/PreType/PreTypeResolver.Match.cs |   4 +-
 .../BoogieGenerator.ExpressionTranslator.cs   | 107 +----
 .../Verifier/BoogieGenerator.LetExpr.cs       | 107 +++++
 .../Verifier/BoogieGenerator.Methods.cs       | 418 +++++++++---------
 .../Verifier/BoogieGenerator.SplitExpr.cs     |  51 +--
 .../BoogieGenerator.TrPredicateStatement.cs   | 169 +++++++
 .../Verifier/BoogieGenerator.TrStatement.cs   | 155 -------
 Source/DafnyCore/Verifier/BoogieGenerator.cs  |  10 +-
 13 files changed, 622 insertions(+), 587 deletions(-)
 create mode 100644 Source/DafnyCore/Verifier/BoogieGenerator.TrPredicateStatement.cs

diff --git a/Source/DafnyCore/AST/Grammar/Printer/Printer.Statement.cs b/Source/DafnyCore/AST/Grammar/Printer/Printer.Statement.cs
index 5714378297..7188e4da1f 100644
--- a/Source/DafnyCore/AST/Grammar/Printer/Printer.Statement.cs
+++ b/Source/DafnyCore/AST/Grammar/Printer/Printer.Statement.cs
@@ -70,22 +70,8 @@ public void PrintStatement(Statement stmt, int indent) {
         PrintAttributeArgs(s.Args, true);
         wr.Write(";");
 
-      } else if (stmt is RevealStmt) {
-        var s = (RevealStmt)stmt;
-        wr.Write("reveal ");
-        var sep = "";
-        foreach (var e in s.Exprs) {
-          wr.Write(sep);
-          sep = ", ";
-          if (RevealStmt.SingleName(e) != null) {
-            // this will do the printing correctly for labels (or label-lookalikes) like 00_023 (which by PrintExpression below would be printed as 23)
-            wr.Write(RevealStmt.SingleName(e));
-          } else {
-            PrintExpression(e, true);
-          }
-        }
-        wr.Write(";");
-
+      } else if (stmt is RevealStmt revealStmt) {
+        PrintRevealStmt(revealStmt);
       } else if (stmt is BreakStmt) {
         var s = (BreakStmt)stmt;
         if (s.TargetLabel != null) {
@@ -471,6 +457,22 @@ public void PrintStatement(Statement stmt, int indent) {
       }
     }
 
+    private void PrintRevealStmt(RevealStmt revealStmt) {
+      wr.Write("reveal ");
+      var sep = "";
+      foreach (var e in revealStmt.Exprs) {
+        wr.Write(sep);
+        sep = ", ";
+        if (RevealStmt.SingleName(e) != null) {
+          // this will do the printing correctly for labels (or label-lookalikes) like 00_023 (which by PrintExpression below would be printed as 23)
+          wr.Write(RevealStmt.SingleName(e));
+        } else {
+          PrintExpression(e, true);
+        }
+      }
+      wr.Write(";");
+    }
+
     private void PrintModifyStmt(int indent, ModifyStmt s, bool omitFrame) {
       Contract.Requires(0 <= indent);
       Contract.Requires(s != null);
diff --git a/Source/DafnyCore/AST/Statements/Verification/RevealStmt.cs b/Source/DafnyCore/AST/Statements/Verification/RevealStmt.cs
index cf42991960..38852d2de1 100644
--- a/Source/DafnyCore/AST/Statements/Verification/RevealStmt.cs
+++ b/Source/DafnyCore/AST/Statements/Verification/RevealStmt.cs
@@ -53,4 +53,51 @@ public static string SingleName(Expression e) {
   public bool SetIndent(int indentBefore, TokenNewIndentCollector formatter) {
     return formatter.SetIndentPrintRevealStmt(indentBefore, OwnedTokens);
   }
+
+  public void ResolveRevealStmt(PreTypeResolver preTypeResolver, ResolutionContext resolutionContext) {
+    foreach (var expr in Exprs) {
+      var name = RevealStmt.SingleName(expr);
+      var labeledAssert = name == null ? null : preTypeResolver.DominatingStatementLabels.Find(name) as AssertLabel;
+      if (labeledAssert != null) {
+        LabeledAsserts.Add(labeledAssert);
+      } else {
+        var revealResolutionContext = resolutionContext with { InReveal = true };
+        if (expr is ApplySuffix applySuffix) {
+          var methodCallInfo = preTypeResolver.ResolveApplySuffix(applySuffix, revealResolutionContext, true);
+          if (methodCallInfo == null) {
+            // error has already been reported
+          } else if (methodCallInfo.Callee.Member is TwoStateLemma && !revealResolutionContext.IsTwoState) {
+            preTypeResolver.ReportError(methodCallInfo.Tok, "a two-state function can only be revealed in a two-state context");
+          } else if (methodCallInfo.Callee.AtLabel != null) {
+            Contract.Assert(methodCallInfo.Callee.Member is TwoStateLemma);
+            preTypeResolver.ReportError(methodCallInfo.Tok, "to reveal a two-state function, do not list any parameters or @-labels");
+          } else {
+            var call = new CallStmt(RangeToken, new List<Expression>(), methodCallInfo.Callee, methodCallInfo.ActualParameters);
+            ResolvedStatements.Add(call);
+          }
+        } else if (expr is NameSegment or ExprDotName) {
+          if (expr is NameSegment) {
+            preTypeResolver.ResolveNameSegment((NameSegment)expr, true, null, revealResolutionContext, true);
+          } else {
+            preTypeResolver.ResolveDotSuffix((ExprDotName)expr, true, null, revealResolutionContext, true);
+          }
+          var callee = (MemberSelectExpr)((ConcreteSyntaxExpression)expr).ResolvedExpression;
+          if (callee == null) {
+          } else if (callee.Member is Lemma or TwoStateLemma && Attributes.Contains(callee.Member.Attributes, "axiom")) {
+            //The revealed member is a function
+            preTypeResolver.ReportError(callee.tok, "to reveal a function ({0}), append parentheses", callee.Member.ToString().Substring(7));
+          } else {
+            var call = new CallStmt(RangeToken, new List<Expression>(), callee, new List<ActualBinding>(), expr.tok);
+            ResolvedStatements.Add(call);
+          }
+        } else {
+          preTypeResolver.ResolveExpression(expr, revealResolutionContext);
+        }
+      }
+    }
+
+    foreach (var a in ResolvedStatements) {
+      preTypeResolver.ResolveStatement(a, resolutionContext);
+    }
+  }
 }
\ No newline at end of file
diff --git a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs
index ad8ea839dc..98ec7e2665 100644
--- a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs
+++ b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs
@@ -1184,7 +1184,7 @@ private void ReportMemberNotFoundError(IToken tok, string memberName, [CanBeNull
     /// <param name="specialOpaqueHackAllowance">If "true", treats an expression "f" where "f" is an instance function, as "this.f", even though
     /// there is no "this" in scope. This seems like a terrible hack, because it breaks scope invariants about the AST. But, for now, it's here
     /// to mimic what the legacy resolver does.</param>
-    Expression ResolveNameSegment(NameSegment expr, bool isLastNameSegment, List<ActualBinding> args,
+    public Expression ResolveNameSegment(NameSegment expr, bool isLastNameSegment, List<ActualBinding> args,
       ResolutionContext resolutionContext, bool allowMethodCall, bool complain = true, bool specialOpaqueHackAllowance = false) {
       Contract.Requires(expr != null);
       Contract.Requires(!expr.WasResolved());
@@ -1439,7 +1439,7 @@ private bool ResolveDatatypeConstructor(NameSegment expr, List<ActualBinding>/*?
     /// <param name="resolutionContext"></param>
     /// <param name="allowMethodCall">If false, generates an error if the name denotes a method. If true and the name denotes a method, returns
     /// a Resolver_MethodCall.</param>
-    Expression ResolveDotSuffix(ExprDotName expr, bool isLastNameSegment, List<ActualBinding> args, ResolutionContext resolutionContext, bool allowMethodCall) {
+    public Expression ResolveDotSuffix(ExprDotName expr, bool isLastNameSegment, List<ActualBinding> args, ResolutionContext resolutionContext, bool allowMethodCall) {
       Contract.Requires(expr != null);
       Contract.Requires(!expr.WasResolved());
       Contract.Requires(resolutionContext != null);
@@ -1710,7 +1710,7 @@ public MethodCallInformation ResolveApplySuffix(ApplySuffix e, ResolutionContext
       }
       Label atLabel = null;
       if (e.AtTok != null) {
-        atLabel = dominatingStatementLabels.Find(e.AtTok.val);
+        atLabel = DominatingStatementLabels.Find(e.AtTok.val);
         if (atLabel == null) {
           ReportError(e.AtTok, "no label '{0}' in scope at this time", e.AtTok.val);
         }
diff --git a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Statements.cs b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Statements.cs
index f9dac43cbf..b3e4551a0e 100644
--- a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Statements.cs
+++ b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Statements.cs
@@ -13,14 +13,9 @@
 
 namespace Microsoft.Dafny {
   public partial class PreTypeResolver : INewOrOldResolver {
-    private Scope<Statement> enclosingStatementLabels;
-    private readonly Scope<Label> dominatingStatementLabels;
-    public Scope<Label> DominatingStatementLabels => dominatingStatementLabels;
+    public Scope<Label> DominatingStatementLabels { get; }
 
-    public Scope<Statement> EnclosingStatementLabels {
-      get => enclosingStatementLabels;
-      set => enclosingStatementLabels = value;
-    }
+    public Scope<Statement> EnclosingStatementLabels { get; set; }
 
     public List<Statement> LoopStack {
       get => loopStack;
@@ -70,10 +65,10 @@ void ResolveStatementWithLabels(Statement stmt, ResolutionContext resolutionCont
         } else {
           var r = EnclosingStatementLabels.Push(lnode.Name, stmt);
           Contract.Assert(r == Scope<Statement>.PushResult.Success);  // since we just checked for duplicates, we expect the Push to succeed
-          if (dominatingStatementLabels.Find(lnode.Name) != null) {
+          if (DominatingStatementLabels.Find(lnode.Name) != null) {
             ReportError(lnode.Tok, "label shadows a dominating label");
           } else {
-            var rr = dominatingStatementLabels.Push(lnode.Name, lnode);
+            var rr = DominatingStatementLabels.Push(lnode.Name, lnode);
             Contract.Assert(rr == Scope<Label>.PushResult.Success);  // since we just checked for duplicates, we expect the Push to succeed
           }
         }
@@ -91,7 +86,7 @@ void ResolveStatementWithLabels(Statement stmt, ResolutionContext resolutionCont
       if (!resolutionContext.IsTwoState) {
         ReportError(tok, $"{expressionDescription} expressions are not allowed in this context");
       } else if (labelName != null) {
-        label = dominatingStatementLabels.Find(labelName);
+        label = DominatingStatementLabels.Find(labelName);
         if (label == null) {
           ReportError(tok, $"no label '{labelName}' in scope at this time");
         }
@@ -117,52 +112,8 @@ public void ResolveStatement(Statement stmt, ResolutionContext resolutionContext
           ResolveExpression(e, resolutionContext);
         }
 
-      } else if (stmt is RevealStmt) {
-        var s = (RevealStmt)stmt;
-        foreach (var expr in s.Exprs) {
-          var name = RevealStmt.SingleName(expr);
-          var labeledAssert = name == null ? null : dominatingStatementLabels.Find(name) as AssertLabel;
-          if (labeledAssert != null) {
-            s.LabeledAsserts.Add(labeledAssert);
-          } else {
-            var revealResolutionContext = resolutionContext with { InReveal = true };
-            if (expr is ApplySuffix applySuffix) {
-              var methodCallInfo = ResolveApplySuffix(applySuffix, revealResolutionContext, true);
-              if (methodCallInfo == null) {
-                // error has already been reported
-              } else if (methodCallInfo.Callee.Member is TwoStateLemma && !revealResolutionContext.IsTwoState) {
-                ReportError(methodCallInfo.Tok, "a two-state function can only be revealed in a two-state context");
-              } else if (methodCallInfo.Callee.AtLabel != null) {
-                Contract.Assert(methodCallInfo.Callee.Member is TwoStateLemma);
-                ReportError(methodCallInfo.Tok, "to reveal a two-state function, do not list any parameters or @-labels");
-              } else {
-                var call = new CallStmt(s.RangeToken, new List<Expression>(), methodCallInfo.Callee, methodCallInfo.ActualParameters);
-                s.ResolvedStatements.Add(call);
-              }
-            } else if (expr is NameSegment or ExprDotName) {
-              if (expr is NameSegment) {
-                ResolveNameSegment((NameSegment)expr, true, null, revealResolutionContext, true);
-              } else {
-                ResolveDotSuffix((ExprDotName)expr, true, null, revealResolutionContext, true);
-              }
-              var callee = (MemberSelectExpr)((ConcreteSyntaxExpression)expr).ResolvedExpression;
-              if (callee == null) {
-              } else if (callee.Member is Lemma or TwoStateLemma && Attributes.Contains(callee.Member.Attributes, "axiom")) {
-                //The revealed member is a function
-                ReportError(callee.tok, "to reveal a function ({0}), append parentheses", callee.Member.ToString().Substring(7));
-              } else {
-                var call = new CallStmt(s.RangeToken, new List<Expression>(), callee, new List<ActualBinding>(), expr.tok);
-                s.ResolvedStatements.Add(call);
-              }
-            } else {
-              ResolveExpression(expr, revealResolutionContext);
-            }
-          }
-        }
-        foreach (var a in s.ResolvedStatements) {
-          ResolveStatement(a, resolutionContext);
-        }
-
+      } else if (stmt is RevealStmt revealStmt) {
+        revealStmt.ResolveRevealStmt(this, resolutionContext);
       } else if (stmt is BreakStmt) {
         var s = (BreakStmt)stmt;
         if (s.TargetLabel != null) {
@@ -329,15 +280,15 @@ public void ResolveStatement(Statement stmt, ResolutionContext resolutionContext
             ScopePushAndReport(v, "bound-variable", false);
           }
         }
-        dominatingStatementLabels.PushMarker();
+        DominatingStatementLabels.PushMarker();
         ResolveBlockStatement(s.Thn, resolutionContext);
-        dominatingStatementLabels.PopMarker();
+        DominatingStatementLabels.PopMarker();
         scope.PopMarker();
 
         if (s.Els != null) {
-          dominatingStatementLabels.PushMarker();
+          DominatingStatementLabels.PushMarker();
           ResolveStatement(s.Els, resolutionContext);
-          dominatingStatementLabels.PopMarker();
+          DominatingStatementLabels.PopMarker();
         }
 
       } else if (stmt is AlternativeStmt) {
@@ -511,9 +462,9 @@ private void ResolveOneBodyLoopStmt(OneBodyLoopStmt s, ResolutionContext resolut
 
       if (s.Body != null) {
         loopStack.Add(s); // push
-        dominatingStatementLabels.PushMarker();
+        DominatingStatementLabels.PushMarker();
         ResolveStatement(s.Body, resolutionContext);
-        dominatingStatementLabels.PopMarker();
+        DominatingStatementLabels.PopMarker();
         loopStack.RemoveAt(loopStack.Count - 1); // pop
       }
 
@@ -560,9 +511,9 @@ private void ResolveCalc(CalcStmt s, ResolutionContext resolutionContext) {
         loopStack = new List<Statement>();
         foreach (var h in s.Hints) {
           foreach (var oneHint in h.Body) {
-            dominatingStatementLabels.PushMarker();
+            DominatingStatementLabels.PushMarker();
             ResolveStatement(oneHint, resolutionContext);
-            dominatingStatementLabels.PopMarker();
+            DominatingStatementLabels.PopMarker();
           }
         }
         EnclosingStatementLabels = prevLblStmts;
@@ -1334,7 +1285,7 @@ void ResolveAlternatives(List<GuardedAlternative> alternatives, AlternativeLoopS
       }
       foreach (var alternative in alternatives) {
         scope.PushMarker();
-        dominatingStatementLabels.PushMarker();
+        DominatingStatementLabels.PushMarker();
         if (alternative.IsBindingGuard) {
           var exists = (ExistsExpr)alternative.Guard;
           foreach (var v in exists.BoundVars) {
@@ -1345,7 +1296,7 @@ void ResolveAlternatives(List<GuardedAlternative> alternatives, AlternativeLoopS
         foreach (Statement ss in alternative.Body) {
           ResolveStatementWithLabels(ss, resolutionContext);
         }
-        dominatingStatementLabels.PopMarker();
+        DominatingStatementLabels.PopMarker();
         scope.PopMarker();
       }
       if (loopToCatchBreaks != null) {
diff --git a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.cs b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.cs
index 41b041930f..c160ef4dcd 100644
--- a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.cs
+++ b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.cs
@@ -427,7 +427,7 @@ private PreTypeResolver(ModuleResolver resolver, PreTypeInferenceModuleState pre
 
       scope = new Scope<IVariable>(resolver.Options);
       EnclosingStatementLabels = new Scope<Statement>(resolver.Options);
-      dominatingStatementLabels = new Scope<Label>(resolver.Options);
+      DominatingStatementLabels = new Scope<Label>(resolver.Options);
       Constraints = new PreTypeConstraints(this);
     }
 
@@ -1216,19 +1216,19 @@ void ResolveIterator(IteratorDecl iter) {
 
       // Resolve body
       if (iter.Body != null) {
-        dominatingStatementLabels.PushMarker();
+        DominatingStatementLabels.PushMarker();
         foreach (var req in iter.Requires) {
           if (req.Label != null) {
-            if (dominatingStatementLabels.Find(req.Label.Name) != null) {
+            if (DominatingStatementLabels.Find(req.Label.Name) != null) {
               ReportError(req.Label.Tok, "assert label shadows a dominating label");
             } else {
-              var rr = dominatingStatementLabels.Push(req.Label.Name, req.Label);
+              var rr = DominatingStatementLabels.Push(req.Label.Name, req.Label);
               Contract.Assert(rr == Scope<Label>.PushResult.Success);  // since we just checked for duplicates, we expect the Push to succeed
             }
           }
         }
         ResolveBlockStatement(iter.Body, ResolutionContext.FromCodeContext(iter));
-        dominatingStatementLabels.PopMarker();
+        DominatingStatementLabels.PopMarker();
         Constraints.SolveAllTypeConstraints($"body of iterator '{iter.Name}'");
       }
 
@@ -1413,19 +1413,19 @@ void ResolveMethod(Method m) {
             ScopePushExpectSuccess(k, "_k parameter", false);
           }
 
-          dominatingStatementLabels.PushMarker();
+          DominatingStatementLabels.PushMarker();
           foreach (var req in m.Req) {
             if (req.Label != null) {
-              if (dominatingStatementLabels.Find(req.Label.Name) != null) {
+              if (DominatingStatementLabels.Find(req.Label.Name) != null) {
                 ReportError(req.Label.Tok, "assert label shadows a dominating label");
               } else {
-                var rr = dominatingStatementLabels.Push(req.Label.Name, req.Label);
+                var rr = DominatingStatementLabels.Push(req.Label.Name, req.Label);
                 Contract.Assert(rr == Scope<Label>.PushResult.Success);  // since we just checked for duplicates, we expect the Push to succeed
               }
             }
           }
           ResolveBlockStatement(m.Body, ResolutionContext.FromCodeContext(m));
-          dominatingStatementLabels.PopMarker();
+          DominatingStatementLabels.PopMarker();
           Constraints.SolveAllTypeConstraints($"body of {m.WhatKind} '{m.Name}'");
         }
 
diff --git a/Source/DafnyCore/Resolver/PreType/PreTypeResolver.Match.cs b/Source/DafnyCore/Resolver/PreType/PreTypeResolver.Match.cs
index b6d1c5beff..cef280731a 100644
--- a/Source/DafnyCore/Resolver/PreType/PreTypeResolver.Match.cs
+++ b/Source/DafnyCore/Resolver/PreType/PreTypeResolver.Match.cs
@@ -23,9 +23,9 @@ void ResolveNestedMatchStmt(NestedMatchStmt stmt, ResolutionContext resolutionCo
         scope.PushMarker();
         ResolveExtendedPattern(stmt.Source.tok, mc.Pat, stmt.Source.PreType, false, resolutionContext);
 
-        dominatingStatementLabels.PushMarker();
+        DominatingStatementLabels.PushMarker();
         mc.Body.ForEach(ss => ResolveStatementWithLabels(ss, resolutionContext));
-        dominatingStatementLabels.PopMarker();
+        DominatingStatementLabels.PopMarker();
 
         scope.PopMarker();
       }
diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs b/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs
index ea44fc07b4..d8bfd2eef8 100644
--- a/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs
+++ b/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs
@@ -10,7 +10,7 @@
 
 namespace Microsoft.Dafny {
   public partial class BoogieGenerator {
-    public class ExpressionTranslator {
+    public partial class ExpressionTranslator {
       private DafnyOptions options;
 
       // HeapExpr == null ==> translation of pure (no-heap) expression
@@ -1292,31 +1292,8 @@ public Boogie.Expr TrExpr(Expression expr) {
                   Contract.Assert(false); throw new cce.UnreachableException();  // unexpected ternary expression
               }
             }
-          case LetExpr letExpr: {
-              var e = letExpr;
-              if (!e.Exact) {
-                var d = BoogieGenerator.LetDesugaring(e);
-                return TrExpr(d);
-              } else {
-                TrLetExprPieces(e, out var lhss, out var rhss);
-                // in the translation of body, treat a let-bound variable as IsLit if its RHS definition is IsLit
-                Contract.Assert(lhss.Count == rhss.Count);  // this is a postcondition of TrLetExprPieces
-                var previousCount = BoogieGenerator.letBoundVariablesWithLitRHS.Count;
-                for (var i = 0; i < lhss.Count; i++) {
-                  if (BoogieGenerator.IsLit(rhss[i])) {
-                    BoogieGenerator.letBoundVariablesWithLitRHS.Add(lhss[i].Name);
-                  }
-                  i++;
-                }
-                var body = TrExpr(e.Body);
-                foreach (var v in lhss) {
-                  BoogieGenerator.letBoundVariablesWithLitRHS.Remove(v.Name);
-                }
-                Contract.Assert(previousCount == BoogieGenerator.letBoundVariablesWithLitRHS.Count);
-                // in the following, use the token for Body instead of the token for the whole let expression; this gives better error locations
-                return new Boogie.LetExpr(GetToken(e.Body), lhss, rhss, null, body);
-              }
-            }
+          case LetExpr letExpr:
+            return TrLetExpr(letExpr);
           case QuantifierExpr quantifierExpr: {
               QuantifierExpr e = quantifierExpr;
 
@@ -1610,25 +1587,6 @@ private Expr TrLambdaExpr(LambdaExpr e) {
           predef.HandleType);
       }
 
-      public void TrLetExprPieces(LetExpr let, out List<Boogie.Variable> lhss, out List<Boogie.Expr> rhss) {
-        Contract.Requires(let != null);
-        var substMap = new Dictionary<IVariable, Expression>();
-        for (int i = 0; i < let.LHSs.Count; i++) {
-          var rhs = TrExpr(let.RHSs[i]);
-          var toType = let.LHSs[i].Var?.Type ?? let.LHSs[i].Expr.Type;
-          rhs = BoogieGenerator.CondApplyBox(rhs.tok, rhs, let.RHSs[i].Type, toType);
-          BoogieGenerator.AddCasePatternVarSubstitutions(let.LHSs[i], rhs, substMap);
-        }
-        lhss = new List<Boogie.Variable>();
-        rhss = new List<Boogie.Expr>();
-        foreach (var v in let.BoundVars) {
-          var rhs = substMap[v];  // this should succeed (that is, "v" is in "substMap"), because the AddCasePatternVarSubstitutions calls above should have added a mapping for each bound variable in let.BoundVars
-          var bv = BplBoundVar(v.AssignUniqueName(BoogieGenerator.currentDeclaration.IdGenerator), BoogieGenerator.TrType(v.Type), out var bvIde);
-          lhss.Add(bv);
-          rhss.Add(TrExpr(rhs));
-        }
-      }
-
       public Expression DesugarMatchExpr(MatchExpr e) {
         Contract.Requires(e != null);
         // Translate:
@@ -2285,63 +2243,8 @@ public Expr CanCallAssumption(Expression expr) {
           var e = (TernaryExpr)expr;
           return BplAnd(CanCallAssumption(e.E0), BplAnd(CanCallAssumption(e.E1), CanCallAssumption(e.E2)));
 
-        } else if (expr is LetExpr) {
-          var e = (LetExpr)expr;
-          if (!e.Exact) {
-            // CanCall[[ var b0,b1 :| RHS(b0,b1,g); Body(b0,b1,g,h) ]] =
-            //   $let$canCall(g) &&
-            //   CanCall[[ Body($let$b0(g), $let$b1(g), h) ]]
-            BoogieGenerator.LetDesugaring(e);  // call LetDesugaring to prepare the desugaring and populate letSuchThatExprInfo with something for e
-            var info = BoogieGenerator.letSuchThatExprInfo[e];
-            // $let$canCall(g)
-            var canCall = info.CanCallFunctionCall(BoogieGenerator, this);
-            Dictionary<IVariable, Expression> substMap = new Dictionary<IVariable, Expression>();
-            foreach (var bv in e.BoundVars) {
-              // create a call to $let$x(g)
-              var args = info.SkolemFunctionArgs(bv, BoogieGenerator, this);
-              var call = new BoogieFunctionCall(bv.tok, info.SkolemFunctionName(bv), info.UsesHeap, info.UsesOldHeap, info.UsesHeapAt, args.Item1, args.Item2);
-              call.Type = bv.Type;
-              substMap.Add(bv, call);
-            }
-            var p = Substitute(e.Body, null, substMap);
-            var cc = BplAnd(canCall, CanCallAssumption(p));
-            return cc;
-          } else {
-            // CanCall[[ var b := RHS(g); Body(b,g,h) ]] =
-            //   CanCall[[ RHS(g) ]] &&
-            //   (var lhs0,lhs1,... := rhs0,rhs1,...;  CanCall[[ Body ]])
-            Boogie.Expr canCallRHS = Boogie.Expr.True;
-            foreach (var rhs in e.RHSs) {
-              canCallRHS = BplAnd(canCallRHS, CanCallAssumption(rhs));
-            }
-
-            var bodyCanCall = CanCallAssumption(e.Body);
-            // We'd like to compute the free variables if "bodyCanCall". It would be nice to use the Boogie
-            // routine Bpl.Expr.ComputeFreeVariables for this purpose. However, calling it requires the Boogie
-            // expression to be resolved. Instead, we do the cheesy thing of computing the set of names of
-            // free variables in "bodyCanCall".
-            var vis = new VariableNameVisitor();
-            vis.Visit(bodyCanCall);
-
-            List<Boogie.Variable> lhssAll;
-            List<Boogie.Expr> rhssAll;
-            TrLetExprPieces(e, out lhssAll, out rhssAll);
-            Contract.Assert(lhssAll.Count == rhssAll.Count);
-
-            // prune lhss,rhss to contain only those pairs where the LHS is used in the body
-            var lhssPruned = new List<Boogie.Variable>();
-            var rhssPruned = new List<Boogie.Expr>();
-            for (var i = 0; i < lhssAll.Count; i++) {
-              var bv = lhssAll[i];
-              if (vis.Names.Contains(bv.Name)) {
-                lhssPruned.Add(bv);
-                rhssPruned.Add(rhssAll[i]);
-              }
-            }
-            Boogie.Expr let = lhssPruned.Count == 0 ? bodyCanCall : new Boogie.LetExpr(e.tok, lhssPruned, rhssPruned, null, bodyCanCall);
-            return BplAnd(canCallRHS, let);
-          }
-
+        } else if (expr is LetExpr letExpr) {
+          return LetCanCallAssumption(letExpr);
         } else if (expr is LambdaExpr) {
           var e = (LambdaExpr)expr;
 
diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.LetExpr.cs b/Source/DafnyCore/Verifier/BoogieGenerator.LetExpr.cs
index 9bcfa1a391..5cad787b4c 100644
--- a/Source/DafnyCore/Verifier/BoogieGenerator.LetExpr.cs
+++ b/Source/DafnyCore/Verifier/BoogieGenerator.LetExpr.cs
@@ -32,6 +32,113 @@
 namespace Microsoft.Dafny {
   public partial class BoogieGenerator {
 
+    partial class ExpressionTranslator {
+
+
+      private Expr LetCanCallAssumption(LetExpr letExpr) {
+        if (!letExpr.Exact) {
+          // CanCall[[ var b0,b1 :| RHS(b0,b1,g); Body(b0,b1,g,h) ]] =
+          //   $let$canCall(g) &&
+          //   CanCall[[ Body($let$b0(g), $let$b1(g), h) ]]
+          BoogieGenerator.LetDesugaring(letExpr);  // call LetDesugaring to prepare the desugaring and populate letSuchThatExprInfo with something for e
+          var info = BoogieGenerator.letSuchThatExprInfo[letExpr];
+          // $let$canCall(g)
+          var canCall = info.CanCallFunctionCall(BoogieGenerator, this);
+          Dictionary<IVariable, Expression> substMap = new Dictionary<IVariable, Expression>();
+          foreach (var bv in letExpr.BoundVars) {
+            // create a call to $let$x(g)
+            var args = info.SkolemFunctionArgs(bv, BoogieGenerator, this);
+            var call = new BoogieFunctionCall(bv.tok, info.SkolemFunctionName(bv), info.UsesHeap, info.UsesOldHeap, info.UsesHeapAt, args.Item1, args.Item2);
+            call.Type = bv.Type;
+            substMap.Add(bv, call);
+          }
+          var p = Substitute(letExpr.Body, null, substMap);
+          var cc = BplAnd(canCall, CanCallAssumption(p));
+          return cc;
+        } else {
+          // CanCall[[ var b := RHS(g); Body(b,g,h) ]] =
+          //   CanCall[[ RHS(g) ]] &&
+          //   (var lhs0,lhs1,... := rhs0,rhs1,...;  CanCall[[ Body ]])
+          Boogie.Expr canCallRHS = Boogie.Expr.True;
+          foreach (var rhs in letExpr.RHSs) {
+            canCallRHS = BplAnd(canCallRHS, CanCallAssumption(rhs));
+          }
+
+          var bodyCanCall = CanCallAssumption(letExpr.Body);
+          // We'd like to compute the free variables if "bodyCanCall". It would be nice to use the Boogie
+          // routine Bpl.Expr.ComputeFreeVariables for this purpose. However, calling it requires the Boogie
+          // expression to be resolved. Instead, we do the cheesy thing of computing the set of names of
+          // free variables in "bodyCanCall".
+          var vis = new VariableNameVisitor();
+          vis.Visit(bodyCanCall);
+
+          List<Boogie.Variable> lhssAll;
+          List<Boogie.Expr> rhssAll;
+          TrLetExprPieces(letExpr, out lhssAll, out rhssAll);
+          Contract.Assert(lhssAll.Count == rhssAll.Count);
+
+          // prune lhss,rhss to contain only those pairs where the LHS is used in the body
+          var lhssPruned = new List<Boogie.Variable>();
+          var rhssPruned = new List<Boogie.Expr>();
+          for (var i = 0; i < lhssAll.Count; i++) {
+            var bv = lhssAll[i];
+            if (vis.Names.Contains(bv.Name)) {
+              lhssPruned.Add(bv);
+              rhssPruned.Add(rhssAll[i]);
+            }
+          }
+          Boogie.Expr let = lhssPruned.Count == 0 ? bodyCanCall : new Boogie.LetExpr(letExpr.tok, lhssPruned, rhssPruned, null, bodyCanCall);
+          return BplAnd(canCallRHS, let);
+        }
+      }
+
+      private Expr TrLetExpr(LetExpr letExpr) {
+        var e = letExpr;
+        if (!e.Exact) {
+          var d = BoogieGenerator.LetDesugaring(e);
+          return TrExpr(d);
+        } else {
+          TrLetExprPieces(e, out var lhss, out var rhss);
+          // in the translation of body, treat a let-bound variable as IsLit if its RHS definition is IsLit
+          Contract.Assert(lhss.Count == rhss.Count);  // this is a postcondition of TrLetExprPieces
+          var previousCount = BoogieGenerator.letBoundVariablesWithLitRHS.Count;
+          for (var i = 0; i < lhss.Count; i++) {
+            if (BoogieGenerator.IsLit(rhss[i])) {
+              BoogieGenerator.letBoundVariablesWithLitRHS.Add(lhss[i].Name);
+            }
+            i++;
+          }
+          var body = TrExpr(e.Body);
+          foreach (var v in lhss) {
+            BoogieGenerator.letBoundVariablesWithLitRHS.Remove(v.Name);
+          }
+          Contract.Assert(previousCount == BoogieGenerator.letBoundVariablesWithLitRHS.Count);
+          // in the following, use the token for Body instead of the token for the whole let expression; this gives better error locations
+          return new Boogie.LetExpr(GetToken(e.Body), lhss, rhss, null, body);
+        }
+      }
+
+
+      public void TrLetExprPieces(LetExpr let, out List<Boogie.Variable> lhss, out List<Boogie.Expr> rhss) {
+        Contract.Requires(let != null);
+        var substMap = new Dictionary<IVariable, Expression>();
+        for (int i = 0; i < let.LHSs.Count; i++) {
+          var rhs = TrExpr(let.RHSs[i]);
+          var toType = let.LHSs[i].Var?.Type ?? let.LHSs[i].Expr.Type;
+          rhs = BoogieGenerator.CondApplyBox(rhs.tok, rhs, let.RHSs[i].Type, toType);
+          BoogieGenerator.AddCasePatternVarSubstitutions(let.LHSs[i], rhs, substMap);
+        }
+        lhss = new List<Boogie.Variable>();
+        rhss = new List<Boogie.Expr>();
+        foreach (var v in let.BoundVars) {
+          var rhs = substMap[v];  // this should succeed (that is, "v" is in "substMap"), because the AddCasePatternVarSubstitutions calls above should have added a mapping for each bound variable in let.BoundVars
+          var bv = BplBoundVar(v.AssignUniqueName(BoogieGenerator.currentDeclaration.IdGenerator), BoogieGenerator.TrType(v.Type), out var bvIde);
+          lhss.Add(bv);
+          rhss.Add(TrExpr(rhs));
+        }
+      }
+    }
+
     /// <summary>
     /// Fills in, if necessary, the e.translationDesugaring field, and returns it.
     /// Also, makes sure that letSuchThatExprInfo maps e to something.
diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs
index 864ee698b1..8fb5d82c79 100644
--- a/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs
+++ b/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs
@@ -565,233 +565,243 @@ private void AddMethodImpl(Method m, Boogie.Procedure proc, bool wellformednessP
         }
       }
 
-      Boogie.StmtList stmts;
-      if (!wellformednessProc) {
-        var inductionVars = ApplyInduction(m.Ins, m.Attributes);
-        if (inductionVars.Count != 0) {
-          // Let the parameters be this,x,y of the method M and suppose ApplyInduction returns this,y.
-          // Also, let Pre be the precondition and VF be the decreases clause.
-          // Then, insert into the method body what amounts to:
-          //     assume case-analysis-on-parameter[[ y' ]];
-          //     forall this',y' | Pre(this', x, y') && (VF(this', x, y') << VF(this', x, y)) {
-          //       this'.M(x, y');
-          //     }
-          // Generate bound variables for the forall statement, and a substitution for the Pre and VF
-
-          // assume case-analysis-on-parameter[[ y' ]];
-          foreach (var inFormal in m.Ins) {
-            var dt = inFormal.Type.AsDatatype;
-            if (dt != null) {
-              var funcID = new Boogie.FunctionCall(new Boogie.IdentifierExpr(inFormal.tok, "$IsA#" + dt.FullSanitizedName, Boogie.Type.Bool));
-              var f = new Boogie.IdentifierExpr(inFormal.tok, inFormal.AssignUniqueName(m.IdGenerator), TrType(inFormal.Type));
-              builder.Add(TrAssumeCmd(inFormal.tok, new Boogie.NAryExpr(inFormal.tok, funcID, new List<Boogie.Expr> { f })));
-            }
-          }
+      var stmts = wellformednessProc
+        ? TrMethodContractWellformedness(m, etran, localVariables, builderInitializationArea, builder, outParams)
+        : TrMethodBody(m, builder, localVariables, etran);
 
-          var parBoundVars = new List<BoundVar>();
-          var parBounds = new List<BoundedPool>();
-          var substMap = new Dictionary<IVariable, Expression>();
-          Expression receiverSubst = null;
-          foreach (var iv in inductionVars) {
-            BoundVar bv;
-            if (iv == null) {
-              // this corresponds to "this"
-              Contract.Assert(!m.IsStatic);  // if "m" is static, "this" should never have gone into the _induction attribute
-              Contract.Assert(receiverSubst == null);  // we expect at most one
-              var receiverType = ModuleResolver.GetThisType(m.tok, (TopLevelDeclWithMembers)m.EnclosingClass);
-              bv = new BoundVar(m.tok, CurrentIdGenerator.FreshId("$ih#this"), receiverType); // use this temporary variable counter, but for a Dafny name (the idea being that the number and the initial "_" in the name might avoid name conflicts)
-              var ie = new IdentifierExpr(m.tok, bv.Name) {
-                Var = bv,
-                Type = bv.Type
-              };
-              receiverSubst = ie;
-            } else {
-              CloneVariableAsBoundVar(iv.tok, iv, "$ih#" + iv.Name, out bv, out var ie);
-              substMap.Add(iv, ie);
-            }
-            parBoundVars.Add(bv);
-            parBounds.Add(new SpecialAllocIndependenceAllocatedBoundedPool());  // record that we don't want alloc antecedents for these variables
-          }
-
-          // Generate a CallStmt to be used as the body of the 'forall' statement.
-          m.RecursiveCallParameters(m.tok, m.TypeArgs, m.Ins, receiverSubst, substMap, out var recursiveCallReceiver, out var recursiveCallArgs);
-          var methodSel = new MemberSelectExpr(m.tok, recursiveCallReceiver, m.Name) {
-            Member = m,
-            TypeApplication_AtEnclosingClass = m.EnclosingClass.TypeArgs.ConvertAll(tp => (Type)new UserDefinedType(tp.tok, tp)),
-            TypeApplication_JustMember = m.TypeArgs.ConvertAll(tp => (Type)new UserDefinedType(tp.tok, tp)),
-            Type = new InferredTypeProxy()
-          };
-          var recursiveCall = new CallStmt(m.tok.ToRange(), new List<Expression>(), methodSel, recursiveCallArgs) {
-            IsGhost = m.IsGhost
-          };
-
-          Expression parRange = Expression.CreateBoolLiteral(m.tok, true);
-          foreach (var pre in m.Req) {
-            parRange = Expression.CreateAnd(parRange, Substitute(pre.E, receiverSubst, substMap));
-          }
-          // construct an expression (generator) for:  VF' << VF
-          ExpressionConverter decrCheck = delegate (Dictionary<IVariable, Expression> decrSubstMap, ExpressionTranslator exprTran) {
-            var decrToks = new List<IToken>();
-            var decrTypes = new List<Type>();
-            var decrCallee = new List<Expr>();
-            var decrCaller = new List<Expr>();
-            var decrCalleeDafny = new List<Expression>();
-            var decrCallerDafny = new List<Expression>();
-            foreach (var ee in m.Decreases.Expressions) {
-              decrToks.Add(ee.tok);
-              decrTypes.Add(ee.Type.NormalizeExpand());
-              decrCallerDafny.Add(ee);
-              decrCaller.Add(exprTran.TrExpr(ee));
-              Expression es = Substitute(ee, receiverSubst, substMap);
-              es = Substitute(es, null, decrSubstMap);
-              decrCalleeDafny.Add(es);
-              decrCallee.Add(exprTran.TrExpr(es));
-            }
-            return DecreasesCheck(decrToks, null, decrCalleeDafny, decrCallerDafny, decrCallee, decrCaller,
-              null, null, false, true);
-          };
+      if (EmitImplementation(m.Attributes)) {
+        // emit impl only when there are proof obligations.
+        var kv = etran.TrAttributes(m.Attributes, null);
+        Bpl.Implementation impl = AddImplementationWithAttributes(GetToken(m), proc,
+           inParams, outParams, localVariables, stmts, kv);
 
-#if VERIFY_CORRECTNESS_OF_TRANSLATION_FORALL_STATEMENT_RANGE
-          var definedness = new BoogieStmtListBuilder(this, options);
-          var exporter = new BoogieStmtListBuilder(this, options);
-          TrForallStmtCall(m.tok, parBoundVars, parRange, decrCheck, null, recursiveCall, definedness, exporter, localVariables, etran);
-          // All done, so put the two pieces together
-          builder.Add(new Bpl.IfCmd(m.tok, null, definedness.Collect(m.tok), null, exporter.Collect(m.tok)));
-#else
-          TrForallStmtCall(m.tok, parBoundVars, parBounds, parRange, decrCheck, null, recursiveCall, null, builder, localVariables, etran);
-#endif
-        }
-        // translate the body of the method
-        Contract.Assert(m.Body != null);  // follows from method precondition and the if guard
-
-        // $_reverifyPost := false;
-        builder.Add(Boogie.Cmd.SimpleAssign(m.tok, new Boogie.IdentifierExpr(m.tok, "$_reverifyPost", Boogie.Type.Bool), Boogie.Expr.False));
-        // register output parameters with definite-assignment trackers
-        Contract.Assert(definiteAssignmentTrackers.Count == 0);
-        m.Outs.ForEach(p => AddExistingDefiniteAssignmentTracker(p, m.IsGhost));
-        // translate the body
-        TrStmt(m.Body, builder, localVariables, etran);
-        m.Outs.ForEach(p => CheckDefiniteAssignmentReturn(m.Body.RangeToken.EndToken, p, builder));
-        if (m is { FunctionFromWhichThisIsByMethodDecl: { ByMethodTok: { } } fun }) {
-          AssumeCanCallForByMethodDecl(m, builder);
+        if (InsertChecksums) {
+          InsertChecksum(m, impl);
         }
-        stmts = builder.Collect(m.Body.RangeToken.StartToken); // TODO should this be EndToken?  the parameter name suggests it should be the closing curly
-        // tear down definite-assignment trackers
-        m.Outs.ForEach(RemoveDefiniteAssignmentTracker);
+      }
 
-        Contract.Assert(definiteAssignmentTrackers.Count == 0);
-      } else {
-        var readsCheckDelayer = new ReadsCheckDelayer(etran, null, localVariables, builderInitializationArea, builder);
-
-        // check well-formedness of any default-value expressions (before assuming preconditions)
-        readsCheckDelayer.DoWithDelayedReadsChecks(true, wfo => {
-          foreach (var formal in m.Ins.Where(formal => formal.DefaultValue != null)) {
-            var e = formal.DefaultValue;
-            CheckWellformed(e, wfo, localVariables, builder, etran.WithReadsFrame(etran.readsFrame, null)); // No scope for default parameters
-            builder.Add(new Boogie.AssumeCmd(e.tok, etran.CanCallAssumption(e)));
-            CheckSubrange(e.tok, etran.TrExpr(e), e.Type, formal.Type, e, builder);
-
-            if (formal.IsOld) {
-              Boogie.Expr wh = GetWhereClause(e.tok, etran.TrExpr(e), e.Type, etran.Old, ISALLOC, true);
-              if (wh != null) {
-                var desc = new PODesc.IsAllocated("default value", "in the two-state lemma's previous state", e);
-                builder.Add(Assert(e.RangeToken, wh, desc));
-              }
-            }
-          }
-        });
+      isAllocContext = null;
+      Reset();
+    }
 
-        // check well-formedness of the preconditions, and then assume each one of them
-        readsCheckDelayer.DoWithDelayedReadsChecks(false, wfo => {
-          foreach (AttributedExpression p in m.Req) {
-            CheckWellformedAndAssume(p.E, wfo, localVariables, builder, etran, "method requires clause");
-          }
-        });
-
-        // check well-formedness of the reads clauses
-        readsCheckDelayer.DoWithDelayedReadsChecks(false, wfo => {
-          CheckFrameWellFormed(wfo, m.Reads.Expressions, localVariables, builder, etran);
-        });
-        // Also check that the reads clause == {} if the {:concurrent} attribute is present
-        // on the method, and {:assume_concurrent} is NOT present on the reads clause.
-        if (Attributes.Contains(m.Attributes, Attributes.ConcurrentAttributeName) &&
-            !Attributes.Contains(m.Reads.Attributes, Attributes.AssumeConcurrentAttributeName)) {
-          var desc = new PODesc.ConcurrentFrameEmpty(m, "reads");
-          if (etran.readsFrame != null) {
-            CheckFrameEmpty(m.tok, etran, etran.ReadsFrame(m.tok), builder, desc, null);
-          } else {
-            // etran.readsFrame being null indicates the default of reads *,
-            // so this is an automatic failure.
-            builder.Add(Assert(m.tok, Expr.False, desc));
+    private StmtList TrMethodContractWellformedness(Method m, ExpressionTranslator etran, List<Variable> localVariables,
+      BoogieStmtListBuilder builderInitializationArea, BoogieStmtListBuilder builder, List<Variable> outParams) {
+      StmtList stmts;
+      var readsCheckDelayer = new ReadsCheckDelayer(etran, null, localVariables, builderInitializationArea, builder);
+
+      // check well-formedness of any default-value expressions (before assuming preconditions)
+      readsCheckDelayer.DoWithDelayedReadsChecks(true, wfo => {
+        foreach (var formal in m.Ins.Where(formal => formal.DefaultValue != null)) {
+          var e = formal.DefaultValue;
+          CheckWellformed(e, wfo, localVariables, builder, etran.WithReadsFrame(etran.readsFrame, null)); // No scope for default parameters
+          builder.Add(new Boogie.AssumeCmd(e.tok, etran.CanCallAssumption(e)));
+          CheckSubrange(e.tok, etran.TrExpr(e), e.Type, formal.Type, e, builder);
+
+          if (formal.IsOld) {
+            Boogie.Expr wh = GetWhereClause(e.tok, etran.TrExpr(e), e.Type, etran.Old, ISALLOC, true);
+            if (wh != null) {
+              var desc = new PODesc.IsAllocated("default value", "in the two-state lemma's previous state", e);
+              builder.Add(Assert(e.RangeToken, wh, desc));
+            }
           }
         }
+      });
 
-        // check well-formedness of the modifies clauses
-        readsCheckDelayer.DoWithDelayedReadsChecks(false, wfo => {
-          CheckFrameWellFormed(wfo, m.Mod.Expressions, localVariables, builder, etran);
-        });
-        // Also check that the modifies clause == {} if the {:concurrent} attribute is present,
-        // and {:assume_concurrent} is NOT present on the modifies clause.
-        if (Attributes.Contains(m.Attributes, Attributes.ConcurrentAttributeName) &&
-            !Attributes.Contains(m.Mod.Attributes, Attributes.AssumeConcurrentAttributeName)) {
-          var desc = new PODesc.ConcurrentFrameEmpty(m, "modifies");
-          CheckFrameEmpty(m.tok, etran, etran.ModifiesFrame(m.tok), builder, desc, null);
+      // check well-formedness of the preconditions, and then assume each one of them
+      readsCheckDelayer.DoWithDelayedReadsChecks(false, wfo => {
+        foreach (AttributedExpression p in m.Req) {
+          CheckWellformedAndAssume(p.E, wfo, localVariables, builder, etran, "method requires clause");
         }
+      });
 
-        // check well-formedness of the decreases clauses
-        foreach (Expression p in m.Decreases.Expressions) {
-          CheckWellformed(p, new WFOptions(), localVariables, builder, etran);
+      // check well-formedness of the reads clauses
+      readsCheckDelayer.DoWithDelayedReadsChecks(false, wfo => {
+        CheckFrameWellFormed(wfo, m.Reads.Expressions, localVariables, builder, etran);
+      });
+      // Also check that the reads clause == {} if the {:concurrent} attribute is present
+      // on the method, and {:assume_concurrent} is NOT present on the reads clause.
+      if (Attributes.Contains(m.Attributes, Attributes.ConcurrentAttributeName) &&
+          !Attributes.Contains(m.Reads.Attributes, Attributes.AssumeConcurrentAttributeName)) {
+        var desc = new PODesc.ConcurrentFrameEmpty(m, "reads");
+        if (etran.readsFrame != null) {
+          CheckFrameEmpty(m.tok, etran, etran.ReadsFrame(m.tok), builder, desc, null);
+        } else {
+          // etran.readsFrame being null indicates the default of reads *,
+          // so this is an automatic failure.
+          builder.Add(Assert(m.tok, Expr.False, desc));
         }
+      }
 
-        if (!(m is TwoStateLemma)) {
-          // play havoc with the heap according to the modifies clause
-          builder.Add(new Boogie.HavocCmd(m.tok, new List<Boogie.IdentifierExpr> { etran.HeapCastToIdentifierExpr }));
-          // assume the usual two-state boilerplate information
-          foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(m.tok, m.Mod.Expressions, m.IsGhost, m.AllowsAllocation, etran.Old, etran, etran.Old)) {
-            if (tri.IsFree) {
-              builder.Add(TrAssumeCmd(m.tok, tri.Expr));
-            }
-          }
-        }
+      // check well-formedness of the modifies clauses
+      readsCheckDelayer.DoWithDelayedReadsChecks(false, wfo => {
+        CheckFrameWellFormed(wfo, m.Mod.Expressions, localVariables, builder, etran);
+      });
+      // Also check that the modifies clause == {} if the {:concurrent} attribute is present,
+      // and {:assume_concurrent} is NOT present on the modifies clause.
+      if (Attributes.Contains(m.Attributes, Attributes.ConcurrentAttributeName) &&
+          !Attributes.Contains(m.Mod.Attributes, Attributes.AssumeConcurrentAttributeName)) {
+        var desc = new PODesc.ConcurrentFrameEmpty(m, "modifies");
+        CheckFrameEmpty(m.tok, etran, etran.ModifiesFrame(m.tok), builder, desc, null);
+      }
+
+      // check well-formedness of the decreases clauses
+      foreach (Expression p in m.Decreases.Expressions) {
+        CheckWellformed(p, new WFOptions(), localVariables, builder, etran);
+      }
 
-        // also play havoc with the out parameters
-        if (outParams.Count != 0) {  // don't create an empty havoc statement
-          List<Boogie.IdentifierExpr> outH = new List<Boogie.IdentifierExpr>();
-          foreach (Boogie.Variable b in outParams) {
-            Contract.Assert(b != null);
-            outH.Add(new Boogie.IdentifierExpr(b.tok, b));
+      if (!(m is TwoStateLemma)) {
+        // play havoc with the heap according to the modifies clause
+        builder.Add(new Boogie.HavocCmd(m.tok, new List<Boogie.IdentifierExpr> { etran.HeapCastToIdentifierExpr }));
+        // assume the usual two-state boilerplate information
+        foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(m.tok, m.Mod.Expressions, m.IsGhost, m.AllowsAllocation, etran.Old, etran, etran.Old)) {
+          if (tri.IsFree) {
+            builder.Add(TrAssumeCmd(m.tok, tri.Expr));
           }
-          builder.Add(new Boogie.HavocCmd(m.tok, outH));
-        }
-        // mark the end of the modifles/out-parameter havocking with a CaptureState; make its location be the first ensures clause, if any (and just
-        // omit the CaptureState if there's no ensures clause)
-        if (m.Ens.Count != 0) {
-          builder.AddCaptureState(m.Ens[0].E.tok, false, "post-state");
         }
+      }
 
-        // check wellformedness of postconditions
-        foreach (AttributedExpression p in m.Ens) {
-          CheckWellformedAndAssume(p.E, new WFOptions(), localVariables, builder, etran, "method ensures clause");
+      // also play havoc with the out parameters
+      if (outParams.Count != 0) {  // don't create an empty havoc statement
+        List<Boogie.IdentifierExpr> outH = new List<Boogie.IdentifierExpr>();
+        foreach (Boogie.Variable b in outParams) {
+          Contract.Assert(b != null);
+          outH.Add(new Boogie.IdentifierExpr(b.tok, b));
         }
+        builder.Add(new Boogie.HavocCmd(m.tok, outH));
+      }
+      // mark the end of the modifles/out-parameter havocking with a CaptureState; make its location be the first ensures clause, if any (and just
+      // omit the CaptureState if there's no ensures clause)
+      if (m.Ens.Count != 0) {
+        builder.AddCaptureState(m.Ens[0].E.tok, false, "post-state");
+      }
 
-        var s0 = builderInitializationArea.Collect(m.tok);
-        var s1 = builder.Collect(m.tok);
-        stmts = new StmtList(new List<BigBlock>(s0.BigBlocks.Concat(s1.BigBlocks)), m.tok);
+      // check wellformedness of postconditions
+      foreach (AttributedExpression p in m.Ens) {
+        CheckWellformedAndAssume(p.E, new WFOptions(), localVariables, builder, etran, "method ensures clause");
       }
 
-      if (EmitImplementation(m.Attributes)) {
-        // emit impl only when there are proof obligations.
-        QKeyValue kv = etran.TrAttributes(m.Attributes, null);
-        Boogie.Implementation impl = AddImplementationWithAttributes(GetToken(m), proc,
-           inParams, outParams, localVariables, stmts, kv);
+      var s0 = builderInitializationArea.Collect(m.tok);
+      var s1 = builder.Collect(m.tok);
+      stmts = new StmtList(new List<BigBlock>(s0.BigBlocks.Concat(s1.BigBlocks)), m.tok);
+      return stmts;
+    }
 
-        if (InsertChecksums) {
-          InsertChecksum(m, impl);
+    private StmtList TrMethodBody(Method m, BoogieStmtListBuilder builder, List<Variable> localVariables, ExpressionTranslator etran) {
+      StmtList stmts;
+      var inductionVars = ApplyInduction(m.Ins, m.Attributes);
+      if (inductionVars.Count != 0) {
+        // Let the parameters be this,x,y of the method M and suppose ApplyInduction returns this,y.
+        // Also, let Pre be the precondition and VF be the decreases clause.
+        // Then, insert into the method body what amounts to:
+        //     assume case-analysis-on-parameter[[ y' ]];
+        //     forall this',y' | Pre(this', x, y') && (VF(this', x, y') << VF(this', x, y)) {
+        //       this'.M(x, y');
+        //     }
+        // Generate bound variables for the forall statement, and a substitution for the Pre and VF
+
+        // assume case-analysis-on-parameter[[ y' ]];
+        foreach (var inFormal in m.Ins) {
+          var dt = inFormal.Type.AsDatatype;
+          if (dt != null) {
+            var funcID = new Boogie.FunctionCall(new Boogie.IdentifierExpr(inFormal.tok, "$IsA#" + dt.FullSanitizedName, Boogie.Type.Bool));
+            var f = new Boogie.IdentifierExpr(inFormal.tok, inFormal.AssignUniqueName(m.IdGenerator), TrType(inFormal.Type));
+            builder.Add(TrAssumeCmd(inFormal.tok, new Boogie.NAryExpr(inFormal.tok, funcID, new List<Boogie.Expr> { f })));
+          }
         }
-      }
 
-      isAllocContext = null;
-      Reset();
+        var parBoundVars = new List<BoundVar>();
+        var parBounds = new List<BoundedPool>();
+        var substMap = new Dictionary<IVariable, Expression>();
+        Expression receiverSubst = null;
+        foreach (var iv in inductionVars) {
+          BoundVar bv;
+          if (iv == null) {
+            // this corresponds to "this"
+            Contract.Assert(!m.IsStatic);  // if "m" is static, "this" should never have gone into the _induction attribute
+            Contract.Assert(receiverSubst == null);  // we expect at most one
+            var receiverType = ModuleResolver.GetThisType(m.tok, (TopLevelDeclWithMembers)m.EnclosingClass);
+            bv = new BoundVar(m.tok, CurrentIdGenerator.FreshId("$ih#this"), receiverType); // use this temporary variable counter, but for a Dafny name (the idea being that the number and the initial "_" in the name might avoid name conflicts)
+            var ie = new IdentifierExpr(m.tok, bv.Name) {
+              Var = bv,
+              Type = bv.Type
+            };
+            receiverSubst = ie;
+          } else {
+            CloneVariableAsBoundVar(iv.tok, iv, "$ih#" + iv.Name, out bv, out var ie);
+            substMap.Add(iv, ie);
+          }
+          parBoundVars.Add(bv);
+          parBounds.Add(new SpecialAllocIndependenceAllocatedBoundedPool());  // record that we don't want alloc antecedents for these variables
+        }
+
+        // Generate a CallStmt to be used as the body of the 'forall' statement.
+        m.RecursiveCallParameters(m.tok, m.TypeArgs, m.Ins, receiverSubst, substMap, out var recursiveCallReceiver, out var recursiveCallArgs);
+        var methodSel = new MemberSelectExpr(m.tok, recursiveCallReceiver, m.Name) {
+          Member = m,
+          TypeApplication_AtEnclosingClass = m.EnclosingClass.TypeArgs.ConvertAll(tp => (Type)new UserDefinedType(tp.tok, tp)),
+          TypeApplication_JustMember = m.TypeArgs.ConvertAll(tp => (Type)new UserDefinedType(tp.tok, tp)),
+          Type = new InferredTypeProxy()
+        };
+        var recursiveCall = new CallStmt(m.tok.ToRange(), new List<Expression>(), methodSel, recursiveCallArgs) {
+          IsGhost = m.IsGhost
+        };
+
+        Expression parRange = Expression.CreateBoolLiteral(m.tok, true);
+        foreach (var pre in m.Req) {
+          parRange = Expression.CreateAnd(parRange, Substitute(pre.E, receiverSubst, substMap));
+        }
+        // construct an expression (generator) for:  VF' << VF
+        ExpressionConverter decrCheck = delegate (Dictionary<IVariable, Expression> decrSubstMap, ExpressionTranslator exprTran) {
+          var decrToks = new List<IToken>();
+          var decrTypes = new List<Type>();
+          var decrCallee = new List<Expr>();
+          var decrCaller = new List<Expr>();
+          var decrCalleeDafny = new List<Expression>();
+          var decrCallerDafny = new List<Expression>();
+          foreach (var ee in m.Decreases.Expressions) {
+            decrToks.Add(ee.tok);
+            decrTypes.Add(ee.Type.NormalizeExpand());
+            decrCallerDafny.Add(ee);
+            decrCaller.Add(exprTran.TrExpr(ee));
+            Expression es = Substitute(ee, receiverSubst, substMap);
+            es = Substitute(es, null, decrSubstMap);
+            decrCalleeDafny.Add(es);
+            decrCallee.Add(exprTran.TrExpr(es));
+          }
+          return DecreasesCheck(decrToks, null, decrCalleeDafny, decrCallerDafny, decrCallee, decrCaller,
+            null, null, false, true);
+        };
+
+#if VERIFY_CORRECTNESS_OF_TRANSLATION_FORALL_STATEMENT_RANGE
+          var definedness = new BoogieStmtListBuilder(this, options);
+          var exporter = new BoogieStmtListBuilder(this, options);
+          TrForallStmtCall(m.tok, parBoundVars, parRange, decrCheck, null, recursiveCall, definedness, exporter, localVariables, etran);
+          // All done, so put the two pieces together
+          builder.Add(new Bpl.IfCmd(m.tok, null, definedness.Collect(m.tok), null, exporter.Collect(m.tok)));
+#else
+        TrForallStmtCall(m.tok, parBoundVars, parBounds, parRange, decrCheck, null, recursiveCall, null, builder, localVariables, etran);
+#endif
+      }
+      // translate the body of the method
+      Contract.Assert(m.Body != null);  // follows from method precondition and the if guard
+
+      // $_reverifyPost := false;
+      builder.Add(Boogie.Cmd.SimpleAssign(m.tok, new Boogie.IdentifierExpr(m.tok, "$_reverifyPost", Boogie.Type.Bool), Boogie.Expr.False));
+      // register output parameters with definite-assignment trackers
+      Contract.Assert(definiteAssignmentTrackers.Count == 0);
+      m.Outs.ForEach(p => AddExistingDefiniteAssignmentTracker(p, m.IsGhost));
+      // translate the body
+      TrStmt(m.Body, builder, localVariables, etran);
+      m.Outs.ForEach(p => CheckDefiniteAssignmentReturn(m.Body.RangeToken.EndToken, p, builder));
+      if (m is { FunctionFromWhichThisIsByMethodDecl: { ByMethodTok: { } } fun }) {
+        AssumeCanCallForByMethodDecl(m, builder);
+      }
+      stmts = builder.Collect(m.Body.RangeToken.StartToken); // TODO should this be EndToken?  the parameter name suggests it should be the closing curly
+      // tear down definite-assignment trackers
+      m.Outs.ForEach(RemoveDefiniteAssignmentTracker);
+
+      Contract.Assert(definiteAssignmentTrackers.Count == 0);
+      return stmts;
     }
 
     private void AddMethodOverrideCheckImpl(Method m, Boogie.Procedure proc) {
diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.SplitExpr.cs b/Source/DafnyCore/Verifier/BoogieGenerator.SplitExpr.cs
index 05b7dabd5e..0a558495ab 100644
--- a/Source/DafnyCore/Verifier/BoogieGenerator.SplitExpr.cs
+++ b/Source/DafnyCore/Verifier/BoogieGenerator.SplitExpr.cs
@@ -39,7 +39,8 @@ public partial class BoogieGenerator {
     /// if its body is available in the current context and its height is less than "heightLimit" (if "heightLimit" is
     /// passed in as 0, then no functions will be inlined).
     /// </summary>
-    bool TrSplitExpr(Expression expr, List<SplitExprInfo/*!*/>/*!*/ splits, bool position, int heightLimit, bool inlineProtectedFunctions, bool apply_induction, ExpressionTranslator etran) {
+    bool TrSplitExpr(Expression expr, List<SplitExprInfo/*!*/>/*!*/ splits, bool position, int heightLimit,
+      bool inlineProtectedFunctions, bool applyInduction, ExpressionTranslator etran) {
       Contract.Requires(expr != null);
       Contract.Requires(expr.Type.IsBoolType || (expr is BoxingCastExpr && ((BoxingCastExpr)expr).E.Type.IsBoolType));
       Contract.Requires(splits != null);
@@ -49,7 +50,7 @@ bool TrSplitExpr(Expression expr, List<SplitExprInfo/*!*/>/*!*/ splits, bool pos
         case BoxingCastExpr castExpr: {
             var bce = castExpr;
             var ss = new List<SplitExprInfo>();
-            if (TrSplitExpr(bce.E, ss, position, heightLimit, inlineProtectedFunctions, apply_induction, etran)) {
+            if (TrSplitExpr(bce.E, ss, position, heightLimit, inlineProtectedFunctions, applyInduction, etran)) {
               foreach (var s in ss) {
                 splits.Add(ToSplitExprInfo(s.Kind, CondApplyBox(s.Tok, s.E, bce.FromType, bce.ToType)));
               }
@@ -60,18 +61,18 @@ bool TrSplitExpr(Expression expr, List<SplitExprInfo/*!*/>/*!*/ splits, bool pos
           }
         case ConcreteSyntaxExpression expression: {
             var e = expression;
-            return TrSplitExpr(e.ResolvedExpression, splits, position, heightLimit, inlineProtectedFunctions, apply_induction, etran);
+            return TrSplitExpr(e.ResolvedExpression, splits, position, heightLimit, inlineProtectedFunctions, applyInduction, etran);
           }
         case NestedMatchExpr nestedMatchExpr:
-          return TrSplitExpr(nestedMatchExpr.Flattened, splits, position, heightLimit, inlineProtectedFunctions, apply_induction, etran);
+          return TrSplitExpr(nestedMatchExpr.Flattened, splits, position, heightLimit, inlineProtectedFunctions, applyInduction, etran);
         case LetExpr letExpr: {
             var e = letExpr;
             if (!e.Exact) {
               var d = LetDesugaring(e);
-              return TrSplitExpr(d, splits, position, heightLimit, inlineProtectedFunctions, apply_induction, etran);
+              return TrSplitExpr(d, splits, position, heightLimit, inlineProtectedFunctions, applyInduction, etran);
             } else {
               var ss = new List<SplitExprInfo>();
-              if (TrSplitExpr(e.Body, ss, position, heightLimit, inlineProtectedFunctions, apply_induction, etran)) {
+              if (TrSplitExpr(e.Body, ss, position, heightLimit, inlineProtectedFunctions, applyInduction, etran)) {
                 // We don't know where the RHSs of the let are used in the body. In particular, we don't know if a RHS
                 // will end up in a spot where TrSplitExpr would like to increase the Layer offset or not. In fact, different
                 // uses of the same let variable may end up needing different Layer constants. The following code will
@@ -98,7 +99,7 @@ bool TrSplitExpr(Expression expr, List<SplitExprInfo/*!*/>/*!*/ splits, bool pos
                 var tok = new NestedToken(GetToken(e), fe.tok);
                 Expression ee = new UnchangedExpr(tok, new List<FrameExpression> { fe }, e.At) { AtLabel = e.AtLabel };
                 ee.Type = Type.Bool;  // resolve here
-                TrSplitExpr(ee, splits, position, heightLimit, inlineProtectedFunctions, apply_induction, etran);
+                TrSplitExpr(ee, splits, position, heightLimit, inlineProtectedFunctions, applyInduction, etran);
               }
               return true;
             }
@@ -109,7 +110,7 @@ bool TrSplitExpr(Expression expr, List<SplitExprInfo/*!*/>/*!*/ splits, bool pos
             var e = opExpr;
             if (e.ResolvedOp == UnaryOpExpr.ResolvedOpcode.BoolNot) {
               var ss = new List<SplitExprInfo>();
-              if (TrSplitExpr(e.E, ss, !position, heightLimit, inlineProtectedFunctions, apply_induction, etran)) {
+              if (TrSplitExpr(e.E, ss, !position, heightLimit, inlineProtectedFunctions, applyInduction, etran)) {
                 foreach (var s in ss) {
                   splits.Add(ToSplitExprInfo(s.Kind, Bpl.Expr.Unary(s.E.tok, UnaryOperator.Opcode.Not, s.E)));
                 }
@@ -122,13 +123,13 @@ bool TrSplitExpr(Expression expr, List<SplitExprInfo/*!*/>/*!*/ splits, bool pos
         case BinaryExpr binaryExpr: {
             var bin = binaryExpr;
             if (position && bin.ResolvedOp == BinaryExpr.ResolvedOpcode.And) {
-              TrSplitExpr(bin.E0, splits, position, heightLimit, inlineProtectedFunctions, apply_induction, etran);
-              TrSplitExpr(bin.E1, splits, position, heightLimit, inlineProtectedFunctions, apply_induction, etran);
+              TrSplitExpr(bin.E0, splits, position, heightLimit, inlineProtectedFunctions, applyInduction, etran);
+              TrSplitExpr(bin.E1, splits, position, heightLimit, inlineProtectedFunctions, applyInduction, etran);
               return true;
 
             } else if (!position && bin.ResolvedOp == BinaryExpr.ResolvedOpcode.Or) {
-              TrSplitExpr(bin.E0, splits, position, heightLimit, inlineProtectedFunctions, apply_induction, etran);
-              TrSplitExpr(bin.E1, splits, position, heightLimit, inlineProtectedFunctions, apply_induction, etran);
+              TrSplitExpr(bin.E0, splits, position, heightLimit, inlineProtectedFunctions, applyInduction, etran);
+              TrSplitExpr(bin.E1, splits, position, heightLimit, inlineProtectedFunctions, applyInduction, etran);
               return true;
 
             } else if (bin.ResolvedOp == BinaryExpr.ResolvedOpcode.Imp) {
@@ -136,14 +137,14 @@ bool TrSplitExpr(Expression expr, List<SplitExprInfo/*!*/>/*!*/ splits, bool pos
               if (position) {
                 var lhs = etran.TrExpr(bin.E0);
                 var ss = new List<SplitExprInfo>();
-                TrSplitExpr(bin.E1, ss, position, heightLimit, inlineProtectedFunctions, apply_induction, etran);
+                TrSplitExpr(bin.E1, ss, position, heightLimit, inlineProtectedFunctions, applyInduction, etran);
                 foreach (var s in ss) {
                   // as the source location in the following implication, use that of the translated "s"
                   splits.Add(ToSplitExprInfo(s.Kind, Bpl.Expr.Binary(s.E.tok, BinaryOperator.Opcode.Imp, lhs, s.E)));
                 }
               } else {
                 var ss = new List<SplitExprInfo>();
-                TrSplitExpr(bin.E0, ss, !position, heightLimit, inlineProtectedFunctions, apply_induction, etran);
+                TrSplitExpr(bin.E0, ss, !position, heightLimit, inlineProtectedFunctions, applyInduction, etran);
                 var rhs = etran.TrExpr(bin.E1);
                 foreach (var s in ss) {
                   // as the source location in the following implication, use that of the translated "s"
@@ -217,8 +218,8 @@ bool TrSplitExpr(Expression expr, List<SplitExprInfo/*!*/>/*!*/ splits, bool pos
             var ssThen = new List<SplitExprInfo>();
             var ssElse = new List<SplitExprInfo>();
 
-            TrSplitExpr(ite.Thn, ssThen, position, heightLimit, inlineProtectedFunctions, apply_induction, etran);
-            TrSplitExpr(ite.Els, ssElse, position, heightLimit, inlineProtectedFunctions, apply_induction, etran);
+            TrSplitExpr(ite.Thn, ssThen, position, heightLimit, inlineProtectedFunctions, applyInduction, etran);
+            TrSplitExpr(ite.Els, ssElse, position, heightLimit, inlineProtectedFunctions, applyInduction, etran);
 
             var op = position ? BinaryOperator.Opcode.Imp : BinaryOperator.Opcode.And;
             var test = etran.TrExpr(ite.Test);
@@ -238,7 +239,7 @@ bool TrSplitExpr(Expression expr, List<SplitExprInfo/*!*/>/*!*/ splits, bool pos
         case MatchExpr matchExpr: {
             var e = matchExpr;
             var ite = etran.DesugarMatchExpr(e);
-            return TrSplitExpr(ite, splits, position, heightLimit, inlineProtectedFunctions, apply_induction, etran);
+            return TrSplitExpr(ite, splits, position, heightLimit, inlineProtectedFunctions, applyInduction, etran);
           }
         case StmtExpr stmtExpr: {
             var e = stmtExpr;
@@ -248,14 +249,14 @@ bool TrSplitExpr(Expression expr, List<SplitExprInfo/*!*/>/*!*/ splits, bool pos
             if (position) {
               var conclusion = etran.TrExpr(e.GetSConclusion());
               var ss = new List<SplitExprInfo>();
-              TrSplitExpr(e.E, ss, position, heightLimit, inlineProtectedFunctions, apply_induction, etran);
+              TrSplitExpr(e.E, ss, position, heightLimit, inlineProtectedFunctions, applyInduction, etran);
               foreach (var s in ss) {
                 // as the source location in the following implication, use that of the translated "s"
                 splits.Add(ToSplitExprInfo(s.Kind, Bpl.Expr.Binary(s.E.tok, BinaryOperator.Opcode.Imp, conclusion, s.E)));
               }
             } else {
               var ss = new List<SplitExprInfo>();
-              TrSplitExpr(e.GetSConclusion(), ss, !position, heightLimit, inlineProtectedFunctions, apply_induction, etran);
+              TrSplitExpr(e.GetSConclusion(), ss, !position, heightLimit, inlineProtectedFunctions, applyInduction, etran);
               var rhs = etran.TrExpr(e.E);
               foreach (var s in ss) {
                 // as the source location in the following implication, use that of the translated "s"
@@ -266,23 +267,23 @@ bool TrSplitExpr(Expression expr, List<SplitExprInfo/*!*/>/*!*/ splits, bool pos
           }
         case OldExpr oldExpr: {
             var e = oldExpr;
-            return TrSplitExpr(e.E, splits, position, heightLimit, inlineProtectedFunctions, apply_induction, etran.OldAt(e.AtLabel));
+            return TrSplitExpr(e.E, splits, position, heightLimit, inlineProtectedFunctions, applyInduction, etran.OldAt(e.AtLabel));
           }
         case FunctionCallExpr callExpr when position: {
             var fexp = callExpr;
-            if (TrSplitFunctionCallExpr(callExpr, splits, heightLimit, inlineProtectedFunctions, apply_induction, etran, fexp)) {
+            if (TrSplitFunctionCallExpr(callExpr, splits, heightLimit, inlineProtectedFunctions, applyInduction, etran, fexp)) {
               return true;
             }
 
             break;
           }
         case QuantifierExpr quantifierExpr when quantifierExpr.SplitQuantifier != null:
-          return TrSplitExpr(quantifierExpr.SplitQuantifierExpression, splits, position, heightLimit, inlineProtectedFunctions, apply_induction, etran);
+          return TrSplitExpr(quantifierExpr.SplitQuantifierExpression, splits, position, heightLimit, inlineProtectedFunctions, applyInduction, etran);
         default: {
             if (((position && expr is ForallExpr) || (!position && expr is ExistsExpr))) {
               var e = (QuantifierExpr)expr;
               var inductionVariables = ApplyInduction(e.BoundVars, e.Attributes);
-              if (apply_induction && inductionVariables.Count != 0) {
+              if (applyInduction && inductionVariables.Count != 0) {
                 // From the given quantifier (forall n :: P(n)), generate the seemingly weaker proof obligation
                 //   (forall n :: (forall k :: k < n ==> P(k)) ==> P(n))
                 // For an existential (exists n :: P(n)), it is
@@ -473,7 +474,7 @@ bool TrSplitExpr(Expression expr, List<SplitExprInfo/*!*/>/*!*/ splits, bool pos
     }
 
     private bool TrSplitFunctionCallExpr(Expression expr, List<SplitExprInfo> splits, int heightLimit, bool inlineProtectedFunctions,
-      bool apply_induction, ExpressionTranslator etran, FunctionCallExpr fexp) {
+      bool applyInduction, ExpressionTranslator etran, FunctionCallExpr fexp) {
       var f = fexp.Function;
       Contract.Assert(f != null); // filled in during resolution
       var module = f.EnclosingClass.EnclosingModuleDefinition;
@@ -529,7 +530,7 @@ private bool TrSplitFunctionCallExpr(Expression expr, List<SplitExprInfo> splits
 
             // recurse on body
             var ss = new List<SplitExprInfo>();
-            TrSplitExpr(typeSpecializedBody, ss, true, functionHeight, inlineProtectedFunctions, apply_induction, etran);
+            TrSplitExpr(typeSpecializedBody, ss, true, functionHeight, inlineProtectedFunctions, applyInduction, etran);
             var needsTokenAdjust = TrSplitNeedsTokenAdjustment(typeSpecializedBody);
             foreach (var s in ss) {
               if (s.IsChecked) {
diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.TrPredicateStatement.cs b/Source/DafnyCore/Verifier/BoogieGenerator.TrPredicateStatement.cs
new file mode 100644
index 0000000000..7a3281e860
--- /dev/null
+++ b/Source/DafnyCore/Verifier/BoogieGenerator.TrPredicateStatement.cs
@@ -0,0 +1,169 @@
+using System;
+using System.Collections.Generic;
+using System.Diagnostics.Contracts;
+using System.Linq;
+using DafnyCore.Verifier;
+using Microsoft.Boogie;
+using Bpl = Microsoft.Boogie;
+using BplParser = Microsoft.Boogie.Parser;
+using static Microsoft.Dafny.Util;
+using PODesc = Microsoft.Dafny.ProofObligationDescription;
+
+namespace Microsoft.Dafny {
+  public partial class BoogieGenerator {
+    private void TrPredicateStmt(PredicateStmt stmt, BoogieStmtListBuilder builder, List<Variable> locals, ExpressionTranslator etran) {
+      Contract.Requires(stmt != null);
+      Contract.Requires(builder != null);
+      Contract.Requires(locals != null);
+      Contract.Requires(etran != null);
+
+      fuelContext = FuelSetting.ExpandFuelContext(stmt.Attributes, stmt.Tok, fuelContext, reporter);
+      if (stmt is AssertStmt || options.DisallowSoundnessCheating) {
+        TrAssertStmt(stmt, builder, locals, etran);
+      } else if (stmt is ExpectStmt expectStmt) {
+        TrExpectStmt(builder, locals, etran, expectStmt);
+      } else if (stmt is AssumeStmt assumeStmt) {
+        TrAssumeStmt(assumeStmt, builder, locals, etran);
+      }
+      fuelContext = FuelSetting.PopFuelContext();
+    }
+
+    private void TrAssumeStmt(AssumeStmt assumeStmt, BoogieStmtListBuilder builder, List<Variable> locals, ExpressionTranslator etran) {
+      AddComment(builder, assumeStmt, "assume statement");
+      stmtContext = StmtType.ASSUME;
+      TrStmt_CheckWellformed(assumeStmt.Expr, builder, locals, etran, false);
+      builder.Add(TrAssumeCmdWithDependencies(etran, assumeStmt.Tok, assumeStmt.Expr, "assume statement", true,
+        etran.TrAttributes(assumeStmt.Attributes, null)));
+      stmtContext = StmtType.NONE; // done with translating assume stmt.
+      if (options.TestGenOptions.Mode != TestGenerationOptions.Modes.None) {
+        builder.AddCaptureState(assumeStmt);
+      }
+    }
+
+    private void TrExpectStmt(BoogieStmtListBuilder builder, List<Variable> locals, ExpressionTranslator etran, ExpectStmt expectStmt) {
+      AddComment(builder, expectStmt, "expect statement");
+      stmtContext = StmtType.ASSUME;
+      TrStmt_CheckWellformed(expectStmt.Expr, builder, locals, etran, false);
+
+      // Need to check the message is well-formed, assuming the expected expression
+      // does NOT hold:
+      //
+      // if Not(TrExpr[[ s.Expr ]]) {
+      //  CheckWellformed[[ s.Message ]]
+      //  assume false;
+      // }
+      BoogieStmtListBuilder thnBuilder = new BoogieStmtListBuilder(this, options);
+      TrStmt_CheckWellformed(expectStmt.Message, thnBuilder, locals, etran, false);
+      thnBuilder.Add(TrAssumeCmd(expectStmt.Tok, new Bpl.LiteralExpr(expectStmt.Tok, false),
+        etran.TrAttributes(expectStmt.Attributes, null)));
+      Bpl.StmtList thn = thnBuilder.Collect(expectStmt.Tok);
+      builder.Add(new Bpl.IfCmd(expectStmt.Tok, Bpl.Expr.Not(etran.TrExpr(expectStmt.Expr)), thn, null, null));
+
+      stmtContext = StmtType.NONE; // done with translating expect stmt.
+    }
+
+    private void TrAssertStmt(PredicateStmt stmt, BoogieStmtListBuilder builder, List<Variable> locals, ExpressionTranslator etran) {
+      var stmtBuilder = new BoogieStmtListBuilder(this, options);
+      var defineFuel = DefineFuelConstant(stmt.Tok, stmt.Attributes, stmtBuilder, etran);
+      var b = defineFuel ? stmtBuilder : builder;
+      var (errorMessage, successMessage) = CustomErrorMessage(stmt.Attributes);
+      stmtContext = StmtType.ASSERT;
+      AddComment(b, stmt, "assert statement");
+      TrStmt_CheckWellformed(stmt.Expr, b, locals, etran, false);
+      IToken enclosingToken = null;
+      if (Attributes.Contains(stmt.Attributes, "_prependAssertToken")) {
+        enclosingToken = stmt.Tok;
+      }
+
+      BoogieStmtListBuilder proofBuilder = null;
+      var assertStmt = stmt as AssertStmt;
+      if (assertStmt != null) {
+        if (assertStmt.Proof != null) {
+          proofBuilder = new BoogieStmtListBuilder(this, options);
+          AddComment(proofBuilder, stmt, "assert statement proof");
+          CurrentIdGenerator.Push();
+          TrStmt(((AssertStmt)stmt).Proof, proofBuilder, locals, etran);
+          CurrentIdGenerator.Pop();
+        } else if (assertStmt.Label != null) {
+          proofBuilder = new BoogieStmtListBuilder(this, options);
+          AddComment(proofBuilder, stmt, "assert statement proof");
+        }
+      }
+
+      var splits = TrSplitExpr(stmt.Expr, etran, true, out var splitHappened);
+      if (!splitHappened) {
+        var tok = enclosingToken == null ? GetToken(stmt.Expr) : new NestedToken(enclosingToken, GetToken(stmt.Expr));
+        var desc = new PODesc.AssertStatementDescription(assertStmt, errorMessage, successMessage);
+        (proofBuilder ?? b).Add(Assert(tok, etran.TrExpr(stmt.Expr), desc, stmt.Tok,
+          etran.TrAttributes(stmt.Attributes, null)));
+      } else {
+        foreach (var split in splits) {
+          if (split.IsChecked) {
+            var tok = enclosingToken == null ? split.E.tok : new NestedToken(enclosingToken, split.Tok);
+            var desc = new PODesc.AssertStatementDescription(assertStmt, errorMessage, successMessage);
+            (proofBuilder ?? b).Add(AssertNS(ToDafnyToken(flags.ReportRanges, tok), split.E, desc, stmt.Tok,
+              etran.TrAttributes(stmt.Attributes, null))); // attributes go on every split
+          }
+        }
+      }
+
+      if (proofBuilder != null) {
+        PathAsideBlock(stmt.Tok, proofBuilder, b);
+      }
+
+      stmtContext = StmtType.NONE; // done with translating assert stmt
+      if (splitHappened || proofBuilder != null) {
+        if (assertStmt != null && assertStmt.Label != null) {
+          // make copies of the variables used in the assertion
+          var name = "$Heap_at_" + assertStmt.Label.AssignUniqueId(CurrentIdGenerator);
+          var heapAt = new Bpl.LocalVariable(stmt.Tok, new Bpl.TypedIdent(stmt.Tok, name, predef.HeapType));
+          locals.Add(heapAt);
+          var h = new Bpl.IdentifierExpr(stmt.Tok, heapAt);
+          b.Add(Bpl.Cmd.SimpleAssign(stmt.Tok, h, etran.HeapExpr));
+          var substMap = new Dictionary<IVariable, Expression>();
+          foreach (var v in FreeVariablesUtil.ComputeFreeVariables(options, assertStmt.Expr)) {
+            if (v is LocalVariable) {
+              var vcopy = new LocalVariable(stmt.RangeToken, string.Format("##{0}#{1}", name, v.Name), v.Type,
+                v.IsGhost);
+              vcopy.type = vcopy.SyntacticType; // resolve local here
+              IdentifierExpr ie = new IdentifierExpr(vcopy.Tok,
+                vcopy.AssignUniqueName(currentDeclaration.IdGenerator));
+              ie.Var = vcopy;
+              ie.Type = ie.Var.Type; // resolve ie here
+              substMap.Add(v, ie);
+              locals.Add(new Bpl.LocalVariable(vcopy.Tok,
+                new Bpl.TypedIdent(vcopy.Tok, vcopy.AssignUniqueName(currentDeclaration.IdGenerator),
+                  TrType(vcopy.Type))));
+              b.Add(Bpl.Cmd.SimpleAssign(stmt.Tok, TrVar(stmt.Tok, vcopy), TrVar(stmt.Tok, v)));
+            }
+          }
+
+          var exprToBeRevealed = Substitute(assertStmt.Expr, null, substMap);
+          var etr = new ExpressionTranslator(etran, h);
+          assertStmt.Label.E = etr.TrExpr(exprToBeRevealed);
+        } else if (!defineFuel) {
+          // Adding the assume stmt, resetting the stmtContext
+          stmtContext = StmtType.ASSUME;
+          adjustFuelForExists = true;
+          b.Add(TrAssumeCmdWithDependencies(etran, stmt.Tok, stmt.Expr, "assert statement", true));
+          stmtContext = StmtType.NONE;
+        }
+      }
+
+      if (defineFuel) {
+        var ifCmd = new Bpl.IfCmd(stmt.Tok, null, b.Collect(stmt.Tok), null,
+          null); // BUGBUG: shouldn't this first append "assume false" to "b"? (use PathAsideBlock to do this)  --KRML
+        builder.Add(ifCmd);
+        // Adding the assume stmt, resetting the stmtContext
+        stmtContext = StmtType.ASSUME;
+        adjustFuelForExists = true;
+        builder.Add(TrAssumeCmdWithDependencies(etran, stmt.Tok, stmt.Expr, "assert statement", true));
+        stmtContext = StmtType.NONE;
+      }
+
+      if (options.TestGenOptions.Mode != TestGenerationOptions.Modes.None) {
+        builder.AddCaptureState(stmt);
+      }
+    }
+  }
+}
diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs b/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs
index 03fa4006b1..3e03c89318 100644
--- a/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs
+++ b/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs
@@ -529,161 +529,6 @@ private void TrStmt(Statement stmt, BoogieStmtListBuilder builder, List<Variable
       }
     }
 
-    private void TrPredicateStmt(PredicateStmt stmt, BoogieStmtListBuilder builder, List<Variable> locals, ExpressionTranslator etran) {
-      Contract.Requires(stmt != null);
-      Contract.Requires(builder != null);
-      Contract.Requires(locals != null);
-      Contract.Requires(etran != null);
-
-      fuelContext = FuelSetting.ExpandFuelContext(stmt.Attributes, stmt.Tok, fuelContext, reporter);
-      if (stmt is AssertStmt || options.DisallowSoundnessCheating) {
-        TrAssertStmt(stmt, builder, locals, etran);
-      } else if (stmt is ExpectStmt expectStmt) {
-        TrExpectStmt(builder, locals, etran, expectStmt);
-      } else if (stmt is AssumeStmt assumeStmt) {
-        TrAssumeStmt(assumeStmt, builder, locals, etran);
-      }
-      fuelContext = FuelSetting.PopFuelContext();
-    }
-
-    private void TrAssumeStmt(AssumeStmt assumeStmt, BoogieStmtListBuilder builder, List<Variable> locals, ExpressionTranslator etran) {
-      AddComment(builder, assumeStmt, "assume statement");
-      stmtContext = StmtType.ASSUME;
-      TrStmt_CheckWellformed(assumeStmt.Expr, builder, locals, etran, false);
-      builder.Add(TrAssumeCmdWithDependencies(etran, assumeStmt.Tok, assumeStmt.Expr, "assume statement", true,
-        etran.TrAttributes(assumeStmt.Attributes, null)));
-      stmtContext = StmtType.NONE; // done with translating assume stmt.
-      if (options.TestGenOptions.Mode != TestGenerationOptions.Modes.None) {
-        builder.AddCaptureState(assumeStmt);
-      }
-    }
-
-    private void TrExpectStmt(BoogieStmtListBuilder builder, List<Variable> locals, ExpressionTranslator etran, ExpectStmt expectStmt) {
-      AddComment(builder, expectStmt, "expect statement");
-      stmtContext = StmtType.ASSUME;
-      TrStmt_CheckWellformed(expectStmt.Expr, builder, locals, etran, false);
-
-      // Need to check the message is well-formed, assuming the expected expression
-      // does NOT hold:
-      //
-      // if Not(TrExpr[[ s.Expr ]]) {
-      //  CheckWellformed[[ s.Message ]]
-      //  assume false;
-      // }
-      BoogieStmtListBuilder thnBuilder = new BoogieStmtListBuilder(this, options);
-      TrStmt_CheckWellformed(expectStmt.Message, thnBuilder, locals, etran, false);
-      thnBuilder.Add(TrAssumeCmd(expectStmt.Tok, new Bpl.LiteralExpr(expectStmt.Tok, false),
-        etran.TrAttributes(expectStmt.Attributes, null)));
-      Bpl.StmtList thn = thnBuilder.Collect(expectStmt.Tok);
-      builder.Add(new Bpl.IfCmd(expectStmt.Tok, Bpl.Expr.Not(etran.TrExpr(expectStmt.Expr)), thn, null, null));
-
-      stmtContext = StmtType.NONE; // done with translating expect stmt.
-    }
-
-    private void TrAssertStmt(PredicateStmt stmt, BoogieStmtListBuilder builder, List<Variable> locals, ExpressionTranslator etran) {
-      var stmtBuilder = new BoogieStmtListBuilder(this, options);
-      var defineFuel = DefineFuelConstant(stmt.Tok, stmt.Attributes, stmtBuilder, etran);
-      var b = defineFuel ? stmtBuilder : builder;
-      var (errorMessage, successMessage) = CustomErrorMessage(stmt.Attributes);
-      stmtContext = StmtType.ASSERT;
-      AddComment(b, stmt, "assert statement");
-      TrStmt_CheckWellformed(stmt.Expr, b, locals, etran, false);
-      IToken enclosingToken = null;
-      if (Attributes.Contains(stmt.Attributes, "_prependAssertToken")) {
-        enclosingToken = stmt.Tok;
-      }
-
-      BoogieStmtListBuilder proofBuilder = null;
-      var assertStmt = stmt as AssertStmt;
-      if (assertStmt != null) {
-        if (assertStmt.Proof != null) {
-          proofBuilder = new BoogieStmtListBuilder(this, options);
-          AddComment(proofBuilder, stmt, "assert statement proof");
-          CurrentIdGenerator.Push();
-          TrStmt(((AssertStmt)stmt).Proof, proofBuilder, locals, etran);
-          CurrentIdGenerator.Pop();
-        } else if (assertStmt.Label != null) {
-          proofBuilder = new BoogieStmtListBuilder(this, options);
-          AddComment(proofBuilder, stmt, "assert statement proof");
-        }
-      }
-
-      var splits = TrSplitExpr(stmt.Expr, etran, true, out var splitHappened);
-      if (!splitHappened) {
-        var tok = enclosingToken == null ? GetToken(stmt.Expr) : new NestedToken(enclosingToken, GetToken(stmt.Expr));
-        var desc = new PODesc.AssertStatementDescription(assertStmt, errorMessage, successMessage);
-        (proofBuilder ?? b).Add(Assert(tok, etran.TrExpr(stmt.Expr), desc, stmt.Tok,
-          etran.TrAttributes(stmt.Attributes, null)));
-      } else {
-        foreach (var split in splits) {
-          if (split.IsChecked) {
-            var tok = enclosingToken == null ? split.E.tok : new NestedToken(enclosingToken, split.Tok);
-            var desc = new PODesc.AssertStatementDescription(assertStmt, errorMessage, successMessage);
-            (proofBuilder ?? b).Add(AssertNS(ToDafnyToken(flags.ReportRanges, tok), split.E, desc, stmt.Tok,
-              etran.TrAttributes(stmt.Attributes, null))); // attributes go on every split
-          }
-        }
-      }
-
-      if (proofBuilder != null) {
-        PathAsideBlock(stmt.Tok, proofBuilder, b);
-      }
-
-      stmtContext = StmtType.NONE; // done with translating assert stmt
-      if (splitHappened || proofBuilder != null) {
-        if (assertStmt != null && assertStmt.Label != null) {
-          // make copies of the variables used in the assertion
-          var name = "$Heap_at_" + assertStmt.Label.AssignUniqueId(CurrentIdGenerator);
-          var heapAt = new Bpl.LocalVariable(stmt.Tok, new Bpl.TypedIdent(stmt.Tok, name, predef.HeapType));
-          locals.Add(heapAt);
-          var h = new Bpl.IdentifierExpr(stmt.Tok, heapAt);
-          b.Add(Bpl.Cmd.SimpleAssign(stmt.Tok, h, etran.HeapExpr));
-          var substMap = new Dictionary<IVariable, Expression>();
-          foreach (var v in FreeVariablesUtil.ComputeFreeVariables(options, assertStmt.Expr)) {
-            if (v is LocalVariable) {
-              var vcopy = new LocalVariable(stmt.RangeToken, string.Format("##{0}#{1}", name, v.Name), v.Type,
-                v.IsGhost);
-              vcopy.type = vcopy.SyntacticType; // resolve local here
-              IdentifierExpr ie = new IdentifierExpr(vcopy.Tok,
-                vcopy.AssignUniqueName(currentDeclaration.IdGenerator));
-              ie.Var = vcopy;
-              ie.Type = ie.Var.Type; // resolve ie here
-              substMap.Add(v, ie);
-              locals.Add(new Bpl.LocalVariable(vcopy.Tok,
-                new Bpl.TypedIdent(vcopy.Tok, vcopy.AssignUniqueName(currentDeclaration.IdGenerator),
-                  TrType(vcopy.Type))));
-              b.Add(Bpl.Cmd.SimpleAssign(stmt.Tok, TrVar(stmt.Tok, vcopy), TrVar(stmt.Tok, v)));
-            }
-          }
-
-          var exprToBeRevealed = Substitute(assertStmt.Expr, null, substMap);
-          var etr = new ExpressionTranslator(etran, h);
-          assertStmt.Label.E = etr.TrExpr(exprToBeRevealed);
-        } else if (!defineFuel) {
-          // Adding the assume stmt, resetting the stmtContext
-          stmtContext = StmtType.ASSUME;
-          adjustFuelForExists = true;
-          b.Add(TrAssumeCmdWithDependencies(etran, stmt.Tok, stmt.Expr, "assert statement", true));
-          stmtContext = StmtType.NONE;
-        }
-      }
-
-      if (defineFuel) {
-        var ifCmd = new Bpl.IfCmd(stmt.Tok, null, b.Collect(stmt.Tok), null,
-          null); // BUGBUG: shouldn't this first append "assume false" to "b"? (use PathAsideBlock to do this)  --KRML
-        builder.Add(ifCmd);
-        // Adding the assume stmt, resetting the stmtContext
-        stmtContext = StmtType.ASSUME;
-        adjustFuelForExists = true;
-        builder.Add(TrAssumeCmdWithDependencies(etran, stmt.Tok, stmt.Expr, "assert statement", true));
-        stmtContext = StmtType.NONE;
-      }
-
-      if (options.TestGenOptions.Mode != TestGenerationOptions.Modes.None) {
-        builder.AddCaptureState(stmt);
-      }
-    }
-
     private void TrCalcStmt(CalcStmt stmt, BoogieStmtListBuilder builder, List<Variable> locals, ExpressionTranslator etran) {
       Contract.Requires(stmt != null);
       Contract.Requires(builder != null);
diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.cs b/Source/DafnyCore/Verifier/BoogieGenerator.cs
index f89eacab52..7821bad63d 100644
--- a/Source/DafnyCore/Verifier/BoogieGenerator.cs
+++ b/Source/DafnyCore/Verifier/BoogieGenerator.cs
@@ -4556,13 +4556,13 @@ internal IsAllocType Var(bool ghostStmt, NonglobalVariable var) {
       }
     }
 
-    List<SplitExprInfo/*!*/>/*!*/ TrSplitExpr(Expression expr, ExpressionTranslator etran, bool apply_induction, out bool splitHappened) {
+    List<SplitExprInfo/*!*/>/*!*/ TrSplitExpr(Expression expr, ExpressionTranslator etran, bool applyInduction, out bool splitHappened) {
       Contract.Requires(expr != null);
       Contract.Requires(etran != null);
       Contract.Ensures(Contract.Result<List<SplitExprInfo>>() != null);
 
       var splits = new List<SplitExprInfo>();
-      splitHappened = TrSplitExpr(expr, splits, true, int.MaxValue, true, apply_induction, etran);
+      splitHappened = TrSplitExpr(expr, splits, true, int.MaxValue, true, applyInduction, etran);
       return splits;
     }
 
@@ -4572,9 +4572,9 @@ List<SplitExprInfo> TrSplitExprForMethodSpec(Expression expr, ExpressionTranslat
       Contract.Ensures(Contract.Result<List<SplitExprInfo>>() != null);
 
       var splits = new List<SplitExprInfo>();
-      var apply_induction = kind == MethodTranslationKind.Implementation;
-      bool splitHappened;  // we don't actually care
-      splitHappened = TrSplitExpr(expr, splits, true, int.MaxValue, kind != MethodTranslationKind.Call, apply_induction, etran);
+      var applyInduction = kind == MethodTranslationKind.Implementation;
+      TrSplitExpr(expr, splits, true, int.MaxValue,
+        kind != MethodTranslationKind.Call, applyInduction, etran);
       return splits;
     }