From bf1ccdf93f283392fcd5fb7db659cff3d6140b54 Mon Sep 17 00:00:00 2001
From: Remy Willems <rwillems@amazon.com>
Date: Wed, 24 Jan 2024 15:06:41 +0100
Subject: [PATCH 1/6] Add option

---
 Source/DafnyDriver/Commands/VerifyCommand.cs | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/Source/DafnyDriver/Commands/VerifyCommand.cs b/Source/DafnyDriver/Commands/VerifyCommand.cs
index 8193fc5a7b5..0990d386d54 100644
--- a/Source/DafnyDriver/Commands/VerifyCommand.cs
+++ b/Source/DafnyDriver/Commands/VerifyCommand.cs
@@ -10,6 +10,9 @@ namespace Microsoft.Dafny;
 
 public static class VerifyCommand {
 
+  public static Option<string> FilterPosition = new("--filter-position",
+    @"Filter what gets verified based on a source location. The location is specified as a file path suffix that allows wildcards, optionally followed by a colon and a line number. For example, ""--filter=lastFolder/source.dfy:23""");
+  
   public static Command Create() {
     var result = new Command("verify", "Verify the program.");
     result.AddArgument(DafnyCommands.FilesArgument);
@@ -36,6 +39,7 @@ public static Command Create() {
 
   private static IReadOnlyList<Option> Options =>
     new Option[] {
+        FilterPosition,
         BoogieOptionBag.BoogieFilter,
       }.Concat(DafnyCommands.VerificationOptions).
       Concat(DafnyCommands.ConsoleOutputOptions).

From 77059d295d72ded76d9f76d9fa109c71b7de36ad Mon Sep 17 00:00:00 2001
From: Remy Willems <rwillems@amazon.com>
Date: Wed, 24 Jan 2024 15:44:15 +0100
Subject: [PATCH 2/6] Add test for --filter option:

---
 Source/DafnyDriver/CliCompilation.cs          | 25 +++++++++++++++++++
 Source/DafnyDriver/Commands/VerifyCommand.cs  |  7 +++++-
 .../LitTest/verification/Input/dfyconfig.toml |  0
 .../verification/Input/src/source1.dfy        |  7 ++++++
 .../verification/Input/src/source2.dfy        |  7 ++++++
 .../LitTest/verification/boogie-filter.dfy    | 11 ++++++++
 .../verification/boogie-filter.dfy.expect     |  6 +++++
 .../LitTests/LitTest/verification/filter.dfy  |  6 +++--
 .../LitTest/verification/filter.dfy.expect    | 16 +++++++++---
 9 files changed, 78 insertions(+), 7 deletions(-)
 create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/Input/dfyconfig.toml
 create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/Input/src/source1.dfy
 create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/Input/src/source2.dfy
 create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/boogie-filter.dfy
 create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/boogie-filter.dfy.expect

diff --git a/Source/DafnyDriver/CliCompilation.cs b/Source/DafnyDriver/CliCompilation.cs
index 59f25b835de..83bcc8ac0bf 100644
--- a/Source/DafnyDriver/CliCompilation.cs
+++ b/Source/DafnyDriver/CliCompilation.cs
@@ -1,8 +1,10 @@
+#nullable enable
 using System;
 using System.Collections.Concurrent;
 using System.Collections.Generic;
 using System.IO;
 using System.Linq;
+using System.Text.RegularExpressions;
 using System.Threading;
 using System.Threading.Tasks;
 using Microsoft.Boogie;
@@ -10,6 +12,7 @@
 using Microsoft.Dafny.LanguageServer.Language;
 using Microsoft.Dafny.LanguageServer.Language.Symbols;
 using Microsoft.Dafny.LanguageServer.Workspace;
+using Microsoft.Extensions.FileSystemGlobbing;
 using Microsoft.Extensions.Logging;
 using VC;
 using IToken = Microsoft.Dafny.IToken;
@@ -189,6 +192,8 @@ public async Task VerifyAllAndPrintSummary() {
       var canVerifies = resolution.CanVerifies?.DistinctBy(v => v.Tok).ToList();
 
       if (canVerifies != null) {
+        canVerifies = FilterCanVerifies(canVerifies);
+
         var orderedCanVerifies = canVerifies.OrderBy(v => v.Tok.pos).ToList();
         foreach (var canVerify in orderedCanVerifies) {
           canVerifyResults[canVerify] = new CliCanVerifyResults();
@@ -228,4 +233,24 @@ public async Task VerifyAllAndPrintSummary() {
       // Failed to resolve the program due to a user error.
     }
   }
+
+  private List<ICanVerify> FilterCanVerifies(List<ICanVerify> canVerifies) {
+    var filterPosition = options.Get(VerifyCommand.FilterPosition);
+    if (filterPosition == null) {
+      return canVerifies;
+    }
+
+    var regex = new Regex(@"((?:[\w.-]+\/)*[\w.-]+)(?::(\d+))?");
+    var result = regex.Match(filterPosition);
+    var filePart = result.Groups[1].Value;
+    string? linePart = result.Groups.Count > 2 ? result.Groups[2].Value : null;
+    var fileFiltered = canVerifies.Where(c => c.Tok.Uri.ToString().EndsWith(filePart)).ToList();
+    if (!string.IsNullOrEmpty(linePart)) {
+      var line = int.Parse(linePart);
+      return fileFiltered.Where(c =>
+        c.RangeToken.StartToken.line <= line && line <= c.RangeToken.EndToken.line).ToList();
+    }
+
+    return fileFiltered;
+  }
 }
\ No newline at end of file
diff --git a/Source/DafnyDriver/Commands/VerifyCommand.cs b/Source/DafnyDriver/Commands/VerifyCommand.cs
index 0990d386d54..9cb4f763462 100644
--- a/Source/DafnyDriver/Commands/VerifyCommand.cs
+++ b/Source/DafnyDriver/Commands/VerifyCommand.cs
@@ -3,6 +3,7 @@
 using System.CommandLine.Invocation;
 using System.Linq;
 using System.Threading.Tasks;
+using DafnyCore;
 using DafnyDriver.Commands;
 using JetBrains.Annotations;
 
@@ -10,9 +11,13 @@ namespace Microsoft.Dafny;
 
 public static class VerifyCommand {
 
+  static VerifyCommand() {
+    DooFile.RegisterNoChecksNeeded(FilterPosition);
+  }
+
   public static Option<string> FilterPosition = new("--filter-position",
     @"Filter what gets verified based on a source location. The location is specified as a file path suffix that allows wildcards, optionally followed by a colon and a line number. For example, ""--filter=lastFolder/source.dfy:23""");
-  
+
   public static Command Create() {
     var result = new Command("verify", "Verify the program.");
     result.AddArgument(DafnyCommands.FilesArgument);
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/Input/dfyconfig.toml b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/Input/dfyconfig.toml
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/Input/src/source1.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/Input/src/source1.dfy
new file mode 100644
index 00000000000..cf223c2cf5f
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/Input/src/source1.dfy
@@ -0,0 +1,7 @@
+method Succeeds()
+  ensures true {
+}
+
+method Fails() 
+  ensures false {
+}
\ No newline at end of file
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/Input/src/source2.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/Input/src/source2.dfy
new file mode 100644
index 00000000000..c6d3780d34b
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/Input/src/source2.dfy
@@ -0,0 +1,7 @@
+method Succeeds2()
+  ensures true {
+}
+
+method Fails2() 
+  ensures false {
+}
\ No newline at end of file
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/boogie-filter.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/boogie-filter.dfy
new file mode 100644
index 00000000000..7fe96e730b4
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/boogie-filter.dfy
@@ -0,0 +1,11 @@
+// RUN: %verify --boogie-filter='*Succeeds*' --bprint:"%t.bpl" %s > %t
+// RUN: ! %verify %s >> %t
+// RUN: %diff "%s.expect" "%t"
+
+method Succeeds()
+  ensures true {
+}
+
+method Fails() 
+  ensures false {
+}
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/boogie-filter.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/boogie-filter.dfy.expect
new file mode 100644
index 00000000000..b2fd7799fda
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/boogie-filter.dfy.expect
@@ -0,0 +1,6 @@
+
+Dafny program verifier finished with 1 verified, 0 errors
+filter.dfy(10,16): Error: a postcondition could not be proved on this return path
+filter.dfy(10,10): Related location: this is the postcondition that could not be proved
+
+Dafny program verifier finished with 1 verified, 1 error
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/filter.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/filter.dfy
index 7fe96e730b4..05f0bd73a0a 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/filter.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/filter.dfy
@@ -1,5 +1,7 @@
-// RUN: %verify --boogie-filter='*Succeeds*' --bprint:"%t.bpl" %s > %t
-// RUN: ! %verify %s >> %t
+// RUN: ! %verify --filter-position='filter.dfy' %s > %t
+// RUN: ! %verify --filter-position='filter.dfy:12' %s >> %t
+// RUN: ! %verify --filter-position='src/source1.dfy:5' %S/Input/dfyconfig.toml >> %t
+// RUN: %verify --filter-position='src/source1.dfy:2' %S/Input/dfyconfig.toml >> %t
 // RUN: %diff "%s.expect" "%t"
 
 method Succeeds()
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/filter.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/filter.dfy.expect
index b2fd7799fda..ebb6db3646d 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/filter.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/filter.dfy.expect
@@ -1,6 +1,14 @@
-
-Dafny program verifier finished with 1 verified, 0 errors
-filter.dfy(10,16): Error: a postcondition could not be proved on this return path
-filter.dfy(10,10): Related location: this is the postcondition that could not be proved
+filter.dfy(12,16): Error: a postcondition could not be proved on this return path
+filter.dfy(12,10): Related location: this is the postcondition that could not be proved
 
 Dafny program verifier finished with 1 verified, 1 error
+filter.dfy(12,16): Error: a postcondition could not be proved on this return path
+filter.dfy(12,10): Related location: this is the postcondition that could not be proved
+
+Dafny program verifier finished with 0 verified, 1 error
+source1.dfy(6,16): Error: a postcondition could not be proved on this return path
+source1.dfy(6,10): Related location: this is the postcondition that could not be proved
+
+Dafny program verifier finished with 0 verified, 1 error
+
+Dafny program verifier finished with 1 verified, 0 errors

From c0b1495613af4cb0ea72c09ea5d048d331d20bb8 Mon Sep 17 00:00:00 2001
From: Remy Willems <rwillems@amazon.com>
Date: Wed, 24 Jan 2024 16:06:51 +0100
Subject: [PATCH 3/6] Update filter tests

---
 Source/DafnyDriver/CliCompilation.cs                       | 7 ++++++-
 Source/DafnyDriver/Commands/VerifyCommand.cs               | 6 +++---
 .../TestFiles/LitTests/LitTest/verification/filter.dfy     | 6 ++++--
 3 files changed, 13 insertions(+), 6 deletions(-)

diff --git a/Source/DafnyDriver/CliCompilation.cs b/Source/DafnyDriver/CliCompilation.cs
index 83bcc8ac0bf..92d2cb7f754 100644
--- a/Source/DafnyDriver/CliCompilation.cs
+++ b/Source/DafnyDriver/CliCompilation.cs
@@ -16,6 +16,7 @@
 using Microsoft.Extensions.Logging;
 using VC;
 using IToken = Microsoft.Dafny.IToken;
+using Token = Microsoft.Dafny.Token;
 
 namespace DafnyDriver.Commands;
 
@@ -240,8 +241,12 @@ private List<ICanVerify> FilterCanVerifies(List<ICanVerify> canVerifies) {
       return canVerifies;
     }
 
-    var regex = new Regex(@"((?:[\w.-]+\/)*[\w.-]+)(?::(\d+))?");
+    var regex = new Regex(@"(.+)(?::(\d+))?", RegexOptions.RightToLeft);
     var result = regex.Match(filterPosition);
+    if (result.Length != filterPosition.Length || !result.Success) {
+      Compilation.Reporter.Error(MessageSource.Project, Token.Cli, "Could not parse value passed to --filter-position");
+      return new List<ICanVerify>();
+    }
     var filePart = result.Groups[1].Value;
     string? linePart = result.Groups.Count > 2 ? result.Groups[2].Value : null;
     var fileFiltered = canVerifies.Where(c => c.Tok.Uri.ToString().EndsWith(filePart)).ToList();
diff --git a/Source/DafnyDriver/Commands/VerifyCommand.cs b/Source/DafnyDriver/Commands/VerifyCommand.cs
index 9cb4f763462..ed2916be247 100644
--- a/Source/DafnyDriver/Commands/VerifyCommand.cs
+++ b/Source/DafnyDriver/Commands/VerifyCommand.cs
@@ -14,9 +14,9 @@ public static class VerifyCommand {
   static VerifyCommand() {
     DooFile.RegisterNoChecksNeeded(FilterPosition);
   }
-
-  public static Option<string> FilterPosition = new("--filter-position",
-    @"Filter what gets verified based on a source location. The location is specified as a file path suffix that allows wildcards, optionally followed by a colon and a line number. For example, ""--filter=lastFolder/source.dfy:23""");
+  
+  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: ""--filter=lastFolder/source.dfy:23""");
 
   public static Command Create() {
     var result = new Command("verify", "Verify the program.");
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/filter.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/filter.dfy
index 05f0bd73a0a..82fd7c50ff2 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/filter.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/filter.dfy
@@ -1,5 +1,7 @@
-// RUN: ! %verify --filter-position='filter.dfy' %s > %t
-// RUN: ! %verify --filter-position='filter.dfy:12' %s >> %t
+// RUN: %verify --filter-position='blaergaerga' %s > %t
+// RUN: %verify --filter-position='C:\windows\path.dfy' %s >> %t
+// RUN: ! %verify --filter-position='filter.dfy' %s >> %t
+// RUN: ! %verify --filter-position='filter.dfy:14' %s >> %t
 // RUN: ! %verify --filter-position='src/source1.dfy:5' %S/Input/dfyconfig.toml >> %t
 // RUN: %verify --filter-position='src/source1.dfy:2' %S/Input/dfyconfig.toml >> %t
 // RUN: %diff "%s.expect" "%t"

From ed3fbc36717fce3eab75800e7a8c95003c82794b Mon Sep 17 00:00:00 2001
From: Remy Willems <rwillems@amazon.com>
Date: Wed, 24 Jan 2024 16:09:42 +0100
Subject: [PATCH 4/6] Add release note

---
 Source/DafnyDriver/CliCompilation.cs | 10 +++++-----
 docs/dev/news/4816.feat              |  1 +
 2 files changed, 6 insertions(+), 5 deletions(-)
 create mode 100644 docs/dev/news/4816.feat

diff --git a/Source/DafnyDriver/CliCompilation.cs b/Source/DafnyDriver/CliCompilation.cs
index 92d2cb7f754..b19e6c5b75c 100644
--- a/Source/DafnyDriver/CliCompilation.cs
+++ b/Source/DafnyDriver/CliCompilation.cs
@@ -250,12 +250,12 @@ private List<ICanVerify> FilterCanVerifies(List<ICanVerify> canVerifies) {
     var filePart = result.Groups[1].Value;
     string? linePart = result.Groups.Count > 2 ? result.Groups[2].Value : null;
     var fileFiltered = canVerifies.Where(c => c.Tok.Uri.ToString().EndsWith(filePart)).ToList();
-    if (!string.IsNullOrEmpty(linePart)) {
-      var line = int.Parse(linePart);
-      return fileFiltered.Where(c =>
-        c.RangeToken.StartToken.line <= line && line <= c.RangeToken.EndToken.line).ToList();
+    if (string.IsNullOrEmpty(linePart)) {
+      return fileFiltered;
     }
 
-    return fileFiltered;
+    var line = int.Parse(linePart);
+    return fileFiltered.Where(c =>
+        c.RangeToken.StartToken.line <= line && line <= c.RangeToken.EndToken.line).ToList();
   }
 }
\ No newline at end of file
diff --git a/docs/dev/news/4816.feat b/docs/dev/news/4816.feat
new file mode 100644
index 00000000000..82004d21786
--- /dev/null
+++ b/docs/dev/news/4816.feat
@@ -0,0 +1 @@
+Add an option `--filter-position` to the `dafny verify` command, that allows verifying a single function or method, based on a file path and a line number. For example, `dafny verify dfyconfig.toml --filter-position=source1.dfy:5` will only verify thing that ranges over line 5 in the file `source1.dfy`.
\ No newline at end of file

From 4fa300ede156d0c2b8c600d3a1dd53509666fe7b Mon Sep 17 00:00:00 2001
From: Remy Willems <rwillems@amazon.com>
Date: Wed, 24 Jan 2024 16:14:09 +0100
Subject: [PATCH 5/6] Fix formatting

---
 Source/DafnyDriver/Commands/VerifyCommand.cs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Source/DafnyDriver/Commands/VerifyCommand.cs b/Source/DafnyDriver/Commands/VerifyCommand.cs
index ed2916be247..258be4d6a3e 100644
--- a/Source/DafnyDriver/Commands/VerifyCommand.cs
+++ b/Source/DafnyDriver/Commands/VerifyCommand.cs
@@ -14,7 +14,7 @@ public static class VerifyCommand {
   static VerifyCommand() {
     DooFile.RegisterNoChecksNeeded(FilterPosition);
   }
-  
+
   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: ""--filter=lastFolder/source.dfy:23""");
 

From 950be3e61d7035371998b1f2d66cbd35d7c6d2bf Mon Sep 17 00:00:00 2001
From: Remy Willems <rwillems@amazon.com>
Date: Wed, 24 Jan 2024 18:44:02 +0100
Subject: [PATCH 6/6] Fixes

---
 .../verification/{Input => Inputs}/dfyconfig.toml    |  0
 .../verification/{Input => Inputs}/src/source1.dfy   |  0
 .../verification/{Input => Inputs}/src/source2.dfy   |  0
 .../LitTest/verification/boogie-filter.dfy.expect    |  4 ++--
 .../LitTests/LitTest/verification/filter.dfy         |  4 ++--
 .../LitTests/LitTest/verification/filter.dfy.expect  | 12 ++++++++----
 6 files changed, 12 insertions(+), 8 deletions(-)
 rename Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/{Input => Inputs}/dfyconfig.toml (100%)
 rename Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/{Input => Inputs}/src/source1.dfy (100%)
 rename Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/{Input => Inputs}/src/source2.dfy (100%)

diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/Input/dfyconfig.toml b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/Inputs/dfyconfig.toml
similarity index 100%
rename from Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/Input/dfyconfig.toml
rename to Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/Inputs/dfyconfig.toml
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/Input/src/source1.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/Inputs/src/source1.dfy
similarity index 100%
rename from Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/Input/src/source1.dfy
rename to Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/Inputs/src/source1.dfy
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/Input/src/source2.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/Inputs/src/source2.dfy
similarity index 100%
rename from Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/Input/src/source2.dfy
rename to Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/Inputs/src/source2.dfy
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/boogie-filter.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/boogie-filter.dfy.expect
index b2fd7799fda..0e083ce5590 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/boogie-filter.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/boogie-filter.dfy.expect
@@ -1,6 +1,6 @@
 
 Dafny program verifier finished with 1 verified, 0 errors
-filter.dfy(10,16): Error: a postcondition could not be proved on this return path
-filter.dfy(10,10): Related location: this is the postcondition that could not be proved
+boogie-filter.dfy(10,16): Error: a postcondition could not be proved on this return path
+boogie-filter.dfy(10,10): Related location: this is the postcondition that could not be proved
 
 Dafny program verifier finished with 1 verified, 1 error
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/filter.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/filter.dfy
index 82fd7c50ff2..70e2e1b8286 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/filter.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/filter.dfy
@@ -2,8 +2,8 @@
 // RUN: %verify --filter-position='C:\windows\path.dfy' %s >> %t
 // RUN: ! %verify --filter-position='filter.dfy' %s >> %t
 // RUN: ! %verify --filter-position='filter.dfy:14' %s >> %t
-// RUN: ! %verify --filter-position='src/source1.dfy:5' %S/Input/dfyconfig.toml >> %t
-// RUN: %verify --filter-position='src/source1.dfy:2' %S/Input/dfyconfig.toml >> %t
+// RUN: ! %verify --filter-position='src/source1.dfy:5' %S/Inputs/dfyconfig.toml >> %t
+// RUN: %verify --filter-position='src/source1.dfy:2' %S/Inputs/dfyconfig.toml >> %t
 // RUN: %diff "%s.expect" "%t"
 
 method Succeeds()
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/filter.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/filter.dfy.expect
index ebb6db3646d..e7fc9735c1b 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/filter.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/filter.dfy.expect
@@ -1,9 +1,13 @@
-filter.dfy(12,16): Error: a postcondition could not be proved on this return path
-filter.dfy(12,10): Related location: this is the postcondition that could not be proved
+
+Dafny program verifier finished with 0 verified, 0 errors
+
+Dafny program verifier finished with 0 verified, 0 errors
+filter.dfy(14,16): Error: a postcondition could not be proved on this return path
+filter.dfy(14,10): Related location: this is the postcondition that could not be proved
 
 Dafny program verifier finished with 1 verified, 1 error
-filter.dfy(12,16): Error: a postcondition could not be proved on this return path
-filter.dfy(12,10): Related location: this is the postcondition that could not be proved
+filter.dfy(14,16): Error: a postcondition could not be proved on this return path
+filter.dfy(14,10): Related location: this is the postcondition that could not be proved
 
 Dafny program verifier finished with 0 verified, 1 error
 source1.dfy(6,16): Error: a postcondition could not be proved on this return path