From 1b89c34ec48f3516b8f8b4f9bd0825b14061aeac Mon Sep 17 00:00:00 2001
From: Alex Chew <alex-chew@users.noreply.github.com>
Date: Thu, 16 Nov 2023 09:31:16 -0800
Subject: [PATCH] fix: print error context snippets after their messages
 (#4788)

Fixes #4787.
---
 Source/DafnyCore/Generic/Reporting.cs         |  4 ++--
 .../git-issues/git-issue-3304.dfy.expect      |  2 +-
 .../LitTest/git-issues/git-issue-4787.dfy     | 19 ++++++++++++++++
 .../git-issues/git-issue-4787.dfy.expect      | 22 +++++++++++++++++++
 docs/dev/news/4787.fix                        |  1 +
 5 files changed, 45 insertions(+), 3 deletions(-)
 create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4787.dfy
 create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4787.dfy.expect
 create mode 100644 docs/dev/news/4787.fix

diff --git a/Source/DafnyCore/Generic/Reporting.cs b/Source/DafnyCore/Generic/Reporting.cs
index fd62cfac2dc..3f31bd655f8 100644
--- a/Source/DafnyCore/Generic/Reporting.cs
+++ b/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;
         }
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3304.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3304.dfy.expect
index c06ad3dc8c5..c7dbeea8972 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3304.dfy.expect
+++ b/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
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4787.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4787.dfy
new file mode 100644
index 00000000000..d3904c1fd0f
--- /dev/null
+++ b/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;
+  }
+}
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4787.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4787.dfy.expect
new file mode 100644
index 00000000000..19013336023
--- /dev/null
+++ b/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
diff --git a/docs/dev/news/4787.fix b/docs/dev/news/4787.fix
new file mode 100644
index 00000000000..9f1684c9949
--- /dev/null
+++ b/docs/dev/news/4787.fix
@@ -0,0 +1 @@
+Fix error messages being printed after their context snippets