From 0db7ca27a89bf6f89f3c33e564b22ac91e0835f5 Mon Sep 17 00:00:00 2001
From: Dargones <sasha.fedchin@gmail.com>
Date: Wed, 3 May 2023 11:24:04 -0400
Subject: [PATCH 1/8] Make sure options are copied in ProgramModification

---
 Source/DafnyTestGeneration/DeadCodeCommand.cs      | 2 --
 Source/DafnyTestGeneration/GenerateTestsCommand.cs | 3 +--
 Source/DafnyTestGeneration/ProgramModification.cs  | 8 +++++---
 3 files changed, 6 insertions(+), 7 deletions(-)

diff --git a/Source/DafnyTestGeneration/DeadCodeCommand.cs b/Source/DafnyTestGeneration/DeadCodeCommand.cs
index 948d5f3546b..e8fe0788bfc 100644
--- a/Source/DafnyTestGeneration/DeadCodeCommand.cs
+++ b/Source/DafnyTestGeneration/DeadCodeCommand.cs
@@ -10,11 +10,9 @@ public class DeadCodeCommand : ICommandSpec {
     new Option[] {
       GenerateTestsCommand.LoopUnroll,
       GenerateTestsCommand.SequenceLengthLimit,
-      BoogieOptionBag.BoogieArguments,
       BoogieOptionBag.SolverLog,
       BoogieOptionBag.SolverOption,
       BoogieOptionBag.SolverPath,
-      BoogieOptionBag.SolverPlugin,
       BoogieOptionBag.SolverResourceLimit,
       BoogieOptionBag.VerificationTimeLimit
     }.Concat(ICommandSpec.ConsoleOutputOptions).
diff --git a/Source/DafnyTestGeneration/GenerateTestsCommand.cs b/Source/DafnyTestGeneration/GenerateTestsCommand.cs
index abaeacd6a27..3aa40c5cac3 100644
--- a/Source/DafnyTestGeneration/GenerateTestsCommand.cs
+++ b/Source/DafnyTestGeneration/GenerateTestsCommand.cs
@@ -4,6 +4,7 @@
 using System.CommandLine.Invocation;
 using System.Linq;
 using DafnyCore;
+using Microsoft.Boogie.SMTLib;
 
 namespace Microsoft.Dafny;
 
@@ -14,11 +15,9 @@ public class GenerateTestsCommand : ICommandSpec {
       SequenceLengthLimit,
       Target,
       TestInlineDepth,
-      BoogieOptionBag.BoogieArguments,
       BoogieOptionBag.SolverLog,
       BoogieOptionBag.SolverOption,
       BoogieOptionBag.SolverPath,
-      BoogieOptionBag.SolverPlugin,
       BoogieOptionBag.SolverResourceLimit,
       BoogieOptionBag.VerificationTimeLimit,
       Verbose,
diff --git a/Source/DafnyTestGeneration/ProgramModification.cs b/Source/DafnyTestGeneration/ProgramModification.cs
index a8aaf4949e5..68bdf4b04f4 100644
--- a/Source/DafnyTestGeneration/ProgramModification.cs
+++ b/Source/DafnyTestGeneration/ProgramModification.cs
@@ -77,8 +77,8 @@ private static DafnyOptions SetupOptions(DafnyOptions original, string procedure
       options.ErrorTrace = 1;
       options.EnhancedErrorMessages = 1;
       options.ModelViewFile = "-";
-      var proverOptions = new SMTLibSolverOptions(options);
-      proverOptions.Parse(options.ProverOptions);
+      var proverOptions = new SMTLibSolverOptions(original);
+      proverOptions.Parse(original.ProverOptions);
       var z3Version = DafnyOptions.GetZ3Version(proverOptions.ProverPath);
       options.ProverOptions = new List<string>() {
         "O:model_evaluator.completion=true",
@@ -89,7 +89,9 @@ private static DafnyOptions SetupOptions(DafnyOptions original, string procedure
       } else {
         options.ProverOptions.Insert(0, "O:model.compact=false");
       }
-
+      options.ResourceLimit = original.ResourceLimit;
+      options.ProverLogFilePath = original.ProverLogFilePath;
+      options.ProverLogFileAppend = original.ProverLogFileAppend;
       options.Prune = !original.TestGenOptions.DisablePrune;
       options.ProverOptions.AddRange(original.ProverOptions);
       options.LoopUnrollCount = original.LoopUnrollCount;

From c78a52f9b85963514d6e98aa5435a8353f584fad Mon Sep 17 00:00:00 2001
From: Dargones <sasha.fedchin@gmail.com>
Date: Thu, 4 May 2023 14:44:07 -0400
Subject: [PATCH 2/8] Fix prover lookup

---
 Source/DafnyTestGeneration/Main.cs             |  2 ++
 .../DafnyTestGeneration/ProgramModification.cs | 18 +++---------------
 Source/DafnyTestGeneration/Utils.cs            | 17 +++++++++++++++++
 3 files changed, 22 insertions(+), 15 deletions(-)

diff --git a/Source/DafnyTestGeneration/Main.cs b/Source/DafnyTestGeneration/Main.cs
index 75dbc8ce112..bb8f1746731 100644
--- a/Source/DafnyTestGeneration/Main.cs
+++ b/Source/DafnyTestGeneration/Main.cs
@@ -25,6 +25,7 @@ public static async IAsyncEnumerable<string> GetDeadCodeStatistics(Program progr
       program.Reporter.Options.PrintMode = PrintModes.Everything;
 
       var cache = new Modifications();
+      Utils.SetProverOptionsBasedOnZ3Version(program.Options);
       var modifications = GetModifications(cache, program).ToList();
       var blocksReached = modifications.Count;
       HashSet<string> allStates = new();
@@ -115,6 +116,7 @@ public static async IAsyncEnumerable<TestMethod> GetTestMethodsForProgram(Progra
       // Generate tests based on counterexamples produced from modifications
 
       var cache = new Modifications();
+      Utils.SetProverOptionsBasedOnZ3Version(program.Options);
       var programModifications = GetModifications(cache, program).ToList();
       foreach (var modification in programModifications) {
 
diff --git a/Source/DafnyTestGeneration/ProgramModification.cs b/Source/DafnyTestGeneration/ProgramModification.cs
index 68bdf4b04f4..059423d50c3 100644
--- a/Source/DafnyTestGeneration/ProgramModification.cs
+++ b/Source/DafnyTestGeneration/ProgramModification.cs
@@ -70,30 +70,18 @@ public ProgramModification(DafnyOptions options, Program program, Implementation
     /// options.Parse() on a new DafnyObject.
     /// </summary>
     private static DafnyOptions SetupOptions(DafnyOptions original, string procedure) {
-      var options = DafnyOptions.Create();
-      options.Parse(new[] { "/proc:" + procedure });
+      var options = DafnyOptions.Create(new[] { "/proc:" + procedure });
+      options.ProverOptions.Clear();
+      options.ProverOptions.AddRange(original.ProverOptions);
       options.NormalizeNames = false;
       options.EmitDebugInformation = true;
       options.ErrorTrace = 1;
       options.EnhancedErrorMessages = 1;
       options.ModelViewFile = "-";
-      var proverOptions = new SMTLibSolverOptions(original);
-      proverOptions.Parse(original.ProverOptions);
-      var z3Version = DafnyOptions.GetZ3Version(proverOptions.ProverPath);
-      options.ProverOptions = new List<string>() {
-        "O:model_evaluator.completion=true",
-        "O:model.completion=true"
-      };
-      if (z3Version is null || z3Version < new Version(4, 8, 6)) {
-        options.ProverOptions.Insert(0, "O:model.compress=false");
-      } else {
-        options.ProverOptions.Insert(0, "O:model.compact=false");
-      }
       options.ResourceLimit = original.ResourceLimit;
       options.ProverLogFilePath = original.ProverLogFilePath;
       options.ProverLogFileAppend = original.ProverLogFileAppend;
       options.Prune = !original.TestGenOptions.DisablePrune;
-      options.ProverOptions.AddRange(original.ProverOptions);
       options.LoopUnrollCount = original.LoopUnrollCount;
       options.DefiniteAssignmentLevel = original.DefiniteAssignmentLevel;
       options.WarnShadowing = original.WarnShadowing;
diff --git a/Source/DafnyTestGeneration/Utils.cs b/Source/DafnyTestGeneration/Utils.cs
index 7809ae8bead..e0c8e141598 100644
--- a/Source/DafnyTestGeneration/Utils.cs
+++ b/Source/DafnyTestGeneration/Utils.cs
@@ -1,9 +1,11 @@
 #nullable disable
+using System;
 using System.Collections.Generic;
 using System.IO;
 using System.Linq;
 using DafnyServer.CounterexampleGeneration;
 using Microsoft.Boogie;
+using Microsoft.Boogie.SMTLib;
 using Microsoft.Dafny;
 using Errors = Microsoft.Dafny.Errors;
 using Function = Microsoft.Dafny.Function;
@@ -16,6 +18,21 @@ namespace DafnyTestGeneration {
 
   public static class Utils {
 
+    public static void SetProverOptionsBasedOnZ3Version(DafnyOptions options) {
+      var proverOptions = new SMTLibSolverOptions(options);
+      proverOptions.Parse(options.ProverOptions);
+      var z3Version = DafnyOptions.GetZ3Version(proverOptions.ProverPath);
+      options.ProverOptions.AddRange(new List<string>() {
+        "O:model_evaluator.completion=true",
+        "O:model.completion=true"
+      });
+      if (z3Version is null || z3Version < new Version(4, 8, 6)) {
+        options.ProverOptions.Insert(0, "O:model_compress=false");
+      } else {
+        options.ProverOptions.Insert(0, "O:model.compact=false");
+      }
+    }
+
     /// <summary>
     /// Call Translator with larger stack to prevent stack overflow
     /// </summary>

From 06ee8e442de3b844dc6295ea0432584724e6336a Mon Sep 17 00:00:00 2001
From: Dargones <sasha.fedchin@gmail.com>
Date: Thu, 4 May 2023 15:20:30 -0400
Subject: [PATCH 3/8] remove redundant import

---
 Source/DafnyTestGeneration/GenerateTestsCommand.cs | 1 -
 1 file changed, 1 deletion(-)

diff --git a/Source/DafnyTestGeneration/GenerateTestsCommand.cs b/Source/DafnyTestGeneration/GenerateTestsCommand.cs
index 3aa40c5cac3..e3348f929bf 100644
--- a/Source/DafnyTestGeneration/GenerateTestsCommand.cs
+++ b/Source/DafnyTestGeneration/GenerateTestsCommand.cs
@@ -4,7 +4,6 @@
 using System.CommandLine.Invocation;
 using System.Linq;
 using DafnyCore;
-using Microsoft.Boogie.SMTLib;
 
 namespace Microsoft.Dafny;
 

From 70a479083e5f6792f0e4f96c2de5dd6239de6c09 Mon Sep 17 00:00:00 2001
From: Dargones <sasha.fedchin@gmail.com>
Date: Thu, 4 May 2023 16:01:27 -0400
Subject: [PATCH 4/8] Move copy method to GenerateTestsCommand to make future
 changes easier

---
 Source/DafnyTestGeneration/DeadCodeCommand.cs |  5 ++
 .../GenerateTestsCommand.cs                   | 46 +++++++++++++++++++
 Source/DafnyTestGeneration/Main.cs            |  2 -
 .../ProgramModification.cs                    | 42 +++++++++--------
 Source/DafnyTestGeneration/Utils.cs           | 15 ------
 5 files changed, 74 insertions(+), 36 deletions(-)

diff --git a/Source/DafnyTestGeneration/DeadCodeCommand.cs b/Source/DafnyTestGeneration/DeadCodeCommand.cs
index e8fe0788bfc..22a9c2c40ce 100644
--- a/Source/DafnyTestGeneration/DeadCodeCommand.cs
+++ b/Source/DafnyTestGeneration/DeadCodeCommand.cs
@@ -8,6 +8,8 @@ namespace Microsoft.Dafny;
 public class DeadCodeCommand : ICommandSpec {
   public IEnumerable<Option> Options =>
     new Option[] {
+      // IMPORTANT: Before adding new options, make sure they are
+      // appropriately copied over in the GenerateTestCommand.CopyForProcedure method 
       GenerateTestsCommand.LoopUnroll,
       GenerateTestsCommand.SequenceLengthLimit,
       BoogieOptionBag.SolverLog,
@@ -25,12 +27,15 @@ public Command Create() {
   }
 
   public void PostProcess(DafnyOptions dafnyOptions, Options options, InvocationContext context) {
+    // IMPORTANT: Before adding new default options, make sure they are
+    // appropriately copied over in the GenerateTestCommand.CopyForProcedure method 
     dafnyOptions.Compile = true;
     dafnyOptions.RunAfterCompile = false;
     dafnyOptions.ForceCompile = false;
     dafnyOptions.CompileVerbose = false;
     dafnyOptions.ForbidNondeterminism = true;
     dafnyOptions.DefiniteAssignmentLevel = 2;
+    dafnyOptions.WarnShadowing = true;
 
     dafnyOptions.TestGenOptions.Mode = TestGenerationOptions.Modes.Block;
     dafnyOptions.TestGenOptions.WarnDeadCode = true;
diff --git a/Source/DafnyTestGeneration/GenerateTestsCommand.cs b/Source/DafnyTestGeneration/GenerateTestsCommand.cs
index e3348f929bf..c8c2c9bcb27 100644
--- a/Source/DafnyTestGeneration/GenerateTestsCommand.cs
+++ b/Source/DafnyTestGeneration/GenerateTestsCommand.cs
@@ -10,6 +10,8 @@ namespace Microsoft.Dafny;
 public class GenerateTestsCommand : ICommandSpec {
   public IEnumerable<Option> Options =>
     new Option[] {
+      // IMPORTANT: Before adding new options, make sure they are
+      // appropriately copied over in the CopyForProcedure method below
       LoopUnroll,
       SequenceLengthLimit,
       Target,
@@ -30,6 +32,47 @@ private enum Mode {
     Block
   }
 
+  /// <summary>
+  /// Return the copy of a given DafnyOption instance that (for the purposes
+  /// of test generation) is identical to the <param name="options"></param>
+  /// parameter in everything except the value of the ProcsToCheck field that
+  /// determines the procedures to be verified and should be set to the value of
+  /// the <param name="procedureToVerify"></param> parameter.
+  /// </summary>
+  internal static DafnyOptions CopyForProcedure(DafnyOptions options, string procedureToVerify) {
+    var copy = DafnyOptions.Create(new[] { "/proc:" + procedureToVerify });
+    // Options set by the user:
+    copy.LoopUnrollCount = options.LoopUnrollCount;
+    copy.TestGenOptions.SeqLengthLimit = options.TestGenOptions.SeqLengthLimit;
+    copy.TestGenOptions.TargetMethod = options.TestGenOptions.TargetMethod;
+    copy.TestGenOptions.TestInlineDepth = options.TestGenOptions.TestInlineDepth;
+    copy.ProverLogFilePath = options.ProverLogFilePath;
+    copy.ProverLogFileAppend = options.ProverLogFileAppend;
+    copy.ProverOptions.Clear();
+    copy.ProverOptions.AddRange(options.ProverOptions);
+    copy.ResourceLimit = options.ResourceLimit;
+    copy.TimeLimit = options.TimeLimit;
+    copy.TestGenOptions.Verbose = options.TestGenOptions.Verbose;
+    copy.TestGenOptions.PrintBpl = options.TestGenOptions.PrintBpl;
+    copy.TestGenOptions.DisablePrune = options.TestGenOptions.DisablePrune;
+    copy.Prune = !options.TestGenOptions.DisablePrune;
+    // Options set by default in PostProcess:
+    copy.CompilerName = options.CompilerName;
+    copy.Compile = options.Compile;
+    copy.RunAfterCompile = options.RunAfterCompile;
+    copy.ForceCompile = options.ForceCompile;
+    copy.CompileVerbose = options.CompileVerbose;
+    copy.DeprecationNoise = options.DeprecationNoise;
+    copy.ForbidNondeterminism = options.ForbidNondeterminism;
+    copy.DefiniteAssignmentLevel = options.DefiniteAssignmentLevel;
+    copy.WarnShadowing = options.WarnShadowing;
+    copy.TestGenOptions.Mode = options.TestGenOptions.Mode;
+    copy.TestGenOptions.WarnDeadCode = options.TestGenOptions.WarnDeadCode;
+    // Options that may be modified by Test Generation itself:
+    copy.VerifyAllModules = options.VerifyAllModules;
+    return copy;
+  }
+
   private readonly Argument<Mode> modeArgument = new("mode", @"
 block - Prints block-coverage tests for the given program.
 path - Prints path-coverage tests for the given program.");
@@ -42,6 +85,8 @@ public Command Create() {
   }
 
   public void PostProcess(DafnyOptions dafnyOptions, Options options, InvocationContext context) {
+    // IMPORTANT: Before adding new default options, make sure they are
+    // appropriately copied over in the CopyForProcedure method above
     dafnyOptions.CompilerName = "cs";
     dafnyOptions.Compile = true;
     dafnyOptions.RunAfterCompile = false;
@@ -50,6 +95,7 @@ public void PostProcess(DafnyOptions dafnyOptions, Options options, InvocationCo
     dafnyOptions.DeprecationNoise = 0;
     dafnyOptions.ForbidNondeterminism = true;
     dafnyOptions.DefiniteAssignmentLevel = 2;
+    dafnyOptions.WarnShadowing = true;
 
     var mode = context.ParseResult.GetValueForArgument(modeArgument);
     dafnyOptions.TestGenOptions.Mode = mode switch {
diff --git a/Source/DafnyTestGeneration/Main.cs b/Source/DafnyTestGeneration/Main.cs
index bb8f1746731..75dbc8ce112 100644
--- a/Source/DafnyTestGeneration/Main.cs
+++ b/Source/DafnyTestGeneration/Main.cs
@@ -25,7 +25,6 @@ public static async IAsyncEnumerable<string> GetDeadCodeStatistics(Program progr
       program.Reporter.Options.PrintMode = PrintModes.Everything;
 
       var cache = new Modifications();
-      Utils.SetProverOptionsBasedOnZ3Version(program.Options);
       var modifications = GetModifications(cache, program).ToList();
       var blocksReached = modifications.Count;
       HashSet<string> allStates = new();
@@ -116,7 +115,6 @@ public static async IAsyncEnumerable<TestMethod> GetTestMethodsForProgram(Progra
       // Generate tests based on counterexamples produced from modifications
 
       var cache = new Modifications();
-      Utils.SetProverOptionsBasedOnZ3Version(program.Options);
       var programModifications = GetModifications(cache, program).ToList();
       foreach (var modification in programModifications) {
 
diff --git a/Source/DafnyTestGeneration/ProgramModification.cs b/Source/DafnyTestGeneration/ProgramModification.cs
index 059423d50c3..f50efde0ec3 100644
--- a/Source/DafnyTestGeneration/ProgramModification.cs
+++ b/Source/DafnyTestGeneration/ProgramModification.cs
@@ -64,30 +64,33 @@ public ProgramModification(DafnyOptions options, Program program, Implementation
     }
 
     /// <summary>
-    /// Setup CommandLineArguments to prepare verification. This is necessary
-    /// because the procsToCheck field in CommandLineOptions (part of Boogie)
-    /// is private meaning that the only way of setting this field is by calling
-    /// options.Parse() on a new DafnyObject.
+    /// Setup DafnyOptions to prepare for counterexample extraction
     /// </summary>
-    private static DafnyOptions SetupOptions(DafnyOptions original, string procedure) {
-      var options = DafnyOptions.Create(new[] { "/proc:" + procedure });
-      options.ProverOptions.Clear();
-      options.ProverOptions.AddRange(original.ProverOptions);
+    private static void SetupForCounterexamples(DafnyOptions options) {
+      // Figure out the Z3 version in use:
+      var proverOptions = new SMTLibSolverOptions(options);
+      proverOptions.Parse(options.ProverOptions);
+      var z3Version = DafnyOptions.GetZ3Version(proverOptions.ProverPath);
+      // Based on Z3 version, determine the options to use:
+      var optionsToAdd = new List<string>() {
+        "O:model_evaluator.completion=true",
+        "O:model.completion=true"
+      };
+      if (z3Version is null || z3Version < new Version(4, 8, 6)) {
+        optionsToAdd.Add("O:model_compress=false");
+      } else {
+        optionsToAdd.Add("O:model.compact=false");
+      }
+      // (Re)set the options necessary for counterexample extraction:
+      foreach (var option in optionsToAdd) {
+        options.ProverOptions.RemoveAll(o => o.Split("=") == option.Split("="));
+        options.ProverOptions.Add(option);
+      }
       options.NormalizeNames = false;
       options.EmitDebugInformation = true;
       options.ErrorTrace = 1;
       options.EnhancedErrorMessages = 1;
       options.ModelViewFile = "-";
-      options.ResourceLimit = original.ResourceLimit;
-      options.ProverLogFilePath = original.ProverLogFilePath;
-      options.ProverLogFileAppend = original.ProverLogFileAppend;
-      options.Prune = !original.TestGenOptions.DisablePrune;
-      options.LoopUnrollCount = original.LoopUnrollCount;
-      options.DefiniteAssignmentLevel = original.DefiniteAssignmentLevel;
-      options.WarnShadowing = original.WarnShadowing;
-      options.VerifyAllModules = original.VerifyAllModules;
-      options.TimeLimit = original.TimeLimit;
-      return options;
     }
 
     /// <summary>
@@ -100,7 +103,8 @@ private static DafnyOptions SetupOptions(DafnyOptions original, string procedure
           (coversBlocks.Count != 0 && IsCovered(cache))) {
         return counterexampleLog;
       }
-      var options = SetupOptions(Options, procedure);
+      var options = GenerateTestsCommand.CopyForProcedure(Options, procedure);
+      SetupForCounterexamples(options);
       var engine = ExecutionEngine.CreateWithoutSharedCache(options);
       var guid = Guid.NewGuid().ToString();
       program.Resolve(options);
diff --git a/Source/DafnyTestGeneration/Utils.cs b/Source/DafnyTestGeneration/Utils.cs
index e0c8e141598..8cd3fe73a6a 100644
--- a/Source/DafnyTestGeneration/Utils.cs
+++ b/Source/DafnyTestGeneration/Utils.cs
@@ -18,21 +18,6 @@ namespace DafnyTestGeneration {
 
   public static class Utils {
 
-    public static void SetProverOptionsBasedOnZ3Version(DafnyOptions options) {
-      var proverOptions = new SMTLibSolverOptions(options);
-      proverOptions.Parse(options.ProverOptions);
-      var z3Version = DafnyOptions.GetZ3Version(proverOptions.ProverPath);
-      options.ProverOptions.AddRange(new List<string>() {
-        "O:model_evaluator.completion=true",
-        "O:model.completion=true"
-      });
-      if (z3Version is null || z3Version < new Version(4, 8, 6)) {
-        options.ProverOptions.Insert(0, "O:model_compress=false");
-      } else {
-        options.ProverOptions.Insert(0, "O:model.compact=false");
-      }
-    }
-
     /// <summary>
     /// Call Translator with larger stack to prevent stack overflow
     /// </summary>

From 4f2c5cc6461a3491111109822aed67933afbdba8 Mon Sep 17 00:00:00 2001
From: Dargones <sasha.fedchin@gmail.com>
Date: Thu, 4 May 2023 16:02:55 -0400
Subject: [PATCH 5/8] Remove unused imports

---
 Source/DafnyTestGeneration/Utils.cs | 2 --
 1 file changed, 2 deletions(-)

diff --git a/Source/DafnyTestGeneration/Utils.cs b/Source/DafnyTestGeneration/Utils.cs
index 8cd3fe73a6a..7809ae8bead 100644
--- a/Source/DafnyTestGeneration/Utils.cs
+++ b/Source/DafnyTestGeneration/Utils.cs
@@ -1,11 +1,9 @@
 #nullable disable
-using System;
 using System.Collections.Generic;
 using System.IO;
 using System.Linq;
 using DafnyServer.CounterexampleGeneration;
 using Microsoft.Boogie;
-using Microsoft.Boogie.SMTLib;
 using Microsoft.Dafny;
 using Errors = Microsoft.Dafny.Errors;
 using Function = Microsoft.Dafny.Function;

From da78f3001c556f4d4deeb1e19c6080840c815162 Mon Sep 17 00:00:00 2001
From: Dargones <sasha.fedchin@gmail.com>
Date: Thu, 4 May 2023 16:08:56 -0400
Subject: [PATCH 6/8] add clarification nnote

---
 Source/DafnyTestGeneration/GenerateTestsCommand.cs | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/Source/DafnyTestGeneration/GenerateTestsCommand.cs b/Source/DafnyTestGeneration/GenerateTestsCommand.cs
index c8c2c9bcb27..960041a0397 100644
--- a/Source/DafnyTestGeneration/GenerateTestsCommand.cs
+++ b/Source/DafnyTestGeneration/GenerateTestsCommand.cs
@@ -38,6 +38,8 @@ private enum Mode {
   /// parameter in everything except the value of the ProcsToCheck field that
   /// determines the procedures to be verified and should be set to the value of
   /// the <param name="procedureToVerify"></param> parameter.
+  /// Note that this cannot be refactored to yse the DafnyOptions.CopyTo method
+  /// because we have to modify ProcsToCheck list, which does not have a setter.
   /// </summary>
   internal static DafnyOptions CopyForProcedure(DafnyOptions options, string procedureToVerify) {
     var copy = DafnyOptions.Create(new[] { "/proc:" + procedureToVerify });

From d423d1cb7996ce516616246075e4a309e7b2dd2e Mon Sep 17 00:00:00 2001
From: Dargones <sasha.fedchin@gmail.com>
Date: Thu, 4 May 2023 16:16:07 -0400
Subject: [PATCH 7/8] Remove an unused option

---
 Source/DafnyTestGeneration/DeadCodeCommand.cs      | 1 -
 Source/DafnyTestGeneration/GenerateTestsCommand.cs | 2 --
 2 files changed, 3 deletions(-)

diff --git a/Source/DafnyTestGeneration/DeadCodeCommand.cs b/Source/DafnyTestGeneration/DeadCodeCommand.cs
index 22a9c2c40ce..78102592084 100644
--- a/Source/DafnyTestGeneration/DeadCodeCommand.cs
+++ b/Source/DafnyTestGeneration/DeadCodeCommand.cs
@@ -35,7 +35,6 @@ public void PostProcess(DafnyOptions dafnyOptions, Options options, InvocationCo
     dafnyOptions.CompileVerbose = false;
     dafnyOptions.ForbidNondeterminism = true;
     dafnyOptions.DefiniteAssignmentLevel = 2;
-    dafnyOptions.WarnShadowing = true;
 
     dafnyOptions.TestGenOptions.Mode = TestGenerationOptions.Modes.Block;
     dafnyOptions.TestGenOptions.WarnDeadCode = true;
diff --git a/Source/DafnyTestGeneration/GenerateTestsCommand.cs b/Source/DafnyTestGeneration/GenerateTestsCommand.cs
index 960041a0397..6135bce9d59 100644
--- a/Source/DafnyTestGeneration/GenerateTestsCommand.cs
+++ b/Source/DafnyTestGeneration/GenerateTestsCommand.cs
@@ -67,7 +67,6 @@ internal static DafnyOptions CopyForProcedure(DafnyOptions options, string proce
     copy.DeprecationNoise = options.DeprecationNoise;
     copy.ForbidNondeterminism = options.ForbidNondeterminism;
     copy.DefiniteAssignmentLevel = options.DefiniteAssignmentLevel;
-    copy.WarnShadowing = options.WarnShadowing;
     copy.TestGenOptions.Mode = options.TestGenOptions.Mode;
     copy.TestGenOptions.WarnDeadCode = options.TestGenOptions.WarnDeadCode;
     // Options that may be modified by Test Generation itself:
@@ -97,7 +96,6 @@ public void PostProcess(DafnyOptions dafnyOptions, Options options, InvocationCo
     dafnyOptions.DeprecationNoise = 0;
     dafnyOptions.ForbidNondeterminism = true;
     dafnyOptions.DefiniteAssignmentLevel = 2;
-    dafnyOptions.WarnShadowing = true;
 
     var mode = context.ParseResult.GetValueForArgument(modeArgument);
     dafnyOptions.TestGenOptions.Mode = mode switch {

From 43a40e561a086f71af927fa24f8feaa7ffd49a28 Mon Sep 17 00:00:00 2001
From: Dargones <sasha.fedchin@gmail.com>
Date: Thu, 4 May 2023 16:18:16 -0400
Subject: [PATCH 8/8] Fix typos

---
 Source/DafnyTestGeneration/GenerateTestsCommand.cs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Source/DafnyTestGeneration/GenerateTestsCommand.cs b/Source/DafnyTestGeneration/GenerateTestsCommand.cs
index 6135bce9d59..0bd8f75f9f3 100644
--- a/Source/DafnyTestGeneration/GenerateTestsCommand.cs
+++ b/Source/DafnyTestGeneration/GenerateTestsCommand.cs
@@ -33,12 +33,12 @@ private enum Mode {
   }
 
   /// <summary>
-  /// Return the copy of a given DafnyOption instance that (for the purposes
+  /// Return a copy of the given DafnyOption instance that (for the purposes
   /// of test generation) is identical to the <param name="options"></param>
   /// parameter in everything except the value of the ProcsToCheck field that
   /// determines the procedures to be verified and should be set to the value of
   /// the <param name="procedureToVerify"></param> parameter.
-  /// Note that this cannot be refactored to yse the DafnyOptions.CopyTo method
+  /// Note that this cannot be refactored to use the DafnyOptions.CopyTo method
   /// because we have to modify ProcsToCheck list, which does not have a setter.
   /// </summary>
   internal static DafnyOptions CopyForProcedure(DafnyOptions options, string procedureToVerify) {