Make Test Generation work with a custom Z3 version

Source/DafnyTestGeneration/DeadCodeCommand.cs

@@ -8,13 +8,13 @@ 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.BoogieArguments,
       BoogieOptionBag.SolverLog,
       BoogieOptionBag.SolverOption,
       BoogieOptionBag.SolverPath,
-      BoogieOptionBag.SolverPlugin,
       BoogieOptionBag.SolverResourceLimit,
       BoogieOptionBag.VerificationTimeLimit
     }.Concat(ICommandSpec.ConsoleOutputOptions).
@@ -27,6 +27,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 GenerateTestCommand.CopyForProcedure method 
     dafnyOptions.Compile = true;
     dafnyOptions.RunAfterCompile = false;
     dafnyOptions.ForceCompile = false;

Source/DafnyTestGeneration/GenerateTestsCommand.cs

@@ -10,15 +10,15 @@ 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,
       TestInlineDepth,
-      BoogieOptionBag.BoogieArguments,
       BoogieOptionBag.SolverLog,
       BoogieOptionBag.SolverOption,
       BoogieOptionBag.SolverPath,
-      BoogieOptionBag.SolverPlugin,
       BoogieOptionBag.SolverResourceLimit,
       BoogieOptionBag.VerificationTimeLimit,
       Verbose,
@@ -32,6 +32,48 @@ private enum Mode {
     Block
   }
 
+  /// <summary>
+  /// 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 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) {
+    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.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.");
@@ -44,6 +86,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;

Source/DafnyTestGeneration/ProgramModification.cs

@@ -64,40 +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();
-      options.Parse(new[] { "/proc:" + procedure });
-      options.NormalizeNames = false;
-      options.EmitDebugInformation = true;
-      options.ErrorTrace = 1;
-      options.EnhancedErrorMessages = 1;
-      options.ModelViewFile = "-";
+    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);
-      options.ProverOptions = new List<string>() {
+      // 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)) {
-        options.ProverOptions.Insert(0, "O:model.compress=false");
+        optionsToAdd.Add("O:model_compress=false");
       } else {
-        options.ProverOptions.Insert(0, "O:model.compact=false");
+        optionsToAdd.Add("O:model.compact=false");
       }
-
-      options.Prune = !original.TestGenOptions.DisablePrune;
-      options.ProverOptions.AddRange(original.ProverOptions);
-      options.LoopUnrollCount = original.LoopUnrollCount;
-      options.DefiniteAssignmentLevel = original.DefiniteAssignmentLevel;
-      options.WarnShadowing = original.WarnShadowing;
-      options.VerifyAllModules = original.VerifyAllModules;
-      options.TimeLimit = original.TimeLimit;
-      return options;
+      // (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 = "-";
     }
 
     /// <summary>
@@ -110,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);