diff --git a/Strata/Backends/CBMC/GOTO/Instruction.lean b/Strata/Backends/CBMC/GOTO/Instruction.lean
index ac0597023..11832259b 100644
--- a/Strata/Backends/CBMC/GOTO/Instruction.lean
+++ b/Strata/Backends/CBMC/GOTO/Instruction.lean
@@ -108,9 +108,15 @@ structure Instruction where
 
 instance : ToString Instruction where
   toString instr :=
-    let code_str := f!" {instr.code}"
+    let payload := match instr.type with
+      | .GOTO => match instr.target with
+        | some t => s!" {t}"
+        | none   => ""
+      | .LOCATION => s!" {instr.locationNum}"
+      | .ASSUME | .ASSERT => ""
+      | _ => s!" {Std.format instr.code}"
     let guard_str := if Expr.beq instr.guard Expr.true then "" else s!" [{Std.format instr.guard}]"
-    s!"{instr.type}{code_str}{guard_str}"
+    s!"{instr.type}{payload}{guard_str}"
 
 -------------------------------------------------------------------------------
 
diff --git a/Strata/DL/Imperative/CFGToCProverGOTO.lean b/Strata/DL/Imperative/CFGToCProverGOTO.lean
new file mode 100644
index 000000000..03715d5bb
--- /dev/null
+++ b/Strata/DL/Imperative/CFGToCProverGOTO.lean
@@ -0,0 +1,140 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+
+import Strata.DL.Imperative.BasicBlock
+import Strata.DL.Imperative.ToCProverGOTO
+
+/-! # CFG to CProverGOTO Translation
+
+Translates an Imperative dialect CFG (deterministic basic blocks with string
+labels) into a flat array of CProverGOTO instructions.
+
+The existing `Stmt.toGotoInstructions` path translates structured statements
+directly to GOTO instructions, interleaving control-flow lowering (emitting
+conditional jumps, patching forward references) with CBMC-specific concerns
+(source locations, instruction encoding). This module separates those two
+responsibilities: `StructuredToUnstructured.stmtsToCFG` handles the
+control-flow lowering once, producing a backend-agnostic CFG, and this module
+handles only the straightforward mapping from CFG blocks to GOTO instructions.
+
+This separation makes it easier to target additional backends (each only needs
+to consume the CFG) and to reason about the control-flow lowering independently
+of any particular backend.
+
+## Gaps relative to the direct `Stmt.toGotoInstructions` path
+
+The following features are not yet supported via the CFG path, and would need
+to be addressed before it can fully replace the direct path:
+
+- **Source locations on control flow**: `DetTransferCmd` already carries a
+  `MetaData` field, but `StructuredToUnstructured.stmtsToBlocks` currently
+  passes `MetaData.empty` when constructing transfer commands (the metadata
+  from `ite`/`loop`/`block`/`exit` statements is discarded as `_md`).
+  Once `stmtsToBlocks` propagates the metadata, this module will pick it up
+  automatically via `metadataToSourceLoc`.
+- **Loop contracts**: The direct path emits `#spec_loop_invariant` and
+  `#spec_decreases` as named sub-expressions on the backward-edge GOTO
+  instruction (recognized by CBMC's DFCC). In the CFG, invariants are lowered
+  to plain `assert` commands and measures are discarded entirely.
+  To fix: `StructuredToUnstructured.stmtsToBlocks` (the `.loop` case) would
+  need to preserve invariants and measures in the `DetTransferCmd` (or in a
+  side channel), and this module would need to emit them as named
+  sub-expressions on the backward-edge GOTO, mirroring the logic in the
+  `.loop` case of `Stmt.toGotoInstructions` in `ToCProverGOTO.lean`.
+- **`Core.CmdExt.call`**: This translation handles `Imperative.Cmd` only.
+  Core procedure calls (`CmdExt.call`) would need a command translator
+  analogous to `coreStmtsToGoto` in `CoreToGOTOPipeline.lean`.
+-/
+
+namespace Imperative
+
+open CProverGOTO
+open Std (Format format)
+
+/-- Translate a deterministic CFG to CProverGOTO instructions.
+
+    The translation processes blocks in the order they appear in `cfg.blocks`.
+    The entry block must appear first; the function returns an error otherwise.
+    For each block:
+    1. Record the current location number as the block's entry point
+    2. Translate each command using `Cmd.toGotoInstructions`
+    3. Translate the transfer command:
+       - `condGoto c lt lf` → GOTO [!c] lf; GOTO lt (conditional + fallthrough)
+       - `finish` → no instruction (handled by END_FUNCTION in the caller)
+
+    After all blocks are emitted, a second pass patches GOTO targets using the
+    label-to-location map built during the first pass.
+-/
+def detCFGToGotoTransform {P} [G : ToGoto P] [BEq P.Ident]
+    (T : P.TyEnv) (functionName : String)
+    (cfg : CFG String (DetBlock String (Cmd P) P))
+    (loc : Nat := 0)
+    (sourceText : Option String := none)
+    : Except Format (GotoTransform P.TyEnv) := do
+  -- Verify the entry block is listed first so that GOTO execution starts at
+  -- the right location. The caller (e.g., CoreToGOTOPipeline) relies on the
+  -- first instruction being the entry point.
+  match cfg.blocks with
+  | (firstLabel, _) :: _ =>
+    if firstLabel != cfg.entry then
+      throw f!"[detCFGToGotoTransform] Entry label '{cfg.entry}' does not match \
+               first block label '{firstLabel}'. The entry block must be listed first."
+  | [] => pure ()
+  -- First pass: emit instructions and build label→locationNum map
+  let mut trans : GotoTransform P.TyEnv :=
+    { instructions := #[], nextLoc := loc, T := T, sourceText := sourceText }
+  -- Pending GOTO patches: (instruction array index, target label)
+  let mut pendingPatches : Array (Nat × String) := #[]
+  let mut labelMap : Std.HashMap String Nat := {}
+  for (label, block) in cfg.blocks do
+    -- Record this block's entry location
+    labelMap := labelMap.insert label trans.nextLoc
+    -- Emit a LOCATION marker for the block
+    -- NOTE(source-locations): `DetTransferCmd` already carries a `MetaData`
+    -- field, but `StructuredToUnstructured.stmtsToBlocks` currently fills it
+    -- with `MetaData.empty`. Once `stmtsToBlocks` propagates the metadata
+    -- from `ite`/`loop`/`block`/`exit` statements, use `metadataToSourceLoc`
+    -- here (see `Stmt.toGotoInstructions` in ToCProverGOTO.lean for the
+    -- pattern).
+    let srcLoc : SourceLocation := { SourceLocation.nil with function := functionName }
+    trans := emitLabel label srcLoc trans
+    -- Translate each command via the existing Cmd-to-GOTO mapping.
+    -- NOTE: This only handles `Imperative.Cmd`. To support `Core.CmdExt.call`,
+    -- either:
+    --   (a) generalize this function over the command type and accept a
+    --       command translator as a parameter, or
+    --   (b) create a Core-specific wrapper (like `coreStmtsToGoto` in
+    --       `CoreToGOTOPipeline.lean`) that pattern-matches on `CmdExt` and
+    --       emits `FUNCTION_CALL` instructions for `.call`, delegating `.cmd`
+    --       to `Cmd.toGotoInstructions`.
+    for cmd in block.cmds do
+      trans ← Cmd.toGotoInstructions trans.T functionName cmd trans
+    -- Translate the transfer command
+    match block.transfer with
+    | .condGoto cond lt lf _md =>
+      let cond_expr ← G.toGotoExpr cond
+      -- Emit: GOTO [!cond] lf
+      let (trans', falseIdx) := emitCondGoto (Expr.not cond_expr) srcLoc trans
+      trans := trans'
+      pendingPatches := pendingPatches.push (falseIdx, lf)
+      -- Emit: GOTO lt (unconditional)
+      let (trans', trueIdx) := emitUncondGoto srcLoc trans
+      trans := trans'
+      pendingPatches := pendingPatches.push (trueIdx, lt)
+    | .finish _md =>
+      -- No instruction needed; the caller appends END_FUNCTION
+      pure ()
+  -- Second pass: resolve all pending labels, then patch in one call
+  let mut resolvedPatches : List (Nat × Nat) := []
+  for (idx, label) in pendingPatches do
+    match labelMap[label]? with
+    | some targetLoc => resolvedPatches := (idx, targetLoc) :: resolvedPatches
+    | none =>
+      throw f!"[detCFGToGotoTransform] Unresolved label '{label}' referenced \
+               by GOTO at instruction index {idx}."
+  return patchGotoTargets trans resolvedPatches
+
+end Imperative
diff --git a/StrataTest/Backends/CBMC/GOTO/ToCProverGOTO.lean b/StrataTest/Backends/CBMC/GOTO/ToCProverGOTO.lean
index b6848552a..0beed0ab7 100644
--- a/StrataTest/Backends/CBMC/GOTO/ToCProverGOTO.lean
+++ b/StrataTest/Backends/CBMC/GOTO/ToCProverGOTO.lean
@@ -147,11 +147,11 @@ def ExampleStmt1 : List (Imperative.Stmt LExprTP (Imperative.Cmd LExprTP)) :=
     {}]
 
 /--
-info: ok: #[LOCATION skip,
+info: ok: #[LOCATION 0,
  DECL (decl (x : unsignedbv[32])),
  ASSIGN (assign (x : unsignedbv[32]) (10 : unsignedbv[32])),
  ASSIGN (assign (x : unsignedbv[32]) (20 : unsignedbv[32])),
- LOCATION skip]
+ LOCATION 4]
 -/
 #guard_msgs in
 #eval do let ans ← Imperative.Stmts.toGotoTransform Lambda.TEnv.default "test1" ExampleStmt1
@@ -174,12 +174,12 @@ info: ok: #[DECL (decl (x : unsignedbv[32])),
  ASSIGN (assign (x : unsignedbv[32]) (0 : unsignedbv[32])),
  DECL (decl (y : unsignedbv[32])),
  ASSIGN (assign (y : unsignedbv[32]) (0 : unsignedbv[32])),
- GOTO skip [((not(true : bool)) : bool)],
+ GOTO 7 [((not(true : bool)) : bool)],
  ASSIGN (assign (x : unsignedbv[32]) (10 : unsignedbv[32])),
- GOTO skip,
- LOCATION skip,
+ GOTO 9,
+ LOCATION 7,
  ASSIGN (assign (y : unsignedbv[32]) (20 : unsignedbv[32])),
- LOCATION skip]
+ LOCATION 9]
 -/
 #guard_msgs in
 #eval do let ans ← Imperative.Stmts.toGotoTransform Lambda.TEnv.default "test2" ExampleStmt2
