diff --git a/Source/Core/AST/Absy.cs b/Source/Core/AST/Absy.cs
index 8305d8fb6..f817c5c0d 100644
--- a/Source/Core/AST/Absy.cs
+++ b/Source/Core/AST/Absy.cs
@@ -280,6 +280,33 @@ public List<int> FindLayers()
       }
       return layers.Distinct().OrderBy(l => l).ToList();
     }
+
+    // Look for {:name string} in list of attributes.
+    public string FindStringAttribute(string name)
+    {
+      return QKeyValue.FindStringAttribute(Attributes, name);
+    }
+
+    public void AddStringAttribute(IToken tok, string name, string parameter)
+    {
+      Attributes = new QKeyValue(tok, name, new List<object>() {parameter}, Attributes);
+    }
+
+    public void CopyIdFrom(IToken tok, ICarriesAttributes src)
+    {
+      var id = src.FindStringAttribute("id");
+      if (id is not null) {
+        AddStringAttribute(tok, "id", id);
+      }
+    }
+
+    public void CopyIdWithSuffixFrom(IToken tok, ICarriesAttributes src, string suffix)
+    {
+      var id = src.FindStringAttribute("id");
+      if (id is not null) {
+        AddStringAttribute(tok, "id", id + suffix);
+      }
+    }
   }
 
   [ContractClassFor(typeof(Absy))]
@@ -410,13 +437,6 @@ public Expr FindExprAttribute(string name)
       return res;
     }
 
-    // Look for {:name string} in list of attributes.
-    public string FindStringAttribute(string name)
-    {
-      Contract.Requires(name != null);
-      return QKeyValue.FindStringAttribute(this.Attributes, name);
-    }
-
     // Look for {:name N} in list of attributes. Return false if attribute
     // 'name' does not exist or if N is not an integer constant.  Otherwise,
     // return true and update 'result' with N.
@@ -1810,7 +1830,7 @@ public byte[] MD5DependencyChecksum
 
     public string Checksum
     {
-      get { return FindStringAttribute("checksum"); }
+      get { return (this as ICarriesAttributes).FindStringAttribute("checksum"); }
     }
 
     string dependencyChecksum;
@@ -3616,7 +3636,7 @@ public string Id
     {
       get
       {
-        var id = FindStringAttribute("id");
+        var id = (this as ICarriesAttributes).FindStringAttribute("id");
         if (id == null)
         {
           id = Name + GetHashCode().ToString() + ":0";
diff --git a/Source/Core/AST/AbsyCmd.cs b/Source/Core/AST/AbsyCmd.cs
index 0c88c4cc4..19697003b 100644
--- a/Source/Core/AST/AbsyCmd.cs
+++ b/Source/Core/AST/AbsyCmd.cs
@@ -3720,6 +3720,7 @@ protected override Cmd ComputeDesugaring(PrintOptions options)
       Dictionary<Variable, Expr> substMapBound = new Dictionary<Variable, Expr>();
       List<Variable> /*!*/
         tempVars = new List<Variable>();
+      string callId = (this as ICarriesAttributes).FindStringAttribute("id");
 
       // proc P(ins) returns (outs)
       //   requires Pre
@@ -3838,6 +3839,7 @@ protected override Cmd ComputeDesugaring(PrintOptions options)
             AssertCmd /*!*/
               a = new AssertRequiresCmd(this, reqCopy);
             Contract.Assert(a != null);
+
             if (Attributes != null)
             {
               // Inherit attributes of call.
@@ -3846,6 +3848,11 @@ protected override Cmd ComputeDesugaring(PrintOptions options)
               a.Attributes = attrCopy;
             }
 
+            // Do this after copying the attributes so it doesn't get overwritten
+            if (callId is not null) {
+              (a as ICarriesAttributes).CopyIdWithSuffixFrom(tok, req,  $"${callId}$requires");
+            }
+
             a.ErrorDataEnhanced = reqCopy.ErrorDataEnhanced;
             newBlockBody.Add(a);
           }
@@ -3857,6 +3864,11 @@ protected override Cmd ComputeDesugaring(PrintOptions options)
           AssumeCmd /*!*/
             a = new AssumeCmd(req.tok, Substituter.Apply(s, req.Condition));
           Contract.Assert(a != null);
+          // These probably won't have IDs, but copy if they do.
+          if (callId is not null) {
+            (a as ICarriesAttributes).CopyIdWithSuffixFrom(tok, req, $"${callId}$requires_assumed");
+          }
+
           newBlockBody.Add(a);
         }
       }
@@ -4019,6 +4031,10 @@ protected override Cmd ComputeDesugaring(PrintOptions options)
 
         #endregion
 
+        if (callId is not null) {
+          (assume as ICarriesAttributes).CopyIdWithSuffixFrom(tok, e, $"${callId}$ensures");
+        }
+
         newBlockBody.Add(assume);
       }
 
@@ -4036,6 +4052,9 @@ protected override Cmd ComputeDesugaring(PrintOptions options)
             cout_exp = new IdentifierExpr(cce.NonNull(couts[i]).tok, cce.NonNull(couts[i]));
           Contract.Assert(cout_exp != null);
           AssignCmd assign = Cmd.SimpleAssign(param_i.tok, cce.NonNull(this.Outs[i]), cout_exp);
+          if (callId is not null) {
+            Attributes = new QKeyValue(param_i.tok, "id", new List<object>(){ $"{callId}$out{i}" }, Attributes);
+          }
           newBlockBody.Add(assign);
         }
       }
diff --git a/Source/Core/AST/AbsyType.cs b/Source/Core/AST/AbsyType.cs
index 76b4f7941..ff7d90e95 100644
--- a/Source/Core/AST/AbsyType.cs
+++ b/Source/Core/AST/AbsyType.cs
@@ -3604,7 +3604,7 @@ public override bool IsSeq
     // be represented using the provided string (and also does not need to be explicitly declared).
     public string GetBuiltin()
     {
-      return this.Decl.FindStringAttribute("builtin");
+      return (this.Decl as ICarriesAttributes).FindStringAttribute("builtin");
     }
 
     //-----------  Cloning  ----------------------------------
diff --git a/Source/Core/AST/Program.cs b/Source/Core/AST/Program.cs
index 10ba93b29..7ac5728ee 100644
--- a/Source/Core/AST/Program.cs
+++ b/Source/Core/AST/Program.cs
@@ -395,7 +395,7 @@ public List<GlobalVariable /*!*/> /*!*/ GlobalVariables
     }
   }
 
