diff --git a/Source/VCGeneration/Splits/IsolateAttributeOnJumpsHandler.cs b/Source/VCGeneration/Splits/IsolateAttributeOnJumpsHandler.cs index 1b38445e6..9a26ea973 100644 --- a/Source/VCGeneration/Splits/IsolateAttributeOnJumpsHandler.cs +++ b/Source/VCGeneration/Splits/IsolateAttributeOnJumpsHandler.cs @@ -44,7 +44,8 @@ public static (List Isolated, ManualSplit Remainder) GetParts(VCGen var blocksToInclude = ancestors.Union(descendants).ToHashSet(); var originalReturn = ((GotoFromReturn)gotoCmd.tok).Origin; - if (originalReturn.tok is ImplicitJump) { + var returnWasFromOriginalSource = originalReturn.tok is not Token; + if (returnWasFromOriginalSource) { continue; }