diff --git a/Source/DafnyCore/CoverageReport/CoverageLabel.cs b/Source/DafnyCore/CoverageReport/CoverageLabel.cs
index 641c1a9d95d..a8a53d63933 100644
--- a/Source/DafnyCore/CoverageReport/CoverageLabel.cs
+++ b/Source/DafnyCore/CoverageReport/CoverageLabel.cs
@@ -4,6 +4,7 @@ namespace Microsoft.Dafny;
 
 public enum CoverageLabel {
   None,
+  NotApplicable,
   FullyCovered,
   NotCovered,
   PartiallyCovered,
@@ -15,6 +16,9 @@ public static class CoverageLabelExtension {
   /// Combine coverage labels. E.g. FullyCovered + NotCovered = PartiallyCovered
   /// </summary>
   public static CoverageLabel Combine(CoverageLabel one, CoverageLabel two) {
+    if (one == CoverageLabel.NotApplicable || two == CoverageLabel.NotApplicable) {
+      return CoverageLabel.NotApplicable;
+    }
     if (one == CoverageLabel.None) {
       return two;
     }
diff --git a/Source/DafnyCore/CoverageReport/CoverageReport.cs b/Source/DafnyCore/CoverageReport/CoverageReport.cs
index 22439517b8e..3593227fc5b 100644
--- a/Source/DafnyCore/CoverageReport/CoverageReport.cs
+++ b/Source/DafnyCore/CoverageReport/CoverageReport.cs
@@ -59,11 +59,13 @@ public void RegisterFiles(Program program) {
   }
 
   public void RegisterFile(Uri uri) {
-    labelsByFile[uri.LocalPath] = new List<CoverageSpan>();
+    if (!labelsByFile.ContainsKey(uri.LocalPath)) {
+      labelsByFile[uri.LocalPath] = new List<CoverageSpan>();
+    }
   }
 
   private void RegisterFiles(Node astNode) {
-    if (astNode.StartToken.ActualFilename != null) {
+    if (astNode.StartToken.ActualFilename != null && !labelsByFile.ContainsKey(astNode.StartToken.ActualFilename)) {
       labelsByFile[astNode.StartToken.ActualFilename] = new();
     }
 
diff --git a/Source/DafnyCore/Options/CommonOptionBag.cs b/Source/DafnyCore/Options/CommonOptionBag.cs
index b4d5d26a99c..b8a108c0e9c 100644
--- a/Source/DafnyCore/Options/CommonOptionBag.cs
+++ b/Source/DafnyCore/Options/CommonOptionBag.cs
@@ -213,6 +213,10 @@ May slow down verification slightly.
     "Emit verification coverage report  to a given directory, in the same format as a test coverage report.") {
     ArgumentHelpName = "directory"
   };
+  public static readonly Option<bool> NoTimeStampForCoverageReport = new("--no-timestamp-for-coverage-report",
+    "Write coverage report directly to the specified folder instead of creating a timestamped subdirectory.") {
+    IsHidden = true
+  };
 
   public static readonly Option<bool> IncludeRuntimeOption = new("--include-runtime",
     "Include the Dafny runtime as source in the target language.");
@@ -475,6 +479,7 @@ void ParsePrintMode(Option<PrintModes> option, Boogie.CommandLineParseState ps,
       WarnContradictoryAssumptions,
       WarnRedundantAssumptions,
       VerificationCoverageReport,
+      NoTimeStampForCoverageReport,
       DefaultFunctionOpacity
     );
   }
diff --git a/Source/DafnyCore/Options/DafnyCommands.cs b/Source/DafnyCore/Options/DafnyCommands.cs
index bf8b49b9326..e338b6e3edd 100644
--- a/Source/DafnyCore/Options/DafnyCommands.cs
+++ b/Source/DafnyCore/Options/DafnyCommands.cs
@@ -42,6 +42,7 @@ static DafnyCommands() {
     CommonOptionBag.DefaultFunctionOpacity,
     CommonOptionBag.WarnContradictoryAssumptions,
     CommonOptionBag.WarnRedundantAssumptions,
+    CommonOptionBag.NoTimeStampForCoverageReport,
     CommonOptionBag.VerificationCoverageReport
   }.ToList();
 
diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs b/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs
index ffe2a56d7e9..c3c9403cb2a 100644
--- a/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs
+++ b/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs
@@ -612,6 +612,9 @@ private void TrPredicateStmt(PredicateStmt stmt, BoogieStmtListBuilder builder,
           builder.Add(TrAssumeCmdWithDependencies(etran, stmt.Tok, stmt.Expr, "assume statement", true));
           stmtContext = StmtType.NONE;
         }
+        if (options.TestGenOptions.Mode != TestGenerationOptions.Modes.None) {
+          builder.AddCaptureState(stmt);
+        }
       } else if (stmt is ExpectStmt) {
         AddComment(builder, stmt, "expect statement");
         var s = (ExpectStmt)stmt;
@@ -639,6 +642,9 @@ private void TrPredicateStmt(PredicateStmt stmt, BoogieStmtListBuilder builder,
         TrStmt_CheckWellformed(s.Expr, builder, locals, etran, false);
         builder.Add(TrAssumeCmdWithDependencies(etran, stmt.Tok, s.Expr, "assume statement", true, etran.TrAttributes(stmt.Attributes, null)));
         stmtContext = StmtType.NONE; // done with translating assume stmt.
+        if (options.TestGenOptions.Mode != TestGenerationOptions.Modes.None) {
+          builder.AddCaptureState(s);
+        }
       }
       this.fuelContext = FuelSetting.PopFuelContext();
     }
diff --git a/Source/DafnyDriver/Commands/CoverageReportCommand.cs b/Source/DafnyDriver/Commands/CoverageReportCommand.cs
index 63cddabb610..846e71440b4 100644
--- a/Source/DafnyDriver/Commands/CoverageReportCommand.cs
+++ b/Source/DafnyDriver/Commands/CoverageReportCommand.cs
@@ -4,7 +4,6 @@
 #nullable disable
 using System.Collections.Generic;
 using System.CommandLine;
-using System.CommandLine.Invocation;
 using System.IO;
 using System.Linq;
 using System.Threading.Tasks;
@@ -13,6 +12,11 @@ namespace Microsoft.Dafny;
 
 static class CoverageReportCommand {
 
+  public static IEnumerable<Option> Options =>
+    new Option[] {
+      CommonOptionBag.NoTimeStampForCoverageReport,
+    };
+
   static CoverageReportCommand() {
     ReportsArgument = new("reports", r => {
       return r.Tokens.Where(t => !string.IsNullOrEmpty(t.Value)).Select(t => new FileInfo(t.Value)).ToList();
@@ -29,6 +33,9 @@ public static Command Create() {
       "Merge several previously generated coverage reports together.");
     result.AddArgument(OutDirArgument);
     result.AddArgument(ReportsArgument);
+    foreach (var option in Options) {
+      result.AddOption(option);
+    }
 
     DafnyCli.SetHandlerUsingDafnyOptionsContinuation(result, (options, _) => {
       var coverageReporter = new CoverageReporter(options);
diff --git a/Source/DafnyDriver/Commands/GenerateTestsCommand.cs b/Source/DafnyDriver/Commands/GenerateTestsCommand.cs
index 1220d587f49..92f085cd62c 100644
--- a/Source/DafnyDriver/Commands/GenerateTestsCommand.cs
+++ b/Source/DafnyDriver/Commands/GenerateTestsCommand.cs
@@ -26,6 +26,7 @@ static class GenerateTestsCommand {
       BoogieOptionBag.VerificationTimeLimit,
       PrintBpl,
       CoverageReport,
+      CommonOptionBag.NoTimeStampForCoverageReport,
       ForcePrune
     }.Concat(DafnyCommands.ConsoleOutputOptions).
       Concat(DafnyCommands.ResolverOptions);
diff --git a/Source/DafnyDriver/CoverageReporter.cs b/Source/DafnyDriver/CoverageReporter.cs
index 2f7229ae437..15eee5f94d5 100644
--- a/Source/DafnyDriver/CoverageReporter.cs
+++ b/Source/DafnyDriver/CoverageReporter.cs
@@ -6,7 +6,6 @@
 using System.Text.RegularExpressions;
 using DafnyCore.Verifier;
 using Microsoft.Boogie;
-using Microsoft.Extensions.Primitives;
 
 namespace Microsoft.Dafny; 
 
@@ -25,7 +24,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 PosRegexInverse = new("class=\"([a-z]+)\" id=\"pos([0-9]+)\">");
+  private static readonly Regex PosRegexInverse = new("class=\"([a-z]+)\" id=\"([0-9]+):([0-9]+)\"");
   private const string CoverageReportTemplatePath = "coverage_report_template.html";
   private const string CoverageReportIndexTemplatePath = "coverage_report_index_template.html";
   private const string CoverageReportSupportingFilesPath = ".resources";
@@ -50,7 +49,7 @@ public void SerializeVerificationCoverageReport(ProofDependencyManager depManage
       depManager
         .GetAllPotentialDependencies()
         .OrderBy(dep => dep.Range.StartToken);
-    var coverageReport = new CoverageReport("Verification coverage", "Lines", "_verification", dafnyProgram);
+    var coverageReport = new CoverageReport("Verification coverage", "Proof Dependencies", "_verification", dafnyProgram);
     foreach (var dep in allDependencies) {
       if (dep is FunctionDefinitionDependency) {
         continue;
@@ -65,8 +64,8 @@ public void SerializeVerificationCoverageReport(ProofDependencyManager depManage
   }
 
   public void Merge(List<string> coverageReportsToMerge, string coverageReportOutDir) {
-    // assume only one report in directory for now
     List<CoverageReport> reports = new();
+    var mergedReport = new CoverageReport("Combined Coverage Report", "Locations", "_combined", null);
     foreach (var reportDir in coverageReportsToMerge) {
       if (!Directory.Exists(reportDir)) {
         reporter.Warning(MessageSource.Documentation, ErrorRegistry.NoneId, Token.NoToken,
@@ -77,8 +76,7 @@ public void Merge(List<string> coverageReportsToMerge, string coverageReportOutD
         var indexFileName = Path.GetFileName(pathToIndexFile);
         var indexFileMatch = IndexFileNameRegex.Match(indexFileName);
         if (!indexFileMatch.Success) {
-          reporter.Warning(MessageSource.Documentation, ErrorRegistry.NoneId, Token.NoToken,
-            $"Directory {reportDir} contains file {indexFileName} which is not part of a coverage report");
+          continue;
         }
         var suffix = indexFileMatch.Groups[1].Value;
         var index = new StreamReader(pathToIndexFile).ReadToEnd();
@@ -87,6 +85,15 @@ public void Merge(List<string> coverageReportsToMerge, string coverageReportOutD
         reports.Add(ParseCoverageReport(reportDir, $"{name} ({Path.GetFileName(reportDir)})", units, suffix));
       }
     }
+    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);
+        }
+      }
+    }
+    reports.Add(mergedReport);
     SerializeCoverageReports(reports, coverageReportOutDir);
   }
 
@@ -104,23 +111,31 @@ private static CoverageReport ParseCoverageReport(string reportDir, string name,
       if (!uriMatch.Success) {
         continue;
       }
+
       var uri = new Uri(uriMatch.Groups[1].Value);
       var lastEndToken = new Token(1, 1);
+      lastEndToken.Uri = uri;
+      var lastLabel = CoverageLabel.NotApplicable;
       report.RegisterFile(uri);
       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);
+        if (int.TryParse(span.Groups[2].Value, out var line) &&
+            int.TryParse(span.Groups[3].Value, out var col)) {
+          var nextToken = new Token(line, col);
+          nextToken.Uri = uri;
+          var precedingToken = new Token(line, col - 1);
+          precedingToken.Uri = uri;
+          var rangeToken = new RangeToken(lastEndToken, precedingToken);
           rangeToken.Uri = uri;
-          report.LabelCode(rangeToken, FromHtmlClass(span.Groups[1].Value));
+          report.LabelCode(rangeToken, lastLabel);
+          lastLabel = FromHtmlClass(span.Groups[1].Value);
+          lastEndToken = nextToken;
         }
       }
+
+      var lastToken = new Token(source.Count(c => c == '\n') + 2, 0);
+      lastToken.Uri = uri;
+      var lastRangeToken = new RangeToken(lastEndToken, lastToken);
+      report.LabelCode(lastRangeToken, lastLabel);
     }
     return report;
   }
@@ -135,8 +150,11 @@ public void SerializeCoverageReports(CoverageReport report, string directory) {
   /// will have links to each other to make comparison easier
   /// </summary>
   private void SerializeCoverageReports(List<CoverageReport> reports, string reportsDirectory) {
-    var sessionName = DateTime.Now.ToString("yyyy-dd-M--HH-mm-ss");
-    var sessionDirectory = Path.Combine(reportsDirectory, sessionName);
+    var sessionDirectory = reportsDirectory;
+    if (!options.Get(CommonOptionBag.NoTimeStampForCoverageReport)) {
+      var sessionName = DateTime.Now.ToString("yyyy-dd-M--HH-mm-ss");
+      sessionDirectory = Path.Combine(reportsDirectory, sessionName);
+    }
     Directory.CreateDirectory(sessionDirectory);
     HashSet<string> allFiles = new();
     reports.ForEach(report => allFiles.UnionWith(report.AllFiles()));
@@ -149,7 +167,7 @@ private void SerializeCoverageReports(List<CoverageReport> reports, string repor
     var prefixLength = new string(
       allFiles.First()[..allFiles.Min(s => Path.GetDirectoryName(s)?.Length ?? 0)]
         .TakeWhile((c, i) => allFiles.All(s => s[i] == c)).ToArray()).Length;
-    Dictionary<string, string> sourceFileToCoverageReport = new Dictionary<string, string>();
+    var sourceFileToCoverageReport = new Dictionary<string, string>();
     foreach (var fileName in allFiles) {
       var directoryForFile = Path.Combine(sessionDirectory, Path.GetDirectoryName(fileName)?[prefixLength..].TrimStart('/') ?? "");
       var pathToRoot = Path.GetRelativePath(directoryForFile, sessionDirectory);
@@ -190,7 +208,9 @@ private void CreateIndexFile(CoverageReport report, Dictionary<string, string> s
     }
     var coverageLabels = Enum.GetValues(typeof(CoverageLabel)).Cast<CoverageLabel>().ToList();
     List<object> header = new() { "File" };
-    header.AddRange(coverageLabels.Select(label => $"{report.Units} {CoverageLabelExtension.ToString(label)}"));
+    header.AddRange(coverageLabels
+      .Where(label => label != CoverageLabel.None && label != CoverageLabel.NotApplicable)
+      .Select(label => $"{report.Units} {CoverageLabelExtension.ToString(label)}"));
 
     List<List<object>> body = new();
     foreach (var sourceFile in sourceFileToCoverageReportFile.Keys) {
@@ -199,13 +219,15 @@ private void CreateIndexFile(CoverageReport report, Dictionary<string, string> s
         $"<a href = \"{relativePath}{report.UniqueSuffix}.html\"" +
         $"class = \"el_package\">{relativePath}</a>"
       });
-      body.Last().AddRange(coverageLabels.Select(label =>
-        report.CoverageSpansForFile(sourceFile).Count(span => span.Label == label)).OfType<object>());
+      body.Last().AddRange(coverageLabels
+        .Where(label => label != CoverageLabel.None && label != CoverageLabel.NotApplicable)
+        .Select(label => report.CoverageSpansForFile(sourceFile).Count(span => span.Label == label)).OfType<object>());
     }
 
     List<object> footer = new() { "Total" };
-    footer.AddRange(coverageLabels.Select(label =>
-      report.AllFiles().Select(sourceFile =>
+    footer.AddRange(coverageLabels
+      .Where(label => label != CoverageLabel.None && label != CoverageLabel.NotApplicable)
+      .Select(label => report.AllFiles().Select(sourceFile =>
         report.CoverageSpansForFile(sourceFile).Count(span => span.Label == label)).Sum()).OfType<object>());
 
     var templateText = new StreamReader(templateStream).ReadToEnd();
@@ -264,29 +286,46 @@ 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");
-    var characterLabels = new CoverageLabel[source.Length];
-    Array.Fill(characterLabels, CoverageLabel.None);
-    IToken lastToken = new Token(1, 1);
+    var lines = source.Split(new[] { Environment.NewLine }, StringSplitOptions.None);
+    var characterLabels = new CoverageLabel[lines.Length][];
+    for (int i = 0; i < lines.Length; i++) {
+      characterLabels[i] = new CoverageLabel[lines[i].Length];
+      Array.Fill(characterLabels[i], CoverageLabel.None);
+    }
     var labeledCodeBuilder = new StringBuilder(source.Length);
     foreach (var span in report.CoverageSpansForFile(pathToSourceFile)) {
-      for (var pos = span.Span.StartToken.pos; pos <= span.Span.EndToken.pos; pos++) {
-        characterLabels[pos] = CoverageLabelExtension.Combine(characterLabels[pos], span.Label);
+      var line = span.Span.StartToken.line - 1;
+      var column = span.Span.StartToken.col - 1;
+      while (true) {
+        if (characterLabels[line].Length <= column) {
+          do { line++; }
+          while (line < characterLabels.Length && characterLabels[line].Length == 0);
+          column = 0;
+          if (characterLabels.Length == line) {
+            break;
+          }
+        }
+        if (line > span.Span.EndToken.line - 1 || (line == span.Span.EndToken.line - 1 && column > span.Span.EndToken.col - 1)) {
+          break;
+        }
+        characterLabels[line][column] = CoverageLabelExtension.Combine(characterLabels[line][column], span.Label);
+        column++;
       }
     }
 
-    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));
+    var lastLabel = CoverageLabel.NotApplicable;
+    labeledCodeBuilder.Append(OpenHtmlTag(1, 1, CoverageLabel.NotApplicable));
+    for (var line = 0; line < lines.Length; line++) {
+      for (var col = 0; col < lines[line].Length; col++) {
+        var thisLabel = characterLabels[line][col] == CoverageLabel.None ? CoverageLabel.NotApplicable : characterLabels[line][col];
+        if (thisLabel != lastLabel) {
+          labeledCodeBuilder.Append(CloseHtmlTag());
+          labeledCodeBuilder.Append(OpenHtmlTag(line + 1, col + 1, thisLabel));
+        }
+        labeledCodeBuilder.Append(lines[line][col]);
+        lastLabel = thisLabel;
       }
-
-      labeledCodeBuilder.Append(source[pos]);
-
-      lastLabel = thisLabel;
+      labeledCodeBuilder.Append(Environment.NewLine);
     }
     labeledCodeBuilder.Append(CloseHtmlTag());
 
@@ -317,6 +356,7 @@ private static string ToHtmlClass(CoverageLabel label) {
       CoverageLabel.NotCovered => "nc",
       CoverageLabel.PartiallyCovered => "pc",
       CoverageLabel.None => "none",
+      CoverageLabel.NotApplicable => "na",
       _ => ""
     };
   }
@@ -331,8 +371,8 @@ private static CoverageLabel FromHtmlClass(string htmlClass) {
     return CoverageLabel.NotCovered; // this is a fallback in case the HTML has invalid classes
   }
 
-  private string OpenHtmlTag(int pos, CoverageLabel label) {
-    var id = $"id=\"pos{pos}\"";
+  private string OpenHtmlTag(int line, int col, CoverageLabel label) {
+    var id = $"id=\"{line}:{col}\"";
     var classLabel = ToHtmlClass(label);
     return $"<span class=\"{classLabel}\" {id}>";
   }
diff --git a/Source/DafnyTestGeneration/BlockBasedModifier.cs b/Source/DafnyTestGeneration/BlockBasedModifier.cs
index 5be526ea629..974ad31f0da 100644
--- a/Source/DafnyTestGeneration/BlockBasedModifier.cs
+++ b/Source/DafnyTestGeneration/BlockBasedModifier.cs
@@ -72,7 +72,7 @@ private IEnumerable<ProgramModification> VisitImplementation(
           twinBlock.cmds.Add(new AssertCmd(new Token(), new LiteralExpr(new Token(), false)));
         }
         var record = modifications.GetProgramModification(program, implementation,
-          new HashSet<string>() { state },
+          Utils.AllBlockIds(block, DafnyInfo.Options).ToHashSet(),
           testEntryNames, $"{implementation.VerboseName.Split(" ")[0]} ({state})");
         if (record.IsCovered(modifications)) {
           foreach (var twinBlock in stateToBlocksMap[state]) {
diff --git a/Source/DafnyTestGeneration/Main.cs b/Source/DafnyTestGeneration/Main.cs
index c2befe4861a..c74f4e1d75f 100644
--- a/Source/DafnyTestGeneration/Main.cs
+++ b/Source/DafnyTestGeneration/Main.cs
@@ -116,7 +116,6 @@ private static void PopulateCoverageReport(CoverageReport coverageReport, Progra
         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) {
@@ -144,12 +143,8 @@ private static void PopulateCoverageReport(CoverageReport coverageReport, Progra
           } catch (ArgumentException) {
             continue;
           }
-          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));
+          var rangeToken = new RangeToken(new Token(lineNumber, 1), new Token(lineNumber + 1, 0));
           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/ProgramModifier.cs b/Source/DafnyTestGeneration/ProgramModifier.cs
index f126e8952eb..0fb8e710280 100644
--- a/Source/DafnyTestGeneration/ProgramModifier.cs
+++ b/Source/DafnyTestGeneration/ProgramModifier.cs
@@ -150,17 +150,15 @@ public AnnotationVisitor(DafnyOptions options) {
       }
 
       public override Block VisitBlock(Block node) {
-        var state = Utils.GetBlockId(node, options);
-        if (state == null) { // cannot map back to Dafny source location
-          return base.VisitBlock(node);
-        }
-        var data = new List<object>
-          { "Block", implementation.Name, state };
         int afterPartition = node.cmds.FindIndex(cmd =>
           cmd is not AssumeCmd assumeCmd || assumeCmd.Attributes == null || assumeCmd.Attributes.Key != "partition");
         afterPartition = afterPartition > -1 ? afterPartition : 0;
-        node.cmds.Insert(afterPartition, GetAssumePrintCmd(data));
-        return node;
+        foreach (var state in Utils.AllBlockIds(node, options)) {
+          var data = new List<object>
+            { "Block", implementation.Name, state };
+          node.cmds.Insert(afterPartition, GetAssumePrintCmd(data));
+        }
+        return base.VisitBlock(node);
       }
 
       public override Implementation VisitImplementation(Implementation node) {
diff --git a/Source/DafnyTestGeneration/Utils.cs b/Source/DafnyTestGeneration/Utils.cs
index b8d5d40e7e5..e82d6513fb8 100644
--- a/Source/DafnyTestGeneration/Utils.cs
+++ b/Source/DafnyTestGeneration/Utils.cs
@@ -8,6 +8,7 @@
 using System.Linq;
 using System.Text.RegularExpressions;
 using System.Threading;
+using JetBrains.Annotations;
 using Microsoft.Boogie;
 using Microsoft.Dafny;
 using Microsoft.Dafny.LanguageServer.CounterExampleGeneration;
@@ -130,36 +131,25 @@ public static string GetStringRepresentation(DafnyOptions options, Microsoft.Boo
     /// Extract string mapping this basic block to a location in Dafny code.
     /// </summary>
     public static string GetBlockId(Block block, DafnyOptions options) {
-      var state = block.cmds.OfType<AssumeCmd>().FirstOrDefault(
-          cmd => cmd.Attributes != null &&
-                 cmd.Attributes.Key == "captureState" &&
-                 cmd.Attributes.Params != null &&
-                 cmd.Attributes.Params.Count() == 1)
-        ?.Attributes.Params[0].ToString();
-      string uniqueId = options.TestGenOptions.Mode != TestGenerationOptions.Modes.Block ? "#" + block.UniqueId : "";
-      return state == null ? null : Regex.Replace(state, @"\s+", "") + uniqueId;
+      return AllBlockIds(block, options).FirstOrDefault((string)null);
     }
 
     /// <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.
+    /// Extract string mapping this basic block to locations in Dafny code.
     /// </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
+    [ItemCanBeNull]
+    public static List<string> AllBlockIds(Block block, DafnyOptions options) {
+      string uniqueId = options.TestGenOptions.Mode != TestGenerationOptions.Modes.Block ? "#" + block.UniqueId : "";
+      var state = block.cmds.OfType<AssumeCmd>()
+        .Where(
+          cmd => cmd.Attributes != null &&
+                 cmd.Attributes.Key == "captureState" &&
+                 cmd.Attributes.Params != null &&
+                 cmd.Attributes.Params.Count() == 1)
+        .Select(
+          cmd => cmd.Attributes.Params[0].ToString())
+        .Select(cmd => Regex.Replace(cmd, @"\s+", "") + uniqueId);
+      return state.ToList();
     }
 
     public static IList<object> GetAttributeValue(Implementation implementation, string attribute) {
diff --git a/Test/logger/CoverageReport.dfy b/Test/logger/CoverageReport.dfy
new file mode 100644
index 00000000000..36a14821d85
--- /dev/null
+++ b/Test/logger/CoverageReport.dfy
@@ -0,0 +1,19 @@
+// NONUNIFORM: Not a compiler test
+// Verification coverage:
+// RUN: rm -rf "%t"/coverage_verification
+// RUN: %baredafny verify --use-basename-for-filename --show-snippets false --verify-included-files --no-timestamp-for-coverage-report --coverage-report "%t/coverage_verification" %s
+// RUN: %sed 's/<h1 hidden.*//' "%t"/coverage_verification/ProofDependencyLogging.dfy_verification.html > "%t"/coverage_verification_actual.html
+// RUN: %diff "%S/ProofDependencyLogging.dfy_verification.html.expect" "%t/coverage_verification_actual.html"
+// Test coverage:
+// RUN: rm -rf "%t"/coverage_testing
+// RUN: %baredafny generate-tests Block --no-timestamp-for-coverage-report --coverage-report "%t/coverage_testing" %s
+// RUN: %sed 's/<h1 hidden.*//' "%t"/coverage_testing/ProofDependencyLogging.dfy_tests_expected.html > "%t"/coverage_testing_actual.html
+// RUN: %diff "%S/ProofDependencyLogging.dfy_tests_expected.html.expect" "%t/coverage_testing_actual.html"
+// Combined coverage:
+// RUN: rm -rf "%t"/coverage_combined
+// 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"
+
+
+include "ProofDependencyLogging.dfy"
diff --git a/Test/logger/ProofDependencyLogging.dfy b/Test/logger/ProofDependencyLogging.dfy
index 4e2ad45a92e..6f23634abe4 100644
--- a/Test/logger/ProofDependencyLogging.dfy
+++ b/Test/logger/ProofDependencyLogging.dfy
@@ -1,30 +1,30 @@
 // RUN: %baredafny verify --log-format:text --boogie -trackVerificationCoverage "%s" > "%t"
 // RUN: %OutputCheck --file-to-check "%t" "%s"
-// CHECK: Results for RedundantAssumeMethod \(correctness\)
+// 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 ContradictoryAssumeMethod \(correctness\)
+// 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 AssumeFalseMethod \(correctness\)
+// CHECK: Results for M.AssumeFalseMethod \(correctness\)
 // CHECK:     Proof dependencies:
 // CHECK:       ProofDependencyLogging.dfy\(192,12\)-\(192,12\): assume statement
 //
-// CHECK: Results for ObviouslyContradictoryRequiresFunc \(well-formedness\)
+// 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 ObviouslyContradictoryRequiresMethod \(correctness\)
+// 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 ObviouslyRedundantRequiresFunc \(well-formedness\)
+// 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
@@ -32,24 +32,24 @@
 // 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: 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 ObviouslyUnnecessaryRequiresFunc \(well-formedness\)
+// 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 ObviouslyUnnecessaryRequiresMethod \(correctness\)
+// 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 ObviouslyUnconstrainedCodeFunc \(well-formedness\)
+// 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
@@ -58,14 +58,14 @@
 // 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: 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 PartiallyRedundantRequiresFunc \(well-formedness\)
+// 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
@@ -73,25 +73,25 @@
 // 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: 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 MultiPartRedundantRequiresFunc \(well-formedness\)
+// 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 MultiPartRedundantRequiresMethod \(correctness\)
+// 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 MultiPartContradictoryRequiresFunc \(well-formedness\)
+// 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
@@ -99,13 +99,13 @@
 // 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: 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 CallContradictoryFunctionFunc \(well-formedness\)
+// 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
@@ -113,41 +113,41 @@
 // 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: 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 FalseAntecedentRequiresClauseMethod \(correctness\)
+// CHECK: Results for M.FalseAntecedentRequiresClauseMethod \(correctness\)
 // CHECK:     Proof dependencies:
 // CHECK:       ProofDependencyLogging.dfy\(357,3\)-\(357,15\): assignment \(or return\)
 //
-// CHECK: Results for FalseAntecedentAssertStatementMethod \(correctness\)
+// 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 FalseAntecedentEnsuresClauseMethod \(correctness\)
+// 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 ObviouslyUnreachableIfExpressionBranchFunc \(well-formedness\)
+// 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 ObviouslyUnreachableIfStatementBranchMethod \(correctness\)
+// 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 ObviouslyUnreachableMatchExpressionCaseFunction \(well-formedness\)
+// CHECK: Results for M.ObviouslyUnreachableMatchExpressionCaseFunction \(well-formedness\)
 //
 // CHECK:     Proof dependencies:
 // CHECK:       ProofDependencyLogging.dfy\(395,1\)-\(403,1\): function definition for ObviouslyUnreachableMatchExpressionCaseFunction
@@ -155,22 +155,22 @@
 // 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: 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 ObviouslyUnreachableReturnStatementMethod \(correctness\)
+// 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 RedundantAssumeMethod(n: int)
+method {:testEntry} RedundantAssumeMethod(n: int)
 {
     // either one or the other assumption shouldn't be covered
     assume n > 4;
@@ -178,7 +178,7 @@ method RedundantAssumeMethod(n: int)
     assert n > 1;
 }
 
-method ContradictoryAssumeMethod(n: int)
+method {:testEntry} ContradictoryAssumeMethod(n: int)
 {
     assume n > 0;
     assume n < 0;
@@ -186,7 +186,7 @@ method ContradictoryAssumeMethod(n: int)
     assert n < 10; // shouldn't be covered
 }
 
-method AssumeFalseMethod(n: int)
+method {:testEntry} AssumeFalseMethod(n: int)
 {
     assume n == 15; // shouldn't be covered
     assume false;
@@ -194,7 +194,7 @@ method AssumeFalseMethod(n: int)
 }
 
 // Obvious contradiction in requires clauses.
-function ObviouslyContradictoryRequiresFunc(x: nat): (r: nat)
+function {:testEntry} ObviouslyContradictoryRequiresFunc(x: nat): (r: nat)
   requires x > 10
   requires x < 10
   ensures r < x // only provable vacuously 
@@ -203,7 +203,7 @@ function ObviouslyContradictoryRequiresFunc(x: nat): (r: nat)
   x - 1 // not necessarily a valid nat
 }
 
-method ObviouslyContradictoryRequiresMethod(x: nat) returns (r: nat)
+method {:testEntry} ObviouslyContradictoryRequiresMethod(x: nat) returns (r: nat)
   requires x > 10
   requires x < 10
   ensures r < x // only provable vacuously
@@ -213,7 +213,7 @@ method ObviouslyContradictoryRequiresMethod(x: nat) returns (r: nat)
 }
 
 // Obvious redundancy in requires clauses.
-function ObviouslyRedundantRequiresFunc(x: nat): (r: nat)
+function {:testEntry} ObviouslyRedundantRequiresFunc(x: nat): (r: nat)
   requires x < 10
   requires x < 100 // implied by previous requires clause
   ensures r < 11 // should cause body and first requires clause to be covered
@@ -221,7 +221,7 @@ function ObviouslyRedundantRequiresFunc(x: nat): (r: nat)
   x + 1
 }
 
-method ObviouslyRedundantRequiresMethod(x: nat) returns (r: nat)
+method {:testEntry} ObviouslyRedundantRequiresMethod(x: nat) returns (r: nat)
   requires x < 10
   requires x < 100 // implied by previous requires clause
   ensures r < 11 // should cause body and first requires clause to be covered
@@ -230,14 +230,14 @@ method ObviouslyRedundantRequiresMethod(x: nat) returns (r: nat)
 }
 
 // Obviously unnecessary requires clauses.
-function ObviouslyUnnecessaryRequiresFunc(x: nat): (r: nat)
+function {:testEntry} ObviouslyUnnecessaryRequiresFunc(x: nat): (r: nat)
   requires x < 10 // not required for the proof
 {
   // cause at least a little proof work to be necessary, for nat bounds
   if (x > 5) then x + 2 else x + 1
 }
 
-method ObviouslyUnnecessaryRequiresMethod(x: nat) returns (r: nat)
+method {:testEntry} ObviouslyUnnecessaryRequiresMethod(x: nat) returns (r: nat)
   requires x < 10 // not required for the proof
 {
   // cause at least a little proof work to be necessary, for nat bounds
@@ -245,7 +245,7 @@ method ObviouslyUnnecessaryRequiresMethod(x: nat) returns (r: nat)
 }
 
 // Code obviously not constrained by ensures clause.
-function ObviouslyUnconstrainedCodeFunc(x: int): (r: (int, int))
+function {:testEntry} ObviouslyUnconstrainedCodeFunc(x: int): (r: (int, int))
   requires x > 10
   ensures r.0 > 10
 {
@@ -255,7 +255,7 @@ function ObviouslyUnconstrainedCodeFunc(x: int): (r: (int, int))
    b)
 }
 
-method ObviouslyUnconstrainedCodeMethod(x: int) returns (r: (int, int))
+method {:testEntry} ObviouslyUnconstrainedCodeMethod(x: int) returns (r: (int, int))
   requires x > 10
   ensures r.0 > 10
 {
@@ -267,7 +267,7 @@ method ObviouslyUnconstrainedCodeMethod(x: int) returns (r: (int, int))
 }
 
 // Partial redundancy in requires clauses.
-function PartiallyRedundantRequiresFunc(x: nat): (r: nat)
+function {:testEntry} PartiallyRedundantRequiresFunc(x: nat): (r: nat)
   requires x < 100 && x < 10 // LHS implied by RHS
   ensures r < 11 // should cause body and RHS clause to be covered
 {
@@ -275,7 +275,7 @@ function PartiallyRedundantRequiresFunc(x: nat): (r: nat)
 }
 
 // Partly unnecessary requires clause.
-function PartiallyUnnecessaryRequiresFunc(x: int): (r: nat)
+function {:testEntry} PartiallyUnnecessaryRequiresFunc(x: int): (r: nat)
   requires x < 10 && x > 0 // RHS required for proof, but not LHS
 {
   // cause at least a little proof work to be necessary, for nat bounds
@@ -285,7 +285,7 @@ function PartiallyUnnecessaryRequiresFunc(x: int): (r: nat)
 
 // 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)
+function {:testEntry} MultiPartRedundantRequiresFunc(x: int): (r: int)
   requires x > 10
   requires x < 12
   requires x == 11 // implied by the previous two, but neither individually
@@ -294,7 +294,7 @@ function MultiPartRedundantRequiresFunc(x: int): (r: int)
   x
 }
 
-method MultiPartRedundantRequiresMethod(x: int) returns (r: int)
+method {:testEntry} MultiPartRedundantRequiresMethod(x: int) returns (r: int)
   requires x > 10
   requires x < 12
   requires x == 11 // implied by the previous two, but neither individually
@@ -306,7 +306,7 @@ method MultiPartRedundantRequiresMethod(x: int) returns (r: int)
 // 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)
+function {:testEntry} MultiPartContradictoryRequiresFunc(x: int, y: int): (r: int)
   requires x > 10
   requires x < 12
   requires y != 11 // contradicts the previous two
@@ -315,7 +315,7 @@ function MultiPartContradictoryRequiresFunc(x: int, y: int): (r: int)
   x
 }
 
-method MultiPartContradictoryRequiresMethod(x: int, y: int) returns (r: int)
+method {:testEntry} MultiPartContradictoryRequiresMethod(x: int, y: int) returns (r: int)
   requires x > 10
   requires x < 12
   requires y != 11 // contradicts the previous two
@@ -324,16 +324,16 @@ method MultiPartContradictoryRequiresMethod(x: int, y: int) returns (r: int)
   return x;
 }
 
-function ContradictoryEnsuresClauseFunc(x: int): (r: int)
+function {:testEntry} ContradictoryEnsuresClauseFunc(x: int): (r: int)
   requires x > 1
   ensures  r > x && r < 0
 
-method ContradictoryEnsuresClauseMethod(x: int) returns (r: int)
+method {:testEntry} ContradictoryEnsuresClauseMethod(x: int) returns (r: int)
   requires x > 1
   ensures  r > x && r < 0
 
 // Call function that has contradictory ensures clauses.
-function CallContradictoryFunctionFunc(x: int): (r: int)
+function {:testEntry} CallContradictoryFunctionFunc(x: int): (r: int)
   requires x > 1
   ensures r < 0
 {
@@ -341,7 +341,7 @@ function CallContradictoryFunctionFunc(x: int): (r: int)
   ContradictoryEnsuresClauseFunc(x) - 1
 }
 
-method CallContradictoryMethodMethod(x: int) returns (r: int)
+method {:testEntry} CallContradictoryMethodMethod(x: int) returns (r: int)
   requires x > 1
   ensures r < 0
 {
@@ -350,7 +350,7 @@ method CallContradictoryMethodMethod(x: int) returns (r: int)
 }
 
 // False antecedent requires clause
-method FalseAntecedentRequiresClauseMethod(x: int) returns (r: int)
+method {:testEntry} FalseAntecedentRequiresClauseMethod(x: int) returns (r: int)
   requires x*x < 0 ==> x == x + 1
   ensures r > x
 {
@@ -358,19 +358,19 @@ method FalseAntecedentRequiresClauseMethod(x: int) returns (r: int)
 }
 
 // False antecedent assert statement.
-method FalseAntecedentAssertStatementMethod(x: int) {
+method {:testEntry} FalseAntecedentAssertStatementMethod(x: int) {
   var y := x*x;
   assert y < 0 ==> x < 0;
 }
 
 // False antecedent ensures clause.
-method FalseAntecedentEnsuresClauseMethod(x: int) returns (r: int)
+method {:testEntry} FalseAntecedentEnsuresClauseMethod(x: int) returns (r: int)
   ensures r < 0 ==> x < 0
 {
   return x*x;
 }
 
-function ObviouslyUnreachableIfExpressionBranchFunc(x: int): (r:int)
+function {:testEntry} ObviouslyUnreachableIfExpressionBranchFunc(x: int): (r:int)
   requires x > 0
   ensures r > 0
 {
@@ -379,7 +379,7 @@ function ObviouslyUnreachableIfExpressionBranchFunc(x: int): (r:int)
   else x + 1
 }
 
-method ObviouslyUnreachableIfStatementBranchMethod(x: int) returns (r:int)
+method {:testEntry} ObviouslyUnreachableIfStatementBranchMethod(x: int) returns (r:int)
   requires x > 0
   ensures r > 0
 {
@@ -392,7 +392,7 @@ method ObviouslyUnreachableIfStatementBranchMethod(x: int) returns (r:int)
 
 datatype T = A | B
 
-function ObviouslyUnreachableMatchExpressionCaseFunction(t: T): (r:int)
+function {:testEntry} ObviouslyUnreachableMatchExpressionCaseFunction(t: T): (r:int)
   requires t != A
   ensures r > 1 // alt: r > 0
 {
@@ -402,7 +402,7 @@ function ObviouslyUnreachableMatchExpressionCaseFunction(t: T): (r:int)
   }
 }
 
-method ObviouslyUnreachableMatchStatementCaseMethod(t: T) returns (r:int)
+method {:testEntry} ObviouslyUnreachableMatchStatementCaseMethod(t: T) returns (r:int)
   requires t != A
   ensures r > 1 // alt: r > 0
 {
@@ -412,7 +412,7 @@ method ObviouslyUnreachableMatchStatementCaseMethod(t: T) returns (r:int)
   }
 }
 
-method ObviouslyUnreachableReturnStatementMethod(t: T) returns (r:int)
+method {:testEntry} ObviouslyUnreachableReturnStatementMethod(t: T) returns (r:int)
   requires t != A
     ensures r > 1 // alt: r > 0
   {
@@ -423,19 +423,19 @@ method ObviouslyUnreachableReturnStatementMethod(t: T) returns (r:int)
     return 1; // unreachable
   }
 
-method CalcStatementWithSideConditions(x: int) {
+method {:testEntry} CalcStatementWithSideConditions(x: int) {
   calc == {
     x / 2;
     (x*2) / 4;
   }
 }
 
-method DontWarnAboutVacuousAssertFalse(x: int) {
+method {:testEntry} DontWarnAboutVacuousAssertFalse(x: int) {
   assume x == x + 1;
   assert false;
 }
 
-// CHECK: Results for GetX \(well-formedness\)
+// CHECK: Results for M.GetX \(well-formedness\)
 // CHECK:     Proof dependencies:
 // CHECK:       ProofDependencyLogging.dfy\(449,5\)-\(449,5\): target object is never null
 
@@ -443,13 +443,15 @@ class C {
   var x: int
 }
 
-function GetX(c: C): int
+function {:testEntry} GetX(c: C): int
   reads c
 {
   c.x
 }
 
-method DontWarnAboutUnusedAssumeTrue(x: int) {
+method {:testEntry} DontWarnAboutUnusedAssumeTrue(x: int) {
   assume true;
   assert 1 + x == x + 1;
 }
+
+}
diff --git a/Test/logger/ProofDependencyLogging.dfy_combined.html.expect b/Test/logger/ProofDependencyLogging.dfy_combined.html.expect
new file mode 100644
index 00000000000..8df98da2bd9
--- /dev/null
+++ b/Test/logger/ProofDependencyLogging.dfy_combined.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="pc" id="176:12">n > 4</span><span class="na" id="176:17">;
+    assume </span><span class="fc" id="177:12">n > 3</span><span class="na" id="177:17">;
+    assert n </span><span class="fc" id="178:14">></span><span class="na" id="178:15"> 1;
+}
+
+method {:testEntry} ContradictoryAssumeMethod(n: int)
+{
+    assume </span><span class="pc" id="183:12">n > 0</span><span class="na" id="183:17">;
+    assume </span><span class="pc" id="184:12">n < 0</span><span class="na" id="184:17">;
+    assume </span><span class="nc" id="185:12">n == 5</span><span class="na" id="185:18">; // shouldn't be covered
+    assert n </span><span class="nc" id="186:14"><</span><span class="na" id="186:15"> 10; // shouldn't be covered
+}
+
+method {:testEntry} AssumeFalseMethod(n: int)
+{
+    assume </span><span class="nc" id="191:12">n == 1</span><span class="na" id="191:18">5; // shouldn't be covered
+    assume </span><span class="pc" id="192:12">f</span><span class="na" id="192:13">alse;
+    assert n </span><span class="nc" id="193:14"><</span><span class="na" id="193:15"> 10; // shouldn't be covered
+}
+
+// Obvious contradiction in requires clauses.
+function {:testEntry} ObviouslyContradictoryRequiresFunc(x: nat): (r: nat)
+  requires x > 10
+  requires x < 10
+  ensures r < x // only provable vacuously 
+{
+  assert x </span><span class="nc" id="202:12">=</span><span class="na" id="202:13">= 10; // contradicts both requires clauses
+  </span><span class="nc" id="203:3">x - 1</span><span class="na" id="203:8"> // not necessarily a valid nat
+}
+
+method {:testEntry} ObviouslyContradictoryRequiresMethod(x: nat) returns (r: nat)
+  requires x > 10
+  requires x < 10
+  ensures r < x // only provable vacuously
+{
+  assert x </span><span class="nc" id="211:12">=</span><span class="na" id="211:13">= 10; // contradicts both requires clauses
+  </span><span class="nc" id="212:3">return x - 1;</span><span class="na" id="212:16"> // not necessarily a valid nat
+</span><span class="nc" id="213:1">}
+
+</span><span class="na" id="215:1">// Obvious redundancy in requires clauses.
+function {:testEntry} ObviouslyRedundantRequiresFunc(x: nat): (r: nat)
+  requires x < 10
+  requires x < 100 // implied by previous requires clause
+  ensures r < 11 // should cause body and first requires clause to be covered
+{
+  </span><span class="fc" id="221:3">x + 1
+</span><span class="na" id="222:1">}
+
+method {:testEntry} ObviouslyRedundantRequiresMethod(x: nat) returns (r: nat)
+  requires x < 10
+  requires x < 100 // implied by previous requires clause
+  ensures r < 11 // should cause body and first requires clause to be covered
+{
+  </span><span class="fc" id="229:3">return x + 1;
+</span><span class="pc" id="230:1">}
+
+</span><span class="na" id="232:1">// Obviously unnecessary requires clauses.
+function {:testEntry} ObviouslyUnnecessaryRequiresFunc(x: nat): (r: nat)
+  requires x < 10 // 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="pc" id="237:19">x + 2</span><span class="na" id="237:24"> else </span><span class="pc" id="237:30">x + 1
+</span><span class="na" id="238:1">}
+
+method {:testEntry} ObviouslyUnnecessaryRequiresMethod(x: nat) returns (r: nat)
+  requires x < 10 // 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="244:16">return x + 2;</span><span class="na" id="244:29"> } else { </span><span class="pc" id="244:39">return x + 1;</span><span class="na" id="244:52"> }
+</span><span class="pc" 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 </span><span class="fc" id="252:7">a</span><span class="na" id="252:8"> := </span><span class="fc" id="252:12">x + 1</span><span class="na" id="252:17">; // constrained by ensures clause
+  var </span><span class="pc" id="253:7">b</span><span class="na" id="253:8"> := </span><span class="pc" 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 </span><span class="fc" id="262:9">:= x + 1;</span><span class="na" id="262:18"> // constrained by ensures clause
+  var b </span><span class="pc" id="263:9">:= x - 1;</span><span class="na" id="263:18"> // not constrained by ensures clause
+  return
+    (a,
+</span><span class="fc" id="266:1">     b);
+</span><span class="pc" id="267:1">}
+
+</span><span class="na" id="269:1">// Partial redundancy in requires clauses.
+function {:testEntry} PartiallyRedundantRequiresFunc(x: nat): (r: nat)
+  requires x < 100 && x < 10 // LHS implied by RHS
+  ensures r < 11 // should cause body and RHS clause to be covered
+{
+  </span><span class="fc" id="274:3">x + 1
+</span><span class="na" id="275:1">}
+
+// Partly unnecessary requires clause.
+function {:testEntry} PartiallyUnnecessaryRequiresFunc(x: int): (r: nat)
+  requires x < 10 && 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="pc" id="282:19">x - 1</span><span class="na" id="282:24"> else </span><span class="pc" id="282:30">x + 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 x > 10
+  requires x < 12
+  requires x == 11 // implied by the previous two, but neither individually
+  ensures r == 11
+{
+  </span><span class="fc" id="294:3">x
+</span><span class="na" id="295:1">}
+
+method {:testEntry} MultiPartRedundantRequiresMethod(x: int) returns (r: int)
+  requires x > 10
+  requires x < 12
+  requires x == 11 // implied by the previous two, but neither individually
+  ensures r == 11
+{
+  </span><span class="pc" id="303:3">return 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 y != 11 // contradicts the previous two
+  ensures r == 11 // provable from first two preconditions, but shouldn't be covered
+{
+  </span><span class="fc" id="315:3">x
+</span><span class="na" id="316:1">}
+
+method {:testEntry} MultiPartContradictoryRequiresMethod(x: int, y: int) returns (r: int)
+  requires x > 10
+  requires x < 12
+  requires y != 11 // contradicts the previous two
+  ensures r == 11 // provable from first two preconditions, but shouldn't be covered
+{
+  </span><span class="pc" id="324:3">return x;
+}
+
+</span><span class="na" id="327:1">function {:testEntry} ContradictoryEnsuresClauseFunc(x: int): (r: int)
+  requires x > 1
+  ensures  r > x && r < 0
+
+method {:testEntry} ContradictoryEnsuresClauseMethod(x: int) returns (r: int)
+  requires x > 1
+  ensures  r > x && r < 0
+
+// Call function that has contradictory ensures clauses.
+function {:testEntry} CallContradictoryFunctionFunc(x: int): (r: int)
+  requires x > 1
+  ensures r < 0
+{
+  // TODO: Dafny doesn't generate sufficient Boogie code to make the contradiction detectable
+  </span><span class="pc" id="341:3">ContradictoryEnsuresClauseFunc(x) - 1
+</span><span class="na" id="342:1">}
+
+method {:testEntry} CallContradictoryMethodMethod(x: int) returns (r: int)
+  requires x > 1
+  ensures r < 0
+{
+  var y </span><span class="nc" id="348:9">:= ContradictoryEnsuresClauseMethod(x);
+</span><span class="na" id="349:1">  </span><span class="nc" id="349:3">return y - 1;
+}
+
+</span><span class="na" id="352:1">// False antecedent requires clause
+method {:testEntry} FalseAntecedentRequiresClauseMethod(x: int) returns (r: int)
+  requires x*x < 0 ==> x == x + 1
+  ensures r > x
+{
+  </span><span class="fc" id="357:3">return x + 1;
+</span><span class="pc" id="358:1">}
+
+</span><span class="na" id="360:1">// False antecedent assert statement.
+method {:testEntry} FalseAntecedentAssertStatementMethod(x: int) {
+  var y </span><span class="fc" id="362:9">:= x*x;
+</span><span class="na" id="363:1">  assert </span><span class="pc" id="363:10">y < 0 ==> x < 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
+{
+  </span><span class="fc" id="370:3">return x*x;
+</span><span class="pc" 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
+  then </span><span class="nc" id="378:8">x - 1</span><span class="na" id="378:13"> // unreachable
+  else </span><span class="fc" id="379:8">x + 1
+</span><span class="na" id="380:1">}
+
+method {:testEntry} ObviouslyUnreachableIfStatementBranchMethod(x: int) returns (r:int)
+  requires x > 0
+  ensures r > 0
+{
+  if x < 0 {
+    </span><span class="nc" id="387:5">return x - 1;</span><span class="na" id="387:18"> // unreachable
+  } else {
+    </span><span class="fc" id="389:5">return x + 1;
+</span><span class="na" id="390:1">  }
+</span><span class="pc" 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 {
+    case A => </span><span class="nc" id="400:15">1</span><span class="na" id="400:16"> // unreachable
+    case B => </span><span class="fc" id="401:15">2
+</span><span class="na" id="402:1">  }
+}
+
+method {:testEntry} ObviouslyUnreachableMatchStatementCaseMethod(t: T) returns (r:int)
+  requires t != A
+  ensures r > 1 // alt: r > 0
+{
+  match t {
+    case A => </span><span class="nc" id="410:15">return 1;</span><span class="na" id="410:24"> // unreachable
+    case B => </span><span class="fc" id="411:15">return 2;
+</span><span class="na" id="412:1">  }
+</span><span class="pc" 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? {
+      </span><span class="fc" id="420:7">return 2;
+</span><span class="na" id="421:1">    }
+
+    </span><span class="nc" id="423:5">return 1;</span><span class="na" id="423:14"> // unreachable
+  </span><span class="pc" id="424:3">}
+
+</span><span class="na" id="426:1">method {:testEntry} CalcStatementWithSideConditions(x: int) {
+  calc == {
+    x / 2;
+    (x*2) / 4;
+  }
+}
+
+method {:testEntry} DontWarnAboutVacuousAssertFalse(x: int) {
+  assume </span><span class="pc" id="434:10">x == x + 1</span><span class="na" id="434:20">;
+  assert </span><span class="nc" id="435:10">f</span><span class="na" id="435:11">alse;
+}
+
+// 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="pc" id="449:3">c.x
+</span><span class="na" id="450:1">}
+
+method {:testEntry} DontWarnAboutUnusedAssumeTrue(x: int) {
+  assume </span><span class="pc" id="453:10">t</span><span class="na" id="453:11">rue;
+  assert 1 + x </span><span class="fc" id="454:16">=</span><span class="na" id="454:17">= 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/ProofDependencyLogging.dfy_tests_expected.html.expect b/Test/logger/ProofDependencyLogging.dfy_tests_expected.html.expect
new file mode 100644
index 00000000000..e3a4c32f06a
--- /dev/null
+++ b/Test/logger/ProofDependencyLogging.dfy_tests_expected.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, Expected Test Coverage</title>
+</head>
+<body onload="window['PR_TAB_WIDTH']=4">
+<div class="menu" id="menu">
+    <a href="./index_tests_expected.html">Index</a>
+    
+</div>
+<h1>ProofDependencyLogging.dfy, Expected Test Coverage</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)
+</span><span class="fc" id="174:1">{
+</span><span class="na" id="175:1">    // either one or the other assumption shouldn't be covered
+</span><span class="fc" id="176:1">    assume n > 4;
+    assume n > 3;
+    assert n > 1;
+}
+
+</span><span class="na" id="181: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 r < x // 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 r < x // 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.
+</span><span class="fc" id="216:1">function {:testEntry} ObviouslyRedundantRequiresFunc(x: nat): (r: nat)
+</span><span class="na" id="217:1">  requires x < 10
+  requires x < 100 // implied by previous requires clause
+  ensures r < 11 // should cause body and first requires clause to be covered
+{
+</span><span class="fc" id="221:1">  x + 1
+}
+
+</span><span class="na" id="224:1">method {:testEntry} ObviouslyRedundantRequiresMethod(x: nat) returns (r: nat)
+  requires x < 10
+  requires x < 100 // implied by previous requires clause
+  ensures r < 11 // should cause body and first requires clause to be covered
+</span><span class="fc" id="228:1">{
+  return x + 1;
+}
+
+</span><span class="na" id="232:1">// Obviously unnecessary requires clauses.
+</span><span class="fc" id="233:1">function {:testEntry} ObviouslyUnnecessaryRequiresFunc(x: nat): (r: nat)
+</span><span class="na" id="234:1">  requires x < 10 // not required for the proof
+{
+  // cause at least a little proof work to be necessary, for nat bounds
+</span><span class="fc" id="237:1">  if (x > 5) then x + 2 else x + 1
+}
+
+</span><span class="na" id="240:1">method {:testEntry} ObviouslyUnnecessaryRequiresMethod(x: nat) returns (r: nat)
+  requires x < 10 // not required for the proof
+</span><span class="fc" id="242:1">{
+</span><span class="na" id="243:1">  // cause at least a little proof work to be necessary, for nat bounds
+</span><span class="fc" id="244:1">  if (x > 5) { return x + 2; } else { return x + 1; }
+}
+
+</span><span class="na" id="247:1">// Code obviously not constrained by ensures clause.
+</span><span class="fc" id="248:1">function {:testEntry} ObviouslyUnconstrainedCodeFunc(x: int): (r: (int, int))
+</span><span class="na" id="249:1">  requires x > 10
+  ensures r.0 > 10
+{
+</span><span class="fc" id="252:1">  var a := x + 1; // constrained by ensures clause
+  var b := x - 1; // not constrained by ensures clause 
+</span><span class="na" id="254:1">  (a,
+</span><span class="fc" id="255:1">   b)
+}
+
+</span><span class="na" id="258:1">method {:testEntry} ObviouslyUnconstrainedCodeMethod(x: int) returns (r: (int, int))
+  requires x > 10
+  ensures r.0 > 10
+</span><span class="fc" id="261:1">{
+  var a := x + 1; // constrained by ensures clause
+  var b := x - 1; // not constrained by ensures clause
+</span><span class="na" id="264:1">  return
+    (a,
+</span><span class="fc" id="266:1">     b);
+}
+
+</span><span class="na" id="269:1">// Partial redundancy in requires clauses.
+</span><span class="fc" id="270:1">function {:testEntry} PartiallyRedundantRequiresFunc(x: nat): (r: nat)
+</span><span class="na" id="271:1">  requires x < 100 && x < 10 // LHS implied by RHS
+  ensures r < 11 // should cause body and RHS clause to be covered
+{
+</span><span class="fc" id="274:1">  x + 1
+}
+
+</span><span class="na" id="277:1">// Partly unnecessary requires clause.
+</span><span class="fc" id="278:1">function {:testEntry} PartiallyUnnecessaryRequiresFunc(x: int): (r: nat)
+</span><span class="na" id="279:1">  requires x < 10 && x > 0 // RHS required for proof, but not LHS
+{
+  // cause at least a little proof work to be necessary, for nat bounds
+</span><span class="fc" id="282:1">  if (x > 5) then x - 1 else x + 1
+}
+
+
+</span><span class="na" id="286: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.
+</span><span class="fc" id="288:1">function {:testEntry} MultiPartRedundantRequiresFunc(x: int): (r: int)
+</span><span class="na" id="289:1">  requires x > 10
+  requires x < 12
+  requires x == 11 // implied by the previous two, but neither individually
+  ensures r == 11
+{
+</span><span class="fc" id="294:1">  x
+}
+
+</span><span class="na" id="297:1">method {:testEntry} MultiPartRedundantRequiresMethod(x: int) returns (r: int)
+  requires x > 10
+  requires x < 12
+  requires x == 11 // implied by the previous two, but neither individually
+  ensures r == 11
+</span><span class="fc" id="302:1">{
+  return 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).
+</span><span class="fc" id="309:1">function {:testEntry} MultiPartContradictoryRequiresFunc(x: int, y: int): (r: int)
+</span><span class="na" id="310:1">  requires x > 10
+  requires x < 12
+  requires y != 11 // contradicts the previous two
+  ensures r == 11 // provable from first two preconditions, but shouldn't be covered
+{
+</span><span class="fc" id="315:1">  x
+}
+
+</span><span class="na" id="318:1">method {:testEntry} MultiPartContradictoryRequiresMethod(x: int, y: int) returns (r: int)
+  requires x > 10
+  requires x < 12
+  requires y != 11 // contradicts the previous two
+  ensures r == 11 // provable from first two preconditions, but shouldn't be covered
+</span><span class="fc" id="323:1">{
+  return x;
+}
+
+</span><span class="na" id="327:1">function {:testEntry} ContradictoryEnsuresClauseFunc(x: int): (r: int)
+  requires x > 1
+  ensures  r > x && r < 0
+
+method {:testEntry} ContradictoryEnsuresClauseMethod(x: int) returns (r: int)
+  requires x > 1
+  ensures  r > x && r < 0
+
+// 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 r < 0
+</span><span class="nc" id="347:1">{
+  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 x*x < 0 ==> x == x + 1
+  ensures r > x
+</span><span class="fc" id="356:1">{
+  return x + 1;
+}
+
+</span><span class="na" id="360:1">// False antecedent assert statement.
+</span><span class="fc" id="361:1">method {:testEntry} FalseAntecedentAssertStatementMethod(x: int) {
+  var y := x*x;
+  assert y < 0 ==> x < 0;
+}
+
+</span><span class="na" id="366:1">// False antecedent ensures clause.
+method {:testEntry} FalseAntecedentEnsuresClauseMethod(x: int) returns (r: int)
+  ensures r < 0 ==> x < 0
+</span><span class="fc" id="369:1">{
+  return x*x;
+}
+
+function {:testEntry} ObviouslyUnreachableIfExpressionBranchFunc(x: int): (r:int)
+</span><span class="na" id="374:1">  requires x > 0
+  ensures r > 0
+{
+  if x < 0
+</span><span class="nc" id="378:1">  then x - 1 // unreachable
+</span><span class="fc" id="379:1">  else x + 1
+}
+
+</span><span class="na" id="382:1">method {:testEntry} ObviouslyUnreachableIfStatementBranchMethod(x: int) returns (r:int)
+  requires x > 0
+  ensures r > 0
+</span><span class="fc" id="385:1">{
+</span><span class="na" id="386:1">  if x < 0 {
+</span><span class="nc" id="387:1">    return x - 1; // unreachable
+</span><span class="na" id="388:1">  } else {
+</span><span class="fc" id="389:1">    return x + 1;
+</span><span class="na" id="390:1">  }
+</span><span class="fc" id="391:1">}
+
+</span><span class="na" id="393:1">datatype T = A | B
+
+</span><span class="fc" id="395:1">function {:testEntry} ObviouslyUnreachableMatchExpressionCaseFunction(t: T): (r:int)
+</span><span class="na" id="396:1">  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="fc" id="401:1">    case B => 2
+  }
+}
+
+</span><span class="na" id="405:1">method {:testEntry} ObviouslyUnreachableMatchStatementCaseMethod(t: T) returns (r:int)
+  requires t != A
+  ensures r > 1 // alt: r > 0
+</span><span class="fc" id="408:1">{
+</span><span class="na" id="409:1">  match t {
+</span><span class="nc" id="410:1">    case A => return 1; // unreachable
+</span><span class="fc" id="411:1">    case B => return 2;
+</span><span class="na" id="412:1">  }
+</span><span class="fc" 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
+</span><span class="fc" id="418:1">  {
+</span><span class="na" id="419:1">    if !t.A? {
+</span><span class="fc" id="420:1">      return 2;
+</span><span class="na" id="421:1">    }
+
+</span><span class="nc" id="423:1">    return 1; // unreachable
+</span><span class="fc" id="424:1">  }
+
+method {:testEntry} CalcStatementWithSideConditions(x: int) {
+</span><span class="na" id="427:1">  calc == {
+    x / 2;
+    (x*2) / 4;
+  }
+</span><span class="fc" id="431:1">}
+
+</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
+}
+
+</span><span class="fc" id="446:1">function {:testEntry} GetX(c: C): int
+</span><span class="na" id="447:1">  reads c
+{
+</span><span class="fc" id="449:1">  c.x
+}
+
+method {:testEntry} DontWarnAboutUnusedAssumeTrue(x: int) {
+  assume true;
+  assert 1 + x == x + 1;
+}
+
+</span><span class="na" id="457: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/ProofDependencyLogging.dfy_verification.html.expect b/Test/logger/ProofDependencyLogging.dfy_verification.html.expect
index 0e90f762f4e..d083f88ba53 100644
--- a/Test/logger/ProofDependencyLogging.dfy_verification.html.expect
+++ b/Test/logger/ProofDependencyLogging.dfy_verification.html.expect
@@ -15,33 +15,33 @@
 <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"
+<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 RedundantAssumeMethod \(correctness\)
+// 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 ContradictoryAssumeMethod \(correctness\)
+// 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 AssumeFalseMethod \(correctness\)
+// CHECK: Results for M.AssumeFalseMethod \(correctness\)
 // CHECK:     Proof dependencies:
 // CHECK:       ProofDependencyLogging.dfy\(192,12\)-\(192,12\): assume statement
 //
-// CHECK: Results for ObviouslyContradictoryRequiresFunc \(well-formedness\)
+// 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 ObviouslyContradictoryRequiresMethod \(correctness\)
+// 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 ObviouslyRedundantRequiresFunc \(well-formedness\)
+// 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
@@ -49,24 +49,24 @@
 // 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: 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 ObviouslyUnnecessaryRequiresFunc \(well-formedness\)
+// 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 ObviouslyUnnecessaryRequiresMethod \(correctness\)
+// 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 ObviouslyUnconstrainedCodeFunc \(well-formedness\)
+// 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
@@ -75,14 +75,14 @@
 // 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: 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 PartiallyRedundantRequiresFunc \(well-formedness\)
+// 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
@@ -90,25 +90,25 @@
 // 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: 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 MultiPartRedundantRequiresFunc \(well-formedness\)
+// 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 MultiPartRedundantRequiresMethod \(correctness\)
+// 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 MultiPartContradictoryRequiresFunc \(well-formedness\)
+// 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
@@ -116,13 +116,13 @@
 // 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: 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 CallContradictoryFunctionFunc \(well-formedness\)
+// 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
@@ -130,41 +130,41 @@
 // 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: 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 FalseAntecedentRequiresClauseMethod \(correctness\)
+// CHECK: Results for M.FalseAntecedentRequiresClauseMethod \(correctness\)
 // CHECK:     Proof dependencies:
 // CHECK:       ProofDependencyLogging.dfy\(357,3\)-\(357,15\): assignment \(or return\)
 //
-// CHECK: Results for FalseAntecedentAssertStatementMethod \(correctness\)
+// 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 FalseAntecedentEnsuresClauseMethod \(correctness\)
+// 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 ObviouslyUnreachableIfExpressionBranchFunc \(well-formedness\)
+// 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 ObviouslyUnreachableIfStatementBranchMethod \(correctness\)
+// 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 ObviouslyUnreachableMatchExpressionCaseFunction \(well-formedness\)
+// CHECK: Results for M.ObviouslyUnreachableMatchExpressionCaseFunction \(well-formedness\)
 //
 // CHECK:     Proof dependencies:
 // CHECK:       ProofDependencyLogging.dfy\(395,1\)-\(403,1\): function definition for ObviouslyUnreachableMatchExpressionCaseFunction
@@ -172,287 +172,287 @@
 // 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: 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 ObviouslyUnreachableReturnStatementMethod \(correctness\)
+// 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 RedundantAssumeMethod(n: int)
+method {:testEntry} 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;
+    assume </span><span class="nc" id="176:12">n > 4</span><span class="na" id="176:17">;
+    assume </span><span class="fc" id="177:12">n > 3</span><span class="na" id="177:17">;
+    assert n </span><span class="fc" id="178:14">></span><span class="na" id="178:15"> 1;
 }
 
-method ContradictoryAssumeMethod(n: int)
+method {:testEntry} 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
+    assume </span><span class="fc" id="183:12">n > 0</span><span class="na" id="183:17">;
+    assume </span><span class="fc" id="184:12">n < 0</span><span class="na" id="184:17">;
+    assume </span><span class="nc" id="185:12">n == 5</span><span class="na" id="185:18">; // shouldn't be covered
+    assert n </span><span class="nc" id="186:14"><</span><span class="na" id="186:15"> 10; // shouldn't be covered
 }
 
-method AssumeFalseMethod(n: int)
+method {:testEntry} 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
+    assume </span><span class="nc" id="191:12">n == 1</span><span class="na" id="191:18">5; // shouldn't be covered
+    assume </span><span class="fc" id="192:12">f</span><span class="na" id="192:13">alse;
+    assert n </span><span class="nc" id="193:14"><</span><span class="na" id="193:15"> 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 
+function {:testEntry} ObviouslyContradictoryRequiresFunc(x: nat): (r: nat)
+  requires </span><span class="fc" id="198:12">x > 1</span><span class="na" id="198:17">0
+  requires </span><span class="fc" id="199:12">x < 1</span><span class="na" id="199:17">0
+  ensures </span><span class="nc" id="200:11">r < x</span><span class="na" id="200:16"> // 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
+  assert x </span><span class="nc" id="202:12">=</span><span class="na" id="202:13">= 10; // contradicts both requires clauses
+  </span><span class="nc" id="203:3">x - 1</span><span class="na" id="203:8"> // 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
+method {:testEntry} ObviouslyContradictoryRequiresMethod(x: nat) returns (r: nat)
+  requires </span><span class="pc" id="207:12">x > 1</span><span class="na" id="207:17">0
+  requires </span><span class="pc" id="208:12">x < 1</span><span class="na" id="208:17">0
+  ensures </span><span class="nc" id="209:11">r < x</span><span class="na" id="209:16"> // 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
+  assert x </span><span class="nc" id="211:12">=</span><span class="na" id="211:13">= 10; // contradicts both requires clauses
+  </span><span class="nc" id="212:3">return x - 1;</span><span class="na" id="212:16"> // not necessarily a valid nat
+</span><span class="nc" id="213:1">}
+
+</span><span class="na" id="215:1">// Obvious redundancy in requires clauses.
+function {:testEntry} ObviouslyRedundantRequiresFunc(x: nat): (r: nat)
+  requires </span><span class="fc" id="217:12">x < 1</span><span class="na" id="217:17">0
+  requires </span><span class="nc" id="218:12">x < 1</span><span class="na" id="218:17">00 // implied by previous requires clause
+  ensures </span><span class="pc" id="219:11">r < 1</span><span class="na" id="219:16">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">
-}
+  </span><span class="fc" id="221:3">x + 1
+</span><span class="na" id="222:1">}
 
-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
+method {:testEntry} ObviouslyRedundantRequiresMethod(x: nat) returns (r: nat)
+  requires </span><span class="pc" id="225:12">x < 1</span><span class="na" id="225:17">0
+  requires </span><span class="nc" id="226:12">x < 1</span><span class="na" id="226:17">00 // implied by previous requires clause
+  ensures </span><span class="pc" id="227:11">r < 1</span><span class="na" id="227:16">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">
+  </span><span class="fc" id="229:3">return x + 1;
+</span><span class="nc" id="230:1">}
 
-// 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
+</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="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">
-}
+  if (x > 5) then </span><span class="nc" id="237:19">x </span><span class="pc" 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="pc" id="237:32">+</span><span class="nc" id="237:33"> 1
+</span><span class="na" id="238:1">}
 