-  public readonly ISet<string> NecessaryAssumes = new HashSet<string>();
+  public readonly ISet<string> AllCoveredElements = new HashSet<string>();
 
   public IEnumerable<Block> Blocks()
   {
diff --git a/Source/Core/Monomorphization.cs b/Source/Core/Monomorphization.cs
index 0004d7060..e09b44592 100644
--- a/Source/Core/Monomorphization.cs
+++ b/Source/Core/Monomorphization.cs
@@ -13,7 +13,7 @@ public class MonomorphismChecker : ReadOnlyVisitor
 
     public static bool DoesTypeCtorDeclNeedMonomorphization(TypeCtorDecl typeCtorDecl)
     {
-      return typeCtorDecl.Arity > 0 && typeCtorDecl.FindStringAttribute("builtin") == null;
+      return typeCtorDecl.Arity > 0 && (typeCtorDecl as ICarriesAttributes).FindStringAttribute("builtin") == null;
     }
 
     public static bool IsMonomorphic(Program program)
diff --git a/Source/ExecutionEngine/CommandLineOptions.cs b/Source/ExecutionEngine/CommandLineOptions.cs
index 9faefcd79..938d10495 100644
--- a/Source/ExecutionEngine/CommandLineOptions.cs
+++ b/Source/ExecutionEngine/CommandLineOptions.cs
@@ -201,7 +201,8 @@ public bool NormalizeDeclarationOrder
 
     public bool ImmediatelyAcceptCommands => StratifiedInlining > 0 || ContractInfer;
 
-    public bool ProduceUnsatCores => PrintNecessaryAssumes || EnableUnSatCoreExtract == 1 ||
+    public bool ProduceUnsatCores => TrackVerificationCoverage ||
+                                     EnableUnSatCoreExtract == 1 ||
                                      ContractInfer && (UseUnsatCoreForContractInfer || ExplainHoudini);
 
     public bool BatchModeSolver { get; set; }
@@ -279,10 +280,9 @@ public bool UseUnsatCoreForContractInfer {
 
     public bool PrintAssignment  { get; set; }
 
-    // TODO(wuestholz): Add documentation for this flag.
-    public bool PrintNecessaryAssumes {
-      get => printNecessaryAssumes;
-      set => printNecessaryAssumes = value;
+    public bool TrackVerificationCoverage {
+      get => trackVerificationCoverage;
+      set => trackVerificationCoverage = value;
     }
 
     public int InlineDepth  { get; set; } = -1;
@@ -544,7 +544,7 @@ void ObjectInvariant5()
     private bool reverseHoudiniWorklist = false;
     private bool houdiniUseCrossDependencies = false;
     private bool useUnsatCoreForContractInfer = false;
-    private bool printNecessaryAssumes = false;
+    private bool trackVerificationCoverage = false;
     private bool useProverEvaluate;
     private bool trustMoverTypes = false;
     private bool trustNoninterference = false;
@@ -1297,7 +1297,7 @@ protected override bool ParseOption(string name, CommandLineParseState ps)
               ps.CheckBooleanFlag("crossDependencies", x => houdiniUseCrossDependencies = x) ||
               ps.CheckBooleanFlag("useUnsatCoreForContractInfer", x => useUnsatCoreForContractInfer = x) ||
               ps.CheckBooleanFlag("printAssignment", x => PrintAssignment = x) ||
-              ps.CheckBooleanFlag("printNecessaryAssumes", x => printNecessaryAssumes = x) ||
+              ps.CheckBooleanFlag("trackVerificationCoverage", x => trackVerificationCoverage = x) ||
               ps.CheckBooleanFlag("useProverEvaluate", x => useProverEvaluate = x) ||
               ps.CheckBooleanFlag("deterministicExtractLoops", x => DeterministicExtractLoops = x) ||
               ps.CheckBooleanFlag("verifySeparately", x => VerifySeparately = x) ||
@@ -1508,7 +1508,10 @@ order in which implementations are verified (default: N = 1).
 
      {:id <string>}
        Assign a unique ID to an implementation to be used for verification
-       result caching (default: ""<impl. name>:0"").
+       result caching (default: ""<impl. name>:0""), or assign a unique ID
+       to a statement or contract clause for use in identifying which program
+       elements were necessary to complete verification. The latter form is
+       used by the `/trackVerificationCoverage` option.
 
      {:timeLimit N}
        Set the time limit for verifying a given implementation.
@@ -1896,6 +1899,13 @@ without requiring the user to actually make those changes.
                 This option is implemented by renaming variables and reordering
                 declarations in the input, and by setting solver options that have
                 similar effects.
+  /trackVerificationCoverage
+                Track and report which program elements labeled with an
+                `{:id ...}` attribute were necessary to complete verification.
+                Assumptions, assertions, requires clauses, ensures clauses,
+                assignments, and calls can be labeled for inclusion in this
+                report. This generalizes and replaces the previous
+                (undocumented) `/printNecessaryAssertions` option.
 
   ---- Verification-condition splitting --------------------------------------
 
diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
index b11cc968e..20e799519 100644
--- a/Source/ExecutionEngine/ExecutionEngine.cs
+++ b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -673,8 +673,8 @@ private async Task<PipelineOutcome> VerifyEachImplementation(TextWriter output,
         CleanupRequest(requestId);
       }
 
-      if (Options.PrintNecessaryAssumes && processedProgram.Program.NecessaryAssumes.Any()) {
-        Options.OutputWriter.WriteLine("Necessary assume command(s): {0}", string.Join(", ", processedProgram.Program.NecessaryAssumes.OrderBy(s => s)));
+      if (Options.TrackVerificationCoverage && processedProgram.Program.AllCoveredElements.Any()) {
+        Options.OutputWriter.WriteLine("Elements covered by verification: {0}", string.Join(", ", processedProgram.Program.AllCoveredElements.OrderBy(s => s)));
       }
 
       cce.NonNull(Options.TheProverFactory).Close();
diff --git a/Source/ExecutionEngine/ExecutionEngine.csproj b/Source/ExecutionEngine/ExecutionEngine.csproj
index 968bdab33..897f68d9b 100644
--- a/Source/ExecutionEngine/ExecutionEngine.csproj
+++ b/Source/ExecutionEngine/ExecutionEngine.csproj
@@ -21,6 +21,7 @@
     <ProjectReference Include="..\Houdini\Houdini.csproj" />
     <ProjectReference Include="..\Model\Model.csproj" />
     <ProjectReference Include="..\VCGeneration\VCGeneration.csproj" />
+    <ProjectReference Include="..\Provers\SMTLib\SMTLib.csproj" />
   </ItemGroup>
 
 </Project>
diff --git a/Source/ExecutionEngine/VerificationResult.cs b/Source/ExecutionEngine/VerificationResult.cs
index b1ccf7ab4..0a685c2fd 100644
--- a/Source/ExecutionEngine/VerificationResult.cs
+++ b/Source/ExecutionEngine/VerificationResult.cs
@@ -11,7 +11,7 @@ public sealed class VerificationResult
 {
   private readonly Implementation implementation;
   public readonly string ProgramId;
-  public string MessageIfVerifies => implementation.FindStringAttribute("msg_if_verifies");
+  public string MessageIfVerifies => (implementation as ICarriesAttributes).FindStringAttribute("msg_if_verifies");
   public string Checksum => implementation.Checksum;
   public string DependenciesChecksum => implementation.DependencyChecksum;
 
diff --git a/Source/Houdini/HoudiniSession.cs b/Source/Houdini/HoudiniSession.cs
index 5dc098482..81b0b541e 100644
--- a/Source/Houdini/HoudiniSession.cs
+++ b/Source/Houdini/HoudiniSession.cs
@@ -126,6 +126,7 @@ public class HoudiniStatistics
     private readonly Houdini houdini;
     public HoudiniStatistics stats;
     public List<Counterexample> Counterexamples { get; } = new();
+    public HashSet<string> CoveredElements { get; } = new();
     private VCExpr conjecture;
     private ProverInterface.ErrorHandler handler;
     ConditionGeneration.VerificationResultCollector collector;
diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index fb028650f..fa6ba0c2b 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -112,7 +112,7 @@ protected ErrorHandler(SMTLibOptions options)
       this.options = options;
     }
 
-    public virtual void AddNecessaryAssume(string id)
+    public virtual void AddCoveredElement(string id)
     {
       throw new System.NotImplementedException();
     }
diff --git a/Source/Provers/SMTLib/SMTLibInteractiveTheoremProver.cs b/Source/Provers/SMTLib/SMTLibInteractiveTheoremProver.cs
index d4fe00fad..1f5693470 100644
--- a/Source/Provers/SMTLib/SMTLibInteractiveTheoremProver.cs
+++ b/Source/Provers/SMTLib/SMTLibInteractiveTheoremProver.cs
@@ -223,18 +223,18 @@ public async Task<Outcome> CheckSat(CancellationToken cancellationToken,
               if (resp.Name != "")
               {
                 usedNamedAssumes.Add(resp.Name);
-                if (libOptions.PrintNecessaryAssumes)
+                if (libOptions.TrackVerificationCoverage)
                 {
-                  reporter.AddNecessaryAssume(resp.Name.Substring("aux$$assume$$".Length));
+                  reporter.AddCoveredElement(resp.Name.Substring("aux$$assume$$".Length));
                 }
               }
 
               foreach (var arg in resp.Arguments)
               {
                 usedNamedAssumes.Add(arg.Name);
-                if (libOptions.PrintNecessaryAssumes)
+                if (libOptions.TrackVerificationCoverage)
                 {
-                  reporter.AddNecessaryAssume(arg.Name.Substring("aux$$assume$$".Length));
+                  reporter.AddCoveredElement(arg.Name.Substring("aux$$assume$$".Length));
                 }
               }
             }
diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs
index 6f2aedf36..0985109ee 100644
--- a/Source/Provers/SMTLib/SMTLibLineariser.cs
+++ b/Source/Provers/SMTLib/SMTLibLineariser.cs
@@ -239,7 +239,7 @@ public string ExtractBuiltin(Function f)
     {
       Contract.Requires(f != null);
       string retVal = null;
-      retVal = f.FindStringAttribute("bvbuiltin");
+      retVal = (f as ICarriesAttributes).FindStringAttribute("bvbuiltin");
 
       // It used to be "sign_extend 12" in Simplify, and is "(_ sign_extend 12)" with SMT
       if (retVal != null && (retVal.StartsWith("sign_extend ") || retVal.StartsWith("zero_extend ")))
@@ -249,7 +249,7 @@ public string ExtractBuiltin(Function f)
 
       if (retVal == null)
       {
-        retVal = f.FindStringAttribute("builtin");
+        retVal = (f as ICarriesAttributes).FindStringAttribute("builtin");
       }
 
       if (retVal != null && !LibOptions.UseArrayTheory && SMTLibOpLineariser.ArrayOps.Contains(retVal))
@@ -398,7 +398,7 @@ public bool Visit(VCExprNAry node, LineariserOptions options)
         return true;
       }
 
-      if (node.Op.Equals(VCExpressionGenerator.NamedAssumeOp))
+      if (node.Op.Equals(VCExpressionGenerator.NamedAssumeOp) || node.Op.Equals(VCExpressionGenerator.NamedAssertOp))
       {
         var exprVar = node[0] as VCExprVar;
         NamedAssumes.Add(exprVar);
diff --git a/Source/Provers/SMTLib/SMTLibOptions.cs b/Source/Provers/SMTLib/SMTLibOptions.cs
index c479e4532..354c91979 100644
--- a/Source/Provers/SMTLib/SMTLibOptions.cs
+++ b/Source/Provers/SMTLib/SMTLibOptions.cs
@@ -14,7 +14,7 @@ public interface SMTLibOptions : CoreOptions
     bool ProduceUnsatCores { get; }
     bool ImmediatelyAcceptCommands { get; }
     bool RunningBoogieFromCommandLine { get; }
-    bool PrintNecessaryAssumes { get; }
+    bool TrackVerificationCoverage { get; }
     string ProverPreamble { get; }
     bool TraceDiagnosticsOnTimeout { get; }
     uint TimeLimitPerAssertionInPercent { get; }
diff --git a/Source/Provers/SMTLib/TypeDeclCollector.cs b/Source/Provers/SMTLib/TypeDeclCollector.cs
index dd22da918..632d56942 100644
--- a/Source/Provers/SMTLib/TypeDeclCollector.cs
+++ b/Source/Provers/SMTLib/TypeDeclCollector.cs
@@ -212,11 +212,11 @@ public override bool Visit(VCExprNAry node, bool arg)
         AddDeclaration(string.Format("(declare-fun {0} () Bool)", exprVar.Name));
         AddDeclaration(string.Format("(assert-soft {0} :weight {1})", exprVar.Name, ((VCExprSoftOp) node.Op).Weight));
       }
-      else if (node.Op.Equals(VCExpressionGenerator.NamedAssumeOp))
+      else if (node.Op.Equals(VCExpressionGenerator.NamedAssumeOp) || node.Op.Equals(VCExpressionGenerator.NamedAssertOp))
       {
         var exprVar = node[0] as VCExprVar;
         AddDeclaration(string.Format("(declare-fun {0} () Bool)", exprVar.Name));
-        if (options.PrintNecessaryAssumes)
+        if (options.TrackVerificationCoverage)
         {
           AddDeclaration(string.Format("(assert (! {0} :named {1}))", exprVar.Name, "aux$$" + exprVar.Name));
         }
@@ -270,8 +270,7 @@ public override bool Visit(VCExprVar node, bool arg)
         RegisterType(node.Type);
         string decl =
           "(declare-fun " + printedName + " () " + TypeToString(node.Type) + ")";
-        if (!(printedName.StartsWith("assume$$") || printedName.StartsWith("soft$$") ||
-              printedName.StartsWith("try$$")))
+        if (node.VarKind == VCExprVarKind.Normal)
         {
           AddDeclaration(decl);
         }
diff --git a/Source/VCExpr/QuantifierInstantiationEngine.cs b/Source/VCExpr/QuantifierInstantiationEngine.cs
index 3d83909a6..f0afc70fd 100644
--- a/Source/VCExpr/QuantifierInstantiationEngine.cs
+++ b/Source/VCExpr/QuantifierInstantiationEngine.cs
@@ -1,4 +1,5 @@
 using System;
+using System.Collections.Concurrent;
 using System.Collections.Generic;
 using System.Diagnostics.Contracts;
 using System.Linq;
@@ -50,7 +51,7 @@ public QuantifierInstantiationInfo(Dictionary<VCExprVar, HashSet<string>> boundV
     private string skolemConstantNamePrefix;
     internal VCExpressionGenerator vcExprGen;
     private Boogie2VCExprTranslator exprTranslator;
-    internal static Dictionary<string, Type> labelToType = new();
+    internal static ConcurrentDictionary<string, Type> labelToType = new();
 
     public static VCExpr Instantiate(Implementation impl, VCExpressionGenerator vcExprGen, Boogie2VCExprTranslator exprTranslator, VCExpr vcExpr)
     {
diff --git a/Source/VCExpr/VCExprAST.cs b/Source/VCExpr/VCExprAST.cs
index a713c0987..a8f68dcbe 100644
--- a/Source/VCExpr/VCExprAST.cs
+++ b/Source/VCExpr/VCExprAST.cs
@@ -1771,6 +1771,15 @@ public override Result Accept<Result, Arg>(
   // Binders (quantifiers and let-expressions). We introduce our own class for
   // term variables, but use the Boogie-AST class for type variables
 
+  public enum VCExprVarKind
+  {
+    Normal, // A normal variable
+    Soft,   // A variable used for tracking an assumption labeled with the `:soft` attribute
+    Try,    // A variable used for tracking an assumption labeled with the `:try` attribute
+    Assert, // A variable used for tracking an assertion labeled with the `:id` attribute
+    Assume  // A variable used for tracking an assumption labeled with the `:id` attribute
+  }
+
   public class VCExprVar : VCExpr
   {
     // the name of the variable. Note that the name is not used for comparison,
@@ -1788,6 +1797,8 @@ public readonly string /*!*/
     private readonly Type /*!*/
       VarType;
 
+    public VCExprVarKind VarKind { get; }
+
     public override Type /*!*/ Type
     {
       get
@@ -1797,12 +1808,26 @@ public override Type /*!*/ Type
       }
     }
 
-    internal VCExprVar(string name, Type type)
+    internal VCExprVar(string name, Type type, VCExprVarKind kind = VCExprVarKind.Normal)
     {
       Contract.Requires(type != null);
       Contract.Requires(name != null);
-      this.Name = name;
+      this.Name = KindPrefix(kind) + name;
       this.VarType = type;
+      this.VarKind = kind;
+    }
+
+    private string KindPrefix(VCExprVarKind kind)
+    {
+      return kind switch
+      {
+        VCExprVarKind.Assert => "assert$$",
+        VCExprVarKind.Assume => "assume$$",
+        VCExprVarKind.Soft => "soft$$",
+        VCExprVarKind.Try => "try$$",
+        VCExprVarKind.Normal => "",
+        _ => throw new cce.UnreachableException()
+      };
     }
 
     public override Result Accept<Result, Arg>(IVCExprVisitor<Result, Arg> visitor, Arg arg)
diff --git a/Source/VCExpr/VCExpressionGenerator.cs b/Source/VCExpr/VCExpressionGenerator.cs
index cf898fa38..6cc61ce05 100644
--- a/Source/VCExpr/VCExpressionGenerator.cs
+++ b/Source/VCExpr/VCExpressionGenerator.cs
@@ -442,9 +442,12 @@ int AndSize(VCExpr e)
 
     public static readonly VCExprOp TimeoutDiagnosticsOp = new VCExprCustomOp("timeoutDiagnostics", 1, Type.Bool);
 
+    // These operators are temporarily added to VCExprs to track where labels for optimization and unsat
+    // core generation should go, but don't appear in the final SMT-Lib output.
     public static readonly VCExprOp MinimizeOp = new VCExprCustomOp("minimize##dummy", 2, Type.Bool);
     public static readonly VCExprOp MaximizeOp = new VCExprCustomOp("maximize##dummy", 2, Type.Bool);
     public static readonly VCExprOp NamedAssumeOp = new VCExprCustomOp("named_assume##dummy", 2, Type.Bool);
+    public static readonly VCExprOp NamedAssertOp = new VCExprCustomOp("named_assert##dummy", 2, Type.Bool);
 
     public VCExprOp BoogieFunctionOp(Function func)
     {
@@ -780,12 +783,12 @@ public VCTrigger Trigger(bool pos, params VCExpr[] exprs)
 
     // Reference to a bound or free variable
 
-    public VCExprVar Variable(string name, Type type)
+    public VCExprVar Variable(string name, Type type, VCExprVarKind kind = VCExprVarKind.Normal)
     {
       Contract.Requires(type != null);
       Contract.Requires(name != null);
       Contract.Ensures(Contract.Result<VCExprVar>() != null);
-      return new VCExprVar(name, type);
+      return new VCExprVar(name, type, kind);
     }
   }
 }
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index bb4b554aa..d02da1aab 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -11,6 +11,7 @@
 using System.IO;
 using System.Runtime.CompilerServices;
 using System.Threading.Tasks;
+using Microsoft.Boogie.VCExprAST;
 using VC;
 using Set = Microsoft.Boogie.GSet<object>;
 
@@ -253,7 +254,10 @@ protected static void InjectPreconditions(VCGenOptions options, ImplementationRu
       {
         Contract.Assert(req != null);
         Expr e = Substituter.Apply(formalProcImplSubst, req.Condition);
-        Cmd c = new AssumeCmd(req.tok, e);
+        AssumeCmd c = new AssumeCmd(req.tok, e);
+        // Copy any {:id ...} from the precondition to the assumption, so
+        // we can track it while analyzing verification coverage.
+        (c as ICarriesAttributes).CopyIdFrom(req.tok, req);
         c.IrrelevantForChecksumComputation = true;
         insertionPoint.Cmds.Add(c);
         if (debugWriter != null)
@@ -316,6 +320,9 @@ protected static void InjectPostConditions(VCGenOptions options, ImplementationR
           ensCopy.Condition = e;
           AssertEnsuresCmd c = new AssertEnsuresCmd(ensCopy);
           c.ErrorDataEnhanced = ensCopy.ErrorDataEnhanced;
+          // Copy any {:id ...} from the postcondition to the assumption, so
+          // we can track it while analyzing verification coverage.
+          (c as ICarriesAttributes).CopyIdFrom(ens.tok, ens);
           unifiedExitBlock.Cmds.Add(c);
           if (debugWriter != null)
           {
@@ -1093,7 +1100,7 @@ private void AddDebugInfo(Cmd c, Dictionary<Variable, Expr> incarnationMap, List
     /// In that case, it remembers the incarnation map BEFORE the havoc.
     /// Meanwhile, record any information needed to later reconstruct a model view.
     /// </summary>
-    protected void TurnIntoPassiveCmd(TextWriter traceWriter, Cmd c, Block enclosingBlock, Dictionary<Variable, Expr> incarnationMap, Substitution oldFrameSubst,
+    private void TurnIntoPassiveCmd(TextWriter traceWriter, Cmd c, Block enclosingBlock, Dictionary<Variable, Expr> incarnationMap, Substitution oldFrameSubst,
       List<Cmd> passiveCmds, ModelViewInfo mvInfo)
     {
       Contract.Requires(c != null);
@@ -1104,429 +1111,443 @@ protected void TurnIntoPassiveCmd(TextWriter traceWriter, Cmd c, Block enclosing
       Contract.Requires(mvInfo != null);
 
       AddDebugInfo(c, incarnationMap, passiveCmds);
-      Substitution incarnationSubst = Substituter.SubstitutionFromDictionary(incarnationMap);
+      var incarnationSubst = Substituter.SubstitutionFromDictionary(incarnationMap);
 
-      Microsoft.Boogie.VCExprAST.QuantifierInstantiationEngine.SubstituteIncarnationInInstantiationSources(c, incarnationSubst);
+      QuantifierInstantiationEngine.SubstituteIncarnationInInstantiationSources(c, incarnationSubst);
 
-      #region assert/assume P |--> assert/assume P[x := in(x)], out := in
+      if (c is PredicateCmd predicateCmd)
+      {
+        PacifyPredicateCmd(traceWriter, enclosingBlock, incarnationMap, oldFrameSubst, passiveCmds, mvInfo, predicateCmd, incarnationSubst);
+      } else if (c is AssignCmd assignCmd)
+      {
+        PacifyAssignCmd(traceWriter, incarnationMap, oldFrameSubst, passiveCmds, assignCmd, incarnationSubst);
+      }
+      else if (c is HavocCmd hc)
+      {
+        PacifyHavocCmd(incarnationMap, oldFrameSubst, passiveCmds, hc);
+      }
+      else if (c is CommentCmd)
+      {
+        // comments are just for debugging and don't affect verification
+      }
+      else if (c is SugaredCmd sug)
+      {
+        Cmd cmd = sug.GetDesugaring(Options);
+        Contract.Assert(cmd != null);
+        TurnIntoPassiveCmd(traceWriter, cmd, enclosingBlock, incarnationMap, oldFrameSubst, passiveCmds, mvInfo);
+      }
+      else if (c is StateCmd st)
+      {
+        PacifyStateCmd(traceWriter, enclosingBlock, incarnationMap, oldFrameSubst, passiveCmds, mvInfo, st);
+      }
+      else
+      {
+        Debug.Fail(
+          "Internal Error: Passive transformation handed a command that is not one of assert,assume,havoc,assign.");
+      } 
 
-      if (c is PredicateCmd)
+      // We remember if we have put an havoc statement into a passive form
+      if (!(c is HavocCmd))
       {
-        Contract.Assert(c is AssertCmd || c is AssumeCmd); // otherwise, unexpected PredicateCmd type
+        this.preHavocIncarnationMap = null;
+      }
+      // else: it has already been set by the case for the HavocCmd
+    }
 
-        PredicateCmd pc = (PredicateCmd) c.Clone();
-        Contract.Assert(pc != null);
+    private void PacifyStateCmd(TextWriter traceWriter, Block enclosingBlock, Dictionary<Variable, Expr> incarnationMap,
+      Substitution oldFrameSubst, List<Cmd> passiveCmds, ModelViewInfo mvInfo, StateCmd st)
+    {
+      this.preHavocIncarnationMap = null; // we do not need to remember the previous incarnations
 
-        QKeyValue current = pc.Attributes;
-        while (current != null)
+      // account for any where clauses among the local variables
+      foreach (Variable v in st.Locals)
+      {
+        Contract.Assert(v != null);
+        Expr w = v.TypedIdent.WhereExpr;
+        if (w != null)
         {
-          if (current.Key == "minimize" || current.Key == "maximize")
-          {
-            Contract.Assume(current.Params.Count == 1);
-            var param = current.Params[0] as Expr;
-            Contract.Assume(param != null && (param.Type.IsInt || param.Type.IsReal || param.Type.IsBv));
-            current.ClearParams();
-            current.AddParam(Substituter.ApplyReplacingOldExprs(incarnationSubst, oldFrameSubst, param));
-          }
-
-          if (current.Key == "verified_under")
-          {
-            Contract.Assume(current.Params.Count == 1);
-            var param = current.Params[0] as Expr;
-            Contract.Assume(param != null && param.Type.IsBool);
-            current.ClearParams();
-            current.AddParam(Substituter.ApplyReplacingOldExprs(incarnationSubst, oldFrameSubst, param));
-          }
-
-          current = current.Next;
+          passiveCmds.Add(new AssumeCmd(v.tok, w));
         }
+      }
 
-        Expr copy = Substituter.ApplyReplacingOldExprs(incarnationSubst, oldFrameSubst, pc.Expr);
-        if (Options.ModelViewFile != null && pc is AssumeCmd captureStateAssumeCmd)
-        {
-          string description = QKeyValue.FindStringAttribute(pc.Attributes, "captureState");
-          if (description != null)
-          {
-            if (!mvInfo.BlockToCapturePointIndex.TryGetValue(enclosingBlock, out var points)) {
-              points = new List<(AssumeCmd, ModelViewInfo.Mapping)>();
-              mvInfo.BlockToCapturePointIndex[enclosingBlock] = points;
-            }
-            var mapping = new ModelViewInfo.Mapping(description, new Dictionary<Variable, Expr>(incarnationMap));
-            points.Add((captureStateAssumeCmd, mapping));
-          }
-        }
+      // do the sub-commands
+      foreach (Cmd s in st.Cmds)
+      {
+        Contract.Assert(s != null);
+        TurnIntoPassiveCmd(traceWriter, s, enclosingBlock, incarnationMap, oldFrameSubst, passiveCmds, mvInfo);
+      }
 
-        Contract.Assert(copy != null);
-        var dropCmd = false;
-        var relevantAssumpVars = currentImplementation != null
-          ? currentImplementation.RelevantInjectedAssumptionVariables(incarnationMap)
-          : new List<LocalVariable>();
-        var relevantDoomedAssumpVars = currentImplementation != null
-          ? currentImplementation.RelevantDoomedInjectedAssumptionVariables(incarnationMap)
-          : new List<LocalVariable>();
-        var checksum = pc.Checksum;
-        if (pc is AssertCmd)
-        {
-          var ac = (AssertCmd) pc;
-          ac.OrigExpr = ac.Expr;
-          Contract.Assert(ac.IncarnationMap == null);
-          ac.IncarnationMap = (Dictionary<Variable, Expr>) cce.NonNull(new Dictionary<Variable, Expr>(incarnationMap));
+      // remove the local variables from the incarnation map
+      foreach (Variable v in st.Locals)
+      {
+        Contract.Assert(v != null);
+        incarnationMap.Remove(v);
+      }
+    }
 
-          var subsumption = Wlp.Subsumption(Options, ac);
-          if (relevantDoomedAssumpVars.Any())
-          {
-            TraceCachingAction(traceWriter, pc, CachingAction.DoNothingToAssert);
-          }
-          else if (currentImplementation != null
-                   && currentImplementation.HasCachedSnapshot
-                   && checksum != null
-                   && currentImplementation.IsAssertionChecksumInCachedSnapshot(checksum)
-                   && !currentImplementation.IsErrorChecksumInCachedSnapshot(checksum))
-          {
-            if (!currentImplementation.AnyErrorsInCachedSnapshot
-                && currentImplementation.InjectedAssumptionVariables.Count == 1
-                && relevantAssumpVars.Count == 1)
-            {
-              TraceCachingAction(traceWriter, pc, CachingAction.MarkAsPartiallyVerified);
-            }
-            else
-            {
-              var assmVars = currentImplementation.ConjunctionOfInjectedAssumptionVariables(incarnationMap, out var isTrue);
-              TraceCachingAction(traceWriter, pc,
-                !isTrue ? CachingAction.MarkAsPartiallyVerified : CachingAction.MarkAsFullyVerified);
-              var litExpr = ac.Expr as LiteralExpr;
-              if (litExpr == null || !litExpr.IsTrue)
-              {
-                ac.MarkAsVerifiedUnder(assmVars);
-              }
-              else
-              {
-                dropCmd = true;
-              }
-            }
-          }
-          else if (currentImplementation != null
-                   && currentImplementation.HasCachedSnapshot
-                   && relevantAssumpVars.Count == 0
-                   && checksum != null
-                   && currentImplementation.IsAssertionChecksumInCachedSnapshot(checksum)
-                   && currentImplementation.IsErrorChecksumInCachedSnapshot(checksum))
-          {
-            TraceCachingAction(traceWriter, pc, CachingAction.RecycleError);
-            ac.MarkAsVerifiedUnder(Expr.True);
-            currentImplementation.AddRecycledFailingAssertion(ac);
-            pc.Attributes = new QKeyValue(Token.NoToken, "recycled_failing_assertion", new List<object>(),
-              pc.Attributes);
-          }
-          else
-          {
-            TraceCachingAction(traceWriter, pc, CachingAction.DoNothingToAssert);
-          }
-        }
-        else if (pc is AssumeCmd
-                 && QKeyValue.FindBoolAttribute(pc.Attributes, "precondition_previous_snapshot")
-                 && pc.SugaredCmdChecksum != null)
+    /// <summary>
+    /// havoc w |--> assume whereClauses, out := in( w |-> w' )
+    /// </summary>
+    private void PacifyHavocCmd(Dictionary<Variable, Expr> incarnationMap, Substitution oldFrameSubst, List<Cmd> passiveCmds,
+      HavocCmd hc)
+    {
+      if (this.preHavocIncarnationMap == null
+         ) // Save a copy of the incarnation map (at the top of a sequence of havoc statements)
+      {
+        this.preHavocIncarnationMap = new Dictionary<Variable, Expr>(incarnationMap);
+      }
+
+      Contract.Assert(hc != null);
+      // If an assumption variable for postconditions is included here, it must have been assigned within a loop.
+      // We do not need to havoc it if we have performed a modular proof of the loop (i.e., using only the loop
+      // invariant) in the previous snapshot and, consequently, the corresponding assumption did not affect the
+      // anything after the loop. We can achieve this by simply not updating/adding it in the incarnation map.
+      List<IdentifierExpr> havocVars = hc.Vars.Where(v =>
+          !(QKeyValue.FindBoolAttribute(v.Decl.Attributes, "assumption") && v.Decl.Name.StartsWith("a##cached##")))
+        .ToList();
+      // First, compute the new incarnations
+      foreach (IdentifierExpr ie in havocVars)
+      {
+        Contract.Assert(ie != null);
+        if (!(ie.Decl is Incarnation))
         {
-          if (!relevantDoomedAssumpVars.Any()
-              && currentImplementation.HasCachedSnapshot
-              && currentImplementation.IsAssertionChecksumInCachedSnapshot(pc.SugaredCmdChecksum)
-              && !currentImplementation.IsErrorChecksumInCachedSnapshot(pc.SugaredCmdChecksum))
-          {
-            var assmVars = currentImplementation.ConjunctionOfInjectedAssumptionVariables(incarnationMap, out var isTrue);
-            if (!isTrue)
-            {
-              copy = LiteralExpr.Imp(assmVars, copy);
-              TraceCachingAction(traceWriter, pc, CachingAction.MarkAsPartiallyVerified);
-            }
-            else
-            {
-              TraceCachingAction(traceWriter, pc, CachingAction.MarkAsFullyVerified);
-            }
-          }
-          else
-          {
-            TraceCachingAction(traceWriter, pc, CachingAction.DropAssume);
-            dropCmd = true;
-          }
+          Variable x = cce.NonNull(ie.Decl);
+          Variable x_prime = CreateIncarnation(x, c);
+          incarnationMap[x] = new IdentifierExpr(x_prime.tok, x_prime);
         }
-        else if (pc is AssumeCmd && QKeyValue.FindBoolAttribute(pc.Attributes, "assumption_variable_initialization"))
+      }
+
+      // Then, perform the assume of the where clauses, using the updated incarnations
+      Substitution updatedIncarnationSubst = Substituter.SubstitutionFromDictionary(incarnationMap);
+      foreach (IdentifierExpr ie in havocVars)
+      {
+        Contract.Assert(ie != null);
+        if (!(ie.Decl is Incarnation))
         {
-          var identExpr = pc.Expr as IdentifierExpr;
-          if (identExpr != null && identExpr.Decl != null && !incarnationMap.ContainsKey(identExpr.Decl))
+          Variable x = cce.NonNull(ie.Decl);
+          Expr w = x.TypedIdent.WhereExpr;
+          if (w != null)
           {
-            incarnationMap[identExpr.Decl] = LiteralExpr.True;
-            dropCmd = true;
+            Expr copy = Substituter.ApplyReplacingOldExprs(updatedIncarnationSubst, oldFrameSubst, w);
+            passiveCmds.Add(new AssumeCmd(c.tok, copy));
           }
         }
+      }
 
-        pc.Expr = copy;
-        if (!dropCmd)
+      // Add the following assume-statement for each assumption variable 'v', where 'v_post' is the new incarnation and 'v_pre' is the old one:
+      // assume v_post ==> v_pre;
+      foreach (IdentifierExpr ie in havocVars)
+      {
+        if (QKeyValue.FindBoolAttribute(ie.Decl.Attributes, "assumption"))
         {
-          passiveCmds.Add(pc);
+          var preInc = (Expr)(preHavocIncarnationMap[ie.Decl].Clone());
+          var postInc = (Expr)(incarnationMap[ie.Decl].Clone());
+          passiveCmds.Add(new AssumeCmd(c.tok, Expr.Imp(postInc, preInc)));
         }
       }
+    }
 
-      #endregion
+    private void PacifyAssignCmd(TextWriter traceWriter, Dictionary<Variable, Expr> incarnationMap, Substitution oldFrameSubst,
+      List<Cmd> passiveCmds, AssignCmd assignCmd, Substitution incarnationSubst)
+    {
+      // x1 := E1, x2 := E2, ... |--> assume x1' = E1[in] & x2' = E2[in], out := in( x |-> x' ) [except as noted below]
+      AssignCmd assign = assignCmd.AsSimpleAssignCmd; // first remove map assignments
+      Contract.Assert(assign != null);
 
-      #region x1 := E1, x2 := E2, ... |--> assume x1' = E1[in] & x2' = E2[in], out := in( x |-> x' ) [except as noted below]
+      #region Substitute all variables in E with the current map
 
-      else if (c is AssignCmd)
+      List<Expr> copies = new List<Expr>();
+      foreach (Expr e in assign.Rhss)
       {
-        AssignCmd assign = ((AssignCmd) c).AsSimpleAssignCmd; // first remove map assignments
-        Contract.Assert(assign != null);
+        Contract.Assert(e != null);
+        copies.Add(Substituter.ApplyReplacingOldExprs(incarnationSubst,
+          oldFrameSubst,
+          e));
+      }
+
+      #endregion
 
-        #region Substitute all variables in E with the current map
+      List<Expr /*!>!*/> assumptions = new List<Expr>();
+      // it might be too slow to create a new dictionary each time ...
+      IDictionary<Variable, Expr> newIncarnationMappings =
+        new Dictionary<Variable, Expr>();
 
-        List<Expr> copies = new List<Expr>();
-        foreach (Expr e in assign.Rhss)
+      for (int i = 0; i < assign.Lhss.Count; ++i)
+      {
+        IdentifierExpr lhsIdExpr =
+          cce.NonNull((SimpleAssignLhs)assign.Lhss[i]).AssignedVariable;
+        Variable lhs = cce.NonNull(lhsIdExpr.Decl);
+        Contract.Assert(lhs != null);
+        Expr rhs = assign.Rhss[i];
+        Contract.Assert(rhs != null);
+
+        // don't create incarnations for assignments of literals or single variables.
+        if (rhs is LiteralExpr)
         {
-          Contract.Assert(e != null);
-          copies.Add(Substituter.ApplyReplacingOldExprs(incarnationSubst,
-            oldFrameSubst,
-            e));
+          incarnationMap[lhs] = rhs;
         }
-
-        #endregion
-
-        List<Expr /*!>!*/> assumptions = new List<Expr>();
-        // it might be too slow to create a new dictionary each time ...
-        IDictionary<Variable, Expr> newIncarnationMappings =
-          new Dictionary<Variable, Expr>();
-
-        for (int i = 0; i < assign.Lhss.Count; ++i)
+        else if (rhs is IdentifierExpr)
         {
-          IdentifierExpr lhsIdExpr =
-            cce.NonNull((SimpleAssignLhs) assign.Lhss[i]).AssignedVariable;
-          Variable lhs = cce.NonNull(lhsIdExpr.Decl);
-          Contract.Assert(lhs != null);
-          Expr rhs = assign.Rhss[i];
-          Contract.Assert(rhs != null);
-
-          // don't create incarnations for assignments of literals or single variables.
-          if (rhs is LiteralExpr)
-          {
-            incarnationMap[lhs] = rhs;
-          }
-          else if (rhs is IdentifierExpr)
+          IdentifierExpr ie = (IdentifierExpr)rhs;
+          if (incarnationMap.ContainsKey(cce.NonNull(ie.Decl)))
           {
-            IdentifierExpr ie = (IdentifierExpr) rhs;
-            if (incarnationMap.ContainsKey(cce.NonNull(ie.Decl)))
-            {
-              newIncarnationMappings[lhs] = cce.NonNull((Expr) incarnationMap[ie.Decl]);
-            }
-            else
-            {
-              newIncarnationMappings[lhs] = ie;
-            }
+            newIncarnationMappings[lhs] = cce.NonNull((Expr)incarnationMap[ie.Decl]);
           }
           else
           {
-            IdentifierExpr x_prime_exp = null;
+            newIncarnationMappings[lhs] = ie;
+          }
+        }
+        else
+        {
+          IdentifierExpr x_prime_exp = null;
 
-            #region Make a new incarnation, x', for variable x, but only if x is *not* already an incarnation
+          #region Make a new incarnation, x', for variable x, but only if x is *not* already an incarnation
 
-            if (lhs is Incarnation)
-            {
-              // incarnations are already written only once, no need to make an incarnation of an incarnation
-              x_prime_exp = lhsIdExpr;
-            }
-            else
-            {
-              Variable v = CreateIncarnation(lhs, c);
-              x_prime_exp = new IdentifierExpr(lhsIdExpr.tok, v);
-              newIncarnationMappings[lhs] = x_prime_exp;
-            }
+          if (lhs is Incarnation)
+          {
+            // incarnations are already written only once, no need to make an incarnation of an incarnation
+            x_prime_exp = lhsIdExpr;
+          }
+          else
+          {
+            Variable v = CreateIncarnation(lhs, c);
+            x_prime_exp = new IdentifierExpr(lhsIdExpr.tok, v);
+            newIncarnationMappings[lhs] = x_prime_exp;
+          }
 
-            #endregion
+          #endregion
 
-            var nAryExpr = copies[i] as NAryExpr;
-            if (nAryExpr != null)
+          var nAryExpr = copies[i] as NAryExpr;
+          if (nAryExpr != null)
+          {
+            var binOp = nAryExpr.Fun as BinaryOperator;
+            if (binOp != null
+                && binOp.Op == BinaryOperator.Opcode.And)
             {
-              var binOp = nAryExpr.Fun as BinaryOperator;
-              if (binOp != null
-                  && binOp.Op == BinaryOperator.Opcode.And)
+              var arg0 = nAryExpr.Args[0] as LiteralExpr;
+              var arg1 = nAryExpr.Args[1] as LiteralExpr;
+              if ((arg0 != null && arg0.IsTrue) || (arg1 != null && arg1.IsFalse))
               {
-                var arg0 = nAryExpr.Args[0] as LiteralExpr;
-                var arg1 = nAryExpr.Args[1] as LiteralExpr;
-                if ((arg0 != null && arg0.IsTrue) || (arg1 != null && arg1.IsFalse))
-                {
-                  // Replace the expressions "true && arg1" or "arg0 && false" by "arg1".
-                  copies[i] = nAryExpr.Args[1];
-                }
+                // Replace the expressions "true && arg1" or "arg0 && false" by "arg1".
+                copies[i] = nAryExpr.Args[1];
               }
             }
+          }
 
-            #region Create an assume command with the new variable
-
-            assumptions.Add(TypedExprEq(x_prime_exp, copies[i],
-              x_prime_exp.Decl != null && x_prime_exp.Decl.Name.Contains("a##cached##")));
+          #region Create an assume command with the new variable
 
-            #endregion
-          }
-        }
+          assumptions.Add(TypedExprEq(x_prime_exp, copies[i],
+            x_prime_exp.Decl != null && x_prime_exp.Decl.Name.Contains("a##cached##")));
 
-        foreach (KeyValuePair<Variable, Expr> pair in newIncarnationMappings)
-        {
-          Contract.Assert(pair.Key != null && pair.Value != null);
-          incarnationMap[pair.Key] = pair.Value;
+          #endregion
         }
+      }
 
-        if (assumptions.Count > 0)
-        {
-          Expr assumption = assumptions[0];
+      foreach (KeyValuePair<Variable, Expr> pair in newIncarnationMappings)
+      {
+        Contract.Assert(pair.Key != null && pair.Value != null);
+        incarnationMap[pair.Key] = pair.Value;
+      }
 
-          for (int i = 1; i < assumptions.Count; ++i)
-          {
-            Contract.Assert(assumption != null);
-            assumption = Expr.And(assumption, assumptions[i]);
-          }
+      if (assumptions.Count > 0)
+      {
+        Expr assumption = assumptions[0];
 
-          passiveCmds.Add(new AssumeCmd(c.tok, assumption));
+        for (int i = 1; i < assumptions.Count; ++i)
+        {
+          Contract.Assert(assumption != null);
+          assumption = Expr.And(assumption, assumptions[i]);
         }
 
-        if (currentImplementation != null
-            && currentImplementation.HasCachedSnapshot
-            && !currentImplementation.AnyErrorsInCachedSnapshot
-            && currentImplementation.DoomedInjectedAssumptionVariables.Count == 0
-            && currentImplementation.InjectedAssumptionVariables.Count == 1
-            && assign.Lhss.Count == 1)
+        var assumeCmd = new AssumeCmd(assignCmd.tok, assumption);
+        // Copy any {:id ...} from the assignment to the assumption, so
+        // we can track it while analyzing verification coverage.
+        (assumeCmd as ICarriesAttributes).CopyIdFrom(assign.tok, assign);
+        passiveCmds.Add(assumeCmd);
+      }
+
+      if (currentImplementation != null
+          && currentImplementation.HasCachedSnapshot
+          && !currentImplementation.AnyErrorsInCachedSnapshot
+          && currentImplementation.DoomedInjectedAssumptionVariables.Count == 0
+          && currentImplementation.InjectedAssumptionVariables.Count == 1
+          && assign.Lhss.Count == 1)
+      {
+        var identExpr = assign.Lhss[0].AsExpr as IdentifierExpr;
+        if (identExpr != null && identExpr.Decl != null &&
+            QKeyValue.FindBoolAttribute(identExpr.Decl.Attributes, "assumption") &&
+            incarnationMap.TryGetValue(identExpr.Decl, out var incarnation))
         {
-          var identExpr = assign.Lhss[0].AsExpr as IdentifierExpr;
-          if (identExpr != null && identExpr.Decl != null &&
-              QKeyValue.FindBoolAttribute(identExpr.Decl.Attributes, "assumption") &&
-              incarnationMap.TryGetValue(identExpr.Decl, out var incarnation))
-          {
-            TraceCachingAction(traceWriter, assign, CachingAction.AssumeNegationOfAssumptionVariable);
-            passiveCmds.Add(new AssumeCmd(c.tok, Expr.Not(incarnation)));
-          }
+          TraceCachingAction(traceWriter, assign, CachingAction.AssumeNegationOfAssumptionVariable);
+          passiveCmds.Add(new AssumeCmd(c.tok, Expr.Not(incarnation)));
         }
       }
+    }
 
-      #endregion
+    /// <summary>
+    /// assert/assume P |--> assert/assume P[x := in(x)], out := in
+    /// </summary>
+    private void PacifyPredicateCmd(TextWriter traceWriter, Block enclosingBlock, Dictionary<Variable, Expr> incarnationMap,
+      Substitution oldFrameSubst, List<Cmd> passiveCmds, ModelViewInfo mvInfo, PredicateCmd predicateCmd,
+      Substitution incarnationSubst)
+    {
+      Contract.Assert(c is AssertCmd || c is AssumeCmd); // otherwise, unexpected PredicateCmd type
 
-      #region havoc w |--> assume whereClauses, out := in( w |-> w' )
+      PredicateCmd pc = (PredicateCmd)predicateCmd.Clone();
+      Contract.Assert(pc != null);
 
-      else if (c is HavocCmd)
+      QKeyValue current = pc.Attributes;
+      while (current != null)
       {
-        if (this.preHavocIncarnationMap == null
-        ) // Save a copy of the incarnation map (at the top of a sequence of havoc statements)
+        if (current.Key == "minimize" || current.Key == "maximize")
         {
-          this.preHavocIncarnationMap = new Dictionary<Variable, Expr>(incarnationMap);
+          Contract.Assume(current.Params.Count == 1);
+          var param = current.Params[0] as Expr;
+          Contract.Assume(param != null && (param.Type.IsInt || param.Type.IsReal || param.Type.IsBv));
+          current.ClearParams();
+          current.AddParam(Substituter.ApplyReplacingOldExprs(incarnationSubst, oldFrameSubst, param));
         }
 
-        HavocCmd hc = (HavocCmd) c;
-        Contract.Assert(c != null);
-        // If an assumption variable for postconditions is included here, it must have been assigned within a loop.
-        // We do not need to havoc it if we have performed a modular proof of the loop (i.e., using only the loop
-        // invariant) in the previous snapshot and, consequently, the corresponding assumption did not affect the
-        // anything after the loop. We can achieve this by simply not updating/adding it in the incarnation map.
-        List<IdentifierExpr> havocVars = hc.Vars.Where(v =>
-            !(QKeyValue.FindBoolAttribute(v.Decl.Attributes, "assumption") && v.Decl.Name.StartsWith("a##cached##")))
-          .ToList();
-        // First, compute the new incarnations
-        foreach (IdentifierExpr ie in havocVars)
+        if (current.Key == "verified_under")
+        {
+          Contract.Assume(current.Params.Count == 1);
+          var param = current.Params[0] as Expr;
+          Contract.Assume(param != null && param.Type.IsBool);
+          current.ClearParams();
+          current.AddParam(Substituter.ApplyReplacingOldExprs(incarnationSubst, oldFrameSubst, param));
+        }
+
+        current = current.Next;
+      }
+
+      Expr copy = Substituter.ApplyReplacingOldExprs(incarnationSubst, oldFrameSubst, pc.Expr);
+      if (Options.ModelViewFile != null && pc is AssumeCmd captureStateAssumeCmd)
+      {
+        string description = QKeyValue.FindStringAttribute(pc.Attributes, "captureState");
+        if (description != null)
         {
-          Contract.Assert(ie != null);
-          if (!(ie.Decl is Incarnation))
+          if (!mvInfo.BlockToCapturePointIndex.TryGetValue(enclosingBlock, out var points))
           {
-            Variable x = cce.NonNull(ie.Decl);
-            Variable x_prime = CreateIncarnation(x, c);
-            incarnationMap[x] = new IdentifierExpr(x_prime.tok, x_prime);
+            points = new List<(AssumeCmd, ModelViewInfo.Mapping)>();
+            mvInfo.BlockToCapturePointIndex[enclosingBlock] = points;
           }
+
+          var mapping = new ModelViewInfo.Mapping(description, new Dictionary<Variable, Expr>(incarnationMap));
+          points.Add((captureStateAssumeCmd, mapping));
         }
+      }
 
-        // Then, perform the assume of the where clauses, using the updated incarnations
-        Substitution updatedIncarnationSubst = Substituter.SubstitutionFromDictionary(incarnationMap);
-        foreach (IdentifierExpr ie in havocVars)
+      Contract.Assert(copy != null);
+      var dropCmd = false;
+      var relevantAssumpVars = currentImplementation != null
+        ? currentImplementation.RelevantInjectedAssumptionVariables(incarnationMap)
+        : new List<LocalVariable>();
+      var relevantDoomedAssumpVars = currentImplementation != null
+        ? currentImplementation.RelevantDoomedInjectedAssumptionVariables(incarnationMap)
+        : new List<LocalVariable>();
+      var checksum = pc.Checksum;
+      if (pc is AssertCmd)
+      {
+        var ac = (AssertCmd)pc;
+        ac.OrigExpr = ac.Expr;
+        Contract.Assert(ac.IncarnationMap == null);
+        ac.IncarnationMap = (Dictionary<Variable, Expr>)cce.NonNull(new Dictionary<Variable, Expr>(incarnationMap));
+
+        var subsumption = Wlp.Subsumption(Options, ac);
+        if (relevantDoomedAssumpVars.Any())
+        {
+          TraceCachingAction(traceWriter, pc, CachingAction.DoNothingToAssert);
+        }
+        else if (currentImplementation != null
+                 && currentImplementation.HasCachedSnapshot
+                 && checksum != null
+                 && currentImplementation.IsAssertionChecksumInCachedSnapshot(checksum)
+                 && !currentImplementation.IsErrorChecksumInCachedSnapshot(checksum))
         {
-          Contract.Assert(ie != null);
-          if (!(ie.Decl is Incarnation))
+          if (!currentImplementation.AnyErrorsInCachedSnapshot
+              && currentImplementation.InjectedAssumptionVariables.Count == 1
+              && relevantAssumpVars.Count == 1)
+          {
+            TraceCachingAction(traceWriter, pc, CachingAction.MarkAsPartiallyVerified);
+          }
+          else
           {
-            Variable x = cce.NonNull(ie.Decl);
-            Expr w = x.TypedIdent.WhereExpr;
-            if (w != null)
+            var assmVars =
+              currentImplementation.ConjunctionOfInjectedAssumptionVariables(incarnationMap, out var isTrue);
+            TraceCachingAction(traceWriter, pc,
+              !isTrue ? CachingAction.MarkAsPartiallyVerified : CachingAction.MarkAsFullyVerified);
+            var litExpr = ac.Expr as LiteralExpr;
+            if (litExpr == null || !litExpr.IsTrue)
             {
-              Expr copy = Substituter.ApplyReplacingOldExprs(updatedIncarnationSubst, oldFrameSubst, w);
-              passiveCmds.Add(new AssumeCmd(c.tok, copy));
+              ac.MarkAsVerifiedUnder(assmVars);
+            }
+            else
+            {
+              dropCmd = true;
             }
           }
         }
-
-        // Add the following assume-statement for each assumption variable 'v', where 'v_post' is the new incarnation and 'v_pre' is the old one:
-        // assume v_post ==> v_pre;
-        foreach (IdentifierExpr ie in havocVars)
+        else if (currentImplementation != null
+                 && currentImplementation.HasCachedSnapshot
+                 && relevantAssumpVars.Count == 0
+                 && checksum != null
+                 && currentImplementation.IsAssertionChecksumInCachedSnapshot(checksum)
+                 && currentImplementation.IsErrorChecksumInCachedSnapshot(checksum))
         {
-          if (QKeyValue.FindBoolAttribute(ie.Decl.Attributes, "assumption"))
-          {
-            var preInc = (Expr) (preHavocIncarnationMap[ie.Decl].Clone());
-            var postInc = (Expr) (incarnationMap[ie.Decl].Clone());
-            passiveCmds.Add(new AssumeCmd(c.tok, Expr.Imp(postInc, preInc)));
-          }
+          TraceCachingAction(traceWriter, pc, CachingAction.RecycleError);
+          ac.MarkAsVerifiedUnder(Expr.True);
+          currentImplementation.AddRecycledFailingAssertion(ac);
+          pc.Attributes = new QKeyValue(Token.NoToken, "recycled_failing_assertion", new List<object>(),
+            pc.Attributes);
+        }
+        else
+        {
+          TraceCachingAction(traceWriter, pc, CachingAction.DoNothingToAssert);
         }
       }
-
-      #endregion
-
-      else if (c is CommentCmd)
-      {
-        // comments are just for debugging and don't affect verification
-      }
-      else if (c is SugaredCmd sug)
-      {
-        Cmd cmd = sug.GetDesugaring(Options);
-        Contract.Assert(cmd != null);
-        TurnIntoPassiveCmd(traceWriter, cmd, enclosingBlock, incarnationMap, oldFrameSubst, passiveCmds, mvInfo);
-      }
-      else if (c is StateCmd st)
+      else if (pc is AssumeCmd
+               && QKeyValue.FindBoolAttribute(pc.Attributes, "precondition_previous_snapshot")
+               && pc.SugaredCmdChecksum != null)
       {
-        this.preHavocIncarnationMap = null; // we do not need to remember the previous incarnations
-
-        // account for any where clauses among the local variables
-        foreach (Variable v in st.Locals)
+        if (!relevantDoomedAssumpVars.Any()
+            && currentImplementation.HasCachedSnapshot
+            && currentImplementation.IsAssertionChecksumInCachedSnapshot(pc.SugaredCmdChecksum)
+            && !currentImplementation.IsErrorChecksumInCachedSnapshot(pc.SugaredCmdChecksum))
         {
-          Contract.Assert(v != null);
-          Expr w = v.TypedIdent.WhereExpr;
-          if (w != null)
+          var assmVars =
+            currentImplementation.ConjunctionOfInjectedAssumptionVariables(incarnationMap, out var isTrue);
+          if (!isTrue)
           {
-            passiveCmds.Add(new AssumeCmd(v.tok, w));
+            copy = LiteralExpr.Imp(assmVars, copy);
+            TraceCachingAction(traceWriter, pc, CachingAction.MarkAsPartiallyVerified);
+          }
+          else
+          {
+            TraceCachingAction(traceWriter, pc, CachingAction.MarkAsFullyVerified);
           }
         }
-
-        // do the sub-commands
-        foreach (Cmd s in st.Cmds)
-        {
-          Contract.Assert(s != null);
-          TurnIntoPassiveCmd(traceWriter, s, enclosingBlock, incarnationMap, oldFrameSubst, passiveCmds, mvInfo);
-        }
-
-        // remove the local variables from the incarnation map
-        foreach (Variable v in st.Locals)
+        else
         {
-          Contract.Assert(v != null);
-          incarnationMap.Remove(v);
+          TraceCachingAction(traceWriter, pc, CachingAction.DropAssume);
+          dropCmd = true;
         }
       }
-
-      #region There shouldn't be any other types of commands at this point
-
-      else
+      else if (pc is AssumeCmd && QKeyValue.FindBoolAttribute(pc.Attributes, "assumption_variable_initialization"))
       {
-        Debug.Fail(
-          "Internal Error: Passive transformation handed a command that is not one of assert,assume,havoc,assign.");
+        var identExpr = pc.Expr as IdentifierExpr;
+        if (identExpr != null && identExpr.Decl != null && !incarnationMap.ContainsKey(identExpr.Decl))
+        {
+          incarnationMap[identExpr.Decl] = LiteralExpr.True;
+          dropCmd = true;
+        }
       }
 
-      #endregion
-
-
-      #region We remember if we have put an havoc statement into a passive form
-
-      if (!(c is HavocCmd))
+      pc.Expr = copy;
+      if (!dropCmd)
       {
-        this.preHavocIncarnationMap = null;
+        passiveCmds.Add(pc);
       }
-      // else: it has already been set by the case for the HavocCmd
-
-      #endregion
     }
 
     NAryExpr TypedExprEq(Expr e0, Expr e1, bool doNotResolveOverloading = false)
diff --git a/Source/VCGeneration/ProofRun.cs b/Source/VCGeneration/ProofRun.cs
index 3bec8b330..752fb4372 100644
--- a/Source/VCGeneration/ProofRun.cs
+++ b/Source/VCGeneration/ProofRun.cs
@@ -7,4 +7,6 @@ public interface ProofRun {
   string Description { get; }
   
   List<Counterexample> Counterexamples { get; }
+
+  HashSet<string> CoveredElements { get;  }
 }
\ No newline at end of file
diff --git a/Source/VCGeneration/Split.cs b/Source/VCGeneration/Split.cs
index 6ede06f00..b9c97ffa6 100644
--- a/Source/VCGeneration/Split.cs
+++ b/Source/VCGeneration/Split.cs
@@ -1271,18 +1271,23 @@ public int GetHashCode(List<Block> obj)
           run.OutputWriter.WriteLine("      --> split #{0} done,  [{1} s] {2}", SplitIndex + 1,
             checker.ProverRunTime.TotalSeconds, outcome);
         }
+        if (options.Trace && options.TrackVerificationCoverage) {
+          run.OutputWriter.WriteLine("Covered elements: {0}",
+            string.Join(", ", CoveredElements.OrderBy(s => s)));
+        }
 
         var resourceCount = await checker.GetProverResourceCount();
         var result = new VCResult(
-          SplitIndex + 1,
-          iteration,
-          checker.ProverStart,
-          outcome,
-          checker.ProverRunTime,
-          checker.Options.ErrorLimit,
-          Counterexamples,
-          Asserts,
-          resourceCount);
+          vcNum: SplitIndex + 1,
+          iteration: iteration,
+          startTime: checker.ProverStart,
+          outcome: outcome,
+          runTime: checker.ProverRunTime,
+          maxCounterExamples: checker.Options.ErrorLimit,
+          counterExamples: Counterexamples,
+          asserts: Asserts,
+          coveredElements: CoveredElements,
+          resourceCount: resourceCount);
         callback.OnVCResult(result);
 
         if (options.VcsDumpSplits)
@@ -1295,6 +1300,8 @@ public int GetHashCode(List<Block> obj)
 
       public List<Counterexample> Counterexamples { get; } = new();
 
+      public HashSet<string> CoveredElements { get; } = new();
+
       /// <summary>
       /// As a side effect, updates "this.parent.CumulativeAssertionCount".
       /// </summary>
diff --git a/Source/VCGeneration/VCGen.cs b/Source/VCGeneration/VCGen.cs
index e1833ea8d..8d9c5066d 100644
--- a/Source/VCGeneration/VCGen.cs
+++ b/Source/VCGeneration/VCGen.cs
@@ -57,7 +57,11 @@ public static AssumeCmd AssertTurnedIntoAssume(VCGenOptions options, AssertCmd a
           throw new cce.UnreachableException(); // unexpected case
       }
 
-      return new AssumeCmd(assrt.tok, expr);
+      var assume = new AssumeCmd(assrt.tok, expr);
+      // Copy any {:id ...} from the assertion to the assumption, so
+      // we can track it while analyzing verification coverage.
+      (assume as ICarriesAttributes).CopyIdFrom(assrt.tok, assrt);
+      return assume;
     }
 
     #region Soundness smoke tester
@@ -458,14 +462,10 @@ void ObjectInvariant()
 
       Program program;
 
-      public IEnumerable<string> NecessaryAssumes
+      public override void AddCoveredElement(string id)
       {
-        get { return program.NecessaryAssumes; }
-      }
-
-      public override void AddNecessaryAssume(string id)
-      {
-        program.NecessaryAssumes.Add(id);
+        program.AllCoveredElements.Add(id);
+        split.CoveredElements.Add(id);
       }
 
       public ErrorReporter(VCGenOptions options,
@@ -704,65 +704,79 @@ private void ConvertCFG2DAGStandard(Implementation impl, Dictionary<Block, List<
         List<Cmd> prefixOfPredicateCmdsMaintained = new List<Cmd>();
         for (int i = 0, n = header.Cmds.Count; i < n; i++)
         {
-          PredicateCmd a = header.Cmds[i] as PredicateCmd;
-          if (a != null)
+          PredicateCmd predicateCmd = header.Cmds[i] as PredicateCmd;
+          if (predicateCmd != null)
           {
-            if (a is AssertCmd)
+            if (predicateCmd is AssertCmd)
             {
-              AssertCmd c = (AssertCmd) a;
-              AssertCmd b = null;
+              AssertCmd assertCmd = (AssertCmd) predicateCmd;
+              AssertCmd initAssertCmd = null;
 
               if (Options.ConcurrentHoudini)
               {
                 Contract.Assert(taskID >= 0);
                 if (Options.Cho[taskID].DisableLoopInvEntryAssert)
                 {
-                  b = new LoopInitAssertCmd(c.tok, Expr.True, c);
+                  initAssertCmd = new LoopInitAssertCmd(assertCmd.tok, Expr.True, assertCmd);
                 }
                 else
                 {
-                  b = new LoopInitAssertCmd(c.tok, c.Expr, c);
+                  initAssertCmd = new LoopInitAssertCmd(assertCmd.tok, assertCmd.Expr, assertCmd);
                 }
               }
               else
               {
-                b = new LoopInitAssertCmd(c.tok, c.Expr, c);
+                initAssertCmd = new LoopInitAssertCmd(assertCmd.tok, assertCmd.Expr, assertCmd);
               }
 
-              b.Attributes = c.Attributes;
-              prefixOfPredicateCmdsInit.Add(b);
+              initAssertCmd.Attributes = (QKeyValue)assertCmd.Attributes?.Clone();
+              // Copy any {:id ...} from the invariant to the assertion that it's established, so
+              // we can track it while analyzing verification coverage.
+              (initAssertCmd as ICarriesAttributes).CopyIdWithSuffixFrom(assertCmd.tok, assertCmd, "$established");
 
+              prefixOfPredicateCmdsInit.Add(initAssertCmd);
+
+              LoopInvMaintainedAssertCmd maintainedAssertCmd;
               if (Options.ConcurrentHoudini)
               {
                 Contract.Assert(taskID >= 0);
                 if (Options.Cho[taskID].DisableLoopInvMaintainedAssert)
                 {
-                  b = new Bpl.LoopInvMaintainedAssertCmd(c.tok, Expr.True, c);
+                  maintainedAssertCmd = new Bpl.LoopInvMaintainedAssertCmd(assertCmd.tok, Expr.True, assertCmd);
                 }
                 else
                 {
-                  b = new Bpl.LoopInvMaintainedAssertCmd(c.tok, c.Expr, c);
+                  maintainedAssertCmd = new Bpl.LoopInvMaintainedAssertCmd(assertCmd.tok, assertCmd.Expr, assertCmd);
                 }
               }
               else
               {
-                b = new Bpl.LoopInvMaintainedAssertCmd(c.tok, c.Expr, c);
+                maintainedAssertCmd = new Bpl.LoopInvMaintainedAssertCmd(assertCmd.tok, assertCmd.Expr, assertCmd);
               }
 
-              b.Attributes = c.Attributes;
-              prefixOfPredicateCmdsMaintained.Add(b);
-              header.Cmds[i] = new AssumeCmd(c.tok, c.Expr);
+              maintainedAssertCmd.Attributes = (QKeyValue)assertCmd.Attributes?.Clone();
+              // Copy any {:id ...} from the invariant to the assertion that it's maintained, so
+              // we can track it while analyzing verification coverage.
+              (maintainedAssertCmd as ICarriesAttributes).CopyIdWithSuffixFrom(assertCmd.tok, assertCmd, "$maintained");
+
+              prefixOfPredicateCmdsMaintained.Add(maintainedAssertCmd);
+              AssumeCmd assume = new AssumeCmd(assertCmd.tok, assertCmd.Expr);
+              // Copy any {:id ...} from the invariant to the assumption used within the body, so
+              // we can track it while analyzing verification coverage.
+              (assume as ICarriesAttributes).CopyIdWithSuffixFrom(assertCmd.tok, assertCmd, "$assume_in_body");
+
+              header.Cmds[i] = assume;
             }
             else
             {
-              Contract.Assert(a is AssumeCmd);
+              Contract.Assert(predicateCmd is AssumeCmd);
               if (Options.AlwaysAssumeFreeLoopInvariants)
               {
                 // Usually, "free" stuff, like free loop invariants (and the assume statements
                 // that stand for such loop invariants) are ignored on the checking side.  This
                 // command-line option changes that behavior to always assume the conditions.
-                prefixOfPredicateCmdsInit.Add(a);
-                prefixOfPredicateCmdsMaintained.Add(a);
+                prefixOfPredicateCmdsInit.Add(predicateCmd);
+                prefixOfPredicateCmdsMaintained.Add(predicateCmd);
               }
             }
           }
diff --git a/Source/VCGeneration/VCResult.cs b/Source/VCGeneration/VCResult.cs
index 9e75668bb..982209ec3 100644
--- a/Source/VCGeneration/VCResult.cs
+++ b/Source/VCGeneration/VCResult.cs
@@ -24,6 +24,7 @@ public record VCResult
     int maxCounterExamples,
     List<Counterexample> counterExamples,
     List<AssertCmd> asserts,
+    IEnumerable<string> coveredElements,
     int resourceCount
   ) {
     public void ComputePerAssertOutcomes(out Dictionary<AssertCmd, ProverInterface.Outcome> perAssertOutcome,
diff --git a/Source/VCGeneration/Wlp.cs b/Source/VCGeneration/Wlp.cs
index 5414ea831..67d8b54f4 100644
--- a/Source/VCGeneration/Wlp.cs
+++ b/Source/VCGeneration/Wlp.cs
@@ -109,6 +109,12 @@ internal static VCExpr Cmd(Block b, Cmd cmd, VCExpr N, VCContext ctxt)
         }
 
         VCExpr C = ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr);
+        var assertId = QKeyValue.FindStringAttribute(ac.Attributes, "id");
+        if (assertId != null && ctxt.Options.TrackVerificationCoverage)
+        {
+          var v = gen.Variable(assertId, Microsoft.Boogie.Type.Bool, VCExprVarKind.Assert);
+          C = gen.Function(VCExpressionGenerator.NamedAssertOp, v, gen.AndSimp(v, C));
+        }
 
         VCExpr VU = null;
         if (!isFullyVerified)
@@ -197,19 +203,19 @@ internal static VCExpr Cmd(Block b, Cmd cmd, VCExpr N, VCContext ctxt)
 
         var expr = ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr);
 
-        var aid = QKeyValue.FindStringAttribute(ac.Attributes, "id");
-        if (aid != null)
+        var assumeId = QKeyValue.FindStringAttribute(ac.Attributes, "id");
+        if (assumeId != null && ctxt.Options.TrackVerificationCoverage)
         {
           var isTry = QKeyValue.FindBoolAttribute(ac.Attributes, "try");
-          var v = gen.Variable((isTry ? "try$$" : "assume$$") + aid, Microsoft.Boogie.Type.Bool);
+          var v = gen.Variable(assumeId, Microsoft.Boogie.Type.Bool, isTry ? VCExprVarKind.Try : VCExprVarKind.Assume);
           expr = gen.Function(VCExpressionGenerator.NamedAssumeOp, v, gen.ImpliesSimp(v, expr));
         }
 
         var soft = QKeyValue.FindBoolAttribute(ac.Attributes, "soft");
         var softWeight = QKeyValue.FindIntAttribute(ac.Attributes, "soft", 0);
-        if ((soft || 0 < softWeight) && aid != null)
+        if ((soft || 0 < softWeight) && assumeId != null)
         {
-          var v = gen.Variable("soft$$" + aid, Microsoft.Boogie.Type.Bool);
+          var v = gen.Variable(assumeId, Microsoft.Boogie.Type.Bool, VCExprVarKind.Soft);
           expr = gen.Function(new VCExprSoftOp(Math.Max(softWeight, 1)), v, gen.ImpliesSimp(v, expr));
         }
 
diff --git a/Test/coverage/verificationCoverage.bpl b/Test/coverage/verificationCoverage.bpl
new file mode 100644
index 000000000..e5e27f135
--- /dev/null
+++ b/Test/coverage/verificationCoverage.bpl
@@ -0,0 +1,108 @@
+// RUN: %boogie "%s" > "%t.plain"
+// RUN: %diff "%s.expect.plain" "%t.plain"
+// RUN: %boogie -trackVerificationCoverage "%s" > "%t.coverage"
+// RUN: %diff "%s.expect.coverage" "%t.coverage"
+// UNSUPPORTED: batch_mode
+
+procedure testRequiresAssign(n: int)
+  requires {:id "r0"} n > 0; // covered
+  requires {:id "r_not_1"} n < 10; // not covered
+{
+    var x: int;
+    x := {:id "a0"} n + 1; // covered
+    assert {:id "assert_a0"} x == n + 1; // covered
+    x := {:id "a_not_1"} 0; // not covered
+    assert {:id "assert_r0"} n > 0; // covered
+}
+
+procedure sum(n: int) returns (s: int)
+  requires {:id "spre1"} n >= 0; // covered
+  ensures {:id "spost"} s == (n * (n + 1)) div 2; // covered
+{
+  var i: int;
+  var foo: int;
+
+  i := 0;
+  s := 0;
+  foo := 27;
+  while (i < n)
+    invariant {:id "sinv1"} 0 <= i && i <= n; // covered: established, maintained, assumed
+    invariant {:id "sinv2"} s == (i * (i + 1)) div 2; // covered: established, maintained, assumed
+    invariant {:id "sinv_not_1"} n >= 0; // covered: established, maintained, NOT assumed
+  {
+    i := i + 1;
+    s := s + i;
+    foo := {:id "update_foo"} foo * 2; // not covered
+  }
+}
+
+procedure contradictoryAssume(n: int)
+{
+    assume {:id "cont_assume_1"} n > 0; // covered
+    assume {:id "cont_assume_2"} n < 0; // covered
+    assume {:id "unreach_assume_1"} n == 5; // not covered
+    assert {:id "unreach_assert_1"} n < 10; // not covered
+}
+
+// NB: an explicit `requires false` leads to _nothing_ being covered
+procedure falseRequires(n: int)
+  requires {:id "false_req"} n != n; // covered
+{
+    assert {:id "false_assert"} false; // not covered
+}
+
+procedure contradictoryRequires(n: int)
+  requires {:id "cont_req_1"} n > 0; // covered
+  requires {:id "cont_req_2"} n < 0; // covered
+{
+    assume {:id "n_eq_5"} n == 5; // not covered
+    assert {:id "n_lt_10"} n > 10; // not covered
+}
+
+procedure assumeFalse() {
+  assume {:id "assumeFalse"} false; // covered
+  assert {:id "assertSimple"} 1 + 1 == 2; // not covered
+}
+
+procedure testEnsuresCallee(n: int) returns (r: int)
+  requires {:id "ter0"} n > 0; // covered
+  ensures {:id "tee0"} r > n; // covered by this procedure and caller
+  ensures {:id "tee1"} r > 0; // covered when proving this procedure, not from caller
+{
+  r := n + 1;
+}
+
+procedure testEnsuresCaller(n: int) returns (r: int)
+  requires {:id "ter1"} n > 0; // covered
+  ensures {:id "tee_not_1"} r > n; // covered
+{
+  var x: int;
+  var y: int;
+  call {:id "call1"} x := testEnsuresCallee(n+1); // requires and ensures covered
+  call {:id "call2"} y := testEnsuresCallee(n+1); // requires and ensures covered
+  assert {:id "call2_tee1"} y > 0;
+  r := {:id "xy_sum"} x + y; // covered
+}
+
+procedure obviouslyUnconstrainedCode(x: int) returns (a: int, b: int)
+  requires {:id "x_gt_10"} x > 10; // covered
+  requires {:id "x_lt_100"} x < 100; // not covered
+  ensures {:id "a_gt_10"} a > 10; // covered
+{
+  a := {:id "constrained"} x + 1;     // covered: constrained by ensures clause
+  b := {:id "not_constrained"} x - 1; // not covered: not constrained by ensures clause
+}
+
+
+procedure contradictoryEnsuresClause(x: int) returns (r: int);
+  requires {:id "xpos_abs"} x > 1; // covered (established by caller)
+  ensures  {:id "cont_ens_abs"} r > x && r < 0; // covered (used by caller proof)
+
+// Call function that has contradictory ensures clauses.
+procedure callContradictoryFunction(x: int) returns (r: int)
+  requires {:id "xpos_caller"} x > 1; // covered
+  ensures {:id "caller_ensures"} r < 0; // not covered
+{
+  call {:id "call_cont"} r := contradictoryEnsuresClause(x); // requires and ensures covered
+  r := {:id "unreachable_assignment"} r - 1; // not covered
+}
diff --git a/Test/coverage/verificationCoverage.bpl.expect.coverage b/Test/coverage/verificationCoverage.bpl.expect.coverage
new file mode 100644
index 000000000..32f5d2408
--- /dev/null
+++ b/Test/coverage/verificationCoverage.bpl.expect.coverage
@@ -0,0 +1,3 @@
+Elements covered by verification: a_gt_10, a0, assert_a0, assert_r0, assumeFalse, call2_tee1, constrained, cont_assume_1, cont_assume_2, cont_ens_abs$call_cont$ensures, cont_req_1, cont_req_2, false_req, r0, sinv_not_1$established, sinv_not_1$maintained, sinv1$assume_in_body, sinv1$established, sinv1$maintained, sinv2$assume_in_body, sinv2$established, sinv2$maintained, spost, spre1, tee_not_1, tee0, tee0$call1$ensures, tee0$call2$ensures, tee1, tee1$call2$ensures, ter0, ter0$call1$requires, ter0$call2$requires, ter1, x_gt_10, xpos_abs$call_cont$requires, xpos_caller, xy_sum
+
+Boogie program verifier finished with 10 verified, 0 errors
diff --git a/Test/coverage/verificationCoverage.bpl.expect.plain b/Test/coverage/verificationCoverage.bpl.expect.plain
new file mode 100644
index 000000000..12041afe1
--- /dev/null
+++ b/Test/coverage/verificationCoverage.bpl.expect.plain
@@ -0,0 +1,2 @@
+
+Boogie program verifier finished with 10 verified, 0 errors
diff --git a/Test/test2/Timeouts0.bpl b/Test/test2/Timeouts0.bpl
index 7ca86452a..733cc119e 100644
--- a/Test/test2/Timeouts0.bpl
+++ b/Test/test2/Timeouts0.bpl
@@ -6,7 +6,6 @@
 // UNSUPPORTED: batch_mode
 // CHECK-L: (set-option :timeout 4000)
 // CHECK-L: (set-option :timeout 8000)
-// CHECK-L: (set-option :timeout 2000)
 procedure TestTimeouts0(in: [int]int, len: int) returns (out: [int]int)
   requires in[0] == 0 && (forall i: int :: 0 <= i ==> in[i + 1] == in[i] + 1);
   requires 0 < len;
@@ -61,32 +60,3 @@ implementation {:timeLimit 8} TestTimeouts1(in: [int]int, len: int) returns (out
         i := i + 1;
     }
 }
-
-
-procedure TestTimeouts2(in: [int]int, len: int) returns (out: [int]int);
-  requires in[0] == 0 && (forall i: int :: 0 <= i ==> in[i + 1] == in[i] + 1);
-  requires 0 < len;
-  ensures (forall j: int :: 0 <= j && j < len ==> out[j] == j);
-
-implementation {:timeLimit 2} TestTimeouts2(in: [int]int, len: int) returns (out: [int]int)
-{
-    var i : int;
-
-    i := 0;
-    out[i] := 0;
-    while (i < len)
-      invariant 0 <= i && i <= len;
-      invariant out[0] == 0 && (forall j: int :: 0 <= j && j < i ==> out[j + 1] == out[j] + 1);
-    {
-        out[i + 1] := out[i] + 1;
-        i := i + 1;
-    }
-
-    i := 0;
-    while (i < len)
-      invariant 0 <= i && i <= len;
-      invariant (forall j: int :: 0 <= j && j < i ==> out[j] == in[j]);
-    {
-        i := i + 1;
-    }
-}
diff --git a/Test/test2/Timeouts0.bpl.expect b/Test/test2/Timeouts0.bpl.expect
index bb09751e0..0b8a02314 100644
--- a/Test/test2/Timeouts0.bpl.expect
+++ b/Test/test2/Timeouts0.bpl.expect
@@ -1,11 +1,8 @@
-Timeouts0.bpl(28,5): Error: a postcondition could not be proved on this return path
-Timeouts0.bpl(13,3): Related location: this is the postcondition that could not be proved
-Timeouts0.bpl(30,7): Error: this invariant could not be proved to be maintained by the loop
-Timeouts0.bpl(57,5): Error: a postcondition could not be proved on this return path
-Timeouts0.bpl(40,3): Related location: this is the postcondition that could not be proved
-Timeouts0.bpl(59,7): Error: this invariant could not be proved to be maintained by the loop
-Timeouts0.bpl(86,5): Error: a postcondition could not be proved on this return path
-Timeouts0.bpl(69,3): Related location: this is the postcondition that could not be proved
-Timeouts0.bpl(88,7): Error: this invariant could not be proved to be maintained by the loop
+Timeouts0.bpl(27,5): Error: a postcondition could not be proved on this return path
+Timeouts0.bpl(12,3): Related location: this is the postcondition that could not be proved
+Timeouts0.bpl(29,7): Error: this invariant could not be proved to be maintained by the loop
+Timeouts0.bpl(56,5): Error: a postcondition could not be proved on this return path
+Timeouts0.bpl(39,3): Related location: this is the postcondition that could not be proved
+Timeouts0.bpl(58,7): Error: this invariant could not be proved to be maintained by the loop
 
-Boogie program verifier finished with 0 verified, 6 errors
+Boogie program verifier finished with 0 verified, 4 errors
diff --git a/Test/unnecessaryassumes/unnecessaryassumes0.bpl b/Test/unnecessaryassumes/unnecessaryassumes0.bpl
index 927b4adaa..6bc21cddb 100644
--- a/Test/unnecessaryassumes/unnecessaryassumes0.bpl
+++ b/Test/unnecessaryassumes/unnecessaryassumes0.bpl
@@ -1,5 +1,5 @@
-// We use boogie instead of parallel-boogie here to fix the order of the output from /printNecessaryAssumes
-// RUN: %boogie /printNecessaryAssumes "%s" > "%t"
+// We use boogie instead of parallel-boogie here to fix the order of the output from /printVerificationCoverage
+// RUN: %boogie /trackVerificationCoverage "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 procedure test0(n: int)
diff --git a/Test/unnecessaryassumes/unnecessaryassumes1.bpl b/Test/unnecessaryassumes/unnecessaryassumes1.bpl
index cb9f18bb4..34377644f 100644
--- a/Test/unnecessaryassumes/unnecessaryassumes1.bpl
+++ b/Test/unnecessaryassumes/unnecessaryassumes1.bpl
@@ -1,5 +1,5 @@
-// We use boogie instead of parallel-boogie here to fix the order of the output from /printNecessaryAssumes 
-// RUN: %boogie /printNecessaryAssumes "%s" > "%t"
+// We use boogie instead of parallel-boogie here to fix the order of the output from /trackVerificationCoverage
+// RUN: %boogie /trackVerificationCoverage "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 // UNSUPPORTED: batch_mode
 
diff --git a/Test/unnecessaryassumes/unnecessaryassumes1.bpl.expect b/Test/unnecessaryassumes/unnecessaryassumes1.bpl.expect
index 0d3aeca22..34f57618e 100644
--- a/Test/unnecessaryassumes/unnecessaryassumes1.bpl.expect
+++ b/Test/unnecessaryassumes/unnecessaryassumes1.bpl.expect
@@ -1,3 +1,3 @@
-Necessary assume command(s): s0, s2, s3
+Elements covered by verification: s0, s2, s3
 
 Boogie program verifier finished with 3 verified, 0 errors