Avoid adding duplicate coverage IDs

Previously, if a program element happened to already be labeled with the
label that's auto-generated for another element, Boogie would fail when
adding an already-existing key to the coverage tracking map.

Author: atomb

Source/Core/CoverageAnnotator.cs

@@ -29,9 +29,11 @@ private void AddIdIfMissing(ICarriesAttributes node, bool isGoal)
       return;
     }
     var idStr = node.FindStringAttribute("id");
-    if (idStr == null) {
-      idStr = $"id_l{absy.tok.line}_c{absy.tok.col}_{NodeType(node)}_{idCount}";
-      idCount++;
+    if (idStr == null || idMap.ContainsKey(idStr)) {
+      do {
+        idStr = $"id_l{absy.tok.line}_c{absy.tok.col}_{NodeType(node)}_{idCount}";
+        idCount++;
+      } while(idMap.ContainsKey(idStr));
     }
     idMap.Add(idStr, absy);
     if (isGoal) {
@@ -112,4 +114,4 @@ public override Ensures VisitEnsures(Ensures ensures)
     AddIdIfMissing(ensures, true);
     return base.VisitEnsures(ensures);
   }
-}
+}

Source/Directory.Build.props

@@ -2,7 +2,7 @@
 
   <!-- Target framework and package configuration -->
   <PropertyGroup>
-    <Version>3.5.2</Version>
+    <Version>3.5.3</Version>
     <TargetFramework>net8.0</TargetFramework>
     <GeneratePackageOnBuild>false</GeneratePackageOnBuild>
     <Authors>Boogie</Authors>

Test/coverage/duplicateIds.bpl

@@ -0,0 +1,12 @@
+// RUN: %boogie /warnVacuousProofs /trace "%s" > "%t"
+// RUN: %OutputCheck "%s" --file-to-check="%t.coverage"
+// CHECK:Proof dependencies:
+// CHECK:  id_l12_c5_assert_0
+// CHECK:  id_l12_c5_assert_1
+// CHECK:Proof dependencies of whole program:
+// CHECK:  id_l12_c5_assert_0
+// CHECK:  id_l12_c5_assert_1
+procedure P(x: int) {
+    assume {:id "id_l12_c5_assert_0"} x > 0;
+    assert x > 0;
+}