diff --git a/Source/DafnyLanguageServer.Test/GutterStatus/SimpleLinearVerificationGutterStatusTester.cs b/Source/DafnyLanguageServer.Test/GutterStatus/SimpleLinearVerificationGutterStatusTester.cs
index 2ad64631be1..c3ba836b81e 100644
--- a/Source/DafnyLanguageServer.Test/GutterStatus/SimpleLinearVerificationGutterStatusTester.cs
+++ b/Source/DafnyLanguageServer.Test/GutterStatus/SimpleLinearVerificationGutterStatusTester.cs
@@ -37,6 +37,20 @@ await VerifyTrace(@"
  ? :}", false, intermediates: false);
   }
 
+  [Fact]
+  public async Task ConstantWithoutRhsMarkedAsVerified() {
+    await VerifyTrace(@"
+ | :class Test {
+ | :  const x: int
+ | :
+ | :  method Testing()
+ | :    requires x > 0
+ | :    ensures x != 0
+ | :  {
+ | :  }
+ | :}", false, intermediates: false);
+  }
+
   [Fact]
   public async Task Fields() {
     var markedSource = @"
diff --git a/Source/DafnyLanguageServer/Workspace/GutterIconAndHoverVerificationDetailsManager.cs b/Source/DafnyLanguageServer/Workspace/GutterIconAndHoverVerificationDetailsManager.cs
index 1c22e7b77db..77d7cd2a214 100644
--- a/Source/DafnyLanguageServer/Workspace/GutterIconAndHoverVerificationDetailsManager.cs
+++ b/Source/DafnyLanguageServer/Workspace/GutterIconAndHoverVerificationDetailsManager.cs
@@ -80,9 +80,8 @@ void AddAndPossiblyMigrateVerificationTree(VerificationTree verificationTree) {
               continue;
             }
 
-            if (member is ConstantField) {
-              var constantHasNoBody = member.RangeToken.EndToken.line == 0;
-              if (constantHasNoBody) {
+            if (member is ConstantField constantField) {
+              if (constantField.Rhs == null) {
                 continue; // Nothing to verify
               }
 
diff --git a/docs/dev/news/5841.fix b/docs/dev/news/5841.fix
new file mode 100644
index 00000000000..df5fa34687a
--- /dev/null
+++ b/docs/dev/news/5841.fix
@@ -0,0 +1 @@
+Green gutter icons cover constants without RHS