@@ -202,11 +202,11 @@ def ExampleStmt3 : List (Imperative.Stmt LExprTP (Imperative.Cmd LExprTP)) :=
 /--
 info: ok: #[DECL (decl (i : unsignedbv[32])),
  ASSIGN (assign (i : unsignedbv[32]) (0 : unsignedbv[32])),
- LOCATION skip,
- GOTO skip [((not(true : bool)) : bool)],
+ LOCATION 2,
+ GOTO 6 [((not(true : bool)) : bool)],
  ASSIGN (assign (i : unsignedbv[32]) (((i : unsignedbv[32]) + (1 : unsignedbv[32])) : unsignedbv[32])),
- GOTO skip,
- LOCATION skip]
+ GOTO 2,
+ LOCATION 6]
 -/
 #guard_msgs in
 #eval do let ans ← Imperative.Stmts.toGotoTransform Lambda.TEnv.default "test3" ExampleStmt3
@@ -226,15 +226,15 @@ def ExampleStmt4 : List (Imperative.Stmt LExprTP (Imperative.Cmd LExprTP)) :=
     {}]
 
 /--
-info: ok: #[LOCATION skip,
+info: ok: #[LOCATION 0,
  DECL (decl (x : unsignedbv[32])),
  ASSIGN (assign (x : unsignedbv[32]) (0 : unsignedbv[32])),
