diff --git a/Source/AutoExtern.Test/Tutorial/ClientApp/GroceryListPrinter.dfy.expect b/Source/AutoExtern.Test/Tutorial/ClientApp/GroceryListPrinter.dfy.expect
index bdc3a6c493..03a358a4c2 100644
--- a/Source/AutoExtern.Test/Tutorial/ClientApp/GroceryListPrinter.dfy.expect
+++ b/Source/AutoExtern.Test/Tutorial/ClientApp/GroceryListPrinter.dfy.expect
@@ -1,3 +1,4 @@
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 
 Dafny program verifier did not attempt verification
 Wrote textual form of target program to GroceryListPrinter.cs
diff --git a/Source/DafnyCore/DafnyOptions.cs b/Source/DafnyCore/DafnyOptions.cs
index 103291e3c7..54c5b78b07 100644
--- a/Source/DafnyCore/DafnyOptions.cs
+++ b/Source/DafnyCore/DafnyOptions.cs
@@ -480,7 +480,7 @@ private bool ParseBoogieOption(string name, Bpl.CommandLineParseState ps) {
       return base.ParseOption(name, ps);
     }
 
-    public override string Help => "Use 'dafny --help' to see help for a newer Dafny CLI format.\n" +
+    public override string Help => "Use 'dafny --help' to see help for the new Dafny CLI format.\n" +
       LegacyUiForOption.GenerateHelp(base.Help, LegacyUis, true);
 
     protected bool ParseDafnySpecificOption(string name, Bpl.CommandLineParseState ps) {
diff --git a/Source/DafnyDriver/Legacy/DafnyBackwardsCompatibleCli.cs b/Source/DafnyDriver/Legacy/DafnyBackwardsCompatibleCli.cs
index d513245f71..260b8a981c 100644
--- a/Source/DafnyDriver/Legacy/DafnyBackwardsCompatibleCli.cs
+++ b/Source/DafnyDriver/Legacy/DafnyBackwardsCompatibleCli.cs
@@ -88,6 +88,11 @@ private static ILegacyParseArguments TryLegacyArgumentParser(
               return new ExitImmediately(ExitValue.SUCCESS);
             }
 
+            if (oldOptions.DeprecationNoise != 0) {
+              oldOptions.OutputWriter.WriteLine(
+                "Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format");
+            }
+
             return new ParsedOptions(oldOptions);
           }
 
diff --git a/Source/DafnyDriver/Legacy/SynchronousCliCompilation.cs b/Source/DafnyDriver/Legacy/SynchronousCliCompilation.cs
index 430fbe92ee..40aa4f8d7a 100644
--- a/Source/DafnyDriver/Legacy/SynchronousCliCompilation.cs
+++ b/Source/DafnyDriver/Legacy/SynchronousCliCompilation.cs
@@ -144,8 +144,8 @@ public static ExitValue GetDafnyFiles(DafnyOptions options,
             dafnyFiles.Add(df);
             isDafnyFile = true;
           }
