Merge branch 'master' into feat-code-actions-forall-calc

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);
+     }
   .)
   .
 

Source/IntegrationTests/TestFiles/LitTests/LitTest/README.md

@@ -68,6 +68,14 @@ will be flagged by CI, and should be fixed by either converting it to use
 to flag it as intentionally inconsistent,
 for tests of backend-specific externs for example.
 
+If a platform is not supported, please use the following command:
+
+```
+// UNSUPPORTED: windows, macosx
+```
+
+You can specify one or multiple platforms separated by a comma among `windows`, `posix`, `macosx`
+
 ## Executing Tests from JetBrains Rider
 
 You will likely find it more convenient to run tests from an IDE such as

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;
+  }
 }

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

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CoinductiveProofs.dfy

@@ -1,6 +1,6 @@
+// UNSUPPORTED: macosx
+// Unsupported because the resource count is slightly different on macosx
 // RUN: %testDafnyForEachResolver --expect-exit-code=4 "%s" -- --allow-deprecation --performance-stats=1
-
-
 codatatype Stream<T> = Cons(head: T, tail: Stream)
 
 ghost function Upward(n: int): Stream<int>

docs/dev/news/6024.fix

@@ -0,0 +1 @@
+By clauses for assign-such-that statements (:|), are now never ignored.