From 029236f14c20646b4b5269ff3b5598a2d5a19e05 Mon Sep 17 00:00:00 2001
From: Remy Willems <rwillems@amazon.com>
Date: Wed, 8 Jan 2025 13:09:42 +0100
Subject: [PATCH] Add fix, test and release note for 6024

---
 Source/DafnyCore/Dafny.atg                               | 9 +++------
 .../LitTests/LitTest/ast/statement/assignSuchThat.dfy    | 8 ++++++++
 .../LitTest/ast/statement/assignSuchThat.dfy.expect      | 2 +-
 docs/dev/news/6024.fix                                   | 1 +
 4 files changed, 13 insertions(+), 7 deletions(-)
 create mode 100644 docs/dev/news/6024.fix

diff --git a/Source/DafnyCore/Dafny.atg b/Source/DafnyCore/Dafny.atg
index 0a5751d168c..2f45f035fd3 100644
--- a/Source/DafnyCore/Dafny.atg
+++ b/Source/DafnyCore/Dafny.atg
@@ -2391,19 +2391,16 @@ AssignStatement<out Statement/*!*/ s>
        s = new AssignSuchThatStmt(rangeToken, lhss, suchThat, suchThatAssume, null);
      } else if (exceptionRhs != null) {
        s = new AssignOrReturnStmt(rangeToken, lhss, exceptionRhs, keywordToken, rhss);
-       if (proof != null) {
-         s = new BlockByProofStmt(rangeToken, proof, s);
-       }
      } else {
        if (lhss.Count == 0 && rhss.Count == 0) {
          s = new BlockStmt(rangeToken, new List<Statement>()); // error, give empty statement
        } else {
          s = new AssignStatement(rangeToken, lhss, rhss);
-         if (proof != null) {
-           s = new BlockByProofStmt(rangeToken, proof, s);
-         }
        }
      }
+     if (proof != null) {
+       s = new BlockByProofStmt(rangeToken, proof, s);
+     }
   .)
   .
 
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/statement/assignSuchThat.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/statement/assignSuchThat.dfy
index 43edfe82cb3..109a9cb3b3e 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/statement/assignSuchThat.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/statement/assignSuchThat.dfy
@@ -5,4 +5,12 @@ method ByClause(b: bool) {
   var r: int :| false by {
     assume {:axiom} false;
   }
+}
+
+function F(x: int): int
+method ByClauseSeparateAssignment() {
+  var a;
+  a :| F(a) == 2 by {
+    assume {:axiom} F(10) == 2;
+  }
 }
\ No newline at end of file
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/statement/assignSuchThat.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/statement/assignSuchThat.dfy.expect
index 823a60a105c..ebe2328e072 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/statement/assignSuchThat.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/statement/assignSuchThat.dfy.expect
@@ -1,2 +1,2 @@
 
-Dafny program verifier finished with 1 verified, 0 errors
+Dafny program verifier finished with 2 verified, 0 errors
diff --git a/docs/dev/news/6024.fix b/docs/dev/news/6024.fix
new file mode 100644
index 00000000000..d8b3b8868e5
--- /dev/null
+++ b/docs/dev/news/6024.fix
@@ -0,0 +1 @@
+By clauses for assign-such-that statements (:|), are now never ignored.
\ No newline at end of file