-        } catch (ArgumentException e) {
-          options.ErrorWriter.WriteLine("*** Error: {0}: ", nameToShow, e.Message);
+        } catch (ArgumentException) {
+          options.ErrorWriter.WriteLine("*** Error: {0}: ", nameToShow);
           return ExitValue.PREPROCESSING_ERROR;
         } catch (Exception e) {
           options.ErrorWriter.WriteLine("*** Error: {0}: {1}", nameToShow, e.Message);
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/diagnosticsFormats.legacy.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/diagnosticsFormats.legacy.dfy.expect
index ffba2da807..2773b6a107 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/diagnosticsFormats.legacy.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/diagnosticsFormats.legacy.dfy.expect
@@ -9,12 +9,14 @@ Dafny program verifier finished with 1 verified, 2 errors
 {"location":{"filename":"diagnosticsFormats.legacy.dfy","uri":"file:///diagnosticsFormats.legacy.dfy","range":{"start":{"line":19,"character":16}}},"severity":1,"message":"Error: a precondition for this call could not be proved","source":"Verifier","relatedInformation":[{"location":{"filename":"diagnosticsFormats.legacy.dfy","uri":"file:///diagnosticsFormats.legacy.dfy","range":{"start":{"line":18,"character":35}}},"message":"Related location: this is the precondition that could not be proved"}]}
 
 Dafny program verifier finished with 1 verified, 2 errors
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 {"location":{"filename":"diagnosticsFormats.legacy.dfy","uri":"file:///diagnosticsFormats.legacy.dfy","range":{"start":{"line":15,"character":0}}},"severity":2,"message":"module-level const declarations are always non-instance, so the \u0027static\u0027 keyword is not allowed here","source":"Parser","relatedInformation":[]}
 {"location":{"filename":"diagnosticsFormats.legacy.dfy","uri":"file:///diagnosticsFormats.legacy.dfy","range":{"start":{"line":14,"character":8}}},"severity":4,"message":"newtype byte resolves as target-complete {:nativeType \u0022byte\u0022} (detected range: 0 .. 256)","source":"Resolver","relatedInformation":[]}
 {"location":{"filename":"diagnosticsFormats.legacy.dfy","uri":"file:///diagnosticsFormats.legacy.dfy","range":{"start":{"line":16,"character":17}}},"severity":1,"message":"Error: result of operation might violate newtype constraint for \u0027byte\u0027","source":"Verifier","relatedInformation":[]}
 {"location":{"filename":"diagnosticsFormats.legacy.dfy","uri":"file:///diagnosticsFormats.legacy.dfy","range":{"start":{"line":19,"character":16}}},"severity":1,"message":"Error: a precondition for this call could not be proved","source":"Verifier","relatedInformation":[{"location":{"filename":"diagnosticsFormats.legacy.dfy","uri":"file:///diagnosticsFormats.legacy.dfy","range":{"start":{"line":18,"character":35}}},"message":"Related location: this is the precondition that could not be proved"}]}
 
 Dafny program verifier finished with 1 verified, 2 errors
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 {"location":{"filename":"diagnosticsFormats.legacy.dfy","uri":"file:///diagnosticsFormats.legacy.dfy","range":{"start":{"line":15,"character":0}}},"severity":2,"message":"module-level const declarations are always non-instance, so the \u0027static\u0027 keyword is not allowed here","source":"Parser","relatedInformation":[]}
 {"location":{"filename":"diagnosticsFormats.legacy.dfy","uri":"file:///diagnosticsFormats.legacy.dfy","range":{"start":{"line":16,"character":17}}},"severity":1,"message":"Error: result of operation might violate newtype constraint for \u0027byte\u0027","source":"Verifier","relatedInformation":[]}
 {"location":{"filename":"diagnosticsFormats.legacy.dfy","uri":"file:///diagnosticsFormats.legacy.dfy","range":{"start":{"line":19,"character":14},"end":{"line":19,"character":18}}},"severity":1,"message":"Error: a precondition for this call could not be proved","source":"Verifier","relatedInformation":[{"location":{"filename":"diagnosticsFormats.legacy.dfy","uri":"file:///diagnosticsFormats.legacy.dfy","range":{"start":{"line":18,"character":35},"end":{"line":18,"character":35}}},"message":"Related location: this is the precondition that could not be proved"}]}
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/cloudmake/CloudMake-ConsistentBuilds.legacy.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/cloudmake/CloudMake-ConsistentBuilds.legacy.dfy.expect
index 1b45cf86b6..1bb49a99b9 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/cloudmake/CloudMake-ConsistentBuilds.legacy.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/cloudmake/CloudMake-ConsistentBuilds.legacy.dfy.expect
@@ -1,2 +1,3 @@
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 
 Dafny program verifier finished with 42 verified, 0 errors
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/BranchCoverage.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/BranchCoverage.dfy.expect
index 9af29a520c..f32f724a96 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/BranchCoverage.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/BranchCoverage.dfy.expect
@@ -1,3 +1,4 @@
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 
 Dafny program verifier finished with 6 verified, 0 errors
 0: BranchCoverage.dfy(20,21): entry to method _module._default.NeverCalled
@@ -84,6 +85,7 @@ Dafny program verifier finished with 6 verified, 0 errors
 39: 10
 40: 1
 41: 3
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 
 Dafny program verifier finished with 6 verified, 0 errors
 0: BranchCoverage.dfy(20,21): entry to method _module._default.NeverCalled
@@ -170,6 +172,7 @@ Dafny program verifier finished with 6 verified, 0 errors
 39: 10
 40: 1
 41: 3
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 
 Dafny program verifier finished with 6 verified, 0 errors
 0: BranchCoverage.dfy(20,21): entry to method _module._default.NeverCalled
@@ -256,6 +259,7 @@ Dafny program verifier finished with 6 verified, 0 errors
 39: 10
 40: 1
 41: 3
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 
 Dafny program verifier finished with 6 verified, 0 errors
 0: BranchCoverage.dfy(20,21): entry to method _module._default.NeverCalled
@@ -342,6 +346,7 @@ Dafny program verifier finished with 6 verified, 0 errors
 39: 10
 40: 1
 41: 3
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 
 Dafny program verifier finished with 6 verified, 0 errors
 0: BranchCoverage.dfy(20,21): entry to method _module._default.NeverCalled
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/TestedExterns.legacy.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/TestedExterns.legacy.dfy.expect
index 33db6e1df8..a2ac9a5b79 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/TestedExterns.legacy.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/TestedExterns.legacy.dfy.expect
@@ -1,3 +1,4 @@
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 
 Dafny program verifier finished with 0 verified, 0 errors
 CheckExtern.dfy(20,13): Warning: The requires clause at this location cannot be compiled to be tested at runtime because it references ghost state.
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/DafnyLibClient.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/DafnyLibClient.dfy.expect
index d587e6f900..96adf7ea9c 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/DafnyLibClient.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/DafnyLibClient.dfy.expect
@@ -1,5 +1,7 @@
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 
 Dafny program verifier finished with 3 verified, 0 errors
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 
 Dafny program verifier finished with 1 verified, 0 errors
 hello from the library
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ForallCompilation.legacy.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ForallCompilation.legacy.dfy.expect
index 66ffe3665d..78374efda7 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ForallCompilation.legacy.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ForallCompilation.legacy.dfy.expect
@@ -1,2 +1,3 @@
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 
 Dafny program verifier finished with 14 verified, 0 errors
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/JavaUseRuntimeLib.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/JavaUseRuntimeLib.dfy.expect
index 97bd1dc93c..94c79db583 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/JavaUseRuntimeLib.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/JavaUseRuntimeLib.dfy.expect
@@ -1,3 +1,4 @@
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 
 Dafny program verifier finished with 0 verified, 0 errors
 bye
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Superposition.legacy.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Superposition.legacy.dfy.expect
index 4ed6129f4d..c6273819d6 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Superposition.legacy.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Superposition.legacy.dfy.expect
@@ -1,3 +1,4 @@
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 Superposition.legacy.dfy(38,9): Warning: the ... refinement feature in statements is deprecated
 
 Verifying M0.C.M (correctness) ...
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots3.run.legacy.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots3.run.legacy.dfy.expect
index 392746d306..2342fa3352 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots3.run.legacy.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots3.run.legacy.dfy.expect
@@ -1,3 +1,4 @@
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 Processing command (at Snapshots3.v0.dfy(9,14)) assert {:id "id0"} Lit(0 != 0);
   >>> DoNothingToAssert
 Snapshots3.v0.dfy(9,13): Error: assertion might not hold
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots4.run.legacy.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots4.run.legacy.dfy.expect
index f5c1207363..3d212d4e11 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots4.run.legacy.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots4.run.legacy.dfy.expect
@@ -1,3 +1,4 @@
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 Processing command (at Snapshots4.v0.dfy(9,14)) assert {:id "id0"} LitInt(0) == LitInt(0);
   >>> DoNothingToAssert
 
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots8.run.legacy.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots8.run.legacy.dfy.expect
index 20638ec120..0b3564e7be 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots8.run.legacy.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots8.run.legacy.dfy.expect
@@ -1,3 +1,4 @@
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 Processing command (at Snapshots8.v0.dfy(2,37)) assert {:id "id0"} x#0 < 20 || LitInt(10) <= x#0;
   >>> DoNothingToAssert
 Processing command (at Snapshots8.v0.dfy(3,12)) assert {:id "id1"} x#0 < 10;
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots9.run.legacy.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots9.run.legacy.dfy.expect
index 0657e360d5..36e8d43cba 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots9.run.legacy.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots9.run.legacy.dfy.expect
@@ -1,3 +1,4 @@
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 Processing command (at Snapshots9.v0.dfy(2,11)) assert {:id "id2"} ok#0;
   >>> DoNothingToAssert
 Snapshots9.v0.dfy(4,7): Error: a postcondition could not be proved on this return path
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny1/InductionOptions.legacy.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny1/InductionOptions.legacy.dfy.expect
index 94d7df9883..a3bc7bb4c8 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny1/InductionOptions.legacy.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny1/InductionOptions.legacy.dfy.expect
@@ -1,3 +1,4 @@
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 InductionOptions.legacy.dfy(21,0): Error: a postcondition could not be proved on this return path
 InductionOptions.legacy.dfy(20,26): Related location: this is the postcondition that could not be proved
 InductionOptions.legacy.dfy(25,9): Error: assertion might not hold
@@ -17,12 +18,15 @@ InductionOptions.legacy.dfy(29,10): Related location: this is the postcondition
 InductionOptions.legacy.dfy(35,9): Error: assertion might not hold
 
 Dafny program verifier finished with 3 verified, 4 errors
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 InductionOptions.legacy.dfy(21,0): Error: a postcondition could not be proved on this return path
 InductionOptions.legacy.dfy(20,26): Related location: this is the postcondition that could not be proved
 
 Dafny program verifier finished with 6 verified, 1 error
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 
 Dafny program verifier finished with 7 verified, 0 errors
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 InductionOptions.legacy.dfy(25,9): Error: assertion might not hold
 InductionOptions.legacy.dfy(30,0): Error: a postcondition could not be proved on this return path
 InductionOptions.legacy.dfy(29,10): Related location: this is the postcondition that could not be proved
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Bug128.legacy.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Bug128.legacy.dfy.expect
index 823a60a105..f5e8881638 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Bug128.legacy.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Bug128.legacy.dfy.expect
@@ -1,2 +1,3 @@
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 
 Dafny program verifier finished with 1 verified, 0 errors
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Lucas-down.legacy.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Lucas-down.legacy.dfy.expect
index e5f9ee5a23..70bd0a38c7 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Lucas-down.legacy.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Lucas-down.legacy.dfy.expect
@@ -1,2 +1,3 @@
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 
 Dafny program verifier finished with 12 verified, 0 errors
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Lucas-up.legacy.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Lucas-up.legacy.dfy.expect
index 8c4d74ae00..c541d906ae 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Lucas-up.legacy.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Lucas-up.legacy.dfy.expect
@@ -1,2 +1,3 @@
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 
 Dafny program verifier finished with 19 verified, 0 errors
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue158.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue158.dfy.expect
index 4a67f9531f..808c08e932 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue158.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue158.dfy.expect
@@ -1,3 +1,4 @@
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 
 Dafny program verifier finished with 4 verified, 0 errors
 map[Record.Make(null, null, _module.Class, 5, 10) := 0.8]
@@ -24,6 +25,7 @@ false
 false false
 false false
 true true
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 
 Dafny program verifier finished with 4 verified, 0 errors
 map[Record.Make(null, null, _module.Class, 5, 10) := 0.8]
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue250.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue250.dfy.expect
index 971a5ef441..1644c59e8b 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue250.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue250.dfy.expect
@@ -1,20 +1,30 @@
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 
 Dafny program verifier finished with 0 verified, 0 errors
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 
 Dafny program verifier finished with 0 verified, 0 errors
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 
 Dafny program verifier finished with 0 verified, 0 errors
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 
 Dafny program verifier finished with 0 verified, 0 errors
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 
 Dafny program verifier finished with 0 verified, 0 errors
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 
 Dafny program verifier finished with 0 verified, 0 errors
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 
 Dafny program verifier finished with 0 verified, 0 errors
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 
 Dafny program verifier finished with 0 verified, 0 errors
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 
 Dafny program verifier finished with 0 verified, 0 errors
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 
 Dafny program verifier finished with 0 verified, 0 errors
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue59.legacy.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue59.legacy.dfy.expect
index 600aed809a..7ac391b40b 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue59.legacy.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue59.legacy.dfy.expect
@@ -1,3 +1,4 @@
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 
 Verifying foo (correctness) ...
   [1 proof obligation]  error
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1248.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1248.dfy.expect
index 9c489d683b..04f483c39c 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1248.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1248.dfy.expect
@@ -4,6 +4,7 @@ git-issue-1248.dfy(19,0): Error: a postcondition could not be proved on this ret
 git-issue-1248.dfy(18,10): Related location: this is the postcondition that could not be proved
 
 Dafny program verifier finished with 0 verified, 2 errors
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 git-issue-1248.dfy(13,0): Error: a postcondition could not be proved on this return path
 git-issue-1248.dfy(12,10): Related location: this is the postcondition that could not be proved
 git-issue-1248.dfy(19,0): Error: a postcondition could not be proved on this return path
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-19c.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-19c.dfy.expect
index 9d50bad425..118d2e4bde 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-19c.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-19c.dfy.expect
@@ -1,3 +1,4 @@
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 git-issue-19c.dfy(41,10): Error: a set comprehension involved in a function definition is not allowed to depend on the set of allocated references, but values of 'basic' (of type 'Basic') may contain references (see documentation for 'older' parameters)
 git-issue-19c.dfy(86,12): Error: a set comprehension involved in a function definition (implicitly by using a function in a reads clause) is not allowed to depend on the set of allocated references, but values of '_x0' (of type 'Basic') may contain references (see documentation for 'older' parameters)
 git-issue-19c.dfy(93,12): Error: a set comprehension involved in a function definition (implicitly by using a function in a reads clause) is not allowed to depend on the set of allocated references, but values of '_x0' (of type 'X') may contain references (perhaps declare its type as 'X(!new)') (see documentation for 'older' parameters)
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2690.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2690.dfy
index 290f2f86d0..b2d1e04ae8 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2690.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2690.dfy
@@ -20,5 +20,5 @@ method Main() {
   print "2 in seq? ", f(2),"\n";
   var g := InSeq2([1, 2]);
   print "2 in seq? ", g(2),"\n";
-  print "All right";
+  print "All right", "\n";
 }
\ No newline at end of file
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2690.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2690.dfy.expect
index 6533295402..bef49ef432 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2690.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2690.dfy.expect
@@ -1,9 +1,12 @@
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 
 Dafny program verifier finished with 3 verified, 0 errors
 2 in seq? true
 2 in seq? true
 All right
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
+
 Dafny program verifier did not attempt verification
 2 in seq? true
 2 in seq? true
-All right
\ No newline at end of file
+All right
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2719.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2719.dfy.expect
index 1f8b85a60e..821c790f5c 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2719.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2719.dfy.expect
@@ -1 +1,2 @@
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 *** Error: file foobar.dll not found
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-277.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-277.dfy.expect
index d02120ea36..3c3d079282 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-277.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-277.dfy.expect
@@ -1,3 +1,4 @@
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 git-issue-277.dfy(5,12): Error: wrong number of indices for multi-selection
 git-issue-277.dfy(5,25): Error: wrong number of indices for multi-selection
 git-issue-277.dfy(5,12): Error: incorrect type for selection into array<int> (got bool)
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2843.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2843.dfy.expect
index 5b97a774f1..4fb686a413 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2843.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2843.dfy.expect
@@ -1,3 +1,4 @@
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 git-issue-2843.dfy(14,7): Error: a function with ghost parameters can be used as a value only in specification contexts
 git-issue-2843.dfy(20,7): Error: a ghost function is allowed only in specification contexts
 git-issue-2843.dfy(33,8): Error: ghost variables such as f are allowed only in specification contexts. f was inferred to be ghost based on its declaration or initialization.
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3267.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3267.dfy.expect
index b9b12d9078..a96d003038 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3267.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3267.dfy.expect
@@ -1,7 +1,10 @@
 *** Error: 'zzzz': The first input must be a command or a legacy option or file with supported extension
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 *** Error: 'test.d': Filename extension '.d' is not supported. Input files must be Dafny programs (.dfy) or supported auxiliary files (.cs, .dll)
 CLI: Error: command-line argument '--zzzz' is neither a recognized option nor a Dafny input file (.dfy, .doo, or .toml).
 CLI: Error: command-line argument 'test' is neither a recognized option nor a Dafny input file (.dfy, .doo, or .toml).
 CLI: Error: command-line argument 'test.d' is neither a recognized option nor a Dafny input file (.dfy, .doo, or .toml).
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 *** Error: 'test.d': Filename extension '.d' is not supported. Input files must be Dafny programs (.dfy) or supported auxiliary files (.cs, .dll)
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 *** Error: Command-line argument 'zzzz' is neither a recognized option nor a filename with a supported extension (.dfy, .cs, .dll).
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-645.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-645.dfy.expect
index 16f0e80fa2..90a4537053 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-645.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-645.dfy.expect
@@ -1 +1,2 @@
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 *** Error: Command-line argument 'xyz' is neither a recognized option nor a filename with a supported extension (.dfy, .cs, .dll).
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/Folding.legacy.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/Folding.legacy.dfy.expect
index c4384266df..3c54825147 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/Folding.legacy.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/Folding.legacy.dfy.expect
@@ -1,3 +1,4 @@
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 
 Dafny program verifier finished with 21 verified, 0 errors
 xs = List.Cons(57, List.Cons(100, List.Cons(-34, List.Cons(1, List.Cons(8, List.Nil)))))
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/irondafny0/inheritreqs0.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/irondafny0/inheritreqs0.dfy.expect
index 82635c3858..ff8132578a 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/irondafny0/inheritreqs0.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/irondafny0/inheritreqs0.dfy.expect
@@ -1,3 +1,4 @@
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 inheritreqs0.dfy(19,13): Error: a precondition for this call could not be proved
 inheritreqs0.dfy[Impl](6,17): Related location: this is the precondition that could not be proved
 
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/irondafny0/inheritreqs1.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/irondafny0/inheritreqs1.dfy.expect
index 6dd57debae..4ac3ca4d20 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/irondafny0/inheritreqs1.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/irondafny0/inheritreqs1.dfy.expect
@@ -1,3 +1,4 @@
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 inheritreqs1.dfy(20,13): Error: a precondition for this call could not be proved
 inheritreqs1.dfy(15,17): Related location: this is the precondition that could not be proved
 
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/irondafny0/optimize0.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/irondafny0/optimize0.dfy.expect
index 4e37c19c36..b1ee3c10f2 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/irondafny0/optimize0.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/irondafny0/optimize0.dfy.expect
@@ -1,3 +1,4 @@
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 
 Dafny program verifier finished with 0 verified, 0 errors
 o hai!
\ No newline at end of file
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencyWarnings.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencyWarnings.dfy
index 47c5da7a04..ec9f858c23 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencyWarnings.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencyWarnings.dfy
@@ -2,6 +2,6 @@
 // RUN: %diff "%s.expect" "%t.new"
 // Also test old CLI
 // RUN: %baredafny /compile:0 /useBaseNameForFileName /verifyAllModules /warnContradictoryAssumptions /warnRedundantAssumptions "%s" > "%t.old"
-// RUN: %diff "%s.expect" "%t.old"
+// RUN: %diff "%s.expect2" "%t.old"
 
 include "ProofDependencies.dfy"
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencyWarnings.dfy.expect2 b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencyWarnings.dfy.expect2
new file mode 100644
index 0000000000..6e17778f8e
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencyWarnings.dfy.expect2
@@ -0,0 +1,21 @@
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
+ProofDependencies.dfy(176,11): Warning: unnecessary (or partly unnecessary) assume statement
+ProofDependencies.dfy(185,11): Warning: unnecessary (or partly unnecessary) assume statement
+ProofDependencies.dfy(186,13): Warning: proved using contradictory assumptions: assertion always holds. (Use the `{:contradiction}` attribute on the `assert` statement to silence.)
+ProofDependencies.dfy(191,11): Warning: unnecessary (or partly unnecessary) assume statement
+ProofDependencies.dfy(193,13): Warning: proved using contradictory assumptions: assertion always holds. (Use the `{:contradiction}` attribute on the `assert` statement to silence.)
+ProofDependencies.dfy(202,11): Warning: proved using contradictory assumptions: assertion always holds. (Use the `{:contradiction}` attribute on the `assert` statement to silence.)
+ProofDependencies.dfy(203,4): Warning: proved using contradictory assumptions: value always satisfies the subset constraints of 'nat'
+ProofDependencies.dfy(209,10): Warning: ensures clause proved using contradictory assumptions
+ProofDependencies.dfy(211,11): Warning: proved using contradictory assumptions: assertion always holds. (Use the `{:contradiction}` attribute on the `assert` statement to silence.)
+ProofDependencies.dfy(212,11): Warning: proved using contradictory assumptions: value always satisfies the subset constraints of 'nat'
+ProofDependencies.dfy(226,11): Warning: unnecessary requires clause
+ProofDependencies.dfy(241,11): Warning: unnecessary requires clause
+ProofDependencies.dfy(298,11): Warning: unnecessary requires clause
+ProofDependencies.dfy(299,11): Warning: unnecessary requires clause
+ProofDependencies.dfy(321,11): Warning: unnecessary requires clause
+ProofDependencies.dfy(346,10): Warning: ensures clause proved using contradictory assumptions
+ProofDependencies.dfy(354,11): Warning: unnecessary requires clause
+ProofDependencies.dfy(363,9): Warning: unnecessary (or partly unnecessary) assert statement
+
+Dafny program verifier finished with 32 verified, 0 errors
diff --git a/docs/DafnyRef/Options.txt b/docs/DafnyRef/Options.txt
index b5d8820901..2c2d90f939 100644
--- a/docs/DafnyRef/Options.txt
+++ b/docs/DafnyRef/Options.txt
@@ -1,5 +1,5 @@
 ```
-Use 'dafny --help' to see help for a newer Dafny CLI format.
+Use 'dafny --help' to see help for the new Dafny CLI format.
 Usage: dafny [ option ... ] [ filename ... ]
 
   ---- General options -------------------------------------------------------
diff --git a/docs/HowToFAQ/Errors-Compiler.md b/docs/HowToFAQ/Errors-Compiler.md
index 32c67c2d20..4203dd1e34 100644
--- a/docs/HowToFAQ/Errors-Compiler.md
+++ b/docs/HowToFAQ/Errors-Compiler.md
@@ -121,7 +121,7 @@ Consequently an explicit constructor is required.
 
 ## **Error: The method '_name_' is not permitted as a main method (_reason_).** {#c_method_may_not_be_main_method}
 
-<!-- %check-legacy %options -compile:2 -Main:mmm -->
+<!-- %check-run %options --main-method:mmm -->
 ```dafny
 method mmm(i: int) {}
 ```
@@ -140,7 +140,7 @@ Most commonly and for clarity, the intended main method is marked with the attri
 
 ## **Error: Could not find the method named by the -Main option: _name_** {#c_could_not_find_stipulated_main_method}
 
-<!-- %check-legacy %options /compile:2 -Main:m -->
+<!-- %check-run %options --main-method:m -->
 ```dafny
 class A { static method mm() {} }
 ```
diff --git a/docs/HowToFAQ/Errors-Compiler.template b/docs/HowToFAQ/Errors-Compiler.template
index 4b7fe81e5d..93e5e82df8 100644
--- a/docs/HowToFAQ/Errors-Compiler.template
+++ b/docs/HowToFAQ/Errors-Compiler.template
@@ -81,7 +81,7 @@ class A { var j: int }
 
 ## **Error: The method '_name_' is not permitted as a main method (_reason_).** {#c_method_may_not_be_main_method}
 
-<!-- %check-legacy %options -compile:2 -Main:mmm -->
+<!-- %check-run %options --main-method:mmm -->
 ```dafny
 method mmm(i: int) {}
 ```
@@ -90,7 +90,7 @@ method mmm(i: int) {}
 
 ## **Error: Could not find the method named by the -Main option: _name_** {#c_could_not_find_stipulated_main_method}
 
-<!-- %check-legacy %options /compile:2 -Main:m -->
+<!-- %check-run %options --main-method:m -->
 ```dafny
 class A { static method mm() {} }
 ```
diff --git a/docs/HowToFAQ/Errors-Parser.md b/docs/HowToFAQ/Errors-Parser.md
index 32ebac2545..0651a09729 100644
--- a/docs/HowToFAQ/Errors-Parser.md
+++ b/docs/HowToFAQ/Errors-Parser.md
@@ -1013,25 +1013,6 @@ that assist in proving the validity of the asserted expression.
 
 <!-- TODO -->
 
-## **Error: a forall statement with an ensures clause must have a body** {#p_forall_with_ensures_must_have_body}
-
-<!-- TODO: This example does not yet work in the new CLI because there is no way to turn on /noCheating in the new CLI -->
-
-<!-- %check-legacy %options -compile:0 -noCheating:1 -->
-```dafny
-module M {
-  predicate f(i: int) { true }
-  method  m(a: seq<int>) {
-    forall i | 0 <= i < 10
-       ensures f(i)
-  }
-}
-```
-
-A forall statement without a body is like an assume statement: the ensures clause is assumed in the following code.
-Assumptions like that are a risk to soundness because there is no check that the assumption is true.
-Thus in a context in which open assumptions are not allowed, body-less forall statements are also not allowed.
-
 ## **Warning: the modify statement with a block statement is deprecated** {#p_deprecated_modify_statement_with_block}
 
 <!-- TODO-->
@@ -1477,7 +1458,7 @@ that is a single underscore is used as a wild-card match.
 
 ## **Warning: deprecated style: a semi-colon is not needed here {#p_deprecated_semicolon}
 
-<!-- %check-legacy %exit 0 %options /compile:0 /deprecation:2 -->
+<!-- %check-resolve %options -->
 ```dafny
 const c := 5;
 ```
diff --git a/docs/HowToFAQ/Errors-Parser.template b/docs/HowToFAQ/Errors-Parser.template
index 8ac51a299e..bffbed1796 100644
--- a/docs/HowToFAQ/Errors-Parser.template
+++ b/docs/HowToFAQ/Errors-Parser.template
@@ -811,23 +811,6 @@ method m() {
 
 <!-- INSERT-TEXT -->
 
-## **Error: a forall statement with an ensures clause must have a body** {#p_forall_with_ensures_must_have_body}
-
-<!-- TODO: This example does not yet work in the new CLI because there is no way to turn on /noCheating in the new CLI -->
-
-<!-- %check-legacy %options -compile:0 -noCheating:1 -->
-```dafny
-module M {
-  predicate f(i: int) { true }
-  method  m(a: seq<int>) {
-    forall i | 0 <= i < 10
-       ensures f(i)
-  }
-}
-```
-
-<!-- INSERT-TEXT -->
-
 ## **Warning: the modify statement with a block statement is deprecated** {#p_deprecated_modify_statement_with_block}
 
 <!-- INSERT-TEXT -->
@@ -1133,7 +1116,7 @@ const _myconst := 5
 
 ## **Warning: deprecated style: a semi-colon is not needed here {#p_deprecated_semicolon}
 
-<!-- %check-legacy %exit 0 %options /compile:0 /deprecation:2 -->
+<!-- %check-resolve %options -->
 ```dafny
 const c := 5;
 ```