- GOTO skip [((not(true : bool)) : bool)],
+ GOTO 6 [((not(true : bool)) : bool)],
  ASSIGN (assign (x : unsignedbv[32]) (100 : unsignedbv[32])),
- GOTO skip,
- LOCATION skip,
- LOCATION skip,
- LOCATION skip]
+ GOTO 7,
+ LOCATION 6,
+ LOCATION 7,
+ LOCATION 8]
 -/
 #guard_msgs in
 #eval do let ans ← Imperative.Stmts.toGotoTransform Lambda.TEnv.default "test4" ExampleStmt4
@@ -254,11 +254,11 @@ def ExampleStmt5 : List (Imperative.Stmt LExprTP (Imperative.Cmd LExprTP)) :=
 /--
 info: ok: #[DECL (decl (x : unsignedbv[32])),
  ASSIGN (assign (x : unsignedbv[32]) (0 : unsignedbv[32])),
- GOTO skip,
+ GOTO 6,
  ASSIGN (assign (x : unsignedbv[32]) (10 : unsignedbv[32])),
- LOCATION skip,
+ LOCATION 4,
  ASSIGN (assign (x : unsignedbv[32]) (20 : unsignedbv[32])),
- LOCATION skip]
+ LOCATION 6]
 -/
 #guard_msgs in
 #eval do let ans ← Imperative.Stmts.toGotoTransform Lambda.TEnv.default "test5" ExampleStmt5
