Add test for issue #4287

dafny-lang · Jul 14, 2023 · 90d020e · 90d020e
1 parent 12d49a7
commit 90d020e
Showing 1 changed file with 8 additions and 0 deletions.
diff --git a/Source/DafnyLanguageServer.Test/GutterStatus/SimpleLinearVerificationGutterStatusTester.cs b/Source/DafnyLanguageServer.Test/GutterStatus/SimpleLinearVerificationGutterStatusTester.cs
@@ -13,6 +13,14 @@ public class SimpleLinearVerificationGutterStatusTester : LinearVerificationGutt
   // the test will fail and give the correct output that can be use for the test
   // Add '//Next<n>:' to edit a line multiple times
 
+  [Fact]
+  public async Task GitIssue4287GutterHighlightingBroken() {
+    await VerifyTrace(@"
+method Test() {
+  assert false;
+}", intermediates: false);
+  }
+
   [Fact]
   public async Task GitIssue3821GutterIgnoredProblem() {
     await VerifyTrace(@"