From 7e04b421fd9789f8a67db66b87d5d829f6fb178e Mon Sep 17 00:00:00 2001
From: Aaron Tomb <aarotomb@amazon.com>
Date: Mon, 8 Jan 2024 11:32:16 -0800
Subject: [PATCH 1/9] First cut at JSON verification logger

---
 Source/DafnyCore/DafnyOptions.cs              |   2 +-
 .../Verifier/ProofDependencyManager.cs        |   4 +
 Source/DafnyDriver/JsonVerificationLogger.cs  | 106 ++++++++++++++++++
 Source/DafnyDriver/TextLogger.cs              |   6 +-
 .../DafnyDriver/VerificationResultLogger.cs   |   6 +
 .../LitTests/LitTest/logger/JsonLogger.dfy    |  11 ++
 6 files changed, 129 insertions(+), 6 deletions(-)
 create mode 100644 Source/DafnyDriver/JsonVerificationLogger.cs
 create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/JsonLogger.dfy

diff --git a/Source/DafnyCore/DafnyOptions.cs b/Source/DafnyCore/DafnyOptions.cs
index 9307b533c69..9c2f592e14c 100644
--- a/Source/DafnyCore/DafnyOptions.cs
+++ b/Source/DafnyCore/DafnyOptions.cs
@@ -722,7 +722,7 @@ protected bool ParseDafnySpecificOption(string name, Bpl.CommandLineParseState p
 
         case "verificationLogger":
           if (ps.ConfirmArgumentCount(1)) {
-            if (args[ps.i].StartsWith("trx") || args[ps.i].StartsWith("csv") || args[ps.i].StartsWith("text")) {
+            if (args[ps.i].StartsWith("trx") || args[ps.i].StartsWith("csv") || args[ps.i].StartsWith("text") || args[ps.i].StartsWith("json")) {
               VerificationLoggerConfigs.Add(args[ps.i]);
             } else {
               InvalidArgumentError(name, ps);
diff --git a/Source/DafnyCore/Verifier/ProofDependencyManager.cs b/Source/DafnyCore/Verifier/ProofDependencyManager.cs
index 0c8a0fc90b6..4add7f73729 100644
--- a/Source/DafnyCore/Verifier/ProofDependencyManager.cs
+++ b/Source/DafnyCore/Verifier/ProofDependencyManager.cs
@@ -83,5 +83,9 @@ public ProofDependency GetFullIdDependency(TrackedNodeComponent component) {
         throw new ArgumentException($"Malformed dependency ID: {component.SolverLabel}");
       }
     }
+
+    public IEnumerable<ProofDependency> GetOrderedFullDependencies(IEnumerable<TrackedNodeComponent> components) {
+      return components.Select(GetFullIdDependency).OrderBy(dep => (dep.RangeString(), dep.Description));
+    }
   }
 }
\ No newline at end of file
diff --git a/Source/DafnyDriver/JsonVerificationLogger.cs b/Source/DafnyDriver/JsonVerificationLogger.cs
new file mode 100644
index 00000000000..b994e3b58db
--- /dev/null
+++ b/Source/DafnyDriver/JsonVerificationLogger.cs
@@ -0,0 +1,106 @@
+using System;
+using System.Collections.Generic;
+using System.IO;
+using System.Linq;
+using System.Text.Json.Nodes;
+using DafnyCore.Verifier;
+using Microsoft.Boogie;
+using VC;
+
+namespace Microsoft.Dafny;
+
+public class JsonVerificationLogger {
+  private TextWriter tw;
+  private TextWriter outWriter;
+  private ProofDependencyManager depManager;
+
+  public JsonVerificationLogger(ProofDependencyManager depManager, TextWriter outWriter) {
+    this.depManager = depManager;
+    this.outWriter = outWriter;
+  }
+
+  public void Initialize(Dictionary<string, string> parameters) {
+    tw = parameters.TryGetValue("LogFileName", out string filename) ? new StreamWriter(filename) : outWriter;
+  }
+
+  private static JsonNode SerializeAssertion(Microsoft.Boogie.IToken tok, string description) {
+    return new JsonObject {
+      ["filename"] = tok.filename,
+      ["line"] = tok.line,
+      ["col"] = tok.col,
+      ["description"] = description
+    };
+  }
+
+  private JsonNode SerializeProofDependency(ProofDependency dependency) {
+    return new JsonObject {
+      ["startFile"] = dependency.Range.StartToken.Filepath,
+      ["startLine"] = dependency.Range.StartToken.line,
+      ["startCol"] = dependency.Range.StartToken.col,
+      ["endFile"] = dependency.Range.EndToken.Filepath,
+      ["endLine"] = dependency.Range.EndToken.line,
+      ["endCol"] = dependency.Range.EndToken.col,
+      ["description"] = dependency.Description,
+      ["originalText"] = dependency.OriginalString()
+    };
+  }
+
+  private JsonNode SerializeVcResult(IEnumerable<ProofDependency> potentialDependencies, DafnyConsolePrinter.VCResultLogEntry vcResult) {
+    var result = new JsonObject {
+      ["vcNum"] = vcResult.VCNum,
+      ["outcome"] = SerializeOutcome(vcResult.Outcome),
+      ["runTime"] = SerializeTimeSpan(vcResult.RunTime),
+      ["resourceCount"] = vcResult.ResourceCount,
+      ["assertions"] = new JsonArray(vcResult.Asserts.Select(x => SerializeAssertion(x.Tok, x.Description)).ToArray()),
+    };
+    if (potentialDependencies is not null) {
+      var fullDependencies = depManager.GetOrderedFullDependencies(vcResult.CoveredElements);
+      var fullDependencySet = fullDependencies.ToHashSet();
+      var unusedDependencies = potentialDependencies.Where(dep => !fullDependencySet.Contains(dep));
+      result["coveredElements"] = new JsonArray(fullDependencies.Select(SerializeProofDependency).ToArray());
+      result["uncoveredElements"] = new JsonArray(unusedDependencies.Select(SerializeProofDependency).ToArray());
+    }
+    return result;
+  }
+
+  private static JsonNode SerializeTimeSpan(TimeSpan timeSpan) {
+    return timeSpan.ToString();
+  }
+
+  private static JsonNode SerializeOutcome(ProverInterface.Outcome outcome) {
+    return outcome.ToString();
+  }
+  private static JsonNode SerializeOutcome(ConditionGeneration.Outcome outcome) {
+    return outcome.ToString();
+  }
+
+  private JsonNode SerializeVerificationResult(DafnyConsolePrinter.ConsoleLogEntry logEntry) {
+    var (impl, verificationResult) = logEntry;
+    var trackProofDependencies =
+      verificationResult.Outcome == ConditionGeneration.Outcome.Correct &&
+      verificationResult.VCResults.Any(vcResult => vcResult.CoveredElements.Any());
+    var potentialDependencies =
+      trackProofDependencies ? depManager.GetPotentialDependenciesForDefinition(impl.Name) : null;
+    var result = new JsonObject {
+      ["name"] = impl.Name,
+      ["outcome"] = SerializeOutcome(verificationResult.Outcome),
+      ["runTime"] = SerializeTimeSpan(verificationResult.RunTime),
+      ["resourceCount"] = verificationResult.ResourceCount,
+      ["vcResults"] = new JsonArray(verificationResult.VCResults.Select(r => SerializeVcResult(potentialDependencies, r)).ToArray())
+    };
+    if (potentialDependencies is not null) {
+      result["programElements"] = new JsonArray(potentialDependencies.Select(SerializeProofDependency).ToArray());
+    }
+    return result;
+  }
+
+  private JsonObject SerializeVerificationResults(IEnumerable<DafnyConsolePrinter.ConsoleLogEntry> verificationResults) {
+    return new JsonObject {
+      ["verificationResults"] = new JsonArray(verificationResults.Select(SerializeVerificationResult).ToArray())
+    };
+  }
+
+  public void LogResults(IEnumerable<DafnyConsolePrinter.ConsoleLogEntry> verificationResults) {
+    tw.Write(SerializeVerificationResults(verificationResults).ToJsonString());
+  }
+}
\ No newline at end of file
diff --git a/Source/DafnyDriver/TextLogger.cs b/Source/DafnyDriver/TextLogger.cs
index f710257e32b..1aaa2ca4521 100644
--- a/Source/DafnyDriver/TextLogger.cs
+++ b/Source/DafnyDriver/TextLogger.cs
@@ -47,11 +47,7 @@ public void LogResults(IEnumerable<DafnyConsolePrinter.ConsoleLogEntry> verifica
         if (vcResult.CoveredElements.Any() && vcResult.Outcome == ProverInterface.Outcome.Valid) {
           tw.WriteLine("");
           tw.WriteLine("    Proof dependencies:");
-          var fullDependencies =
-            vcResult
-            .CoveredElements
-            .Select(depManager.GetFullIdDependency)
-            .OrderBy(dep => (dep.RangeString(), dep.Description));
+          var fullDependencies = depManager.GetOrderedFullDependencies(vcResult.CoveredElements);
           foreach (var dep in fullDependencies) {
             tw.WriteLine($"      {dep.RangeString()}: {dep.Description}");
           }
diff --git a/Source/DafnyDriver/VerificationResultLogger.cs b/Source/DafnyDriver/VerificationResultLogger.cs
index 35286248ac3..0d8a3d94f16 100644
--- a/Source/DafnyDriver/VerificationResultLogger.cs
+++ b/Source/DafnyDriver/VerificationResultLogger.cs
@@ -59,6 +59,12 @@ public static void RaiseTestLoggerEvents(DafnyOptions options, ProofDependencyMa
         } else if (loggerName == "csv") {
           var csvLogger = new CSVTestLogger(options.OutputWriter);
           csvLogger.Initialize(events, parameters);
+        } else if (loggerName == "json") {
+          // This logger doesn't implement the ITestLogger interface because
+          // it uses information that's tricky to encode in a TestResult.
+          var jsonLogger = new JsonVerificationLogger(depManager, options.OutputWriter);
+          jsonLogger.Initialize(parameters);
+          jsonLogger.LogResults(verificationResults);
         } else if (loggerName == "text") {
           // This logger doesn't implement the ITestLogger interface because
           // it uses information that's tricky to encode in a TestResult.
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/JsonLogger.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/JsonLogger.dfy
new file mode 100644
index 00000000000..c4bb744972b
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/JsonLogger.dfy
@@ -0,0 +1,11 @@
+// RUN: %exits-with 4 %baredafny verify --show-snippets:false --log-format:json --isolate-assertions "%s" > "%t"
+// RUN: %OutputCheck --file-to-check "%t" "%s"
+// CHECK: vcNum.:1,.outcome.:.Valid
+// CHECK: vcNum.:3,.outcome.:.Invalid
+method M(x: int, y: int)
+  requires y > 0
+  requires x > 0
+{
+  var d := x / y;
+  assert(d * y == x); // Should fail
+}

From 97672e24a6e417450984651fc3d3b3bb128087a1 Mon Sep 17 00:00:00 2001
From: Aaron Tomb <aarotomb@amazon.com>
Date: Mon, 8 Jan 2024 11:33:07 -0800
Subject: [PATCH 2/9] Rename TextLogger -> TextVerificationLogger

---
 .../DafnyDriver/{TextLogger.cs => TextVerificationLogger.cs}  | 4 ++--
 Source/DafnyDriver/VerificationResultLogger.cs                | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)
 rename Source/DafnyDriver/{TextLogger.cs => TextVerificationLogger.cs} (95%)

diff --git a/Source/DafnyDriver/TextLogger.cs b/Source/DafnyDriver/TextVerificationLogger.cs
similarity index 95%
rename from Source/DafnyDriver/TextLogger.cs
rename to Source/DafnyDriver/TextVerificationLogger.cs
index 1aaa2ca4521..6839b6008f4 100644
--- a/Source/DafnyDriver/TextLogger.cs
+++ b/Source/DafnyDriver/TextVerificationLogger.cs
@@ -5,12 +5,12 @@
 
 namespace Microsoft.Dafny;
 
-public class TextLogger {
+public class TextVerificationLogger {
   private TextWriter tw;
   private TextWriter outWriter;
   private ProofDependencyManager depManager;
 
-  public TextLogger(ProofDependencyManager depManager, TextWriter outWriter) {
+  public TextVerificationLogger(ProofDependencyManager depManager, TextWriter outWriter) {
     this.depManager = depManager;
     this.outWriter = outWriter;
   }
diff --git a/Source/DafnyDriver/VerificationResultLogger.cs b/Source/DafnyDriver/VerificationResultLogger.cs
index 0d8a3d94f16..ec7e4b0a103 100644
--- a/Source/DafnyDriver/VerificationResultLogger.cs
+++ b/Source/DafnyDriver/VerificationResultLogger.cs
@@ -68,7 +68,7 @@ public static void RaiseTestLoggerEvents(DafnyOptions options, ProofDependencyMa
         } else if (loggerName == "text") {
           // This logger doesn't implement the ITestLogger interface because
           // it uses information that's tricky to encode in a TestResult.
-          var textLogger = new TextLogger(depManager, options.OutputWriter);
+          var textLogger = new TextVerificationLogger(depManager, options.OutputWriter);
           textLogger.Initialize(parameters);
           textLogger.LogResults(verificationResults);
         } else {

From 9cfcb57eb1b27ed9b59aa6f83de941c3f9a371d9 Mon Sep 17 00:00:00 2001
From: Aaron Tomb <aarotomb@amazon.com>
Date: Mon, 8 Jan 2024 11:39:20 -0800
Subject: [PATCH 3/9] Make fields readonly

---
 Source/DafnyDriver/JsonVerificationLogger.cs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Source/DafnyDriver/JsonVerificationLogger.cs b/Source/DafnyDriver/JsonVerificationLogger.cs
index b994e3b58db..b9557a70656 100644
--- a/Source/DafnyDriver/JsonVerificationLogger.cs
+++ b/Source/DafnyDriver/JsonVerificationLogger.cs
@@ -11,8 +11,8 @@ namespace Microsoft.Dafny;
 
 public class JsonVerificationLogger {
   private TextWriter tw;
-  private TextWriter outWriter;
-  private ProofDependencyManager depManager;
+  private readonly TextWriter outWriter;
+  private readonly ProofDependencyManager depManager;
 
   public JsonVerificationLogger(ProofDependencyManager depManager, TextWriter outWriter) {
     this.depManager = depManager;

From 35c22a32518874a437ad44e3c0ca7a862083731d Mon Sep 17 00:00:00 2001
From: Aaron Tomb <aarotomb@amazon.com>
Date: Mon, 8 Jan 2024 12:01:55 -0800
Subject: [PATCH 4/9] Fix test

---
 .../TestFiles/LitTests/LitTest/logger/JsonLogger.dfy           | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/JsonLogger.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/JsonLogger.dfy
index c4bb744972b..1d876681729 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/JsonLogger.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/JsonLogger.dfy
@@ -1,7 +1,6 @@
 // RUN: %exits-with 4 %baredafny verify --show-snippets:false --log-format:json --isolate-assertions "%s" > "%t"
 // RUN: %OutputCheck --file-to-check "%t" "%s"
-// CHECK: vcNum.:1,.outcome.:.Valid
-// CHECK: vcNum.:3,.outcome.:.Invalid
+// CHECK: vcNum.:1,.outcome.:.Valid.*vcNum.:3,.outcome.:.Invalid
 method M(x: int, y: int)
   requires y > 0
   requires x > 0

From 106857ddc997583631d1c10c70c75e85d5b19107 Mon Sep 17 00:00:00 2001
From: Aaron Tomb <aarotomb@amazon.com>
Date: Wed, 10 Jan 2024 08:17:50 -0800
Subject: [PATCH 5/9] Apply suggestion from @keyboardDrummer

---
 Source/DafnyCore/Verifier/ProofDependencyManager.cs | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/Source/DafnyCore/Verifier/ProofDependencyManager.cs b/Source/DafnyCore/Verifier/ProofDependencyManager.cs
index 4add7f73729..0d5522e6ce0 100644
--- a/Source/DafnyCore/Verifier/ProofDependencyManager.cs
+++ b/Source/DafnyCore/Verifier/ProofDependencyManager.cs
@@ -85,7 +85,10 @@ public ProofDependency GetFullIdDependency(TrackedNodeComponent component) {
     }
 
     public IEnumerable<ProofDependency> GetOrderedFullDependencies(IEnumerable<TrackedNodeComponent> components) {
-      return components.Select(GetFullIdDependency).OrderBy(dep => (dep.RangeString(), dep.Description));
+      return components
+        .Select(GetFullIdDependency)
+        .OrderBy(dep => dep.Range)
+        .ThenBy(dep => dep.Description);
     }
   }
 }
\ No newline at end of file

From fd928f7df072448f78dd0a87d4916aa7fa3f5c36 Mon Sep 17 00:00:00 2001
From: Aaron Tomb <aarotomb@amazon.com>
Date: Wed, 10 Jan 2024 09:10:16 -0800
Subject: [PATCH 6/9] Change output ordering to reflect code change

---
 .../LitTests/LitTest/logger/ProofDependencyLogging.dfy      | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencyLogging.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencyLogging.dfy
index ceb2a08ac95..7301be4f40f 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencyLogging.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencyLogging.dfy
@@ -36,8 +36,8 @@
 // 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:       ProofDependencyLogging.dfy\(229,12\)-\(229,12\): value always satisfies the subset constraints of 'nat'
 //
 // CHECK: Results for M.ObviouslyUnnecessaryRequiresFunc \(well-formedness\)
 // CHECK:     Proof dependencies:
@@ -54,8 +54,8 @@
 // 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\(252,12\)-\(252,16\): let expression binding RHS well-formed
 // CHECK:       ProofDependencyLogging.dfy\(254,3\)-\(254,3\): let expression result
 //
 // CHECK: Results for M.ObviouslyUnconstrainedCodeMethod \(correctness\)
@@ -110,8 +110,8 @@
 // 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:       ProofDependencyLogging.dfy\(341,3\)-\(341,3\): function precondition satisfied
 //
 // CHECK: Results for M.CallContradictoryMethodMethod \(correctness\)
 // CHECK:     Proof dependencies:

From eda4c5a84daaba978cac1fb83857c9a3f3085320 Mon Sep 17 00:00:00 2001
From: Aaron Tomb <aarotomb@amazon.com>
Date: Wed, 10 Jan 2024 11:02:24 -0800
Subject: [PATCH 7/9] Make proof dependency tests less fragile

---
 .../LitTest/logger/CoverageReport.dfy         |  18 +-
 ...roofDependencies.dfy_combined.html.expect} | 352 +++++++------
 ...ndencies.dfy_combined_limited.html.expect} | 353 +++++++------
 ...ependencies.dfy_tests_expected.html.expect | 481 +++++++++++++++++
 ...Dependencies.dfy_verification.html.expect} | 350 +++++++------
 .../LitTest/logger/ProofDependencyLogging.dfy | 462 ++++-------------
 ...encyLogging.dfy_tests_expected.html.expect | 484 ------------------
 .../logger/ProofDependencyWarnings.dfy        |   2 +-
 .../logger/ProofDependencyWarnings.dfy.expect |  36 +-
 9 files changed, 1122 insertions(+), 1416 deletions(-)
 rename Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/{ProofDependencyLogging.dfy_combined.html.expect => ProofDependencies.dfy_combined.html.expect} (50%)
 rename Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/{ProofDependencyLogging.dfy_combined_limited.html.expect => ProofDependencies.dfy_combined_limited.html.expect} (51%)
 create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_tests_expected.html.expect
 rename Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/{ProofDependencyLogging.dfy_verification.html.expect => ProofDependencies.dfy_verification.html.expect} (60%)
 delete mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencyLogging.dfy_tests_expected.html.expect

diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/CoverageReport.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/CoverageReport.dfy
index eb76fc3925d..4c6b0e93032 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/CoverageReport.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/CoverageReport.dfy
@@ -2,23 +2,23 @@
 // 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 --verification-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"
+// RUN: %sed 's/<h1 hidden.*//' "%t"/coverage_verification/ProofDependencies.dfy_verification.html > "%t"/coverage_verification_actual.html
+// RUN: %diff "%S/ProofDependencies.dfy_verification.html.expect" "%t/coverage_verification_actual.html"
 // Expected 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"
+// RUN: %sed 's/<h1 hidden.*//' "%t"/coverage_testing/ProofDependencies.dfy_tests_expected.html > "%t"/coverage_testing_actual.html
+// RUN: %diff "%S/ProofDependencies.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"
+// RUN: %sed 's/<h1 hidden.*//' "%t"/coverage_combined/ProofDependencies.dfy_combined.html > "%t"/coverage_combined.html
+// RUN: %diff "%S/ProofDependencies.dfy_combined.html.expect" "%t/coverage_combined.html"
 // Combined, limited coverage:
 // RUN: rm -rf "%t"/coverage_combined
 // RUN: %baredafny merge-coverage-reports --only-label NotCovered --no-timestamp-for-coverage-report "%t"/coverage_combined_limited "%t"/coverage_testing "%t"/coverage_verification
-// RUN: %sed 's/<h1 hidden.*//' "%t"/coverage_combined_limited/ProofDependencyLogging.dfy_combined.html > "%t"/coverage_combined_limited.html
-// RUN: %diff "%S/ProofDependencyLogging.dfy_combined_limited.html.expect" "%t/coverage_combined_limited.html"
+// RUN: %sed 's/<h1 hidden.*//' "%t"/coverage_combined_limited/ProofDependencies.dfy_combined.html > "%t"/coverage_combined_limited.html
+// RUN: %diff "%S/ProofDependencies.dfy_combined_limited.html.expect" "%t/coverage_combined_limited.html"
 
 
-include "ProofDependencyLogging.dfy"
+include "ProofDependencies.dfy"
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencyLogging.dfy_combined.html.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_combined.html.expect
similarity index 50%
rename from Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencyLogging.dfy_combined.html.expect
rename to Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_combined.html.expect
index 61b2aeea4ed..c44944bd02a 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencyLogging.dfy_combined.html.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_combined.html.expect
@@ -5,187 +5,187 @@
 <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>
+    <title>ProofDependencies.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>
+    <a href="ProofDependencies.dfy_tests_expected_2.html" class="el_report">Expected Test Coverage (coverage_testing)</a><a href="ProofDependencies.dfy_verification_3.html" class="el_report">Verification coverage (coverage_verification)</a>
 </div>
-<h1>ProofDependencyLogging.dfy, Combined Coverage Report</h1>
+<h1>ProofDependencies.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,16\) from call
-// CHECK:       ProofDependencyLogging.dfy\(348,9\)-\(348,47\): ensures clause at ProofDependencyLogging.dfy\(333,21\)-\(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,21\)-\(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\)
-// CHECK:     Unused by proof:
-// CHECK:       ProofDependencyLogging.dfy\(428,7\)-\(428,7\): assumption that divisor is always non-zero.
-// CHECK:       ProofDependencyLogging.dfy\(428,5\)-\(429,13\): calc statement result
+<span class="na" id="1:1">// RUN: %diff "%s" "%s"
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
 module M {
 method {:testEntry} RedundantAssumeMethod(n: int)
 {
@@ -452,10 +452,6 @@ method {:testEntry} DontWarnAboutVacuousAssertFalse(x: int) {
   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
 }
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencyLogging.dfy_combined_limited.html.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_combined_limited.html.expect
similarity index 51%
rename from Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencyLogging.dfy_combined_limited.html.expect
rename to Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_combined_limited.html.expect
index c2b140f2eab..cbf6d92c871 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencyLogging.dfy_combined_limited.html.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_combined_limited.html.expect
@@ -5,187 +5,187 @@
 <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>
+    <title>ProofDependencies.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>
+    <a href="ProofDependencies.dfy_tests_expected_2.html" class="el_report">Expected Test Coverage (coverage_testing)</a><a href="ProofDependencies.dfy_verification_3.html" class="el_report">Verification coverage (coverage_verification)</a>
 </div>
-<h1>ProofDependencyLogging.dfy, Combined Coverage Report</h1>
+<h1>ProofDependencies.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,16\) from call
-// CHECK:       ProofDependencyLogging.dfy\(348,9\)-\(348,47\): ensures clause at ProofDependencyLogging.dfy\(333,21\)-\(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,21\)-\(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\)
-// CHECK:     Unused by proof:
-// CHECK:       ProofDependencyLogging.dfy\(428,7\)-\(428,7\): assumption that divisor is always non-zero.
-// CHECK:       ProofDependencyLogging.dfy\(428,5\)-\(429,13\): calc statement result
+<span class="na" id="1:1">// RUN: %diff "%s" "%s"
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
 module M {
 method {:testEntry} RedundantAssumeMethod(n: int)
 {
@@ -452,10 +452,7 @@ method {:testEntry} ObviouslyUnreachableMatchStatementCaseMethod(t: T) returns (
   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
-
+</span><span class="na" id="438:1">
 class C {
   var x: int
 }
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_tests_expected.html.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_tests_expected.html.expect
new file mode 100644
index 00000000000..8be4a591cfc
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_tests_expected.html.expect
@@ -0,0 +1,481 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
+<html
+        xmlns="http://www.w3.org/1999/xhtml" lang="en">
+<head>
+    <meta http-equiv="Content-Type" content="text/html;charset=UTF-8"/>
+    <link rel="stylesheet" href="./.resources/coverage.css" type="text/css"/>
+    <title>ProofDependencies.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>ProofDependencies.dfy, Expected Test Coverage</h1>
+
+<pre class="source lang-java linenums">
+<span class="na" id="1:1">// RUN: %diff "%s" "%s"
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+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">
+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/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencyLogging.dfy_verification.html.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_verification.html.expect
similarity index 60%
rename from Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencyLogging.dfy_verification.html.expect
rename to Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_verification.html.expect
index f599417ecbf..9f915c991c1 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencyLogging.dfy_verification.html.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_verification.html.expect
@@ -5,187 +5,187 @@
 <head>
     <meta http-equiv="Content-Type" content="text/html;charset=UTF-8"/>
     <link rel="stylesheet" href="./.resources/coverage.css" type="text/css"/>
-    <title>ProofDependencyLogging.dfy, Verification coverage</title>
+    <title>ProofDependencies.dfy, Verification coverage</title>
 </head>
 <body onload="window['PR_TAB_WIDTH']=4">
 <div class="menu" id="menu">
     <a href="./index_verification.html">Index</a>
     
 </div>
-<h1>ProofDependencyLogging.dfy, Verification coverage</h1>
+<h1>ProofDependencies.dfy, Verification 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,16\) from call
-// CHECK:       ProofDependencyLogging.dfy\(348,9\)-\(348,47\): ensures clause at ProofDependencyLogging.dfy\(333,21\)-\(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,21\)-\(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\)
-// CHECK:     Unused by proof:
-// CHECK:       ProofDependencyLogging.dfy\(428,7\)-\(428,7\): assumption that divisor is always non-zero.
-// CHECK:       ProofDependencyLogging.dfy\(428,5\)-\(429,13\): calc statement result
+<span class="na" id="1:1">// RUN: %diff "%s" "%s"
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
 module M {
 method {:testEntry} RedundantAssumeMethod(n: int)
 {
@@ -452,10 +452,6 @@ method {:testEntry} DontWarnAboutVacuousAssertFalse(x: int) {
   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
 }
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencyLogging.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencyLogging.dfy
index 7301be4f40f..4cebdca5640 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencyLogging.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencyLogging.dfy
@@ -1,457 +1,177 @@
-// RUN: %baredafny verify --log-format:text --boogie -trackVerificationCoverage "%s" > "%t"
+// RUN: %baredafny verify --log-format:text --verify-included-files --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:       ProofDependencies.dfy\(177,12\)-\(177,16\): assume statement
+// CHECK:       ProofDependencies.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:       ProofDependencies.dfy\(183,12\)-\(183,16\): assume statement
+// CHECK:       ProofDependencies.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:       ProofDependencies.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:       ProofDependencies.dfy\(198,12\)-\(198,16\): requires clause
+// CHECK:       ProofDependencies.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:       ProofDependencies.dfy\(207,12\)-\(207,16\): requires clause
+// CHECK:       ProofDependencies.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:       ProofDependencies.dfy\(216,1\)-\(222,1\): function definition for ObviouslyRedundantRequiresFunc
+// CHECK:       ProofDependencies.dfy\(217,12\)-\(217,16\): requires clause
+// CHECK:       ProofDependencies.dfy\(219,11\)-\(219,15\): ensures clause
+// CHECK:       ProofDependencies.dfy\(221,3\)-\(221,7\): function call result
+// CHECK:       ProofDependencies.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,3\)-\(229,15\): assignment \(or return\)
-// CHECK:       ProofDependencyLogging.dfy\(229,12\)-\(229,12\): value always satisfies the subset constraints of 'nat'
+// CHECK:       ProofDependencies.dfy\(225,12\)-\(225,16\): requires clause
+// CHECK:       ProofDependencies.dfy\(227,11\)-\(227,15\): ensures clause
+// CHECK:       ProofDependencies.dfy\(229,3\)-\(229,15\): assignment \(or return\)
+// CHECK:       ProofDependencies.dfy\(229,12\)-\(229,12\): value always satisfies the subset constraints of 'nat'
 //
 // 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:       ProofDependencies.dfy\(237,21\)-\(237,21\): value always satisfies the subset constraints of 'nat'
+// CHECK:       ProofDependencies.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:       ProofDependencies.dfy\(244,25\)-\(244,25\): value always satisfies the subset constraints of 'nat'
+// CHECK:       ProofDependencies.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,7\)-\(252,7\): let expression binding
-// CHECK:       ProofDependencyLogging.dfy\(252,12\)-\(252,16\): let expression binding RHS well-formed
-// CHECK:       ProofDependencyLogging.dfy\(254,3\)-\(254,3\): let expression result
+// CHECK:       ProofDependencies.dfy\(248,1\)-\(256,1\): function definition for ObviouslyUnconstrainedCodeFunc
+// CHECK:       ProofDependencies.dfy\(249,12\)-\(249,16\): requires clause
+// CHECK:       ProofDependencies.dfy\(250,11\)-\(250,17\): ensures clause
+// CHECK:       ProofDependencies.dfy\(252,7\)-\(252,7\): let expression binding
+// CHECK:       ProofDependencies.dfy\(252,12\)-\(252,16\): let expression binding RHS well-formed
+// CHECK:       ProofDependencies.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:       ProofDependencies.dfy\(259,12\)-\(259,16\): requires clause
+// CHECK:       ProofDependencies.dfy\(260,11\)-\(260,17\): ensures clause
+// CHECK:       ProofDependencies.dfy\(262,9\)-\(262,17\): assignment \(or return\)
+// CHECK:       ProofDependencies.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:       ProofDependencies.dfy\(270,1\)-\(275,1\): function definition for PartiallyRedundantRequiresFunc
+// CHECK:       ProofDependencies.dfy\(271,23\)-\(271,27\): requires clause
+// CHECK:       ProofDependencies.dfy\(272,11\)-\(272,15\): ensures clause
+// CHECK:       ProofDependencies.dfy\(274,3\)-\(274,7\): function call result
+// CHECK:       ProofDependencies.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:       ProofDependencies.dfy\(279,22\)-\(279,26\): requires clause
+// CHECK:       ProofDependencies.dfy\(282,21\)-\(282,21\): value always satisfies the subset constraints of 'nat'
+// CHECK:       ProofDependencies.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:       ProofDependencies.dfy\(288,1\)-\(295,1\): function definition for MultiPartRedundantRequiresFunc
+// CHECK:       ProofDependencies.dfy\(291,12\)-\(291,17\): requires clause
+// CHECK:       ProofDependencies.dfy\(292,11\)-\(292,16\): ensures clause
+// CHECK:       ProofDependencies.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:       ProofDependencies.dfy\(300,12\)-\(300,17\): requires clause
+// CHECK:       ProofDependencies.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:       ProofDependencies.dfy\(309,1\)-\(316,1\): function definition for MultiPartContradictoryRequiresFunc
+// CHECK:       ProofDependencies.dfy\(310,12\)-\(310,16\): requires clause
+// CHECK:       ProofDependencies.dfy\(311,12\)-\(311,16\): requires clause
+// CHECK:       ProofDependencies.dfy\(313,11\)-\(313,16\): ensures clause
+// CHECK:       ProofDependencies.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:       ProofDependencies.dfy\(319,12\)-\(319,16\): requires clause
+// CHECK:       ProofDependencies.dfy\(320,12\)-\(320,16\): requires clause
+// CHECK:       ProofDependencies.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,39\): function call result
-// CHECK:       ProofDependencyLogging.dfy\(341,3\)-\(341,3\): function precondition satisfied
+// CHECK:       ProofDependencies.dfy\(336,1\)-\(342,1\): function definition for CallContradictoryFunctionFunc
+// CHECK:       ProofDependencies.dfy\(337,12\)-\(337,16\): requires clause
+// CHECK:       ProofDependencies.dfy\(338,11\)-\(338,15\): ensures clause
+// CHECK:       ProofDependencies.dfy\(341,3\)-\(341,39\): function call result
+// CHECK:       ProofDependencies.dfy\(341,3\)-\(341,3\): function precondition satisfied
 //
 // 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,16\) from call
-// CHECK:       ProofDependencyLogging.dfy\(348,9\)-\(348,47\): ensures clause at ProofDependencyLogging.dfy\(333,21\)-\(333,25\) from call
-// CHECK:       ProofDependencyLogging.dfy\(348,9\)-\(348,47\): requires clause at ProofDependencyLogging.dfy\(332,12\)-\(332,16\) from call
+// CHECK:       ProofDependencies.dfy\(345,12\)-\(345,16\): requires clause
+// CHECK:       ProofDependencies.dfy\(348,9\)-\(348,47\): ensures clause at ProofDependencies.dfy\(333,12\)-\(333,16\) from call
+// CHECK:       ProofDependencies.dfy\(348,9\)-\(348,47\): ensures clause at ProofDependencies.dfy\(333,21\)-\(333,25\) from call
+// CHECK:       ProofDependencies.dfy\(348,9\)-\(348,47\): requires clause at ProofDependencies.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:       ProofDependencies.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:       ProofDependencies.dfy\(362,9\)-\(362,15\): assignment \(or return\)
+// CHECK:       ProofDependencies.dfy\(363,20\)-\(363,24\): assertion always holds
 //
 // CHECK: Results for M.FalseAntecedentEnsuresClauseMethod \(correctness\)
 // CHECK:     Proof dependencies:
-// CHECK:       ProofDependencyLogging.dfy\(368,21\)-\(368,25\): ensures clause
-// CHECK:       ProofDependencyLogging.dfy\(370,3\)-\(370,13\): assignment \(or return\)
+// CHECK:       ProofDependencies.dfy\(368,21\)-\(368,25\): ensures clause
+// CHECK:       ProofDependencies.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:       ProofDependencies.dfy\(373,1\)-\(380,1\): function definition for ObviouslyUnreachableIfExpressionBranchFunc
+// CHECK:       ProofDependencies.dfy\(374,12\)-\(374,16\): requires clause
+// CHECK:       ProofDependencies.dfy\(375,11\)-\(375,15\): ensures clause
+// CHECK:       ProofDependencies.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:       ProofDependencies.dfy\(383,12\)-\(383,16\): requires clause
+// CHECK:       ProofDependencies.dfy\(384,11\)-\(384,15\): ensures clause
+// CHECK:       ProofDependencies.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:       ProofDependencies.dfy\(395,1\)-\(403,1\): function definition for ObviouslyUnreachableMatchExpressionCaseFunction
+// CHECK:       ProofDependencies.dfy\(396,12\)-\(396,17\): requires clause
+// CHECK:       ProofDependencies.dfy\(397,11\)-\(397,15\): ensures clause
+// CHECK:       ProofDependencies.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:       ProofDependencies.dfy\(406,12\)-\(406,17\): requires clause
+// CHECK:       ProofDependencies.dfy\(407,11\)-\(407,15\): ensures clause
+// CHECK:       ProofDependencies.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\)
+// CHECK:       ProofDependencies.dfy\(416,12\)-\(416,17\): requires clause
+// CHECK:       ProofDependencies.dfy\(417,13\)-\(417,17\): ensures clause
+// CHECK:       ProofDependencies.dfy\(420,7\)-\(420,15\): assignment \(or return\)
 // CHECK:     Unused by proof:
-// CHECK:       ProofDependencyLogging.dfy\(428,7\)-\(428,7\): assumption that divisor is always non-zero.
-// CHECK:       ProofDependencyLogging.dfy\(428,5\)-\(429,13\): calc statement result
-module M {
-method {:testEntry} RedundantAssumeMethod(n: int)
-{
-    // either one or the other assumption shouldn't be covered
-    assume n > 4;
-    assume n > 3;
-    assert n > 1;
-}
-
-method {:testEntry} ContradictoryAssumeMethod(n: int)
-{
-    assume n > 0;
-    assume n < 0;
-    assume n == 5; // shouldn't be covered
-    assert n < 10; // shouldn't be covered
-}
-
-method {:testEntry} AssumeFalseMethod(n: int)
-{
-    assume n == 15; // shouldn't be covered
-    assume false;
-    assert n < 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 == 10; // contradicts both requires clauses
-  x - 1 // 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 == 10; // contradicts both requires clauses
-  return x - 1; // not necessarily a valid nat
-}
-
-// 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
-{
-  x + 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
-{
-  return x + 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 x + 2 else x + 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) { return x + 2; } else { return x + 1; }
-}
-
-// Code obviously not constrained by ensures clause.
-function {:testEntry} ObviouslyUnconstrainedCodeFunc(x: int): (r: (int, int))
-  requires x > 10
-  ensures r.0 > 10
-{
-  var a := x + 1; // constrained by ensures clause
-  var b := x - 1; // not constrained by ensures clause 
-  (a,
-   b)
-}
-
-method {:testEntry} ObviouslyUnconstrainedCodeMethod(x: int) returns (r: (int, int))
-  requires x > 10
-  ensures r.0 > 10
-{
-  var a := x + 1; // constrained by ensures clause
-  var b := x - 1; // not constrained by ensures clause
-  return
-    (a,
-     b);
-}
-
-// 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
-{
-  x + 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 x - 1 else x + 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
-{
-  x
-}
-
-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
-{
-  return x;
-}
-
-// 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
-{
-  x
-}
-
-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
-{
-  return x;
-}
-
-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
-  ContradictoryEnsuresClauseFunc(x) - 1
-}
-
-method {:testEntry} CallContradictoryMethodMethod(x: int) returns (r: int)
-  requires x > 1
-  ensures r < 0
-{
-  var y := ContradictoryEnsuresClauseMethod(x);
-  return y - 1;
-}
-
-// False antecedent requires clause
-method {:testEntry} FalseAntecedentRequiresClauseMethod(x: int) returns (r: int)
-  requires x*x < 0 ==> x == x + 1
-  ensures r > x
-{
-  return x + 1;
-}
-
-// False antecedent assert statement.
-method {:testEntry} FalseAntecedentAssertStatementMethod(x: int) {
-  var y := x*x;
-  assert y < 0 ==> x < 0;
-}
-
-// False antecedent ensures clause.
-method {:testEntry} FalseAntecedentEnsuresClauseMethod(x: int) returns (r: int)
-  ensures r < 0 ==> x < 0
-{
-  return x*x;
-}
-
-function {:testEntry} ObviouslyUnreachableIfExpressionBranchFunc(x: int): (r:int)
-  requires x > 0
-  ensures r > 0
-{
-  if x < 0
-  then x - 1 // unreachable
-  else x + 1
-}
-
-method {:testEntry} ObviouslyUnreachableIfStatementBranchMethod(x: int) returns (r:int)
-  requires x > 0
-  ensures r > 0
-{
-  if x < 0 {
-    return x - 1; // unreachable
-  } else {
-    return x + 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 => 1 // unreachable
-    case B => 2
-  }
-}
-
-method {:testEntry} ObviouslyUnreachableMatchStatementCaseMethod(t: T) returns (r:int)
-  requires t != A
-  ensures r > 1 // alt: r > 0
-{
-  match t {
-    case A => return 1; // unreachable
-    case B => return 2;
-  }
-}
-
-method {:testEntry} ObviouslyUnreachableReturnStatementMethod(t: T) returns (r:int)
-  requires t != A
-    ensures r > 1 // alt: r > 0
-  {
-    if !t.A? {
-      return 2;
-    }
-
-    return 1; // unreachable
-  }
-
-method {:testEntry} CalcStatementWithSideConditions(x: int) {
-  calc == {
-    x / 2;
-    (x*2) / 4;
-  }
-}
-
-method {:testEntry} DontWarnAboutVacuousAssertFalse(x: int) {
-  assume x == x + 1;
-  assert false;
-}
-
+// CHECK:       ProofDependencies.dfy\(428,7\)-\(428,7\): assumption that divisor is always non-zero.
+// CHECK:       ProofDependencies.dfy\(428,5\)-\(429,13\): calc statement result
+//
 // 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
-{
-  c.x
-}
-
-method {:testEntry} DontWarnAboutUnusedAssumeTrue(x: int) {
-  assume true;
-  assert 1 + x == x + 1;
-}
+// CHECK:       ProofDependencies.dfy\(445,5\)-\(445,5\): target object is never null
 
-}
+include "ProofDependencies.dfy"
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencyLogging.dfy_tests_expected.html.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencyLogging.dfy_tests_expected.html.expect
deleted file mode 100644
index 56095534796..00000000000
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencyLogging.dfy_tests_expected.html.expect
+++ /dev/null
@@ -1,484 +0,0 @@
-<?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,16\) from call
-// CHECK:       ProofDependencyLogging.dfy\(348,9\)-\(348,47\): ensures clause at ProofDependencyLogging.dfy\(333,21\)-\(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,21\)-\(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\)
-// CHECK:     Unused by proof:
-// CHECK:       ProofDependencyLogging.dfy\(428,7\)-\(428,7\): assumption that divisor is always non-zero.
-// CHECK:       ProofDependencyLogging.dfy\(428,5\)-\(429,13\): calc statement result
-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/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencyWarnings.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencyWarnings.dfy
index 419b325cf41..a959e0fb882 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencyWarnings.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencyWarnings.dfy
@@ -1,4 +1,4 @@
 // RUN: %baredafny verify --use-basename-for-filename --show-snippets false --verify-included-files --warn-contradictory-assumptions --warn-redundant-assumptions "%s" > "%t"
 // RUN: %diff "%t" "%s.expect"
 
-include "ProofDependencyLogging.dfy"
+include "ProofDependencies.dfy"
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencyWarnings.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencyWarnings.dfy.expect
index 9e350f9250b..8de569bd023 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencyWarnings.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencyWarnings.dfy.expect
@@ -1,20 +1,20 @@
-ProofDependencyLogging.dfy(176,11): Warning: unnecessary (or partly unnecessary) assume statement
-ProofDependencyLogging.dfy(186,13): Warning: proved using contradictory assumptions: assertion always holds
-ProofDependencyLogging.dfy(185,11): Warning: unnecessary (or partly unnecessary) assume statement
-ProofDependencyLogging.dfy(193,13): Warning: proved using contradictory assumptions: assertion always holds
-ProofDependencyLogging.dfy(191,11): Warning: unnecessary (or partly unnecessary) assume statement
-ProofDependencyLogging.dfy(202,11): Warning: proved using contradictory assumptions: assertion always holds
-ProofDependencyLogging.dfy(203,4): Warning: proved using contradictory assumptions: value always satisfies the subset constraints of 'nat'
-ProofDependencyLogging.dfy(211,11): Warning: proved using contradictory assumptions: assertion always holds
-ProofDependencyLogging.dfy(212,11): Warning: proved using contradictory assumptions: value always satisfies the subset constraints of 'nat'
-ProofDependencyLogging.dfy(209,10): Warning: ensures clause proved using contradictory assumptions
-ProofDependencyLogging.dfy(226,11): Warning: unnecessary requires clause
-ProofDependencyLogging.dfy(241,11): Warning: unnecessary requires clause
-ProofDependencyLogging.dfy(298,11): Warning: unnecessary requires clause
-ProofDependencyLogging.dfy(299,11): Warning: unnecessary requires clause
-ProofDependencyLogging.dfy(321,11): Warning: unnecessary requires clause
-ProofDependencyLogging.dfy(346,10): Warning: ensures clause proved using contradictory assumptions
-ProofDependencyLogging.dfy(354,11): Warning: unnecessary requires clause
-ProofDependencyLogging.dfy(363,9): Warning: unnecessary (or partly unnecessary) assert statement
+ProofDependencies.dfy(176,11): Warning: unnecessary (or partly unnecessary) assume statement
+ProofDependencies.dfy(186,13): Warning: proved using contradictory assumptions: assertion always holds
+ProofDependencies.dfy(185,11): Warning: unnecessary (or partly unnecessary) assume statement
+ProofDependencies.dfy(193,13): Warning: proved using contradictory assumptions: assertion always holds
+ProofDependencies.dfy(191,11): Warning: unnecessary (or partly unnecessary) assume statement
+ProofDependencies.dfy(202,11): Warning: proved using contradictory assumptions: assertion always holds
+ProofDependencies.dfy(203,4): Warning: proved using contradictory assumptions: value always satisfies the subset constraints of 'nat'
+ProofDependencies.dfy(211,11): Warning: proved using contradictory assumptions: assertion always holds
+ProofDependencies.dfy(212,11): Warning: proved using contradictory assumptions: value always satisfies the subset constraints of 'nat'
+ProofDependencies.dfy(209,10): Warning: ensures clause proved using contradictory assumptions
+ProofDependencies.dfy(226,11): Warning: unnecessary requires clause
+ProofDependencies.dfy(241,11): Warning: unnecessary requires clause
+ProofDependencies.dfy(298,11): Warning: unnecessary requires clause
+ProofDependencies.dfy(299,11): Warning: unnecessary requires clause
+ProofDependencies.dfy(321,11): Warning: unnecessary requires clause
+ProofDependencies.dfy(346,10): Warning: ensures clause proved using contradictory assumptions
+ProofDependencies.dfy(354,11): Warning: unnecessary requires clause
+ProofDependencies.dfy(363,9): Warning: unnecessary (or partly unnecessary) assert statement
 
 Dafny program verifier finished with 32 verified, 0 errors

From 6e8ed74d283caccc7fd63a17a43055705566275c Mon Sep 17 00:00:00 2001
From: Aaron Tomb <aarotomb@amazon.com>
Date: Wed, 10 Jan 2024 11:37:21 -0800
Subject: [PATCH 8/9] Add missing file

---
 .../LitTest/logger/ProofDependencies.dfy      | 453 ++++++++++++++++++
 1 file changed, 453 insertions(+)
 create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy

diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy
new file mode 100644
index 00000000000..97359697131
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy
@@ -0,0 +1,453 @@
+// RUN: %diff "%s" "%s"
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+module M {
+method {:testEntry} RedundantAssumeMethod(n: int)
+{
+    // either one or the other assumption shouldn't be covered
+    assume n > 4;
+    assume n > 3;
+    assert n > 1;
+}
+
+method {:testEntry} ContradictoryAssumeMethod(n: int)
+{
+    assume n > 0;
+    assume n < 0;
+    assume n == 5; // shouldn't be covered
+    assert n < 10; // shouldn't be covered
+}
+
+method {:testEntry} AssumeFalseMethod(n: int)
+{
+    assume n == 15; // shouldn't be covered
+    assume false;
+    assert n < 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 == 10; // contradicts both requires clauses
+  x - 1 // 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 == 10; // contradicts both requires clauses
+  return x - 1; // not necessarily a valid nat
+}
+
+// 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
+{
+  x + 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
+{
+  return x + 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 x + 2 else x + 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) { return x + 2; } else { return x + 1; }
+}
+
+// Code obviously not constrained by ensures clause.
+function {:testEntry} ObviouslyUnconstrainedCodeFunc(x: int): (r: (int, int))
+  requires x > 10
+  ensures r.0 > 10
+{
+  var a := x + 1; // constrained by ensures clause
+  var b := x - 1; // not constrained by ensures clause 
+  (a,
+   b)
+}
+
+method {:testEntry} ObviouslyUnconstrainedCodeMethod(x: int) returns (r: (int, int))
+  requires x > 10
+  ensures r.0 > 10
+{
+  var a := x + 1; // constrained by ensures clause
+  var b := x - 1; // not constrained by ensures clause
+  return
+    (a,
+     b);
+}
+
+// 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
+{
+  x + 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 x - 1 else x + 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
+{
+  x
+}
+
+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
+{
+  return x;
+}
+
+// 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
+{
+  x
+}
+
+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
+{
+  return x;
+}
+
+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
+  ContradictoryEnsuresClauseFunc(x) - 1
+}
+
+method {:testEntry} CallContradictoryMethodMethod(x: int) returns (r: int)
+  requires x > 1
+  ensures r < 0
+{
+  var y := ContradictoryEnsuresClauseMethod(x);
+  return y - 1;
+}
+
+// False antecedent requires clause
+method {:testEntry} FalseAntecedentRequiresClauseMethod(x: int) returns (r: int)
+  requires x*x < 0 ==> x == x + 1
+  ensures r > x
+{
+  return x + 1;
+}
+
+// False antecedent assert statement.
+method {:testEntry} FalseAntecedentAssertStatementMethod(x: int) {
+  var y := x*x;
+  assert y < 0 ==> x < 0;
+}
+
+// False antecedent ensures clause.
+method {:testEntry} FalseAntecedentEnsuresClauseMethod(x: int) returns (r: int)
+  ensures r < 0 ==> x < 0
+{
+  return x*x;
+}
+
+function {:testEntry} ObviouslyUnreachableIfExpressionBranchFunc(x: int): (r:int)
+  requires x > 0
+  ensures r > 0
+{
+  if x < 0
+  then x - 1 // unreachable
+  else x + 1
+}
+
+method {:testEntry} ObviouslyUnreachableIfStatementBranchMethod(x: int) returns (r:int)
+  requires x > 0
+  ensures r > 0
+{
+  if x < 0 {
+    return x - 1; // unreachable
+  } else {
+    return x + 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 => 1 // unreachable
+    case B => 2
+  }
+}
+
+method {:testEntry} ObviouslyUnreachableMatchStatementCaseMethod(t: T) returns (r:int)
+  requires t != A
+  ensures r > 1 // alt: r > 0
+{
+  match t {
+    case A => return 1; // unreachable
+    case B => return 2;
+  }
+}
+
+method {:testEntry} ObviouslyUnreachableReturnStatementMethod(t: T) returns (r:int)
+  requires t != A
+    ensures r > 1 // alt: r > 0
+  {
+    if !t.A? {
+      return 2;
+    }
+
+    return 1; // unreachable
+  }
+
+method {:testEntry} CalcStatementWithSideConditions(x: int) {
+  calc == {
+    x / 2;
+    (x*2) / 4;
+  }
+}
+
+method {:testEntry} DontWarnAboutVacuousAssertFalse(x: int) {
+  assume x == x + 1;
+  assert false;
+}
+
+class C {
+  var x: int
+}
+
+function {:testEntry} GetX(c: C): int
+  reads c
+{
+  c.x
+}
+
+method {:testEntry} DontWarnAboutUnusedAssumeTrue(x: int) {
+  assume true;
+  assert 1 + x == x + 1;
+}
+
+}

From ae2d2bbe218e0b3b3e68b3cd75a53e44ae312b80 Mon Sep 17 00:00:00 2001
From: Aaron Tomb <aarotomb@amazon.com>
Date: Wed, 10 Jan 2024 15:08:17 -0800
Subject: [PATCH 9/9] Fix expected coverage report output

---
 .../logger/ProofDependencies.dfy_combined.html.expect |  8 ++++----
 ...ProofDependencies.dfy_combined_limited.html.expect |  7 +++----
 .../ProofDependencies.dfy_tests_expected.html.expect  | 11 +++++------
 .../ProofDependencies.dfy_verification.html.expect    |  8 ++++----
 4 files changed, 16 insertions(+), 18 deletions(-)

diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_combined.html.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_combined.html.expect
index c44944bd02a..2457134dab0 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_combined.html.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_combined.html.expect
@@ -459,12 +459,12 @@ class C {
 function {:testEntry} GetX(c: C): int
   reads c
 {
-  </span><span class="pc" id="449:3">c.x
-</span><span class="na" id="450:1">}
+  </span><span class="pc" id="445:3">c.x
+</span><span class="na" id="446: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;
+  assume </span><span class="pc" id="449:10">t</span><span class="na" id="449:11">rue;
+  assert 1 + x </span><span class="fc" id="450:16">=</span><span class="na" id="450:17">= x + 1;
 }
 
 }
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_combined_limited.html.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_combined_limited.html.expect
index cbf6d92c871..1e9dd0cc5e5 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_combined_limited.html.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_combined_limited.html.expect
@@ -452,19 +452,18 @@ method {:testEntry} ObviouslyUnreachableMatchStatementCaseMethod(t: T) returns (
   assert false;
 }
 
-</span><span class="na" id="438:1">
-class C {
+</span><span class="na" id="438:1">class C {
   var x: int
 }
 
 function {:testEntry} GetX(c: C): int
   reads c
 {
-  </span><span class="nc" id="449:3">c.</span><span class="na" id="449:5">x
+  </span><span class="nc" id="445:3">c.</span><span class="na" id="445:5">x
 }
 
 method {:testEntry} DontWarnAboutUnusedAssumeTrue(x: int) {
-  assume </span><span class="nc" id="453:10">t</span><span class="na" id="453:11">rue;
+  assume </span><span class="nc" id="449:10">t</span><span class="na" id="449:11">rue;
   assert 1 + x == x + 1;
 }
 
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_tests_expected.html.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_tests_expected.html.expect
index 8be4a591cfc..34830695408 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_tests_expected.html.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_tests_expected.html.expect
@@ -452,15 +452,14 @@ method {:testEntry} CalcStatementWithSideConditions(x: int) {
   assert false;
 }
 
-</span><span class="na" id="438:1">
-class C {
+</span><span class="na" id="438:1">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="442:1">function {:testEntry} GetX(c: C): int
+</span><span class="na" id="443:1">  reads c
 {
-</span><span class="fc" id="449:1">  c.x
+</span><span class="fc" id="445:1">  c.x
 }
 
 method {:testEntry} DontWarnAboutUnusedAssumeTrue(x: int) {
@@ -468,7 +467,7 @@ method {:testEntry} DontWarnAboutUnusedAssumeTrue(x: int) {
   assert 1 + x == x + 1;
 }
 
-</span><span class="na" id="457:1">}
+</span><span class="na" id="453:1">}
 
 </span></pre>
 <div class="footer">
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_verification.html.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_verification.html.expect
index 9f915c991c1..af02650fdbd 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_verification.html.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_verification.html.expect
@@ -459,12 +459,12 @@ class C {
 function {:testEntry} GetX(c: C): int
   reads c
 {
-  </span><span class="nc" id="449:3">c.</span><span class="pc" id="449:5">x
-</span><span class="na" id="450:1">}
+  </span><span class="nc" id="445:3">c.</span><span class="pc" id="445:5">x
+</span><span class="na" id="446: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;
+  assume </span><span class="nc" id="449:10">t</span><span class="na" id="449:11">rue;
+  assert 1 + x </span><span class="fc" id="450:16">=</span><span class="na" id="450:17">= x + 1;
 }
 
 }