diff --git a/Source/DafnyCore/AST/Members/ConstantField.cs b/Source/DafnyCore/AST/Members/ConstantField.cs
index 3df0fed129f..95d3273b509 100644
--- a/Source/DafnyCore/AST/Members/ConstantField.cs
+++ b/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>(); } }
diff --git a/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs b/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs
index 706181406bd..7edddd6163a 100644
--- a/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs
+++ b/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs
@@ -2236,8 +2236,11 @@ protected override void EmitNew(Type type, IToken tok, CallStmt initCall /*?*/,
       if (cl is TraitDecl { IsObjectTrait: true }) {
         wr.Write("_dafny.New_Object()");
       } else {
+        var ctor = (Constructor)initCall?.Method; // correctness of cast follows from precondition of "EmitNew"
+        var sep = "";
         wr.Write("{0}(", TypeName_Initializer(type, wr, tok));
         EmitTypeDescriptorsActuals(TypeArgumentInstantiation.ListFromClass(cl, type.TypeArgs), tok, wr);
+        wr.Write(ConstructorArguments(initCall, wStmts, ctor, sep));
         wr.Write(")");
       }
     }
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/functions/constantWithReveal.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/functions/constantWithReveal.dfy
new file mode 100644
index 00000000000..4d95901ac88
--- /dev/null
+++ b/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)
\ No newline at end of file
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/functions/constantWithReveal.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/functions/constantWithReveal.dfy.expect
new file mode 100644
index 00000000000..823a60a105c
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/functions/constantWithReveal.dfy.expect
@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 1 verified, 0 errors
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ExternCtors-externs/Class.java b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ExternCtors-externs/Class.java
index 1827be2bfc6..f6549c6aaf0 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ExternCtors-externs/Class.java
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ExternCtors-externs/Class.java
@@ -2,7 +2,7 @@
 
 import java.math.BigInteger;
 
-public class Class extends _ExternBase_Class {
+public class Class {
     private final BigInteger n;
 
     public Class(BigInteger n) {
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ExternCtors-externs/Library.go b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ExternCtors-externs/Library.go
index 93aaf858db5..2bcbd00321c 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ExternCtors-externs/Library.go
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ExternCtors-externs/Library.go
@@ -17,12 +17,6 @@ func (obj *Class) Get() dafny.Int {
 	return obj.n
 }
 
-// have to implement this because the Go backend can't mix Dafny and Go code :-\
-
-func (obj *Class) Print() {
-	fmt.Printf("My value is %d\n", obj.n)
-}
-
 type CompanionStruct_Class_ struct{}
 var Companion_Class_ = CompanionStruct_Class_{}
 
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ExternCtors-externs/Library.py b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ExternCtors-externs/Library.py
index 3aa02f16f22..219b6d1836c 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ExternCtors-externs/Library.py
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ExternCtors-externs/Library.py
@@ -17,8 +17,3 @@ def SayHi():
 
     def Get(self):
         return self.n
-
-    def Print(self):
-        _dafny.print(_dafny.string_of(_dafny.Seq("My value is ")))
-        _dafny.print(_dafny.string_of((self).Get()))
-        _dafny.print(_dafny.string_of(_dafny.Seq("\n")))
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ExternCtors.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ExternCtors.dfy
index d0d50d7383d..e3cacf6ee6a 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ExternCtors.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ExternCtors.dfy
@@ -1,15 +1,16 @@
 // RUN: %run --target cs "%s" --input %S/ExternCtors-externs/Library.cs > "%t"
 // RUN: %run --target java "%s" --input %S/ExternCtors-externs/Class.java >> "%t"
 // RUN: %run --target py "%s" --input %S/ExternCtors-externs/Library.py >> "%t"
+// RUN: %run --target go "%s" --input %S/ExternCtors-externs/Library.go >> "%t"
 // RUN: %diff "%s.expect" "%t"
 
-// FIXME: Extern constructors are currently broken in Go and JavaScript,
-// so they are omitted
+// FIXME: Extern constructors are currently broken in JavaScript,
+// so that is omitted
 
 method Main() {
   Library.Class.SayHi();
   var obj := new Library.Class(42);
-  obj.Print();
+  print "My value is ", obj.Get(), "\n";
 }
 
 module {:extern "Library"} Library {
@@ -17,8 +18,6 @@ module {:extern "Library"} Library {
     constructor {:extern} (n: int)
     static method {:extern} SayHi()
     function {:extern} Get() : int
-    method Print() {
-      print "My value is ", Get(), "\n";
-    }
   }
 }
+
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ExternCtors.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ExternCtors.dfy.expect
index ce258f458fa..ef9433efad1 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ExternCtors.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ExternCtors.dfy.expect
@@ -10,3 +10,7 @@ My value is 42
 Dafny program verifier finished with 1 verified, 0 errors
 Hello!
 My value is 42
+
+Dafny program verifier finished with 1 verified, 0 errors
+Hello!
+My value is 42
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/SubsetTypes.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/SubsetTypes.dfy
index 1a450dbf14f..19773e1c00a 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/SubsetTypes.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/SubsetTypes.dfy
@@ -1,4 +1,4 @@
-// RUN: %exits-with 4 %verify "%s" --performance-stats=10 --relax-definite-assignment --allow-axioms > "%t"
+// RUN: %exits-with 4 %verify "%s" --performance-stats=100 --relax-definite-assignment --allow-axioms > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 module AssignmentToNat {
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/SubsetTypes.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/SubsetTypes.dfy.expect
index ad13e6b5b66..f1a6f5942d5 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/SubsetTypes.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/SubsetTypes.dfy.expect
@@ -91,5 +91,5 @@ SubsetTypes.dfy(459,15): Error: assertion might not hold
 SubsetTypes.dfy(464,13): Error: assertion might not hold
 
 Dafny program verifier finished with 13 verified, 91 errors
-Total resources used is 774980
-Max resources used by VC is 101850
+Total resources used is 775000
+Max resources used by VC is 101900
diff --git a/docs/dev/news/5761.feat b/docs/dev/news/5761.feat
new file mode 100644
index 00000000000..1d01f56a6e0
--- /dev/null
+++ b/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.
\ No newline at end of file
diff --git a/docs/dev/news/5779.feat b/docs/dev/news/5779.feat
new file mode 100644
index 00000000000..ba2d7b37f35
--- /dev/null
+++ b/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. 
\ No newline at end of file
diff --git a/docs/dev/news/5823.fix b/docs/dev/news/5823.fix
new file mode 100644
index 00000000000..86cf98f5763
--- /dev/null
+++ b/docs/dev/news/5823.fix
@@ -0,0 +1 @@
+Fix a bug that prevented using reveal statement expressions in the body of a constant.
\ No newline at end of file