Make --filter-* work with measure-complexity

Source/DafnyCore/Options/CommonOptionBag.cs

@@ -358,6 +358,12 @@ Allow Dafny code to depend on the standard libraries included with the Dafny dis
 If verification fails, report a detailed counterexample for the first failing assertion (experimental).".TrimStart()) {
   };
 
+  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""");
+
+  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`");
+
   static CommonOptionBag() {
     DafnyOptions.RegisterLegacyBinding(WarnAsErrors, (options, value) => {
       if (!options.Get(AllowWarnings) && !options.Get(WarnAsErrors)) {
@@ -634,7 +640,9 @@ void ParsePrintMode(Option<PrintModes> option, Boogie.CommandLineParseState ps,
       AddCompileSuffix,
       SystemModule,
       ExecutionCoverageReport,
-      ExtractCounterexample
+      ExtractCounterexample,
+      FilterSymbol,
+      FilterPosition
       );
   }
 

Source/DafnyCore/Options/DafnyCommands.cs

@@ -49,7 +49,9 @@ static DafnyCommands() {
     CommonOptionBag.VerificationCoverageReport,
     CommonOptionBag.ExtractCounterexample,
     CommonOptionBag.ShowInference,
-    CommonOptionBag.ManualTriggerOption
+    CommonOptionBag.ManualTriggerOption,
+    CommonOptionBag.FilterSymbol,
+    CommonOptionBag.FilterPosition
   }.ToList();
 
   public static IReadOnlyList<Option> TranslationOptions = new Option[] {

Source/DafnyDriver/CliCompilation.cs

@@ -245,12 +245,12 @@ public async IAsyncEnumerable<CanVerifyResult> VerifyAllLazily(int? randomSeed)
   }
 
   private List<ICanVerify> FilterCanVerifies(List<ICanVerify> canVerifies, out int? line) {
-    var symbolFilter = Options.Get(VerifyCommand.FilterSymbol);
+    var symbolFilter = Options.Get(CommonOptionBag.FilterSymbol);
     if (symbolFilter != null) {
       canVerifies = canVerifies.Where(canVerify => canVerify.FullDafnyName.Contains(symbolFilter)).ToList();
     }
 
-    var filterPosition = Options.Get(VerifyCommand.FilterPosition);
+    var filterPosition = Options.Get(CommonOptionBag.FilterPosition);
     if (filterPosition == null) {
       line = null;
       return canVerifies;

Source/DafnyDriver/Commands/VerifyCommand.cs

@@ -17,17 +17,6 @@ namespace Microsoft.Dafny;
 
 public static class VerifyCommand {
 
-  static VerifyCommand() {
-    DooFile.RegisterNoChecksNeeded(FilterSymbol);
-    DooFile.RegisterNoChecksNeeded(FilterPosition);
-  }
-
-  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""");
-
-  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`");
-
   public static Command Create() {
     var result = new Command("verify", "Verify the program.");
     result.AddArgument(DafnyCommands.FilesArgument);
@@ -39,14 +28,10 @@ public static Command Create() {
   }
 
   private static IReadOnlyList<Option> VerifyOptions =>
-    new Option[] {
-        FilterSymbol,
-        FilterPosition,
-      }.Concat(DafnyCommands.VerificationOptions).
+      DafnyCommands.VerificationOptions.
       Concat(DafnyCommands.ConsoleOutputOptions).
       Concat(DafnyCommands.ResolverOptions);
 
-
   public static async Task<int> HandleVerification(DafnyOptions options) {
     if (options.Get(CommonOptionBag.VerificationCoverageReport) != null) {
       options.TrackVerificationCoverage = true;