diff --git a/Source/Core/AST/AbsyCmd.cs b/Source/Core/AST/AbsyCmd.cs
index 3583e68b5..85d35413d 100644
--- a/Source/Core/AST/AbsyCmd.cs
+++ b/Source/Core/AST/AbsyCmd.cs
@@ -3539,6 +3539,11 @@ public GotoCmd(IToken /*!*/ tok, List<Block> /*!*/ blockSeq)
       this.labelTargets = blockSeq;
     }
 
+    public void RemoveTarget(Block b) {
+      labelNames.Remove(b.Label);
+      labelTargets.Remove(b);
+    }
+    
     public void AddTarget(Block b)
     {
       Contract.Requires(b != null);
diff --git a/Source/Core/AST/Program.cs b/Source/Core/AST/Program.cs
index 5684c315f..a347a4500 100644
--- a/Source/Core/AST/Program.cs
+++ b/Source/Core/AST/Program.cs
@@ -3,7 +3,6 @@
 using System.Collections.Generic;
 using System.Diagnostics.Contracts;
 using System.Linq;
-using System.Text;
 using Microsoft.Boogie.GraphUtil;
 
 namespace Microsoft.Boogie;
@@ -501,26 +500,30 @@ public static Graph<Implementation> BuildCallGraph(CoreOptions options, Program
 
   public static Graph<Block> GraphFromBlocks(List<Block> blocks, bool forward = true)
   {
-    Graph<Block> g = new Graph<Block>();
+    var result = new Graph<Block>();
+    if (!blocks.Any())
+    {
+      return result;
+    }
     void AddEdge(Block a, Block b) {
       Contract.Assert(a != null && b != null);
       if (forward) {
-        g.AddEdge(a, b);
+        result.AddEdge(a, b);
       } else {
-        g.AddEdge(b, a);
+        result.AddEdge(b, a);
       }
     }
 
-    g.AddSource(cce.NonNull(blocks[0])); // there is always at least one node in the graph
-    foreach (Block b in blocks)
+    result.AddSource(cce.NonNull(blocks[0])); // there is always at least one node in the graph
+    foreach (var block in blocks)
     {
-      if (b.TransferCmd is GotoCmd gtc)
+      if (block.TransferCmd is GotoCmd gtc)
       {
         Contract.Assume(gtc.labelTargets != null);
-        gtc.labelTargets.ForEach(dest => AddEdge(b, dest));
+        gtc.labelTargets.ForEach(dest => AddEdge(block, dest));
       }
     }
-    return g;
+    return result;
   }
 
   public static Graph<Block /*!*/> /*!*/ GraphFromImpl(Implementation impl, bool forward = true)
diff --git a/Source/Core/Analysis/BlockCoalescer.cs b/Source/Core/Analysis/BlockCoalescer.cs
index 959ff9275..f1065f65b 100644
--- a/Source/Core/Analysis/BlockCoalescer.cs
+++ b/Source/Core/Analysis/BlockCoalescer.cs
@@ -1,5 +1,8 @@
+#nullable enable
+
 using System.Collections.Generic;
 using System.Diagnostics.Contracts;
+using System.Linq;
 
 namespace Microsoft.Boogie;
 
@@ -7,159 +10,152 @@ public class BlockCoalescer : ReadOnlyVisitor
 {
   public static void CoalesceBlocks(Program program)
   {
-    Contract.Requires(program != null);
-    BlockCoalescer blockCoalescer = new BlockCoalescer();
+    var blockCoalescer = new BlockCoalescer();
     blockCoalescer.Visit(program);
   }
 
-  private static HashSet<Block /*!*/> /*!*/ ComputeMultiPredecessorBlocks(Implementation /*!*/ impl)
+  private static HashSet<Block> ComputeMultiPredecessorBlocks(Block rootBlock)
   {
-    Contract.Requires(impl != null);
     Contract.Ensures(cce.NonNullElements(Contract.Result<HashSet<Block>>()));
-    HashSet<Block /*!*/> visitedBlocks = new HashSet<Block /*!*/>();
-    HashSet<Block /*!*/> multiPredBlocks = new HashSet<Block /*!*/>();
-    Stack<Block /*!*/> dfsStack = new Stack<Block /*!*/>();
-    dfsStack.Push(impl.Blocks[0]);
+    var visitedBlocks = new HashSet<Block /*!*/>();
+    var result = new HashSet<Block>();
+    var dfsStack = new Stack<Block>();
+    dfsStack.Push(rootBlock);
     while (dfsStack.Count > 0)
     {
-      Block /*!*/
-        b = dfsStack.Pop();
-      Contract.Assert(b != null);
-      if (visitedBlocks.Contains(b))
+      var /*!*/ block = dfsStack.Pop();
+      Contract.Assert(block != null);
+      if (!visitedBlocks.Add(block))
       {
-        multiPredBlocks.Add(b);
+        result.Add(block);
         continue;
       }
 
-      visitedBlocks.Add(b);
-      if (b.TransferCmd == null)
+      if (block.TransferCmd == null)
       {
         continue;
       }
 
-      if (b.TransferCmd is ReturnCmd)
+      if (block.TransferCmd is ReturnCmd)
       {
         continue;
       }
 
-      Contract.Assert(b.TransferCmd is GotoCmd);
-      GotoCmd gotoCmd = (GotoCmd) b.TransferCmd;
+      Contract.Assert(block.TransferCmd is GotoCmd);
+      var gotoCmd = (GotoCmd) block.TransferCmd;
       if (gotoCmd.labelTargets == null)
       {
         continue;
       }
 
-      foreach (Block /*!*/ succ in gotoCmd.labelTargets)
+      foreach (var /*!*/ succ in gotoCmd.labelTargets)
       {
         Contract.Assert(succ != null);
         dfsStack.Push(succ);
       }
     }
 
-    return multiPredBlocks;
+    return result;
   }
 
   public override Implementation VisitImplementation(Implementation impl)
   {
-    //Contract.Requires(impl != null);
-    Contract.Ensures(Contract.Result<Implementation>() != null);
-    //Console.WriteLine("Procedure {0}", impl.Name);
-    //Console.WriteLine("Initial number of blocks = {0}", impl.Blocks.Count);
-
-    HashSet<Block /*!*/> multiPredBlocks = ComputeMultiPredecessorBlocks(impl);
-    Contract.Assert(cce.NonNullElements(multiPredBlocks));
-    HashSet<Block /*!*/> visitedBlocks = new HashSet<Block /*!*/>();
-    HashSet<Block /*!*/> removedBlocks = new HashSet<Block /*!*/>();
-    Stack<Block /*!*/> dfsStack = new Stack<Block /*!*/>();
-    dfsStack.Push(impl.Blocks[0]);
-    while (dfsStack.Count > 0)
+    var newBlocks = CoalesceFromRootBlock(impl.Blocks);
+    impl.Blocks = newBlocks;
+    foreach (var block in impl.Blocks)
     {
-      Block /*!*/
-        b = dfsStack.Pop();
-      Contract.Assert(b != null);
-      if (visitedBlocks.Contains(b))
+      if (block.TransferCmd is ReturnCmd)
       {
         continue;
       }
 
-      visitedBlocks.Add(b);
-      if (b.TransferCmd == null)
+      var gotoCmd = (GotoCmd)block.TransferCmd;
+      gotoCmd.labelNames = new List<string>();
+      foreach (var successor in gotoCmd.labelTargets)
+      {
+        gotoCmd.labelNames.Add(successor.Label);
+      }
+    }
+    return impl;
+  }
+
+  public static List<Block> CoalesceFromRootBlock(List<Block> blocks)
+  {
+    if (!blocks.Any())
+    {
+      return blocks;
+    }
+    var multiPredecessorBlocks = ComputeMultiPredecessorBlocks(blocks[0]);
+    Contract.Assert(cce.NonNullElements(multiPredecessorBlocks));
+    var visitedBlocks = new HashSet<Block>();
+    var removedBlocks = new HashSet<Block>();
+    var toVisit = new Stack<Block>();
+    toVisit.Push(blocks[0]);
+    while (toVisit.Count > 0)
+    {
+      var block = toVisit.Pop();
+      Contract.Assert(block != null);
+      if (!visitedBlocks.Add(block))
       {
         continue;
       }
 
-      if (b.TransferCmd is ReturnCmd)
+      if (block.TransferCmd == null)
       {
         continue;
       }
 
-      Contract.Assert(b.TransferCmd is GotoCmd);
-      GotoCmd gotoCmd = (GotoCmd) b.TransferCmd;
+      if (block.TransferCmd is ReturnCmd)
+      {
+        continue;
+      }
+
+      Contract.Assert(block.TransferCmd is GotoCmd);
+      var gotoCmd = (GotoCmd) block.TransferCmd;
       if (gotoCmd.labelTargets == null)
       {
         continue;
       }
 
-      if (gotoCmd.labelTargets.Count == 1)
+      if (gotoCmd.labelTargets.Count != 1)
       {
-        Block /*!*/
-          succ = cce.NonNull(gotoCmd.labelTargets[0]);
-        if (!multiPredBlocks.Contains(succ))
+        foreach (var aSuccessor in gotoCmd.labelTargets)
         {
-          foreach (Cmd /*!*/ cmd in succ.Cmds)
-          {
-            Contract.Assert(cmd != null);
-            b.Cmds.Add(cmd);
-          }
-
-          b.TransferCmd = succ.TransferCmd;
-          if (!b.tok.IsValid && succ.tok.IsValid)
-          {
-            b.tok = succ.tok;
-            b.Label = succ.Label;
-          }
-
-          removedBlocks.Add(succ);
-          dfsStack.Push(b);
-          visitedBlocks.Remove(b);
-          continue;
+          Contract.Assert(aSuccessor != null);
+          toVisit.Push(aSuccessor);
         }
+        continue;
       }
 
-      foreach (Block /*!*/ succ in gotoCmd.labelTargets)
+      var successor = cce.NonNull(gotoCmd.labelTargets[0]);
+      if (multiPredecessorBlocks.Contains(successor))
       {
-        Contract.Assert(succ != null);
-        dfsStack.Push(succ);
+        toVisit.Push(successor);
+        continue;
       }
-    }
 
-    List<Block /*!*/> newBlocks = new List<Block /*!*/>();
-    foreach (Block /*!*/ b in impl.Blocks)
-    {
-      Contract.Assert(b != null);
-      if (visitedBlocks.Contains(b) && !removedBlocks.Contains(b))
+      block.Cmds.AddRange(successor.Cmds);
+      block.TransferCmd = successor.TransferCmd;
+      if (!block.tok.IsValid && successor.tok.IsValid)
       {
-        newBlocks.Add(b);
+        block.tok = successor.tok;
+        block.Label = successor.Label;
       }
+
+      removedBlocks.Add(successor);
+      toVisit.Push(block);
+      visitedBlocks.Remove(block);
     }
 
-    impl.Blocks = newBlocks;
-    foreach (Block b in impl.Blocks)
+    var newBlocks = new List<Block>();
+    foreach (var block in blocks)
     {
-      if (b.TransferCmd is ReturnCmd)
-      {
-        continue;
-      }
-
-      GotoCmd gotoCmd = b.TransferCmd as GotoCmd;
-      gotoCmd.labelNames = new List<string>();
-      foreach (Block succ in gotoCmd.labelTargets)
+      Contract.Assert(block != null);
+      if (visitedBlocks.Contains(block) && !removedBlocks.Contains(block))
       {
-        gotoCmd.labelNames.Add(succ.Label);
+        newBlocks.Add(block);
       }
     }
-
-    // Console.WriteLine("Final number of blocks = {0}", impl.Blocks.Count);
-    return impl;
+    return newBlocks;
   }
 }
\ No newline at end of file
diff --git a/Source/Core/Analysis/LiveVariableAnalysis/GenKillWeight.cs b/Source/Core/Analysis/LiveVariableAnalysis/GenKillWeight.cs
index bd4366c01..60d2578d3 100644
--- a/Source/Core/Analysis/LiveVariableAnalysis/GenKillWeight.cs
+++ b/Source/Core/Analysis/LiveVariableAnalysis/GenKillWeight.cs
@@ -1,4 +1,4 @@
-using System.Collections.Generic;
+using System.Collections.Generic;
 using System.Diagnostics.Contracts;
 
 namespace Microsoft.Boogie;
diff --git a/Source/Core/Analysis/LiveVariableAnalysis/InterProcGenKill.cs b/Source/Core/Analysis/LiveVariableAnalysis/InterProcGenKill.cs
index 615bc384b..147221dd9 100644
--- a/Source/Core/Analysis/LiveVariableAnalysis/InterProcGenKill.cs
+++ b/Source/Core/Analysis/LiveVariableAnalysis/InterProcGenKill.cs
@@ -4,7 +4,6 @@
 
 namespace Microsoft.Boogie
 {
-  // Interprocedural Gen/Kill Analysis
   public class InterProcGenKill
   {
     private CoreOptions options;
@@ -554,19 +553,6 @@ public void Compute()
         varsLiveAtEntry.Add(cfg.impl.Name, lv);
         varsLiveSummary.Add(cfg.impl.Name, cfg.summary);
       }
-
-      /*
-      foreach(Block/*!*/
-      /* b in mainImpl.Blocks){
-Contract.Assert(b != null);
-//Set<Variable!> lv = cfg.weightBefore[b].getLiveVars();
-b.liveVarsBefore = procICFG[mainImpl.Name].liveVarsAfter[b];
-//foreach(GlobalVariable/*!*/
-      /* v in program.GlobalVariables){Contract.Assert(v != null);
-//  b.liveVarsBefore.Add(v);
-//}
-}
-*/
     }
 
     // Called when summaries have already been computed
diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
index 576020815..23e42ec75 100644
--- a/Source/ExecutionEngine/ExecutionEngine.cs
+++ b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -224,7 +224,7 @@ public void CoalesceBlocks(Program program)
           Options.OutputWriter.WriteLine("Coalescing blocks...");
         }
 
-        Microsoft.Boogie.BlockCoalescer.CoalesceBlocks(program);
+        BlockCoalescer.CoalesceBlocks(program);
       }
     }
 
