Resolved a crash that would occur when using a match statement inside…

Source/DafnyCore/AST/Substituter.cs

@@ -879,7 +879,9 @@ protected virtual Statement SubstStmt(Statement stmt) {
         rr.ResolvedStatements.AddRange(revealStmt.ResolvedStatements.ConvertAll(SubstStmt));
         rr.OffsetMembers = revealStmt.OffsetMembers.ToList();
         r = rr;
-      } else {
+      } else if (stmt is NestedMatchStmt nestedMatchStmt) {
+        r = SubstStmt(nestedMatchStmt.Flattened);
+      }else {
         Contract.Assert(false); throw new cce.UnreachableException();  // unexpected statement
       }
 

Source/IntegrationTests/TestFiles/LitTests/LitTest/patterns/matchInAssertBy.dfy

@@ -0,0 +1,12 @@
+// RUN: %verify "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+datatype D = D 
+function f(d:D):bool {
+  assert true by {
+    match d {
+      case _ => assert true;
+    }
+  }
+  true
+}

Source/IntegrationTests/TestFiles/LitTests/LitTest/patterns/matchInAssertBy.dfy.expect

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

docs/dev/news/5671.fix

@@ -0,0 +1 @@
+Resolved a crash that would occur when using a match statement inside an assert by block