-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
+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) { </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">
+  if (x > 5) { </span><span class="pc" id="244:16">r</span><span class="nc" id="244:17">eturn x </span><span class="pc" id="244:25">+</span><span class="nc" id="244:26"> 2;</span><span class="na" id="244:29"> } else { </span><span class="pc" id="244:39">r</span><span class="nc" id="244:40">eturn x </span><span class="pc" 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">}
 
-// 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
+</span><span class="na" id="247:1">// Code obviously not constrained by ensures clause.
+function {:testEntry} ObviouslyUnconstrainedCodeFunc(x: int): (r: (int, int))
+  requires </span><span class="fc" id="249:12">x > 1</span><span class="na" id="249:17">0
+  ensures </span><span class="pc" id="250:11">r.0 > 1</span><span class="na" id="250:18">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,
+  var </span><span class="fc" id="252:7">a</span><span class="na" id="252:8"> := </span><span class="fc" id="252:12">x + 1</span><span class="na" id="252:17">; // 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 
+  </span><span class="fc" id="254:3">(</span><span class="na" id="254:4">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
+method {:testEntry} ObviouslyUnconstrainedCodeMethod(x: int) returns (r: (int, int))
+  requires </span><span class="pc" id="259:12">x > 1</span><span class="na" id="259:17">0
+  ensures </span><span class="pc" id="260:11">r.0 > 1</span><span class="na" id="260:18">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
+  var a </span><span class="fc" id="262:9">:= x + 1;</span><span class="na" id="262:18"> // 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
+  </span><span class="fc" id="264:3">return
     (a,
-     b);</span><span class="none" id="pos13584">
-</span><span class="nc" id="pos13585">}</span><span class="none" id="pos13586">
+     b);
+</span><span class="nc" id="267:1">}
 
