diff --git a/Source/DafnyTestGeneration/CoverageReport/CoverageLabel.cs b/Source/DafnyCore/CoverageReport/CoverageLabel.cs
similarity index 84%
rename from Source/DafnyTestGeneration/CoverageReport/CoverageLabel.cs
rename to Source/DafnyCore/CoverageReport/CoverageLabel.cs
index 5e820a6c70f..641c1a9d95d 100644
--- a/Source/DafnyTestGeneration/CoverageReport/CoverageLabel.cs
+++ b/Source/DafnyCore/CoverageReport/CoverageLabel.cs
@@ -3,9 +3,10 @@
 namespace Microsoft.Dafny;
 
 public enum CoverageLabel {
+  None,
   FullyCovered,
   NotCovered,
-  PartiallyCovered
+  PartiallyCovered,
 }
 
 public static class CoverageLabelExtension {
@@ -14,6 +15,12 @@ public static class CoverageLabelExtension {
   /// Combine coverage labels. E.g. FullyCovered + NotCovered = PartiallyCovered
   /// </summary>
   public static CoverageLabel Combine(CoverageLabel one, CoverageLabel two) {
+    if (one == CoverageLabel.None) {
+      return two;
+    }
+    if (two == CoverageLabel.None) {
+      return one;
+    }
     if (one == CoverageLabel.PartiallyCovered || two == CoverageLabel.PartiallyCovered || one != two) {
       return CoverageLabel.PartiallyCovered;
     }
diff --git a/Source/DafnyTestGeneration/CoverageReport/CoverageReport.cs b/Source/DafnyCore/CoverageReport/CoverageReport.cs
similarity index 67%
rename from Source/DafnyTestGeneration/CoverageReport/CoverageReport.cs
rename to Source/DafnyCore/CoverageReport/CoverageReport.cs
index 12dfa5be2f2..22439517b8e 100644
--- a/Source/DafnyTestGeneration/CoverageReport/CoverageReport.cs
+++ b/Source/DafnyCore/CoverageReport/CoverageReport.cs
@@ -11,7 +11,6 @@ public class CoverageReport {
 
   private static int nextUniqueId = 0;
 
-  // INVARIANT: CoverageSpans are sorted within each list by the position of the StartToken
   private readonly Dictionary<string, List<CoverageSpan>> labelsByFile;
   public readonly string Name; // the name to assign to this coverage report
   public readonly string Units; // the units of coverage (plural). This will be written in the coverage report table.
@@ -39,37 +38,12 @@ public CoverageReport(string name, string units, string suffix, Program program)
 
   /// <summary>
   /// Assign a coverage label to the code indicated by the <param name="span"></param> range token.
-  /// If the span intersects with existing coverage information, it will be merged according to
-  /// CoverageLabelExtension.Combine. 
   /// </summary>
   public void LabelCode(RangeToken span, CoverageLabel label) {
     Contract.Assert(labelsByFile.ContainsKey(span.ActualFilename));
-    if (span.StartToken.CompareTo(span.EndToken) == 0) {
-      return;
-    }
     var labeledFile = labelsByFile[span.ActualFilename];
     var coverageSpan = new CoverageSpan(span, label);
-    int index = labeledFile.BinarySearch(0, labeledFile.Count, coverageSpan, null);
-    if (index < 0) {
-      labeledFile.Insert(~index, coverageSpan);
-      return;
-    }
-    var overlappingSpan = labeledFile[index];
-    labeledFile.RemoveAt(index);
-    var combinedLabel = CoverageLabelExtension.Combine(label, overlappingSpan.Label);
-    switch (overlappingSpan.Span.EndToken.CompareTo(span.EndToken)) {
-      case 0:
-        labeledFile.Insert(index, new CoverageSpan(span, combinedLabel));
-        break;
-      case > 0:
-        labeledFile.Insert(index, new CoverageSpan(span, combinedLabel));
-        labeledFile.Insert(index + 1, new CoverageSpan(new RangeToken(span.EndToken, overlappingSpan.Span.EndToken), overlappingSpan.Label));
-        break;
-      default:
-        labeledFile.Insert(index, new CoverageSpan(overlappingSpan.Span, combinedLabel));
-        LabelCode(new RangeToken(overlappingSpan.Span.EndToken, span.EndToken), label);
-        break;
-    }
+    labeledFile.Add(coverageSpan);
   }
 
   public IEnumerable<CoverageSpan> CoverageSpansForFile(string fileName) {
@@ -92,8 +66,12 @@ private void RegisterFiles(Node astNode) {
     if (astNode.StartToken.ActualFilename != null) {
       labelsByFile[astNode.StartToken.ActualFilename] = new();
     }
+
     foreach (var declaration in astNode.Children.OfType<LiteralModuleDecl>()) {
       RegisterFiles(declaration);
     }
+    foreach (var declaration in astNode.Children.OfType<Declaration>()) {
+      RegisterFiles(declaration);
+    }
   }
 }
\ No newline at end of file
diff --git a/Source/DafnyTestGeneration/CoverageReport/CoverageSpan.cs b/Source/DafnyCore/CoverageReport/CoverageSpan.cs
similarity index 89%
rename from Source/DafnyTestGeneration/CoverageReport/CoverageSpan.cs
rename to Source/DafnyCore/CoverageReport/CoverageSpan.cs
index 9f07fe48be2..a3ae066d427 100644
--- a/Source/DafnyTestGeneration/CoverageReport/CoverageSpan.cs
+++ b/Source/DafnyCore/CoverageReport/CoverageSpan.cs
@@ -13,7 +13,6 @@ public CoverageSpan(RangeToken span, CoverageLabel label) {
     Contract.Assert(span.Uri != null);
     Contract.Assert(span.StartToken != null);
     Contract.Assert(span.EndToken != null);
-    Contract.Assert(span.StartToken.CompareTo(span.EndToken) != 0);
     Span = span;
     Label = label;
   }
diff --git a/Source/DafnyCore/Options/CommonOptionBag.cs b/Source/DafnyCore/Options/CommonOptionBag.cs
index 4320351cf11..b4d5d26a99c 100644
--- a/Source/DafnyCore/Options/CommonOptionBag.cs
+++ b/Source/DafnyCore/Options/CommonOptionBag.cs
@@ -209,6 +209,10 @@ May slow down verification slightly.
 May produce spurious warnings.") {
     IsHidden = true
   };
+  public static readonly Option<string> VerificationCoverageReport = new("--coverage-report",
+    "Emit verification coverage report  to a given directory, in the same format as a test coverage report.") {
+    ArgumentHelpName = "directory"
+  };
 
   public static readonly Option<bool> IncludeRuntimeOption = new("--include-runtime",
     "Include the Dafny runtime as source in the target language.");
@@ -470,6 +474,7 @@ void ParsePrintMode(Option<PrintModes> option, Boogie.CommandLineParseState ps,
       IncludeRuntimeOption,
       WarnContradictoryAssumptions,
       WarnRedundantAssumptions,
+      VerificationCoverageReport,
       DefaultFunctionOpacity
     );
   }
diff --git a/Source/DafnyCore/Options/DafnyCommands.cs b/Source/DafnyCore/Options/DafnyCommands.cs
index c812c991dd1..bf8b49b9326 100644
--- a/Source/DafnyCore/Options/DafnyCommands.cs
+++ b/Source/DafnyCore/Options/DafnyCommands.cs
@@ -41,7 +41,8 @@ static DafnyCommands() {
     BoogieOptionBag.VerificationErrorLimit,
     CommonOptionBag.DefaultFunctionOpacity,
     CommonOptionBag.WarnContradictoryAssumptions,
-    CommonOptionBag.WarnRedundantAssumptions
+    CommonOptionBag.WarnRedundantAssumptions,
+    CommonOptionBag.VerificationCoverageReport
   }.ToList();
 
   public static IReadOnlyList<Option> TranslationOptions = new Option[] {
diff --git a/Source/DafnyCore/Verifier/ProofDependencyManager.cs b/Source/DafnyCore/Verifier/ProofDependencyManager.cs
index 6b9c82652f0..0c8a0fc90b6 100644
--- a/Source/DafnyCore/Verifier/ProofDependencyManager.cs
+++ b/Source/DafnyCore/Verifier/ProofDependencyManager.cs
@@ -7,6 +7,7 @@
 //-----------------------------------------------------------------------------
 using System;
 using System.Collections.Generic;
+using System.Linq;
 using Dafny;
 using Bpl = Microsoft.Boogie;
 using BplParser = Microsoft.Boogie.Parser;
@@ -42,6 +43,10 @@ public IEnumerable<ProofDependency> GetPotentialDependenciesForDefinition(string
       return idsByMemberName[defName];
     }
 
+    public IEnumerable<ProofDependency> GetAllPotentialDependencies() {
+      return idsByMemberName.Values.SelectMany(deps => deps);
+    }
+
     // The "id" attribute on a Boogie AST node is used by Boogie to label
     // that AST node in the SMT-Lib formula when constructing a verification
     // condition.
diff --git a/Source/DafnyDriver/Commands/VerifyCommand.cs b/Source/DafnyDriver/Commands/VerifyCommand.cs
index 4c2eb1ea865..f9b0eb64c25 100644
--- a/Source/DafnyDriver/Commands/VerifyCommand.cs
+++ b/Source/DafnyDriver/Commands/VerifyCommand.cs
@@ -15,6 +15,9 @@ public static Command Create() {
       result.AddOption(option);
     }
     DafnyCli.SetHandlerUsingDafnyOptionsContinuation(result, (options, _) => {
+      if (options.Get(CommonOptionBag.VerificationCoverageReport) != null) {
+        options.TrackVerificationCoverage = true;
+      }
       options.Compile = false;
       return CompilerDriver.RunCompiler(options);
     });
diff --git a/Source/DafnyDriver/CompilerDriver.cs b/Source/DafnyDriver/CompilerDriver.cs
index c576fd30a4a..e811d139692 100644
--- a/Source/DafnyDriver/CompilerDriver.cs
+++ b/Source/DafnyDriver/CompilerDriver.cs
@@ -155,6 +155,13 @@ private async Task<ExitValue> ProcessFilesAsync(IReadOnlyList<DafnyFile/*!*/>/*!
 
         if (options.TrackVerificationCoverage) {
           ProofDependencyWarnings.WarnAboutSuspiciousDependencies(options, dafnyProgram.Reporter, depManager);
+          var coverageReportDir = options.Get(CommonOptionBag.VerificationCoverageReport);
+          if (coverageReportDir != null) {
+            new CoverageReporter(options).SerializeVerificationCoverageReport(
+              depManager, dafnyProgram,
+              boogiePrograms.SelectMany(tp => tp.Item2.AllCoveredElements),
+              coverageReportDir);
+          }
         }
 
         bool compiled;
diff --git a/Source/DafnyDriver/CoverageReporter.cs b/Source/DafnyDriver/CoverageReporter.cs
index df8fdd8ae8e..2f7229ae437 100644
--- a/Source/DafnyDriver/CoverageReporter.cs
+++ b/Source/DafnyDriver/CoverageReporter.cs
@@ -4,6 +4,9 @@
 using System.Linq;
 using System.Text;
 using System.Text.RegularExpressions;
+using DafnyCore.Verifier;
+using Microsoft.Boogie;
+using Microsoft.Extensions.Primitives;
 
 namespace Microsoft.Dafny; 
 
@@ -22,7 +25,7 @@ public class CoverageReporter {
   private static readonly Regex TableFooterRegex = new(@"\{\{TABLE_FOOTER\}\}");
   private static readonly Regex TableBodyRegex = new(@"\{\{TABLE_BODY\}\}");
   private static readonly Regex IndexFileNameRegex = new(@"index(.*)\.html");
-  private static readonly Regex SpanRegexInverse = new("class=\"([a-z]+)\" id=\"line([0-9]+)col([0-9]+)-line([0-9]+)col([0-9]+)\"");
+  private static readonly Regex PosRegexInverse = new("class=\"([a-z]+)\" id=\"pos([0-9]+)\">");
   private const string CoverageReportTemplatePath = "coverage_report_template.html";
   private const string CoverageReportIndexTemplatePath = "coverage_report_index_template.html";
   private const string CoverageReportSupportingFilesPath = ".resources";
@@ -39,6 +42,28 @@ public CoverageReporter(DafnyOptions options) {
     this.options = options;
   }
 
+
+  public void SerializeVerificationCoverageReport(ProofDependencyManager depManager, Program dafnyProgram, IEnumerable<TrackedNodeComponent> usedComponents, string coverageReportDir) {
+    var usedDependencies =
+      usedComponents.Select(depManager.GetFullIdDependency).ToHashSet();
+    var allDependencies =
+      depManager
+        .GetAllPotentialDependencies()
+        .OrderBy(dep => dep.Range.StartToken);
+    var coverageReport = new CoverageReport("Verification coverage", "Lines", "_verification", dafnyProgram);
+    foreach (var dep in allDependencies) {
+      if (dep is FunctionDefinitionDependency) {
+        continue;
+      }
+      coverageReport.LabelCode(dep.Range,
+        usedDependencies.Contains(dep)
+          ? CoverageLabel.FullyCovered
+          : CoverageLabel.NotCovered);
+    }
+
+    SerializeCoverageReports(coverageReport, coverageReportDir);
+  }
+
   public void Merge(List<string> coverageReportsToMerge, string coverageReportOutDir) {
     // assume only one report in directory for now
     List<CoverageReport> reports = new();
@@ -80,16 +105,17 @@ private static CoverageReport ParseCoverageReport(string reportDir, string name,
         continue;
       }
       var uri = new Uri(uriMatch.Groups[1].Value);
+      var lastEndToken = new Token(1, 1);
       report.RegisterFile(uri);
-      foreach (var span in SpanRegexInverse.Matches(source).Where(match => match.Success)) {
-        if (int.TryParse(span.Groups[2].Value, out var startLine) &&
-            int.TryParse(span.Groups[3].Value, out var startCol) &&
-            int.TryParse(span.Groups[4].Value, out var endLine) &&
-            int.TryParse(span.Groups[5].Value, out var endCol)) {
-          var startToken = new Token(startLine, startCol);
-          startToken.Uri = uri;
-          var endToken = new Token(endLine, endCol);
+      foreach (var span in PosRegexInverse.Matches(source).Where(match => match.Success)) {
+        if (int.TryParse(span.Groups[2].Value, out var pos)) {
+          var startToken = new Token(1, 1);
           startToken.Uri = uri;
+          startToken.pos = pos;
+          lastEndToken.pos = pos;
+          var endToken = new Token(1, 1);
+          endToken.Uri = uri;
+          lastEndToken = endToken;
           var rangeToken = new RangeToken(startToken, endToken);
           rangeToken.Uri = uri;
           report.LabelCode(rangeToken, FromHtmlClass(span.Groups[1].Value));
@@ -125,7 +151,7 @@ private void SerializeCoverageReports(List<CoverageReport> reports, string repor
         .TakeWhile((c, i) => allFiles.All(s => s[i] == c)).ToArray()).Length;
     Dictionary<string, string> sourceFileToCoverageReport = new Dictionary<string, string>();
     foreach (var fileName in allFiles) {
-      var directoryForFile = Path.Combine(sessionDirectory, Path.GetDirectoryName(fileName)?[prefixLength..] ?? "");
+      var directoryForFile = Path.Combine(sessionDirectory, Path.GetDirectoryName(fileName)?[prefixLength..].TrimStart('/') ?? "");
       var pathToRoot = Path.GetRelativePath(directoryForFile, sessionDirectory);
       Directory.CreateDirectory(directoryForFile);
       for (int i = 0; i < reports.Count; i++) {
@@ -239,16 +265,31 @@ private void CopyStyleFiles(string baseDirectory) {
   private string HtmlReportForFile(CoverageReport report, string pathToSourceFile, string baseDirectory, string linksToOtherReports) {
     var source = new StreamReader(pathToSourceFile).ReadToEnd();
     var lines = source.Split("\n");
-    IToken lastToken = new Token(0, 0);
+    var characterLabels = new CoverageLabel[source.Length];
+    Array.Fill(characterLabels, CoverageLabel.None);
+    IToken lastToken = new Token(1, 1);
     var labeledCodeBuilder = new StringBuilder(source.Length);
     foreach (var span in report.CoverageSpansForFile(pathToSourceFile)) {
-      AppendCodeBetweenTokens(labeledCodeBuilder, lines, lastToken, span.Span.StartToken);
-      labeledCodeBuilder.Append(OpenHtmlTag(span));
-      AppendCodeBetweenTokens(labeledCodeBuilder, lines, span.Span.StartToken, span.Span.EndToken);
-      labeledCodeBuilder.Append(CloseHtmlTag(span));
-      lastToken = span.Span.EndToken;
+      for (var pos = span.Span.StartToken.pos; pos <= span.Span.EndToken.pos; pos++) {
+        characterLabels[pos] = CoverageLabelExtension.Combine(characterLabels[pos], span.Label);
+      }
     }
-    AppendCodeBetweenTokens(labeledCodeBuilder, lines, lastToken, null);
+
+    CoverageLabel lastLabel = CoverageLabel.None;
+    labeledCodeBuilder.Append(OpenHtmlTag(0, CoverageLabel.None));
+    for (var pos = 0; pos < source.Length; pos++) {
+      var thisLabel = characterLabels[pos];
+      if (thisLabel != lastLabel) {
+        labeledCodeBuilder.Append(CloseHtmlTag());
+        labeledCodeBuilder.Append(OpenHtmlTag(pos, thisLabel));
+      }
+
+      labeledCodeBuilder.Append(source[pos]);
+
+      lastLabel = thisLabel;
+    }
+    labeledCodeBuilder.Append(CloseHtmlTag());
+
     var assembly = System.Reflection.Assembly.GetCallingAssembly();
     var templateStream = assembly.GetManifestResourceStream(CoverageReportTemplatePath);
     var labeledCode = labeledCodeBuilder.ToString();
@@ -266,21 +307,6 @@ private string HtmlReportForFile(CoverageReport report, string pathToSourceFile,
     return LabeledCodeRegex.Replace(templateText, labeledCode);
   }
 
-  /// <summary>
-  /// Append code from <param name="lines"></param> that lies between <param name="start"></param> and
-  /// <param name="end"></param> tokens to the <param name="stringBuilder"></param>
-  /// </summary>
-  private static void AppendCodeBetweenTokens(StringBuilder stringBuilder, string[] lines, IToken start, IToken end) {
-    var currToken = new Token(start.line, start.col);
-    while (currToken.line < lines.Length && (end == null || currToken.line < end.line)) {
-      stringBuilder.Append(lines[currToken.line][currToken.col..] + "\n");
-      currToken.line += 1;
-    }
-    if (end != null && currToken.line < lines.Length) {
-      stringBuilder.Append(lines[currToken.line][currToken.col..end.col]);
-    }
-  }
-
   /// <summary>
   /// Return HTML class used to highlight lines in different colors depending on the coverage.
   /// Look at assets/.resources/coverage.css for the styles corresponding to these classes
@@ -290,6 +316,7 @@ private static string ToHtmlClass(CoverageLabel label) {
       CoverageLabel.FullyCovered => "fc",
       CoverageLabel.NotCovered => "nc",
       CoverageLabel.PartiallyCovered => "pc",
+      CoverageLabel.None => "none",
       _ => ""
     };
   }
@@ -304,13 +331,13 @@ private static CoverageLabel FromHtmlClass(string htmlClass) {
     return CoverageLabel.NotCovered; // this is a fallback in case the HTML has invalid classes
   }
 
-  private string OpenHtmlTag(CoverageSpan span) {
-    var id = $"id=\"line{span.Span.StartToken.line}col{span.Span.StartToken.col}-line{span.Span.EndToken.line}col{span.Span.EndToken.col}\"";
-    var classLabel = ToHtmlClass(span.Label);
+  private string OpenHtmlTag(int pos, CoverageLabel label) {
+    var id = $"id=\"pos{pos}\"";
+    var classLabel = ToHtmlClass(label);
     return $"<span class=\"{classLabel}\" {id}>";
   }
 
-  private string CloseHtmlTag(CoverageSpan span) {
+  private string CloseHtmlTag() {
     return "</span>";
   }
 }
\ No newline at end of file
diff --git a/Source/DafnyTestGeneration/Main.cs b/Source/DafnyTestGeneration/Main.cs
index 997832f73e3..c2befe4861a 100644
--- a/Source/DafnyTestGeneration/Main.cs
+++ b/Source/DafnyTestGeneration/Main.cs
@@ -115,6 +115,8 @@ private static void PopulateCoverageReport(CoverageReport coverageReport, Progra
       if (coverageReport == null) {
         return;
       }
+
+      var lineNumToPosCache = new Dictionary<Uri, int[]>();
       var lineRegex = new Regex("^(.*)\\(([0-9]+),[0-9]+\\)");
       HashSet<string> coveredStates = new(); // set of program states that are expected to be covered by tests
       foreach (var modification in cache.Values) {
@@ -133,7 +135,6 @@ private static void PopulateCoverageReport(CoverageReport coverageReport, Progra
           if (!int.TryParse(match.Groups[2].Value, out var lineNumber) || lineNumber == 0) {
             continue;
           }
-          lineNumber -= 1; // to zero-based
           Uri uri;
           try {
             uri = new Uri(
@@ -143,8 +144,12 @@ private static void PopulateCoverageReport(CoverageReport coverageReport, Progra
           } catch (ArgumentException) {
             continue;
           }
-          var rangeToken = new RangeToken(new Token(lineNumber, 0), new Token(lineNumber + 1, 0));
+          var linePos = Utils.GetPosFromLine(uri, lineNumber, lineNumToPosCache);
+          var lineLength = Utils.GetPosFromLine(uri, lineNumber + 1, lineNumToPosCache) - linePos - 1;
+          var rangeToken = new RangeToken(new Token(lineNumber, 1), new Token(lineNumber, lineLength));
           rangeToken.Uri = uri;
+          rangeToken.StartToken.pos = linePos;
+          rangeToken.EndToken.pos = linePos + lineLength;
           coverageReport.LabelCode(rangeToken,
             coveredStates.Contains(state)
               ? CoverageLabel.FullyCovered
diff --git a/Source/DafnyTestGeneration/Utils.cs b/Source/DafnyTestGeneration/Utils.cs
index f16775b5aee..b8d5d40e7e5 100644
--- a/Source/DafnyTestGeneration/Utils.cs
+++ b/Source/DafnyTestGeneration/Utils.cs
@@ -140,6 +140,28 @@ public static string GetBlockId(Block block, DafnyOptions options) {
       return state == null ? null : Regex.Replace(state, @"\s+", "") + uniqueId;
     }
 
+    /// <summary>
+    /// Given a file URI and a one-based line number, return the position of the character at the start of the line.
+    /// Use a cache to prevent reading the same file twice.
+    /// </summary>
+    public static int GetPosFromLine(Uri fileUri, int lineNum, Dictionary<Uri, int[]> cache) {
+      if (!cache.ContainsKey(fileUri)) {
+        var source = new StreamReader(fileUri.LocalPath).ReadToEnd();
+        var lines = source.Split("\n");
+        var pos = 0;
+        var line = 0;
+        var linePositions = new int[lines.Length + 1];
+        while (pos < source.Length) {
+          linePositions[line] = pos;
+          pos += lines[line].Length + 1;
+          line++;
+        }
+        linePositions[^1] = pos;
+        cache[fileUri] = linePositions;
+      }
+      return cache[fileUri][lineNum - 1]; // subtract one because lineNum is one-based
+    }
+
     public static IList<object> GetAttributeValue(Implementation implementation, string attribute) {
       var attributes = implementation.Attributes;
       while (attributes != null) {
diff --git a/Test/logger/ProofDependencyLogging.dfy_verification.html.expect b/Test/logger/ProofDependencyLogging.dfy_verification.html.expect
new file mode 100644
index 00000000000..3542509b0a5
--- /dev/null
+++ b/Test/logger/ProofDependencyLogging.dfy_verification.html.expect
@@ -0,0 +1,481 @@
+<?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, Verification coverage</title>
+</head>
+<body onload="window['PR_TAB_WIDTH']=4">
+<div class="menu" id="menu">
+    <a href="./index_verification.html">Index</a>
+    
+</div>
+<h1>ProofDependencyLogging.dfy, Verification coverage</h1>
+
+<pre class="source lang-java linenums">
+<span class="none" id="pos0">// RUN: %baredafny verify --log-format:text --boogie -trackVerificationCoverage "%s" > "%t"
+// RUN: %OutputCheck --file-to-check "%t" "%s"
+// CHECK: Results for RedundantAssumeMethod \(correctness\)
+// CHECK:     Proof dependencies:
+// CHECK:       ProofDependencyLogging.dfy\(177,12\)-\(177,16\): assume statement
+// CHECK:       ProofDependencyLogging.dfy\(178,12\)-\(178,12\): assertion always holds
+//
+// CHECK: Results for 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 AssumeFalseMethod \(correctness\)
+// CHECK:     Proof dependencies:
+// CHECK:       ProofDependencyLogging.dfy\(192,12\)-\(192,12\): assume statement
+//
+// CHECK: Results for 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 FalseAntecedentRequiresClauseMethod \(correctness\)
+// CHECK:     Proof dependencies:
+// CHECK:       ProofDependencyLogging.dfy\(357,3\)-\(357,15\): assignment \(or return\)
+//
+// CHECK: Results for FalseAntecedentAssertStatementMethod \(correctness\)
+// CHECK:     Proof dependencies:
+// CHECK:       ProofDependencyLogging.dfy\(362,9\)-\(362,15\): assignment \(or return\)
+// CHECK:       ProofDependencyLogging.dfy\(363,20\)-\(363,20\): assertion always holds
+//
+// CHECK: Results for 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 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 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 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 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 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\)
+
+
+
+
+method RedundantAssumeMethod(n: int)
+{
+    // either one or the other assumption shouldn't be covered
+    assume </span><span class="nc" id="pos11147">n > 4</span><span class="none" id="pos11152">;
+    assume </span><span class="fc" id="pos11165">n > 3</span><span class="none" id="pos11170">;
+    assert n </span><span class="fc" id="pos11185">></span><span class="none" id="pos11186"> 1;
+}
+
+method ContradictoryAssumeMethod(n: int)
+{
+    assume </span><span class="fc" id="pos11247">n > 0</span><span class="none" id="pos11252">;
+    assume </span><span class="fc" id="pos11265">n < 0</span><span class="none" id="pos11270">;
+    assume </span><span class="nc" id="pos11283">n == 5</span><span class="none" id="pos11289">; // shouldn't be covered
+    assert n </span><span class="nc" id="pos11328"><</span><span class="none" id="pos11329"> 10; // shouldn't be covered
+}
+
+method AssumeFalseMethod(n: int)
+{
+    assume </span><span class="nc" id="pos11407">n == 1</span><span class="none" id="pos11413">5; // shouldn't be covered
+    assume </span><span class="fc" id="pos11451">f</span><span class="none" id="pos11452">alse;
+    assert n </span><span class="nc" id="pos11471"><</span><span class="none" id="pos11472"> 10; // shouldn't be covered
+}
+
+// Obvious contradiction in requires clauses.
+function ObviouslyContradictoryRequiresFunc(x: nat): (r: nat)
+  requires </span><span class="fc" id="pos11623">x > 1</span><span class="none" id="pos11628">0
+  requires </span><span class="fc" id="pos11641">x < 1</span><span class="none" id="pos11646">0
+  ensures </span><span class="nc" id="pos11658">r < x</span><span class="none" id="pos11663"> // only provable vacuously 
+{
+  assert x </span><span class="nc" id="pos11705">=</span><span class="none" id="pos11706">= 10; // contradicts both requires clauses
+  </span><span class="nc" id="pos11751">x - 1</span><span class="none" id="pos11756"> // not necessarily a valid nat
+}
+
+method ObviouslyContradictoryRequiresMethod(x: nat) returns (r: nat)
+  requires </span><span class="pc" id="pos11871">x > 1</span><span class="none" id="pos11876">0
+  requires </span><span class="pc" id="pos11889">x < 1</span><span class="none" id="pos11894">0
+  ensures </span><span class="nc" id="pos11906">r < x</span><span class="none" id="pos11911"> // only provable vacuously
+{
+  assert x </span><span class="nc" id="pos11952">=</span><span class="none" id="pos11953">= 10; // contradicts both requires clauses
+  </span><span class="nc" id="pos11998">return x - 1;</span><span class="none" id="pos12011"> // not necessarily a valid nat
+</span><span class="nc" id="pos12043">}</span><span class="none" id="pos12044">
+
+// Obvious redundancy in requires clauses.
+function ObviouslyRedundantRequiresFunc(x: nat): (r: nat)
+  requires </span><span class="fc" id="pos12158">x < 1</span><span class="none" id="pos12163">0
+  requires </span><span class="nc" id="pos12176">x < 1</span><span class="none" id="pos12181">00 // implied by previous requires clause
+  ensures </span><span class="pc" id="pos12233">r < 1</span><span class="none" id="pos12238">1 // should cause body and first requires clause to be covered
+{
+  </span><span class="fc" id="pos12305">x + 1</span><span class="none" id="pos12310">
+}
+
+method ObviouslyRedundantRequiresMethod(x: nat) returns (r: nat)
+  requires </span><span class="pc" id="pos12390">x < 1</span><span class="none" id="pos12395">0
+  requires </span><span class="nc" id="pos12408">x < 1</span><span class="none" id="pos12413">00 // implied by previous requires clause
+  ensures </span><span class="pc" id="pos12465">r < 1</span><span class="none" id="pos12470">1 // should cause body and first requires clause to be covered
+{
+  </span><span class="fc" id="pos12537">return x + 1;</span><span class="none" id="pos12550">
+</span><span class="nc" id="pos12551">}</span><span class="none" id="pos12552">
+
+// Obviously unnecessary requires clauses.
+function ObviouslyUnnecessaryRequiresFunc(x: nat): (r: nat)
+  requires </span><span class="nc" id="pos12668">x < 1</span><span class="none" id="pos12673">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="pos12797">x </span><span class="pc" id="pos12799">+</span><span class="nc" id="pos12800"> 2</span><span class="none" id="pos12802"> else </span><span class="nc" id="pos12808">x </span><span class="pc" id="pos12810">+</span><span class="nc" id="pos12811"> 1</span><span class="none" id="pos12813">
+}
+
+method ObviouslyUnnecessaryRequiresMethod(x: nat) returns (r: nat)
+  requires </span><span class="nc" id="pos12895">x < 1</span><span class="none" id="pos12900">0 // not required for the proof
+{
+  // cause at least a little proof work to be necessary, for nat bounds
+  if (x > 5) { </span><span class="pc" id="pos13021">r</span><span class="nc" id="pos13022">eturn x </span><span class="pc" id="pos13030">+</span><span class="nc" id="pos13031"> 2;</span><span class="none" id="pos13034"> } else { </span><span class="pc" id="pos13044">r</span><span class="nc" id="pos13045">eturn x </span><span class="pc" id="pos13053">+</span><span class="nc" id="pos13054"> 1;</span><span class="none" id="pos13057"> }
+</span><span class="nc" id="pos13060">}</span><span class="none" id="pos13061">
+
+// Code obviously not constrained by ensures clause.
+function ObviouslyUnconstrainedCodeFunc(x: int): (r: (int, int))
+  requires </span><span class="fc" id="pos13192">x > 1</span><span class="none" id="pos13197">0
+  ensures </span><span class="pc" id="pos13209">r.0 > 1</span><span class="none" id="pos13216">0
+{
+  var </span><span class="fc" id="pos13226">a</span><span class="none" id="pos13227"> := </span><span class="fc" id="pos13231">x + 1</span><span class="none" id="pos13236">; // constrained by ensures clause
+  var </span><span class="nc" id="pos13277">b</span><span class="none" id="pos13278"> := </span><span class="nc" id="pos13282">x - 1</span><span class="none" id="pos13287">; // not constrained by ensures clause 
+  </span><span class="fc" id="pos13329">(</span><span class="none" id="pos13330">a,
+   b)
+}
+
+method ObviouslyUnconstrainedCodeMethod(x: int) returns (r: (int, int))
+  requires </span><span class="pc" id="pos13425">x > 1</span><span class="none" id="pos13430">0
+  ensures </span><span class="pc" id="pos13442">r.0 > 1</span><span class="none" id="pos13449">0
+{
+  var a </span><span class="fc" id="pos13461">:= x + 1;</span><span class="none" id="pos13470"> // constrained by ensures clause
+  var b </span><span class="nc" id="pos13512">:= x - 1;</span><span class="none" id="pos13521"> // not constrained by ensures clause
+  </span><span class="fc" id="pos13561">return
+    (a,
+     b);</span><span class="none" id="pos13584">
+</span><span class="nc" id="pos13585">}</span><span class="none" id="pos13586">
+
+// Partial redundancy in requires clauses.
+function PartiallyRedundantRequiresFunc(x: nat): (r: nat)
+  requires </span><span class="nc" id="pos13700">x < 1</span><span class="none" id="pos13705">00 && </span><span class="fc" id="pos13711">x < 1</span><span class="none" id="pos13716">0 // LHS implied by RHS
+  ensures </span><span class="pc" id="pos13750">r < 1</span><span class="none" id="pos13755">1 // should cause body and RHS clause to be covered
+{
+  </span><span class="fc" id="pos13811">x + 1</span><span class="none" id="pos13816">
+}
+
+// Partly unnecessary requires clause.
+function PartiallyUnnecessaryRequiresFunc(x: int): (r: nat)
+  requires </span><span class="nc" id="pos13930">x < 1</span><span class="none" id="pos13935">0 && </span><span class="fc" id="pos13940">x > 0</span><span class="none" id="pos13945"> // 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="pos14077">x </span><span class="pc" id="pos14079">-</span><span class="nc" id="pos14080"> 1</span><span class="none" id="pos14082"> else </span><span class="nc" id="pos14088">x </span><span class="pc" id="pos14090">+</span><span class="nc" id="pos14091"> 1</span><span class="none" id="pos14093">
+}
+
+
+// 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 MultiPartRedundantRequiresFunc(x: int): (r: int)
+  requires </span><span class="nc" id="pos14313">x > 1</span><span class="none" id="pos14318">0
+  requires </span><span class="nc" id="pos14331">x < 1</span><span class="none" id="pos14336">2
+  requires </span><span class="fc" id="pos14349">x == 1</span><span class="none" id="pos14355">1 // implied by the previous two, but neither individually
+  ensures </span><span class="pc" id="pos14424">r == 1</span><span class="none" id="pos14430">1
+{
+  </span><span class="fc" id="pos14436">x</span><span class="none" id="pos14437">
+}
+
+method MultiPartRedundantRequiresMethod(x: int) returns (r: int)
+  requires </span><span class="nc" id="pos14517">x > 1</span><span class="none" id="pos14522">0
+  requires </span><span class="nc" id="pos14535">x < 1</span><span class="none" id="pos14540">2
+  requires </span><span class="pc" id="pos14553">x == 1</span><span class="none" id="pos14559">1 // implied by the previous two, but neither individually
+  ensures </span><span class="pc" id="pos14628">r == 1</span><span class="none" id="pos14634">1
+{
+  </span><span class="pc" id="pos14640">r</span><span class="nc" id="pos14641">eturn x;</span><span class="none" id="pos14649">
+</span><span class="nc" id="pos14650">}</span><span class="none" id="pos14651">
+
+// Contradiction between three different requires clauses, with at least one of
+// the three being partly in a separately-defined function (function and
+// method).
+function MultiPartContradictoryRequiresFunc(x: int, y: int): (r: int)
+  requires </span><span class="fc" id="pos14899">x > 1</span><span class="none" id="pos14904">0
+  requires </span><span class="fc" id="pos14917">x < 1</span><span class="none" id="pos14922">2
+  requires </span><span class="nc" id="pos14935">y != 1</span><span class="none" id="pos14941">1 // contradicts the previous two
+  ensures </span><span class="pc" id="pos14985">r == 1</span><span class="none" id="pos14991">1 // provable from first two preconditions, but shouldn't be covered
+{
+  </span><span class="fc" id="pos15064">x</span><span class="none" id="pos15065">
+}
+
+method MultiPartContradictoryRequiresMethod(x: int, y: int) returns (r: int)
+  requires </span><span class="pc" id="pos15157">x > 1</span><span class="none" id="pos15162">0
+  requires </span><span class="pc" id="pos15175">x < 1</span><span class="none" id="pos15180">2
+  requires </span><span class="nc" id="pos15193">y != 1</span><span class="none" id="pos15199">1 // contradicts the previous two
+  ensures </span><span class="pc" id="pos15243">r == 1</span><span class="none" id="pos15249">1 // provable from first two preconditions, but shouldn't be covered
+{
+  </span><span class="pc" id="pos15322">r</span><span class="nc" id="pos15323">eturn x;</span><span class="none" id="pos15331">
+</span><span class="nc" id="pos15332">}</span><span class="none" id="pos15333">
+
+function ContradictoryEnsuresClauseFunc(x: int): (r: int)
+  requires </span><span class="nc" id="pos15404">x > 1</span><span class="none" id="pos15409">
+  ensures  </span><span class="nc" id="pos15421">r > x && r < 0</span><span class="none" id="pos15435">
+
+method ContradictoryEnsuresClauseMethod(x: int) returns (r: int)
+  requires </span><span class="nc" id="pos15513">x > 1</span><span class="none" id="pos15518">
+  ensures  </span><span class="nc" id="pos15530">r > x && r < 0</span><span class="none" id="pos15544">
+
+// Call function that has contradictory ensures clauses.
+function CallContradictoryFunctionFunc(x: int): (r: int)
+  requires </span><span class="fc" id="pos15671">x > 1</span><span class="none" id="pos15676">
+  ensures </span><span class="pc" id="pos15687">r < 0</span><span class="none" id="pos15692">
+{
+  // TODO: Dafny doesn't generate sufficient Boogie code to make the contradiction detectable
+  </span><span class="fc" id="pos15791">ContradictoryEnsuresClauseFunc(x) - 1</span><span class="none" id="pos15828">
+}
+
+method CallContradictoryMethodMethod(x: int) returns (r: int)
+  requires </span><span class="pc" id="pos15905">x > 1</span><span class="none" id="pos15910">
+  ensures </span><span class="nc" id="pos15921">r < 0</span><span class="none" id="pos15926">
+{
+  var y </span><span class="nc" id="pos15937">:= ContradictoryEnsuresClauseMethod(x);</span><span class="none" id="pos15976">
+  </span><span class="nc" id="pos15979">return y - 1;</span><span class="none" id="pos15992">
+</span><span class="nc" id="pos15993">}</span><span class="none" id="pos15994">
+
+// False antecedent requires clause
+method FalseAntecedentRequiresClauseMethod(x: int) returns (r: int)
+  requires </span><span class="nc" id="pos16111">x*x < 0 ==> x == x + 1</span><span class="none" id="pos16133">
+  ensures </span><span class="pc" id="pos16144">r > x</span><span class="none" id="pos16149">
+{
+  </span><span class="fc" id="pos16154">return x + 1;</span><span class="none" id="pos16167">
+</span><span class="nc" id="pos16168">}</span><span class="none" id="pos16169">
+
+// False antecedent assert statement.
+method FalseAntecedentAssertStatementMethod(x: int) {
+  var y </span><span class="fc" id="pos16271">:= x*x;</span><span class="none" id="pos16278">
+  assert </span><span class="nc" id="pos16288">y < 0 ==> x </span><span class="pc" id="pos16300"><</span><span class="nc" id="pos16301"> 0</span><span class="none" id="pos16303">;
+}
+
+// False antecedent ensures clause.
+method FalseAntecedentEnsuresClauseMethod(x: int) returns (r: int)
+  ensures </span><span class="pc" id="pos16421">r < 0 ==> x < 0</span><span class="none" id="pos16436">
+{
+  </span><span class="fc" id="pos16441">return x*x;</span><span class="none" id="pos16452">
+</span><span class="nc" id="pos16453">}</span><span class="none" id="pos16454">
+
+function ObviouslyUnreachableIfExpressionBranchFunc(x: int): (r:int)
+  requires </span><span class="fc" id="pos16536">x > 0</span><span class="none" id="pos16541">
+  ensures </span><span class="pc" id="pos16552">r > 0</span><span class="none" id="pos16557">
+{
+  if x < 0
+  then </span><span class="nc" id="pos16578">x - 1</span><span class="none" id="pos16583"> // unreachable
+  else </span><span class="fc" id="pos16606">x + 1</span><span class="none" id="pos16611">
+}
+
+method ObviouslyUnreachableIfStatementBranchMethod(x: int) returns (r:int)
+  requires </span><span class="pc" id="pos16701">x > 0</span><span class="none" id="pos16706">
+  ensures </span><span class="pc" id="pos16717">r > 0</span><span class="none" id="pos16722">
+{
+  if x < 0 {
+    </span><span class="nc" id="pos16742">return x - 1;</span><span class="none" id="pos16755"> // unreachable
+  } else {
+    </span><span class="fc" id="pos16786">return x + 1;</span><span class="none" id="pos16799">
+  }
+</span><span class="nc" id="pos16804">}</span><span class="none" id="pos16805">
+
+datatype T = A | B
+
+function ObviouslyUnreachableMatchExpressionCaseFunction(t: T): (r:int)
+  requires </span><span class="fc" id="pos16910">t != A</span><span class="none" id="pos16916">
+  ensures </span><span class="pc" id="pos16927">r > 1</span><span class="none" id="pos16932"> // alt: r > 0
+{
+  match t {
+    case A => </span><span class="nc" id="pos16975">1</span><span class="none" id="pos16976"> // unreachable
+    case B => </span><span class="fc" id="pos17006">2</span><span class="none" id="pos17007">
+  }
+}
+
+method ObviouslyUnreachableMatchStatementCaseMethod(t: T) returns (r:int)
+  requires </span><span class="pc" id="pos17100">t != A</span><span class="none" id="pos17106">
+  ensures </span><span class="pc" id="pos17117">r > 1</span><span class="none" id="pos17122"> // alt: r > 0
+{
+  match t {
+    case A => </span><span class="nc" id="pos17165">return 1;</span><span class="none" id="pos17174"> // unreachable
+    case B => </span><span class="fc" id="pos17204">return 2;</span><span class="none" id="pos17213">
+  }
+</span><span class="nc" id="pos17218">}</span><span class="none" id="pos17219">
+
+method ObviouslyUnreachableReturnStatementMethod(t: T) returns (r:int)
+  requires </span><span class="pc" id="pos17303">t != A</span><span class="none" id="pos17309">
+    ensures </span><span class="pc" id="pos17322">r > 1</span><span class="none" id="pos17327"> // alt: r > 0
+  {
+    if !t.A? {
+      </span><span class="fc" id="pos17367">return 2;</span><span class="none" id="pos17376">
+    }
+
+    </span><span class="nc" id="pos17388">return 1;</span><span class="none" id="pos17397"> // unreachable
+  </span><span class="nc" id="pos17415">}</span><span class="none" id="pos17416">
+
+method CalcStatementWithSideConditions(x: int) {
+  calc == {
+    </span><span class="nc" id="pos17483">x </span><span class="pc" id="pos17485">/</span><span class="nc" id="pos17486"> 2;
+    (x*2) </span><span class="pc" id="pos17500">/</span><span class="nc" id="pos17501"> 4</span><span class="none" id="pos17503">;
+  }
+}
+
+method DontWarnAboutVacuousAssertFalse(x: int) {
+  assume </span><span class="fc" id="pos17570">x == x + 1</span><span class="none" id="pos17580">;
+  assert </span><span class="nc" id="pos17591">f</span><span class="none" id="pos17592">alse;
+}
+
+// CHECK: Results for GetX \(well-formedness\)
+// CHECK:     Proof dependencies:
+// CHECK:       ProofDependencyLogging.dfy\(449,5\)-\(449,5\): target object is never null
+
+class C {
+  var x: int
+}
+
+function GetX(c: C): int
+  reads c
+{
+  </span><span class="nc" id="pos17839">c.</span><span class="pc" id="pos17841">x</span><span class="none" id="pos17842">
+}
+
+method DontWarnAboutUnusedAssumeTrue(x: int) {
+  assume </span><span class="nc" id="pos17902">t</span><span class="none" id="pos17903">rue;
+  assert 1 + x </span><span class="fc" id="pos17923">=</span><span class="none" id="pos17924">= 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/Test/logger/VerificationCoverageReport.dfy b/Test/logger/VerificationCoverageReport.dfy
new file mode 100644
index 00000000000..c8553c17cf3
--- /dev/null
+++ b/Test/logger/VerificationCoverageReport.dfy
@@ -0,0 +1,7 @@
+// NONUNIFORM: Not a compiler test
+// RUN: rm -rf "%t"/coverage
+// RUN: %baredafny verify --use-basename-for-filename --show-snippets false --verify-included-files --coverage-report "%t/coverage" %s
+// RUN: %sed 's/<h1 hidden.*//' "%t"/coverage/*/ProofDependencyLogging.dfy_verification.html > "%t"/coverage_actual.html
+// RUN: %diff "%S/ProofDependencyLogging.dfy_verification.html.expect" "%t/coverage_actual.html"
+
+include "ProofDependencyLogging.dfy"
diff --git a/docs/dev/news/4625.feat b/docs/dev/news/4625.feat
new file mode 100644
index 00000000000..fc2354afce0
--- /dev/null
+++ b/docs/dev/news/4625.feat
@@ -0,0 +1 @@
+The new `--coverage-report` flag to `dafny verify` creates an HTML report highlighting which portions of the program were and were not necessary for verification. The format is the same as for `dafny generate-tests --coverage-report` and files from the two commands can be merged.