@@ -240,7 +240,7 @@ public void CollectModSets(Program program)
 
     public void EliminateDeadVariables(Program program)
     {
-      Microsoft.Boogie.UnusedVarEliminator.Eliminate(program);
+      UnusedVarEliminator.Eliminate(program);
     }
     
     public void PrintBplFile(string filename, Program program, 
@@ -737,6 +737,7 @@ public async Task<IReadOnlyList<IVerificationTask>> GetVerificationTasks(Program
         var writer = TextWriter.Null;
         var vcGenerator = new VerificationConditionGenerator(processedProgram.Program, CheckerPool);
 
+        
         var run = new ImplementationRun(implementation, writer);
         var collector = new VerificationResultCollector(Options);
         vcGenerator.PrepareImplementation(run, collector, out _,
@@ -744,7 +745,7 @@ public async Task<IReadOnlyList<IVerificationTask>> GetVerificationTasks(Program
           out var modelViewInfo);
 
         ConditionGeneration.ResetPredecessors(run.Implementation.Blocks);
-        var splits = ManualSplitFinder.FocusAndSplit(Options, run, gotoCmdOrigins, vcGenerator).ToList();
+        var splits = ManualSplitFinder.FocusAndSplit(program, Options, run, gotoCmdOrigins, vcGenerator).ToList();
         for (var index = 0; index < splits.Count; index++) {
           var split = splits[index];
           split.SplitIndex = index;
diff --git a/Source/ExecutionEngine/VerificationTask.cs b/Source/ExecutionEngine/VerificationTask.cs
index 8ef2793a7..deeb66b54 100644
--- a/Source/ExecutionEngine/VerificationTask.cs
+++ b/Source/ExecutionEngine/VerificationTask.cs
@@ -44,7 +44,7 @@ public VerificationTask(ExecutionEngine engine, ProcessedProgram processedProgra
 
   public IVerificationTask FromSeed(int newSeed)
   {
-    var split = new ManualSplit(Split.Options, Split.Blocks, Split.GotoCmdOrigins, 
+    var split = new ManualSplit(Split.Options, () => Split.Blocks, Split.GotoCmdOrigins, 
       Split.parent, Split.Run, Split.Token, newSeed);
     split.SplitIndex = Split.SplitIndex;
     return new VerificationTask(engine, ProcessedProgram, split, modelViewInfo);
diff --git a/Source/UnitTests/ExecutionEngineTests/ExecutionEngineTest.cs b/Source/UnitTests/ExecutionEngineTests/ExecutionEngineTest.cs
index be504fd0b..6c39f1ec0 100644
--- a/Source/UnitTests/ExecutionEngineTests/ExecutionEngineTest.cs
+++ b/Source/UnitTests/ExecutionEngineTests/ExecutionEngineTest.cs
@@ -99,9 +99,9 @@ procedure Procedure(y: int)
     var tasks = await engine.GetVerificationTasks(program);
     
     // The first split is empty. Maybe it can be optimized away
-    Assert.AreEqual(5, tasks.Count);
+    Assert.AreEqual(4, tasks.Count);
 
-    var outcomes = new List<SolverOutcome> { SolverOutcome.Valid, SolverOutcome.Invalid, SolverOutcome.Valid, SolverOutcome.Invalid, SolverOutcome.Valid };
+    var outcomes = new List<SolverOutcome> { SolverOutcome.Invalid, SolverOutcome.Valid, SolverOutcome.Invalid, SolverOutcome.Valid };
     for (var index = 0; index < outcomes.Count; index++)
     {
       var result0 = await tasks[index].TryRun()!.ToTask();
diff --git a/Source/VCGeneration/BlockTransformations.cs b/Source/VCGeneration/BlockTransformations.cs
index 9e9606ecf..b6472e319 100644
--- a/Source/VCGeneration/BlockTransformations.cs
+++ b/Source/VCGeneration/BlockTransformations.cs
@@ -1,16 +1,56 @@
+using System;
+using System.Collections;
 using System.Collections.Generic;
-using System.Diagnostics.Contracts;
+using System.Collections.Immutable;
 using System.Linq;
+using System.Reactive;
 using Microsoft.Boogie;
+using Microsoft.Boogie.GraphUtil;
+using VCGeneration.Prune;
 
 namespace VCGeneration;
 
-public static class BlockTransformations
-{
-  public static List<Block> DeleteNoAssertionBlocks(List<Block> blocks)
+public static class BlockTransformations {
+  
+  public static void Optimize(List<Block> blocks) {
+    foreach (var block in blocks)
+    {
+      // make blocks ending in assume false leaves of the CFG-DAG
+      StopControlFlowAtAssumeFalse(block); 
+    }
+
+    DeleteBlocksNotLeadingToAssertions(blocks);
+    DeleteUselessBlocks(blocks);
+
+    var coalesced = BlockCoalescer.CoalesceFromRootBlock(blocks);
+    blocks.Clear();
+    blocks.AddRange(coalesced);
+  }
+
+  private static void StopControlFlowAtAssumeFalse(Block block)
   {
+    var firstFalseIdx = block.Cmds.FindIndex(IsAssumeFalse);
+    if (firstFalseIdx == -1)
+    {
+      return;
+    }
 
-    blocks.ForEach(StopControlFlowAtAssumeFalse); // make blocks ending in assume false leaves of the CFG-DAG -- this is probably unnecessary, may have been done previously
+    block.Cmds = block.Cmds.Take(firstFalseIdx + 1).ToList();
+    if (block.TransferCmd is not GotoCmd gotoCmd)
+    {
+      return;
+    }
+
+    block.TransferCmd = new ReturnCmd(block.tok);
+    foreach (var target in gotoCmd.labelTargets) {
+      target.Predecessors.Remove(block);
+    }
+  }
+  
+  private static bool IsAssumeFalse (Cmd c) { return c is AssumeCmd { Expr: LiteralExpr { asBool: false } }; }
+
+  public static void DeleteBlocksNotLeadingToAssertions(List<Block> blocks)
+  {
     var todo = new Stack<Block>();
     var peeked = new HashSet<Block>();
     var interestingBlocks = new HashSet<Block>();
@@ -28,10 +68,9 @@ public static List<Block> DeleteNoAssertionBlocks(List<Block> blocks)
       if (currentBlock.TransferCmd is GotoCmd exit) {
         if (pop)
         {
-          Contract.Assert(pop);
           var gtc = new GotoCmd(exit.tok, exit.labelTargets.Where(l => interestingBlocks.Contains(l)).ToList());
           currentBlock.TransferCmd = gtc;
-          interesting = interesting || gtc.labelTargets.Count != 0;
+          interesting = gtc.labelTargets.Count != 0;
         }
         else
         {
@@ -48,26 +87,73 @@ public static List<Block> DeleteNoAssertionBlocks(List<Block> blocks)
       }
     }
     interestingBlocks.Add(blocks[0]); // must not be empty
-    return blocks.Where(b => interestingBlocks.Contains(b)).ToList(); // this is not the same as interestingBlocks.ToList() because the resulting lists will have different orders.
+    var result = blocks.Where(b => interestingBlocks.Contains(b)).ToList(); // this is not the same as interestingBlocks.ToList() because the resulting lists will have different orders.
+    blocks.Clear();
+    blocks.AddRange(result);
   }
 
   private static bool ContainsAssert(Block b)
   {
-    bool IsNonTrivialAssert (Cmd c) { return c is AssertCmd ac && !(ac.Expr is LiteralExpr le && le.asBool); }
     return b.Cmds.Exists(IsNonTrivialAssert);
   }
+  
+  public static bool IsNonTrivialAssert (Cmd c) { return c is AssertCmd ac && !(ac.Expr is LiteralExpr { asBool: true }); }
 
-  private static void StopControlFlowAtAssumeFalse(Block b)
-  {
-    var firstFalseIdx = b.Cmds.FindIndex(IsAssumeFalse);
-    if (firstFalseIdx == -1)
-    {
-      return;
+  private static void DeleteUselessBlocks(List<Block> blocks) {
+    var toVisit = new HashSet<Block>();
+    var removed = new HashSet<Block>();
+    foreach (var block in blocks) {
+      toVisit.Add(block);
     }
+    while(toVisit.Count > 0) {
+      var block = toVisit.First();
+      toVisit.Remove(block);
+      if (removed.Contains(block)) {
+        continue;
+      }
+      if (block.Cmds.Any()) {
+        continue;
+      }
+
+      var isBranchingBlock = block.TransferCmd is GotoCmd gotoCmd1 && gotoCmd1.labelTargets.Count > 1 && 
+                             block.Predecessors.Count != 1;
+      if (isBranchingBlock) {
+        continue;
+      }
+
+      removed.Add(block);
+      blocks.Remove(block);
+
+      var noPredecessors = !block.Predecessors.Any();
+      var noSuccessors = block.TransferCmd is not GotoCmd outGoto2 || !outGoto2.labelTargets.Any();
+      foreach (var predecessor in block.Predecessors) {
+        var intoCmd = (GotoCmd)predecessor.TransferCmd;
+        intoCmd.RemoveTarget(block);
+        if (noSuccessors) {
+          toVisit.Add(predecessor);
+        }
+      }
+
+      if (block.TransferCmd is not GotoCmd outGoto) {
+        continue;
+      }
+
+      foreach (var outBlock in outGoto.labelTargets) {
+        outBlock.Predecessors.Remove(block);
+        if (noPredecessors) {
+          toVisit.Add(outBlock);
+        }
+      }
 
-    b.Cmds = b.Cmds.Take(firstFalseIdx + 1).ToList();
-    b.TransferCmd = b.TransferCmd is GotoCmd ? new ReturnCmd(b.tok) : b.TransferCmd;
+      foreach (var predecessor in block.Predecessors) {
+        var intoCmd = (GotoCmd)predecessor.TransferCmd;
+        foreach (var outBlock in outGoto.labelTargets) {
+          if (!intoCmd.labelTargets.Contains(outBlock)) {
+            intoCmd.AddTarget(outBlock);
+            outBlock.Predecessors.Add(predecessor);
+          }
+        }
+      }
+    }
   }
-  
-  private static bool IsAssumeFalse (Cmd c) { return c is AssumeCmd { Expr: LiteralExpr { asBool: false } }; }
 }
\ No newline at end of file
diff --git a/Source/VCGeneration/FocusAttribute.cs b/Source/VCGeneration/FocusAttribute.cs
index ebaeedf60..da5bac811 100644
--- a/Source/VCGeneration/FocusAttribute.cs
+++ b/Source/VCGeneration/FocusAttribute.cs
@@ -28,7 +28,7 @@ public static List<ManualSplit> FocusImpl(VCGenOptions options, ImplementationRu
       focusBlocks.Reverse();
     }
     if (!focusBlocks.Any()) {
-      return new List<ManualSplit> { new(options, impl.Blocks, gotoCmdOrigins, par, run, run.Implementation.tok) };
+      return new List<ManualSplit> { new(options, () => impl.Blocks, gotoCmdOrigins, par, run, run.Implementation.tok) };
     }
 
     var ancestorsPerBlock = new Dictionary<Block, HashSet<Block>>();
@@ -71,7 +71,11 @@ void FocusRec(IToken focusToken, int focusIndex, IReadOnlyList<Block> blocksToIn
         }
         newBlocks.Reverse();
         Contract.Assert(newBlocks[0] == oldToNewBlockMap[impl.Blocks[0]]);
-        result.Add(new ManualSplit(options, BlockTransformations.DeleteNoAssertionBlocks(newBlocks), gotoCmdOrigins, par, run, focusToken));
+        result.Add(new ManualSplit(options, () =>
+        {
+          BlockTransformations.DeleteBlocksNotLeadingToAssertions(newBlocks);
+          return newBlocks;
+        }, gotoCmdOrigins, par, run, focusToken));
       }
       else if (!blocksToInclude.Contains(focusBlocks[focusIndex].Block) || freeAssumeBlocks.Contains(focusBlocks[focusIndex].Block))
       {
diff --git a/Source/VCGeneration/ManualSplit.cs b/Source/VCGeneration/ManualSplit.cs
index daa7c6bdc..09927d3c1 100644
--- a/Source/VCGeneration/ManualSplit.cs
+++ b/Source/VCGeneration/ManualSplit.cs
@@ -8,10 +8,9 @@ public class ManualSplit : Split
 {
 
   public IToken Token { get; }
-
-
+  
   public ManualSplit(VCGenOptions options, 
-    List<Block> blocks, 
+    Func<List<Block>> blocks, 
     Dictionary<TransferCmd, ReturnCmd> gotoCmdOrigins, 
     VerificationConditionGenerator par, 
     ImplementationRun run, 
diff --git a/Source/VCGeneration/ManualSplitFinder.cs b/Source/VCGeneration/ManualSplitFinder.cs
index 41bd02472..5fe10f268 100644
--- a/Source/VCGeneration/ManualSplitFinder.cs
+++ b/Source/VCGeneration/ManualSplitFinder.cs
@@ -1,3 +1,4 @@
+#nullable enable
 using System.Collections.Generic;
 using System.Diagnostics.Contracts;
 using System.Linq;
@@ -7,12 +8,13 @@
 namespace VCGeneration;
 
 public static class ManualSplitFinder {
-  public static IEnumerable<ManualSplit> FocusAndSplit(VCGenOptions options, ImplementationRun run, Dictionary<TransferCmd, ReturnCmd> gotoCmdOrigins, VerificationConditionGenerator par) {
+  public static IEnumerable<ManualSplit> FocusAndSplit(Program program, VCGenOptions options, ImplementationRun run, 
+    Dictionary<TransferCmd, ReturnCmd> gotoCmdOrigins, VerificationConditionGenerator par) {
     var focussedImpl = FocusAttribute.FocusImpl(options, run, gotoCmdOrigins, par);
-    return focussedImpl.SelectMany(FindManualSplits);
+    return focussedImpl.SelectMany(s => FindManualSplits(program, s));
   }
 
-  private static List<ManualSplit /*!*/> FindManualSplits(ManualSplit initialSplit) {
+  private static List<ManualSplit /*!*/> FindManualSplits(Program program, ManualSplit initialSplit) {
     Contract.Requires(initialSplit.Implementation != null);
     Contract.Ensures(Contract.Result<List<Split>>() == null || cce.NonNullElements(Contract.Result<List<Split>>()));
 
@@ -34,10 +36,15 @@ public static IEnumerable<ManualSplit> FocusAndSplit(VCGenOptions options, Imple
       Block entryPoint = initialSplit.Blocks[0];
       var blockAssignments = PickBlocksToVerify(initialSplit.Blocks, splitPoints);
       var entryBlockHasSplit = splitPoints.ContainsKey(entryPoint);
-      var baseSplitBlocks = BlockTransformations.DeleteNoAssertionBlocks(
-        DoPreAssignedManualSplit(initialSplit.Options, initialSplit.Blocks, blockAssignments,
-          -1, entryPoint, !entryBlockHasSplit, splitOnEveryAssert));
-      splits.Add(new ManualSplit(initialSplit.Options, baseSplitBlocks, initialSplit.GotoCmdOrigins, initialSplit.parent, initialSplit.Run, initialSplit.Token));
+      var firstSplitBlocks = DoPreAssignedManualSplit(initialSplit.Options, initialSplit.Blocks, blockAssignments,
+        -1, entryPoint, !entryBlockHasSplit, splitOnEveryAssert);
+      if (firstSplitBlocks != null)
+      {
+        splits.Add(new ManualSplit(initialSplit.Options, () => {
+          BlockTransformations.Optimize(firstSplitBlocks);
+          return firstSplitBlocks;
+        }, initialSplit.GotoCmdOrigins, initialSplit.parent, initialSplit.Run, initialSplit.Token));
+      }
       foreach (var block in initialSplit.Blocks) {
         var tokens = splitPoints.GetValueOrDefault(block);
         if (tokens == null) {
@@ -48,8 +55,14 @@ public static IEnumerable<ManualSplit> FocusAndSplit(VCGenOptions options, Imple
           var token = tokens[i];
           bool lastSplitInBlock = i == tokens.Count - 1;
           var newBlocks = DoPreAssignedManualSplit(initialSplit.Options, initialSplit.Blocks, blockAssignments, i, block, lastSplitInBlock, splitOnEveryAssert);
-          splits.Add(new ManualSplit(initialSplit.Options, 
-            BlockTransformations.DeleteNoAssertionBlocks(newBlocks), initialSplit.GotoCmdOrigins, initialSplit.parent, initialSplit.Run, token));
+          if (newBlocks != null)
+          {
+            splits.Add(new ManualSplit(initialSplit.Options, 
+              () => {
+                BlockTransformations.Optimize(newBlocks);
+                return newBlocks;
+              }, initialSplit.GotoCmdOrigins, initialSplit.parent, initialSplit.Run, token));
+          }
         }
       }
     }
@@ -90,10 +103,29 @@ private static Dictionary<Block, Block> PickBlocksToVerify(List<Block> blocks, D
     return blockAssignments;
   }
 
-  private static List<Block> DoPreAssignedManualSplit(VCGenOptions options, List<Block> blocks, Dictionary<Block, Block> blockAssignments, int splitNumberWithinBlock,
+  private static List<Block> SplitOnAssert(VCGenOptions options, List<Block> oldBlocks, AssertCmd assertToKeep) {
+    var oldToNewBlockMap = new Dictionary<Block, Block>(oldBlocks.Count);
+    
+    var newBlocks = new List<Block>(oldBlocks.Count);
+    foreach (var oldBlock in oldBlocks) {
+      var newBlock = new Block(oldBlock.tok) {
+        Label = oldBlock.Label,
+        Cmds = oldBlock.Cmds.Select(cmd => 
+          cmd != assertToKeep ? CommandTransformations.AssertIntoAssume(options, cmd) : cmd).ToList()
+      };
+      oldToNewBlockMap[oldBlock] = newBlock;
+      newBlocks.Add(newBlock);
+    }
+
+    AddBlockJumps(oldBlocks, oldToNewBlockMap);
+    return newBlocks;
+  }
+  private static List<Block>? DoPreAssignedManualSplit(VCGenOptions options, List<Block> blocks, 
+    Dictionary<Block, Block> blockAssignments, int splitNumberWithinBlock,
     Block containingBlock, bool lastSplitInBlock, bool splitOnEveryAssert) {
     var newBlocks = new List<Block>(blocks.Count); // Copies of the original blocks
     //var duplicator = new Duplicator();
+    var assertionCount = 0;
     var oldToNewBlockMap = new Dictionary<Block, Block>(blocks.Count); // Maps original blocks to their new copies in newBlocks
     foreach (var currentBlock in blocks) {
       var newBlock = new Block(currentBlock.tok)
@@ -112,14 +144,23 @@ private static List<Block> DoPreAssignedManualSplit(VCGenOptions options, List<B
             splitCount++;
             verify = splitCount == splitNumberWithinBlock;
           }
+
+          if (verify && BlockTransformations.IsNonTrivialAssert(command))
+          {
+            assertionCount++;
+          }
           newCmds.Add(verify ? command : CommandTransformations.AssertIntoAssume(options, command));
         }
         newBlock.Cmds = newCmds;
       } else if (lastSplitInBlock && blockAssignments[currentBlock] == containingBlock) {
         var verify = true;
         var newCmds = new List<Cmd>();
-        foreach (Cmd command in currentBlock.Cmds) {
+        foreach (var command in currentBlock.Cmds) {
           verify = !ShouldSplitHere(command, splitOnEveryAssert) && verify;
+          if (verify && BlockTransformations.IsNonTrivialAssert(command))
+          {
+            assertionCount++;
+          }
           newCmds.Add(verify ? command : CommandTransformations.AssertIntoAssume(options, command));
         }
         newBlock.Cmds = newCmds;
@@ -127,9 +168,23 @@ private static List<Block> DoPreAssignedManualSplit(VCGenOptions options, List<B
         newBlock.Cmds = currentBlock.Cmds.Select(x => CommandTransformations.AssertIntoAssume(options, x)).ToList();
       }
     }
+
+    if (assertionCount == 0)
+    {
+      return null;
+    }
+    
     // Patch the edges between the new blocks
-    foreach (var oldBlock in blocks) {
-      if (oldBlock.TransferCmd is ReturnCmd) {
+    AddBlockJumps(blocks, oldToNewBlockMap);
+    return newBlocks;
+  }
+
+  private static void AddBlockJumps(List<Block> oldBlocks, Dictionary<Block, Block> oldToNewBlockMap)
+  {
+    foreach (var oldBlock in oldBlocks) {
+      var newBlock = oldToNewBlockMap[oldBlock];
+      if (oldBlock.TransferCmd is ReturnCmd returnCmd) {
+        ((ReturnCmd)newBlock.TransferCmd).tok = returnCmd.tok;
         continue;
       }
 
@@ -143,6 +198,5 @@ private static List<Block> DoPreAssignedManualSplit(VCGenOptions options, List<B
 
       oldToNewBlockMap[oldBlock].TransferCmd = new GotoCmd(gotoCmd.tok, newLabelNames, newLabelTargets);
     }
-    return newBlocks;
   }
 }
\ No newline at end of file
diff --git a/Source/VCGeneration/Split.cs b/Source/VCGeneration/Split.cs
index 4012a6bdd..7cf747118 100644
--- a/Source/VCGeneration/Split.cs
+++ b/Source/VCGeneration/Split.cs
@@ -1,6 +1,5 @@
 using System;
 using System.Collections.Generic;
-using System.ComponentModel;
 using System.Diagnostics;
 using System.Linq;
 using System.Threading;
@@ -11,7 +10,6 @@
 using Microsoft.Boogie.VCExprAST;
 using Microsoft.Boogie.SMTLib;
 using System.Threading.Tasks;
-using VCGeneration;
 
 namespace VC
 {
@@ -23,10 +21,11 @@ public class Split : ProofRun
 
       public int RandomSeed { get; }
 
-      public List<Block> Blocks { get; set; }
+      private List<Block> blocks;
+      public List<Block> Blocks => blocks ??= getBlocks();
+
       readonly List<Block> bigBlocks = new();
       public List<AssertCmd> Asserts => Blocks.SelectMany(block => block.cmds.OfType<AssertCmd>()).ToList();
-      public readonly IReadOnlyList<Declaration> TopLevelDeclarations;
       public IReadOnlyList<Declaration> prunedDeclarations;
       
       public IReadOnlyList<Declaration> PrunedDeclarations {
@@ -63,43 +62,36 @@ public readonly VerificationConditionGenerator /*!*/
 
       public Implementation /*!*/ Implementation => Run.Implementation;
 
-      Dictionary<Block /*!*/, Block /*!*/> /*!*/
-        copies = new Dictionary<Block /*!*/, Block /*!*/>();
+      Dictionary<Block /*!*/, Block /*!*/> /*!*/ copies = new();
 
       bool doingSlice;
       double sliceInitialLimit;
       double sliceLimit;
       bool slicePos;
-
-      HashSet<Block /*!*/> /*!*/ protectedFromAssertToAssume = new HashSet<Block /*!*/>();
-
-      HashSet<Block /*!*/> /*!*/ keepAtAll = new HashSet<Block /*!*/>();
+      HashSet<Block /*!*/> /*!*/ protectedFromAssertToAssume = new();
+      HashSet<Block /*!*/> /*!*/ keepAtAll = new();
 
       // async interface
       public int SplitIndex { get; set; }
       public VerificationConditionGenerator.ErrorReporter reporter;
 
-      public Split(VCGenOptions options, List<Block /*!*/> /*!*/ blocks,
+      public Split(VCGenOptions options, Func<List<Block /*!*/>> /*!*/ getBlocks,
         Dictionary<TransferCmd, ReturnCmd> /*!*/ gotoCmdOrigins,
         VerificationConditionGenerator /*!*/ par, ImplementationRun run, int? randomSeed = null)
       {
-        Contract.Requires(cce.NonNullElements(blocks));
         Contract.Requires(gotoCmdOrigins != null);
         Contract.Requires(par != null);
-        this.Blocks = blocks;
+        this.getBlocks = getBlocks;
         this.GotoCmdOrigins = gotoCmdOrigins;
         parent = par;
         this.Run = run;
         this.Options = options;
         Interlocked.Increment(ref currentId);
 
-        TopLevelDeclarations = par.program.TopLevelDeclarations;
         RandomSeed = randomSeed ?? Implementation.RandomSeed ?? Options.RandomSeed ?? 0;
         randomGen = new Random(RandomSeed);
       }
       
-      
-
       public void PrintSplit() {
         if (Options.PrintSplitFile == null) {
           return;
@@ -196,21 +188,13 @@ public void DumpDot(int splitNum)
         string filename = string.Format("{0}.split.{1}.bpl", Implementation.Name, splitNum);
         using (StreamWriter sw = File.CreateText(filename))
         {
-          int oldPrintUnstructured = Options.PrintUnstructured;
-          Options.PrintUnstructured = 2; // print only the unstructured program
-          bool oldPrintDesugaringSetting = Options.PrintDesugarings;
-          Options.PrintDesugarings = false;
-          List<Block> backup = Implementation.Blocks;
-          Contract.Assert(backup != null);
-          Implementation.Blocks = Blocks;
-          Implementation.Emit(new TokenTextWriter(filename, sw, /*setTokens=*/ false, /*pretty=*/ false, Options), 0);
-          Implementation.Blocks = backup;
-          Options.PrintDesugarings = oldPrintDesugaringSetting;
-          Options.PrintUnstructured = oldPrintUnstructured;
+          var writer = new TokenTextWriter(filename, sw, /*setTokens=*/ false, /*pretty=*/ false, Options);
+          Implementation.Emit(writer, 0);
         }
       }
 
       int bsid;
+      private readonly Func<List<Block>> getBlocks;
 
       BlockStats GetBlockStats(Block b)
       {
@@ -697,7 +681,7 @@ private Split DoSplit()
           }
         }
 
-        return new Split(Options, newBlocks, newGotoCmdOrigins, parent, Run);
+        return new Split(Options, () => newBlocks, newGotoCmdOrigins, parent, Run);
       }
 
       private Split SplitAt(int idx)
diff --git a/Source/VCGeneration/SplitAndVerifyWorker.cs b/Source/VCGeneration/SplitAndVerifyWorker.cs
index 37fd641d4..a42723458 100644
--- a/Source/VCGeneration/SplitAndVerifyWorker.cs
+++ b/Source/VCGeneration/SplitAndVerifyWorker.cs
@@ -36,6 +36,7 @@ public class SplitAndVerifyWorker
     private int totalResourceCount;
 
     public SplitAndVerifyWorker(
+      Program program,
       VCGenOptions options, 
       VerificationConditionGenerator verificationConditionGenerator,
       ImplementationRun run,
@@ -65,7 +66,7 @@ public SplitAndVerifyWorker(
 
 
       ResetPredecessors(Implementation.Blocks);
-      ManualSplits = ManualSplitFinder.FocusAndSplit(options, run, gotoCmdOrigins, verificationConditionGenerator).ToList<Split>();
+      ManualSplits = ManualSplitFinder.FocusAndSplit(program, options, run, gotoCmdOrigins, verificationConditionGenerator).ToList<Split>();
 
       if (ManualSplits.Count == 1 && maxSplits > 1)
       {
diff --git a/Source/VCGeneration/VerificationConditionGenerator.cs b/Source/VCGeneration/VerificationConditionGenerator.cs
index bdff1b0f2..d9f14c4c7 100644
--- a/Source/VCGeneration/VerificationConditionGenerator.cs
+++ b/Source/VCGeneration/VerificationConditionGenerator.cs
@@ -407,7 +407,7 @@ public override async Task<VcOutcome> VerifyImplementation(ImplementationRun run
         }
       }
 
-      var worker = new SplitAndVerifyWorker(Options, this, run, dataGotoCmdOrigins, callback,
+      var worker = new SplitAndVerifyWorker(program, Options, this, run, dataGotoCmdOrigins, callback,
         dataModelViewInfo, vcOutcome);
 
       vcOutcome = await worker.WorkUntilDone(cancellationToken);
diff --git a/Test/civl/samples/treiber-stack.bpl b/Test/civl/samples/treiber-stack.bpl
index b9e426474..21340742e 100644
--- a/Test/civl/samples/treiber-stack.bpl
+++ b/Test/civl/samples/treiber-stack.bpl
@@ -1,4 +1,4 @@
-// RUN: %parallel-boogie -lib:base -lib:node -vcsSplitOnEveryAssert "%s" > "%t"
+// RUN: %parallel-boogie -lib:base -lib:node -timeLimit:0 -vcsSplitOnEveryAssert "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 datatype LocPiece { Left(), Right() }
diff --git a/Test/commandline/SplitOnEveryAssert.bpl b/Test/commandline/SplitOnEveryAssert.bpl
index 1751a4d99..2e3878802 100644
--- a/Test/commandline/SplitOnEveryAssert.bpl
+++ b/Test/commandline/SplitOnEveryAssert.bpl
@@ -3,20 +3,19 @@
 // RUN: %OutputCheck --file-to-check "%t" "%s"
 
 // CHECK: Verifying Ex ...
-// CHECK:      checking split 1/12 .*
-// CHECK:      checking split 2/12 .*
-// CHECK:      checking split 3/12 .*
-// CHECK:      checking split 4/12 .*
-// CHECK:      --> split #4 done,  \[.* s\] Invalid
-// CHECK:      checking split 5/12 .*
-// CHECK:      checking split 6/12 .*
-// CHECK:      checking split 7/12 .*
-// CHECK:      checking split 8/12 .*
-// CHECK:      checking split 9/12 .*
-// CHECK:      checking split 10/12 .*
-// CHECK:      checking split 11/12 .*
-// CHECK:      checking split 12/12 .*
-// CHECK-L: SplitOnEveryAssert.bpl(32,5): Error: this assertion could not be proved
+// CHECK:      checking split 1/11 .*
+// CHECK:      checking split 2/11 .*
+// CHECK:      checking split 3/11 .*
+// CHECK:      --> split #3 done,  \[.* s\] Invalid
+// CHECK:      checking split 4/11 .*
+// CHECK:      checking split 5/11 .*
+// CHECK:      checking split 6/11 .*
+// CHECK:      checking split 7/11 .*
+// CHECK:      checking split 8/11 .*
+// CHECK:      checking split 9/11 .*
+// CHECK:      checking split 10/11 .*
+// CHECK:      checking split 11/11 .*
+// CHECK-L: SplitOnEveryAssert.bpl(31,5): Error: this assertion could not be proved
 
 procedure Ex() returns (y: int)
   ensures y >= 0;
diff --git a/Test/test0/AssumeFalseSplit/Foo.split.0.bpl.expect b/Test/test0/AssumeFalseSplit/Foo.split.0.bpl.expect
index c03efb956..c8727ad27 100644
--- a/Test/test0/AssumeFalseSplit/Foo.split.0.bpl.expect
+++ b/Test/test0/AssumeFalseSplit/Foo.split.0.bpl.expect
@@ -1,9 +1,6 @@
 implementation Foo()
 {
 
-  anon0:
-    goto anon3_Then;
-
   anon3_Then:
     assert 2 == 1 + 1;
     assume false;
diff --git a/Test/test0/AssumeFalseSplit/Foo.split.1.bpl.expect b/Test/test0/AssumeFalseSplit/Foo.split.1.bpl.expect
index 84c8ec7ce..29ba05d16 100644
--- a/Test/test0/AssumeFalseSplit/Foo.split.1.bpl.expect
+++ b/Test/test0/AssumeFalseSplit/Foo.split.1.bpl.expect
@@ -1,9 +1,6 @@
 implementation Foo()
 {
 
-  anon0:
-    goto anon3_Else;
-
   anon3_Else:
     assume 2 == 1 + 1;
     assert {:split_here} 2 == 2;
diff --git a/Test/test0/AssumeFalseSplit/Foo.split.2.bpl.expect b/Test/test0/AssumeFalseSplit/Foo.split.2.bpl.expect
index 46590b6d5..838d5aebd 100644
--- a/Test/test0/AssumeFalseSplit/Foo.split.2.bpl.expect
+++ b/Test/test0/AssumeFalseSplit/Foo.split.2.bpl.expect
@@ -1,9 +1,6 @@
 implementation Foo()
 {
 
-  anon0:
-    goto anon3_Else;
-
   anon3_Else:
     assume 2 == 1 + 1;
     assume 2 == 2;
diff --git a/Test/test0/Split/Foo.split.0.bpl.expect b/Test/test0/Split/Foo.split.0.bpl.expect
index d00176cde..79578bccc 100644
--- a/Test/test0/Split/Foo.split.0.bpl.expect
+++ b/Test/test0/Split/Foo.split.0.bpl.expect
@@ -1,25 +1,13 @@
 implementation Foo() returns (y: int)
 {
 
-  PreconditionGeneratedEntry:
-    goto anon0;
-
   anon0:
     assert 5 + 0 == 5;
     assert 5 * 5 <= 25;
-    goto anon5_LoopHead;
-
-  anon5_LoopHead:
     assume x#AT#0 + y#AT#0 == 5;
     assume x#AT#0 * x#AT#0 <= 25;
-    goto anon5_LoopDone;
-
-  anon5_LoopDone:
     assume {:partition} 0 >= x#AT#0;
     assume y#AT#2 == y#AT#0;
-    goto GeneratedUnifiedExit;
-
-  GeneratedUnifiedExit:
     assert y#AT#2 >= 0;
     return;
 }
diff --git a/Test/test0/Split/Foo.split.1.bpl.expect b/Test/test0/Split/Foo.split.1.bpl.expect
index bc4ea17f5..37297e028 100644
--- a/Test/test0/Split/Foo.split.1.bpl.expect
+++ b/Test/test0/Split/Foo.split.1.bpl.expect
@@ -1,27 +1,15 @@
 implementation Foo() returns (y: int)
 {
 
-  PreconditionGeneratedEntry:
-    goto anon0;
-
   anon0:
     assume 5 + 0 == 5;
     assume 5 * 5 <= 25;
-    goto anon5_LoopHead;
-
-  anon5_LoopHead:
     assume x#AT#0 + y#AT#0 == 5;
     assume x#AT#0 * x#AT#0 <= 25;
-    goto anon5_LoopBody;
-
-  anon5_LoopBody:
     assume {:partition} x#AT#0 > 0;
     assume x#AT#1 == x#AT#0 - 1;
     assert {:split_here} (x#AT#1 + y#AT#0) * (x#AT#1 + y#AT#0) > 25;
     assume y#AT#1 == y#AT#0 + 1;
-    goto anon6_Then;
-
-  anon6_Then:
     assume {:partition} x#AT#1 < 3;
     assert 2 < 2;
     assume y#AT#1 * y#AT#1 > 4;
diff --git a/Test/test0/Split/Foo.split.2.bpl.expect b/Test/test0/Split/Foo.split.2.bpl.expect
index b07405c80..7f28a2ebf 100644
--- a/Test/test0/Split/Foo.split.2.bpl.expect
+++ b/Test/test0/Split/Foo.split.2.bpl.expect
@@ -1,27 +1,15 @@
 implementation Foo() returns (y: int)
 {
 
-  PreconditionGeneratedEntry:
-    goto anon0;
-
   anon0:
     assume 5 + 0 == 5;
     assume 5 * 5 <= 25;
-    goto anon5_LoopHead;
-
-  anon5_LoopHead:
     assume x#AT#0 + y#AT#0 == 5;
     assume x#AT#0 * x#AT#0 <= 25;
-    goto anon5_LoopBody;
-
-  anon5_LoopBody:
     assume {:partition} x#AT#0 > 0;
     assume x#AT#1 == x#AT#0 - 1;
     assume (x#AT#1 + y#AT#0) * (x#AT#1 + y#AT#0) > 25;
     assume y#AT#1 == y#AT#0 + 1;
-    goto anon6_Else;
-
-  anon6_Else:
     assume {:partition} 3 <= x#AT#1;
     assert {:split_here} y#AT#1 * y#AT#1 * y#AT#1 < 8;
     assert 2 < 2;
diff --git a/Test/test0/Split/Foo.split.3.bpl.expect b/Test/test0/Split/Foo.split.3.bpl.expect
index 9ef24510f..eb031aa38 100644
--- a/Test/test0/Split/Foo.split.3.bpl.expect
+++ b/Test/test0/Split/Foo.split.3.bpl.expect
@@ -1,20 +1,11 @@
 implementation Foo() returns (y: int)
 {
 
-  PreconditionGeneratedEntry:
-    goto anon0;
-
   anon0:
     assume 5 + 0 == 5;
     assume 5 * 5 <= 25;
-    goto anon5_LoopHead;
-
-  anon5_LoopHead:
     assume x#AT#0 + y#AT#0 == 5;
     assume x#AT#0 * x#AT#0 <= 25;
-    goto anon5_LoopBody;
-
-  anon5_LoopBody:
     assume {:partition} x#AT#0 > 0;
     assume x#AT#1 == x#AT#0 - 1;
     assume (x#AT#1 + y#AT#0) * (x#AT#1 + y#AT#0) > 25;
diff --git a/Test/test0/Split/Split.bpl.expect b/Test/test0/Split/Split.bpl.expect
index ad3ef1049..67f8e9921 100644
--- a/Test/test0/Split/Split.bpl.expect
+++ b/Test/test0/Split/Split.bpl.expect
@@ -1,7 +1,5 @@
 Split.bpl(19,5): Error: this assertion could not be proved
 Execution trace:
     Split.bpl(12,5): anon0
-    Split.bpl(14,3): anon5_LoopHead
-    Split.bpl(18,7): anon5_LoopBody
 
 Boogie program verifier finished with 0 verified, 1 error
diff --git a/Test/test0/SplitOnEveryAssert.bpl b/Test/test0/SplitOnEveryAssert.bpl
index 43698941f..c883fb50c 100644
--- a/Test/test0/SplitOnEveryAssert.bpl
+++ b/Test/test0/SplitOnEveryAssert.bpl
@@ -3,20 +3,19 @@
 // RUN: %OutputCheck --file-to-check "%t" "%s"
 
 // CHECK: Verifying DoTheSplitting ...
-// CHECK:      checking split 1/12.*
-// CHECK:      checking split 2/12.*
-// CHECK:      checking split 3/12.*
-// CHECK:      checking split 4/12.*
-// CHECK:      --> split #4 done,  \[.* s\] Invalid
-// CHECK:      checking split 5/12.*
-// CHECK:      checking split 6/12.*
-// CHECK:      checking split 7/12.*
-// CHECK:      checking split 8/12.*
-// CHECK:      checking split 9/12.*
-// CHECK:      checking split 10/12.*
-// CHECK:      checking split 11/12.*
-// CHECK:      checking split 12/12.*
-// CHECK-L: SplitOnEveryAssert.bpl(37,5): Error: this assertion could not be proved
+// CHECK:      checking split 1/11.*
+// CHECK:      checking split 2/11.*
+// CHECK:      checking split 3/11.*
+// CHECK:      --> split #3 done,  \[.* s\] Invalid
+// CHECK:      checking split 4/11.*
+// CHECK:      checking split 5/11.*
+// CHECK:      checking split 6/11.*
+// CHECK:      checking split 7/11.*
+// CHECK:      checking split 8/11.*
+// CHECK:      checking split 9/11.*
+// CHECK:      checking split 10/11.*
+// CHECK:      checking split 11/11.*
+// CHECK-L: SplitOnEveryAssert.bpl(36,5): Error: this assertion could not be proved
 
 // Verify the second procedure is NOT split. .* is necessary to match the blank line in-between.
 // CHECK-NEXT: .*