-// 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="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 && </span><span class="fc" id="271:23">x < 1</span><span class="na" id="271:28">0 // LHS implied by RHS
+  ensures </span><span class="pc" id="272:11">r < 1</span><span class="na" id="272:16">1 // should cause body and RHS clause to be covered
 {
-  </span><span class="fc" id="pos13811">x + 1</span><span class="none" id="pos13816">
-}
+  </span><span class="fc" id="274:3">x + 1
+</span><span class="na" id="275:1">}
 
 // 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
+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 && </span><span class="fc" id="279:22">x > 0</span><span class="na" id="279:27"> // 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">
-}
+  if (x > 5) then </span><span class="nc" id="282:19">x </span><span class="pc" 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="pc" 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 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
+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 </span><span class="fc" id="291:12">x == 1</span><span class="na" id="291:18">1 // implied by the previous two, but neither individually
+  ensures </span><span class="pc" id="292:11">r == 1</span><span class="na" id="292:17">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="fc" id="294:3">x
+</span><span class="na" id="295:1">}
+
+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 </span><span class="pc" id="300:12">x == 1</span><span class="na" id="300:18">1 // implied by the previous two, but neither individually
+  ensures </span><span class="pc" id="301:11">r == 1</span><span class="na" id="301:17">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">
+  </span><span class="pc" id="303:3">r</span><span class="nc" id="303:4">eturn x;
+}
 
