diff --git a/Source/DafnyCore/AST/Substituter.cs b/Source/DafnyCore/AST/Substituter.cs
index 2cf2d0b05d0..91f01b04844 100644
--- a/Source/DafnyCore/AST/Substituter.cs
+++ b/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
       }
 
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/patterns/matchInAssertBy.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/patterns/matchInAssertBy.dfy
new file mode 100644
index 00000000000..921cb68bdcc
--- /dev/null
+++ b/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
+}
\ No newline at end of file
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/patterns/matchInAssertBy.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/patterns/matchInAssertBy.dfy.expect
new file mode 100644
index 00000000000..823a60a105c
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/patterns/matchInAssertBy.dfy.expect
@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 1 verified, 0 errors
diff --git a/docs/dev/news/5671.fix b/docs/dev/news/5671.fix
new file mode 100644
index 00000000000..426e85a82f4
--- /dev/null
+++ b/docs/dev/news/5671.fix
@@ -0,0 +1 @@
+Resolved a crash that would occur when using a match statement inside an assert by block
\ No newline at end of file