Tests pass now

boogie-org · Oct 22, 2024 · ca07b3f · ca07b3f
1 parent 14934ec
commit ca07b3f
Showing 1 changed file with 7 additions and 3 deletions.
diff --git a/Source/VCGeneration/Splits/IsolateAttributeOnJumpsHandler.cs b/Source/VCGeneration/Splits/IsolateAttributeOnJumpsHandler.cs
@@ -59,9 +59,13 @@ public static (List<ManualSplit> Isolated, ManualSplit Remainder) GetParts(VCGen
               .ToList();
           } else {
             newBlock.Cmds = oldBlock.Cmds;
-            // if (newBlock.TransferCmd is ReturnCmd) {
-            //   newBlock.TransferCmd = gotoFromReturn?.Origin;
-            // }
+            if (newBlock.TransferCmd is ReturnCmd && gotoFromReturn != null) {
+              /*
+               I'm not sure why this is necessary.
+               Possibly two block are coalesced which deletes the goto with the GotoFromReturn
+               */
+              newBlock.TransferCmd = gotoFromReturn.Origin;
+            }
           }
         });
         results.Add(rewriter.CreateSplit(new JumpOrigin(originalJump), newBlocks));