From fc300da3c15d6796a176564885af3583a036a2a2 Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@amazon.com>
Date: Wed, 21 Dec 2022 10:33:45 -0800
Subject: [PATCH 1/2] fix: Count proof obligations of loop headers

---
 .../Verifier/BoogieStmtListBuilder.cs         | 10 ++++++++-
 Test/git-issues/git-issue-3243.dfy            | 22 +++++++++++++++++++
 Test/git-issues/git-issue-3243.dfy.expect     |  7 ++++++
 3 files changed, 38 insertions(+), 1 deletion(-)
 create mode 100644 Test/git-issues/git-issue-3243.dfy
 create mode 100644 Test/git-issues/git-issue-3243.dfy.expect

diff --git a/Source/DafnyCore/Verifier/BoogieStmtListBuilder.cs b/Source/DafnyCore/Verifier/BoogieStmtListBuilder.cs
index fa643e6d667..1e3a8df159b 100644
--- a/Source/DafnyCore/Verifier/BoogieStmtListBuilder.cs
+++ b/Source/DafnyCore/Verifier/BoogieStmtListBuilder.cs
@@ -1,3 +1,4 @@
+using System.Linq;
 using Microsoft.Boogie;
 
 namespace Microsoft.Dafny {
@@ -26,7 +27,14 @@ public void Add(Cmd cmd) {
         }
       }
     }
-    public void Add(StructuredCmd scmd) { builder.Add(scmd); }
+
+    public void Add(StructuredCmd scmd) {
+      builder.Add(scmd);
+      if (scmd is Boogie.WhileCmd whyle && whyle.Invariants.Any(inv => inv is Boogie.AssertCmd)) {
+        tran.assertionCount++;
+      }
+    }
+
     public void Add(TransferCmd tcmd) { builder.Add(tcmd); }
     public void AddLabelCmd(string label) { builder.AddLabelCmd(label); }
     public void AddLocalVariable(string name) { builder.AddLocalVariable(name); }
diff --git a/Test/git-issues/git-issue-3243.dfy b/Test/git-issues/git-issue-3243.dfy
new file mode 100644
index 00000000000..704f8530c24
--- /dev/null
+++ b/Test/git-issues/git-issue-3243.dfy
@@ -0,0 +1,22 @@
+// RUN: %exits-with 4 %dafny /compile:0 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+method LoopWithBody(x: int)
+  decreases *
+{
+  var i := 0;
+  while i < x
+    // The following loop-invariant-on-entry check was once omitted when it was the only proof obligation.
+    invariant i <= x // error: loop invariant does not hold on entry
+    decreases *
+  {
+  }
+}
+
+method BodylessLoop(x: int)
+{
+  var i := 0;
+  while i < x
+    // The following loop-invariant-on-entry check was once omitted when it was the only proof obligation.
+    invariant i <= x // error: loop invariant does not hold on entry
+}
diff --git a/Test/git-issues/git-issue-3243.dfy.expect b/Test/git-issues/git-issue-3243.dfy.expect
new file mode 100644
index 00000000000..bf2959adc5b
--- /dev/null
+++ b/Test/git-issues/git-issue-3243.dfy.expect
@@ -0,0 +1,7 @@
+git-issue-3243.dfy(19,2): Warning: note, this loop has no body (loop frame: i)
+git-issue-3243.dfy(10,16): Error: This loop invariant might not hold on entry.
+git-issue-3243.dfy(10,16): Related message: loop invariant violation
+git-issue-3243.dfy(21,16): Error: This loop invariant might not hold on entry.
+git-issue-3243.dfy(21,16): Related message: loop invariant violation
+
+Dafny program verifier finished with 0 verified, 2 errors

From d1edbd7bde10301282b24d33b99eec5a76a0d601 Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@amazon.com>
Date: Wed, 21 Dec 2022 10:38:20 -0800
Subject: [PATCH 2/2] Add release notes

---
 docs/dev/news/3244.fix | 1 +
 1 file changed, 1 insertion(+)
 create mode 100644 docs/dev/news/3244.fix

diff --git a/docs/dev/news/3244.fix b/docs/dev/news/3244.fix
new file mode 100644
index 00000000000..c8d2af4fd00
--- /dev/null
+++ b/docs/dev/news/3244.fix
@@ -0,0 +1 @@
+Check loop invariants on entry, even when such are the only proof obligations in a method.