-// Contradiction between three different requires clauses, with at least one of
+</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 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
+function {:testEntry} MultiPartContradictoryRequiresFunc(x: int, y: int): (r: int)
+  requires </span><span class="fc" id="310:12">x > 1</span><span class="na" id="310:17">0
+  requires </span><span class="fc" id="311:12">x < 1</span><span class="na" id="311:17">2
+  requires </span><span class="nc" id="312:12">y != 1</span><span class="na" id="312:18">1 // contradicts the previous two
+  ensures </span><span class="pc" id="313:11">r == 1</span><span class="na" id="313:17">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="fc" id="315:3">x
+</span><span class="na" id="316:1">}
+
+method {:testEntry} MultiPartContradictoryRequiresMethod(x: int, y: int) returns (r: int)
+  requires </span><span class="pc" id="319:12">x > 1</span><span class="na" id="319:17">0
+  requires </span><span class="pc" id="320:12">x < 1</span><span class="na" id="320:17">2
+  requires </span><span class="nc" id="321:12">y != 1</span><span class="na" id="321:18">1 // contradicts the previous two
+  ensures </span><span class="pc" id="322:11">r == 1</span><span class="na" id="322:17">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">
+  </span><span class="pc" id="324:3">r</span><span class="nc" id="324:4">eturn x;
+}
 
