Penetrating by blocks

Source/DafnyCore/AST/Grammar/Printer/Printer.Statement.cs

@@ -30,7 +30,7 @@ public partial class Printer {
     /// If the statement requires several lines, subsequent lines are indented at "indent".
     /// No newline is printed after the statement.
     /// </summary>
-    public void PrintStatement(Statement stmt, int indent) {
+    public void PrintStatement(Statement stmt, int indent, bool includeSemicolon = true) {
       Contract.Requires(stmt != null);
 
       if (stmt.IsGhost && printMode == PrintModes.NoGhostOrIncludes) {
@@ -50,7 +50,7 @@ public void PrintStatement(Statement stmt, int indent) {
       }
 
       if (stmt is PredicateStmt) {
-        PrintPredicateStmt(stmt);
+        PrintPredicateStmt(stmt, includeSemicolon);
       } else if (stmt is PrintStmt) {
         PrintStmt s = (PrintStmt)stmt;
         wr.Write("print");
@@ -330,7 +330,7 @@ public void PrintStatement(Statement stmt, int indent) {
         }
 
       } else if (stmt is ConcreteAssignStatement) {
-        PrintConcreteUpdateStatement(stmt, indent);
+        PrintConcreteUpdateStatement(stmt, indent, includeSemicolon);
       } else if (stmt is CallStmt) {
         // Most calls are printed from their concrete syntax given in the input. However, recursive calls to
         // prefix lemmas end up as CallStmt's by the end of resolution and they may need to be printed here.
@@ -361,7 +361,10 @@ public void PrintStatement(Statement stmt, int indent) {
           wr.Write(" ");
           PrintUpdateRHS(s.Assign, indent);
         }
-        wr.Write(";");
+
+        if (includeSemicolon) {
+          wr.Write(";");
+        }
       } else if (stmt is VarDeclPattern) {
         var s = (VarDeclPattern)stmt;
         if (s.tok is AutoGeneratedToken) {

Source/DafnyCore/AST/Statements/BlockByProofStmt.cs

@@ -50,15 +50,7 @@ internal static void ResolveByProof(INewOrOldResolver resolver, BlockStmt proof,
   }
 
   public void Render(TextWriter wr, Printer printer, int indent) {
-    if (Body is AssertStmt assertStmt) {
-      printer.PrintPredicateStmt(assertStmt, false);
-    } else if (Body is ConcreteAssignStatement updateStmt) {
-      printer.PrintConcreteUpdateStatement(updateStmt, indent, false);
-    } else if (Body is BlockStmt blockStmt) {
-      printer.PrintBlockStmt(blockStmt, indent);
-    } else {
-      throw new NotImplementedException();
-    }
+    printer.PrintStatement(Body, indent, false);
     wr.Write(" by ");
     printer.PrintBlockStmt(Proof, indent);
   }

Source/DafnyCore/Verifier/Statements/BlockByProofStmtVerifier.cs

@@ -14,6 +14,7 @@ public static void EmitBoogie(BoogieGenerator generator, BlockByProofStmt block,
     generator.CurrentIdGenerator.Pop();
 
     generator.TrStmt(block.Body, proofBuilder, locals, etran);
+    //generator.RemoveDefiniteAssignmentTrackers(new [] { block.Body }, prevDefiniteAssignmentTrackerCount);
     generator.PathAsideBlock(block.Tok, proofBuilder, builder);
     generator.TrStmt(block.Body, builder.WithContext(builder.Context with {
       AssertMode = AssertMode.Assume