@@ -291,16 +291,16 @@ info: ok: #[DECL (decl (i : unsignedbv[32])),
  ASSIGN (assign (i : unsignedbv[32]) (0 : unsignedbv[32])),
  DECL (decl (sum : unsignedbv[32])),
  ASSIGN (assign (sum : unsignedbv[32]) (0 : unsignedbv[32])),
- LOCATION skip,
- GOTO skip [((not(true : bool)) : bool)],
- GOTO skip [((not(true : bool)) : bool)],
+ LOCATION 4,
+ GOTO 13 [((not(true : bool)) : bool)],
+ GOTO 9 [((not(true : bool)) : bool)],
  ASSIGN (assign (sum : unsignedbv[32]) (((sum : unsignedbv[32]) + (i : unsignedbv[32])) : unsignedbv[32])),
- GOTO skip,
- LOCATION skip,
- LOCATION skip,
+ GOTO 10,
+ LOCATION 9,
+ LOCATION 10,
  ASSIGN (assign (i : unsignedbv[32]) (((i : unsignedbv[32]) + (1 : unsignedbv[32])) : unsignedbv[32])),
- GOTO skip,
- LOCATION skip]
+ GOTO 4,
+ LOCATION 13]
 -/
 #guard_msgs in
 #eval do let ans ← Imperative.Stmts.toGotoTransform Lambda.TEnv.default "test6" ExampleStmt6
@@ -324,17 +324,17 @@ def ExampleStmt7 : List (Imperative.Stmt LExprTP (Imperative.Cmd LExprTP)) :=
      {}]
 
 /--
-info: ok: #[LOCATION skip,
+info: ok: #[LOCATION 0,
  DECL (decl (x : unsignedbv[32])),
  ASSIGN (assign (x : unsignedbv[32]) (10 : unsignedbv[32])),
- LOCATION skip,
- LOCATION skip,
+ LOCATION 3,
+ LOCATION 4,
  DECL (decl (y : unsignedbv[32])),
  ASSIGN (assign (y : unsignedbv[32]) (20 : unsignedbv[32])),
- LOCATION skip,
- LOCATION skip,
+ LOCATION 7,
+ LOCATION 8,
  ASSIGN (assign (x : unsignedbv[32]) (((x : unsignedbv[32]) + (y : unsignedbv[32])) : unsignedbv[32])),
- LOCATION skip]
+ LOCATION 10]
 -/
 #guard_msgs in
 #eval do let ans ← Imperative.Stmts.toGotoTransform Lambda.TEnv.default "test7" ExampleStmt7
@@ -354,11 +354,11 @@ def ExampleStmt8 : List (Imperative.Stmt LExprTP (Imperative.Cmd LExprTP)) :=
 /--
 info: ok: #[DECL (decl (x : unsignedbv[32])),
  ASSIGN (assign (x : unsignedbv[32]) (0 : unsignedbv[32])),
- GOTO skip [((not(true : bool)) : bool)],
- GOTO skip,
- LOCATION skip,
+ GOTO 4 [((not(true : bool)) : bool)],
+ GOTO 6,
+ LOCATION 4,
  ASSIGN (assign (x : unsignedbv[32]) (100 : unsignedbv[32])),
- LOCATION skip]
+ LOCATION 6]
 -/
 #guard_msgs in
 #eval do let ans ← Imperative.Stmts.toGotoTransform Lambda.TEnv.default "test8" ExampleStmt8
@@ -376,7 +376,7 @@ def ExampleStmt9 : List (Imperative.Stmt LExprTP (Imperative.Cmd LExprTP)) :=
      {}]
 
 /--
