diff --git a/Source/AbstractInterpretation/NativeLattice.cs b/Source/AbstractInterpretation/NativeLattice.cs
index 2efc1f0bf..2881152ce 100644
--- a/Source/AbstractInterpretation/NativeLattice.cs
+++ b/Source/AbstractInterpretation/NativeLattice.cs
@@ -185,8 +185,7 @@ public void Analyze(Implementation impl, NativeLattice lattice, NativeLattice.El
       // We need to keep track of some information for each(some) block(s).  To do that efficiently,
       // we number the implementation's blocks sequentially, and then we can use arrays to store
       // the additional information.
-      var pre = new NativeLattice.Element[impl.Blocks
-        .Count]; // set to null if we never compute a join/widen at this block
+      var pre = new NativeLattice.Element[impl.Blocks.Count]; // set to null if we never compute a join/widen at this block
       var post = options.InstrumentInfer == CoreOptions.InstrumentationPlaces.Everywhere
         ? new NativeLattice.Element[impl.Blocks.Count]
         : null;
@@ -195,7 +194,7 @@ public void Analyze(Implementation impl, NativeLattice lattice, NativeLattice.El
       int n = 0;
       foreach (var block in impl.Blocks)
       {
-        block.aiId = n;
+        block.AiId = n;
         // Note:  The forward analysis below will store lattice elements in pre[n] if pre[n] is non-null.
         // Thus, the assignment "pre[n] = bottom;" below must be done under the following condition:
         //    n == 0 || block.widenBlock
@@ -219,7 +218,7 @@ public void Analyze(Implementation impl, NativeLattice lattice, NativeLattice.El
       {
         var workItem = workItems.Dequeue();
         var b = workItem.Item1;
-        var id = b.aiId;
+        var id = b.AiId;
         var e = workItem.Item2;
         if (pre[id] == null)
         {
@@ -230,7 +229,7 @@ public void Analyze(Implementation impl, NativeLattice lattice, NativeLattice.El
           // no change
           continue;
         }
-        else if (b.widenBlock && options.Ai.StepsBeforeWidening <= iterations[id])
+        else if (b.WidenBlock && options.Ai.StepsBeforeWidening <= iterations[id])
         {
           e = lattice.Widen(pre[id], e);
           pre[id] = e;
@@ -275,8 +274,8 @@ void Instrument(Implementation impl, NativeLattice.Element[] pre, NativeLattice.
 
       foreach (var b in impl.Blocks)
       {
-        var element = pre[b.aiId];
-        if (element != null && (b.widenBlock || options.InstrumentInfer ==
+        var element = pre[b.AiId];
+        if (element != null && (b.WidenBlock || options.InstrumentInfer ==
           CoreOptions.InstrumentationPlaces.Everywhere))
         {
           List<Cmd> newCommands = new List<Cmd>();
@@ -294,9 +293,9 @@ void Instrument(Implementation impl, NativeLattice.Element[] pre, NativeLattice.
 
           newCommands.Add(cmd);
           newCommands.AddRange(b.Cmds);
-          if (post != null && post[b.aiId] != null)
+          if (post != null && post[b.AiId] != null)
           {
-            inv = post[b.aiId].ToExpr(options);
+            inv = post[b.AiId].ToExpr(options);
             kv = new QKeyValue(Token.NoToken, "inferred", new List<object>(), null);
             if (options.InstrumentWithAsserts)
             {
diff --git a/Source/AbstractInterpretation/Traverse.cs b/Source/AbstractInterpretation/Traverse.cs
index 1a1315c51..69a6d361f 100644
--- a/Source/AbstractInterpretation/Traverse.cs
+++ b/Source/AbstractInterpretation/Traverse.cs
@@ -54,7 +54,7 @@ static void Visit(Block b)
       {
         cce.BeginExpose(b);
         // we got here through a back-edge
-        b.widenBlock = true;
+        b.WidenBlock = true;
         cce.EndExpose();
       }
       else if (b.TraversingStatus == Block.VisitState.AlreadyVisited)
@@ -111,7 +111,7 @@ static void Visit(Block b)
     /// </summary>
     public static List<Block> ComputeLoopBodyFrom(Block block)
     {
-      Contract.Requires(block.widenBlock);
+      Contract.Requires(block.WidenBlock);
       Contract.Requires(block != null);
       Contract.Ensures(cce.NonNullElements(Contract.Result<List<Block>>()));
 
diff --git a/Source/Concurrency/LinearPermissionInstrumentation.cs b/Source/Concurrency/LinearPermissionInstrumentation.cs
index f1a799bfe..9da3f1fb8 100644
--- a/Source/Concurrency/LinearPermissionInstrumentation.cs
+++ b/Source/Concurrency/LinearPermissionInstrumentation.cs
@@ -61,10 +61,10 @@ public List<Cmd> DisjointnessAndWellFormedAssumeCmds(Absy absy, bool addGlobals)
     public void AddDisjointnessAndWellFormedAssumptions(Implementation impl)
     {
       // calls and parallel calls
-      foreach (var b in impl.Blocks)
+      foreach (var block in impl.Blocks)
       {
         var newCmds = new List<Cmd>();
-        foreach (var cmd in b.Cmds)
+        foreach (var cmd in block.Cmds)
         {
           newCmds.Add(cmd);
           if (cmd is ParCallCmd)
@@ -72,7 +72,7 @@ public void AddDisjointnessAndWellFormedAssumptions(Implementation impl)
             newCmds.AddRange(DisjointnessAndWellFormedAssumeCmds(cmd, true));
           }
         }
-        b.Cmds = newCmds;
+        block.Cmds = newCmds;
       }
 
       // loop headers
diff --git a/Source/Concurrency/LinearTypeChecker.cs b/Source/Concurrency/LinearTypeChecker.cs
index 812616bf8..883bf4e71 100644
--- a/Source/Concurrency/LinearTypeChecker.cs
+++ b/Source/Concurrency/LinearTypeChecker.cs
@@ -852,14 +852,14 @@ void ProcessIfCmd(IfCmd ifCmd)
                   {
                     checkingContext.Error(ifCmd.tok, "access to linear store not allowed");
                   }
-                  stmtLists.Push(ifCmd.thn);
-                  if (ifCmd.elseIf != null)
+                  stmtLists.Push(ifCmd.Thn);
+                  if (ifCmd.ElseIf != null)
                   {
-                    ProcessIfCmd(ifCmd.elseIf);
+                    ProcessIfCmd(ifCmd.ElseIf);
                   }
-                  else if (ifCmd.elseBlock != null)
+                  else if (ifCmd.ElseBlock != null)
                   {
-                    stmtLists.Push(ifCmd.elseBlock);
+                    stmtLists.Push(ifCmd.ElseBlock);
                   }
                 }
                 ProcessIfCmd(ifCmd);
diff --git a/Source/Concurrency/YieldingProcInstrumentation.cs b/Source/Concurrency/YieldingProcInstrumentation.cs
index 71a3623f4..8fc55130e 100644
--- a/Source/Concurrency/YieldingProcInstrumentation.cs
+++ b/Source/Concurrency/YieldingProcInstrumentation.cs
@@ -474,65 +474,61 @@ private void DesugarConcurrency(Implementation impl, List<Cmd> preconditions)
 
       // add jumps to noninterferenceChecker, returnChecker, and refinementChecker blocks
       var implRefinementCheckingBlocks = new List<Block>();
-      foreach (var b in impl.Blocks)
-      {
-        if (b.TransferCmd is GotoCmd gotoCmd)
-        {
-          var targetBlocks = new List<Block>();
-          var addEdge = false;
-          foreach (var nextBlock in gotoCmd.LabelTargets)
-          {
-            if (nextBlock.cmds.Count > 0)
-            {
-              var cmd = nextBlock.cmds[0];
-              if (cmd is ParCallCmd parCallCmd)
-              {
-                foreach (var callCmd in parCallCmd.CallCmds)
-                {
-                  if (refinementBlocks.ContainsKey(callCmd))
-                  {
-                    var targetBlock = refinementBlocks[callCmd];
-                    FixUpImplRefinementCheckingBlock(targetBlock,
-                      CivlAttributes.IsCallMarked(callCmd)
-                        ? returnCheckerBlock
-                        : unchangedCheckerBlock);
-                    targetBlocks.Add(targetBlock);
-                    implRefinementCheckingBlocks.Add(targetBlock);
-                  }
-                }
-                addEdge = true;
-              }
-            }
+      foreach (var b in impl.Blocks) {
+        if (b.TransferCmd is not GotoCmd gotoCmd) {
+          b.TransferCmd = new GotoCmd(b.TransferCmd.tok,
+            new List<Block> { returnCheckerBlock, returnBlock, noninterferenceCheckerBlock });
+          continue;
+        }
+
+        var targetBlocks = new List<Block>();
+        var addEdge = false;
+        foreach (var nextBlock in gotoCmd.LabelTargets) {
+          if (nextBlock.Cmds.Count <= 0) {
+            continue;
           }
 
-          gotoCmd.AddTargets(targetBlocks);
-          if (addEdge)
-          {
-            AddEdge(gotoCmd, noninterferenceCheckerBlock);
-            if (blocksInYieldingLoops.Contains(b))
-            {
-              AddEdge(gotoCmd, unchangedCheckerBlock);
-            }
-            else
-            {
-              b.Cmds.AddRange(refinementInstrumentation.CreateActionEvaluationCmds());
-              AddEdge(gotoCmd, refinementCheckerBlock);
+          var cmd = nextBlock.Cmds[0];
+          if (cmd is not ParCallCmd parCallCmd) {
+            continue;
+          }
+
+          foreach (var callCmd in parCallCmd.CallCmds) {
+            if (!refinementBlocks.TryGetValue(callCmd, out var targetBlock)) {
+              continue;
             }
+
+            FixUpImplRefinementCheckingBlock(targetBlock,
+              CivlAttributes.IsCallMarked(callCmd)
+                ? returnCheckerBlock
+                : unchangedCheckerBlock);
+            targetBlocks.Add(targetBlock);
+            implRefinementCheckingBlocks.Add(targetBlock);
           }
+
+          addEdge = true;
         }
-        else
-        {
-          b.TransferCmd = new GotoCmd(b.TransferCmd.tok,
-            new List<Block> {returnCheckerBlock, returnBlock, noninterferenceCheckerBlock});
+
+        gotoCmd.AddTargets(targetBlocks);
+        if (!addEdge) {
+          continue;
+        }
+
+        AddEdge(gotoCmd, noninterferenceCheckerBlock);
+        if (blocksInYieldingLoops.Contains(b)) {
+          AddEdge(gotoCmd, unchangedCheckerBlock);
+        } else {
+          b.Cmds.AddRange(refinementInstrumentation.CreateActionEvaluationCmds());
+          AddEdge(gotoCmd, refinementCheckerBlock);
         }
       }
 
       // desugar ParCallCmd 
       foreach (Block b in impl.Blocks)
       {
-        if (b.cmds.Count > 0)
+        if (b.Cmds.Count > 0)
         {
-          var cmd = b.cmds[0];
+          var cmd = b.Cmds[0];
           if (cmd is ParCallCmd)
           {
             DesugarParCallCmdInBlock(b, blocksInYieldingLoops.Contains(b));
@@ -545,7 +541,9 @@ private void DesugarConcurrency(Implementation impl, List<Cmd> preconditions)
       impl.Blocks.Add(unchangedCheckerBlock);
       impl.Blocks.Add(returnCheckerBlock);
       impl.Blocks.Add(returnBlock);
-      impl.Blocks.AddRange(implRefinementCheckingBlocks);
+      foreach (var block in implRefinementCheckingBlocks) {
+        impl.Blocks.Add(block);
+      }
       impl.Blocks.Insert(0, CreateInitialBlock(impl, preconditions));
     }
 
@@ -578,11 +576,11 @@ private void SplitBlocks(Implementation impl)
       {
         var currTransferCmd = b.TransferCmd;
         int labelCount = 0;
-        int lastSplitIndex = b.cmds.Count;
-        for (int i = b.cmds.Count - 1; i >= 0; i--)
+        int lastSplitIndex = b.Cmds.Count;
+        for (int i = b.Cmds.Count - 1; i >= 0; i--)
         {
           var split = false;
-          var cmd = b.cmds[i];
+          var cmd = b.Cmds[i];
           if (cmd is ParCallCmd)
           {
             split = true;
@@ -590,7 +588,7 @@ private void SplitBlocks(Implementation impl)
 
           if (split)
           {
-            var newBlock = new Block(b.tok, $"{b.Label}_{labelCount++}", b.cmds.GetRange(i, lastSplitIndex - i),
+            var newBlock = new Block(b.tok, $"{b.Label}_{labelCount++}", b.Cmds.GetRange(i, lastSplitIndex - i),
               currTransferCmd);
             newBlocks.Add(newBlock);
             currTransferCmd = new GotoCmd(b.tok, new List<Block> {newBlock});
@@ -598,11 +596,13 @@ private void SplitBlocks(Implementation impl)
           }
         }
 
-        b.cmds = b.cmds.GetRange(0, lastSplitIndex);
+        b.Cmds = b.Cmds.GetRange(0, lastSplitIndex);
         b.TransferCmd = currTransferCmd;
       }
 
-      impl.Blocks.AddRange(newBlocks);
+      foreach (var newBlock in newBlocks) {
+        impl.Blocks.Add(newBlock);
+      }
     }
 
     private Block CreateNoninterferenceCheckerBlock()
@@ -714,8 +714,8 @@ private void DesugarParCallCmdInBlock(Block block, bool isBlockInYieldingLoop)
       newCmds.AddRange(CreateUpdatesToOldGlobalVars());
       newCmds.AddRange(refinementInstrumentation.CreateUpdatesToOldOutputVars());
       newCmds.AddRange(CreateUpdatesToPermissionCollector(parCallCmd));
-      newCmds.AddRange(block.cmds.GetRange(1, block.cmds.Count - 1));
-      block.cmds = newCmds;
+      newCmds.AddRange(block.Cmds.GetRange(1, block.Cmds.Count - 1));
+      block.Cmds = newCmds;
     }
 
     private Formal ParCallDesugarFormal(Variable v, int count, bool incoming)
diff --git a/Source/Core/AST/Expression/AbsyExpr.cs b/Source/Core/AST/Expression/AbsyExpr.cs
index 06305894f..d433e0739 100644
--- a/Source/Core/AST/Expression/AbsyExpr.cs
+++ b/Source/Core/AST/Expression/AbsyExpr.cs
@@ -3890,7 +3890,7 @@ public class CodeExpr : Expr
     public List<Variable> /*!*/
       LocVars;
 
-    [Rep] public List<Block /*!*/> /*!*/ Blocks;
+    [Rep] public IList<Block /*!*/> /*!*/ Blocks;
 
     [ContractInvariantMethod]
     void ObjectInvariant()
diff --git a/Source/Core/AST/GotoBoogie/Block.cs b/Source/Core/AST/GotoBoogie/Block.cs
index 0bc535bdb..7ec347060 100644
--- a/Source/Core/AST/GotoBoogie/Block.cs
+++ b/Source/Core/AST/GotoBoogie/Block.cs
@@ -7,37 +7,11 @@ namespace Microsoft.Boogie;
 
 public sealed class Block : Absy
 {
-  private string /*!*/ label; // Note, Label is mostly readonly, but it can change to the name of a nearby block during block coalescing and empty-block removal
+  public string /*!*/ Label { get; set; } // Note, Label is mostly readonly, but it can change to the name of a nearby block during block coalescing and empty-block removal
 
-  public string /*!*/ Label
-  {
-    get
-    {
-      Contract.Ensures(Contract.Result<string>() != null);
-      return this.label;
-    }
-    set
-    {
-      Contract.Requires(value != null);
-      this.label = value;
-    }
-  }
-
-  [Rep] [ElementsPeer] public List<Cmd> /*!*/ cmds;
-
-  public List<Cmd> /*!*/ Cmds
-  {
-    get
-    {
-      Contract.Ensures(Contract.Result<List<Cmd>>() != null);
-      return this.cmds;
-    }
-    set
-    {
-      Contract.Requires(value != null);
-      this.cmds = value;
-    }
-  }
+  [Rep] 
+  [ElementsPeer] 
+  public List<Cmd> /*!*/ Cmds;
 
   public IEnumerable<Block> Exits()
   {
@@ -54,10 +28,6 @@ public TransferCmd
 
   public byte[] Checksum;
 
-  // Abstract interpretation
-
-  // public bool currentlyTraversed;
-
   public enum VisitState
   {
     ToVisit,
@@ -67,17 +37,16 @@ public enum VisitState
 
   public VisitState TraversingStatus;
 
-  public int aiId; // block ID used by the abstract interpreter, which may change these numbers with each AI run
-  public bool widenBlock;
+  public int AiId; // block ID used by the abstract interpreter, which may change these numbers with each AI run
+  public bool WidenBlock;
 
-  public int
-    iterations; // Count the number of time we visited the block during fixpoint computation. Used to decide if we widen or not
+  public int Iterations; // Count the number of time we visited the block during fixpoint computation. Used to decide if we widen or not
 
   // VC generation and SCC computation
   public List<Block> /*!*/ Predecessors;
 
   // This field is used during passification to null-out entries in block2Incarnation dictionary early
-  public int succCount;
+  public int SuccCount;
 
   private HashSet<Variable /*!*/> liveVarsBefore;
 
@@ -112,8 +81,8 @@ public IEnumerable<Variable /*!*/> LiveVarsBefore
   [ContractInvariantMethod]
   void ObjectInvariant()
   {
-    Contract.Invariant(this.label != null);
-    Contract.Invariant(this.cmds != null);
+    Contract.Invariant(this.Label != null);
+    Contract.Invariant(this.Cmds != null);
     Contract.Invariant(cce.NonNullElements(this.liveVarsBefore, true));
   }
 
@@ -143,13 +112,13 @@ public Block(IToken tok, string /*!*/ label, List<Cmd> /*!*/ cmds, TransferCmd t
     Contract.Requires(label != null);
     Contract.Requires(cmds != null);
     Contract.Requires(tok != null);
-    this.label = label;
-    this.cmds = cmds;
+    this.Label = label;
+    this.Cmds = cmds;
     this.TransferCmd = transferCmd;
     this.Predecessors = new List<Block>();
     this.liveVarsBefore = null;
     this.TraversingStatus = VisitState.ToVisit;
-    this.iterations = 0;
+    this.Iterations = 0;
   }
 
   public void Emit(TokenTextWriter stream, int level)
@@ -163,7 +132,7 @@ public void Emit(TokenTextWriter stream, int level)
       stream.Options.PrintWithUniqueASTIds
         ? String.Format("h{0}^^{1}", this.GetHashCode(), this.Label)
         : this.Label,
-      this.widenBlock ? "  // cut point" : "");
+      this.WidenBlock ? "  // cut point" : "");
 
     foreach (Cmd /*!*/ c in this.Cmds)
     {
@@ -212,14 +181,14 @@ public void ResetAbstractInterpretationState()
   {
     //      this.currentlyTraversed = false;
     this.TraversingStatus = VisitState.ToVisit;
-    this.iterations = 0;
+    this.Iterations = 0;
   }
 
   [Pure]
   public override string ToString()
   {
     Contract.Ensures(Contract.Result<string>() != null);
-    return this.Label + (this.widenBlock ? "[w]" : "");
+    return this.Label + (this.WidenBlock ? "[w]" : "");
   }
 
   public override Absy StdDispatch(StandardVisitor visitor)
diff --git a/Source/Core/AST/GotoBoogie/GotoCmd.cs b/Source/Core/AST/GotoBoogie/GotoCmd.cs
index 9b7aa5340..acfefc7ae 100644
--- a/Source/Core/AST/GotoBoogie/GotoCmd.cs
+++ b/Source/Core/AST/GotoBoogie/GotoCmd.cs
@@ -7,7 +7,7 @@ namespace Microsoft.Boogie;
 
 public class GotoCmd : TransferCmd
 {
-  [Rep] public List<String> LabelNames;
+  [Rep] public List<string> LabelNames;
   [Rep] public List<Block> LabelTargets;
 
   public QKeyValue Attributes { get; set; }
@@ -19,28 +19,28 @@ void ObjectInvariant()
   }
 
   [NotDelayed]
-  public GotoCmd(IToken /*!*/ tok, List<String> /*!*/ labelSeq)
+  public GotoCmd(IToken /*!*/ tok, List<string> /*!*/ labels)
     : base(tok)
   {
     Contract.Requires(tok != null);
-    Contract.Requires(labelSeq != null);
-    this.LabelNames = labelSeq;
+    Contract.Requires(labels != null);
+    this.LabelNames = labels;
   }
 
-  public GotoCmd(IToken /*!*/ tok, List<String> /*!*/ labelSeq, List<Block> /*!*/ blockSeq)
+  public GotoCmd(IToken /*!*/ tok, List<string> /*!*/ labels, List<Block> /*!*/ blocks)
     : base(tok)
   {
     Contract.Requires(tok != null);
-    Contract.Requires(labelSeq != null);
-    Contract.Requires(blockSeq != null);
-    Debug.Assert(labelSeq.Count == blockSeq.Count);
-    for (int i = 0; i < labelSeq.Count; i++)
+    Contract.Requires(labels != null);
+    Contract.Requires(blocks != null);
+    Debug.Assert(labels.Count == blocks.Count);
+    for (int i = 0; i < labels.Count; i++)
     {
-      Debug.Assert(Equals(labelSeq[i], cce.NonNull(blockSeq[i]).Label));
+      Debug.Assert(Equals(labels[i], cce.NonNull(blocks[i]).Label));
     }
 
-    this.LabelNames = labelSeq;
-    this.LabelTargets = blockSeq;
+    this.LabelNames = labels;
+    this.LabelTargets = blocks;
   }
 
   public GotoCmd(IToken /*!*/ tok, List<Block> /*!*/ blockSeq)
@@ -49,7 +49,7 @@ public GotoCmd(IToken /*!*/ tok, List<Block> /*!*/ blockSeq)
     //requires (blockSeq[i] != null ==> blockSeq[i].Label != null);
     Contract.Requires(tok != null);
     Contract.Requires(blockSeq != null);
-    List<String> labelSeq = new List<String>();
+    List<string> labelSeq = new List<string>();
     for (int i = 0; i < blockSeq.Count; i++)
     {
       labelSeq.Add(cce.NonNull(blockSeq[i]).Label);
diff --git a/Source/Core/AST/Implementation.cs b/Source/Core/AST/Implementation.cs
index d1b497dfb..62d5438dd 100644
--- a/Source/Core/AST/Implementation.cs
+++ b/Source/Core/AST/Implementation.cs
@@ -10,10 +10,11 @@ namespace Microsoft.Boogie;
 public class Implementation : DeclWithFormals {
   public List<Variable> LocVars;
 
-  [Rep] public StmtList StructuredStmts;
+  [Rep] 
+  public StmtList StructuredStmts { get; set; }
 
-  [field: Rep]
-  public List<Block> Blocks {
+  [Rep]
+  public IList<Block> Blocks {
     get; 
     set;
   }
@@ -21,7 +22,7 @@ public List<Block> Blocks {
 
   // Blocks before applying passification etc.
   // Both are used only when /inline is set.
-  public List<Block> OriginalBlocks;
+  public IList<Block> OriginalBlocks;
   public List<Variable> OriginalLocVars;
     
   // Map filled in during passification to allow augmented error trace reporting
@@ -965,7 +966,7 @@ public void ComputePredecessorsForBlocks()
     this.BlockPredecessorsComputed = true;
   }
 
-  public static void ComputePredecessorsForBlocks(List<Block> blocks)
+  public static void ComputePredecessorsForBlocks(IList<Block> blocks)
   {
     foreach (var block in blocks) {
       if (block.TransferCmd is not GotoCmd gtc) {
diff --git a/Source/Core/AST/Program.cs b/Source/Core/AST/Program.cs
index 810b73232..fe1b21359 100644
--- a/Source/Core/AST/Program.cs
+++ b/Source/Core/AST/Program.cs
@@ -498,7 +498,7 @@ public static Graph<Implementation> BuildCallGraph(CoreOptions options, Program
     return callGraph;
   }
 
-  public static Graph<Block> GraphFromBlocksSubset(IReadOnlyList<Block> blocks, IReadOnlySet<Block> subset = null, bool forward = true)
+  public static Graph<Block> GraphFromBlocksSubset(IList<Block> blocks, IReadOnlySet<Block> subset = null, bool forward = true)
   {
     var result = new Graph<Block>();
     if (!blocks.Any())
@@ -529,7 +529,7 @@ void AddEdge(Block a, Block b) {
     return result;
   }
   
-  public static Graph<Block> GraphFromBlocks(IReadOnlyList<Block> blocks, bool forward = true) {
+  public static Graph<Block> GraphFromBlocks(IList<Block> blocks, bool forward = true) {
     return GraphFromBlocksSubset(blocks, null, forward);
   }
 
diff --git a/Source/Core/AST/StructuredBoogie/BigBlock.cs b/Source/Core/AST/StructuredBoogie/BigBlock.cs
index 0fbe65e52..dc0370a4a 100644
--- a/Source/Core/AST/StructuredBoogie/BigBlock.cs
+++ b/Source/Core/AST/StructuredBoogie/BigBlock.cs
@@ -79,8 +79,7 @@ public TransferCmd tc
     }
   }
 
-  public BigBlock
-    successorBigBlock; // semantic successor (may be a back-edge, pointing back to enclosing while statement); null if successor is end of procedure body (or if field has not yet been initialized)
+  public BigBlock SuccessorBigBlock; // semantic successor (may be a back-edge, pointing back to enclosing while statement); null if successor is end of procedure body (or if field has not yet been initialized)
 
   public BigBlock(IToken tok, string labelName, [Captured] List<Cmd> simpleCmds, StructuredCmd ec, TransferCmd tc)
   {
diff --git a/Source/Core/AST/StructuredBoogie/BigBlocksResolutionContext.cs b/Source/Core/AST/StructuredBoogie/BigBlocksResolutionContext.cs
index a6974fc07..1172696f5 100644
--- a/Source/Core/AST/StructuredBoogie/BigBlocksResolutionContext.cs
+++ b/Source/Core/AST/StructuredBoogie/BigBlocksResolutionContext.cs
@@ -65,9 +65,9 @@ private void ComputeAllLabels(StructuredCmd cmd)
     if (cmd is IfCmd)
     {
       IfCmd ifCmd = (IfCmd) cmd;
-      ComputeAllLabels(ifCmd.thn);
-      ComputeAllLabels(ifCmd.elseIf);
-      ComputeAllLabels(ifCmd.elseBlock);
+      ComputeAllLabels(ifCmd.Thn);
+      ComputeAllLabels(ifCmd.ElseIf);
+      ComputeAllLabels(ifCmd.ElseBlock);
     }
     else if (cmd is WhileCmd)
     {
@@ -106,7 +106,7 @@ public List<Block /*!*/> /*!*/ Blocks
         NameAnonymousBlocks(stmtList);
 
         // determine successor blocks
-        RecordSuccessors(stmtList, null);
+        AssignSuccessors(stmtList, null);
 
         if (this.errorHandler.count == startErrorCount)
         {
@@ -141,15 +141,15 @@ void InjectEmptyBigBlockInsideWhileLoopBody(StructuredCmd structuredCmd)
     }
     else if (structuredCmd is IfCmd ifCmd)
     {
-      InjectEmptyBigBlockInsideWhileLoopBody(ifCmd.thn);
-      if (ifCmd.elseBlock != null)
+      InjectEmptyBigBlockInsideWhileLoopBody(ifCmd.Thn);
+      if (ifCmd.ElseBlock != null)
       {
-        InjectEmptyBigBlockInsideWhileLoopBody(ifCmd.elseBlock);
+        InjectEmptyBigBlockInsideWhileLoopBody(ifCmd.ElseBlock);
       }
 
-      if (ifCmd.elseIf != null)
+      if (ifCmd.ElseIf != null)
       {
-        InjectEmptyBigBlockInsideWhileLoopBody(ifCmd.elseIf);
+        InjectEmptyBigBlockInsideWhileLoopBody(ifCmd.ElseIf);
       }
     }
   }
@@ -165,11 +165,11 @@ void CheckLegalLabels(StmtList stmtList, StmtList parentContext, BigBlock parent
     stmtList.ParentBigBlock = parentBigBlock;
 
     // record the labels declared in this StmtList
-    foreach (BigBlock b in stmtList.BigBlocks)
+    foreach (BigBlock bigBlock in stmtList.BigBlocks)
     {
-      if (b.LabelName != null)
+      if (bigBlock.LabelName != null)
       {
-        string n = b.LabelName;
+        string n = bigBlock.LabelName;
         if (n.StartsWith(prefix))
         {
           if (prefix.Length < n.Length && n[prefix.Length] == '0')
@@ -182,17 +182,17 @@ void CheckLegalLabels(StmtList stmtList, StmtList parentContext, BigBlock parent
           }
         }
 
-        stmtList.AddLabel(b.LabelName);
+        stmtList.AddLabel(bigBlock.LabelName);
       }
     }
 
     // check that labels in this and nested StmtList's are legal
-    foreach (BigBlock b in stmtList.BigBlocks)
+    foreach (var bigBlock in stmtList.BigBlocks)
     {
       // goto's must reference blocks in enclosing blocks
-      if (b.tc is GotoCmd)
+      if (bigBlock.tc is GotoCmd)
       {
-        GotoCmd g = (GotoCmd) b.tc;
+        GotoCmd g = (GotoCmd) bigBlock.tc;
         foreach (string /*!*/ lbl in cce.NonNull(g.LabelNames))
         {
           Contract.Assert(lbl != null);
@@ -216,9 +216,9 @@ void CheckLegalLabels(StmtList stmtList, StmtList parentContext, BigBlock parent
       }
 
       // break labels must refer to an enclosing while statement
-      else if (b.ec is BreakCmd)
+      else if (bigBlock.ec is BreakCmd)
       {
-        BreakCmd bcmd = (BreakCmd) b.ec;
+        BreakCmd bcmd = (BreakCmd) bigBlock.ec;
         Contract.Assert(bcmd.BreakEnclosure == null); // it hasn't been initialized yet
         bool found = false;
         for (StmtList sl = stmtList; sl.ParentBigBlock != null; sl = sl.ParentContext)
@@ -271,19 +271,19 @@ void CheckLegalLabels(StmtList stmtList, StmtList parentContext, BigBlock parent
       }
 
       // recurse
-      else if (b.ec is WhileCmd)
+      else if (bigBlock.ec is WhileCmd)
       {
-        WhileCmd wcmd = (WhileCmd) b.ec;
-        CheckLegalLabels(wcmd.Body, stmtList, b);
+        WhileCmd wcmd = (WhileCmd) bigBlock.ec;
+        CheckLegalLabels(wcmd.Body, stmtList, bigBlock);
       }
       else
       {
-        for (IfCmd ifcmd = b.ec as IfCmd; ifcmd != null; ifcmd = ifcmd.elseIf)
+        for (IfCmd ifcmd = bigBlock.ec as IfCmd; ifcmd != null; ifcmd = ifcmd.ElseIf)
         {
-          CheckLegalLabels(ifcmd.thn, stmtList, b);
-          if (ifcmd.elseBlock != null)
+          CheckLegalLabels(ifcmd.Thn, stmtList, bigBlock);
+          if (ifcmd.ElseBlock != null)
           {
-            CheckLegalLabels(ifcmd.elseBlock, stmtList, b);
+            CheckLegalLabels(ifcmd.ElseBlock, stmtList, bigBlock);
           }
         }
       }
@@ -293,58 +293,57 @@ void CheckLegalLabels(StmtList stmtList, StmtList parentContext, BigBlock parent
   void NameAnonymousBlocks(StmtList stmtList)
   {
     Contract.Requires(stmtList != null);
-    foreach (BigBlock b in stmtList.BigBlocks)
+    foreach (var bigBlock in stmtList.BigBlocks)
     {
-      if (b.LabelName == null)
+      if (bigBlock.LabelName == null)
       {
-        b.LabelName = prefix + FreshAnon();
+        bigBlock.LabelName = prefix + FreshAnon();
       }
 
-      if (b.ec is WhileCmd)
+      if (bigBlock.ec is WhileCmd)
       {
-        WhileCmd wcmd = (WhileCmd) b.ec;
+        WhileCmd wcmd = (WhileCmd) bigBlock.ec;
         NameAnonymousBlocks(wcmd.Body);
       }
       else
       {
-        for (IfCmd ifcmd = b.ec as IfCmd; ifcmd != null; ifcmd = ifcmd.elseIf)
+        for (IfCmd ifcmd = bigBlock.ec as IfCmd; ifcmd != null; ifcmd = ifcmd.ElseIf)
         {
-          NameAnonymousBlocks(ifcmd.thn);
-          if (ifcmd.elseBlock != null)
+          NameAnonymousBlocks(ifcmd.Thn);
+          if (ifcmd.ElseBlock != null)
           {
-            NameAnonymousBlocks(ifcmd.elseBlock);
+            NameAnonymousBlocks(ifcmd.ElseBlock);
           }
         }
       }
     }
   }
 
-  void RecordSuccessors(StmtList stmtList, BigBlock successor)
+  private static void AssignSuccessors(StmtList stmtList, BigBlock next)
   {
     Contract.Requires(stmtList != null);
     for (int i = stmtList.BigBlocks.Count; 0 <= --i;)
     {
-      BigBlock big = stmtList.BigBlocks[i];
-      big.successorBigBlock = successor;
+      BigBlock current = stmtList.BigBlocks[i];
+      current.SuccessorBigBlock = next;
 
-      if (big.ec is WhileCmd)
+      if (current.ec is WhileCmd whileCmd)
       {
-        WhileCmd wcmd = (WhileCmd) big.ec;
-        RecordSuccessors(wcmd.Body, big);
+        AssignSuccessors(whileCmd.Body, current);
       }
       else
       {
-        for (IfCmd ifcmd = big.ec as IfCmd; ifcmd != null; ifcmd = ifcmd.elseIf)
+        for (IfCmd ifcmd = current.ec as IfCmd; ifcmd != null; ifcmd = ifcmd.ElseIf)
         {
-          RecordSuccessors(ifcmd.thn, successor);
-          if (ifcmd.elseBlock != null)
+          AssignSuccessors(ifcmd.Thn, next);
+          if (ifcmd.ElseBlock != null)
           {
-            RecordSuccessors(ifcmd.elseBlock, successor);
+            AssignSuccessors(ifcmd.ElseBlock, next);
           }
         }
       }
 
-      successor = big;
+      next = current;
     }
   }
 
@@ -354,221 +353,231 @@ void CreateBlocks(StmtList stmtList, string runOffTheEndLabel)
   {
     Contract.Requires(stmtList != null);
     Contract.Requires(blocks != null);
-    List<Cmd> cmdPrefixToApply = stmtList.PrefixCommands;
+    var cmdPrefixToApply = stmtList.PrefixCommands;
 
-    int n = stmtList.BigBlocks.Count;
-    foreach (BigBlock b in stmtList.BigBlocks)
+    int remainingBigBlocks = stmtList.BigBlocks.Count;
+    foreach (var bigBlock in stmtList.BigBlocks)
     {
-      n--;
-      Contract.Assert(b.LabelName != null);
+      remainingBigBlocks--;
+      Contract.Assert(bigBlock.LabelName != null);
       List<Cmd> theSimpleCmds;
       if (cmdPrefixToApply == null)
       {
-        theSimpleCmds = b.simpleCmds;
+        theSimpleCmds = bigBlock.simpleCmds;
       }
       else
       {
         theSimpleCmds = new List<Cmd>();
         theSimpleCmds.AddRange(cmdPrefixToApply);
-        theSimpleCmds.AddRange(b.simpleCmds);
+        theSimpleCmds.AddRange(bigBlock.simpleCmds);
         cmdPrefixToApply = null; // now, we've used 'em up
       }
 
-      if (b.tc != null)
+      if (bigBlock.tc != null)
       {
         // this BigBlock has the very same components as a Block
-        Contract.Assert(b.ec == null);
-        Block block = new Block(b.tok, b.LabelName, theSimpleCmds, b.tc);
+        Contract.Assert(bigBlock.ec == null);
+        Block block = new Block(bigBlock.tok, bigBlock.LabelName, theSimpleCmds, bigBlock.tc);
         blocks.Add(block);
       }
-      else if (b.ec == null)
-      {
-        TransferCmd trCmd;
-        if (n == 0 && runOffTheEndLabel != null)
-        {
-          // goto the given label instead of the textual successor block
-          trCmd = new GotoCmd(stmtList.EndCurly, new List<String> {runOffTheEndLabel});
-        }
-        else
-        {
-          trCmd = GotoSuccessor(stmtList.EndCurly, b);
-        }
-
-        Block block = new Block(b.tok, b.LabelName, theSimpleCmds, trCmd);
-        blocks.Add(block);
-      }
-      else if (b.ec is BreakCmd)
-      {
-        BreakCmd bcmd = (BreakCmd) b.ec;
-        Contract.Assert(bcmd.BreakEnclosure != null);
-        Block block = new Block(b.tok, b.LabelName, theSimpleCmds, GotoSuccessor(b.ec.tok, bcmd.BreakEnclosure));
-        blocks.Add(block);
-      }
-      else if (b.ec is WhileCmd)
-      {
-        WhileCmd wcmd = (WhileCmd) b.ec;
-        var a = FreshAnon();
-        string loopHeadLabel = prefix + a + "_LoopHead";
-        string /*!*/
-          loopBodyLabel = prefix + a + "_LoopBody";
-        string loopDoneLabel = prefix + a + "_LoopDone";
-
-        List<Cmd> ssBody = new List<Cmd>();
-        List<Cmd> ssDone = new List<Cmd>();
-        if (wcmd.Guard != null)
-        {
-          var ac = new AssumeCmd(wcmd.tok, wcmd.Guard);
-          ac.Attributes = new QKeyValue(wcmd.tok, "partition", new List<object>(), null);
-          ssBody.Add(ac);
-
-          ac = new AssumeCmd(wcmd.tok, Expr.Not(wcmd.Guard));
-          ac.Attributes = new QKeyValue(wcmd.tok, "partition", new List<object>(), null);
-          ssDone.Add(ac);
-        }
-
-        // Try to squeeze in ssBody into the first block of wcmd.Body
-        bool bodyGuardTakenCareOf = wcmd.Body.PrefixFirstBlock(ssBody, ref loopBodyLabel);
-
-        // ... goto LoopHead;
-        Block block = new Block(b.tok, b.LabelName, theSimpleCmds,
-          new GotoCmd(wcmd.tok, new List<String> {loopHeadLabel}));
-        blocks.Add(block);
-
-        // LoopHead: assert/assume loop_invariant; goto LoopDone, LoopBody;
-        List<Cmd> ssHead = new List<Cmd>();
-        foreach (CallCmd yield in wcmd.Yields)
-        {
-          ssHead.Add(yield);
-        }
-        foreach (PredicateCmd inv in wcmd.Invariants)
-        {
-          ssHead.Add(inv);
-        }
-
-        block = new Block(wcmd.tok, loopHeadLabel, ssHead,
-          new GotoCmd(wcmd.tok, new List<String> {loopDoneLabel, loopBodyLabel}));
-        blocks.Add(block);
-
-        if (!bodyGuardTakenCareOf)
-        {
-          // LoopBody: assume guard; goto firstLoopBlock;
-          block = new Block(wcmd.tok, loopBodyLabel, ssBody,
-            new GotoCmd(wcmd.tok, new List<String> {wcmd.Body.BigBlocks[0].LabelName}));
-          blocks.Add(block);
-        }
-
-        // recurse to create the blocks for the loop body
-        CreateBlocks(wcmd.Body, loopHeadLabel);
-
-        // LoopDone: assume !guard; goto loopSuccessor;
-        TransferCmd trCmd;
-        if (n == 0 && runOffTheEndLabel != null)
-        {
-          // goto the given label instead of the textual successor block
-          trCmd = new GotoCmd(wcmd.tok, new List<String> {runOffTheEndLabel});
-        }
-        else
-        {
-          trCmd = GotoSuccessor(wcmd.tok, b);
-        }
-
-        block = new Block(wcmd.tok, loopDoneLabel, ssDone, trCmd);
-        blocks.Add(block);
-      }
-      else
-      {
-        IfCmd ifcmd = (IfCmd) b.ec;
-        string predLabel = b.LabelName;
-        List<Cmd> predCmds = theSimpleCmds;
-
-        for (; ifcmd != null; ifcmd = ifcmd.elseIf)
+      else {
+        switch (bigBlock.ec)
         {
-          var a = FreshAnon();
-          string thenLabel = prefix + a + "_Then";
-          Contract.Assert(thenLabel != null);
-          string elseLabel = prefix + a + "_Else";
-          Contract.Assert(elseLabel != null);
-
-          List<Cmd> ssThen = new List<Cmd>();
-          List<Cmd> ssElse = new List<Cmd>();
-          if (ifcmd.Guard != null)
+          case null:
           {
-            var ac = new AssumeCmd(ifcmd.tok, ifcmd.Guard);
-            ac.Attributes = new QKeyValue(ifcmd.tok, "partition", new List<object>(), null);
-            ssThen.Add(ac);
+            TransferCmd trCmd;
+            if (remainingBigBlocks == 0 && runOffTheEndLabel != null)
+            {
+              // goto the given label instead of the textual successor block
+              trCmd = new GotoCmd(stmtList.EndCurly, new List<String> {runOffTheEndLabel});
+            }
+            else
+            {
+              trCmd = GotoSuccessor(stmtList.EndCurly, bigBlock);
+            }
 
-            ac = new AssumeCmd(ifcmd.tok, Expr.Not(ifcmd.Guard));
-            ac.Attributes = new QKeyValue(ifcmd.tok, "partition", new List<object>(), null);
-            ssElse.Add(ac);
+            Block block = new Block(bigBlock.tok, bigBlock.LabelName, theSimpleCmds, trCmd);
+            blocks.Add(block);
+            break;
           }
-
-          // Try to squeeze in ssThen/ssElse into the first block of ifcmd.thn/ifcmd.elseBlock
-          bool thenGuardTakenCareOf = ifcmd.thn.PrefixFirstBlock(ssThen, ref thenLabel);
-          bool elseGuardTakenCareOf = false;
-          if (ifcmd.elseBlock != null)
+          case BreakCmd breakCmd:
           {
-            elseGuardTakenCareOf = ifcmd.elseBlock.PrefixFirstBlock(ssElse, ref elseLabel);
+            BreakCmd bcmd = breakCmd;
+            Contract.Assert(bcmd.BreakEnclosure != null);
+            Block block = new Block(bigBlock.tok, bigBlock.LabelName, theSimpleCmds, GotoSuccessor(breakCmd.tok, bcmd.BreakEnclosure));
+            blocks.Add(block);
+            break;
           }
+          case WhileCmd whileCmd:
+          {
+            WhileCmd wcmd = whileCmd;
+            var a = FreshAnon();
+            string loopHeadLabel = prefix + a + "_LoopHead";
+            string /*!*/
+              loopBodyLabel = prefix + a + "_LoopBody";
+            string loopDoneLabel = prefix + a + "_LoopDone";
+
+            List<Cmd> ssBody = new List<Cmd>();
+            List<Cmd> ssDone = new List<Cmd>();
+            if (wcmd.Guard != null)
+            {
+              var ac = new AssumeCmd(wcmd.tok, wcmd.Guard);
+              ac.Attributes = new QKeyValue(wcmd.tok, "partition", new List<object>(), null);
+              ssBody.Add(ac);
 
-          // ... goto Then, Else;
-          var jumpBlock = new Block(b.tok, predLabel, predCmds,
-            new GotoCmd(ifcmd.tok, new List<String> {thenLabel, elseLabel}));
-          blocks.Add(jumpBlock);
+              ac = new AssumeCmd(wcmd.tok, Expr.Not(wcmd.Guard));
+              ac.Attributes = new QKeyValue(wcmd.tok, "partition", new List<object>(), null);
+              ssDone.Add(ac);
+            }
 
-          if (!thenGuardTakenCareOf)
-          {
-            // Then: assume guard; goto firstThenBlock;
-            var thenJumpBlock = new Block(ifcmd.tok, thenLabel, ssThen,
-              new GotoCmd(ifcmd.tok, new List<String> {ifcmd.thn.BigBlocks[0].LabelName}));
-            blocks.Add(thenJumpBlock);
-          }
+            // Try to squeeze in ssBody into the first block of wcmd.Body
+            bool bodyGuardTakenCareOf = wcmd.Body.PrefixFirstBlock(ssBody, ref loopBodyLabel);
 
-          // recurse to create the blocks for the then branch
-          CreateBlocks(ifcmd.thn, n == 0 ? runOffTheEndLabel : null);
+            // ... goto LoopHead;
+            Block block = new Block(bigBlock.tok, bigBlock.LabelName, theSimpleCmds,
+              new GotoCmd(wcmd.tok, new List<String> {loopHeadLabel}));
+            blocks.Add(block);
 
-          if (ifcmd.elseBlock != null)
-          {
-            Contract.Assert(ifcmd.elseIf == null);
-            if (!elseGuardTakenCareOf)
+            // LoopHead: assert/assume loop_invariant; goto LoopDone, LoopBody;
+            List<Cmd> ssHead = new List<Cmd>();
+            foreach (CallCmd yield in wcmd.Yields)
+            {
+              ssHead.Add(yield);
+            }
+            foreach (PredicateCmd inv in wcmd.Invariants)
             {
-              // Else: assume !guard; goto firstElseBlock;
-              var elseJumpBlock = new Block(ifcmd.tok, elseLabel, ssElse,
-                new GotoCmd(ifcmd.tok, new List<String> {ifcmd.elseBlock.BigBlocks[0].LabelName}));
-              blocks.Add(elseJumpBlock);
+              ssHead.Add(inv);
             }
 
-            // recurse to create the blocks for the else branch
-            CreateBlocks(ifcmd.elseBlock, n == 0 ? runOffTheEndLabel : null);
-          }
-          else if (ifcmd.elseIf != null)
-          {
-            // this is an "else if"
-            predLabel = elseLabel;
-            predCmds = new List<Cmd>();
-            if (ifcmd.Guard != null)
+            block = new Block(wcmd.tok, loopHeadLabel, ssHead,
+              new GotoCmd(wcmd.tok, new List<String> {loopDoneLabel, loopBodyLabel}));
+            blocks.Add(block);
+
+            if (!bodyGuardTakenCareOf)
             {
-              var ac = new AssumeCmd(ifcmd.tok, Expr.Not(ifcmd.Guard));
-              ac.Attributes = new QKeyValue(ifcmd.tok, "partition", new List<object>(), null);
-              predCmds.Add(ac);
+              // LoopBody: assume guard; goto firstLoopBlock;
+              block = new Block(wcmd.tok, loopBodyLabel, ssBody,
+                new GotoCmd(wcmd.tok, new List<String> {wcmd.Body.BigBlocks[0].LabelName}));
+              blocks.Add(block);
             }
-          }
-          else
-          {
-            // no else alternative is specified, so else branch is just "skip"
-            // Else: assume !guard; goto ifSuccessor;
+
+            // recurse to create the blocks for the loop body
+            CreateBlocks(wcmd.Body, loopHeadLabel);
+
+            // LoopDone: assume !guard; goto loopSuccessor;
             TransferCmd trCmd;
-            if (n == 0 && runOffTheEndLabel != null)
+            if (remainingBigBlocks == 0 && runOffTheEndLabel != null)
             {
               // goto the given label instead of the textual successor block
-              trCmd = new GotoCmd(ifcmd.tok, new List<String> {runOffTheEndLabel});
+              trCmd = new GotoCmd(wcmd.tok, new List<String> {runOffTheEndLabel});
             }
             else
             {
-              trCmd = GotoSuccessor(ifcmd.tok, b);
+              trCmd = GotoSuccessor(wcmd.tok, bigBlock);
             }
 
-            var block = new Block(ifcmd.tok, elseLabel, ssElse, trCmd);
+            block = new Block(wcmd.tok, loopDoneLabel, ssDone, trCmd);
             blocks.Add(block);
+            break;
+          }
+          default:
+          {
+            IfCmd ifcmd = (IfCmd) bigBlock.ec;
+            string predLabel = bigBlock.LabelName;
+            List<Cmd> predCmds = theSimpleCmds;
+
+            for (; ifcmd != null; ifcmd = ifcmd.ElseIf)
+            {
+              var a = FreshAnon();
+              string thenLabel = prefix + a + "_Then";
+              Contract.Assert(thenLabel != null);
+              string elseLabel = prefix + a + "_Else";
+              Contract.Assert(elseLabel != null);
+
+              List<Cmd> ssThen = new List<Cmd>();
+              List<Cmd> ssElse = new List<Cmd>();
+              if (ifcmd.Guard != null)
+              {
+                var ac = new AssumeCmd(ifcmd.tok, ifcmd.Guard);
+                ac.Attributes = new QKeyValue(ifcmd.tok, "partition", new List<object>(), null);
+                ssThen.Add(ac);
+
+                ac = new AssumeCmd(ifcmd.tok, Expr.Not(ifcmd.Guard));
+                ac.Attributes = new QKeyValue(ifcmd.tok, "partition", new List<object>(), null);
+                ssElse.Add(ac);
+              }
+
+              // Try to squeeze in ssThen/ssElse into the first block of ifcmd.thn/ifcmd.elseBlock
+              bool thenGuardTakenCareOf = ifcmd.Thn.PrefixFirstBlock(ssThen, ref thenLabel);
+              bool elseGuardTakenCareOf = false;
+              if (ifcmd.ElseBlock != null)
+              {
+                elseGuardTakenCareOf = ifcmd.ElseBlock.PrefixFirstBlock(ssElse, ref elseLabel);
+              }
+
+              // ... goto Then, Else;
+              var jumpBlock = new Block(bigBlock.tok, predLabel, predCmds,
+                new GotoCmd(ifcmd.tok, new List<String> {thenLabel, elseLabel}));
+              blocks.Add(jumpBlock);
+
+              if (!thenGuardTakenCareOf)
+              {
+                // Then: assume guard; goto firstThenBlock;
+                var thenJumpBlock = new Block(ifcmd.tok, thenLabel, ssThen,
+                  new GotoCmd(ifcmd.tok, new List<String> {ifcmd.Thn.BigBlocks[0].LabelName}));
+                blocks.Add(thenJumpBlock);
+              }
+
+              // recurse to create the blocks for the then branch
+              CreateBlocks(ifcmd.Thn, remainingBigBlocks == 0 ? runOffTheEndLabel : null);
+
+              if (ifcmd.ElseBlock != null)
+              {
+                Contract.Assert(ifcmd.ElseIf == null);
+                if (!elseGuardTakenCareOf)
+                {
+                  // Else: assume !guard; goto firstElseBlock;
+                  var elseJumpBlock = new Block(ifcmd.tok, elseLabel, ssElse,
+                    new GotoCmd(ifcmd.tok, new List<String> {ifcmd.ElseBlock.BigBlocks[0].LabelName}));
+                  blocks.Add(elseJumpBlock);
+                }
+
+                // recurse to create the blocks for the else branch
+                CreateBlocks(ifcmd.ElseBlock, remainingBigBlocks == 0 ? runOffTheEndLabel : null);
+              }
+              else if (ifcmd.ElseIf != null)
+              {
+                // this is an "else if"
+                predLabel = elseLabel;
+                predCmds = new List<Cmd>();
+                if (ifcmd.Guard != null)
+                {
+                  var ac = new AssumeCmd(ifcmd.tok, Expr.Not(ifcmd.Guard));
+                  ac.Attributes = new QKeyValue(ifcmd.tok, "partition", new List<object>(), null);
+                  predCmds.Add(ac);
+                }
+              }
+              else
+              {
+                // no else alternative is specified, so else branch is just "skip"
+                // Else: assume !guard; goto ifSuccessor;
+                TransferCmd trCmd;
+                if (remainingBigBlocks == 0 && runOffTheEndLabel != null)
+                {
+                  // goto the given label instead of the textual successor block
+                  trCmd = new GotoCmd(ifcmd.tok, new List<String> {runOffTheEndLabel});
+                }
+                else
+                {
+                  trCmd = GotoSuccessor(ifcmd.tok, bigBlock);
+                }
+
+                var block = new Block(ifcmd.tok, elseLabel, ssElse, trCmd);
+                blocks.Add(block);
+              }
+            }
+
+            break;
           }
         }
       }
@@ -580,9 +589,9 @@ TransferCmd GotoSuccessor(IToken tok, BigBlock b)
     Contract.Requires(b != null);
     Contract.Requires(tok != null);
     Contract.Ensures(Contract.Result<TransferCmd>() != null);
-    if (b.successorBigBlock != null)
+    if (b.SuccessorBigBlock != null)
     {
-      return new GotoCmd(new ImplicitJump(tok), new List<String> {b.successorBigBlock.LabelName});
+      return new GotoCmd(new ImplicitJump(tok), new List<string> {b.SuccessorBigBlock.LabelName});
     }
     else
     {
diff --git a/Source/Core/AST/StructuredBoogie/IfCmd.cs b/Source/Core/AST/StructuredBoogie/IfCmd.cs
index 5f29f407d..ed2dff9e3 100644
--- a/Source/Core/AST/StructuredBoogie/IfCmd.cs
+++ b/Source/Core/AST/StructuredBoogie/IfCmd.cs
@@ -6,52 +6,51 @@ public class IfCmd : StructuredCmd
 {
   public Expr Guard;
 
-  private StmtList /*!*/
-    _thn;
+  private StmtList /*!*/ thn;
 
-  public StmtList /*!*/ thn
+  public StmtList /*!*/ Thn
   {
     get
     {
       Contract.Ensures(Contract.Result<StmtList>() != null);
-      return this._thn;
+      return this.thn;
     }
     set
     {
       Contract.Requires(value != null);
-      this._thn = value;
+      this.thn = value;
     }
   }
 
-  private IfCmd _elseIf;
+  private IfCmd elseIf;
 
-  public IfCmd elseIf
+  public IfCmd ElseIf
   {
-    get { return this._elseIf; }
+    get { return this.elseIf; }
     set
     {
-      Contract.Requires(value == null || this.elseBlock == null);
-      this._elseIf = value;
+      Contract.Requires(value == null || this.ElseBlock == null);
+      this.elseIf = value;
     }
   }
 
-  private StmtList _elseBlock;
+  private StmtList elseBlock;
 
-  public StmtList elseBlock
+  public StmtList ElseBlock
   {
-    get { return this._elseBlock; }
+    get { return this.elseBlock; }
     set
     {
-      Contract.Requires(value == null || this.elseIf == null);
-      this._elseBlock = value;
+      Contract.Requires(value == null || this.ElseIf == null);
+      this.elseBlock = value;
     }
   }
 
   [ContractInvariantMethod]
   void ObjectInvariant()
   {
-    Contract.Invariant(this._thn != null);
-    Contract.Invariant(this._elseIf == null || this._elseBlock == null);
+    Contract.Invariant(this.thn != null);
+    Contract.Invariant(this.elseIf == null || this.elseBlock == null);
   }
 
   public IfCmd(IToken /*!*/ tok, Expr guard, StmtList /*!*/ thn, IfCmd elseIf, StmtList elseBlock)
@@ -61,9 +60,9 @@ public IfCmd(IToken /*!*/ tok, Expr guard, StmtList /*!*/ thn, IfCmd elseIf, Stm
     Contract.Requires(thn != null);
     Contract.Requires(elseIf == null || elseBlock == null);
     this.Guard = guard;
-    this._thn = thn;
-    this._elseIf = elseIf;
-    this._elseBlock = elseBlock;
+    this.thn = thn;
+    this.elseIf = elseIf;
+    this.elseBlock = elseBlock;
   }
 
   public override void Emit(TokenTextWriter stream, int level)
@@ -85,20 +84,20 @@ public override void Emit(TokenTextWriter stream, int level)
       stream.WriteLine(")");
 
       stream.WriteLine(level, "{");
-      ifcmd.thn.Emit(stream, level + 1);
+      ifcmd.Thn.Emit(stream, level + 1);
       stream.WriteLine(level, "}");
 
-      if (ifcmd.elseIf != null)
+      if (ifcmd.ElseIf != null)
       {
         stream.Write(level, "else if (");
-        ifcmd = ifcmd.elseIf;
+        ifcmd = ifcmd.ElseIf;
         continue;
       }
-      else if (ifcmd.elseBlock != null)
+      else if (ifcmd.ElseBlock != null)
       {
         stream.WriteLine(level, "else");
         stream.WriteLine(level, "{");
-        ifcmd.elseBlock.Emit(stream, level + 1);
+        ifcmd.ElseBlock.Emit(stream, level + 1);
         stream.WriteLine(level, "}");
       }
 
diff --git a/Source/Core/Analysis/BlockCoalescer.cs b/Source/Core/Analysis/BlockCoalescer.cs
index 60100930f..82ba4a099 100644
--- a/Source/Core/Analysis/BlockCoalescer.cs
+++ b/Source/Core/Analysis/BlockCoalescer.cs
@@ -79,7 +79,7 @@ public override Implementation VisitImplementation(Implementation impl)
     return impl;
   }
 
-  public static List<Block> CoalesceFromRootBlock(List<Block> blocks)
+  public static IList<Block> CoalesceFromRootBlock(IList<Block> blocks)
   {
     if (!blocks.Any())
     {
diff --git a/Source/Core/BasicTypeVisitor.cs b/Source/Core/BasicTypeVisitor.cs
index 3fd2ad5ad..a9aaeecf8 100644
--- a/Source/Core/BasicTypeVisitor.cs
+++ b/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);
diff --git a/Source/Core/Duplicator.cs b/Source/Core/Duplicator.cs
index 75ca3f65c..22b9db295 100644
--- a/Source/Core/Duplicator.cs
+++ b/Source/Core/Duplicator.cs
@@ -142,7 +142,7 @@ public override List<Block> VisitBlockSeq(List<Block> blockSeq)
       return base.VisitBlockSeq(new List<Block>(blockSeq));
     }
 
-    public override List<Block /*!*/> /*!*/ VisitBlockList(List<Block /*!*/> /*!*/ blocks)
+    public override IList<Block> /*!*/ VisitBlockList(IList<Block> blocks /*!*/ /*!*/)
     {
       //Contract.Requires(cce.NonNullElements(blocks));
       Contract.Ensures(cce.NonNullElements(Contract.Result<List<Block>>()));
diff --git a/Source/Core/Inline.cs b/Source/Core/Inline.cs
index d67732fa2..60e2c7a33 100644
--- a/Source/Core/Inline.cs
+++ b/Source/Core/Inline.cs
@@ -354,7 +354,7 @@ private int InlineCallCmd(Block block, CallCmd callCmd, Implementation impl, Lis
       return nextlblCount;
     }
 
-    public virtual List<Block /*!*/> /*!*/ DoInlineBlocks(List<Block /*!*/> /*!*/ blocks, ref bool inlinedSomething)
+    public virtual List<Block /*!*/> /*!*/ DoInlineBlocks(IList<Block /*!*/> /*!*/ blocks, ref bool inlinedSomething)
     {
       Contract.Requires(cce.NonNullElements(blocks));
       Contract.Ensures(cce.NonNullElements(Contract.Result<List<Block>>()));
@@ -625,8 +625,7 @@ private List<Cmd> RemoveAsserts(List<Cmd> cmds)
       Contract.Requires(codeCopier.oldSubstMap != null);
 
       Contract.Ensures(cce.NonNullElements(Contract.Result<List<Block>>()));
-      List<Block /*!*/> /*!*/
-        implBlocks = cce.NonNull(impl.OriginalBlocks);
+      var /*!*/ implBlocks = cce.NonNull(impl.OriginalBlocks);
       Contract.Assert(implBlocks.Count > 0);
 
       Procedure proc = impl.Proc;
diff --git a/Source/Core/StandardVisitor.cs b/Source/Core/StandardVisitor.cs
index 0c72da8df..e16f7160c 100644
--- a/Source/Core/StandardVisitor.cs
+++ b/Source/Core/StandardVisitor.cs
@@ -219,7 +219,7 @@ public virtual List<Block> VisitBlockSeq(List<Block> blockSeq)
       return blockSeq;
     }
 
-    public virtual List<Block /*!*/> /*!*/ VisitBlockList(List<Block /*!*/> /*!*/ blocks)
+    public virtual IList<Block> /*!*/ VisitBlockList(IList<Block> blocks /*!*/ /*!*/)
     {
       Contract.Requires(blocks != null);
       Contract.Ensures(Contract.Result<List<Block>>() != null);
@@ -1150,14 +1150,12 @@ public override List<Block> VisitBlockSeq(List<Block> blockSeq)
       return blockSeq;
     }
 
-    public override List<Block /*!*/> /*!*/ VisitBlockList(List<Block /*!*/> /*!*/ blocks)
+    public override IList<Block> /*!*/ VisitBlockList(IList<Block> blocks /*!*/ /*!*/)
     {
       Contract.Ensures(Contract.Result<List<Block>>() == blocks);
-      for (int i = 0, n = blocks.Count; i < n; i++)
-      {
-        this.VisitBlock(blocks[i]);
+      foreach (var block in blocks) {
+        this.VisitBlock(block);
       }
-
       return blocks;
     }
 
diff --git a/Source/Provers/LeanAuto/LeanAutoGenerator.cs b/Source/Provers/LeanAuto/LeanAutoGenerator.cs
index dde6fa6d1..82684398f 100644
--- a/Source/Provers/LeanAuto/LeanAutoGenerator.cs
+++ b/Source/Provers/LeanAuto/LeanAutoGenerator.cs
@@ -879,7 +879,7 @@ public override List<Block> VisitBlockSeq(List<Block> blockSeq)
     throw new LeanConversionException(Token.NoToken, $"Internal: List<Block> should never be directly visited ({blockSeq}).");
   }
 
-  public override List<Block> VisitBlockList(List<Block> blocks)
+  public override IList<Block> VisitBlockList(IList<Block> blocks)
   {
     throw new LeanConversionException(Token.NoToken, $"Internal: List<Block> should never be directly visited ({blocks}).");
   }
diff --git a/Source/Provers/SMTLib/SMTLibProcess.cs b/Source/Provers/SMTLib/SMTLibProcess.cs
index ac0627019..65fc55e62 100644
--- a/Source/Provers/SMTLib/SMTLibProcess.cs
+++ b/Source/Provers/SMTLib/SMTLibProcess.cs
@@ -69,7 +69,7 @@ public SMTLibProcess(SMTLibOptions libOptions, SMTLibSolverOptions options)
       }
       catch (System.ComponentModel.Win32Exception e)
       {
-        throw new ProverException(string.Format("Unable to start the process {0}: {1}", psi.FileName, e.Message));
+        throw new ProverException($"Unable to start the process {psi.FileName}: {e.Message}");
       }
     }
 
diff --git a/Source/UnitTests/ExecutionEngineTests/ExecutionEngineTest.cs b/Source/UnitTests/ExecutionEngineTests/ExecutionEngineTest.cs
index 85d1f41a1..7cfe2ef9d 100644
--- a/Source/UnitTests/ExecutionEngineTests/ExecutionEngineTest.cs
+++ b/Source/UnitTests/ExecutionEngineTests/ExecutionEngineTest.cs
@@ -252,7 +252,7 @@ public async Task LoopInvariantDescriptions()
 
     Parser.Parse(programString, "fakeFilename", out var program1);
     foreach (var block in program1.Implementations.First().Blocks) {
-      foreach (var cmd in block.cmds) {
+      foreach (var cmd in block.Cmds) {
         if (cmd is AssertCmd assertCmd) {
           assertCmd.Description = new FakeDescription();
         }
diff --git a/Source/VCExpr/Boogie2VCExpr.cs b/Source/VCExpr/Boogie2VCExpr.cs
index a4596afe0..8b4682f17 100644
--- a/Source/VCExpr/Boogie2VCExpr.cs
+++ b/Source/VCExpr/Boogie2VCExpr.cs
@@ -889,7 +889,7 @@ public override List<Block> VisitBlockSeq(List<Block> blockSeq)
       throw new cce.UnreachableException();
     }
 
-    public override List<Block /*!*/> /*!*/ VisitBlockList(List<Block /*!*/> /*!*/ blocks)
+    public override IList<Block> /*!*/ VisitBlockList(IList<Block> blocks /*!*/ /*!*/)
     {
       //Contract.Requires(cce.NonNullElements(blocks));
       Contract.Ensures(cce.NonNullElements(Contract.Result<List<Block>>()));
diff --git a/Source/VCGeneration/BlockTransformations.cs b/Source/VCGeneration/BlockTransformations.cs
index b0e72c7f3..561113331 100644
--- a/Source/VCGeneration/BlockTransformations.cs
+++ b/Source/VCGeneration/BlockTransformations.cs
@@ -99,7 +99,7 @@ private static bool ContainsAssert(Block b)
   
   public static bool IsNonTrivialAssert (Cmd c) { return c is AssertCmd { Expr: not LiteralExpr { asBool: true } }; }
 
-  private static void DeleteUselessBlocks(List<Block> blocks) {
+  private static void DeleteUselessBlocks(IList<Block> blocks) {
     var toVisit = new HashSet<Block>(blocks);
     var removed = new HashSet<Block>();
     while(toVisit.Count > 0) {
diff --git a/Source/VCGeneration/Checker.cs b/Source/VCGeneration/Checker.cs
index 49f23b1df..e4ff0b351 100644
--- a/Source/VCGeneration/Checker.cs
+++ b/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;
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index 13ee3a18a..cd720b8cb 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/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)
@@ -450,7 +450,7 @@ public static void EmitImpl(VCGenOptions options, ImplementationRun run, bool pr
       options.PrintDesugarings = oldPrintDesugaringSetting;
     }
 
-    public static void ResetPredecessors(List<Block> blocks)
+    public static void ResetPredecessors(IList<Block> blocks)
     {
       Contract.Requires(blocks != null);
       foreach (Block b in blocks)
@@ -686,7 +686,7 @@ protected Dictionary<Variable, Expr> Convert2PassiveCmd(ImplementationRun run, M
 
       var start = DateTime.UtcNow;
 
-      Dictionary<Variable, Expr> r = ConvertBlocks2PassiveCmd(run.OutputWriter, implementation.Blocks, implementation.Proc.Modifies, mvInfo, implementation.debugInfos);
+      var r = ConvertBlocks2PassiveCmd(run.OutputWriter, implementation.Blocks, implementation.Proc.Modifies, mvInfo, implementation.debugInfos);
 
       var end = DateTime.UtcNow;
 
@@ -722,7 +722,7 @@ protected Dictionary<Variable, Expr> Convert2PassiveCmd(ImplementationRun run, M
       return r;
     }
 
-    protected Dictionary<Variable, Expr> ConvertBlocks2PassiveCmd(TextWriter traceWriter, List<Block> blocks, List<IdentifierExpr> modifies,
+    protected Dictionary<Variable, Expr> ConvertBlocks2PassiveCmd(TextWriter traceWriter, IList<Block> blocks, List<IdentifierExpr> modifies,
       ModelViewInfo mvInfo, Dictionary<Cmd, List<object>> debugInfos)
     {
       Contract.Requires(blocks != null);
@@ -773,7 +773,7 @@ protected Dictionary<Variable, Expr> ConvertBlocks2PassiveCmd(TextWriter traceWr
         variableCollectors[b] = mvc;
         foreach (Block p in b.Predecessors)
         {
-          p.succCount--;
+          p.SuccCount--;
           if (p.Checksum != null)
           {
             // Compute the checksum based on the checksums of the predecessor. The order should not matter.
@@ -781,7 +781,7 @@ protected Dictionary<Variable, Expr> ConvertBlocks2PassiveCmd(TextWriter traceWr
           }
 
           mvc.AddUsedVariables(variableCollectors[p].UsedVariables);
-          if (p.succCount == 0)
+          if (p.SuccCount == 0)
           {
             block2Incarnation.Remove(p);
           }
@@ -792,12 +792,12 @@ protected Dictionary<Variable, Expr> ConvertBlocks2PassiveCmd(TextWriter traceWr
         GotoCmd gotoCmd = b.TransferCmd as GotoCmd;
         if (gotoCmd == null)
         {
-          b.succCount = 0;
+          b.SuccCount = 0;
         }
         else
         {
           // incarnationMap needs to be added only if there is some successor of b
-          b.succCount = gotoCmd.LabelNames.Count;
+          b.SuccCount = gotoCmd.LabelNames.Count;
           block2Incarnation.Add(b, incarnationMap);
         }
 
@@ -1427,7 +1427,7 @@ public Block CreateBlockBetween(int predIndex, Block succ)
       return newBlock;
     }
 
-    protected void AddBlocksBetween(List<Block> blocks)
+    protected void AddBlocksBetween(IList<Block> blocks)
     {
       Contract.Requires(blocks != null);
 
@@ -1451,7 +1451,9 @@ protected void AddBlocksBetween(List<Block> blocks)
         }
       }
 
-      blocks.AddRange(tweens); // must wait until iteration is done before changing the list
+      foreach (var tween in tweens) {
+        blocks.Add(tween); // must wait until iteration is done before changing the list
+      }
 
       #endregion
     }
diff --git a/Source/VCGeneration/ManualSplit.cs b/Source/VCGeneration/ManualSplit.cs
index 5b47299b7..e96cc73ea 100644
--- a/Source/VCGeneration/ManualSplit.cs
+++ b/Source/VCGeneration/ManualSplit.cs
@@ -11,7 +11,7 @@ public class ManualSplit : Split
   public IImplementationPartOrigin Token { get; }
   
   public ManualSplit(VCGenOptions options, 
-    Func<List<Block>> blocks, 
+    Func<IList<Block>> blocks, 
     VerificationConditionGenerator parent, 
     ImplementationRun run, 
     IImplementationPartOrigin origin, int? randomSeed = null) 
diff --git a/Source/VCGeneration/Prune/Pruner.cs b/Source/VCGeneration/Prune/Pruner.cs
index 39d479405..43af44c9d 100644
--- a/Source/VCGeneration/Prune/Pruner.cs
+++ b/Source/VCGeneration/Prune/Pruner.cs
@@ -57,7 +57,7 @@ public class Pruner {
      * See Checker.Setup for more information.
      * Data type constructor declarations are not pruned and they do affect VC generation.
      */
-    public static IEnumerable<Declaration> GetLiveDeclarations(VCGenOptions options, Program program, List<Block>? blocks)
+    public static IEnumerable<Declaration> GetLiveDeclarations(VCGenOptions options, Program program, IList<Block>? blocks)
     {
       if (program.DeclarationDependencies == null || blocks == null || !options.Prune)
       {
@@ -83,7 +83,7 @@ bool TraverseDeclaration(object parent, object child) {
       }
     }
 
-    private static RevealedState GetRevealedState(List<Block> blocks)
+    private static RevealedState GetRevealedState(IList<Block> blocks)
     {
       var controlFlowGraph = GetControlFlowGraph(blocks);
       var starts = controlFlowGraph.Nodes.Where(n => !controlFlowGraph.Predecessors(n).Any()).ToList();
@@ -97,7 +97,7 @@ private static RevealedState GetRevealedState(List<Block> blocks)
         Aggregate(RevealedState.AllHidden, RevealedAnalysis.MergeStates);
     }
 
-    public static Graph<Absy> GetControlFlowGraph(List<Block> blocks)
+    public static Graph<Absy> GetControlFlowGraph(IList<Block> blocks)
     {
       /*
        * Generally the blocks created by splitting have unset block.Predecessors fields
diff --git a/Source/VCGeneration/SmokeTester.cs b/Source/VCGeneration/SmokeTester.cs
index 350567ebb..140ee3319 100644
--- a/Source/VCGeneration/SmokeTester.cs
+++ b/Source/VCGeneration/SmokeTester.cs
@@ -262,7 +262,7 @@ async Task<bool> CheckUnreachable(TextWriter traceWriter, Block cur, List<Cmd> s
     Block copy = CopyBlock(cur);
     Contract.Assert(copy != null);
     copy.Cmds = seq;
-    List<Block> backup = run.Implementation.Blocks;
+    var backup = run.Implementation.Blocks;
     Contract.Assert(backup != null);
     run.Implementation.Blocks = GetCopiedBlocks();
     copy.TransferCmd = new ReturnCmd(Token.NoToken);
diff --git a/Source/VCGeneration/Splits/BlockRewriter.cs b/Source/VCGeneration/Splits/BlockRewriter.cs
index dc93dab28..717accf65 100644
--- a/Source/VCGeneration/Splits/BlockRewriter.cs
+++ b/Source/VCGeneration/Splits/BlockRewriter.cs
@@ -15,10 +15,10 @@ public class BlockRewriter {
   public List<Block> OrderedBlocks { get; }
   public VCGenOptions Options { get; }
   public Graph<Block> Dag { get; }
-  public Func<IImplementationPartOrigin, List<Block>, ManualSplit> CreateSplit { get; }
+  public Func<IImplementationPartOrigin, IList<Block>, ManualSplit> CreateSplit { get; }
 
-  public BlockRewriter(VCGenOptions options, List<Block> blocks,
-    Func<IImplementationPartOrigin, List<Block>, ManualSplit> createSplit) {
+  public BlockRewriter(VCGenOptions options, IList<Block> blocks,
+    Func<IImplementationPartOrigin, IList<Block>, ManualSplit> createSplit) {
     this.Options = options;
     CreateSplit = createSplit;
     Dag = Program.GraphFromBlocks(blocks);
diff --git a/Source/VCGeneration/Splits/FocusAttributeHandler.cs b/Source/VCGeneration/Splits/FocusAttributeHandler.cs
index 812d80407..9ed2eca04 100644
--- a/Source/VCGeneration/Splits/FocusAttributeHandler.cs
+++ b/Source/VCGeneration/Splits/FocusAttributeHandler.cs
@@ -19,7 +19,7 @@ public class FocusAttributeHandler {
   /// We recurse twice for each focus, leading to potentially 2^N splits
   /// </summary>
   public static List<ManualSplit> GetParts(VCGenOptions options, ImplementationRun run, 
-    Func<IImplementationPartOrigin, List<Block>, ManualSplit> createPart)
+    Func<IImplementationPartOrigin, IList<Block>, ManualSplit> createPart)
   {
     var rewriter = new BlockRewriter(options, run.Implementation.Blocks, createPart);
     
diff --git a/Source/VCGeneration/Splits/IsolateAttributeOnAssertsHandler.cs b/Source/VCGeneration/Splits/IsolateAttributeOnAssertsHandler.cs
index f08ee284f..137b678d6 100644
--- a/Source/VCGeneration/Splits/IsolateAttributeOnAssertsHandler.cs
+++ b/Source/VCGeneration/Splits/IsolateAttributeOnAssertsHandler.cs
@@ -12,7 +12,7 @@ namespace VCGeneration;
 class IsolateAttributeOnAssertsHandler {
 
   public static (List<ManualSplit> IsolatedParts, ManualSplit Remainder) GetParts(VCGenOptions options, ManualSplit partToDivide, 
-    Func<IImplementationPartOrigin, List<Block>, ManualSplit> createPart) {
+    Func<IImplementationPartOrigin, IList<Block>, ManualSplit> createPart) {
     var rewriter = new BlockRewriter(options, partToDivide.Blocks, createPart);
       
     var splitOnEveryAssert = partToDivide.Options.VcsSplitOnEveryAssert;
diff --git a/Source/VCGeneration/Splits/IsolateAttributeOnJumpsHandler.cs b/Source/VCGeneration/Splits/IsolateAttributeOnJumpsHandler.cs
index 9a26ea973..368cb9621 100644
--- a/Source/VCGeneration/Splits/IsolateAttributeOnJumpsHandler.cs
+++ b/Source/VCGeneration/Splits/IsolateAttributeOnJumpsHandler.cs
@@ -13,7 +13,7 @@ namespace VCGeneration;
 
 class IsolateAttributeOnJumpsHandler {
   public static (List<ManualSplit> Isolated, ManualSplit Remainder) GetParts(VCGenOptions options, ManualSplit partToDivide, 
-    Func<IImplementationPartOrigin, List<Block>, ManualSplit> createPart) {
+    Func<IImplementationPartOrigin, IList<Block>, ManualSplit> createPart) {
 
     var rewriter = new BlockRewriter(options, partToDivide.Blocks, createPart);
     
diff --git a/Source/VCGeneration/Splits/ManualSplitFinder.cs b/Source/VCGeneration/Splits/ManualSplitFinder.cs
index 934a2aa40..651ebdc44 100644
--- a/Source/VCGeneration/Splits/ManualSplitFinder.cs
+++ b/Source/VCGeneration/Splits/ManualSplitFinder.cs
@@ -11,7 +11,7 @@ namespace VCGeneration;
 public static class ManualSplitFinder {
   
   public static IEnumerable<ManualSplit> GetParts(VCGenOptions options, ImplementationRun run,
-    Func<IImplementationPartOrigin, List<Block>, ManualSplit> createPart) {
+    Func<IImplementationPartOrigin, IList<Block>, ManualSplit> createPart) {
     
     var focussedParts = FocusAttributeHandler.GetParts(options, run, createPart);
     var result = focussedParts.SelectMany(focussedPart =>
diff --git a/Source/VCGeneration/Splits/Split.cs b/Source/VCGeneration/Splits/Split.cs
index d34affb12..3b8b1c6e4 100644
--- a/Source/VCGeneration/Splits/Split.cs
+++ b/Source/VCGeneration/Splits/Split.cs
@@ -22,11 +22,11 @@ public class Split : ProofRun
 
       public int RandomSeed { get; }
 
-      private List<Block> blocks;
-      public List<Block> Blocks => blocks ??= getBlocks();
+      private IList<Block> blocks;
+      public IList<Block> Blocks => blocks ??= getBlocks();
 
       readonly List<Block> bigBlocks = new();
-      public List<AssertCmd> Asserts => Blocks.SelectMany(block => block.cmds.OfType<AssertCmd>()).ToList();
+      public List<AssertCmd> Asserts => Blocks.SelectMany(block => block.Cmds.OfType<AssertCmd>()).ToList();
       public IReadOnlyList<Declaration> prunedDeclarations;
       
       public IReadOnlyList<Declaration> PrunedDeclarations {
@@ -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;
 
@@ -74,7 +73,7 @@ public readonly VerificationConditionGenerator /*!*/
       public int SplitIndex { get; set; }
       public VerificationConditionGenerator.ErrorReporter reporter;
 
-      public Split(VCGenOptions options, Func<List<Block /*!*/>> /*!*/ getBlocks,
+      public Split(VCGenOptions options, Func<IList<Block /*!*/>> /*!*/ getBlocks,
         VerificationConditionGenerator /*!*/ parent, ImplementationRun run, int? randomSeed = null)
       {
         Contract.Requires(parent != null);
@@ -199,7 +198,7 @@ public void DumpDot(int splitNum)
       }
 
       int bsid;
-      private readonly Func<List<Block>> getBlocks;
+      private readonly Func<IList<Block>> getBlocks;
 
       BlockStats GetBlockStats(Block b)
       {
diff --git a/Source/VCGeneration/Splits/SplitAttributeHandler.cs b/Source/VCGeneration/Splits/SplitAttributeHandler.cs
index 8adb35a41..a71952000 100644
--- a/Source/VCGeneration/Splits/SplitAttributeHandler.cs
+++ b/Source/VCGeneration/Splits/SplitAttributeHandler.cs
@@ -77,7 +77,7 @@ private static bool ShouldSplitHere(Cmd c) {
     return predicateCmd.Attributes.FindBoolAttribute("split_here");
   }
 
-  private static Dictionary<Block, Cmd?> GetMapFromBlockStartToSplit(List<Block> blocks, Dictionary<Block, List<Cmd>> splitsPerBlock) {
+  private static Dictionary<Block, Cmd?> GetMapFromBlockStartToSplit(IList<Block> blocks, Dictionary<Block, List<Cmd>> splitsPerBlock) {
     var todo = new Stack<Block>();
     var blockAssignments = new Dictionary<Block, Cmd?>();
     var immediateDominators = Program.GraphFromBlocks(blocks).ImmediateDominator();
@@ -169,7 +169,7 @@ List<Cmd> GetCommandsForBlockWithSplit(Block currentBlock)
     }
   }
 
-  private static List<Block> UpdateBlocks(IReadOnlyList<Block> blocks,
+  private static List<Block> UpdateBlocks(IList<Block> blocks,
     Func<Block, List<Cmd>> getCommands)
   {
     var newBlocks = new List<Block>(blocks.Count);
diff --git a/Source/VCGeneration/VerificationConditionGenerator.cs b/Source/VCGeneration/VerificationConditionGenerator.cs
index 8c41526b2..c0463d88f 100644
--- a/Source/VCGeneration/VerificationConditionGenerator.cs
+++ b/Source/VCGeneration/VerificationConditionGenerator.cs
@@ -31,7 +31,7 @@ record ImplementationTransformationData
 
   public class VerificationConditionGenerator : ConditionGeneration
   {
-    private static ConditionalWeakTable<Implementation, ImplementationTransformationData> implementationData = new();
+    private static readonly ConditionalWeakTable<Implementation, ImplementationTransformationData> implementationData = new();
 
 
     /// <summary>
@@ -474,7 +474,7 @@ public class ErrorReporter : ProverInterface.ErrorHandler
 
       ControlFlowIdMap<Absy> absyIds;
 
-      List<Block> blocks;
+      IList<Block> blocks;
 
       protected Dictionary<Cmd, List<object>> debugInfos;
 
@@ -505,7 +505,7 @@ public override void AddCoveredElement(TrackedNodeComponent elt)
 
       public ErrorReporter(VCGenOptions options,
         ControlFlowIdMap<Absy> /*!*/ absyIds,
-        List<Block /*!*/> /*!*/ blocks,
+        IList<Block /*!*/> /*!*/ blocks,
         Dictionary<Cmd, List<object>> debugInfos,
         VerifierCallback /*!*/ callback,
         ModelViewInfo mvInfo,
@@ -1479,7 +1479,7 @@ public static Counterexample AssertCmdToCloneCounterexample(VCGenOptions options
      *
      */
 
-    VCExpr LetVC(List<Block> blocks,
+    VCExpr LetVC(IList<Block> blocks,
       VCExpr controlFlowVariableExpr,
       ControlFlowIdMap<Absy> absyIds,
       ProverContext proverCtxt,
@@ -1622,7 +1622,7 @@ VCExpr DagVC(Block block,
     /// <summary>
     /// Remove empty blocks reachable from the startBlock of the CFG
     /// </summary>
-    static void RemoveEmptyBlocks(List<Block> blocks)
+    static void RemoveEmptyBlocks(IList<Block> blocks)
     {
       // postorder traversal of cfg
       //   noting loop heads in [keep] and