Fix concurrency issue

Source/Core/BasicTypeVisitor.cs

@@ -1,15 +1,25 @@
+using System;
 using System.Collections.Generic;
 
 namespace Microsoft.Boogie;
 
 public class BasicTypeVisitor : ReadOnlyVisitor
 {
+  private readonly Func<Absy, bool> enterNode;
   private HashSet<Type> basicTypes = new();
-  public BasicTypeVisitor(Absy absy)
-  {
+  public BasicTypeVisitor(Absy absy, Func<Absy, bool> enterNode) {
+    this.enterNode = enterNode;
     Visit(absy);
   }
 
+  public override Absy Visit(Absy node) {
+    if (enterNode(node)) {
+      return base.Visit(node);
+    }
+
+    return node;
+  }
+
   public override Type VisitBasicType(BasicType node)
   {
     basicTypes.Add(node);

Source/VCGeneration/Checker.cs

@@ -128,7 +128,11 @@ public Checker(CheckerPool pool, string /*?*/ logFilePath, bool appendLogFile)
 
     public void Target(Program prog, ProverContext ctx, Split split)
     {
-      var usedTypes = new BasicTypeVisitor(prog).GetBasicTypes().ToList();
+      /* We should not traverse implementations other than the current one, because they might be in the process of being modified.
+       */
+      bool EnterNode(Absy node) => node is not Implementation implementation || implementation == split.Implementation;
+
+      var usedTypes = new BasicTypeVisitor(prog, EnterNode).GetBasicTypes().ToList();
       lock (this)
       {
         hasOutput = default;

Source/VCGeneration/ConditionGeneration.cs

@@ -85,7 +85,7 @@ void ObjectInvariant()
 
     public Dictionary<Incarnation, Absy> IncarnationOriginMap = new();
 
-    public Program program;
+    public readonly Program program;
     public CheckerPool CheckerPool { get; }
 
     public ConditionGeneration(Program program, CheckerPool checkerPool)

Source/VCGeneration/Splits/Split.cs

@@ -56,8 +56,7 @@ public IReadOnlyList<Declaration> PrunedDeclarations {
       int assertionCount;
       double assertionCost; // without multiplication by paths
 
-      public readonly VerificationConditionGenerator /*!*/
-        parent;
+      public readonly VerificationConditionGenerator /*!*/ parent;
 
       public Implementation /*!*/ Implementation => Run.Implementation;
 

Source/VCGeneration/VerificationConditionGenerator.cs

@@ -32,7 +32,7 @@ record ImplementationTransformationData
 
   public class VerificationConditionGenerator : ConditionGeneration
   {
-    private static ConditionalWeakTable<Implementation, ImplementationTransformationData> implementationData = new();
+    private static readonly ConditionalWeakTable<Implementation, ImplementationTransformationData> implementationData = new();
 
 
     /// <summary>