Clone Split instead of using ConcurrentBag

Source/Houdini/HoudiniSession.cs

@@ -127,7 +127,7 @@ public class HoudiniStatistics
     private readonly Houdini houdini;
     public HoudiniStatistics stats;
     public List<Counterexample> Counterexamples { get; } = new();
-    public ConcurrentBag<TrackedNodeComponent> CoveredElements { get; } = new();
+    public HashSet<TrackedNodeComponent> CoveredElements { get; } = new();
     private VCExpr conjecture;
     private ProverInterface.ErrorHandler handler;
     VerificationResultCollector collector;

Source/VCGeneration/ProofRun.cs

@@ -9,5 +9,5 @@ public interface ProofRun {
 
   List<Counterexample> Counterexamples { get; }
 
-  ConcurrentBag<TrackedNodeComponent> CoveredElements { get;  }
+  HashSet<TrackedNodeComponent> CoveredElements { get;  }
 }

Source/VCGeneration/Split.cs

@@ -89,6 +89,39 @@ public Split(VCGenOptions options, List<Block /*!*/> /*!*/ blocks,
         randomGen = new Random(RandomSeed ?? 0);
       }
 
+      public Split(Split oldSplit)
+      {
+        Options = oldSplit.Options;
+        randomGen = oldSplit.randomGen;
+        Run = oldSplit.Run;
+        Blocks = oldSplit.Blocks; // Could be deep, but doesn't need to be here.
+        bigBlocks = oldSplit.bigBlocks; // Could be deep, but doesn't need to be here.
+        TopLevelDeclarations = oldSplit.TopLevelDeclarations; // Could be deep, but doesn't need to be here.
+        stats = oldSplit.stats; // Could be deep, but doesn't need to be here.
+        splitBlock = oldSplit.splitBlock;
+        assertToAssume = oldSplit.assertToAssume;
+        assumizedBranches = oldSplit.assumizedBranches; // Could be deep, but doesn't need to be here.
+        score = oldSplit.score;
+        scoreComputed = oldSplit.scoreComputed;
+        totalCost = oldSplit.totalCost;
+        assertionCount = oldSplit.assertionCount;
+        assertionCost = oldSplit.assertionCost;
+        GotoCmdOrigins = oldSplit.GotoCmdOrigins; // Could be deep, but doesn't need to be here.
+        parent = oldSplit.parent; // Could be deep, but doesn't need to be here.
+        copies = oldSplit.copies; // Could be deep, but doesn't need to be here.
+        doingSlice = oldSplit.doingSlice;
+        sliceInitialLimit = oldSplit.sliceInitialLimit;
+        sliceLimit = oldSplit.sliceLimit;
+        slicePos = oldSplit.slicePos;
+        protectedFromAssertToAssume = oldSplit.protectedFromAssertToAssume; // Could be deep, but doesn't need to be here.
+        keepAtAll = oldSplit.keepAtAll; // Could be deep, but doesn't need to be here.
+        SplitIndex = oldSplit.SplitIndex;
+        reporter = oldSplit.reporter;
+        bsid = oldSplit.bsid;
+        Counterexamples = new(); // Create fresh, so it can be updated.
+        CoveredElements = new(); // Create fresh, so it can be updated.
+      }
+
       private void PrintTopLevelDeclarationsForPruning(Program program, Implementation implementation, string suffix)
       {
         if (!Options.Prune || Options.PrintPrunedFile == null)
@@ -913,7 +946,7 @@ public VerificationRunResult ReadOutcome(int iteration, Checker checker, Verifie
 
       public List<Counterexample> Counterexamples { get; } = new();
 
-      public ConcurrentBag<TrackedNodeComponent> CoveredElements { get; } = new();
+      public HashSet<TrackedNodeComponent> CoveredElements { get; } = new();
 
       /// <summary>
       /// As a side effect, updates "this.parent.CumulativeAssertionCount".

Source/VCGeneration/SplitAndVerifyWorker.cs

@@ -110,7 +110,8 @@ async Task DoWorkForMultipleIterations(Split split, CancellationToken cancellati
       int currentSplitNumber = DoSplitting ? Interlocked.Increment(ref splitNumber) - 1 : -1;
       split.SplitIndex = currentSplitNumber;
       var tasks = Enumerable.Range(0, options.RandomizeVcIterations).Select(iteration =>
-        DoWork(iteration, split, cancellationToken));
+        // Clone the split so it can be safely updated in each parallel task.
+        DoWork(iteration, new Split(split), cancellationToken));
       await Task.WhenAll(tasks);
     }