Merge branch 'master' into per-backend-code-support-in-stdlibs

Source/DafnyCore/Generic/Reporting.cs

@@ -66,14 +66,14 @@ protected override bool MessageCore(MessageSource source, ErrorLevel level, stri
           errorLine += "\n";
         }
 
+        Options.OutputWriter.Write(errorLine);
+
         if (Options.Get(DafnyConsolePrinter.ShowSnippets) && tok != Token.NoToken) {
           TextWriter tw = new StringWriter();
           new DafnyConsolePrinter(Options).WriteSourceCodeSnippet(tok.ToRange(), tw);
           Options.OutputWriter.Write(tw.ToString());
         }
 
-        Options.OutputWriter.Write(errorLine);
-
         if (Options.OutputWriter == Console.Out) {
           Console.ForegroundColor = previousColor;
         }

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3304.dfy.expect

@@ -1,6 +1,6 @@
+git-issue-3304.dfy(5,9): Error: the type of this expression is underspecified
   |
 5 |   assert [] == [[]];
   |          ^
 
-git-issue-3304.dfy(5,9): Error: the type of this expression is underspecified
 1 resolution/type errors detected in git-issue-3304.dfy

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4787.dfy

@@ -0,0 +1,19 @@
+// RUN: %exits-with 4 %baredafny verify %args --warn-redundant-assumptions --warn-contradictory-assumptions --show-snippets:true "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+module M {
+  opaque function ToSet(xs: seq<int>): set<int> {
+    set x: int | x in xs
+  }
+
+  lemma LemmaCardinality(xs: seq<int>)
+    ensures |ToSet(xs)| <= |xs|
+  {}
+
+  lemma LemmaEmpty(xs: seq<int>)
+    requires xs == []
+    ensures |ToSet(xs)| == 0
+  {
+    assume false;
+  }
+}

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4787.dfy.expect

@@ -0,0 +1,22 @@
+git-issue-4787.dfy(11,2): Error: a postcondition could not be proved on this return path
+   |
+11 |   {}
+   |   ^
+
+git-issue-4787.dfy(10,12): Related location: this is the postcondition that could not be proved
+   |
+10 |     ensures |ToSet(xs)| <= |xs|
+   |             ^^^^^^^^^^^^^^^^^^^
+
+git-issue-4787.dfy(15,12): Warning: ensures clause proved using contradictory assumptions
+   |
+15 |     ensures |ToSet(xs)| == 0
+   |             ^^^^^^^^^^^^^^^^
+
+git-issue-4787.dfy(14,13): Warning: unnecessary requires clause
+   |
+14 |     requires xs == []
+   |              ^^^^^^^^
+
+
+Dafny program verifier finished with 1 verified, 1 error

docs/dev/news/4787.fix

@@ -0,0 +1 @@
+Fix error messages being printed after their context snippets