diff --git a/Strata/DL/Imperative/BasicBlock.lean b/Strata/DL/Imperative/BasicBlock.lean
index c956006655..ff7aaa36ca 100644
--- a/Strata/DL/Imperative/BasicBlock.lean
+++ b/Strata/DL/Imperative/BasicBlock.lean
@@ -40,8 +40,8 @@ inductive DetTransferCmd (Label : Type) (P : PureExpr) where
 model it instead using `condGoto`. By defining this function, we can easily
 create unconditional jumps, and future proof against the possibility of adding
 it as a constructor in the future.  -/
-def DetTransferCmd.goto [HasBool P] (l : Label) : DetTransferCmd Label P :=
-  condGoto HasBool.tt l l
+def DetTransferCmd.goto [HasBool P] (l : Label) (md : MetaData P := .empty) : DetTransferCmd Label P :=
+  condGoto HasBool.tt l l md
 
 /-- A `NondetTransfer` command terminates a non-deterministic basic block,
 indicating the list of possible blocks where execution could proceed next, if
diff --git a/Strata/Transform/StructuredToUnstructured.lean b/Strata/Transform/StructuredToUnstructured.lean
index eb8d3e9558..60b9165aff 100644
--- a/Strata/Transform/StructuredToUnstructured.lean
+++ b/Strata/Transform/StructuredToUnstructured.lean
@@ -65,7 +65,7 @@ match ss with
 | .typeDecl _ _ :: rest => do
   -- Not yet supported, so just continue with `rest`.
   stmtsToBlocks k rest exitConts accum
-| .block l bss _md :: rest => do
+| .block l bss md :: rest => do
   -- Process rest first
   let (kNext, bsNext) ← stmtsToBlocks k rest exitConts []
   -- Process block body, extending the list of exit continuations.
@@ -77,9 +77,9 @@ match ss with
     -- Empty accumulated block
     pure (accumEntry, accumBlocks ++ bbs ++ bsNext)
   else
-    let b := (l, { cmds := [], transfer := .goto bl })
+    let b := (l, { cmds := [], transfer := .goto bl md })
     pure (l, accumBlocks ++ [b] ++ bbs ++ bsNext)
-| .ite c tss fss _md :: rest => do
+| .ite c tss fss md :: rest => do
   -- Process rest first
   let (kNext, bsNext) ← stmtsToBlocks k rest exitConts []
   -- Create ite block
@@ -95,9 +95,9 @@ match ss with
       let initCmd := HasInit.init ident HasBool.boolTy .nondet MetaData.empty
       pure (HasFvar.mkFvar ident, [initCmd])
   let (accumEntry, accumBlocks) ← flushCmds "ite$" (accum ++ extraCmds)
-    (.some (.condGoto condExpr tl fl)) l
+    (.some (.condGoto condExpr tl fl md)) l
   pure (accumEntry, accumBlocks ++ tbs ++ fbs ++ bsNext)
-| .loop c m is bss _md :: rest => do
+| .loop c m is bss md :: rest => do
   -- Process rest first
   let (kNext, bsNext) ← stmtsToBlocks k rest exitConts []
   -- Create loop entry block
@@ -135,7 +135,7 @@ match ss with
   -- For nondet guards, introduce a fresh boolean variable
   match c with
   | .det e =>
-    let b := (lentry, { cmds := invCmds ++ measureCmds, transfer := .condGoto e bl kNext })
+    let b := (lentry, { cmds := invCmds ++ measureCmds, transfer := .condGoto e bl kNext md })
     let (accumEntry, accumBlocks) ← flushCmds "before_loop$" accum .none lentry
     pure (accumEntry, accumBlocks ++ [b] ++ bbs ++ decreaseBlocks ++ bsNext)
   | .nondet => do
@@ -143,10 +143,10 @@ match ss with
     let ident := HasIdent.ident (P := P) freshName
     let initCmd := HasInit.init ident HasBool.boolTy .nondet MetaData.empty
     let b := (lentry, { cmds := [initCmd] ++ invCmds ++ measureCmds,
-                        transfer := .condGoto (HasFvar.mkFvar ident) bl kNext })
+                        transfer := .condGoto (HasFvar.mkFvar ident) bl kNext md })
     let (accumEntry, accumBlocks) ← flushCmds "before_loop$" accum .none lentry
     pure (accumEntry, accumBlocks ++ [b] ++ bbs ++ decreaseBlocks ++ bsNext)
-| .exit l? _md :: _ => do
+| .exit l? md :: _ => do
   -- Find the continuation of the block labeled `l`, or the most recently-added
   -- block if `l` is `.none`.
   let bk :=
@@ -167,7 +167,7 @@ match ss with
     match l? with
     | .some l => s!"block${l}$"
     | .none => "block$"
-  flushCmds exitName accum .none bk
+  flushCmds exitName accum (.some (.goto bk md)) bk
 
 def stmtsToCFGM
   [HasBool P] [HasPassiveCmds P CmdT] [HasInit P CmdT]
