diff --git a/Source/Directory.Build.props b/Source/Directory.Build.props
index c8f378583..7ba4204a9 100644
--- a/Source/Directory.Build.props
+++ b/Source/Directory.Build.props
@@ -2,7 +2,7 @@
 
   <!-- Target framework and package configuration -->
   <PropertyGroup>
-    <Version>3.4.0</Version>
+    <Version>3.4.1</Version>
     <TargetFramework>net6.0</TargetFramework>
     <GeneratePackageOnBuild>false</GeneratePackageOnBuild>
     <Authors>Boogie</Authors>
diff --git a/Source/VCGeneration/Splits/BlockRewriter.cs b/Source/VCGeneration/Splits/BlockRewriter.cs
index 404dd4605..dbf03f8ca 100644
--- a/Source/VCGeneration/Splits/BlockRewriter.cs
+++ b/Source/VCGeneration/Splits/BlockRewriter.cs
@@ -74,7 +74,7 @@ void AddSplitsFromIndex(ImmutableStack<IToken> choices, int gotoIndex, IReadOnly
               newBlock.TransferCmd = new ReturnCmd(origin);
             }
           });
-        result.Add(CreateSplit(new PathOrigin(origin, choices.OrderBy(b => b.pos).ToList(), "paths"), newBlocks));
+        result.Add(CreateSplit(new PathOrigin(origin, choices.OrderBy(b => b.pos).ToList()), newBlocks));
       } else {
         var splitGoto = splitCommands[gotoIndex];
         if (!blocksToIncludeForChoices.Contains(splitGoto.Block))
diff --git a/Source/VCGeneration/Splits/FocusAttributeHandler.cs b/Source/VCGeneration/Splits/FocusAttributeHandler.cs
index 85d69efa5..7beca7b53 100644
--- a/Source/VCGeneration/Splits/FocusAttributeHandler.cs
+++ b/Source/VCGeneration/Splits/FocusAttributeHandler.cs
@@ -48,16 +48,17 @@ public static List<ManualSplit> GetParts(VCGenOptions options, ImplementationRun
     AddSplitsFromIndex(ImmutableStack<IToken>.Empty, 0, implementation.Blocks.ToHashSet(), ImmutableHashSet<Block>.Empty);
     return result;
 
-    void AddSplitsFromIndex(ImmutableStack<IToken> path, int focusIndex, IReadOnlySet<Block> blocksToInclude, ISet<Block> freeAssumeBlocks) {
+    void AddSplitsFromIndex(ImmutableStack<IToken> focusedBlocks, int focusIndex, IReadOnlySet<Block> blocksToInclude, ISet<Block> freeAssumeBlocks) {
       var allFocusBlocksHaveBeenProcessed = focusIndex == focusBlocks.Count;
       if (allFocusBlocksHaveBeenProcessed) {
         
         // freeBlocks consist of the predecessors of the relevant foci.
         // Their assertions turn into assumes and any splits inside them are disabled.
         var newBlocks = rewriter.ComputeNewBlocks(blocksToInclude, freeAssumeBlocks);
-        IImplementationPartOrigin token = path.Any() 
-          ? new PathOrigin(new ImplementationRootOrigin(run.Implementation), 
-            path.OrderBy(t => t.pos).ToList(), "focus") 
+        var focussedSet = focusedBlocks.ToHashSet();
+        IImplementationPartOrigin token = focusedBlocks.Any() 
+          ? new FocusOrigin(new ImplementationRootOrigin(run.Implementation), 
+            focusBlocks.Select(b => (b.Token, focussedSet.Contains(b.Token))).ToList()) 
           : new ImplementationRootOrigin(run.Implementation); 
         result.Add(rewriter.CreateSplit(token, newBlocks));
       } else {
@@ -65,21 +66,21 @@ void AddSplitsFromIndex(ImmutableStack<IToken> path, int focusIndex, IReadOnlySe
         if (!blocksToInclude.Contains(focusBlock) || freeAssumeBlocks.Contains(focusBlock))
         {
           // This focus block can not be reached in our current path, so we ignore it by continuing
-          AddSplitsFromIndex(path, focusIndex + 1, blocksToInclude, freeAssumeBlocks);
+          AddSplitsFromIndex(focusedBlocks, focusIndex + 1, blocksToInclude, freeAssumeBlocks);
         }
         else
         {
           var dominatedBlocks = BlockRewriter.DominatedBlocks(rewriter.OrderedBlocks, focusBlock, blocksToInclude);
           // Recursive call that does NOT focus the block
           // Contains all blocks except the ones dominated by the focus block
-          AddSplitsFromIndex(path, focusIndex + 1, 
+          AddSplitsFromIndex(focusedBlocks, focusIndex + 1, 
             blocksToInclude.Where(blk => !dominatedBlocks.Contains(blk)).ToHashSet(), freeAssumeBlocks);
           var ancestors = ancestorsPerBlock[focusBlock];
           var descendants = descendantsPerBlock[focusBlock];
           
           // Recursive call that does focus the block
           // Contains all the ancestors, the focus block, and the descendants.
-          AddSplitsFromIndex(path.Push(nextToken), focusIndex + 1, 
+          AddSplitsFromIndex(focusedBlocks.Push(nextToken), focusIndex + 1, 
             ancestors.Union(descendants).Intersect(blocksToInclude).ToHashSet(), 
             ancestors.Union(freeAssumeBlocks).ToHashSet());
         } 
diff --git a/Source/VCGeneration/Splits/FocusOrigin.cs b/Source/VCGeneration/Splits/FocusOrigin.cs
new file mode 100644
index 000000000..9794c0de7
--- /dev/null
+++ b/Source/VCGeneration/Splits/FocusOrigin.cs
@@ -0,0 +1,23 @@
+#nullable enable
+using System.Collections.Generic;
+using System.Linq;
+using Microsoft.Boogie;
+
+namespace VCGeneration;
+
+public class FocusOrigin : TokenWrapper, IImplementationPartOrigin {
+
+  public FocusOrigin(IImplementationPartOrigin inner, List<(IToken Token, bool DidFocus)> focusChoices) : base(inner) {
+    Inner = inner;
+    FocusChoices = focusChoices;
+  }
+
+  public new IImplementationPartOrigin Inner { get; }
+  public List<(IToken Token, bool DidFocus)> FocusChoices { get; }
+  public string ShortName {
+    get {
+      var choices = string.Join(",", FocusChoices.Select(b => (b.DidFocus ? "+" : "-") + b.Token.line));
+      return $"{Inner.ShortName}/focus[{choices}]";
+    }
+  }
+}
\ No newline at end of file
diff --git a/Source/VCGeneration/Splits/ImplementationRootOrigin.cs b/Source/VCGeneration/Splits/ImplementationRootOrigin.cs
new file mode 100644
index 000000000..f43bc325b
--- /dev/null
+++ b/Source/VCGeneration/Splits/ImplementationRootOrigin.cs
@@ -0,0 +1,12 @@
+#nullable enable
+using Microsoft.Boogie;
+
+namespace VCGeneration;
+
+public class ImplementationRootOrigin : TokenWrapper, IImplementationPartOrigin {
+  public ImplementationRootOrigin(Implementation implementation) : base(implementation.tok)
+  {
+  }
+
+  public string ShortName => "";
+}
\ No newline at end of file
diff --git a/Source/VCGeneration/Splits/IsolateAttributeOnAssertsHandler.cs b/Source/VCGeneration/Splits/IsolateAttributeOnAssertsHandler.cs
index 9cd8bd66f..305e5186d 100644
--- a/Source/VCGeneration/Splits/IsolateAttributeOnAssertsHandler.cs
+++ b/Source/VCGeneration/Splits/IsolateAttributeOnAssertsHandler.cs
@@ -81,7 +81,7 @@ List<Cmd> GetCommandsForBlockWithAssert(Block currentBlock, AssertCmd assert)
 
     ManualSplit GetSplitWithoutIsolatedAssertions() {
       if (!isolatedAssertions.Any()) {
-        return rewriter.CreateSplit(partToDivide.Token, partToDivide.Blocks);
+        return rewriter.CreateSplit(new RemainingAssertionsOrigin(partToDivide.Token), partToDivide.Blocks);
       }
 
       var newBlocks = rewriter.ComputeNewBlocks(null, (oldBlock, newBlock) => newBlock.Cmds = GetCommands(oldBlock));
@@ -103,5 +103,4 @@ public IsolatedAssertionOrigin(IImplementationPartOrigin origin, AssertCmd isola
   }
 
   public string ShortName => $"{Origin.ShortName}/assert@{IsolatedAssert.Line}";
-  public string KindName => "assertion";
 }
\ No newline at end of file
diff --git a/Source/VCGeneration/Splits/IsolateAttributeOnJumpsHandler.cs b/Source/VCGeneration/Splits/IsolateAttributeOnJumpsHandler.cs
index a11a9f3c0..b8d8af84a 100644
--- a/Source/VCGeneration/Splits/IsolateAttributeOnJumpsHandler.cs
+++ b/Source/VCGeneration/Splits/IsolateAttributeOnJumpsHandler.cs
@@ -45,12 +45,12 @@ public static (List<ManualSplit> Isolated, ManualSplit Remainder) GetParts(VCGen
       var blocksToInclude = ancestors.Union(descendants).ToHashSet();
 
       var originalJump = gotoFromReturn?.Origin ?? (TransferCmd)gotoCmd;
+      var origin = new JumpOrigin(partToDivide.Token, originalJump);
       
       if (isolateAttribute != null && isolateAttribute.Params.OfType<string>().Any(p => Equals(p, "paths"))) {
         // These conditions hold if the goto was originally a return
         Debug.Assert(gotoCmd.LabelTargets.Count == 1);
         Debug.Assert(gotoCmd.LabelTargets[0].TransferCmd is not GotoCmd);
-        var origin = new JumpOrigin(originalJump);
         results.AddRange(rewriter.GetSplitsForIsolatedPaths(gotoCmd.LabelTargets[0], blocksToInclude, origin));
       } else {
         var newBlocks = rewriter.ComputeNewBlocks(blocksToInclude, (oldBlock, newBlock) => {
@@ -68,7 +68,7 @@ Possibly two block are coalesced which deletes the goto with the GotoFromReturn
             }
           }
         });
-        results.Add(rewriter.CreateSplit(new JumpOrigin(originalJump), newBlocks));
+        results.Add(rewriter.CreateSplit(origin, newBlocks));
       }
     }
 
@@ -84,20 +84,20 @@ ManualSplit GetPartWithoutIsolatedReturns() {
           newBlock.TransferCmd = new ReturnCmd(Token.NoToken);
         }
       });
-      return rewriter.CreateSplit(new ImplementationRootOrigin(partToDivide.Implementation), 
-        newBlocks);
+      return rewriter.CreateSplit(new RemainingAssertionsOrigin(partToDivide.Token), newBlocks);
     }
   }
 }
 
-
 public class JumpOrigin : TokenWrapper, IImplementationPartOrigin {
+  public IImplementationPartOrigin Origin { get; }
   public TransferCmd IsolatedReturn { get; }
 
-  public JumpOrigin(TransferCmd isolatedReturn) : base(isolatedReturn.tok) {
+  public JumpOrigin(IImplementationPartOrigin origin, TransferCmd isolatedReturn) : base(isolatedReturn.tok) {
+    Origin = origin;
     this.IsolatedReturn = isolatedReturn;
   }
 
-  public string ShortName => $"/{KindName}@{IsolatedReturn.Line}";
+  public string ShortName => $"{Origin.ShortName}/{KindName}@{IsolatedReturn.Line}";
   public string KindName => IsolatedReturn is ReturnCmd ? "return" : "goto";
 }
\ No newline at end of file
diff --git a/Source/VCGeneration/Splits/ManualSplitFinder.cs b/Source/VCGeneration/Splits/ManualSplitFinder.cs
index a2706da9e..a9c653b70 100644
--- a/Source/VCGeneration/Splits/ManualSplitFinder.cs
+++ b/Source/VCGeneration/Splits/ManualSplitFinder.cs
@@ -45,5 +45,4 @@ public static IEnumerable<ManualSplit> GetParts(VCGenOptions options, Implementa
 
 public interface IImplementationPartOrigin : IToken {
   string ShortName { get; }
-  string KindName { get; }
 }
\ No newline at end of file
diff --git a/Source/VCGeneration/Splits/PathOrigin.cs b/Source/VCGeneration/Splits/PathOrigin.cs
new file mode 100644
index 000000000..cc7a4d49c
--- /dev/null
+++ b/Source/VCGeneration/Splits/PathOrigin.cs
@@ -0,0 +1,18 @@
+#nullable enable
+using System.Collections.Generic;
+using System.Linq;
+using Microsoft.Boogie;
+
+namespace VCGeneration;
+
+public class PathOrigin : TokenWrapper, IImplementationPartOrigin {
+
+  public PathOrigin(IImplementationPartOrigin inner, List<IToken> branchTokens) : base(inner) {
+    Inner = inner;
+    BranchTokens = branchTokens;
+  }
+
+  public new IImplementationPartOrigin Inner { get; }
+  public List<IToken> BranchTokens { get; }
+  public string ShortName => $"{Inner.ShortName}/path[{string.Join(",", BranchTokens.Select(b => b.line))}]";
+}
\ No newline at end of file
diff --git a/Source/VCGeneration/Splits/PathToken.cs b/Source/VCGeneration/Splits/PathToken.cs
deleted file mode 100644
index a8ce48964..000000000
--- a/Source/VCGeneration/Splits/PathToken.cs
+++ /dev/null
@@ -1,33 +0,0 @@
-#nullable enable
-using System.Collections.Generic;
-using System.Collections.Immutable;
-using System.IO;
-using System.Linq;
-using Microsoft.Boogie;
-using Microsoft.Boogie.GraphUtil;
-
-namespace VCGeneration;
-
-public class PathOrigin : TokenWrapper, IImplementationPartOrigin {
-  private readonly string kindName;
-
-  public PathOrigin(IImplementationPartOrigin inner, List<IToken> branchTokens, string kindName) : base(inner) {
-    this.kindName = kindName;
-    Inner = inner;
-    BranchTokens = branchTokens;
-  }
-
-  public new IImplementationPartOrigin Inner { get; }
-  public List<IToken> BranchTokens { get; }
-  public string ShortName => $"{Inner.ShortName}/{kindName}[{string.Join(",", BranchTokens.Select(b => b.line))}]";
-  public string KindName => "path";
-}
-
-class ImplementationRootOrigin : TokenWrapper, IImplementationPartOrigin {
-  public ImplementationRootOrigin(Implementation implementation) : base(implementation.tok)
-  {
-  }
-
-  public string ShortName => "";
-  public string KindName => "root";
-}
\ No newline at end of file
diff --git a/Source/VCGeneration/Splits/RemainingAssertionsOrigin.cs b/Source/VCGeneration/Splits/RemainingAssertionsOrigin.cs
new file mode 100644
index 000000000..a3efc82e8
--- /dev/null
+++ b/Source/VCGeneration/Splits/RemainingAssertionsOrigin.cs
@@ -0,0 +1,12 @@
+#nullable enable
+namespace VCGeneration;
+
+public class RemainingAssertionsOrigin : TokenWrapper, IImplementationPartOrigin {
+  public IImplementationPartOrigin Origin { get; }
+
+  public RemainingAssertionsOrigin(IImplementationPartOrigin origin) : base(origin) {
+    Origin = origin;
+  }
+
+  public string ShortName => $"{Origin.ShortName}/remainingAssertions";
+}
\ No newline at end of file
diff --git a/Source/VCGeneration/Splits/SplitAttributeHandler.cs b/Source/VCGeneration/Splits/SplitAttributeHandler.cs
index 0b6fccacf..8e414fb6c 100644
--- a/Source/VCGeneration/Splits/SplitAttributeHandler.cs
+++ b/Source/VCGeneration/Splits/SplitAttributeHandler.cs
@@ -38,7 +38,7 @@ public static List<ManualSplit> GetParts(ManualSplit partToSplit) {
     var blockStartToSplit = GetMapFromBlockStartToSplit(partToSplit.Blocks, splitsPerBlock);
 
     var beforeSplitsVc = GetImplementationPartAfterSplit(CreateVc, partToSplit, blockStartToSplit,
-      entryPoint, splits, null);
+      entryPoint, splits, null, new UntilFirstSplitOrigin(partToSplit.Token));
     if (beforeSplitsVc != null)
     {
       vcs.Add(beforeSplitsVc);
@@ -52,7 +52,7 @@ public static List<ManualSplit> GetParts(ManualSplit partToSplit) {
       foreach (var split in splitsForBlock)
       {
         var splitVc = GetImplementationPartAfterSplit(CreateVc, partToSplit, 
-          blockStartToSplit, block, splits, split);
+          blockStartToSplit, block, splits, split, new AfterSplitOrigin(partToSplit.Token, split.tok));
         if (splitVc != null)
         {
           vcs.Add(splitVc);
@@ -112,7 +112,7 @@ private static bool ShouldSplitHere(Cmd c) {
   private static ManualSplit? GetImplementationPartAfterSplit(Func<IImplementationPartOrigin, List<Block>, ManualSplit> createVc, 
     ManualSplit partToSplit, 
     Dictionary<Block, Cmd?> blockStartToSplit, Block blockWithSplit, 
-    HashSet<Cmd> splits, Cmd? split) 
+    HashSet<Cmd> splits, Cmd? split, IImplementationPartOrigin origin) 
   {
     var assertionCount = 0;
     
@@ -132,7 +132,7 @@ private static bool ShouldSplitHere(Cmd c) {
       return null;
     }
 
-    return createVc(split == null ? partToSplit.Token : new SplitOrigin(partToSplit.Token, split.tok), newBlocks);
+    return createVc(origin, newBlocks);
 
     List<Cmd> GetCommandsForBlockImmediatelyDominatedBySplit(Block currentBlock)
     {
@@ -208,15 +208,24 @@ private static void AddJumpsToNewBlocks(Dictionary<Block, Block> oldToNewBlockMa
   }
 }
 
-class SplitOrigin : TokenWrapper, IImplementationPartOrigin {
+public class UntilFirstSplitOrigin : TokenWrapper, IImplementationPartOrigin {
+  public new IImplementationPartOrigin Inner { get; }
+
+  public UntilFirstSplitOrigin(IImplementationPartOrigin inner) : base(inner) {
+    Inner = inner;
+  }
+
+  public string ShortName => $"{Inner.ShortName}/untilFirstSplit";
+}
+
+public class AfterSplitOrigin : TokenWrapper, IImplementationPartOrigin {
   public new IImplementationPartOrigin Inner { get; }
   public IToken Tok { get; }
 
-  public SplitOrigin(IImplementationPartOrigin inner, IToken tok) : base(tok) {
+  public AfterSplitOrigin(IImplementationPartOrigin inner, IToken tok) : base(tok) {
     Inner = inner;
     Tok = tok;
   }
 
-  public string ShortName => $"{Inner.ShortName}/split@{line}";
-  public string KindName => "split";
+  public string ShortName => $"{Inner.ShortName}/afterSplit@{line}";
 }
\ No newline at end of file
diff --git a/Test/implementationDivision/focus/focus.bpl.expect b/Test/implementationDivision/focus/focus.bpl.expect
index 8bb01ee29..cb760a9d1 100644
--- a/Test/implementationDivision/focus/focus.bpl.expect
+++ b/Test/implementationDivision/focus/focus.bpl.expect
@@ -13,7 +13,7 @@ implementation Ex() returns (y: int)
 }
 
 
-implementation Ex/focus[16]/split@15() returns (y: int)
+implementation Ex/focus[+16,-20,-25]/afterSplit@15() returns (y: int)
 {
 
   anon0:
@@ -32,7 +32,7 @@ implementation Ex/focus[16]/split@15() returns (y: int)
 }
 
 
-implementation Ex/focus[16,25]() returns (y: int)
+implementation Ex/focus[+16,-20,+25]() returns (y: int)
 {
 
   anon0:
@@ -56,7 +56,7 @@ implementation Ex/focus[16,25]() returns (y: int)
 }
 
 
-implementation Ex/focus[16,20]() returns (y: int)
+implementation Ex/focus[+16,+20,-25]() returns (y: int)
 {
 
   anon0:
@@ -76,7 +76,7 @@ implementation Ex/focus[16,20]() returns (y: int)
 }
 
 
-implementation Ex/focus[16,20,25]() returns (y: int)
+implementation Ex/focus[+16,+20,+25]() returns (y: int)
 {
 
   anon0:
@@ -102,7 +102,7 @@ implementation Ex/focus[16,20,25]() returns (y: int)
 
 
 focus.bpl(15,5): Error: this assertion could not be proved
-implementation focusInconsistency/focus[38](x: int) returns (y: int)
+implementation focusInconsistency/focus[+38](x: int) returns (y: int)
 {
 
   anon0:
diff --git a/Test/implementationDivision/isolateAssertion/isolateAssertion.bpl.expect b/Test/implementationDivision/isolateAssertion/isolateAssertion.bpl.expect
index c17e44842..140bd6834 100644
--- a/Test/implementationDivision/isolateAssertion/isolateAssertion.bpl.expect
+++ b/Test/implementationDivision/isolateAssertion/isolateAssertion.bpl.expect
@@ -81,7 +81,7 @@ implementation IsolateAssertion(x: int, y: int)
 
 isolateAssertion.bpl(20,3): Error: this assertion could not be proved
 isolateAssertion.bpl(21,3): Error: this assertion could not be proved
-implementation IsolatePathsAssertion/assert@50/paths[29,45](x: int, y: int)
+implementation IsolatePathsAssertion/assert@50/path[29,45](x: int, y: int)
 {
 
   anon0:
@@ -112,7 +112,7 @@ implementation IsolatePathsAssertion/assert@50/paths[29,45](x: int, y: int)
 }
 
 
-implementation IsolatePathsAssertion/assert@50/paths[29,47](x: int, y: int)
+implementation IsolatePathsAssertion/assert@50/path[29,47](x: int, y: int)
 {
 
   anon0:
@@ -143,7 +143,7 @@ implementation IsolatePathsAssertion/assert@50/paths[29,47](x: int, y: int)
 }
 
 
-implementation IsolatePathsAssertion/assert@50/paths[31,32,45](x: int, y: int)
+implementation IsolatePathsAssertion/assert@50/path[31,32,45](x: int, y: int)
 {
 
   anon0:
@@ -175,7 +175,7 @@ implementation IsolatePathsAssertion/assert@50/paths[31,32,45](x: int, y: int)
 }
 
 
-implementation IsolatePathsAssertion/assert@50/paths[31,32,47](x: int, y: int)
+implementation IsolatePathsAssertion/assert@50/path[31,32,47](x: int, y: int)
 {
 
   anon0:
@@ -207,7 +207,7 @@ implementation IsolatePathsAssertion/assert@50/paths[31,32,47](x: int, y: int)
 }
 
 
-implementation IsolatePathsAssertion/assert@50/paths[31,35,45](x: int, y: int)
+implementation IsolatePathsAssertion/assert@50/path[31,35,45](x: int, y: int)
 {
 
   anon0:
@@ -239,7 +239,7 @@ implementation IsolatePathsAssertion/assert@50/paths[31,35,45](x: int, y: int)
 }
 
 
-implementation IsolatePathsAssertion/assert@50/paths[31,35,47](x: int, y: int)
+implementation IsolatePathsAssertion/assert@50/path[31,35,47](x: int, y: int)
 {
 
   anon0:
diff --git a/Test/implementationDivision/isolateJump/isolateContinue.bpl.expect b/Test/implementationDivision/isolateJump/isolateContinue.bpl.expect
index 564b013b1..c0be7f14b 100644
--- a/Test/implementationDivision/isolateJump/isolateContinue.bpl.expect
+++ b/Test/implementationDivision/isolateJump/isolateContinue.bpl.expect
@@ -1,4 +1,4 @@
-implementation IsolateContinue(x: int) returns (r: int)
+implementation IsolateContinue/remainingAssertions(x: int) returns (r: int)
 {
 
   anon0:
diff --git a/Test/implementationDivision/isolateJump/isolateJump.bpl.expect b/Test/implementationDivision/isolateJump/isolateJump.bpl.expect
index f83e90f0d..c3d50827e 100644
--- a/Test/implementationDivision/isolateJump/isolateJump.bpl.expect
+++ b/Test/implementationDivision/isolateJump/isolateJump.bpl.expect
@@ -1,4 +1,4 @@
-implementation IsolateReturn(x: int, y: int) returns (r: int)
+implementation IsolateReturn/remainingAssertions(x: int, y: int) returns (r: int)
 {
 
   anon0:
@@ -54,7 +54,7 @@ implementation IsolateReturn/return@16(x: int, y: int) returns (r: int)
 
 isolateJump.bpl(16,21): Error: a postcondition could not be proved on this return path
 isolateJump.bpl(5,3): Related location: this is the postcondition that could not be proved
-implementation IsolateReturnPaths(x: int, y: int) returns (r: int)
+implementation IsolateReturnPaths/remainingAssertions(x: int, y: int) returns (r: int)
 {
 
   anon0:
@@ -98,7 +98,7 @@ implementation IsolateReturnPaths(x: int, y: int) returns (r: int)
 }
 
 
-implementation IsolateReturnPaths/return@44/paths[27](x: int, y: int) returns (r: int)
+implementation IsolateReturnPaths/return@44/path[27](x: int, y: int) returns (r: int)
 {
 
   anon0:
@@ -125,7 +125,7 @@ implementation IsolateReturnPaths/return@44/paths[27](x: int, y: int) returns (r
 }
 
 
-implementation IsolateReturnPaths/return@44/paths[29,30](x: int, y: int) returns (r: int)
+implementation IsolateReturnPaths/return@44/path[29,30](x: int, y: int) returns (r: int)
 {
 
   anon0:
@@ -153,7 +153,7 @@ implementation IsolateReturnPaths/return@44/paths[29,30](x: int, y: int) returns
 }
 
 
-implementation IsolateReturnPaths/return@44/paths[29,33](x: int, y: int) returns (r: int)
+implementation IsolateReturnPaths/return@44/path[29,33](x: int, y: int) returns (r: int)
 {
 
   anon0:
diff --git a/Test/implementationDivision/split/AssumeFalseSplit.bpl.expect b/Test/implementationDivision/split/AssumeFalseSplit.bpl.expect
index 3e453dc52..27e62fe1a 100644
--- a/Test/implementationDivision/split/AssumeFalseSplit.bpl.expect
+++ b/Test/implementationDivision/split/AssumeFalseSplit.bpl.expect
@@ -1,4 +1,4 @@
-implementation Foo()
+implementation Foo/untilFirstSplit()
 {
 
   anon3_Then:
@@ -8,7 +8,7 @@ implementation Foo()
 }
 
 
-implementation Foo/split@11()
+implementation Foo/afterSplit@11()
 {
 
   anon3_Else:
@@ -20,7 +20,7 @@ implementation Foo/split@11()
 }
 
 
-implementation Foo/split@12()
+implementation Foo/afterSplit@12()
 {
 
   anon3_Else:
diff --git a/Test/implementationDivision/split/Split.bpl.expect b/Test/implementationDivision/split/Split.bpl.expect
index 0765bcc8f..217f1176f 100644
--- a/Test/implementationDivision/split/Split.bpl.expect
+++ b/Test/implementationDivision/split/Split.bpl.expect
@@ -1,4 +1,4 @@
-implementation Foo() returns (y: int)
+implementation Foo/untilFirstSplit() returns (y: int)
 {
 
   anon0:
@@ -13,7 +13,7 @@ implementation Foo() returns (y: int)
 }
 
 
-implementation Foo/split@15() returns (y: int)
+implementation Foo/afterSplit@15() returns (y: int)
 {
 
   anon0:
@@ -32,7 +32,7 @@ implementation Foo/split@15() returns (y: int)
 }
 
 
-implementation Foo/split@22() returns (y: int)
+implementation Foo/afterSplit@22() returns (y: int)
 {
 
   anon0:
@@ -51,7 +51,7 @@ implementation Foo/split@22() returns (y: int)
 }
 
 
-implementation Foo/split@25() returns (y: int)
+implementation Foo/afterSplit@25() returns (y: int)
 {
 
   anon0:
@@ -86,7 +86,7 @@ implementation Foo/split@25() returns (y: int)
 }
 
 
-implementation Foo/split@19() returns (y: int)
+implementation Foo/afterSplit@19() returns (y: int)
 {
 
   anon0: