From 3dbf68f78caab17d64621dc3b204d23eabbfa45c Mon Sep 17 00:00:00 2001
From: Mikael Mayer <mimayere@amazon.com>
Date: Wed, 22 Jan 2025 13:06:23 -0600
Subject: [PATCH 1/4] Chore: Support for `--do-boogie-translation` And not
 activated by default if `--no-verify` is set. This option emulates the
 `/dafnyVerify` command in the previous CLI Added tests

---
 Source/DafnyCore/Options/BoogieOptionBag.cs | 14 +++-
 Source/DafnyCore/Options/DafnyCommands.cs   |  1 +
 Source/DafnyDriver.Test/OptionsTest.cs      | 72 +++++++++++++++++++++
 Source/DafnyDriver/Commands/RunCommand.cs   |  6 +-
 Source/DafnyDriver/DafnyNewCli.cs           |  6 +-
 Source/DafnyDriver/WritersConsole.cs        |  2 +-
 docs/DafnyRef/UserGuide.md                  |  2 +
 7 files changed, 96 insertions(+), 7 deletions(-)
 create mode 100644 Source/DafnyDriver.Test/OptionsTest.cs

diff --git a/Source/DafnyCore/Options/BoogieOptionBag.cs b/Source/DafnyCore/Options/BoogieOptionBag.cs
index 59ffe8bfcbe..4d7a1302fef 100644
--- a/Source/DafnyCore/Options/BoogieOptionBag.cs
+++ b/Source/DafnyCore/Options/BoogieOptionBag.cs
@@ -46,6 +46,8 @@ public static class BoogieOptionBag {
 
   public static readonly Option<bool> NoVerify = new("--no-verify", "Skip verification");
 
+  public static readonly Option<bool> DoBoogieTranslation = new("--do-boogie-translation", "Requires --no-verify. Does translation to Boogie but Boogie won't verify it.");
+
   public static readonly Option<bool> HiddenNoVerify = new("--hidden-no-verify",
     "Allows building unverified libraries without recording that they were not verified.") {
     IsHidden = true
@@ -107,9 +109,14 @@ static BoogieOptionBag() {
     });
     DafnyOptions.RegisterLegacyBinding(Cores,
       (o, f) => o.VcsCores = f == 0 ? (1 + System.Environment.ProcessorCount) / 2 : (int)f);
-    DafnyOptions.RegisterLegacyBinding(NoVerify, (options, value) => {
-      var shouldVerify = !value && !options.Get(HiddenNoVerify);
-      options.Verify = shouldVerify;
+    DafnyOptions.RegisterLegacyBinding(NoVerify, (options, dotNotVerify) => {
+      var shouldVerify = !dotNotVerify && !options.Get(HiddenNoVerify);
+      options.Verify = shouldVerify; // Boogie won't verify
+    });
+    // Previously /dafnyVerify
+    DafnyOptions.RegisterLegacyBinding(DoBoogieTranslation, (options, doBoogieTranslation) => {
+      options.DafnyVerify = (!options.Get(NoVerify) && !options.Get(HiddenNoVerify))
+        || doBoogieTranslation || options.Get(DeveloperOptionBag.BoogiePrint) != null; // Dafny won't translate the code to Boogie
     });
     DafnyOptions.RegisterLegacyBinding(VerificationTimeLimit, (o, f) => o.TimeLimit = f);
 
@@ -144,6 +151,7 @@ static BoogieOptionBag() {
 
     OptionRegistry.RegisterGlobalOption(BoogieArguments, OptionCompatibility.CheckOptionMatches);
     OptionRegistry.RegisterGlobalOption(NoVerify, OptionCompatibility.OptionLibraryImpliesLocalError);
+    OptionRegistry.RegisterGlobalOption(DoBoogieTranslation, OptionCompatibility.OptionLibraryImpliesLocalError);
     OptionRegistry.RegisterOption(HiddenNoVerify, OptionScope.Cli);
     OptionRegistry.RegisterOption(Cores, OptionScope.Cli);
     OptionRegistry.RegisterOption(VerificationTimeLimit, OptionScope.Cli);
diff --git a/Source/DafnyCore/Options/DafnyCommands.cs b/Source/DafnyCore/Options/DafnyCommands.cs
index 3f8c281c9ce..6dee61a1c40 100644
--- a/Source/DafnyCore/Options/DafnyCommands.cs
+++ b/Source/DafnyCore/Options/DafnyCommands.cs
@@ -52,6 +52,7 @@ static DafnyCommands() {
 
   public static readonly IReadOnlyList<Option> TranslationOptions = new Option[] {
     BoogieOptionBag.NoVerify,
+    BoogieOptionBag.DoBoogieTranslation,
     BoogieOptionBag.HiddenNoVerify,
     CommonOptionBag.OptimizeErasableDatatypeWrapper,
     CommonOptionBag.TestAssumptions,
diff --git a/Source/DafnyDriver.Test/OptionsTest.cs b/Source/DafnyDriver.Test/OptionsTest.cs
new file mode 100644
index 00000000000..9f4fe25ff10
--- /dev/null
+++ b/Source/DafnyDriver.Test/OptionsTest.cs
@@ -0,0 +1,72 @@
+using System.CommandLine;
+using System.CommandLine.Builder;
+using System.CommandLine.Invocation;
+using System.CommandLine.Parsing;
+using System.Diagnostics;
+using System.IO.Pipelines;
+using System.Reactive.Concurrency;
+using System.Reflection;
+using System.Text;
+using Microsoft.Dafny;
+using Microsoft.Extensions.Logging.Abstractions;
+using OmniSharp.Extensions.JsonRpc;
+using OmniSharp.Extensions.JsonRpc.Client;
+using OmniSharp.Extensions.JsonRpc.Serialization;
+using OmniSharp.Extensions.LanguageServer.Protocol.Client.Capabilities;
+using OmniSharp.Extensions.LanguageServer.Protocol.Models;
+using XunitAssertMessages;
+using Command = System.CommandLine.Command;
+
+namespace DafnyDriver.Test;
+
+
+public class OptionsTest {
+  [Fact]
+  public async Task RunFlagsOverride() {
+    await TestCliRunArgs([], options => {
+      Assert.True(options.DafnyVerify);
+      Assert.True(options.Verify);
+      return 0;
+    });
+    await TestCliRunArgs(["--no-verify"], options => {
+      Assert.False(options.DafnyVerify);
+      Assert.False(options.Verify);
+      return 0;
+    });
+    await TestCliRunArgs(["--no-verify", "--do-boogie-translation"], options => {
+      Assert.True(options.DafnyVerify);
+      Assert.False(options.Verify);
+      return 0;
+    });
+    await TestCliRunArgs(["--no-verify", "--bprint=-"], options => {
+      Assert.True(options.DafnyVerify);
+      Assert.False(options.Verify);
+      return 0;
+    });
+  }
+
+  private static async Task TestCliRunArgs(string[] cmdArgs, Func<DafnyOptions, int> optionsCallback) {
+    var fullArgs = new string[] {
+      "run"
+    };
+    fullArgs = fullArgs.Concat(cmdArgs).Concat(new string[] { "file.dfy" }).ToArray();
+    var callbackCalled = false;
+    var newOptionsCallback = (DafnyOptions options) => {
+      callbackCalled = true;
+      return optionsCallback(options);
+    };
+    Command cmd = RunCommand.Create(newOptionsCallback);
+    var rootCommand = new RootCommand("Test root command");
+    rootCommand.AddCommand(cmd);
+    var builder = new CommandLineBuilder(rootCommand).UseDefaults();
+    var parser = builder.Build();
+    TextReader inputReader = new StringReader("");
+    var outputWriter = new StringWriter();
+    var errorWriter = new StringWriter();
+    var console = new WritersConsole(inputReader, outputWriter, errorWriter);
+    var exitCode = await DafnyNewCli.ExecuteForParser(console, fullArgs, parser);
+    Assert.Equal<object>("", errorWriter.ToString());
+    Assert.Equal(0, exitCode);
+    Assert.True(callbackCalled);
+  }
+}
diff --git a/Source/DafnyDriver/Commands/RunCommand.cs b/Source/DafnyDriver/Commands/RunCommand.cs
index ce994f0d1bc..6fe26b9c1ae 100644
--- a/Source/DafnyDriver/Commands/RunCommand.cs
+++ b/Source/DafnyDriver/Commands/RunCommand.cs
@@ -49,7 +49,7 @@ static RunCommand() {
       Concat(DafnyCommands.ConsoleOutputOptions).
       Concat(DafnyCommands.ResolverOptions);
 
-  public static Command Create() {
+  public static Command Create(Func<DafnyOptions, int> continuation = null) {
     var result = new Command("run", "Run the program.");
     result.AddArgument(DafnyCommands.FileArgument);
     result.AddArgument(UserProgramArguments);
@@ -63,7 +63,9 @@ public static Command Create() {
       options.Compile = true;
       options.RunAfterCompile = true;
       options.ForceCompile = options.Get(BoogieOptionBag.NoVerify);
-
+      if (continuation != null) {
+        return continuation(options);
+      }
       return await SynchronousCliCompilation.Run(options);
     });
     return result;
diff --git a/Source/DafnyDriver/DafnyNewCli.cs b/Source/DafnyDriver/DafnyNewCli.cs
index ce476e9d98b..d38d84cd036 100644
--- a/Source/DafnyDriver/DafnyNewCli.cs
+++ b/Source/DafnyDriver/DafnyNewCli.cs
@@ -172,6 +172,10 @@ private static void ProcessOption(InvocationContext context, Option option, Dafn
   }
 
   public static Task<int> Execute(IConsole console, IReadOnlyList<string> arguments) {
+    return ExecuteForParser(console, arguments, Parser);
+  }
+
+  public static Task<int> ExecuteForParser(IConsole console, IReadOnlyList<string> arguments, System.CommandLine.Parsing.Parser parser) {
     foreach (var symbol in AllSymbols) {
       if (symbol is Option option) {
         if (!option.Arity.Equals(ArgumentArity.ZeroOrMore) && !option.Arity.Equals(ArgumentArity.OneOrMore)) {
@@ -180,7 +184,7 @@ public static Task<int> Execute(IConsole console, IReadOnlyList<string> argument
       }
     }
 
-    return Parser.InvokeAsync(arguments.ToArray(), console);
+    return parser.InvokeAsync(arguments.ToArray(), console);
   }
 
   private static readonly MethodInfo GetValueForOptionMethod;
diff --git a/Source/DafnyDriver/WritersConsole.cs b/Source/DafnyDriver/WritersConsole.cs
index 471f41dbc7f..1dba93bcb22 100644
--- a/Source/DafnyDriver/WritersConsole.cs
+++ b/Source/DafnyDriver/WritersConsole.cs
@@ -5,7 +5,7 @@
 
 namespace Microsoft.Dafny;
 
-class WritersConsole : IConsole {
+public class WritersConsole : IConsole {
   public TextReader InputWriter { get; }
   public TextWriter ErrWriter { get; }
   public TextWriter OutWriter { get; }
diff --git a/docs/DafnyRef/UserGuide.md b/docs/DafnyRef/UserGuide.md
index 8fd4ce1c5dc..372f1b3a04b 100644
--- a/docs/DafnyRef/UserGuide.md
+++ b/docs/DafnyRef/UserGuide.md
@@ -2294,6 +2294,8 @@ and what information it produces about the verification process.
 
 * `--no-verify` - turns off verification (for translate, build, run commands)
 
+* `--do-boogie-translation` - turns on translation to Boogie after resolving or if `--no-verify` is set. Automatically set if `--bprint` is set.
+
 * `--verify-included-files` (was `-verifyAllModules`) - verify modules that come from include directives.
 
   By default, Dafny only verifies files explicitly listed on the command

From 865aa96db7118174e496fbf32e8ab54f12947bb8 Mon Sep 17 00:00:00 2001
From: Mikael Mayer <mimayere@amazon.com>
Date: Thu, 23 Jan 2025 09:38:28 -0600
Subject: [PATCH 2/4] review comments

---
 Source/DafnyCore/Options/BoogieOptionBag.cs    | 9 +--------
 Source/DafnyCore/Options/DafnyCommands.cs      | 1 -
 Source/DafnyCore/Options/DeveloperOptionBag.cs | 2 +-
 Source/DafnyDriver.Test/OptionsTest.cs         | 5 -----
 4 files changed, 2 insertions(+), 15 deletions(-)

diff --git a/Source/DafnyCore/Options/BoogieOptionBag.cs b/Source/DafnyCore/Options/BoogieOptionBag.cs
index 4d7a1302fef..bef4f5355a7 100644
--- a/Source/DafnyCore/Options/BoogieOptionBag.cs
+++ b/Source/DafnyCore/Options/BoogieOptionBag.cs
@@ -46,8 +46,6 @@ public static class BoogieOptionBag {
 
   public static readonly Option<bool> NoVerify = new("--no-verify", "Skip verification");
 
-  public static readonly Option<bool> DoBoogieTranslation = new("--do-boogie-translation", "Requires --no-verify. Does translation to Boogie but Boogie won't verify it.");
-
   public static readonly Option<bool> HiddenNoVerify = new("--hidden-no-verify",
     "Allows building unverified libraries without recording that they were not verified.") {
     IsHidden = true
@@ -112,11 +110,7 @@ static BoogieOptionBag() {
     DafnyOptions.RegisterLegacyBinding(NoVerify, (options, dotNotVerify) => {
       var shouldVerify = !dotNotVerify && !options.Get(HiddenNoVerify);
       options.Verify = shouldVerify; // Boogie won't verify
-    });
-    // Previously /dafnyVerify
-    DafnyOptions.RegisterLegacyBinding(DoBoogieTranslation, (options, doBoogieTranslation) => {
-      options.DafnyVerify = (!options.Get(NoVerify) && !options.Get(HiddenNoVerify))
-        || doBoogieTranslation || options.Get(DeveloperOptionBag.BoogiePrint) != null; // Dafny won't translate the code to Boogie
+      options.DafnyVerify = shouldVerify || options.Get(DeveloperOptionBag.BoogiePrint) != null;
     });
     DafnyOptions.RegisterLegacyBinding(VerificationTimeLimit, (o, f) => o.TimeLimit = f);
 
@@ -151,7 +145,6 @@ static BoogieOptionBag() {
 
     OptionRegistry.RegisterGlobalOption(BoogieArguments, OptionCompatibility.CheckOptionMatches);
     OptionRegistry.RegisterGlobalOption(NoVerify, OptionCompatibility.OptionLibraryImpliesLocalError);
-    OptionRegistry.RegisterGlobalOption(DoBoogieTranslation, OptionCompatibility.OptionLibraryImpliesLocalError);
     OptionRegistry.RegisterOption(HiddenNoVerify, OptionScope.Cli);
     OptionRegistry.RegisterOption(Cores, OptionScope.Cli);
     OptionRegistry.RegisterOption(VerificationTimeLimit, OptionScope.Cli);
diff --git a/Source/DafnyCore/Options/DafnyCommands.cs b/Source/DafnyCore/Options/DafnyCommands.cs
index 6dee61a1c40..3f8c281c9ce 100644
--- a/Source/DafnyCore/Options/DafnyCommands.cs
+++ b/Source/DafnyCore/Options/DafnyCommands.cs
@@ -52,7 +52,6 @@ static DafnyCommands() {
 
   public static readonly IReadOnlyList<Option> TranslationOptions = new Option[] {
     BoogieOptionBag.NoVerify,
-    BoogieOptionBag.DoBoogieTranslation,
     BoogieOptionBag.HiddenNoVerify,
     CommonOptionBag.OptimizeErasableDatatypeWrapper,
     CommonOptionBag.TestAssumptions,
diff --git a/Source/DafnyCore/Options/DeveloperOptionBag.cs b/Source/DafnyCore/Options/DeveloperOptionBag.cs
index bff35feaa0b..94d8b88294a 100644
--- a/Source/DafnyCore/Options/DeveloperOptionBag.cs
+++ b/Source/DafnyCore/Options/DeveloperOptionBag.cs
@@ -21,7 +21,7 @@ Print passified Boogie program translated from Dafny
     IsHidden = true,
     ArgumentHelpName = "file",
   };
-
+  // This flag is the only one that can trigger /dafnyVerify in the new CLI and I think it's sufficient
   public static readonly Option<string> BoogiePrint = new("--bprint",
   @"
 Print Boogie program translated from Dafny
diff --git a/Source/DafnyDriver.Test/OptionsTest.cs b/Source/DafnyDriver.Test/OptionsTest.cs
index 9f4fe25ff10..c50ca4d60a2 100644
--- a/Source/DafnyDriver.Test/OptionsTest.cs
+++ b/Source/DafnyDriver.Test/OptionsTest.cs
@@ -33,11 +33,6 @@ await TestCliRunArgs(["--no-verify"], options => {
       Assert.False(options.Verify);
       return 0;
     });
-    await TestCliRunArgs(["--no-verify", "--do-boogie-translation"], options => {
-      Assert.True(options.DafnyVerify);
-      Assert.False(options.Verify);
-      return 0;
-    });
     await TestCliRunArgs(["--no-verify", "--bprint=-"], options => {
       Assert.True(options.DafnyVerify);
       Assert.False(options.Verify);

From 2e5d2c8dbc3bd673029306968c1c8610d2498acb Mon Sep 17 00:00:00 2001
From: Mikael Mayer <mimayere@amazon.com>
Date: Thu, 23 Jan 2025 10:48:27 -0600
Subject: [PATCH 3/4] Fixed the CI

---
 Source/DafnyCore/Options/BoogieOptionBag.cs   |  6 ++-
 Source/DafnyDriver.Test/OptionsTest.cs        | 10 ++++
 .../Legacy/SynchronousCliCompilation.cs       | 47 +++++++++++--------
 docs/DafnyRef/UserGuide.md                    |  2 -
 4 files changed, 43 insertions(+), 22 deletions(-)

diff --git a/Source/DafnyCore/Options/BoogieOptionBag.cs b/Source/DafnyCore/Options/BoogieOptionBag.cs
index bef4f5355a7..90d65d9af83 100644
--- a/Source/DafnyCore/Options/BoogieOptionBag.cs
+++ b/Source/DafnyCore/Options/BoogieOptionBag.cs
@@ -110,7 +110,11 @@ static BoogieOptionBag() {
     DafnyOptions.RegisterLegacyBinding(NoVerify, (options, dotNotVerify) => {
       var shouldVerify = !dotNotVerify && !options.Get(HiddenNoVerify);
       options.Verify = shouldVerify; // Boogie won't verify
-      options.DafnyVerify = shouldVerify || options.Get(DeveloperOptionBag.BoogiePrint) != null;
+      options.DafnyVerify =
+        shouldVerify ||
+        options.Get(DeveloperOptionBag.BoogiePrint) != null ||
+        options.Get(DeveloperOptionBag.SplitPrint) != null ||
+        options.Get(DeveloperOptionBag.PassivePrint) != null;
     });
     DafnyOptions.RegisterLegacyBinding(VerificationTimeLimit, (o, f) => o.TimeLimit = f);
 
diff --git a/Source/DafnyDriver.Test/OptionsTest.cs b/Source/DafnyDriver.Test/OptionsTest.cs
index c50ca4d60a2..e93c050f1e0 100644
--- a/Source/DafnyDriver.Test/OptionsTest.cs
+++ b/Source/DafnyDriver.Test/OptionsTest.cs
@@ -38,6 +38,16 @@ await TestCliRunArgs(["--no-verify", "--bprint=-"], options => {
       Assert.False(options.Verify);
       return 0;
     });
+    await TestCliRunArgs(["--no-verify", "--sprint=-"], options => {
+      Assert.True(options.DafnyVerify);
+      Assert.False(options.Verify);
+      return 0;
+    });
+    await TestCliRunArgs(["--no-verify", "--pprint=-"], options => {
+      Assert.True(options.DafnyVerify);
+      Assert.False(options.Verify);
+      return 0;
+    });
   }
 
   private static async Task TestCliRunArgs(string[] cmdArgs, Func<DafnyOptions, int> optionsCallback) {
diff --git a/Source/DafnyDriver/Legacy/SynchronousCliCompilation.cs b/Source/DafnyDriver/Legacy/SynchronousCliCompilation.cs
index 73c9270560c..281ec437a60 100644
--- a/Source/DafnyDriver/Legacy/SynchronousCliCompilation.cs
+++ b/Source/DafnyDriver/Legacy/SynchronousCliCompilation.cs
@@ -287,25 +287,34 @@ public async Task<ExitValue> ProcessFilesAsync(IReadOnlyList<DafnyFile/*!*/>/*!*
       if (err != null) {
         exitValue = ExitValue.DAFNY_ERROR;
         options.Printer.ErrorWriteLine(options.OutputWriter, err);
-      } else if (dafnyProgram != null && !options.NoResolve && !options.NoTypecheck
-          && options.DafnyVerify) {
-
-        dafnyProgram.ProofDependencyManager = depManager;
-        var boogiePrograms =
-          await DafnyMain.LargeStackFactory.StartNew(() => Translate(engine.Options, dafnyProgram).ToList());
-
-        string baseName = cce.NonNull(Path.GetFileName(dafnyFileNames[^1]));
-        var (verified, outcome, moduleStats) =
-          await BoogieAsync(dafnyProgram.Reporter, options, baseName, boogiePrograms, programId);
-
-        if (options.TrackVerificationCoverage) {
-          ProofDependencyWarnings.WarnAboutSuspiciousDependenciesUsingStoredPartialResults(options, dafnyProgram.Reporter, depManager);
-          var coverageReportDir = options.Get(CommonOptionBag.VerificationCoverageReport);
-          if (coverageReportDir != null) {
-            await new CoverageReporter(options).SerializeVerificationCoverageReport(
-              depManager, dafnyProgram,
-              boogiePrograms.SelectMany(tp => tp.Item2.AllCoveredElements),
-              coverageReportDir);
+      } else if (dafnyProgram != null && !options.NoResolve && !options.NoTypecheck) {
+
+        bool verified;
+        PipelineOutcome outcome;
+        IDictionary<string, PipelineStatistics> moduleStats;
+        if (!options.DafnyVerify) {
+          verified = false;
+          outcome = PipelineOutcome.Done;
+          moduleStats = new Dictionary<string, PipelineStatistics>();
+        } else {
+          dafnyProgram.ProofDependencyManager = depManager;
+          var boogiePrograms =
+            await DafnyMain.LargeStackFactory.StartNew(() => Translate(engine.Options, dafnyProgram).ToList());
+
+          string baseName = cce.NonNull(Path.GetFileName(dafnyFileNames[^1]));
+          (verified, outcome, moduleStats) =
+            await BoogieAsync(dafnyProgram.Reporter, options, baseName, boogiePrograms, programId);
+
+          if (options.TrackVerificationCoverage) {
+            ProofDependencyWarnings.WarnAboutSuspiciousDependenciesUsingStoredPartialResults(options,
+              dafnyProgram.Reporter, depManager);
+            var coverageReportDir = options.Get(CommonOptionBag.VerificationCoverageReport);
+            if (coverageReportDir != null) {
+              await new CoverageReporter(options).SerializeVerificationCoverageReport(
+                depManager, dafnyProgram,
+                boogiePrograms.SelectMany(tp => tp.Item2.AllCoveredElements),
+                coverageReportDir);
+            }
           }
         }
 
diff --git a/docs/DafnyRef/UserGuide.md b/docs/DafnyRef/UserGuide.md
index 372f1b3a04b..8fd4ce1c5dc 100644
--- a/docs/DafnyRef/UserGuide.md
+++ b/docs/DafnyRef/UserGuide.md
@@ -2294,8 +2294,6 @@ and what information it produces about the verification process.
 
 * `--no-verify` - turns off verification (for translate, build, run commands)
 
-* `--do-boogie-translation` - turns on translation to Boogie after resolving or if `--no-verify` is set. Automatically set if `--bprint` is set.
-
 * `--verify-included-files` (was `-verifyAllModules`) - verify modules that come from include directives.
 
   By default, Dafny only verifies files explicitly listed on the command

From 54e6ec233ba28cca61af12209a022fbf5d2841c6 Mon Sep 17 00:00:00 2001
From: Mikael Mayer <mimayere@amazon.com>
Date: Fri, 24 Jan 2025 13:32:07 -0600
Subject: [PATCH 4/4] Fixed CI + enhanced error reporting

---
 Source/DafnyDriver/Legacy/SynchronousCliCompilation.cs | 4 ++--
 Source/TestDafny/MultiBackendTest.cs                   | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/Source/DafnyDriver/Legacy/SynchronousCliCompilation.cs b/Source/DafnyDriver/Legacy/SynchronousCliCompilation.cs
index 281ec437a60..1056439299e 100644
--- a/Source/DafnyDriver/Legacy/SynchronousCliCompilation.cs
+++ b/Source/DafnyDriver/Legacy/SynchronousCliCompilation.cs
@@ -292,12 +292,12 @@ public async Task<ExitValue> ProcessFilesAsync(IReadOnlyList<DafnyFile/*!*/>/*!*
         bool verified;
         PipelineOutcome outcome;
         IDictionary<string, PipelineStatistics> moduleStats;
+        dafnyProgram.ProofDependencyManager = depManager;
         if (!options.DafnyVerify) {
           verified = false;
           outcome = PipelineOutcome.Done;
           moduleStats = new Dictionary<string, PipelineStatistics>();
         } else {
-          dafnyProgram.ProofDependencyManager = depManager;
           var boogiePrograms =
             await DafnyMain.LargeStackFactory.StartNew(() => Translate(engine.Options, dafnyProgram).ToList());
 
@@ -338,7 +338,7 @@ public async Task<ExitValue> ProcessFilesAsync(IReadOnlyList<DafnyFile/*!*/>/*!*
         }
 
         var failBecauseOfDiagnostics = dafnyProgram.Reporter.FailCompilationMessage;
-        if (!verified) {
+        if (!verified && options.DafnyVerify) {
           exitValue = ExitValue.VERIFICATION_ERROR;
         } else if (!compiled) {
           exitValue = ExitValue.COMPILE_ERROR;
diff --git a/Source/TestDafny/MultiBackendTest.cs b/Source/TestDafny/MultiBackendTest.cs
index ea81a97689c..ed92f909ad4 100644
--- a/Source/TestDafny/MultiBackendTest.cs
+++ b/Source/TestDafny/MultiBackendTest.cs
@@ -507,7 +507,7 @@ await output.WriteLineAsync(
     }
     await output.WriteLineAsync("Execution failed, for reasons other than known unsupported features. Output:");
     await output.WriteLineAsync(outputString);
-    await output.WriteLineAsync("Error:");
+    await output.WriteLineAsync($"Error (code={exitCode}):");
     await output.WriteLineAsync(error);
     return exitCode;
   }