diff --git a/Source/DafnyDriver/Commands/CoverageReportCommand.cs b/Source/DafnyDriver/Commands/CoverageReportCommand.cs
index 846e71440b4..b5b538384c3 100644
--- a/Source/DafnyDriver/Commands/CoverageReportCommand.cs
+++ b/Source/DafnyDriver/Commands/CoverageReportCommand.cs
@@ -7,20 +7,26 @@
 using System.IO;
 using System.Linq;
 using System.Threading.Tasks;
+using DafnyCore;
 
 namespace Microsoft.Dafny; 
 
 static class CoverageReportCommand {
 
+  public static readonly Option<CoverageLabel?> OnlyLabelOption = new("--only-label",
+    "Skip coverage labels other than the given one, after merging labels from the input reports.");
+
   public static IEnumerable<Option> Options =>
     new Option[] {
       CommonOptionBag.NoTimeStampForCoverageReport,
+      OnlyLabelOption
     };
 
   static CoverageReportCommand() {
     ReportsArgument = new("reports", r => {
       return r.Tokens.Where(t => !string.IsNullOrEmpty(t.Value)).Select(t => new FileInfo(t.Value)).ToList();
     }, true, "directories with coverage reports to be merged");
+    DooFile.RegisterNoChecksNeeded(OnlyLabelOption);
   }
 
   // FilesArgument is intended for Dafny files, so CoverageReportCommand adds its own argument instead
diff --git a/Source/DafnyDriver/CoverageReporter.cs b/Source/DafnyDriver/CoverageReporter.cs
index 15eee5f94d5..dc170fc0d98 100644
--- a/Source/DafnyDriver/CoverageReporter.cs
+++ b/Source/DafnyDriver/CoverageReporter.cs
@@ -85,11 +85,15 @@ public void Merge(List<string> coverageReportsToMerge, string coverageReportOutD
         reports.Add(ParseCoverageReport(reportDir, $"{name} ({Path.GetFileName(reportDir)})", units, suffix));
       }
     }
+
+    var onlyLabel = options.Get(CoverageReportCommand.OnlyLabelOption);
     foreach (var report in reports) {
       foreach (var fileName in report.AllFiles()) {
         foreach (var span in report.CoverageSpansForFile(fileName)) {
           mergedReport.RegisterFile(span.Span.Uri);
-          mergedReport.LabelCode(span.Span, span.Label);
+          if ((onlyLabel ?? span.Label) == span.Label) {
+            mergedReport.LabelCode(span.Span, span.Label);
+          }
         }
       }
     }
diff --git a/Test/logger/CoverageReport.dfy b/Test/logger/CoverageReport.dfy
index 36a14821d85..dc530f4421e 100644
--- a/Test/logger/CoverageReport.dfy
+++ b/Test/logger/CoverageReport.dfy
@@ -14,6 +14,11 @@
 // RUN: %baredafny merge-coverage-reports --no-timestamp-for-coverage-report "%t"/coverage_combined "%t"/coverage_testing "%t"/coverage_verification
 // RUN: %sed 's/<h1 hidden.*//' "%t"/coverage_combined/ProofDependencyLogging.dfy_combined.html > "%t"/coverage_combined.html
 // RUN: %diff "%S/ProofDependencyLogging.dfy_combined.html.expect" "%t/coverage_combined.html"
+// Combined, limited coverage:
+// RUN: rm -rf "%t"/coverage_combined
+// RUN: %baredafny merge-coverage-reports --only-label NotCovered --no-timestamp-for-coverage-report "%t"/coverage_combined_limited "%t"/coverage_testing "%t"/coverage_verification
+// RUN: %sed 's/<h1 hidden.*//' "%t"/coverage_combined_limited/ProofDependencyLogging.dfy_combined.html > "%t"/coverage_combined_limited.html
+// RUN: %diff "%S/ProofDependencyLogging.dfy_combined_limited.html.expect" "%t/coverage_combined_limited.html"
 
 
 include "ProofDependencyLogging.dfy"