diff --git a/StrataTest/Languages/Core/Examples/Exit.lean b/StrataTest/Languages/Core/Examples/Exit.lean
index 53dedb039d..7d9b7529f4 100644
--- a/StrataTest/Languages/Core/Examples/Exit.lean
+++ b/StrataTest/Languages/Core/Examples/Exit.lean
@@ -116,10 +116,10 @@ Result: ✅ pass
 info: Entry: l1
 
 l1:
-  condGoto true block$l1$_2 block$l1$_2
+  #[<[fileRange]: :387-502>] condGoto true block$l1$_2 block$l1$_2
 block$l1$_2:
   assert [a1]: x == x;
-  condGoto true l$_1 l$_1
+  #[<[fileRange]: :426-434>] condGoto true l$_1 l$_1
 l$_1:
   assert [a3]: x == x;
   condGoto true end$_0 end$_0
@@ -133,29 +133,29 @@ end$_0:
 info: Entry: l5
 
 l5:
-  condGoto true l4 l4
+  #[<[fileRange]: :577-1056>] condGoto true l4 l4
 l4:
-  condGoto true l4_before l4_before
+  #[<[fileRange]: :589-1050>] condGoto true l4_before l4_before
 l4_before:
-  condGoto true l3_before l3_before
+  #[<[fileRange]: :603-996>] condGoto true l3_before l3_before
 l3_before:
-  condGoto true l1 l1
+  #[<[fileRange]: :626-933>] condGoto true l1 l1
 l1:
-  condGoto true ite$_5 ite$_5
+  #[<[fileRange]: :651-835>] condGoto true ite$_5 ite$_5
 ite$_5:
   assert [a4]: x == x;
-  condGoto x > 0 block$l5$_2 block$l5$_1
+  #[<[fileRange]: :706-821>] condGoto x > 0 block$l5$_2 block$l5$_1
 l2:
-  condGoto true l$_3 l$_3
+  #[<[fileRange]: :848-921>] condGoto true l$_3 l$_3
 l$_3:
   assert [a5]: !(x == x);
   condGoto true block$l5$_2 block$l5$_2
 block$l5$_2:
   assert [a6]: x * 2 > x;
-  condGoto true end$_0 end$_0
+  #[<[fileRange]: :978-986>] condGoto true end$_0 end$_0
 block$l5$_1:
   assert [a7]: x <= 0;
-  condGoto true end$_0 end$_0
+  #[<[fileRange]: :1034-1042>] condGoto true end$_0 end$_0
 end$_0:
   finish
 -/
diff --git a/StrataTest/Languages/Core/Examples/Loops.lean b/StrataTest/Languages/Core/Examples/Loops.lean
index 729c9c9a23..e382bc4314 100644
--- a/StrataTest/Languages/Core/Examples/Loops.lean
+++ b/StrataTest/Languages/Core/Examples/Loops.lean
@@ -52,7 +52,7 @@ loop_entry$_1:
   var loop_measure$_2 : int;
   assume [assume_loop_measure$_2]: loop_measure$_2 == n;
   assert [measure_lb_loop_measure$_2]: !(loop_measure$_2 < 0);
-  condGoto i < n l$_4 end$_0
+  #[<[fileRange]: :813-919>] condGoto i < n l$_4 end$_0
 l$_4:
   i := i + 1;
   condGoto true measure_decrease$_3 measure_decrease$_3
@@ -140,7 +140,7 @@ loop_entry$_1:
   var loop_measure$_2 : int;
   assume [assume_loop_measure$_2]: loop_measure$_2 == n - i;
   assert [measure_lb_loop_measure$_2]: !(loop_measure$_2 < 0);
-  condGoto i < n l$_4 end$_0
+  #[<[fileRange]: :2438-2594>] condGoto i < n l$_4 end$_0
 l$_4:
   i := i + 1;
   s := s + i;
@@ -387,7 +387,7 @@ Context: Global scope:
   var loop_measure$_2 : int;
   assume [assume_loop_measure$_2]: loop_measure$_2 == n - x;
   assert [measure_lb_loop_measure$_2]: !(loop_measure$_2 < 0);
-  condGoto x < n before_loop$_11 end$_0
+  #[<[fileRange]: :8059-8312>] condGoto x < n before_loop$_11 end$_0
 before_loop$_11:
   y := 0;
   condGoto true loop_entry$_5 loop_entry$_5
@@ -397,7 +397,7 @@ loop_entry$_5:
   var loop_measure$_6 : int;
   assume [assume_loop_measure$_6]: loop_measure$_6 == x - y;
   assert [measure_lb_loop_measure$_6]: !(loop_measure$_6 < 0);
-  condGoto y < x l$_8 l$_4
+  #[<[fileRange]: :8179-8292>] condGoto y < x l$_8 l$_4
 l$_8:
   y := y + 1;
   condGoto true measure_decrease$_7 measure_decrease$_7