-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">
+</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
 
-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">
+</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
 
-// 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">
-{
+</span><span class="na" id="335:1">// Call function that has contradictory ensures clauses.
+function {:testEntry} CallContradictoryFunctionFunc(x: int): (r: int)
+  requires </span><span class="fc" id="337:12">x > 1
+</span><span class="na" id="338:1">  ensures </span><span class="pc" id="338:11">r < 0
+</span><span class="na" id="339:1">{
   // 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">
+  </span><span class="fc" id="341:3">ContradictoryEnsuresClauseFunc(x) - 1
+</span><span class="na" id="342:1">}
+
+method {:testEntry} CallContradictoryMethodMethod(x: int) returns (r: int)
+  requires </span><span class="pc" id="345:12">x > 1
+</span><span class="na" id="346:1">  ensures </span><span class="nc" id="346:11">r < 0
+</span><span class="na" id="347:1">{
+  var y </span><span class="nc" id="348:9">:= ContradictoryEnsuresClauseMethod(x);
+</span><span class="na" id="349:1">  </span><span class="nc" id="349:3">return y - 1;
 }
 
-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">;
+</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 </span><span class="pc" id="355:11">r > x
+</span><span class="na" id="356:1">{
+  </span><span class="fc" id="357:3">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 </span><span class="fc" id="362:9">:= x*x;
+</span><span class="na" id="363:1">  assert </span><span class="nc" id="363:10">y < 0 ==> x </span><span class="pc" id="363:22"><</span><span class="nc" id="363:23"> 0</span><span class="na" id="363:25">;
 }
 
 // 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">
-{
+method {:testEntry} FalseAntecedentEnsuresClauseMethod(x: int) returns (r: int)
+  ensures </span><span class="pc" id="368:11">r < 0 ==> x < 0
+</span><span class="na" id="369:1">{
+  </span><span class="fc" id="370:3">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 </span><span class="fc" id="374:12">x > 0
+</span><span class="na" id="375:1">  ensures </span><span class="pc" id="375:11">r > 0
+</span><span class="na" id="376:1">{
   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">
-{
+  then </span><span class="nc" id="378:8">x - 1</span><span class="na" id="378:13"> // unreachable
+  else </span><span class="fc" id="379:8">x + 1
+</span><span class="na" id="380:1">}
+
+method {:testEntry} ObviouslyUnreachableIfStatementBranchMethod(x: int) returns (r:int)
+  requires </span><span class="pc" id="383:12">x > 0
+</span><span class="na" id="384:1">  ensures </span><span class="pc" id="384:11">r > 0
+</span><span class="na" id="385:1">{
   if x < 0 {
-    </span><span class="nc" id="pos16742">return x - 1;</span><span class="none" id="pos16755"> // unreachable
+    </span><span class="nc" id="387:5">return x - 1;</span><span class="na" id="387:18"> // 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">
+    </span><span class="fc" id="389:5">return x + 1;
+</span><span class="na" id="390:1">  }
+</span><span class="nc" id="391:1">}
 
-datatype T = A | B
+</span><span class="na" id="393:1">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
+function {:testEntry} ObviouslyUnreachableMatchExpressionCaseFunction(t: T): (r:int)
+  requires </span><span class="fc" id="396:12">t != A
+</span><span class="na" id="397:1">  ensures </span><span class="pc" id="397:11">r > 1</span><span class="na" id="397:16"> // 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">
-  }
+    case A => </span><span class="nc" id="400:15">1</span><span class="na" id="400:16"> // unreachable
+    case B => </span><span class="fc" id="401:15">2
+</span><span class="na" id="402:1">  }
 }
 
-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
+method {:testEntry} ObviouslyUnreachableMatchStatementCaseMethod(t: T) returns (r:int)
+  requires </span><span class="pc" id="406:12">t != A
+</span><span class="na" id="407:1">  ensures </span><span class="pc" id="407:11">r > 1</span><span class="na" id="407:16"> // 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
+    case A => </span><span class="nc" id="410:15">return 1;</span><span class="na" id="410:24"> // unreachable
+    case B => </span><span class="fc" id="411:15">return 2;
+</span><span class="na" id="412:1">  }
+</span><span class="nc" id="413:1">}
+
+</span><span class="na" id="415:1">method {:testEntry} ObviouslyUnreachableReturnStatementMethod(t: T) returns (r:int)
+  requires </span><span class="pc" id="416:12">t != A
+</span><span class="na" id="417:1">    ensures </span><span class="pc" id="417:13">r > 1</span><span class="na" id="417:18"> // alt: r > 0
   {
     if !t.A? {
-      </span><span class="fc" id="pos17367">return 2;</span><span class="none" id="pos17376">
-    }
+      </span><span class="fc" id="420:7">return 2;
+</span><span class="na" id="421:1">    }
 
