Merge branch 'master' into renameImportsToAvoidNameCollision

Source/DafnyCore/AST/Members/ConstantField.cs

@@ -25,10 +25,7 @@ public override bool CanBeRevealed() {
     return true;
   }
 
-  public bool ContainsHide {
-    get => throw new NotSupportedException();
-    set => throw new NotSupportedException();
-  }
+  public bool ContainsHide { get; set; }
 
   public new bool IsGhost { get { return this.isGhost; } }
   public List<TypeParameter> TypeArgs { get { return new List<TypeParameter>(); } }

Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/functions/constantWithReveal.dfy

@@ -0,0 +1,8 @@
+// RUN: %verify %s &> "%t"
+// RUN: %diff "%s.expect" "%t"
+
+opaque function Foo(x: int): int {
+  x
+}
+
+const C := reveal Foo(); Foo(42)

Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/functions/constantWithReveal.dfy.expect

@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 1 verified, 0 errors

docs/dev/news/5761.feat

@@ -0,0 +1 @@
+Added opaque blocks to the language. Opaque blocks enable improving verification performance. See the documentation for more details.

docs/dev/news/5779.feat

@@ -0,0 +1 @@
+By blocks ("... by { ... }") are now available for assert statements, call statements, and the three types of assignments (:=, :-, :|). Also, by blocks should now be more intuitive since they enable proving any assertions on the left-hand side of the 'by', not just the 'outermost' one. For example, previously `assert 3 / x == 1 by { assume x == 3; }` could still give a possible division by zero error, but now it won't. 

docs/dev/news/5823.fix

@@ -0,0 +1 @@
+Fix a bug that prevented using reveal statement expressions in the body of a constant.