diff --git a/Test/logger/ProofDependencyLogging.dfy_combined_limited.html.expect b/Test/logger/ProofDependencyLogging.dfy_combined_limited.html.expect
new file mode 100644
index 00000000000..5a004f2552c
--- /dev/null
+++ b/Test/logger/ProofDependencyLogging.dfy_combined_limited.html.expect
@@ -0,0 +1,484 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
+<html
+        xmlns="http://www.w3.org/1999/xhtml" lang="en">
+<head>
+    <meta http-equiv="Content-Type" content="text/html;charset=UTF-8"/>
+    <link rel="stylesheet" href="./.resources/coverage.css" type="text/css"/>
+    <title>ProofDependencyLogging.dfy, Combined Coverage Report</title>
+</head>
+<body onload="window['PR_TAB_WIDTH']=4">
+<div class="menu" id="menu">
+    <a href="./index_combined.html">Index</a>
+    <a href="ProofDependencyLogging.dfy_tests_expected_2.html" class="el_report">Expected Test Coverage (coverage_testing)</a><a href="ProofDependencyLogging.dfy_verification_3.html" class="el_report">Verification coverage (coverage_verification)</a>
+</div>
+<h1>ProofDependencyLogging.dfy, Combined Coverage Report</h1>
+
+<pre class="source lang-java linenums">
+<span class="na" id="1:1">// RUN: %baredafny verify --log-format:text --boogie -trackVerificationCoverage "%s" > "%t"
+// RUN: %OutputCheck --file-to-check "%t" "%s"
+// CHECK: Results for M.RedundantAssumeMethod \(correctness\)
+// CHECK:     Proof dependencies:
+// CHECK:       ProofDependencyLogging.dfy\(177,12\)-\(177,16\): assume statement
+// CHECK:       ProofDependencyLogging.dfy\(178,12\)-\(178,16\): assertion always holds
+//
+// CHECK: Results for M.ContradictoryAssumeMethod \(correctness\)
+// CHECK:     Proof dependencies:
+// CHECK:       ProofDependencyLogging.dfy\(183,12\)-\(183,16\): assume statement
+// CHECK:       ProofDependencyLogging.dfy\(184,12\)-\(184,16\): assume statement
+//
+// CHECK: Results for M.AssumeFalseMethod \(correctness\)
+// CHECK:     Proof dependencies:
+// CHECK:       ProofDependencyLogging.dfy\(192,12\)-\(192,12\): assume statement
+//
+// CHECK: Results for M.ObviouslyContradictoryRequiresFunc \(well-formedness\)
+// CHECK:     Proof dependencies:
+// CHECK:       ProofDependencyLogging.dfy\(198,12\)-\(198,16\): requires clause
+// CHECK:       ProofDependencyLogging.dfy\(199,12\)-\(199,16\): requires clause
+//
+// CHECK: Results for M.ObviouslyContradictoryRequiresMethod \(correctness\)
+// CHECK:     Proof dependencies:
+// CHECK:       ProofDependencyLogging.dfy\(207,12\)-\(207,16\): requires clause
+// CHECK:       ProofDependencyLogging.dfy\(208,12\)-\(208,16\): requires clause
+//
+// CHECK: Results for M.ObviouslyRedundantRequiresFunc \(well-formedness\)
+// CHECK:     Proof dependencies:
+// CHECK:       ProofDependencyLogging.dfy\(216,1\)-\(222,1\): function definition for ObviouslyRedundantRequiresFunc
+// CHECK:       ProofDependencyLogging.dfy\(217,12\)-\(217,16\): requires clause
+// CHECK:       ProofDependencyLogging.dfy\(219,11\)-\(219,15\): ensures clause
+// CHECK:       ProofDependencyLogging.dfy\(221,3\)-\(221,7\): function call result
+// CHECK:       ProofDependencyLogging.dfy\(221,5\)-\(221,5\): value always satisfies the subset constraints of 'nat'
+//
+// CHECK: Results for M.ObviouslyRedundantRequiresMethod \(correctness\)
+// CHECK:     Proof dependencies:
+// CHECK:       ProofDependencyLogging.dfy\(225,12\)-\(225,16\): requires clause
+// CHECK:       ProofDependencyLogging.dfy\(227,11\)-\(227,15\): ensures clause
+// CHECK:       ProofDependencyLogging.dfy\(229,12\)-\(229,12\): value always satisfies the subset constraints of 'nat'
+// CHECK:       ProofDependencyLogging.dfy\(229,3\)-\(229,15\): assignment \(or return\)
+//
+// CHECK: Results for M.ObviouslyUnnecessaryRequiresFunc \(well-formedness\)
+// CHECK:     Proof dependencies:
+// CHECK:       ProofDependencyLogging.dfy\(237,21\)-\(237,21\): value always satisfies the subset constraints of 'nat'
+// CHECK:       ProofDependencyLogging.dfy\(237,32\)-\(237,32\): value always satisfies the subset constraints of 'nat'
+//
+// CHECK: Results for M.ObviouslyUnnecessaryRequiresMethod \(correctness\)
+// CHECK:     Proof dependencies:
+// CHECK:       ProofDependencyLogging.dfy\(244,25\)-\(244,25\): value always satisfies the subset constraints of 'nat'
+// CHECK:       ProofDependencyLogging.dfy\(244,48\)-\(244,48\): value always satisfies the subset constraints of 'nat'
+//
+// CHECK: Results for M.ObviouslyUnconstrainedCodeFunc \(well-formedness\)
+// CHECK:     Proof dependencies:
+// CHECK:       ProofDependencyLogging.dfy\(248,1\)-\(256,1\): function definition for ObviouslyUnconstrainedCodeFunc
+// CHECK:       ProofDependencyLogging.dfy\(249,12\)-\(249,16\): requires clause
+// CHECK:       ProofDependencyLogging.dfy\(250,11\)-\(250,17\): ensures clause
+// CHECK:       ProofDependencyLogging.dfy\(252,12\)-\(252,16\): let expression binding RHS well-formed
+// CHECK:       ProofDependencyLogging.dfy\(252,7\)-\(252,7\): let expression binding
+// CHECK:       ProofDependencyLogging.dfy\(254,3\)-\(254,3\): let expression result
+//
+// CHECK: Results for M.ObviouslyUnconstrainedCodeMethod \(correctness\)
+// CHECK:     Proof dependencies:
+// CHECK:       ProofDependencyLogging.dfy\(259,12\)-\(259,16\): requires clause
+// CHECK:       ProofDependencyLogging.dfy\(260,11\)-\(260,17\): ensures clause
+// CHECK:       ProofDependencyLogging.dfy\(262,9\)-\(262,17\): assignment \(or return\)
+// CHECK:       ProofDependencyLogging.dfy\(264,3\)-\(266,8\): assignment \(or return\)
+//
+// CHECK: Results for M.PartiallyRedundantRequiresFunc \(well-formedness\)
+// CHECK:     Proof dependencies:
+// CHECK:       ProofDependencyLogging.dfy\(270,1\)-\(275,1\): function definition for PartiallyRedundantRequiresFunc
+// CHECK:       ProofDependencyLogging.dfy\(271,23\)-\(271,27\): requires clause
+// CHECK:       ProofDependencyLogging.dfy\(272,11\)-\(272,15\): ensures clause
+// CHECK:       ProofDependencyLogging.dfy\(274,3\)-\(274,7\): function call result
+// CHECK:       ProofDependencyLogging.dfy\(274,5\)-\(274,5\): value always satisfies the subset constraints of 'nat'
+//
+// CHECK: Results for M.PartiallyUnnecessaryRequiresFunc \(well-formedness\)
+// CHECK:     Proof dependencies:
+// CHECK:       ProofDependencyLogging.dfy\(279,22\)-\(279,26\): requires clause
+// CHECK:       ProofDependencyLogging.dfy\(282,21\)-\(282,21\): value always satisfies the subset constraints of 'nat'
+// CHECK:       ProofDependencyLogging.dfy\(282,32\)-\(282,32\): value always satisfies the subset constraints of 'nat'
+//
+// CHECK: Results for M.MultiPartRedundantRequiresFunc \(well-formedness\)
+// CHECK:     Proof dependencies:
+// CHECK:       ProofDependencyLogging.dfy\(288,1\)-\(295,1\): function definition for MultiPartRedundantRequiresFunc
+// CHECK:       ProofDependencyLogging.dfy\(291,12\)-\(291,17\): requires clause
+// CHECK:       ProofDependencyLogging.dfy\(292,11\)-\(292,16\): ensures clause
+// CHECK:       ProofDependencyLogging.dfy\(294,3\)-\(294,3\): function call result
+//
+// CHECK: Results for M.MultiPartRedundantRequiresMethod \(correctness\)
+// CHECK:     Proof dependencies:
+// CHECK:       ProofDependencyLogging.dfy\(300,12\)-\(300,17\): requires clause
+// CHECK:       ProofDependencyLogging.dfy\(301,11\)-\(301,16\): ensures clause
+//
+// CHECK: Results for M.MultiPartContradictoryRequiresFunc \(well-formedness\)
+// CHECK:     Proof dependencies:
+// CHECK:       ProofDependencyLogging.dfy\(309,1\)-\(316,1\): function definition for MultiPartContradictoryRequiresFunc
+// CHECK:       ProofDependencyLogging.dfy\(310,12\)-\(310,16\): requires clause
+// CHECK:       ProofDependencyLogging.dfy\(311,12\)-\(311,16\): requires clause
+// CHECK:       ProofDependencyLogging.dfy\(313,11\)-\(313,16\): ensures clause
+// CHECK:       ProofDependencyLogging.dfy\(315,3\)-\(315,3\): function call result
+//
+// CHECK: Results for M.MultiPartContradictoryRequiresMethod \(correctness\)
+// CHECK:     Proof dependencies:
+// CHECK:       ProofDependencyLogging.dfy\(319,12\)-\(319,16\): requires clause
+// CHECK:       ProofDependencyLogging.dfy\(320,12\)-\(320,16\): requires clause
+// CHECK:       ProofDependencyLogging.dfy\(322,11\)-\(322,16\): ensures clause
+//
+// CHECK: Results for M.CallContradictoryFunctionFunc \(well-formedness\)
+// CHECK:     Proof dependencies:
+// CHECK:       ProofDependencyLogging.dfy\(336,1\)-\(342,1\): function definition for CallContradictoryFunctionFunc
+// CHECK:       ProofDependencyLogging.dfy\(337,12\)-\(337,16\): requires clause
+// CHECK:       ProofDependencyLogging.dfy\(338,11\)-\(338,15\): ensures clause
+// CHECK:       ProofDependencyLogging.dfy\(341,3\)-\(341,3\): function precondition satisfied
+// CHECK:       ProofDependencyLogging.dfy\(341,3\)-\(341,39\): function call result
+//
+// CHECK: Results for M.CallContradictoryMethodMethod \(correctness\)
+// CHECK:     Proof dependencies:
+// CHECK:       ProofDependencyLogging.dfy\(345,12\)-\(345,16\): requires clause
+// CHECK:       ProofDependencyLogging.dfy\(348,9\)-\(348,47\): ensures clause at ProofDependencyLogging.dfy\(333,12\)-\(333,25\) from call
+// CHECK:       ProofDependencyLogging.dfy\(348,9\)-\(348,47\): ensures clause at ProofDependencyLogging.dfy\(333,12\)-\(333,25\) from call
+// CHECK:       ProofDependencyLogging.dfy\(348,9\)-\(348,47\): requires clause at ProofDependencyLogging.dfy\(332,12\)-\(332,16\) from call
+//
+// CHECK: Results for M.FalseAntecedentRequiresClauseMethod \(correctness\)
+// CHECK:     Proof dependencies:
+// CHECK:       ProofDependencyLogging.dfy\(357,3\)-\(357,15\): assignment \(or return\)
+//
+// CHECK: Results for M.FalseAntecedentAssertStatementMethod \(correctness\)
+// CHECK:     Proof dependencies:
+// CHECK:       ProofDependencyLogging.dfy\(362,9\)-\(362,15\): assignment \(or return\)
+// CHECK:       ProofDependencyLogging.dfy\(363,20\)-\(363,24\): assertion always holds
+//
+// CHECK: Results for M.FalseAntecedentEnsuresClauseMethod \(correctness\)
+// CHECK:     Proof dependencies:
+// CHECK:       ProofDependencyLogging.dfy\(368,11\)-\(368,25\): ensures clause
+// CHECK:       ProofDependencyLogging.dfy\(370,3\)-\(370,13\): assignment \(or return\)
+//
+// CHECK: Results for M.ObviouslyUnreachableIfExpressionBranchFunc \(well-formedness\)
+// CHECK:     Proof dependencies:
+// CHECK:       ProofDependencyLogging.dfy\(373,1\)-\(380,1\): function definition for ObviouslyUnreachableIfExpressionBranchFunc
+// CHECK:       ProofDependencyLogging.dfy\(374,12\)-\(374,16\): requires clause
+// CHECK:       ProofDependencyLogging.dfy\(375,11\)-\(375,15\): ensures clause
+// CHECK:       ProofDependencyLogging.dfy\(379,8\)-\(379,12\): if expression else branch
+//
+// CHECK: Results for M.ObviouslyUnreachableIfStatementBranchMethod \(correctness\)
+// CHECK:     Proof dependencies:
+// CHECK:       ProofDependencyLogging.dfy\(383,12\)-\(383,16\): requires clause
+// CHECK:       ProofDependencyLogging.dfy\(384,11\)-\(384,15\): ensures clause
+// CHECK:       ProofDependencyLogging.dfy\(389,5\)-\(389,17\): assignment \(or return\)
+//
+// CHECK: Results for M.ObviouslyUnreachableMatchExpressionCaseFunction \(well-formedness\)
+//
+// CHECK:     Proof dependencies:
+// CHECK:       ProofDependencyLogging.dfy\(395,1\)-\(403,1\): function definition for ObviouslyUnreachableMatchExpressionCaseFunction
+// CHECK:       ProofDependencyLogging.dfy\(396,12\)-\(396,17\): requires clause
+// CHECK:       ProofDependencyLogging.dfy\(397,11\)-\(397,15\): ensures clause
+// CHECK:       ProofDependencyLogging.dfy\(401,15\)-\(401,15\): match expression branch result
+//
+// CHECK: Results for M.ObviouslyUnreachableMatchStatementCaseMethod \(correctness\)
+// CHECK:     Proof dependencies:
+// CHECK:       ProofDependencyLogging.dfy\(406,12\)-\(406,17\): requires clause
+// CHECK:       ProofDependencyLogging.dfy\(407,11\)-\(407,15\): ensures clause
+// CHECK:       ProofDependencyLogging.dfy\(411,15\)-\(411,23\): assignment \(or return\)
+//
+// CHECK: Results for M.ObviouslyUnreachableReturnStatementMethod \(correctness\)
+// CHECK:     Proof dependencies:
+// CHECK:       ProofDependencyLogging.dfy\(416,12\)-\(416,17\): requires clause
+// CHECK:       ProofDependencyLogging.dfy\(417,13\)-\(417,17\): ensures clause
+// CHECK:       ProofDependencyLogging.dfy\(420,7\)-\(420,15\): assignment \(or return\)
+
+
+module M {
+
+method {:testEntry} RedundantAssumeMethod(n: int)
+{
+    // either one or the other assumption shouldn't be covered
+    assume </span><span class="nc" id="176:12">n > 4</span><span class="na" id="176:17">;
+    assume n > 3;
+    assert n > 1;
+}
+
+method {:testEntry} ContradictoryAssumeMethod(n: int)
+</span><span class="nc" id="182:1">{
+    assume n > 0;
+    assume n < 0;
+    assume n == 5; // shouldn't be covered
+    assert n < 10; // shouldn't be covered
+}
+
+</span><span class="na" id="189:1">method {:testEntry} AssumeFalseMethod(n: int)
+</span><span class="nc" id="190:1">{
+    assume n == 15; // shouldn't be covered
+    assume false;
+    assert n < 10; // shouldn't be covered
+}
+
+</span><span class="na" id="196:1">// Obvious contradiction in requires clauses.
+</span><span class="nc" id="197:1">function {:testEntry} ObviouslyContradictoryRequiresFunc(x: nat): (r: nat)
+</span><span class="na" id="198:1">  requires x > 10
+  requires x < 10
+  ensures </span><span class="nc" id="200:11">r < x</span><span class="na" id="200:16"> // only provable vacuously 
+{
+</span><span class="nc" id="202:1">  assert x == 10; // contradicts both requires clauses
+  x - 1 // not necessarily a valid nat
+}
+
+</span><span class="na" id="206:1">method {:testEntry} ObviouslyContradictoryRequiresMethod(x: nat) returns (r: nat)
+  requires x > 10
+  requires x < 10
+  ensures </span><span class="nc" id="209:11">r < x</span><span class="na" id="209:16"> // only provable vacuously
+</span><span class="nc" id="210:1">{
+  assert x == 10; // contradicts both requires clauses
+  return x - 1; // not necessarily a valid nat
+}
+
+</span><span class="na" id="215:1">// Obvious redundancy in requires clauses.
+function {:testEntry} ObviouslyRedundantRequiresFunc(x: nat): (r: nat)
+  requires x < 10
+  requires </span><span class="nc" id="218:12">x < 1</span><span class="na" id="218:17">00 // implied by previous requires clause
+  ensures r < 11 // should cause body and first requires clause to be covered
+{
+  x + 1
+}
+
+method {:testEntry} ObviouslyRedundantRequiresMethod(x: nat) returns (r: nat)
+  requires x < 10
+  requires </span><span class="nc" id="226:12">x < 1</span><span class="na" id="226:17">00 // implied by previous requires clause
+  ensures r < 11 // should cause body and first requires clause to be covered
+{
+  return x + 1;
+</span><span class="nc" id="230:1">}
+
+</span><span class="na" id="232:1">// Obviously unnecessary requires clauses.
+function {:testEntry} ObviouslyUnnecessaryRequiresFunc(x: nat): (r: nat)
+  requires </span><span class="nc" id="234:12">x < 1</span><span class="na" id="234:17">0 // not required for the proof
+{
+  // cause at least a little proof work to be necessary, for nat bounds
+  if (x > 5) then </span><span class="nc" id="237:19">x </span><span class="na" id="237:21">+</span><span class="nc" id="237:22"> 2</span><span class="na" id="237:24"> else </span><span class="nc" id="237:30">x </span><span class="na" id="237:32">+</span><span class="nc" id="237:33"> 1
+</span><span class="na" id="238:1">}
+
+method {:testEntry} ObviouslyUnnecessaryRequiresMethod(x: nat) returns (r: nat)
+  requires </span><span class="nc" id="241:12">x < 1</span><span class="na" id="241:17">0 // not required for the proof
+{
+  // cause at least a little proof work to be necessary, for nat bounds
+  if (x > 5) { r</span><span class="nc" id="244:17">eturn x </span><span class="na" id="244:25">+</span><span class="nc" id="244:26"> 2;</span><span class="na" id="244:29"> } else { r</span><span class="nc" id="244:40">eturn x </span><span class="na" id="244:48">+</span><span class="nc" id="244:49"> 1;</span><span class="na" id="244:52"> }
+</span><span class="nc" id="245:1">}
+
+</span><span class="na" id="247:1">// Code obviously not constrained by ensures clause.
+function {:testEntry} ObviouslyUnconstrainedCodeFunc(x: int): (r: (int, int))
+  requires x > 10
+  ensures r.0 > 10
+{
+  var a := x + 1; // constrained by ensures clause
+  var </span><span class="nc" id="253:7">b</span><span class="na" id="253:8"> := </span><span class="nc" id="253:12">x - 1</span><span class="na" id="253:17">; // not constrained by ensures clause 
+  (a,
+   b)
+}
+
+method {:testEntry} ObviouslyUnconstrainedCodeMethod(x: int) returns (r: (int, int))
+  requires x > 10
+  ensures r.0 > 10
+{
+  var a := x + 1; // constrained by ensures clause
+  var b </span><span class="nc" id="263:9">:= x - 1;</span><span class="na" id="263:18"> // not constrained by ensures clause
+  return
+    (a,
+     b);
+</span><span class="nc" id="267:1">}
+
+</span><span class="na" id="269:1">// Partial redundancy in requires clauses.
+function {:testEntry} PartiallyRedundantRequiresFunc(x: nat): (r: nat)
+  requires </span><span class="nc" id="271:12">x < 1</span><span class="na" id="271:17">00 && x < 10 // LHS implied by RHS
+  ensures r < 11 // should cause body and RHS clause to be covered
+{
+  x + 1
+}
+
+// Partly unnecessary requires clause.
+function {:testEntry} PartiallyUnnecessaryRequiresFunc(x: int): (r: nat)
+  requires </span><span class="nc" id="279:12">x < 1</span><span class="na" id="279:17">0 && x > 0 // RHS required for proof, but not LHS
+{
+  // cause at least a little proof work to be necessary, for nat bounds
+  if (x > 5) then </span><span class="nc" id="282:19">x </span><span class="na" id="282:21">-</span><span class="nc" id="282:22"> 1</span><span class="na" id="282:24"> else </span><span class="nc" id="282:30">x </span><span class="na" id="282:32">+</span><span class="nc" id="282:33"> 1
+</span><span class="na" id="283:1">}
+
+
+// Redundancy of one requires clause due to at least two others, with at least
+// one of the three being partly in a separately-defined function.
+function {:testEntry} MultiPartRedundantRequiresFunc(x: int): (r: int)
+  requires </span><span class="nc" id="289:12">x > 1</span><span class="na" id="289:17">0
+  requires </span><span class="nc" id="290:12">x < 1</span><span class="na" id="290:17">2
+  requires x == 11 // implied by the previous two, but neither individually
+  ensures r == 11
+{
+  x
+}
+
+method {:testEntry} MultiPartRedundantRequiresMethod(x: int) returns (r: int)
+  requires </span><span class="nc" id="298:12">x > 1</span><span class="na" id="298:17">0
+  requires </span><span class="nc" id="299:12">x < 1</span><span class="na" id="299:17">2
+  requires x == 11 // implied by the previous two, but neither individually
+  ensures r == 11
+{
+  r</span><span class="nc" id="303:4">eturn x;
+}
+
+</span><span class="na" id="306:1">// Contradiction between three different requires clauses, with at least one of
+// the three being partly in a separately-defined function (function and
+// method).
+function {:testEntry} MultiPartContradictoryRequiresFunc(x: int, y: int): (r: int)
+  requires x > 10
+  requires x < 12
+  requires </span><span class="nc" id="312:12">y != 1</span><span class="na" id="312:18">1 // contradicts the previous two
+  ensures r == 11 // provable from first two preconditions, but shouldn't be covered
+{
+  x
+}
+
+method {:testEntry} MultiPartContradictoryRequiresMethod(x: int, y: int) returns (r: int)
+  requires x > 10
+  requires x < 12
+  requires </span><span class="nc" id="321:12">y != 1</span><span class="na" id="321:18">1 // contradicts the previous two
+  ensures r == 11 // provable from first two preconditions, but shouldn't be covered
+{
+  r</span><span class="nc" id="324:4">eturn x;
+}
+
+</span><span class="na" id="327:1">function {:testEntry} ContradictoryEnsuresClauseFunc(x: int): (r: int)
+  requires </span><span class="nc" id="328:12">x > 1
+</span><span class="na" id="329:1">  ensures  </span><span class="nc" id="329:12">r > x && r < 0
+
+</span><span class="na" id="331:1">method {:testEntry} ContradictoryEnsuresClauseMethod(x: int) returns (r: int)
+  requires </span><span class="nc" id="332:12">x > 1
+</span><span class="na" id="333:1">  ensures  </span><span class="nc" id="333:12">r > x && r < 0
+
+</span><span class="na" id="335:1">// Call function that has contradictory ensures clauses.
+</span><span class="nc" id="336:1">function {:testEntry} CallContradictoryFunctionFunc(x: int): (r: int)
+</span><span class="na" id="337:1">  requires x > 1
+  ensures r < 0
+{
+  // TODO: Dafny doesn't generate sufficient Boogie code to make the contradiction detectable
+</span><span class="nc" id="341:1">  ContradictoryEnsuresClauseFunc(x) - 1
+}
+
+</span><span class="na" id="344:1">method {:testEntry} CallContradictoryMethodMethod(x: int) returns (r: int)
+  requires x > 1
+  ensures </span><span class="nc" id="346:11">r < 0
+{
+  var y := ContradictoryEnsuresClauseMethod(x);
+  return y - 1;
+}
+
+</span><span class="na" id="352:1">// False antecedent requires clause
+method {:testEntry} FalseAntecedentRequiresClauseMethod(x: int) returns (r: int)
+  requires </span><span class="nc" id="354:12">x*x < 0 ==> x == x + 1
+</span><span class="na" id="355:1">  ensures r > x
+{
+  return x + 1;
+</span><span class="nc" id="358:1">}
+
+</span><span class="na" id="360:1">// False antecedent assert statement.
+method {:testEntry} FalseAntecedentAssertStatementMethod(x: int) {
+  var y := x*x;
+  assert </span><span class="nc" id="363:10">y < 0 ==> x </span><span class="na" id="363:22"><</span><span class="nc" id="363:23"> 0</span><span class="na" id="363:25">;
+}
+
+// False antecedent ensures clause.
+method {:testEntry} FalseAntecedentEnsuresClauseMethod(x: int) returns (r: int)
+  ensures r < 0 ==> x < 0
+{
+  return x*x;
+</span><span class="nc" id="371:1">}
+
+</span><span class="na" id="373:1">function {:testEntry} ObviouslyUnreachableIfExpressionBranchFunc(x: int): (r:int)
+  requires x > 0
+  ensures r > 0
+{
+  if x < 0
+</span><span class="nc" id="378:1">  then x - 1 // unreachable
+</span><span class="na" id="379:1">  else x + 1
+}
+
+method {:testEntry} ObviouslyUnreachableIfStatementBranchMethod(x: int) returns (r:int)
+  requires x > 0
+  ensures r > 0
+{
+  if x < 0 {
+</span><span class="nc" id="387:1">    return x - 1; // unreachable
+</span><span class="na" id="388:1">  } else {
+    return x + 1;
+  }
+</span><span class="nc" id="391:1">}
+
+</span><span class="na" id="393:1">datatype T = A | B
+
+function {:testEntry} ObviouslyUnreachableMatchExpressionCaseFunction(t: T): (r:int)
+  requires t != A
+  ensures r > 1 // alt: r > 0
+{
+  match t {
+</span><span class="nc" id="400:1">    case A => 1 // unreachable
+</span><span class="na" id="401:1">    case B => 2
+  }
+}
+
+method {:testEntry} ObviouslyUnreachableMatchStatementCaseMethod(t: T) returns (r:int)
+  requires t != A
+  ensures r > 1 // alt: r > 0
+{
+  match t {
+</span><span class="nc" id="410:1">    case A => return 1; // unreachable
+</span><span class="na" id="411:1">    case B => return 2;
+  }
+</span><span class="nc" id="413:1">}
+
+</span><span class="na" id="415:1">method {:testEntry} ObviouslyUnreachableReturnStatementMethod(t: T) returns (r:int)
+  requires t != A
+    ensures r > 1 // alt: r > 0
+  {
+    if !t.A? {
+      return 2;
+    }
+
+</span><span class="nc" id="423:1">    return 1; // unreachable
+</span><span class="na" id="424:1">  </span><span class="nc" id="424:3">}
+
+</span><span class="na" id="426:1">method {:testEntry} CalcStatementWithSideConditions(x: int) {
+  calc == {
+    </span><span class="nc" id="428:5">x </span><span class="na" id="428:7">/</span><span class="nc" id="428:8"> 2;
+    (x*2) </span><span class="na" id="429:11">/</span><span class="nc" id="429:12"> 4</span><span class="na" id="429:14">;
+  }
+}
+
+</span><span class="nc" id="433:1">method {:testEntry} DontWarnAboutVacuousAssertFalse(x: int) {
+  assume x == x + 1;
+  assert false;
+}
+
+</span><span class="na" id="438:1">// CHECK: Results for M.GetX \(well-formedness\)
+// CHECK:     Proof dependencies:
+// CHECK:       ProofDependencyLogging.dfy\(449,5\)-\(449,5\): target object is never null
+
+class C {
+  var x: int
+}
+
+function {:testEntry} GetX(c: C): int
+  reads c
+{
+  </span><span class="nc" id="449:3">c.</span><span class="na" id="449:5">x
+}
+
+method {:testEntry} DontWarnAboutUnusedAssumeTrue(x: int) {
+  assume </span><span class="nc" id="453:10">t</span><span class="na" id="453:11">rue;
+  assert 1 + x == x + 1;
+}
+
+}
+
+</span></pre>
+<div class="footer">
+    <span class="right">
+        Created with 
+        <a href="https://github.com/dafny-lang/dafny">Dafny</a>
+    </span>
+</div>
+</body>
+</html>
\ No newline at end of file
diff --git a/docs/dev/news/4673.feat b/docs/dev/news/4673.feat
new file mode 100644
index 00000000000..2867fa8ef31
--- /dev/null
+++ b/docs/dev/news/4673.feat
@@ -0,0 +1 @@
+The new `--only-label` option to `merge-coverage-reports` includes only one category of highlighting in the output. For example, merging coverage reports from test generation and verification using the option `--only-label NotCovered` will highlight only the regions not covered by either testing or verification.
