diff --git a/Source/DafnyCore/ProofDependencyWarnings.cs b/Source/DafnyCore/ProofDependencyWarnings.cs
index 21058e16554..93a0ac5f0d8 100644
--- a/Source/DafnyCore/ProofDependencyWarnings.cs
+++ b/Source/DafnyCore/ProofDependencyWarnings.cs
@@ -1,6 +1,7 @@
 using System.Linq;
 using DafnyCore.Verifier;
 using Microsoft.Dafny.ProofObligationDescription;
+using VC;
 
 namespace Microsoft.Dafny;
 
@@ -16,6 +17,10 @@ public static void WarnAboutSuspiciousDependencies(DafnyOptions dafnyOptions, Er
   }
 
   public static void WarnAboutSuspiciousDependenciesForImplementation(DafnyOptions dafnyOptions, ErrorReporter reporter, ProofDependencyManager depManager, DafnyConsolePrinter.ImplementationLogEntry logEntry, DafnyConsolePrinter.VerificationResultLogEntry result) {
+    if (result.Outcome != ConditionGeneration.Outcome.Correct) {
+      return;
+    }
+
     var potentialDependencies = depManager.GetPotentialDependenciesForDefinition(logEntry.Name);
     var usedDependencies =
       result
@@ -81,8 +86,13 @@ private static bool ShouldWarnVacuous(DafnyOptions options, string verboseName,
         return false;
       }
 
-      // Similarly here
-      if (poDep.ProofObligation is MatchIsComplete or AlternativeIsComplete) {
+      // Some proof obligations occur in a context that the Dafny programmer
+      // doesn't have control of, so warning about vacuity isn't helpful.
+      if (poDep.ProofObligation
+          is MatchIsComplete
+          or AlternativeIsComplete
+          or ValidInRecursion
+          or TraitDecreases) {
         return false;
       }
 
diff --git a/Source/DafnyCore/Verifier/ProofDependency.cs b/Source/DafnyCore/Verifier/ProofDependency.cs
index f3a0ebc4b79..b91f08ef1d0 100644
--- a/Source/DafnyCore/Verifier/ProofDependency.cs
+++ b/Source/DafnyCore/Verifier/ProofDependency.cs
@@ -66,6 +66,20 @@ public ProofObligationDependency(IToken tok, PODesc.ProofObligationDescription p
   }
 }
 
+public class AssumedProofObligationDependency : ProofDependency {
+  public override RangeToken Range { get; }
+
+  public PODesc.ProofObligationDescription ProofObligation { get; }
+
+  public override string Description =>
+      $"assumption that {ProofObligation.SuccessDescription}";
+
+  public AssumedProofObligationDependency(IToken tok, PODesc.ProofObligationDescription proofObligation) {
+    Range = tok as RangeToken ?? new RangeToken(tok, tok);
+    ProofObligation = proofObligation;
+  }
+}
+
 // Represents the assumption of a requires clause in the process of
 // proving a Dafny definition.
 public class RequiresDependency : ProofDependency {
diff --git a/Source/DafnyCore/Verifier/Translator.cs b/Source/DafnyCore/Verifier/Translator.cs
index 9d892041e5f..12d8d86f1b4 100644
--- a/Source/DafnyCore/Verifier/Translator.cs
+++ b/Source/DafnyCore/Verifier/Translator.cs
@@ -7491,10 +7491,11 @@ Bpl.PredicateCmd Assert(IToken tok, Bpl.Expr condition, PODesc.ProofObligationDe
           || (RefinementToken.IsInherited(refinesToken, currentModule) && (codeContext == null || !codeContext.MustReverify))) {
         // produce an assume instead
         cmd = TrAssumeCmd(tok, condition, kv);
+        proofDependencies?.AddProofDependencyId(cmd, tok, new AssumedProofObligationDependency(tok, description));
       } else {
         cmd = TrAssertCmdDesc(ForceCheckToken.Unwrap(tok), condition, description, kv);
+        proofDependencies?.AddProofDependencyId(cmd, tok, new ProofObligationDependency(tok, description));
       }
-      proofDependencies?.AddProofDependencyId(cmd, tok, new ProofObligationDependency(tok, description));
       return cmd;
     }
 
diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs
index 56010751eea..f052bdd336b 100644
--- a/Source/DafnyDriver/DafnyDriver.cs
+++ b/Source/DafnyDriver/DafnyDriver.cs
@@ -468,7 +468,7 @@ private async Task<ExitValue> ProcessFilesAsync(IReadOnlyList<DafnyFile/*!*/>/*!
         string baseName = cce.NonNull(Path.GetFileName(dafnyFileNames[^1]));
         var (verified, outcome, moduleStats) = await BoogieAsync(options, baseName, boogiePrograms, programId);
 
-        if (options.TrackVerificationCoverage && verified) {
+        if (options.TrackVerificationCoverage) {
           ProofDependencyWarnings.WarnAboutSuspiciousDependencies(options, dafnyProgram.Reporter, depManager);
         }
 
diff --git a/Test/logger/ProofDependencyLogging.dfy b/Test/logger/ProofDependencyLogging.dfy
index 637c372b069..522dee90705 100644
--- a/Test/logger/ProofDependencyLogging.dfy
+++ b/Test/logger/ProofDependencyLogging.dfy
@@ -423,6 +423,13 @@ method ObviouslyUnreachableReturnStatementMethod(t: T) returns (r:int)
     return 1; // unreachable
   }
 
+method CalcStatementWithSideConditions(x: int) {
+  calc == {
+    x / 2;
+    (x*2) / 4;
+  }
+}
+
 method DontWarnAboutVacuousAssertFalse(x: int) {
   assume x == x + 1;
   assert false;
diff --git a/Test/logger/ProofDependencyWarnings.dfy b/Test/logger/ProofDependencyWarnings.dfy
index 7f61c0aac3a..419b325cf41 100644
--- a/Test/logger/ProofDependencyWarnings.dfy
+++ b/Test/logger/ProofDependencyWarnings.dfy
@@ -1,4 +1,4 @@
-// RUN: %verify --verify-included-files --warn-contradictory-assumptions --warn-redundant-assumptions "%s" > "%t"
+// 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"
diff --git a/Test/logger/ProofDependencyWarnings.dfy.expect b/Test/logger/ProofDependencyWarnings.dfy.expect
index 6fdf6aae938..a433ec699ec 100644
--- a/Test/logger/ProofDependencyWarnings.dfy.expect
+++ b/Test/logger/ProofDependencyWarnings.dfy.expect
@@ -17,4 +17,4 @@ ProofDependencyLogging.dfy(346,10): Warning: ensures clause proved using contrad
 ProofDependencyLogging.dfy(354,11): Warning: unnecessary requires clause
 ProofDependencyLogging.dfy(363,9): Warning: unnecessary assumption
 
-Dafny program verifier finished with 29 verified, 0 errors
+Dafny program verifier finished with 30 verified, 0 errors