diff --git a/Source/TestDafny/MultiBackendTest.cs b/Source/TestDafny/MultiBackendTest.cs
index 35907c196a5..09890fce07d 100644
--- a/Source/TestDafny/MultiBackendTest.cs
+++ b/Source/TestDafny/MultiBackendTest.cs
@@ -94,6 +94,22 @@ private int ForEachCompiler(ForEachCompilerOptions options) {
     output.WriteLine("Verifying...");
 
     var (exitCode, outputString, error) = RunDafny(options.DafnyCliPath, dafnyArgs);
+    // If there is a .verifier.expect file, then we expect the output to match the .verifier.expect file contents. Otherwise, we
+    // expect the output to be empty.
+    var expectedOutput = "";
+    var expectFileForVerifier = $"{options.TestFile}.verifier.expect";
+    if (File.Exists(expectFileForVerifier)) {
+      expectedOutput = File.ReadAllText(expectFileForVerifier);
+    }
+    // Chop off the "Dafny program verifier finished with..." trailer
+    var trailer = new Regex("\r?\nDafny program verifier[^\r\n]*\r?\n").Match(outputString);
+    var actualOutput = outputString.Remove(trailer.Index, trailer.Length);
+    var diffMessage = AssertWithDiff.GetDiffMessage(expectedOutput, actualOutput);
+    if (diffMessage != null) {
+      output.WriteLine(diffMessage);
+      return 1;
+    }
+    // We expect verification to return exit code 0.
     if (exitCode != 0) {
       output.WriteLine("Verification failed. Output:");
       output.WriteLine(outputString);
@@ -101,26 +117,11 @@ private int ForEachCompiler(ForEachCompilerOptions options) {
       output.WriteLine(error);
       return exitCode;
     }
-    var expectFileForVerifier = $"{options.TestFile}.verifier.expect";
-    if (File.Exists(expectFileForVerifier)) {
-      var expectedOutput = File.ReadAllText(expectFileForVerifier);
-      // Chop off the "Dafny program verifier finished with..." trailer
-      var trailer = new Regex("\r?\nDafny program verifier[^\r\n]*\r?\n").Match(outputString);
-      var actualOutput = outputString.Remove(trailer.Index, trailer.Length);
-      var diffMessage = AssertWithDiff.GetDiffMessage(expectedOutput, actualOutput);
-      if (diffMessage == null) {
-        return 0;
-      }
-
-      output.WriteLine(diffMessage);
-      return 1;
-    }
 
     // Then execute the program for each available compiler.
 
     string expectFile = options.TestFile + ".expect";
-    var commonExpectedOutput = "\nDafny program verifier did not attempt verification\n" +
-                         File.ReadAllText(expectFile);
+    var commonExpectedOutput = File.ReadAllText(expectFile);
 
     var success = true;
     foreach (var plugin in dafnyOptions.Plugins) {
@@ -132,12 +133,11 @@ private int ForEachCompiler(ForEachCompilerOptions options) {
         }
 
         // Check for backend-specific exceptions (because of known bugs or inconsistencies)
-        var expectedOutput = commonExpectedOutput;
+        expectedOutput = commonExpectedOutput;
         string? checkFile = null;
         var expectFileForBackend = $"{options.TestFile}.{compiler.TargetId}.expect";
         if (File.Exists(expectFileForBackend)) {
-          expectedOutput = "\nDafny program verifier did not attempt verification\n" +
-                           File.ReadAllText(expectFileForBackend);
+          expectedOutput = File.ReadAllText(expectFileForBackend);
         }
         var checkFileForBackend = $"{options.TestFile}.{compiler.TargetId}.check";
         if (File.Exists(checkFileForBackend)) {
@@ -185,6 +185,10 @@ private int RunWithCompiler(ForEachCompilerOptions options, IExecutableBackend b
     }.Concat(options.OtherArgs);
 
     var (exitCode, outputString, error) = RunDafny(options.DafnyCliPath, dafnyArgs);
+    var compilationOutputPrior = new Regex("\r?\nDafny program verifier[^\r\n]*\r?\n").Match(outputString);
+    if (compilationOutputPrior.Success) {
+      outputString = outputString.Remove(0, compilationOutputPrior.Index + compilationOutputPrior.Length);
+    }
 
     if (exitCode == 0) {
       var diffMessage = AssertWithDiff.GetDiffMessage(expectedOutput, outputString);
@@ -273,11 +277,6 @@ private static bool IsAllowedOutputLine(IExecutableBackend backend, string line)
       return true;
     }
 
-    // This is the first non-blank line we expect when we pass /noVerify
-    if (line == "Dafny program verifier did not attempt verification") {
-      return true;
-    }
-
     // This is output if the compiler emits any errors
     if (line.StartsWith("Wrote textual form of partial target program to")) {
       return true;
diff --git a/Test/metatests/InconsistentCompilerBehavior.dfy.testdafny.expect b/Test/metatests/InconsistentCompilerBehavior.dfy.testdafny.expect
index d747e3f2822..63d05550a1b 100644
--- a/Test/metatests/InconsistentCompilerBehavior.dfy.testdafny.expect
+++ b/Test/metatests/InconsistentCompilerBehavior.dfy.testdafny.expect
@@ -2,8 +2,6 @@ Verifying...
 Executing on C#...
 AssertEqualWithDiff() Failure
 Diff (changing expected into actual):
- 
- Dafny program verifier did not attempt verification
 -Different than any output
 +0
  
@@ -11,8 +9,6 @@ Diff (changing expected into actual):
 Executing on JavaScript...
 AssertEqualWithDiff() Failure
 Diff (changing expected into actual):
- 
- Dafny program verifier did not attempt verification
 -Different than any output
 +0
  
@@ -20,8 +16,6 @@ Diff (changing expected into actual):
 Executing on Go...
 AssertEqualWithDiff() Failure
 Diff (changing expected into actual):
- 
- Dafny program verifier did not attempt verification
 -Different than any output
 +0
  
@@ -29,8 +23,6 @@ Diff (changing expected into actual):
 Executing on Java...
 AssertEqualWithDiff() Failure
 Diff (changing expected into actual):
- 
- Dafny program verifier did not attempt verification
 -Different than any output
 +0
  
@@ -38,8 +30,6 @@ Diff (changing expected into actual):
 Executing on Python...
 AssertEqualWithDiff() Failure
 Diff (changing expected into actual):
- 
- Dafny program verifier did not attempt verification
 -Different than any output
 +0
  
diff --git a/Test/metatests/TestBeyondVerifierExpect.dfy b/Test/metatests/TestBeyondVerifierExpect.dfy
new file mode 100644
index 00000000000..dadd3116247
--- /dev/null
+++ b/Test/metatests/TestBeyondVerifierExpect.dfy
@@ -0,0 +1,9 @@
+// RUN: ! %testDafnyForEachCompiler "%s" > "%t"
+// RUN: %diff "%s.testdafny.expect" "%t"
+
+method Main() {
+  ghost var n := 15;
+  if j :| 0 <= j < n { // this gives a no-trigger warning
+  }
+  print "hello\n";
+}
diff --git a/Test/metatests/TestBeyondVerifierExpect.dfy.expect b/Test/metatests/TestBeyondVerifierExpect.dfy.expect
new file mode 100644
index 00000000000..024d23dc14f
--- /dev/null
+++ b/Test/metatests/TestBeyondVerifierExpect.dfy.expect
@@ -0,0 +1 @@
+good bye
diff --git a/Test/metatests/TestBeyondVerifierExpect.dfy.testdafny.expect b/Test/metatests/TestBeyondVerifierExpect.dfy.testdafny.expect
new file mode 100644
index 00000000000..1152e6c710e
--- /dev/null
+++ b/Test/metatests/TestBeyondVerifierExpect.dfy.testdafny.expect
@@ -0,0 +1,37 @@
+Verifying...
+Executing on C#...
+AssertEqualWithDiff() Failure
+Diff (changing expected into actual):
+-good bye
++hello
+ 
+
+Executing on JavaScript...
+AssertEqualWithDiff() Failure
+Diff (changing expected into actual):
+-good bye
++hello
+ 
+
+Executing on Go...
+AssertEqualWithDiff() Failure
+Diff (changing expected into actual):
+-good bye
++hello
+ 
+
+Executing on Java...
+AssertEqualWithDiff() Failure
+Diff (changing expected into actual):
+-good bye
++hello
+ 
+
+Executing on Python...
+AssertEqualWithDiff() Failure
+Diff (changing expected into actual):
+-good bye
++hello
+ 
+
+Executing on C++...
diff --git a/Test/metatests/TestBeyondVerifierExpect.dfy.verifier.expect b/Test/metatests/TestBeyondVerifierExpect.dfy.verifier.expect
new file mode 100644
index 00000000000..dc52d4a07e1
--- /dev/null
+++ b/Test/metatests/TestBeyondVerifierExpect.dfy.verifier.expect
@@ -0,0 +1 @@
+TestBeyondVerifierExpect.dfy(6,5): Warning: /!\ No terms found to trigger on.
diff --git a/Test/metatests/TestDoesNotVerify.dfy b/Test/metatests/TestDoesNotVerify.dfy
new file mode 100644
index 00000000000..aec66dca876
--- /dev/null
+++ b/Test/metatests/TestDoesNotVerify.dfy
@@ -0,0 +1,8 @@
+// RUN: ! %testDafnyForEachCompiler "%s" > "%t"
+// RUN: %diff "%s.testdafny.expect" "%t"
+
+method Main() {
+  ghost var n := 15;
+  assert n < 12; // error: the verifier complains about this
+  print "hello\n";
+}
diff --git a/Test/metatests/TestDoesNotVerify.dfy.expect b/Test/metatests/TestDoesNotVerify.dfy.expect
new file mode 100644
index 00000000000..ce013625030
--- /dev/null
+++ b/Test/metatests/TestDoesNotVerify.dfy.expect
@@ -0,0 +1 @@
+hello
diff --git a/Test/metatests/TestDoesNotVerify.dfy.testdafny.expect b/Test/metatests/TestDoesNotVerify.dfy.testdafny.expect
new file mode 100644
index 00000000000..28812ebda2c
--- /dev/null
+++ b/Test/metatests/TestDoesNotVerify.dfy.testdafny.expect
@@ -0,0 +1,8 @@
+Verifying...
+Verification failed. Output:
+TestDoesNotVerify.dfy(6,11): Error: assertion might not hold
+
+Dafny program verifier finished with 0 verified, 1 error
+
+Error:
+
diff --git a/Test/metatests/TestDoesNotVerify.dfy.verifier.expect b/Test/metatests/TestDoesNotVerify.dfy.verifier.expect
new file mode 100644
index 00000000000..61b04415c49
--- /dev/null
+++ b/Test/metatests/TestDoesNotVerify.dfy.verifier.expect
@@ -0,0 +1 @@
+TestDoesNotVerify.dfy(6,11): Error: assertion might not hold
diff --git a/Test/metatests/TestMissingVerifierExpect.dfy b/Test/metatests/TestMissingVerifierExpect.dfy
new file mode 100644
index 00000000000..dadd3116247
--- /dev/null
+++ b/Test/metatests/TestMissingVerifierExpect.dfy
@@ -0,0 +1,9 @@
+// RUN: ! %testDafnyForEachCompiler "%s" > "%t"
+// RUN: %diff "%s.testdafny.expect" "%t"
+
+method Main() {
+  ghost var n := 15;
+  if j :| 0 <= j < n { // this gives a no-trigger warning
+  }
+  print "hello\n";
+}
diff --git a/Test/metatests/TestMissingVerifierExpect.dfy.expect b/Test/metatests/TestMissingVerifierExpect.dfy.expect
new file mode 100644
index 00000000000..ce013625030
--- /dev/null
+++ b/Test/metatests/TestMissingVerifierExpect.dfy.expect
@@ -0,0 +1 @@
+hello
diff --git a/Test/metatests/TestMissingVerifierExpect.dfy.testdafny.expect b/Test/metatests/TestMissingVerifierExpect.dfy.testdafny.expect
new file mode 100644
index 00000000000..60892ad9dff
--- /dev/null
+++ b/Test/metatests/TestMissingVerifierExpect.dfy.testdafny.expect
@@ -0,0 +1,6 @@
+Verifying...
+AssertEqualWithDiff() Failure
+Diff (changing expected into actual):
++TestMissingVerifierExpect.dfy(6,5): Warning: /!\ No terms found to trigger on.
++
+
diff --git a/Test/metatests/TestWrongVerifierExpect.dfy b/Test/metatests/TestWrongVerifierExpect.dfy
new file mode 100644
index 00000000000..dadd3116247
--- /dev/null
+++ b/Test/metatests/TestWrongVerifierExpect.dfy
@@ -0,0 +1,9 @@
+// RUN: ! %testDafnyForEachCompiler "%s" > "%t"
+// RUN: %diff "%s.testdafny.expect" "%t"
+
+method Main() {
+  ghost var n := 15;
+  if j :| 0 <= j < n { // this gives a no-trigger warning
+  }
+  print "hello\n";
+}
diff --git a/Test/metatests/TestWrongVerifierExpect.dfy.expect b/Test/metatests/TestWrongVerifierExpect.dfy.expect
new file mode 100644
index 00000000000..ce013625030
--- /dev/null
+++ b/Test/metatests/TestWrongVerifierExpect.dfy.expect
@@ -0,0 +1 @@
+hello
diff --git a/Test/metatests/TestWrongVerifierExpect.dfy.testdafny.expect b/Test/metatests/TestWrongVerifierExpect.dfy.testdafny.expect
new file mode 100644
index 00000000000..e2e28307304
--- /dev/null
+++ b/Test/metatests/TestWrongVerifierExpect.dfy.testdafny.expect
@@ -0,0 +1,7 @@
+Verifying...
+AssertEqualWithDiff() Failure
+Diff (changing expected into actual):
+-warning: out of bananas
++TestWrongVerifierExpect.dfy(6,5): Warning: /!\ No terms found to trigger on.
+ 
+
diff --git a/Test/metatests/TestWrongVerifierExpect.dfy.verifier.expect b/Test/metatests/TestWrongVerifierExpect.dfy.verifier.expect
new file mode 100644
index 00000000000..c13ffbd13ac
--- /dev/null
+++ b/Test/metatests/TestWrongVerifierExpect.dfy.verifier.expect
@@ -0,0 +1 @@
+warning: out of bananas