Address comments from @fabiomadge

Author: atomb

Source/Core/CoverageAnnotator.cs

@@ -30,8 +30,8 @@ private void AddIdIfMissing(ICarriesAttributes node, bool isGoal)
     }
     var idStr = node.FindStringAttribute("id");
     if (idStr == null) {
-      idCount++;
       idStr = $"id_l{absy.tok.line}_c{absy.tok.col}_{NodeType(node)}_{idCount}";
+      idCount++;
     }
     idMap.Add(idStr, absy);
     if (isGoal) {

Source/ExecutionEngine/CommandLineOptions.cs

@@ -317,19 +317,13 @@ public bool UseUnsatCoreForContractInfer {
 
     public bool PrintAssignment  { get; set; }
 
-    public bool TrackVerificationCoverage {
-      get => trackVerificationCoverage;
+    public bool TrackVerificationCoverage
+    {
+      get => trackVerificationCoverage || WarnVacuousProofs;
       set => trackVerificationCoverage = value;
     }
 
-    public bool WarnVacuousProofs
-    {
-      get => warnVacuousProofs;
-      set {
-        warnVacuousProofs = value;
-        if (warnVacuousProofs) { trackVerificationCoverage = true; }
-      }
-    }
+    public bool WarnVacuousProofs { get; set; }
 
     public int InlineDepth  { get; set; } = -1;
 
@@ -614,7 +608,6 @@ void ObjectInvariant5()
     private bool normalizeNames;
     private bool normalizeDeclarationOrder = true;
     private bool keepQuantifier = false;
-    private bool warnVacuousProofs;
 
     public List<CoreOptions.ConcurrentHoudiniOptions> Cho { get; set; } = new();
 
@@ -2017,8 +2010,8 @@ Track and report which program elements labeled with an
                 report. This generalizes and replaces the previous
                 (undocumented) `/printNecessaryAssertions` option.
   /warnVacuousProofs
-                Automatically add `{:id ...}` attributes to assumptions, assertions,
-                requires clauses, ensures clauses, and calls; enable the
+                Automatically add missing `{:id ...}` attributes to assumptions,
+                assertions, requires clauses, ensures clauses, and calls; enable the
                 `/trackVerificationCoverage` option; and warn when proof goals are
                 not covered by a proof.
   /keepQuantifier