-info: ok: #[LOCATION skip, GOTO skip [((not(false : bool)) : bool)], GOTO skip, LOCATION skip]
+info: ok: #[LOCATION 0, GOTO 3 [((not(false : bool)) : bool)], GOTO 0, LOCATION 3]
 -/
 #guard_msgs in
 #eval do let ans ← Imperative.Stmts.toGotoTransform Lambda.TEnv.default "test9" ExampleStmt9
@@ -398,13 +398,13 @@ def ExampleStmt10 : List (Imperative.Stmt LExprTP (Imperative.Cmd LExprTP)) :=
 /--
 info: ok: #[DECL (decl (x : unsignedbv[32])),
  ASSIGN (assign (x : unsignedbv[32]) (5 : unsignedbv[32])),
- GOTO skip [((not(true : bool)) : bool)],
- ASSUME skip,
+ GOTO 7 [((not(true : bool)) : bool)],
+ ASSUME,
  ASSIGN (assign (x : unsignedbv[32]) (10 : unsignedbv[32])),
- ASSERT skip,
- GOTO skip,
- LOCATION skip,
- LOCATION skip]
+ ASSERT,
+ GOTO 8,
+ LOCATION 7,
+ LOCATION 8]
 -/
 #guard_msgs in
 #eval do let ans ← Imperative.Stmts.toGotoTransform Lambda.TEnv.default "test10" ExampleStmt10
@@ -417,7 +417,7 @@ def ExampleCover : List (Imperative.Stmt LExprTP (Imperative.Cmd LExprTP)) :=
   [.cmd (.cover "reachable" (.const { underlying := (), type := mty[bool] } (.boolConst true)) {})]
 
 /--
-info: ok: #[ASSERT skip]
+info: ok: #[ASSERT]
 -/
 #guard_msgs in
 #eval do let ans ← Imperative.Stmts.toGotoTransform Lambda.TEnv.default "testCover" ExampleCover
@@ -458,11 +458,11 @@ def ExampleLoopInvariant : List (Imperative.Stmt LExprTP (Imperative.Cmd LExprTP
 /--
 info: ok: #[DECL (decl (i : unsignedbv[32])),
  ASSIGN (assign (i : unsignedbv[32]) (0 : unsignedbv[32])),
- LOCATION skip,
- GOTO skip [((not(true : bool)) : bool)],
+ LOCATION 2,
+ GOTO 6 [((not(true : bool)) : bool)],
  ASSIGN (assign (i : unsignedbv[32]) (((i : unsignedbv[32]) + (1 : unsignedbv[32])) : unsignedbv[32])),
- GOTO skip,
- LOCATION skip]
+ GOTO 2,
+ LOCATION 6]
 -/
 #guard_msgs in
 #eval do let ans ← Imperative.Stmts.toGotoTransform Lambda.TEnv.default "testInv" ExampleLoopInvariant
