diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
index 7d50d99873c..b181dac5d1d 100644
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@@ -74,7 +74,7 @@ After doing these steps once, for other PRs, one only needs to re-run deep check
 - If some required tests fail, investigate and push more commits, but know that each CI run takes a lot of time, so try to fix the problem with as few commits as possible (ideally 1)
   It is also possible you find some tests that fail randomly, in that case, re-run them and report to the team. Avoid using the re-run all failed jobs here, because it will re-run _all_ jobs, so select them individually instead.
 - Have someone approve the PR and merge it (or auto-merge).
-- Once the PR with the fix to the CI is merged to master, go to https://github.com/dafny-lang/dafny/actions/workflows/deep-tests.yml
+- Once the PR with the fix to the CI is merged to master, go to https://github.com/dafny-lang/dafny/actions/workflows/nightly-build.yml
 - Select "Run workflow..."
 - Select master
 - Wait for this new run to succeed.
@@ -106,4 +106,4 @@ You can find a description of the release process in [docs/dev/RELEASE.md](https
 
 Dafny is still changing and backwards incompatible changes may be made. Any backwards compatibility breaking change must be easy to adapt to, such as by adding a command line option. In the future, we plan to add a `dafny migrate` command which should support migrating any Dafny codebase from the previous to the current CLI version. 
 
-As rule, Dafny features must be marked as deprecated, including migration instructions, at least one release before they are removed.
\ No newline at end of file
+As rule, Dafny features must be marked as deprecated, including migration instructions, at least one release before they are removed.
diff --git a/Source/DafnyDriver/CliCompilation.cs b/Source/DafnyDriver/CliCompilation.cs
index 5ce3b1c63c5..8ef85d82403 100644
--- a/Source/DafnyDriver/CliCompilation.cs
+++ b/Source/DafnyDriver/CliCompilation.cs
@@ -24,6 +24,7 @@ public class CliCompilation {
   public Compilation Compilation { get; }
   private readonly ConcurrentDictionary<MessageSource, int> errorsPerSource = new();
   private int errorCount;
+  private int warningCount;
   public bool DidVerification { get; private set; }
 
   private CliCompilation(
@@ -48,10 +49,13 @@ private CliCompilation(
     Compilation = createCompilation(executionEngine, input);
   }
 
-  public int ExitCode => (int)ExitValue;
+  public async Task<int> GetAndReportExitCode() {
+    var value = await GetAndReportExitValue();
+    return (int)value;
+  }
 
-  public ExitValue ExitValue {
-    get {
+  public async Task<ExitValue> GetAndReportExitValue() {
+    if (errorCount > 0) {
       if (HasErrorsFromSource(MessageSource.Project)) {
         return ExitValue.PREPROCESSING_ERROR;
       }
@@ -59,11 +63,19 @@ public ExitValue ExitValue {
       if (HasErrorsFromSource(MessageSource.Verifier)) {
         return ExitValue.VERIFICATION_ERROR;
       }
-      return errorCount > 0 ? ExitValue.DAFNY_ERROR : ExitValue.SUCCESS;
+      return ExitValue.DAFNY_ERROR;
+    }
 
-      bool HasErrorsFromSource(MessageSource source) {
-        return errorsPerSource.GetOrAdd(source, _ => 0) != 0;
-      }
+    if (warningCount > 0 && !Options.Get(CommonOptionBag.AllowWarnings)) {
+      await Options.OutputWriter.WriteLineAsync(
+        "Compilation failed because warnings were found and --allow-warnings is false");
+      return ExitValue.DAFNY_ERROR;
+    }
+
+    return ExitValue.SUCCESS;
+
+    bool HasErrorsFromSource(MessageSource source) {
+      return errorsPerSource.GetOrAdd(source, _ => 0) != 0;
     }
   }
 
@@ -105,6 +117,10 @@ public void Start() {
             (_, previous) => previous + 1);
           Interlocked.Increment(ref errorCount);
         }
+
+        if (newDiagnostic.Diagnostic.Level == ErrorLevel.Warning) {
+          Interlocked.Increment(ref warningCount);
+        }
         var dafnyDiagnostic = newDiagnostic.Diagnostic;
         consoleReporter.Message(dafnyDiagnostic.Source, dafnyDiagnostic.Level,
           dafnyDiagnostic.ErrorId, dafnyDiagnostic.Token, dafnyDiagnostic.Message);
diff --git a/Source/DafnyDriver/Commands/MeasureComplexityCommand.cs b/Source/DafnyDriver/Commands/MeasureComplexityCommand.cs
index 0927fdcee4c..3eb79d2a6e2 100644
--- a/Source/DafnyDriver/Commands/MeasureComplexityCommand.cs
+++ b/Source/DafnyDriver/Commands/MeasureComplexityCommand.cs
@@ -71,7 +71,7 @@ private static async Task<int> Execute(DafnyOptions options) {
       await verificationResultsLogged;
     }
 
-    return compilation.ExitCode;
+    return await compilation.GetAndReportExitCode();
   }
 
   private static async Task RunVerificationIterations(DafnyOptions options, CliCompilation compilation,
diff --git a/Source/DafnyDriver/Commands/ResolveCommand.cs b/Source/DafnyDriver/Commands/ResolveCommand.cs
index f0491cd1b4c..ec0342164cc 100644
--- a/Source/DafnyDriver/Commands/ResolveCommand.cs
+++ b/Source/DafnyDriver/Commands/ResolveCommand.cs
@@ -17,10 +17,11 @@ public static Command Create() {
       compilation.Start();
       await compilation.Resolution;
 
-      if (compilation.ExitValue == ExitValue.SUCCESS) {
+      var value = await compilation.GetAndReportExitValue();
+      if (value == ExitValue.SUCCESS) {
         await options.OutputWriter.WriteLineAsync("\nDafny program verifier did not attempt verification");
       }
-      return compilation.ExitCode;
+      return (int)value;
     });
     return result;
   }
diff --git a/Source/DafnyDriver/Commands/VerifyCommand.cs b/Source/DafnyDriver/Commands/VerifyCommand.cs
index 7a2212419ac..5913ead4e9c 100644
--- a/Source/DafnyDriver/Commands/VerifyCommand.cs
+++ b/Source/DafnyDriver/Commands/VerifyCommand.cs
@@ -69,7 +69,7 @@ public static async Task<int> HandleVerification(DafnyOptions options) {
       await verificationResultsLogged;
     }
 
-    return compilation.ExitCode;
+    return await compilation.GetAndReportExitCode();
   }
   public static async Task ReportVerificationSummary(
     CliCompilation cliCompilation,
diff --git a/Source/DafnyDriver/DafnyNewCli.cs b/Source/DafnyDriver/DafnyNewCli.cs
index 5497dfe02ec..274681cfaaa 100644
--- a/Source/DafnyDriver/DafnyNewCli.cs
+++ b/Source/DafnyDriver/DafnyNewCli.cs
@@ -224,11 +224,7 @@ private static async Task<bool> ProcessProjectFile(DafnyOptions dafnyOptions, Fi
 
     foreach (var diagnostic in projectFile.Errors.AllMessages) {
       var message = $"{diagnostic.Level}: {diagnostic.Message}";
-      if (diagnostic.Level == ErrorLevel.Error) {
-        await dafnyOptions.ErrorWriter.WriteLineAsync(message);
-      } else {
-        await dafnyOptions.OutputWriter.WriteLineAsync(message);
-      }
+      await dafnyOptions.OutputWriter.WriteLineAsync(message);
     }
 
     projectFile.Validate(dafnyOptions.OutputWriter, AllOptions);
diff --git a/Source/DafnyStandardLibraries/scripts/check-examples b/Source/DafnyStandardLibraries/scripts/check-examples
index ebe308a99e6..72f22dc9035 100755
--- a/Source/DafnyStandardLibraries/scripts/check-examples
+++ b/Source/DafnyStandardLibraries/scripts/check-examples
@@ -219,6 +219,7 @@ do
           ec=2
         elif [ "$command" == "%check-resolve-warn" ]; then
           com=resolve
+          dOptions="$dOptions --allow-warnings"
           ec=0
         elif [ "$command" == "%check-translate" ]; then
           com=translate
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/assume.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/assume.dfy
index 933fbd21867..b269a967583 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/assume.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/assume.dfy
@@ -1,6 +1,6 @@
-// RUN: %testDafnyForEachResolver "%s" -- --allow-axioms=false 
+// RUN: ! %testDafnyForEachResolver "%s" -- --allow-axioms=false
 // NONUNIFORM: warning will be the same for all back-end
-// RUN: %verify --standard-libraries --allow-axioms:false "%s" > "%t"
+// RUN: ! %verify --standard-libraries --allow-axioms:false "%s" &> "%t"
 // RUN: %diff "%s.expect" "%t"
 
 method Foo() {
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/assume.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/assume.dfy.expect
index 2ec7eb2f42b..f144db9d004 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/assume.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/assume.dfy.expect
@@ -3,3 +3,4 @@ assume.dfy(11,10): Warning: assume keyword in assign-such-that statement has no
 assume.dfy(13,11): Warning: assume keyword in update-with-failure statement has no {:axiom} annotation
 
 Dafny program verifier finished with 2 verified, 0 errors
+Compilation failed because warnings were found and --allow-warnings is false
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/function.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/function.dfy
index 75137a203d4..e075afe77be 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/function.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/function.dfy
@@ -1,6 +1,6 @@
-// RUN: %verify --allow-axioms:false --type-system-refresh "%s" > "%t"
+// RUN: ! %verify --allow-axioms:false --type-system-refresh "%s" &> "%t"
 // NONUNIFORM: warning will be the same for all back-end
-// RUN: ! %run --allow-axioms:false "%s" >> "%t"
+// RUN: ! %run --allow-axioms:false "%s" &>> "%t"
 // RUN: %diff "%s.expect" "%t"
 
 
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/function.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/function.dfy.expect
index 043d0e4174e..f42d7c92817 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/function.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/function.dfy.expect
@@ -4,6 +4,7 @@ function.dfy(8,36): Warning: This ensures clause is part of a bodyless function.
 function.dfy(8,50): Warning: This ensures clause is part of a bodyless function. Add the {:axiom} attribute to it or the enclosing function to suppress this warning
 
 Dafny program verifier finished with 9 verified, 0 errors
+Compilation failed because warnings were found and --allow-warnings is false
 function.dfy(7,33): Warning: This ensures clause is part of a bodyless function. Add the {:axiom} attribute to it or the enclosing function to suppress this warning
 function.dfy(7,47): Warning: This ensures clause is part of a bodyless function. Add the {:axiom} attribute to it or the enclosing function to suppress this warning
 function.dfy(8,36): Warning: This ensures clause is part of a bodyless function. Add the {:axiom} attribute to it or the enclosing function to suppress this warning
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/method.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/method.dfy
index bebce60ecc4..d944cbeaeed 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/method.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/method.dfy
@@ -1,4 +1,4 @@
-// RUN: %verify --allow-axioms:false --type-system-refresh "%s" > "%t"
+// RUN: %verify --allow-axioms:false --type-system-refresh --allow-warnings "%s" > "%t"
 // NONUNIFORM: warning will be the same for all back-ends
 // RUN: ! %run --allow-axioms:false "%s" >> "%t"
 // RUN: %diff "%s.expect" "%t"
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/projectFile/projectFile.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/projectFile/projectFile.dfy
index f8691d186fa..187680cf63e 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/projectFile/projectFile.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/projectFile/projectFile.dfy
@@ -1,40 +1,40 @@
 // Invalid value gives error and stops compilation
-// RUN: ! %resolve --warn-shadowing=true %S/broken/invalidValue.toml 2> "%t"
+// RUN: ! %resolve --warn-shadowing=true %S/broken/invalidValue.toml &> "%t"
 
 // A project file can specify input files and configure options
-// RUN: %resolve "%S/dfyconfig.toml" >> "%t"
+// RUN: ! %resolve "%S/dfyconfig.toml" &>> "%t"
 
 // Test using a URL instead of a local file as a project file
-// RUN: ! %resolve "https://github.com/dafny-lang/dafny/blob/master/web.toml" 2>> %t
+// RUN: ! %resolve "https://github.com/dafny-lang/dafny/blob/master/web.toml" &>> %t
 
 // Test option override behavior
-// RUN: %resolve "%S/dfyconfig.toml" --warn-shadowing=false >> "%t"
+// RUN: %resolve "%S/dfyconfig.toml" --warn-shadowing=false &>> "%t"
 
 // Test option with default override behavior
-// RUN: ! %resolve "%S/dfyconfig.toml" --function-syntax=3 >> "%t"
+// RUN: ! %resolve "%S/dfyconfig.toml" --function-syntax=3 &>> "%t"
 
 // Multiple project files are not allowed
-// RUN: ! %resolve "%S/dfyconfig.toml" "%S/broken/dfyconfig.toml" 2>> %t
+// RUN: ! %resolve "%S/dfyconfig.toml" "%S/broken/dfyconfig.toml" &>> %t
 
 // Project files may not contain unknown properties
-// RUN: ! %resolve "%S/broken/dfyconfig.toml" 2>> %t
+// RUN: ! %resolve "%S/broken/dfyconfig.toml" &>> %t
 
 // Warn if file contains options that don't exist
-// RUN: %resolve "%S/broken/invalidOption.toml" >> "%t"
+// RUN: ! %resolve "%S/broken/invalidOption.toml" &>> "%t"
 
 // Project files must be files on disk.
-// RUN: ! %resolve "%S/doesNotExist.toml" 2>> %t
+// RUN: ! %resolve "%S/doesNotExist.toml" &>> %t
 
 // Project file options must have the right type
-// RUN: ! %resolve "%S/badTypes/dfyconfig.toml" >> "%t"
+// RUN: ! %resolve "%S/badTypes/dfyconfig.toml" &>> "%t"
 
 // A project file without includes will take all .dfy files as input
-// RUN: %resolve "%S/noIncludes/dfyconfig.toml" >> "%t"
+// RUN: ! %resolve "%S/noIncludes/dfyconfig.toml" &>> "%t"
 
 // Files included by the project file and on the CLI, duplicate is ignored.
-// RUN: %resolve "%S/dfyconfig.toml" "%S/src/input.dfy" >> "%t"
+// RUN: ! %resolve "%S/dfyconfig.toml" "%S/src/input.dfy" &>> "%t"
 
 // Files excluded by the project file and included on the CLI, are included
-// RUN: ! %resolve "%S/dfyconfig.toml" "%S/src/excluded.dfy" >> "%t"
+// RUN: ! %resolve "%S/dfyconfig.toml" "%S/src/excluded.dfy" &>> "%t"
 
 // RUN: %diff "%s.expect" "%t"
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/projectFile/projectFile.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/projectFile/projectFile.dfy.expect
index b13b069af36..6a3f7ba9852 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/projectFile/projectFile.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/projectFile/projectFile.dfy.expect
@@ -1,8 +1,8 @@
 Error: The Dafny project file invalidValue.toml contains the following errors: (3,14) : error : Unexpected token `NoIncludes` for a value
 
+Warning: only Dafny project files named dfyconfig.toml are recognised by the Dafny IDE.
 input.dfy(6,8): Warning: Shadowed local-variable name: x
-
-Dafny program verifier did not attempt verification
+Compilation failed because warnings were found and --allow-warnings is false
 Error: file web.toml not found
 
 Dafny program verifier did not attempt verification
@@ -14,17 +14,14 @@ Error: The Dafny project file dfyconfig.toml contains the following errors: (1,1
 Warning: only Dafny project files named dfyconfig.toml are recognised by the Dafny IDE.
 Warning: option 'does-not-exist' that was specified in the project file, is not a valid Dafny option.
 invalidOption.toml(1,0): Warning: only Dafny project files named dfyconfig.toml are recognised by the Dafny IDE.
-
-Dafny program verifier did not attempt verification
+Compilation failed because warnings were found and --allow-warnings is false
 Error: file doesNotExist.toml not found
 dfyconfig.toml(1,0): Error: could not parse value '3' for option 'warn-shadowing' that has type 'Boolean'
 input.dfy(6,8): Warning: Shadowed local-variable name: x
 moreInput.dfy(6,8): Warning: Shadowed local-variable name: x
-
-Dafny program verifier did not attempt verification
+Compilation failed because warnings were found and --allow-warnings is false
 input.dfy(6,8): Warning: Shadowed local-variable name: x
-
-Dafny program verifier did not attempt verification
+Compilation failed because warnings were found and --allow-warnings is false
 excluded.dfy(3,7): Error: Duplicate member name: Foo
 input.dfy(6,8): Warning: Shadowed local-variable name: x
 excluded.dfy(6,8): Warning: Shadowed local-variable name: z
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/cloudmake/CloudMake-CachedBuilds.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/cloudmake/CloudMake-CachedBuilds.dfy
index 499b64b33b8..5511b29226f 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/cloudmake/CloudMake-CachedBuilds.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/cloudmake/CloudMake-CachedBuilds.dfy
@@ -1,4 +1,4 @@
-// RUN: %verify --manual-triggers "%s" > "%t"
+// RUN: %verify --manual-triggers --allow-deprecation "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 // This module proves the correctness of the algorithms.  It leaves a number of things undefined.
@@ -959,7 +959,7 @@ abstract module M0 {
     ensures p.fst == pC.fst
     ensures StateCorrespondence(p.snd, pC.snd)
   {
-    assume |args| == Arity(primExec) ==>
+    assume {:axiom} |args| == Arity(primExec) ==>
       ValidArgs(primExec, args, stCombined) == ValidArgs(primExec, args, stCombinedC);  // TODO:  This will require some work!
 
     if |args| == Arity(primExec) && ValidArgs(primExec, args, stCombined) {
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/cloudmake/CloudMake-CachedBuilds.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/cloudmake/CloudMake-CachedBuilds.dfy.expect
index 3216b1d7c7d..a4d7ffedb36 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/cloudmake/CloudMake-CachedBuilds.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/cloudmake/CloudMake-CachedBuilds.dfy.expect
@@ -1,6 +1,2 @@
-CloudMake-CachedBuilds.dfy(107,6): Warning: a forall statement with no bound variables is deprecated; use an 'assert by' statement instead
-CloudMake-CachedBuilds.dfy(447,4): Warning: a forall statement with no bound variables is deprecated; use an 'assert by' statement instead
-CloudMake-CachedBuilds.dfy(1249,8): Warning: a forall statement with no bound variables is deprecated; use an 'assert by' statement instead
-CloudMake-CachedBuilds.dfy(962,4): Warning: assume statement has no {:axiom} annotation
 
 Dafny program verifier finished with 76 verified, 0 errors
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/cloudmake/CloudMake-ParallelBuilds.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/cloudmake/CloudMake-ParallelBuilds.dfy
index 0dd0d35942c..90eb085b47f 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/cloudmake/CloudMake-ParallelBuilds.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/cloudmake/CloudMake-ParallelBuilds.dfy
@@ -1,4 +1,4 @@
-// RUN: %verify --relax-definite-assignment --manual-triggers "%s" > "%t"
+// RUN: %verify --relax-definite-assignment --manual-triggers --allow-deprecation "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 // This module proves the correctness of the algorithms.  It leaves a number of things undefined.
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/cloudmake/CloudMake-ParallelBuilds.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/cloudmake/CloudMake-ParallelBuilds.dfy.expect
index 3cebd6e69a8..f397c7f3388 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/cloudmake/CloudMake-ParallelBuilds.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/cloudmake/CloudMake-ParallelBuilds.dfy.expect
@@ -1,3 +1,2 @@
-CloudMake-ParallelBuilds.dfy(562,6): Warning: a forall statement with no bound variables is deprecated; use an 'assert by' statement instead
 
 Dafny program verifier finished with 101 verified, 0 errors
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/DirtyLoops.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/DirtyLoops.dfy
index f96f5810646..ecb6919530a 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/DirtyLoops.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/DirtyLoops.dfy
@@ -1,5 +1,5 @@
 // RUN: %exits-with 4 %verify --relax-definite-assignment --print:"%t.dprint.dfy" "%s" > "%t"
-// RUN: %resolve "%t.dprint.dfy" >> "%t"
+// RUN: %resolve "%t.dprint.dfy" --allow-warnings >> "%t"
 // RUN: %diff "%s.expect" "%t"
 
 // For a body-less loop specification, a local variable or
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ISets.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ISets.dfy
index fced236863c..ccb837a7d66 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ISets.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ISets.dfy
@@ -35,9 +35,9 @@ ghost method m1() {
  assert s2 - s3 == iset{3}; // set difference
 
  assert (iset x | x in s2 :: x+1) == iset{2,3,4}; // set comprehension
- assert 17 in (iset x: int | true :: x); // set comprehension
+ assert 17 in (iset x: int {:trigger} | true :: x); // set comprehension
 
- assert (imap x: int | true :: x+1)[14] == 15;
+ assert (imap x: int {:trigger} | true :: x+1)[14] == 15;
 }
 
 
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ISets.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ISets.dfy.expect
index e07c395e639..ebe2328e072 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ISets.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ISets.dfy.expect
@@ -1,4 +1,2 @@
-ISets.dfy(38,15): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual.
-ISets.dfy(40,9): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual.
 
 Dafny program verifier finished with 2 verified, 0 errors
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/JustWarnings.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/JustWarnings.dfy
index a6d4239363e..c3380be4cf1 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/JustWarnings.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/JustWarnings.dfy
@@ -1,4 +1,4 @@
-// RUN: %testDafnyForEachResolver "%s" -- --warn-shadowing
+// RUN: %testDafnyForEachResolver "%s" -- --warn-shadowing --allow-warnings
 
 
 // This file tests the behavior where the Resolver reports some warnings
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/PrecedenceLinter.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/PrecedenceLinter.dfy
index df4a2058480..5eb498de61c 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/PrecedenceLinter.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/PrecedenceLinter.dfy
@@ -1,4 +1,4 @@
-// RUN: %resolve "%s" > "%t"
+// RUN: %resolve "%s" --allow-warnings > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 ghost predicate P0(A: bool, B: bool, C: bool) {
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/SmallTests.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/SmallTests.dfy
index f7dc8f1792a..7402392fd87 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/SmallTests.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/SmallTests.dfy
@@ -1,5 +1,5 @@
 // RUN: %exits-with 4 %verify --relax-definite-assignment --allow-axioms --allow-deprecation --print "%t.dprint.dfy" "%s" > "%t"
-// RUN: %resolve --allow-axioms "%t.dprint.dfy" >> "%t"
+// RUN: %resolve --allow-axioms --allow-warnings "%t.dprint.dfy" >> "%t"
 // RUN: %diff "%s.expect" "%t"
 
 class Node {
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Stdin.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Stdin.dfy
index 74cd0093ada..adb6e495710 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Stdin.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Stdin.dfy
@@ -1,6 +1,6 @@
 // RUN: %exits-with 0 %stdin "module A{}" %baredafny verify --show-snippets:false --stdin > "%t"
 // RUN: %exits-with 4 %stdin "method a() { assert false; }" %baredafny verify --show-snippets:false --stdin >> "%t"
-// RUN: %exits-with 0 %stdin "" %baredafny verify --show-snippets:false --stdin >> "%t"
+// RUN: %exits-with 0 %stdin "" %baredafny verify --allow-warnings --show-snippets:false --stdin >> "%t"
 // Ensuring include statements work when processing standard in too
 // (regression test for https://github.com/dafny-lang/dafny/issues/4135)
 // We don't capture the output to %t because it ends up including paths,
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny1/SchorrWaite-stages.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny1/SchorrWaite-stages.dfy
index a46373e26cb..e5ed5eaa8d7 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny1/SchorrWaite-stages.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny1/SchorrWaite-stages.dfy
@@ -1,4 +1,4 @@
-// RUN: %testDafnyForEachResolver "%s"
+// RUN: %testDafnyForEachResolver "%s" -- --allow-deprecation
 
 
 // Schorr-Waite algorithms, written and verified in Dafny.
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny1/SchorrWaite-stages.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny1/SchorrWaite-stages.dfy.expect
index 4ea2437c20d..851aaf58286 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny1/SchorrWaite-stages.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny1/SchorrWaite-stages.dfy.expect
@@ -1,23 +1,2 @@
-SchorrWaite-stages.dfy(149,7): Warning: the ... refinement feature in statements is deprecated
-SchorrWaite-stages.dfy(150,10): Warning: the ... refinement feature in statements is deprecated
-SchorrWaite-stages.dfy(161,9): Warning: the ... refinement feature in statements is deprecated
-SchorrWaite-stages.dfy(162,16): Warning: the ... refinement feature in statements is deprecated
-SchorrWaite-stages.dfy(164,11): Warning: the ... refinement feature in statements is deprecated
-SchorrWaite-stages.dfy(168,15): Warning: the ... refinement feature in statements is deprecated
-SchorrWaite-stages.dfy(174,11): Warning: the ... refinement feature in statements is deprecated
-SchorrWaite-stages.dfy(175,11): Warning: the ... refinement feature in statements is deprecated
-SchorrWaite-stages.dfy(201,7): Warning: the ... refinement feature in statements is deprecated
-SchorrWaite-stages.dfy(202,10): Warning: the ... refinement feature in statements is deprecated
-SchorrWaite-stages.dfy(221,9): Warning: the ... refinement feature in statements is deprecated
-SchorrWaite-stages.dfy(223,11): Warning: the ... refinement feature in statements is deprecated
-SchorrWaite-stages.dfy(225,16): Warning: the ... refinement feature in statements is deprecated
-SchorrWaite-stages.dfy(230,11): Warning: the ... refinement feature in statements is deprecated
-SchorrWaite-stages.dfy(236,11): Warning: the ... refinement feature in statements is deprecated
-SchorrWaite-stages.dfy(239,11): Warning: the ... refinement feature in statements is deprecated
-SchorrWaite-stages.dfy(255,7): Warning: the ... refinement feature in statements is deprecated
-SchorrWaite-stages.dfy(256,10): Warning: the ... refinement feature in statements is deprecated
-SchorrWaite-stages.dfy(260,9): Warning: the ... refinement feature in statements is deprecated
-SchorrWaite-stages.dfy(261,16): Warning: the ... refinement feature in statements is deprecated
-SchorrWaite-stages.dfy(263,11): Warning: the ... refinement feature in statements is deprecated
 
 Dafny program verifier finished with 7 verified, 0 errors
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny2/MonotonicHeapstate.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny2/MonotonicHeapstate.dfy
index e0257ba6ec3..0f666e6e506 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny2/MonotonicHeapstate.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny2/MonotonicHeapstate.dfy
@@ -1,4 +1,4 @@
-// RUN: %testDafnyForEachResolver "%s"
+// RUN: %testDafnyForEachResolver "%s" -- --allow-deprecation
 
 
 module M0 {
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny2/MonotonicHeapstate.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny2/MonotonicHeapstate.dfy.expect
index f015f6885ea..25822a5c6cc 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny2/MonotonicHeapstate.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny2/MonotonicHeapstate.dfy.expect
@@ -1,7 +1,2 @@
-MonotonicHeapstate.dfy(92,13): Warning: the ... refinement feature in statements is deprecated
-MonotonicHeapstate.dfy(99,13): Warning: the ... refinement feature in statements is deprecated
-MonotonicHeapstate.dfy(106,13): Warning: the ... refinement feature in statements is deprecated
-MonotonicHeapstate.dfy(146,9): Warning: the ... refinement feature in statements is deprecated
-MonotonicHeapstate.dfy(147,13): Warning: the ... refinement feature in statements is deprecated
 
 Dafny program verifier finished with 24 verified, 0 errors
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny3/InductionVsCoinduction.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny3/InductionVsCoinduction.dfy
index e94b03b727c..0bb116a1692 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny3/InductionVsCoinduction.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny3/InductionVsCoinduction.dfy
@@ -78,7 +78,7 @@ lemma {:induction false} SAppendIsAssociativeK(k:nat, a:Stream, b:Stream, c:Stre
 lemma SAppendIsAssociative(a:Stream, b:Stream, c:Stream)
   ensures SAppend(SAppend(a, b), c) == SAppend(a, SAppend(b, c));
 {
-  forall k:nat { SAppendIsAssociativeK(k, a, b, c); }
+  forall k:nat {:trigger} { SAppendIsAssociativeK(k, a, b, c); }
   // assert for clarity only, postcondition follows directly from it
   assert (forall k:nat {:autotriggers false} :: SAppend(SAppend(a, b), c) ==#[k] SAppend(a, SAppend(b, c))); //FIXME: Should Dafny generate a trigger here? If so then which one?
 }
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny3/InductionVsCoinduction.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny3/InductionVsCoinduction.dfy.expect
index 73aebefff54..e5f9ee5a233 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny3/InductionVsCoinduction.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny3/InductionVsCoinduction.dfy.expect
@@ -1,3 +1,2 @@
-InductionVsCoinduction.dfy(81,2): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual.
 
 Dafny program verifier finished with 12 verified, 0 errors
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny3/Streams.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny3/Streams.dfy
index 2118c9dcc07..0ffe3988ec1 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny3/Streams.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny3/Streams.dfy
@@ -62,7 +62,7 @@ greatest lemma Theorem0_Alt(M: Stream<X>)
 lemma Theorem0_Par(M: Stream<X>)
   ensures map_fg(M) == map_f(map_g(M));
 {
-  forall k: nat {
+  forall k: nat {:trigger} {
     Theorem0_Ind(k, M);
   }
 }
@@ -102,7 +102,7 @@ greatest lemma Theorem1_Alt(M: Stream<X>, N: Stream<X>)
 lemma Theorem1_Par(M: Stream<X>, N: Stream<X>)
   ensures map_f(append(M, N)) == append(map_f(M), map_f(N));
 {
-  forall k: nat {
+  forall k: nat {:trigger} {
     Theorem1_Ind(k, M, N);
   }
 }
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny3/Streams.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny3/Streams.dfy.expect
index a08ea0c11dc..9e74af046b4 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny3/Streams.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny3/Streams.dfy.expect
@@ -1,4 +1,2 @@
-Streams.dfy(65,2): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual.
-Streams.dfy(105,2): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual.
 
 Dafny program verifier finished with 29 verified, 0 errors
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Bug121.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Bug121.dfy
index ed12bf32722..914b90ffbf0 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Bug121.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Bug121.dfy
@@ -1,4 +1,4 @@
-// RUN: %testDafnyForEachResolver "%s"
+// RUN: %testDafnyForEachResolver "%s" -- --allow-warnings
 
 
 method Try (a:int, b:int, c:int)
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Bug122.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Bug122.dfy
index 4be16d622d7..594b274d52d 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Bug122.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Bug122.dfy
@@ -1,4 +1,4 @@
-// RUN: %testDafnyForEachResolver "%s"
+// RUN: %testDafnyForEachResolver "%s" -- --allow-warnings
 
 
 method Try (a:int)
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Bug142.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Bug142.dfy
index 3224df84312..0796b715c13 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Bug142.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Bug142.dfy
@@ -1,4 +1,4 @@
-// RUN: %resolve --warn-shadowing "%s" > "%t"
+// RUN: %resolve --warn-shadowing --allow-warnings "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 ghost function P(x:int):int
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Regression1.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Regression1.dfy
index 34382ea05c1..c07347d1bf8 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Regression1.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Regression1.dfy
@@ -1,4 +1,4 @@
-// RUN: %testDafnyForEachResolver "%s"
+// RUN: %testDafnyForEachResolver "%s" -- --allow-warnings
 
 
 ghost method M() {
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue1.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue1.dfy
index f3dca105a6c..7c660053156 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue1.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue1.dfy
@@ -1,4 +1,4 @@
-// RUN: %testDafnyForEachResolver "%s"
+// RUN: %testDafnyForEachResolver "%s" -- --allow-warnings
 
 
 datatype T = T(n:int)
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue18.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue18.dfy
index dd6abb8ae74..ad3a3a76dea 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue18.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue18.dfy
@@ -1,4 +1,4 @@
-// RUN: %testDafnyForEachResolver "%s"
+// RUN: %testDafnyForEachResolver "%s" -- --allow-warnings
 
 
 datatype Maybe = Nothing | Just
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue22.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue22.dfy
index 3bac5d690a9..e929b1dbbaf 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue22.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue22.dfy
@@ -1,4 +1,4 @@
-// RUN: %testDafnyForEachResolver "%s"
+// RUN: %testDafnyForEachResolver "%s" -- --allow-warnings
 
 
 ghost predicate bad()
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue42.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue42.dfy
index 612c5528a26..0da1f6ce98b 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue42.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue42.dfy
@@ -1,4 +1,4 @@
-// RUN: %verify --warn-shadowing "%s" > "%t"
+// RUN: %verify --warn-shadowing --allow-warnings "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 lemma L(x:int)
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue48.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue48.dfy
index 1d2b776a69a..cb232154321 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue48.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue48.dfy
@@ -1,4 +1,4 @@
-// RUN: %testDafnyForEachResolver "%s"
+// RUN: %testDafnyForEachResolver "%s" -- --allow-warnings
 
 
 include "git-issue48-include.dfyi"
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue75.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue75.dfy
index 9c833d86526..37b4a2f292d 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue75.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue75.dfy
@@ -1,4 +1,4 @@
-// RUN: %verify "%s" > "%t"
+// RUN: %verify "%s" --allow-warnings > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 type t = i:int | 0 <= i < 10
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue92.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue92.dfy
index dfd9e1967e1..c3c1d34bcd5 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue92.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue92.dfy
@@ -1,4 +1,4 @@
-// RUN: %testDafnyForEachResolver "%s"
+// RUN: %testDafnyForEachResolver "%s" -- --allow-warnings
 
 
 datatype d = D(i:int)
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue96.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue96.dfy
index ece6846e075..861b465368b 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue96.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue96.dfy
@@ -1,4 +1,4 @@
-// RUN: %testDafnyForEachResolver "%s"
+// RUN: %testDafnyForEachResolver "%s" -- --allow-warnings
 
 
 ghost predicate P(s:seq<int>)
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/doofiles/allowWarningsDoo.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/doofiles/allowWarningsDoo.dfy
index 09744e91a4d..0f55dec43a3 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/doofiles/allowWarningsDoo.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/doofiles/allowWarningsDoo.dfy
@@ -1,5 +1,5 @@
-// RUN: %build %s -t:lib --allow-warnings --output="%S/Output/allowWarnings.doo" > "%t"
-// RUN: %resolve %s %S/Output/allowWarnings.doo >> %t
+// RUN: %build %s -t:lib --allow-warnings --output="%S/Output/allowWarnings.doo" &> "%t"
+// RUN: ! %stdin "method Bar() { }" %resolve --stdin %S/Output/allowWarnings.doo &>> %t
 // RUN: %diff "%s.expect" "%t"
 
 method Foo() {
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/doofiles/allowWarningsDoo.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/doofiles/allowWarningsDoo.dfy.expect
index 06400d05c3a..2a1bfb0eddf 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/doofiles/allowWarningsDoo.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/doofiles/allowWarningsDoo.dfy.expect
@@ -1,5 +1,4 @@
 
 Dafny program verifier finished with 0 verified, 0 errors
 CLI: Warning: cannot load allowWarnings.doo: --allow-warnings is set locally to False, but the library was built with True
-
-Dafny program verifier did not attempt verification
+Compilation failed because warnings were found and --allow-warnings is false
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-032a.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-032a.dfy
index 25970f3d615..08dae444dcc 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-032a.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-032a.dfy
@@ -1,4 +1,4 @@
-// RUN: %testDafnyForEachResolver "%s"
+// RUN: %testDafnyForEachResolver "%s" -- --allow-warnings
 
 
 method m() {
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2026.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2026.dfy
index 07d945681f1..9c250624fb8 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2026.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2026.dfy
@@ -1,4 +1,4 @@
-// RUN: %exits-with 4 %baredafny verify --extract-counterexample "%s" > "%t"
+// RUN: %exits-with 4 %verify --extract-counterexample "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 // NB: with recent Z3 versions (e.g., 4.12.1), this program no longer
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2026.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2026.dfy.expect
index bbd416ec0a8..6e0c90512a3 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2026.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2026.dfy.expect
@@ -1,36 +1,32 @@
-TestFiles/LitTests/LitTest/git-issues/git-issue-2026.dfy(18,18): Error: this invariant could not be proved to be maintained by the loop
+git-issue-2026.dfy(18,18): Error: this invariant could not be proved to be maintained by the loop
  Related message: loop invariant violation
  Related counterexample:
- TestFiles/LitTests/LitTest/git-issues/git-issue-2026.dfy(12,0): initial state:
+ git-issue-2026.dfy(12,0): initial state:
  	n : int = 2
  	ret : ? = ?
- TestFiles/LitTests/LitTest/git-issues/git-issue-2026.dfy(13,24):
+ git-issue-2026.dfy(13,24):
  	n : int = 2
  	ret : _System.array?<seq<char>> = (Length := 2, [0] := @0)
  	@0 : seq<char> = ['o', 'd', 'd']
- TestFiles/LitTests/LitTest/git-issues/git-issue-2026.dfy(15,14):
+ git-issue-2026.dfy(15,14):
  	n : int = 2
  	ret : _System.array?<seq<char>> = (Length := 2, [0] := @0)
  	i : int = 0
  	@0 : seq<char> = ['o', 'd', 'd']
- TestFiles/LitTests/LitTest/git-issues/git-issue-2026.dfy(16,4): after some loop iterations:
+ git-issue-2026.dfy(16,4): after some loop iterations:
  	n : int = 2
  	ret : _System.array?<seq<char>> = (Length := 2)
  	i : int = 0
- TestFiles/LitTests/LitTest/git-issues/git-issue-2026.dfy(22,27):
+ git-issue-2026.dfy(22,27):
  	n : int = 2
  	ret : _System.array?<seq<char>> = (Length := 2, [0] := @0)
  	i : int = 0
  	@0 : seq<char> = ['o', 'd', 'd']
- TestFiles/LitTests/LitTest/git-issues/git-issue-2026.dfy(26,18):
+ git-issue-2026.dfy(26,18):
  	n : int = 2
  	ret : _System.array?<seq<char>> = (Length := 2, [0] := @0)
  	i : int = 1
  	@0 : seq<char> = ['o', 'd', 'd']
  
-   |
-18 |         invariant forall j :: 0 <= j < i ==> j % 2 == 0 ==> ret[j] == "even"
-   |                   ^^^^^^
-
 
 Dafny program verifier finished with 0 verified, 1 error
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2265.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2265.dfy
index 31d39b38524..1bbd3648816 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2265.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2265.dfy
@@ -1,4 +1,4 @@
-// RUN: %testDafnyForEachResolver "%s"
+// RUN: %testDafnyForEachResolver "%s" -- --allow-warnings
 
 
 module DefaultModule {
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2593.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2593.dfy
index fb26738788c..f2011067c28 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2593.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2593.dfy
@@ -1,4 +1,4 @@
-// RUN: %testDafnyForEachResolver "%s"
+// RUN: %testDafnyForEachResolver "%s" -- --allow-warnings
 
 
 ghost predicate P(x: int)
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2747.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2747.dfy
index ce214ae6a95..69ad728a878 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2747.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2747.dfy
@@ -1,4 +1,4 @@
-// RUN: %testDafnyForEachResolver "%s"
+// RUN: %testDafnyForEachResolver "%s" -- --allow-warnings
 
 
 ghost function AnotherBrokenFunction(): nat {
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3288c.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3288c.dfy
index e7f93ed7ead..c59a2794f98 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3288c.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3288c.dfy
@@ -1,4 +1,4 @@
-// RUN: %verify "%s" > "%t"
+// RUN: %verify "%s" --allow-warnings > "%t"
 // RUN: %diff "%s.expect" "%t" 
 
 module M {
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3358.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3358.dfy
index dd79f2faaa6..01b25cc589f 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3358.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3358.dfy
@@ -1,4 +1,4 @@
-// RUN: %verify "%s" > "%t"
+// RUN: %verify "%s" --allow-warnings > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 datatype MyResult = Ok | Err(error: set<string>)
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3496.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3496.dfy
index 62f2adbcb7f..f78785490b3 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3496.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3496.dfy
@@ -1,4 +1,4 @@
-// RUN: %resolve --allow-axioms:false "%s" > "%t"
+// RUN: %resolve --allow-axioms:false --allow-warnings "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 method m() {
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3497.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3497.dfy
index d452775c850..f6a4d39e0b7 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3497.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3497.dfy
@@ -1,4 +1,4 @@
-// RUN: %resolve "%s" > "%t"
+// RUN: %resolve "%s" --allow-warnings > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 method m() {
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4778.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4778.dfy
index 5cc6f56d8a0..216baa17c0e 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4778.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4778.dfy
@@ -1,4 +1,4 @@
-// RUN: %verify --warn-contradictory-assumptions "%s" > "%t"
+// RUN: %verify --warn-contradictory-assumptions --allow-warnings "%s" > "%t"
 // DIFF: "%s.expect" "%t"
 
 type CodeUnit
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-845.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-845.dfy
index cc9976fd91f..667632373fd 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-845.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-845.dfy
@@ -1,4 +1,4 @@
-// RUN: %verify %S/git-issue-845.dfy > "%t"
+// RUN: %verify %S/git-issue-845.dfy --allow-warnings > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 /* blah blah /* blah */
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-897a.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-897a.dfy
index 8fb9494c819..6cc88379b33 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-897a.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-897a.dfy
@@ -7,7 +7,7 @@ ghost function missing_number(nums: seq<nat>): nat
 {
   var p := x => 0 <= x <= |nums| && x !in nums;
   assert exists x :: p(x) && forall y :: p(y) ==> y == x by {
-    var range := set i | 0 <= i <= |nums|;
+    var range := set i {:trigger} | 0 <= i <= |nums|;
     assume |range| == |nums| + 1;
     var missing := range - set i | i in nums;
     assert |missing| == 1;
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-897a.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-897a.dfy.expect
index b2b4a91b6f8..823a60a105c 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-897a.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-897a.dfy.expect
@@ -1,3 +1,2 @@
-git-issue-897a.dfy(10,17): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual.
 
 Dafny program verifier finished with 1 verified, 0 errors
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/github-issue-4144.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/github-issue-4144.dfy
index 070c277615b..745cfad7313 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/github-issue-4144.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/github-issue-4144.dfy
@@ -1,4 +1,4 @@
-// RUN: %verify %s > %t
+// RUN: %verify --allow-warnings %s > %t
 // RUN: %diff "%s.expect" "%t"
 
 module P {
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/SumSum.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/SumSum.dfy
index 51c687cea96..4a7f8894e41 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/SumSum.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/SumSum.dfy
@@ -74,7 +74,7 @@ lemma BetaReductionInside(n': nat, g: (int,int) -> int)
   ensures Sum(n', x => g(x,n') + Sum(n', y => g(x,y)))
        == Sum(n', x => (w => g(w,n'))(x) + (w => Sum(n', y => g(w,y)))(x))
 {
-  forall i | 0 <= i < n'
+  forall i {:trigger} | 0 <= i < n'
   {
     calc {
       (x => g(x,n') + Sum(n', y => g(x,y)))(i);
@@ -103,7 +103,7 @@ lemma L(n: nat, n': nat, g: (int, int) -> int)
     { assert (y => g(n',y))(n') == g(n',n'); }
     g(n',n') + Sum(n', y => g(n',y)) + Sum(n', x => Sum(n, y => g(x,y)));
     {
-      forall i | 0 <= i < n' {
+      forall i {:trigger} | 0 <= i < n' {
         calc {
           (x => Sum(n, y => g(x,y)))(i);
           { PrettyBasicBetaReduction(n, g, i); }
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/SumSum.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/SumSum.dfy.expect
index 081616a94b4..ccc01c35f48 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/SumSum.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/SumSum.dfy.expect
@@ -1,4 +1,2 @@
-SumSum.dfy(77,2): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual.
-SumSum.dfy(106,6): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual.
 
 Dafny program verifier finished with 11 verified, 0 errors
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/linters/constructorCaseWithoutParentheses.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/linters/constructorCaseWithoutParentheses.dfy
index c93907cc5a9..19ec978d8bf 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/linters/constructorCaseWithoutParentheses.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/linters/constructorCaseWithoutParentheses.dfy
@@ -1,4 +1,4 @@
-// RUN: %verify --warn-missing-constructor-parentheses "%s" > "%t"
+// RUN: %verify --warn-missing-constructor-parentheses "%s" --allow-warnings > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 module WithWarning {
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencyWarnings.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencyWarnings.dfy
index 6b5f52e5bde..5ef994e089f 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencyWarnings.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencyWarnings.dfy
@@ -1,4 +1,4 @@
-// RUN: %baredafny verify --use-basename-for-filename --allow-axioms --show-snippets false --verify-included-files --warn-contradictory-assumptions --warn-redundant-assumptions "%s" > "%t.new"
+// RUN: %baredafny verify --use-basename-for-filename --allow-axioms --show-snippets false --verify-included-files --warn-contradictory-assumptions --warn-redundant-assumptions --allow-warnings "%s" > "%t.new"
 // RUN: %diff "%s.expect" "%t.new"
 // RUN: %baredafny /compile:0 /useBaseNameForFileName /verifyAllModules /warnContradictoryAssumptions /warnRedundantAssumptions "%s" > "%t.old"
 // RUN: %diff "%s.expect" "%t.old"
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/metatests/TestMissingVerifierExpect.dfy.testdafny.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/metatests/TestMissingVerifierExpect.dfy.testdafny.expect
index 4a06fe9d9b3..b73dd50e4ae 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/metatests/TestMissingVerifierExpect.dfy.testdafny.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/metatests/TestMissingVerifierExpect.dfy.testdafny.expect
@@ -2,5 +2,6 @@ Using legacy resolver and verifying...
 AssertEqualWithDiff() Failure
 Diff (changing expected into actual):
 +TestMissingVerifierExpect.dfy(6,5): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual.
++Compilation failed because warnings were found and --allow-warnings is false
 +
 
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/metatests/TestWrongVerifierExpect.dfy.testdafny.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/metatests/TestWrongVerifierExpect.dfy.testdafny.expect
index fe05592e8ad..a619131d401 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/metatests/TestWrongVerifierExpect.dfy.testdafny.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/metatests/TestWrongVerifierExpect.dfy.testdafny.expect
@@ -3,5 +3,6 @@ AssertEqualWithDiff() Failure
 Diff (changing expected into actual):
 -warning: out of bananas
 +TestWrongVerifierExpect.dfy(6,5): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual.
++Compilation failed because warnings were found and --allow-warnings is false
  
 
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/loop-detection-messages--unit-tests.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/loop-detection-messages--unit-tests.dfy
index 6a32aaadbbc..5b3d54288c6 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/loop-detection-messages--unit-tests.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/loop-detection-messages--unit-tests.dfy
@@ -1,4 +1,4 @@
-// RUN: %verify --show-inference "%s" > "%t"
+// RUN: %verify --show-inference --allow-warnings "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 // This file is a series of basic tests for loop detection, focusing on the
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/old-is-a-special-case-for-triggers.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/old-is-a-special-case-for-triggers.dfy
index a18aee5db56..8d0edd0e2ab 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/old-is-a-special-case-for-triggers.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/old-is-a-special-case-for-triggers.dfy
@@ -1,4 +1,4 @@
-// RUN: %verify --show-inference "%s" > "%t"
+// RUN: %verify --show-inference "%s" --allow-warnings > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 // This file ensures that `old()` receives the special treatment that it
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/regression-tests.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/regression-tests.dfy
index 8bf9dbd2e77..4e5320d0898 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/regression-tests.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/regression-tests.dfy
@@ -1,4 +1,4 @@
-// RUN: %verify --show-inference "%s" > "%t"
+// RUN: %verify --show-inference "%s" --allow-warnings > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 // This tests checks that quantifier splitting is resilient to the fact that
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/suppressing-warnings-behaves-properly.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/suppressing-warnings-behaves-properly.dfy
index 8f23b16acec..ce7f477d011 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/suppressing-warnings-behaves-properly.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/suppressing-warnings-behaves-properly.dfy
@@ -1,4 +1,4 @@
-// RUN: %verify --show-inference "%s" > "%t"
+// RUN: %verify --show-inference --allow-warnings "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 // This file checks that suppressing warnings works properly
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/filter.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/filter.dfy
index 0db23fb8333..c5cb15cc764 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/filter.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/filter.dfy
@@ -1,4 +1,4 @@
-// RUN: %verify --filter-position='C:\windows\path.dfy' %s > %t
+// RUN: %verify --allow-warnings --filter-position='C:\windows\path.dfy' %s > %t
 // RUN: ! %verify --filter-position='src/source1.dfy:5' %S/Inputs/dfyconfig.toml >> %t
 // RUN: %verify --filter-position='src/source1.dfy:1' %S/Inputs/dfyconfig.toml >> %t
 // RUN: ! %verify --filter-position='e.dfy' %S/Inputs/single-file.dfy >> %t
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/wishlist/we-should-always-print-tooltips.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/wishlist/we-should-always-print-tooltips.dfy
index 85b5a7b0ae7..8a3069f419a 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/wishlist/we-should-always-print-tooltips.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/wishlist/we-should-always-print-tooltips.dfy
@@ -1,4 +1,4 @@
-// RUN: %verify --show-inference %s > "%t"
+// RUN: %verify --show-inference --allow-warnings %s > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 // WISH it would be great to add /printTooltips to all tests
diff --git a/docs/DafnyRef/Modules.md b/docs/DafnyRef/Modules.md
index ab757469ce9..31ee26bbfe1 100644
--- a/docs/DafnyRef/Modules.md
+++ b/docs/DafnyRef/Modules.md
@@ -352,9 +352,8 @@ Examples:
 ```dafny
 export E extends F reveals f,g provides g,h
 export E reveals *
-export reveals f
+export reveals f,g provides g,h
 export E
-export
 export E ... reveals f
 ```
 
@@ -375,15 +374,16 @@ module using the `import` mechanism.
 An _export set_ enables a module to disallow the
 use of some declarations outside the module.
 
-Export sets have names; those names are used in `import` statements to
-designate which export set of a module is being imported.
-If a module `M` has export sets
-`E1` and `E2`, we can write ``import A = M`E1`` to create a module alias
-`A` that contains only the
-names in `E1`. Or we can write ``import A = M`{E1,E2}`` to import the union
+An export set has an optional name used to disambiguate
+in case of multiple export sets;
+If specified, such names are used in `import` statements
+to designate which export set of a module is being imported.
+If a module `M` has export sets `E1` and `E2`,
+we can write ``import A = M`E1`` to create a module alias
+`A` that contains only the names in `E1`.
+Or we can write ``import A = M`{E1,E2}`` to import the union
 of names in `E1` and `E2` as module alias `A`.
-As before, ``import M`E1`` is an
-abbreviation of ``import M = M`E1``.
+As before, ``import M`E1`` is an abbreviation of ``import M = M`E1``.
 
 If no export set is given in an import
 statement, the default export set of the module is used.
diff --git a/docs/check-examples b/docs/check-examples
index d716422a203..e43a9acb198 100755
--- a/docs/check-examples
+++ b/docs/check-examples
@@ -340,6 +340,7 @@ do
         if [ -z "$expect" -a "$useHeadings" == "0" ]; then
           defaultExit=0
         elif [ "$iswarn" == "1" ]; then
+          dOptions="$dOptions --allow-warnings"
           defaultExit=0
         elif [ "$verb" == "verify" ]; then
           defaultExit=4