Fix opaque block in conjunction with match statements (#5785)

### Description
- Fix opaque block in conjunction with match statements
- Add a small feature to `--filter-symbol`

### How has this been tested?
- Added testcase to `opaqueBlock.dfy`

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>

Source/DafnyCore/AST/Expressions/Conditional/NestedMatchStmt.cs

@@ -45,7 +45,14 @@ public NestedMatchStmt(Cloner cloner, NestedMatchStmt original) : base(cloner, o
 
   public override IEnumerable<INode> Children => new[] { Source }.Concat<Node>(Cases);
 
-  public override IEnumerable<Statement> SubStatements => Cases.SelectMany(c => c.Body);
+  public override IEnumerable<Statement> SubStatements {
+    get {
+      if (Flattened != null) {
+        return Flattened.SubStatements;
+      }
+      return Cases.SelectMany(c => c.Body);
+    }
+  }
 
   public override IEnumerable<Statement> PreResolveSubStatements {
     get => this.Cases.SelectMany(oneCase => oneCase.Body);

Source/DafnyDriver/CliCompilation.cs

@@ -271,7 +271,12 @@ public static string DescribeOutcome(VcOutcome outcome) {
   private List<ICanVerify> FilterCanVerifies(List<ICanVerify> canVerifies, out int? line) {
     var symbolFilter = Options.Get(VerifyCommand.FilterSymbol);
     if (symbolFilter != null) {
-      canVerifies = canVerifies.Where(canVerify => canVerify.FullDafnyName.Contains(symbolFilter)).ToList();
+      if (symbolFilter.EndsWith(".")) {
+        var withoutDot = new string(symbolFilter.SkipLast(1).ToArray());
+        canVerifies = canVerifies.Where(canVerify => canVerify.FullDafnyName.EndsWith(withoutDot)).ToList();
+      } else {
+        canVerifies = canVerifies.Where(canVerify => canVerify.FullDafnyName.Contains(symbolFilter)).ToList();
+      }
     }
 
     var filterPosition = Options.Get(VerifyCommand.FilterPosition);

Source/DafnyDriver/Commands/VerifyCommand.cs

@@ -37,7 +37,7 @@ static VerifyCommand() {
     IsHidden = true
   };
   public static readonly Option<string> FilterSymbol = new("--filter-symbol",
-    @"Filter what gets verified by selecting only symbols whose fully qualified name contains the given argument. For example: ""--filter-symbol=MyNestedModule.MyFooFunction""");
+    @"Filter what gets verified by selecting only symbols whose fully qualified name contains the given argument, for example: ""--filter-symbol=MyNestedModule.MyFooFunction"". Place a dot at the end of the argument to indicate the symbol name must end like this, which can be useful if one symbol name is a prefix of another.");
 
   public static readonly Option<string> FilterPosition = new("--filter-position",
     @"Filter what gets verified based on a source location. The location is specified as a file path suffix, optionally followed by a colon and a line number. For example, `dafny verify dfyconfig.toml --filter-position=source1.dfy:5` will only verify things that range over line 5 in the file `source1.dfy`. In combination with `--isolate-assertions`, individual assertions can be verified by filtering on the line that contains them. When processing a single file, the filename can be skipped, for example: `dafny verify MyFile.dfy --filter-position=:23`");

Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/statement/opaqueBlock.dfy

@@ -180,4 +180,19 @@ method MultipleAssignment() returns (r: int) {
     x, y := tuple.0, tuple.1;
   }
   r := x;
+}
+
+method FlattenedMatch(x: Option<int>, y: Option<int>) {
+   // This match statement must copy some of the case bodies when flattening
+   var z := 3;
+   opaque {
+     match (x, y) {
+       case (Some(a), _) =>
+         var y := a;
+       case (_, Some(b)) =>
+         var z := b;
+       case _ =>
+     }
+   }
+   assert z == 3;
 }

Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/statement/opaqueBlock.dfy.expect

@@ -11,4 +11,4 @@ opaqueBlock.dfy(127,12): Error: variable 'y', which is subject to definite-assig
 opaqueBlock.dfy(130,17): Error: variable 'z', which is subject to definite-assignment rules, might be uninitialized here
 opaqueBlock.dfy(142,12): Error: ensures might not hold
 
-Dafny program verifier finished with 2 verified, 12 errors
+Dafny program verifier finished with 3 verified, 12 errors