-    </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">
+    </span><span class="nc" id="423:5">return 1;</span><span class="na" id="423:14"> // unreachable
+  </span><span class="nc" id="424:3">}
 
-method CalcStatementWithSideConditions(x: int) {
+</span><span class="na" id="426:1">method {:testEntry} 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">;
+    </span><span class="nc" id="428:5">x </span><span class="pc" id="428:7">/</span><span class="nc" id="428:8"> 2;
+    (x*2) </span><span class="pc" id="429:11">/</span><span class="nc" id="429:12"> 4</span><span class="na" id="429:14">;
   }
 }
 
-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;
+method {:testEntry} DontWarnAboutVacuousAssertFalse(x: int) {
+  assume </span><span class="fc" id="434:10">x == x + 1</span><span class="na" id="434:20">;
+  assert </span><span class="nc" id="435:10">f</span><span class="na" id="435:11">alse;
 }
 
-// CHECK: Results for GetX \(well-formedness\)
+// CHECK: Results for M.GetX \(well-formedness\)
 // CHECK:     Proof dependencies:
 // CHECK:       ProofDependencyLogging.dfy\(449,5\)-\(449,5\): target object is never null
 
@@ -460,16 +460,19 @@ class C {
   var x: int
 }
 
-function GetX(c: C): int
+function {:testEntry} 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">
+  </span><span class="nc" id="449:3">c.</span><span class="pc" id="449:5">x
+</span><span class="na" id="450:1">}
+
+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 </span><span class="fc" id="454:16">=</span><span class="na" id="454:17">= x + 1;
 }
 
-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">
diff --git a/Test/logger/VerificationCoverageReport.dfy b/Test/logger/VerificationCoverageReport.dfy
deleted file mode 100644
index 820bd64666a..00000000000
--- a/Test/logger/VerificationCoverageReport.dfy
+++ /dev/null
@@ -1,8 +0,0 @@
-// NONUNIFORM: Not a compiler test
-// UNSUPPORTED: windows
-// 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"