diff --git a/StrataTest/DL/Imperative/CFGToCProverGOTO.lean b/StrataTest/DL/Imperative/CFGToCProverGOTO.lean
new file mode 100644
index 000000000..283883379
--- /dev/null
+++ b/StrataTest/DL/Imperative/CFGToCProverGOTO.lean
@@ -0,0 +1,310 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+
+import Strata.DL.Imperative.CFGToCProverGOTO
+import Strata.Transform.StructuredToUnstructured
+import StrataTest.Backends.CBMC.GOTO.LambdaToCProverGOTO
+
+/-! ## Tests for CFG-to-CProverGOTO translation
+
+These tests verify that `detCFGToGotoTransform` correctly translates
+deterministic CFGs into CProverGOTO instruction arrays.
+-/
+
+section
+open Std (ToFormat Format format)
+open Lambda.LTy.Syntax
+
+private abbrev TestParams : Lambda.LExprParams := ⟨Unit, Unit⟩
+
+private abbrev LExprTP : Imperative.PureExpr :=
+   { Ident := TestParams.Identifier,
+     Expr := Lambda.LExprT TestParams.mono,
+     Ty := Lambda.LMonoTy,
+     ExprMetadata := TestParams.Metadata,
+     TyEnv := @Lambda.TEnv TestParams.IDMeta,
+     TyContext := @Lambda.LContext TestParams,
+     EvalEnv := Lambda.LState TestParams
+     EqIdent := inferInstanceAs (DecidableEq TestParams.Identifier) }
+
+private def lookupType (T : LExprTP.TyEnv) (i : LExprTP.Ident) : Except Format CProverGOTO.Ty :=
+  match T.context.types.find? i with
+  | none => .error f!"Cannot find {i} in the type context!"
+  | some ty =>
+    if ty.isMonoType then
+      let ty := ty.toMonoTypeUnsafe
+      ty.toGotoType
+    else .error f!"Poly-type unexpected in the context for {i}: {ty}"
+
+private def updateType (T : LExprTP.TyEnv) (i : LExprTP.Ident) (ty : LExprTP.Ty) : LExprTP.TyEnv :=
+  T.addInNewestContext [(i, (.forAll [] ty))]
+
+instance : Imperative.ToGoto LExprTP where
+  lookupType := lookupType
+  updateType := updateType
+  identToString := (fun i => i.name)
+  toGotoType := Lambda.LMonoTy.toGotoType
+  toGotoExpr := Lambda.LExprT.toGotoExpr
+
+instance : Imperative.HasBool LExprTP where
+  tt := .const { underlying := (), type := mty[bool] } (.boolConst true)
+  ff := .const { underlying := (), type := mty[bool] } (.boolConst false)
+
+instance : Imperative.HasIdent LExprTP where
+  ident s := ⟨s, ()⟩
+
+private abbrev md : Lambda.Typed Unit := { underlying := (), type := mty[bool] }
+
+instance : Imperative.HasFvar LExprTP where
+  mkFvar := (.fvar md · none)
+  getFvar
+  | .fvar _ v _ => some v
+  | _ => none
+
+instance : Imperative.HasIntOrder LExprTP where
+  eq    e1 e2 := .eq md e1 e2
+  lt    e1 e2 := .app md (.app md (.op md ⟨"Int.Lt", ()⟩ none) e1) e2
+  zero        := .intConst md 0
+  intTy       := .tcons "int" []
+
+instance : Imperative.HasNot LExprTP where
+  not e := .app md (.op md ⟨"Bool.Not", ()⟩ none) e
+
+-------------------------------------------------------------------------------
+
+/-! ### Test: simple sequential commands -/
+
+private def seqCmds : List (Imperative.Stmt LExprTP (Imperative.Cmd LExprTP)) :=
+  [.cmd (.init (Lambda.Identifier.mk "x" ()) mty[bv32]
+    (some (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 0))) {}),
+   .cmd (.set (Lambda.Identifier.mk "x" ())
+    (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 42)) {})]
+
+/--
+info: ok: #[LOCATION 0,
+ DECL (decl (x : unsignedbv[32])),
+ ASSIGN (assign (x : unsignedbv[32]) (0 : unsignedbv[32])),
+ ASSIGN (assign (x : unsignedbv[32]) (42 : unsignedbv[32])),
+ GOTO 6 [((not(true : bool)) : bool)],
+ GOTO 6,
+ LOCATION 6]
+-/
+#guard_msgs in
+#eval do
+  let cfg := Imperative.stmtsToCFG seqCmds
+  let ans ← Imperative.detCFGToGotoTransform Lambda.TEnv.default "test" cfg
+  return format ans.instructions
+
+-------------------------------------------------------------------------------
+
+/-! ### Test: if-then-else -/
+
+private def iteCmds : List (Imperative.Stmt LExprTP (Imperative.Cmd LExprTP)) :=
+  [.cmd (.init (Lambda.Identifier.mk "x" ()) mty[bv32]
+    (some (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 0))) {}),
+   .ite
+     (.const { underlying := (), type := mty[bool] } (.boolConst true))
+     [.cmd (.set (Lambda.Identifier.mk "x" ())
+       (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 10)) {})]
+     [.cmd (.set (Lambda.Identifier.mk "x" ())
+       (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 20)) {})]
+     {}]
+
+/--
+info: ok: #[LOCATION 0,
+ DECL (decl (x : unsignedbv[32])),
+ ASSIGN (assign (x : unsignedbv[32]) (0 : unsignedbv[32])),
+ GOTO 9 [((not(true : bool)) : bool)],
+ GOTO 5,
+ LOCATION 5,
+ ASSIGN (assign (x : unsignedbv[32]) (10 : unsignedbv[32])),
+ GOTO 13 [((not(true : bool)) : bool)],
+ GOTO 13,
+ LOCATION 9,
+ ASSIGN (assign (x : unsignedbv[32]) (20 : unsignedbv[32])),
+ GOTO 13 [((not(true : bool)) : bool)],
+ GOTO 13,
+ LOCATION 13]
+-/
+#guard_msgs in
+#eval do
+  let cfg := Imperative.stmtsToCFG iteCmds
+  let ans ← Imperative.detCFGToGotoTransform Lambda.TEnv.default "test" cfg
+  return format ans.instructions
+
+-- Verify all emitted GOTOs have resolved targets
+/--
+info: ok: ()
+-/
+#guard_msgs in
+#eval do
+  let cfg := Imperative.stmtsToCFG iteCmds
+  let ans ← Imperative.detCFGToGotoTransform Lambda.TEnv.default "test" cfg
+  let gotos := ans.instructions.toList.filter (fun (i : CProverGOTO.Instruction) =>
+    i.type == CProverGOTO.InstructionType.GOTO)
+  assert! gotos.all (fun (i : CProverGOTO.Instruction) => i.target.isSome)
+
+-------------------------------------------------------------------------------
+
+/-! ### Test: loop -/
+
+private def addBV32 (op1 op2 : Lambda.LExprT TestParams.mono) : Lambda.LExprT TestParams.mono :=
+  (Lambda.LExpr.app { underlying := (), type := mty[bv32] }
+    (Lambda.LExpr.app { underlying := (), type := mty[bv32 → bv32] }
+      (.op { underlying := (), type := mty[bv32 → bv32 → bv32] }
+        (Lambda.Identifier.mk "Bv32.Add" ()) (some mty[bv32 → bv32 → bv32])) op1)
+    op2)
+
+private def loopCmds : List (Imperative.Stmt LExprTP (Imperative.Cmd LExprTP)) :=
+  [.cmd (.init (Lambda.Identifier.mk "i" ()) mty[bv32]
+    (some (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 0))) {}),
+   .loop
+     (.const { underlying := (), type := mty[bool] } (.boolConst true))
+     none
+     []
+     [.cmd (.set (Lambda.Identifier.mk "i" ()) (addBV32
+       (.fvar { underlying := (), type := mty[bv32] } (Lambda.Identifier.mk "i" ()) (some mty[bv32]))
+       (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 1))) {})]
+     {}]
+
+/--
+info: ok: #[LOCATION 0,
+ DECL (decl (i : unsignedbv[32])),
+ ASSIGN (assign (i : unsignedbv[32]) (0 : unsignedbv[32])),
+ GOTO 5 [((not(true : bool)) : bool)],
+ GOTO 5,
+ LOCATION 5,
+ GOTO 12 [((not(true : bool)) : bool)],
+ GOTO 8,
+ LOCATION 8,
+ ASSIGN (assign (i : unsignedbv[32]) (((i : unsignedbv[32]) + (1 : unsignedbv[32])) : unsignedbv[32])),
+ GOTO 5 [((not(true : bool)) : bool)],
+ GOTO 5,
+ LOCATION 12]
+-/
+#guard_msgs in
+#eval do
+  let cfg := Imperative.stmtsToCFG loopCmds
+  let ans ← Imperative.detCFGToGotoTransform Lambda.TEnv.default "test" cfg
+  return format ans.instructions
+
+-- Verify the loop back-edge: there should be a GOTO targeting the loop entry
+/--
+info: ok: ()
+-/
+#guard_msgs in
+#eval do
+  let cfg := Imperative.stmtsToCFG loopCmds
+  let ans ← Imperative.detCFGToGotoTransform Lambda.TEnv.default "test" cfg
+  let gotos := ans.instructions.toList.filter (fun (i : CProverGOTO.Instruction) =>
+    i.type == CProverGOTO.InstructionType.GOTO && i.target.isSome)
+  -- At least one GOTO should jump backwards (target < its own locationNum)
+  assert! gotos.any (fun (i : CProverGOTO.Instruction) =>
+    i.target.any (· < i.locationNum))
+
+-------------------------------------------------------------------------------
+
+/-! ### Test: empty CFG (single finish block) -/
+
+private def emptyCmds : List (Imperative.Stmt LExprTP (Imperative.Cmd LExprTP)) := []
+
+/--
+info: ok: #[LOCATION 0]
+-/
+#guard_msgs in
+#eval do
+  let cfg := Imperative.stmtsToCFG emptyCmds
+  let ans ← Imperative.detCFGToGotoTransform Lambda.TEnv.default "test" cfg
+  return format ans.instructions
+
+-------------------------------------------------------------------------------
+
+/-! ### Test: assert and assume commands -/
+
+private def assertAssumeCmds : List (Imperative.Stmt LExprTP (Imperative.Cmd LExprTP)) :=
+  [.cmd (.assume "pre" (.const { underlying := (), type := mty[bool] } (.boolConst true)) {}),
+   .cmd (.assert "post" (.const { underlying := (), type := mty[bool] } (.boolConst true)) {})]
+
+/--
+info: ok: #[LOCATION 0, ASSUME, ASSERT, GOTO 5 [((not(true : bool)) : bool)], GOTO 5, LOCATION 5]
+-/
+#guard_msgs in
+#eval do
+  let cfg := Imperative.stmtsToCFG assertAssumeCmds
+  let ans ← Imperative.detCFGToGotoTransform Lambda.TEnv.default "test" cfg
+  return format ans.instructions
+
+-------------------------------------------------------------------------------
+
+/-! ### Test: havoc command -/
+
+private def havocCmds : List (Imperative.Stmt LExprTP (Imperative.Cmd LExprTP)) :=
+  [.cmd (.init (Lambda.Identifier.mk "x" ()) mty[bv32]
+    (some (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 0))) {}),
+   .cmd (.havoc (Lambda.Identifier.mk "x" ()) {})]
+
+/--
+info: ok: #[LOCATION 0,
+ DECL (decl (x : unsignedbv[32])),
+ ASSIGN (assign (x : unsignedbv[32]) (0 : unsignedbv[32])),
+ ASSIGN (assign (x : unsignedbv[32]) (nondet : unsignedbv[32])),
+ GOTO 6 [((not(true : bool)) : bool)],
+ GOTO 6,
+ LOCATION 6]
+-/
+#guard_msgs in
+#eval do
+  let cfg := Imperative.stmtsToCFG havocCmds
+  let ans ← Imperative.detCFGToGotoTransform Lambda.TEnv.default "test" cfg
+  return format ans.instructions
+
+-------------------------------------------------------------------------------
+
+/-! ### Test: entry block must be listed first -/
+
+#eval do
+  -- Construct a CFG where entry label doesn't match the first block
+  let cfg : Imperative.CFG String (Imperative.DetBlock String (Imperative.Cmd LExprTP) LExprTP) :=
+    { entry := "second",
+      blocks := [("first", { cmds := [], transfer := .finish }),
+                 ("second", { cmds := [], transfer := .finish })] }
+  match Imperative.detCFGToGotoTransform Lambda.TEnv.default "test" cfg with
+  | .error e => assert! (s!"{e}".splitOn "Entry label").length > 1
+  | .ok _ => assert! false
+
+-------------------------------------------------------------------------------
+
+/-! ### Test: all GOTOs have resolved targets (sequential) -/
+
+/--
+info: ok: ()
+-/
+#guard_msgs in
+#eval do
+  let cfg := Imperative.stmtsToCFG seqCmds
+  let ans ← Imperative.detCFGToGotoTransform Lambda.TEnv.default "test" cfg
+  let gotos := ans.instructions.toList.filter (fun (i : CProverGOTO.Instruction) =>
+    i.type == CProverGOTO.InstructionType.GOTO)
+  assert! gotos.all (fun (i : CProverGOTO.Instruction) => i.target.isSome)
+
+-------------------------------------------------------------------------------
+
+/-! ### Test: unresolved label produces an error -/
+
+#eval do
+  let trueExpr : LExprTP.Expr :=
+    .const { underlying := (), type := mty[bool] } (.boolConst true)
+  let blk : Imperative.DetBlock String (Imperative.Cmd LExprTP) LExprTP :=
+    { cmds := [], transfer := .condGoto trueExpr "missing_label" "also_missing" }
+  let cfg : Imperative.CFG String (Imperative.DetBlock String (Imperative.Cmd LExprTP) LExprTP) :=
+    { entry := "entry", blocks := [("entry", blk)] }
+  match Imperative.detCFGToGotoTransform Lambda.TEnv.default "test" cfg with
+  | .error e => assert! (s!"{e}".splitOn "Unresolved label").length > 1
+  | .ok _ => assert! false
+
+-------------------------------------------------------------------------------
+
+end