diff --git a/Strata/DL/Imperative/ToCProverGOTO.lean b/Strata/DL/Imperative/ToCProverGOTO.lean
index 675c7f1dc..807eabdfe 100644
--- a/Strata/DL/Imperative/ToCProverGOTO.lean
+++ b/Strata/DL/Imperative/ToCProverGOTO.lean
@@ -15,6 +15,8 @@ open Std (ToFormat Format format)
 
 namespace Imperative
 
+open CProverGOTO
+
 class ToGoto (P : PureExpr) where
   -- NOTE: `lookupType` and `updateType` correspond to the functions `lookup`
   -- and `update` in the `Imperative.TypeContext` class.
@@ -129,3 +131,212 @@ def Cmds.toGotoTransform {P} [G: ToGoto P] (T : P.TyEnv)
   go { instructions := #[], nextLoc := loc, T := T } cs
 
 -------------------------------------------------------------------------------
+
+/-! ## Imperative's Statements to CProverGOTO's Instructions -/
+
+/-
+Mutual recursion between Stmt.toGotoInstructions and Block.toGotoInstructions:
+Statements can contain blocks (e.g., in .ite and .loop), and blocks contain statements.
+This mutual dependency requires both functions to be defined in a mutual block.
+-/
+mutual
+
+/--
+Convert an `Imperative.Stmt` to one or more `CProverGOTO.Instruction`s.
+
+This function handles all statement types including control flow constructs like
+blocks, conditionals, and loops.
+-/
+def Stmt.toGotoInstructions {P} [G: ToGoto P]
+    (T : P.TyEnv) (functionName : String) (s : Stmt P (Cmd P)) (trans : GotoTransform P.TyEnv) :
+    Except Format (GotoTransform P.TyEnv) := do
+  match s with
+  | .cmd c =>
+    -- Atomic command - delegate to existing Cmd transformation
+    Cmd.toGotoInstructions trans.T functionName c trans
+
+  | .block label body _md =>
+    -- Block with label - emit a LOCATION instruction with the label, then process body
+    let label_inst : Instruction :=
+      { type := .LOCATION,
+        locationNum := trans.nextLoc,
+        sourceLoc := { SourceLocation.nil with function := functionName },
+        labels := [label],
+        code := Code.skip }
+    let trans := { trans with
+                    instructions := trans.instructions.push label_inst,
+                    nextLoc := trans.nextLoc + 1 }
+    Block.toGotoInstructions trans.T functionName body trans
+
+  | .ite cond thenb elseb _md =>
+    /-
+    Conditional: if cond then thenb else elseb
+    Structure:
+      GOTO [!cond] else_label    ; jump to else branch if condition is false
+      <then branch instructions>
+      GOTO end_label             ; skip else branch
+      LOCATION else_label        ; else branch starts here
+      <else branch instructions>
+      LOCATION end_label         ; after conditional
+    -/
+    let else_label := s!"else_{trans.nextLoc}"
+    let end_label := s!"end_if_{trans.nextLoc}"
+
+    -- Emit conditional GOTO to else branch
+    let cond_expr ← G.toGotoExpr cond
+    let neg_cond := Expr.not cond_expr
+    let goto_else_inst : Instruction :=
+      { type := .GOTO, locationNum := trans.nextLoc,
+        sourceLoc := { SourceLocation.nil with function := functionName },
+        guard := neg_cond, target := .none }
+    let trans := { trans with
+                    instructions := trans.instructions.push goto_else_inst,
+                    nextLoc := trans.nextLoc + 1 }
+    let goto_else_loc := trans.nextLoc - 1
+
+    -- Process then branch
+    let trans ← Block.toGotoInstructions trans.T functionName thenb trans
+
+    -- Emit unconditional GOTO to end
+    let goto_end_inst : Instruction :=
+      { type := .GOTO, locationNum := trans.nextLoc,
+        sourceLoc := { SourceLocation.nil with function := functionName },
+        guard := Expr.true, target := .none }
+    let trans := { trans with
+                    instructions := trans.instructions.push goto_end_inst,
+                    nextLoc := trans.nextLoc + 1 }
+    let goto_end_loc := trans.nextLoc - 1
+
+    -- Emit else branch label
+    let else_loc := trans.nextLoc
+    let else_label_inst : Instruction :=
+      { type := .LOCATION, locationNum := else_loc,
+        sourceLoc := { SourceLocation.nil with function := functionName },
+        labels := [else_label], code := Code.skip }
+    let trans := { trans with
+                    instructions := trans.instructions.push else_label_inst,
+                    nextLoc := trans.nextLoc + 1 }
+
+    -- Process else branch
+    let trans ← Block.toGotoInstructions trans.T functionName elseb trans
+
+    -- Emit end label
+    let end_loc := trans.nextLoc
+    let end_label_inst : Instruction :=
+      { type := .LOCATION, locationNum := end_loc,
+        sourceLoc := { SourceLocation.nil with function := functionName },
+        labels := [end_label], code := Code.skip }
+    let trans := { trans with
+                    instructions := trans.instructions.push end_label_inst,
+                    nextLoc := trans.nextLoc + 1 }
+
+    -- Patch GOTO targets
+    let insts := trans.instructions
+    let insts := insts.set! goto_else_loc
+      { insts[goto_else_loc]! with target := .some else_loc }
+    let insts := insts.set! goto_end_loc
+      { insts[goto_end_loc]! with target := .some end_loc }
+    return { trans with instructions := insts }
+
+  | .loop guard _measure _invariant body _md =>
+    /-
+    Loop: while guard do body
+    Structure:
+      LOCATION loop_start        ; loop entry point
+      GOTO [!guard] loop_end     ; exit loop if guard false
+      <body instructions>
+      GOTO loop_start            ; back edge
+      LOCATION loop_end          ; after loop
+    -/
+    let loop_start_label := s!"loop_start_{trans.nextLoc}"
+    let loop_end_label := s!"loop_end_{trans.nextLoc}"
+
+    -- Emit loop start label
+    let loop_start_loc := trans.nextLoc
+    let loop_start_inst : Instruction :=
+      { type := .LOCATION, locationNum := loop_start_loc,
+        sourceLoc := { SourceLocation.nil with function := functionName },
+        labels := [loop_start_label], code := Code.skip }
+    let trans := { trans with
+                    instructions := trans.instructions.push loop_start_inst,
+                    nextLoc := trans.nextLoc + 1 }
+
+    -- Emit conditional GOTO to exit loop
+    let guard_expr ← G.toGotoExpr guard
+    let neg_guard := Expr.not guard_expr
+    let goto_end_inst : Instruction :=
+      { type := .GOTO, locationNum := trans.nextLoc,
+        sourceLoc := { SourceLocation.nil with function := functionName },
+        guard := neg_guard, target := .none }
+    let trans := { trans with
+                    instructions := trans.instructions.push goto_end_inst,
+                    nextLoc := trans.nextLoc + 1 }
+    let goto_end_loc := trans.nextLoc - 1
+
+    -- Process loop body
+    let trans ← Block.toGotoInstructions trans.T functionName body trans
+
+    -- Emit unconditional GOTO back to loop start
+    let goto_start_inst : Instruction :=
+      { type := .GOTO, locationNum := trans.nextLoc,
+        sourceLoc := { SourceLocation.nil with function := functionName },
+        guard := Expr.true, target := .some loop_start_loc }
+    let trans := { trans with
+                    instructions := trans.instructions.push goto_start_inst,
+                    nextLoc := trans.nextLoc + 1 }
+
+    -- Emit loop end label
+    let loop_end_loc := trans.nextLoc
+    let loop_end_inst : Instruction :=
+      { type := .LOCATION, locationNum := loop_end_loc,
+        sourceLoc := { SourceLocation.nil with function := functionName },
+        labels := [loop_end_label], code := Code.skip }
+    let trans := { trans with
+                    instructions := trans.instructions.push loop_end_inst,
+                    nextLoc := trans.nextLoc + 1 }
+
+    -- Patch GOTO to loop end
+    let insts := trans.instructions
+    let insts := insts.set! goto_end_loc
+      { insts[goto_end_loc]! with target := .some loop_end_loc }
+    return { trans with instructions := insts }
+
+  | .goto label _md =>
+    -- Goto statement - creates an incomplete GOTO (target will be resolved later)
+    -- Note: In a full implementation, we would need a second pass to resolve labels
+    let goto_inst : Instruction :=
+      { type := .INCOMPLETE_GOTO,
+        locationNum := trans.nextLoc,
+        sourceLoc := { SourceLocation.nil with function := functionName },
+        code := Code.goto label }
+    return { trans with
+              instructions := trans.instructions.push goto_inst,
+              nextLoc := trans.nextLoc + 1 }
+termination_by Stmt.sizeOf s
+decreasing_by all_goals simp [*] at * <;> omega
+
+/--
+Convert a block (list of statements) to GOTO instructions.
+-/
+def Block.toGotoInstructions {P} [G: ToGoto P]
+    (T : P.TyEnv) (functionName : String) (stmts : Block P (Cmd P)) (trans : GotoTransform P.TyEnv) :
+    Except Format (GotoTransform P.TyEnv) := do
+  match stmts with
+  | [] => return trans
+  | s :: rest => do
+    let new_trans ← Stmt.toGotoInstructions T functionName s trans
+    Block.toGotoInstructions T functionName rest new_trans
+termination_by Block.sizeOf stmts
+decreasing_by all_goals simp [*] at * <;> omega
+end
+
+/--
+Transform a block of statements to a GotoTransform structure.
+This is the main entry point for statement transformation.
+-/
+def Stmts.toGotoTransform {P} [G: ToGoto P] (T : P.TyEnv)
+    (functionName : String) (stmts : List (Stmt P (Cmd P))) (loc : Nat := 0) :
+    Except Format (GotoTransform P.TyEnv) := do
+  Block.toGotoInstructions T functionName stmts { instructions := #[], nextLoc := loc, T := T }
+
+-------------------------------------------------------------------------------
diff --git a/StrataTest/Backends/CBMC/ToCProverGOTO.lean b/StrataTest/Backends/CBMC/ToCProverGOTO.lean
index 4ba14958f..470b9ea90 100644
--- a/StrataTest/Backends/CBMC/ToCProverGOTO.lean
+++ b/StrataTest/Backends/CBMC/ToCProverGOTO.lean
@@ -120,4 +120,273 @@ info: ok: #[DECL (decl (x : unsignedbv[32])),
 
 -------------------------------------------------------------------------------
 
+/-! ## Tests for Statement Transformation -/
+
+/-- Test block statement transformation -/
+def ExampleStmt1 : List (Imperative.Stmt LExprTP (Imperative.Cmd LExprTP)) :=
+  [.block "test_block"
+    [.cmd (.init (Lambda.Identifier.mk "x" ()) mty[bv32] (.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 skip,
+ DECL (decl (x : unsignedbv[32])),
+ ASSIGN (assign (x : unsignedbv[32]) (10 : unsignedbv[32])),
+ ASSIGN (assign (x : unsignedbv[32]) (20 : unsignedbv[32]))]
+-/
+#guard_msgs in
+#eval do let ans ← Imperative.Stmts.toGotoTransform Lambda.TEnv.default "test1" ExampleStmt1
+          return format ans.instructions
+
+-------------------------------------------------------------------------------
+
+/-- Test if-then-else (ite) statement transformation -/
+def ExampleStmt2 : List (Imperative.Stmt LExprTP (Imperative.Cmd LExprTP)) :=
+  [.cmd (.init (Lambda.Identifier.mk "x" ()) mty[bv32] (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 0))),
+   .cmd (.init (Lambda.Identifier.mk "y" ()) mty[bv32] (.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 "y" ()) (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 20)))]
+     {}]
+
+/--
+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)],
+ ASSIGN (assign (x : unsignedbv[32]) (10 : unsignedbv[32])),
+ GOTO skip,
+ LOCATION skip,
+ ASSIGN (assign (y : unsignedbv[32]) (20 : unsignedbv[32])),
+ LOCATION skip]
+-/
+#guard_msgs in
+#eval do let ans ← Imperative.Stmts.toGotoTransform Lambda.TEnv.default "test2" ExampleStmt2
+          return format ans.instructions
+
+-------------------------------------------------------------------------------
+
+/-- Test loop statement transformation -/
+def ExampleStmt3 : List (Imperative.Stmt LExprTP (Imperative.Cmd LExprTP)) :=
+  [.cmd (.init (Lambda.Identifier.mk "i" ()) mty[bv32] (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 0))),
+   .loop
+     (.const { underlying := (), type := mty[bool] } (.boolConst true))
+     none
+     none
+     [.cmd (.set (Lambda.Identifier.mk "i" ()) (addBV32LExpr
+       (.fvar { underlying := (), type := mty[bv32] } (Lambda.Identifier.mk "i" ()) (some mty[bv32]))
+       (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 1))))]
+     {}]
+
+/--
+info: ok: #[DECL (decl (i : unsignedbv[32])),
+ ASSIGN (assign (i : unsignedbv[32]) (0 : unsignedbv[32])),
+ LOCATION skip,
+ GOTO skip [((not(true : bool)) : bool)],
+ ASSIGN (assign (i : unsignedbv[32]) (((i : unsignedbv[32]) + (1 : unsignedbv[32])) : unsignedbv[32])),
+ GOTO skip,
+ LOCATION skip]
+-/
+#guard_msgs in
+#eval do let ans ← Imperative.Stmts.toGotoTransform Lambda.TEnv.default "test3" ExampleStmt3
+          return format ans.instructions
+
+-------------------------------------------------------------------------------
+
+/-- Test nested control flow: if inside block -/
+def ExampleStmt4 : List (Imperative.Stmt LExprTP (Imperative.Cmd LExprTP)) :=
+  [.block "outer"
+    [.cmd (.init (Lambda.Identifier.mk "x" ()) mty[bv32] (.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 100)))]
+       []
+       {}]
+    {}]
+
+/--
+info: ok: #[LOCATION skip,
+ DECL (decl (x : unsignedbv[32])),
+ ASSIGN (assign (x : unsignedbv[32]) (0 : unsignedbv[32])),
+ GOTO skip [((not(true : bool)) : bool)],
+ ASSIGN (assign (x : unsignedbv[32]) (100 : unsignedbv[32])),
+ GOTO skip,
+ LOCATION skip,
+ LOCATION skip]
+-/
+#guard_msgs in
+#eval do let ans ← Imperative.Stmts.toGotoTransform Lambda.TEnv.default "test4" ExampleStmt4
+          return format ans.instructions
+
+-------------------------------------------------------------------------------
+
+/-- Test goto statement transformation -/
+def ExampleStmt5 : List (Imperative.Stmt LExprTP (Imperative.Cmd LExprTP)) :=
+  [.cmd (.init (Lambda.Identifier.mk "x" ()) mty[bv32] (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 0))),
+   .goto "target_label" {},
+   .cmd (.set (Lambda.Identifier.mk "x" ()) (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 10))),
+   .block "target_label"
+     [.cmd (.set (Lambda.Identifier.mk "x" ()) (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 20)))]
+     {}]
+
+/--
+info: ok: #[DECL (decl (x : unsignedbv[32])),
+ ASSIGN (assign (x : unsignedbv[32]) (0 : unsignedbv[32])),
+ INCOMPLETE_GOTO goto target_label,
+ ASSIGN (assign (x : unsignedbv[32]) (10 : unsignedbv[32])),
+ LOCATION skip,
+ ASSIGN (assign (x : unsignedbv[32]) (20 : unsignedbv[32]))]
+-/
+#guard_msgs in
+#eval do let ans ← Imperative.Stmts.toGotoTransform Lambda.TEnv.default "test5" ExampleStmt5
+          return format ans.instructions
+
+-------------------------------------------------------------------------------
+
+/-- Test complex nested control flow: loop with if inside -/
+def ExampleStmt6 : List (Imperative.Stmt LExprTP (Imperative.Cmd LExprTP)) :=
+  [.cmd (.init (Lambda.Identifier.mk "i" ()) mty[bv32] (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 0))),
+   .cmd (.init (Lambda.Identifier.mk "sum" ()) mty[bv32] (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 0))),
+   .loop
+     (.const { underlying := (), type := mty[bool] } (.boolConst true))
+     none
+     none
+     [.ite
+       (.const { underlying := (), type := mty[bool] } (.boolConst true))
+       [.cmd (.set (Lambda.Identifier.mk "sum" ()) (addBV32LExpr
+         (.fvar { underlying := (), type := mty[bv32] } (Lambda.Identifier.mk "sum" ()) (some mty[bv32]))
+         (.fvar { underlying := (), type := mty[bv32] } (Lambda.Identifier.mk "i" ()) (some mty[bv32]))))]
+       []
+       {},
+      .cmd (.set (Lambda.Identifier.mk "i" ()) (addBV32LExpr
+        (.fvar { underlying := (), type := mty[bv32] } (Lambda.Identifier.mk "i" ()) (some mty[bv32]))
+        (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 1))))]
+     {}]
+
+/--
+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)],
+ ASSIGN (assign (sum : unsignedbv[32]) (((sum : unsignedbv[32]) + (i : unsignedbv[32])) : unsignedbv[32])),
+ GOTO skip,
+ LOCATION skip,
+ LOCATION skip,
+ ASSIGN (assign (i : unsignedbv[32]) (((i : unsignedbv[32]) + (1 : unsignedbv[32])) : unsignedbv[32])),
+ GOTO skip,
+ LOCATION skip]
+-/
+#guard_msgs in
+#eval do let ans ← Imperative.Stmts.toGotoTransform Lambda.TEnv.default "test6" ExampleStmt6
+          return format ans.instructions
+
+-------------------------------------------------------------------------------
+
+/-- Test multiple blocks in sequence -/
+def ExampleStmt7 : List (Imperative.Stmt LExprTP (Imperative.Cmd LExprTP)) :=
+  [.block "block1"
+     [.cmd (.init (Lambda.Identifier.mk "x" ()) mty[bv32] (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 10)))]
+     {},
+   .block "block2"
+     [.cmd (.init (Lambda.Identifier.mk "y" ()) mty[bv32] (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 20)))]
+     {},
+   .block "block3"
+     [.cmd (.set (Lambda.Identifier.mk "x" ())
+       (addBV32LExpr
+         (.fvar { underlying := (), type := mty[bv32] } (Lambda.Identifier.mk "x" ()) (some mty[bv32]))
+         (.fvar { underlying := (), type := mty[bv32] } (Lambda.Identifier.mk "y" ()) (some mty[bv32]))))]
+     {}]
+
+/--
+info: ok: #[LOCATION skip,
+ DECL (decl (x : unsignedbv[32])),
+ ASSIGN (assign (x : unsignedbv[32]) (10 : unsignedbv[32])),
+ LOCATION skip,
+ DECL (decl (y : unsignedbv[32])),
+ ASSIGN (assign (y : unsignedbv[32]) (20 : unsignedbv[32])),
+ LOCATION skip,
+ ASSIGN (assign (x : unsignedbv[32]) (((x : unsignedbv[32]) + (y : unsignedbv[32])) : unsignedbv[32]))]
+-/
+#guard_msgs in
+#eval do let ans ← Imperative.Stmts.toGotoTransform Lambda.TEnv.default "test7" ExampleStmt7
+          return format ans.instructions
+
+-------------------------------------------------------------------------------
+
+/-- Test empty branches in if-then-else -/
+def ExampleStmt8 : List (Imperative.Stmt LExprTP (Imperative.Cmd LExprTP)) :=
+  [.cmd (.init (Lambda.Identifier.mk "x" ()) mty[bv32] (.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 100)))]
+     {}]
+
+/--
+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,
+ ASSIGN (assign (x : unsignedbv[32]) (100 : unsignedbv[32])),
+ LOCATION skip]
+-/
+#guard_msgs in
+#eval do let ans ← Imperative.Stmts.toGotoTransform Lambda.TEnv.default "test8" ExampleStmt8
+          return format ans.instructions
+
+-------------------------------------------------------------------------------
+
+/-- Test loop with empty body -/
+def ExampleStmt9 : List (Imperative.Stmt LExprTP (Imperative.Cmd LExprTP)) :=
+  [.loop
+     (.const { underlying := (), type := mty[bool] } (.boolConst false))
+     none
+     none
+     []
+     {}]
+
+/--
+info: ok: #[LOCATION skip, GOTO skip [((not(false : bool)) : bool)], GOTO skip, LOCATION skip]
+-/
+#guard_msgs in
+#eval do let ans ← Imperative.Stmts.toGotoTransform Lambda.TEnv.default "test9" ExampleStmt9
+          return format ans.instructions
+
+-------------------------------------------------------------------------------
+
+/-- Test assertions and assumptions within control flow -/
+def ExampleStmt10 : List (Imperative.Stmt LExprTP (Imperative.Cmd LExprTP)) :=
+  [.cmd (.init (Lambda.Identifier.mk "x" ()) mty[bv32] (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 5))),
+   .ite
+     (.const { underlying := (), type := mty[bool] } (.boolConst true))
+     [.cmd (.assume "precond" (.const { underlying := (), type := mty[bool] } (.boolConst true))),
+      .cmd (.set (Lambda.Identifier.mk "x" ()) (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 10))),
+      .cmd (.assert "postcond" (.const { underlying := (), type := mty[bool] } (.boolConst true)))]
+     []
+     {}]
+
+/--
+info: ok: #[DECL (decl (x : unsignedbv[32])),
+ ASSIGN (assign (x : unsignedbv[32]) (5 : unsignedbv[32])),
+ GOTO skip [((not(true : bool)) : bool)],
+ ASSUME skip,
+ ASSIGN (assign (x : unsignedbv[32]) (10 : unsignedbv[32])),
+ ASSERT skip,
+ GOTO skip,
+ LOCATION skip,
+ LOCATION skip]
+-/
+#guard_msgs in
+#eval do let ans ← Imperative.Stmts.toGotoTransform Lambda.TEnv.default "test10" ExampleStmt10
+          return format ans.instructions
+
+-------------------------------------------------------------------------------
+
 end