diff --git a/Source/DafnyCore/Compilers/Compiler-Csharp.cs b/Source/DafnyCore/Compilers/Compiler-Csharp.cs
index 45a003b94f6..9431e46afdb 100644
--- a/Source/DafnyCore/Compilers/Compiler-Csharp.cs
+++ b/Source/DafnyCore/Compilers/Compiler-Csharp.cs
@@ -3390,7 +3390,7 @@ public override bool RunTargetProgram(string dafnyProgramName, string targetProg
     }
 
     private void AddTestCheckerIfNeeded(string name, Declaration decl, ConcreteSyntaxTree wr) {
-      if (DafnyOptions.O.RunAllTests || !Attributes.Contains(decl.Attributes, "test")) {
+      if (DafnyOptions.O.Compile || DafnyOptions.O.RunAllTests || !Attributes.Contains(decl.Attributes, "test")) {
         return;
       }
 
diff --git a/Source/DafnyCore/Options/DeveloperOptionBag.cs b/Source/DafnyCore/Options/DeveloperOptionBag.cs
index 64949a23d6d..df4cf86fdfb 100644
--- a/Source/DafnyCore/Options/DeveloperOptionBag.cs
+++ b/Source/DafnyCore/Options/DeveloperOptionBag.cs
@@ -5,13 +5,18 @@ namespace Microsoft.Dafny;
 
 public class DeveloperOptionBag {
 
+  public static readonly Option<bool> SpillTranslation = new("--spill-translation",
+    @"In case the Dafny source code is translated to another language, emit that translation.") {
+    IsHidden = true
+  };
+
   public static readonly Option<bool> UseBaseFileName = new("--use-basename-for-filename",
     "When parsing use basename of file for tokens instead of the path supplied on the command line") {
     IsHidden = true
   };
 
   public static readonly Option<string> BoogiePrint = new("--bprint",
-    @"
+  @"
 Print Boogie program translated from Dafny
 (use - as <file> to print to console)".TrimStart()) {
     IsHidden = true,
@@ -33,6 +38,8 @@ Print Dafny program after resolving it.
   };
 
   static DeveloperOptionBag() {
+    DafnyOptions.RegisterLegacyBinding(SpillTranslation, (o, f) => o.SpillTargetCode = f ? 1U : 0U);
+
     DafnyOptions.RegisterLegacyBinding(ResolvedPrint, (options, value) => {
       options.DafnyPrintResolvedFile = value;
       options.ExpandFilename(options.DafnyPrintResolvedFile, x => options.DafnyPrintResolvedFile = x, options.LogPrefix,
diff --git a/Source/DafnyCore/Options/ICommandSpec.cs b/Source/DafnyCore/Options/ICommandSpec.cs
index 3033445dde9..36d52f0848c 100644
--- a/Source/DafnyCore/Options/ICommandSpec.cs
+++ b/Source/DafnyCore/Options/ICommandSpec.cs
@@ -34,7 +34,8 @@ static ICommandSpec() {
   }.Concat(VerificationOptions).ToList();
 
   public static IReadOnlyList<Option> ExecutionOptions = new Option[] {
-    CommonOptionBag.Target
+    CommonOptionBag.Target,
+    DeveloperOptionBag.SpillTranslation
   }.Concat(TranslationOptions).ToList();
 
   public static IReadOnlyList<Option> ConsoleOutputOptions = new List<Option>(new Option[] {
diff --git a/docs/check-examples b/docs/check-examples
index ad89826e28f..7fbd70dc585 100755
--- a/docs/check-examples
+++ b/docs/check-examples
@@ -36,20 +36,20 @@
 ##   %no-check : do nothing
 ##   %check-verify <expect> or
 ##   %check-verify-warn : runs the command 
-##              "dafny verify --useBaseNameForFileName $F" and checks 
+##              "dafny verify --use-basename-for-filename $F" and checks
 ##              (1) if <expect> is absent then the exit code is 0 and
 ##                  the output is just a success message
 ##              (2) if <expect> is non-empty. then the exit code is 4 and
 ##                  the actual output matches the content of the file <expect>
 ##                  if the command is %check-verify-warn, the exit code is 0
 ##   %check-resolve <expect> : runs the command
-##              "dafny resolve --useBaseNameForFileName $F" and checks
+##              "dafny resolve --use-basename-for-filename $F" and checks
 ##              (1) if <expect> is absent then the exit code is 0 and
 ##                  the output is just a success message
 ##              (2) if <expect> is non-empty. then the exit code is 2 and
 ##                  the actual output matches the content of the file <expect>
 ##   %check-run <expect> : runs the command
-##              "dafny run --useBaseNameForFileName $F" and, 
+##              "dafny run --use-basename-for-filename $F" and,
 ##              if <expect> is present, then the output matches the
 ##              content of the file names <expect>
 ##   %check-error