diff --git a/compiler/rustc_codegen_llvm/src/gotoc/assumptions.rs b/compiler/rustc_codegen_llvm/src/gotoc/assumptions.rs
index 63a06b7f6451..c4001d3ede81 100644
--- a/compiler/rustc_codegen_llvm/src/gotoc/assumptions.rs
+++ b/compiler/rustc_codegen_llvm/src/gotoc/assumptions.rs
@@ -54,7 +54,7 @@ impl<'tcx> GotocCtx<'tcx> {
                     .dereference()
                     .ge(Expr::int_constant(below, Type::signed_int(32)))
                     .and(ptr.dereference().le(Expr::int_constant(above, Type::signed_int(32))))
-                    .ret();
+                    .ret(Location::none());
                 body.push(exp)
             })
         });
@@ -69,7 +69,7 @@ impl<'tcx> GotocCtx<'tcx> {
                     .dereference()
                     .eq(Expr::c_true())
                     .or(ptr.dereference().eq(Expr::c_false()))
-                    .ret();
+                    .ret(Location::none());
                 body.push(exp)
             })
         });
@@ -221,22 +221,29 @@ impl<'tcx> GotocCtx<'tcx> {
                 //CHECKME: why is this 2?
                 let idx = tcx.gen_function_local_variable(2, &fname, Type::size_t()).to_expr();
                 body.push(Stmt::decl(idx.clone(), Some(Type::size_t().zero()), Location::none()));
-                let lbody = Stmt::block(vec![
-                    data.clone()
-                        .neq(data.typ().null())
-                        .implies(f.call(vec![data.plus(idx.clone())]))
-                        .not()
-                        .if_then_else(Expr::bool_false().ret(), None, Location::none()),
-                ]);
+                let lbody = Stmt::block(
+                    vec![
+                        data.clone()
+                            .neq(data.typ().null())
+                            .implies(f.call(vec![data.plus(idx.clone())]))
+                            .not()
+                            .if_then_else(
+                                Expr::bool_false().ret(Location::none()),
+                                None,
+                                Location::none(),
+                            ),
+                    ],
+                    Location::none(),
+                );
                 body.push(Stmt::for_loop(
                     Stmt::skip(Location::none()),
                     idx.clone().lt(len),
-                    idx.postincr().as_stmt(),
+                    idx.postincr().as_stmt(Location::none()),
                     lbody,
                     Location::none(),
                 ));
             }
-            body.push(fold_invariants(invariants).ret());
+            body.push(fold_invariants(invariants).ret(Location::none()));
         })
     }
 
@@ -260,7 +267,7 @@ impl<'tcx> GotocCtx<'tcx> {
             if let Some(f) = f {
                 invarints.push(x.clone().neq(x.typ().null()).implies(f.call(vec![x])));
             }
-            body.push(fold_invariants(invarints).ret());
+            body.push(fold_invariants(invarints).ret(Location::none()));
         })
     }
 
@@ -296,7 +303,7 @@ impl<'tcx> GotocCtx<'tcx> {
     ) -> Symbol {
         self.codegen_assumption_genfunc(fname, t, |tcx, ptr, body| {
             let invariants = tcx.codegen_assumption_struct_invariant(ptr, variant, subst);
-            body.push(fold_invariants(invariants).ret());
+            body.push(fold_invariants(invariants).ret(Location::none()));
         })
     }
 
@@ -336,7 +343,7 @@ impl<'tcx> GotocCtx<'tcx> {
     ) -> Symbol {
         self.codegen_assumption_genfunc(fname, t, |tcx, ptr, body| {
             let invariants = tcx.codegen_assumption_struct_invariant(ptr, variant, subst);
-            body.push(fold_invariants(invariants).ret());
+            body.push(fold_invariants(invariants).ret(Location::none()));
         })
     }
 
@@ -382,7 +389,7 @@ impl<'tcx> GotocCtx<'tcx> {
 
             let data_invar = tcx.codegen_assumption_struct_invariant(ptr, variant, subst);
             invariants.push(fold_invariants(data_invar));
-            body.push(fold_invariants_or(invariants).ret());
+            body.push(fold_invariants_or(invariants).ret(Location::none()));
         })
     }
 
@@ -486,7 +493,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 }
             }
 
-            body.push(fold_invariants(invariants).ret());
+            body.push(fold_invariants(invariants).ret(Location::none()));
         })
     }
 
@@ -510,25 +517,29 @@ impl<'tcx> GotocCtx<'tcx> {
                 let idx = tcx.gen_function_local_variable(2, &fname, Type::size_t());
                 body.push(Stmt::decl(idx.to_expr(), Some(Type::size_t().zero()), Location::none()));
                 let idxe = idx.to_expr();
-                let lbody = Stmt::block(vec![
-                    f.call(vec![
-                        tcx.codegen_idx_array(ptr.clone().dereference(), idxe.clone()).address_of(),
-                    ])
-                    .not()
-                    .if_then_else(
-                        Expr::bool_false().ret(),
-                        None,
-                        Location::none(),
-                    ),
-                ]);
+                let lbody = Stmt::block(
+                    vec![
+                        f.call(vec![
+                            tcx.codegen_idx_array(ptr.clone().dereference(), idxe.clone())
+                                .address_of(),
+                        ])
+                        .not()
+                        .if_then_else(
+                            Expr::bool_false().ret(Location::none()),
+                            None,
+                            Location::none(),
+                        ),
+                    ],
+                    Location::none(),
+                );
                 body.push(Stmt::for_loop(
                     Stmt::skip(Location::none()),
                     idxe.clone().lt(tcx.codegen_const(c, None)),
-                    idxe.postincr().as_stmt(),
+                    idxe.postincr().as_stmt(Location::none()),
                     lbody,
                     Location::none(),
                 ));
-                body.push(Expr::bool_true().ret());
+                body.push(Expr::bool_true().ret(Location::none()));
             }
         })
     }
@@ -553,7 +564,7 @@ impl<'tcx> GotocCtx<'tcx> {
                     invariants.push(f.call(vec![field]));
                 }
             }
-            body.push(fold_invariants(invariants).ret());
+            body.push(fold_invariants(invariants).ret(Location::none()));
         })
     }
 
@@ -570,7 +581,7 @@ impl<'tcx> GotocCtx<'tcx> {
         let mut stmts = vec![];
         //let mut body = Stmt::block(vec![]);
         f(self, ptr, &mut stmts);
-        let body = Stmt::block(stmts);
+        let body = Stmt::block(stmts, Location::none());
         Symbol::function(
             fname,
             Type::code(vec![var.to_function_parameter()], Type::bool()),
diff --git a/compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/expr.rs b/compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/expr.rs
index ee3b51798158..66519bd0e020 100644
--- a/compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/expr.rs
+++ b/compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/expr.rs
@@ -1172,14 +1172,12 @@ impl Expr {
 /// The statement constructors do typechecking, so we don't redundantly do that here.
 impl Expr {
     /// `self;`
-    pub fn as_stmt(self) -> Stmt {
-        let loc = self.location.clone();
+    pub fn as_stmt(self, loc: Location) -> Stmt {
         Stmt::code_expression(self, loc)
     }
 
     /// `self = rhs;`
-    pub fn assign(self, rhs: Expr) -> Stmt {
-        let loc = rhs.location.clone();
+    pub fn assign(self, rhs: Expr, loc: Location) -> Stmt {
         Stmt::assign(self, rhs, loc)
     }
 
@@ -1189,8 +1187,7 @@ impl Expr {
     }
 
     /// `return self;`
-    pub fn ret(self) -> Stmt {
-        let loc = self.location.clone();
+    pub fn ret(self, loc: Location) -> Stmt {
         Stmt::ret(Some(self), loc)
     }
 
diff --git a/compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/stmt.rs b/compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/stmt.rs
index 74a9a192c40a..6d42500d7944 100644
--- a/compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/stmt.rs
+++ b/compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/stmt.rs
@@ -170,7 +170,7 @@ impl Stmt {
             );
             let nondet_value = lhs.typ().nondet();
             let nondet_assign_stmt = stmt!(Assign { lhs, rhs: nondet_value }, loc.clone());
-            return Stmt::block(vec![assert_stmt, nondet_assign_stmt]);
+            return Stmt::block(vec![assert_stmt, nondet_assign_stmt], loc);
         }
         stmt!(Assign { lhs, rhs }, loc)
     }
@@ -178,7 +178,9 @@ impl Stmt {
     /// `__CPROVER_assert(cond, msg);`
     pub fn assert(cond: Expr, msg: &str, loc: Location) -> Self {
         assert!(cond.typ().is_bool());
-        BuiltinFn::CProverAssert.call(vec![cond, Expr::string_constant(msg)], loc).as_stmt()
+        BuiltinFn::CProverAssert
+            .call(vec![cond, Expr::string_constant(msg)], loc.clone())
+            .as_stmt(loc)
     }
 
     pub fn assert_false(msg: &str, loc: Location) -> Self {
@@ -192,14 +194,12 @@ impl Stmt {
     }
 
     /// { ATOMIC_BEGIN stmt1; stmt2; ... ATOMIC_END }
-    pub fn atomic_block(stmts: Vec<Stmt>) -> Self {
-        let loc = if stmts.is_empty() { Location::none() } else { stmts[0].location().clone() };
+    pub fn atomic_block(stmts: Vec<Stmt>, loc: Location) -> Self {
         stmt!(AtomicBlock(stmts), loc)
     }
 
     /// `{ stmt1; stmt2; ... }`
-    pub fn block(stmts: Vec<Stmt>) -> Self {
-        let loc = if stmts.is_empty() { Location::none() } else { stmts[0].location().clone() };
+    pub fn block(stmts: Vec<Stmt>, loc: Location) -> Self {
         stmt!(Block(stmts), loc)
     }
 
diff --git a/compiler/rustc_codegen_llvm/src/gotoc/cbmc/irep/to_irep.rs b/compiler/rustc_codegen_llvm/src/gotoc/cbmc/irep/to_irep.rs
index a3d66fa24a07..246aec29c2a0 100644
--- a/compiler/rustc_codegen_llvm/src/gotoc/cbmc/irep/to_irep.rs
+++ b/compiler/rustc_codegen_llvm/src/gotoc/cbmc/irep/to_irep.rs
@@ -237,7 +237,7 @@ impl ToIrep for ExprValue {
             ExprValue::SelfOp { op, e } => side_effect_irep(op.to_irep_id(), vec![e.to_irep(mm)]),
             ExprValue::StatementExpression { statements: ops } => side_effect_irep(
                 IrepId::StatementExpression,
-                vec![Stmt::block(ops.to_vec()).to_irep(mm)],
+                vec![Stmt::block(ops.to_vec(), Location::none()).to_irep(mm)],
             ),
             ExprValue::StringConstant { s } => Irep {
                 id: IrepId::StringConstant,
diff --git a/compiler/rustc_codegen_llvm/src/gotoc/hooks.rs b/compiler/rustc_codegen_llvm/src/gotoc/hooks.rs
index 947210fdfaab..6e6f452a58b2 100644
--- a/compiler/rustc_codegen_llvm/src/gotoc/hooks.rs
+++ b/compiler/rustc_codegen_llvm/src/gotoc/hooks.rs
@@ -103,7 +103,10 @@ impl<'tcx> GotocHook<'tcx> for Assume {
         let target = target.unwrap();
         let loc = tcx.codegen_span_option2(span);
 
-        Stmt::block(vec![Stmt::assume(cond, loc.clone()), Stmt::goto(tcx.find_label(&target), loc)])
+        Stmt::block(
+            vec![Stmt::assume(cond, loc.clone()), Stmt::goto(tcx.find_label(&target), loc.clone())],
+            loc,
+        )
     }
 }
 
@@ -132,15 +135,18 @@ impl<'tcx> GotocHook<'tcx> for Nondet {
             Stmt::goto(tcx.find_label(&target), loc)
         } else {
             let pe = tcx.codegen_place(&p).goto_expr;
-            Stmt::block(vec![
-                pe.clone().assign(tcx.codegen_ty(pt).nondet()),
-                // we should potentially generate an assumption
-                match tcx.codegen_assumption(pt) {
-                    None => Stmt::skip(loc.clone()),
-                    Some(f) => Stmt::assume(f.call(vec![pe.address_of()]), loc.clone()),
-                },
-                Stmt::goto(tcx.find_label(&target), loc.clone()),
-            ])
+            Stmt::block(
+                vec![
+                    pe.clone().assign(tcx.codegen_ty(pt).nondet(), loc.clone()),
+                    // we should potentially generate an assumption
+                    match tcx.codegen_assumption(pt) {
+                        None => Stmt::skip(loc.clone()),
+                        Some(f) => Stmt::assume(f.call(vec![pe.address_of()]), loc.clone()),
+                    },
+                    Stmt::goto(tcx.find_label(&target), loc.clone()),
+                ],
+                loc,
+            )
         }
     }
 }
@@ -217,10 +223,13 @@ impl<'tcx> GotocHook<'tcx> for Intrinsic {
         let loc = tcx.codegen_span_option2(span);
         let p = assign_to.unwrap();
         let target = target.unwrap();
-        Stmt::block(vec![
-            tcx.codegen_intrinsic(instance, fargs, &p, span),
-            Stmt::goto(tcx.find_label(&target), loc),
-        ])
+        Stmt::block(
+            vec![
+                tcx.codegen_intrinsic(instance, fargs, &p, span),
+                Stmt::goto(tcx.find_label(&target), loc.clone()),
+            ],
+            loc,
+        )
     }
 }
 
@@ -250,17 +259,20 @@ impl<'tcx> GotocHook<'tcx> for MemReplace {
         let place_layout = tcx.layout_of(place_type);
         let place_is_zst = place_layout.is_zst();
         if place_is_zst {
-            Stmt::block(vec![Stmt::goto(tcx.find_label(&target), loc)])
+            Stmt::block(vec![Stmt::goto(tcx.find_label(&target), loc.clone())], loc)
         } else {
             let dest = fargs.remove(0);
             let src = fargs.remove(0);
-            Stmt::block(vec![
-                tcx.codegen_place(&p)
-                    .goto_expr
-                    .assign(dest.clone().dereference().with_location(loc.clone())),
-                dest.dereference().assign(src).with_location(loc.clone()),
-                Stmt::goto(tcx.find_label(&target), loc),
-            ])
+            Stmt::block(
+                vec![
+                    tcx.codegen_place(&p)
+                        .goto_expr
+                        .assign(dest.clone().dereference().with_location(loc.clone()), loc.clone()),
+                    dest.dereference().assign(src, loc.clone()),
+                    Stmt::goto(tcx.find_label(&target), loc.clone()),
+                ],
+                loc,
+            )
         }
     }
 }
@@ -302,8 +314,8 @@ impl<'tcx> GotocHook<'tcx> for MemSwap {
             block.push(Stmt::decl(var.to_expr(), Some(xe.clone().dereference()), Location::none()));
             let ye = y_param.to_expr();
             let var = var.to_expr();
-            block.push(xe.dereference().assign(ye.clone().dereference()));
-            block.push(ye.dereference().assign(var));
+            block.push(xe.dereference().assign(ye.clone().dereference(), loc.clone()));
+            block.push(ye.dereference().assign(var, loc.clone()));
 
             Symbol::function(
                 &func_name,
@@ -311,19 +323,18 @@ impl<'tcx> GotocHook<'tcx> for MemSwap {
                     vec![x_param.to_function_parameter(), y_param.to_function_parameter()],
                     Type::empty(),
                 ),
-                Some(Stmt::block(block)),
+                Some(Stmt::block(block, loc.clone())),
                 Location::none(),
             )
         });
 
-        Stmt::block(vec![
-            tcx.find_function(&func_name)
-                .unwrap()
-                .call(vec![x, y])
-                .as_stmt()
-                .with_location(loc.clone()),
-            Stmt::goto(tcx.find_label(&target), loc),
-        ])
+        Stmt::block(
+            vec![
+                tcx.find_function(&func_name).unwrap().call(vec![x, y]).as_stmt(loc.clone()),
+                Stmt::goto(tcx.find_label(&target), loc.clone()),
+            ],
+            loc,
+        )
     }
 }
 
@@ -353,10 +364,15 @@ impl<'tcx> GotocHook<'tcx> for PtrRead {
         let p = assign_to.unwrap();
         let target = target.unwrap();
         let src = fargs.remove(0);
-        Stmt::block(vec![
-            tcx.codegen_place(&p).goto_expr.assign(src.dereference().with_location(loc.clone())),
-            Stmt::goto(tcx.find_label(&target), loc),
-        ])
+        Stmt::block(
+            vec![
+                tcx.codegen_place(&p)
+                    .goto_expr
+                    .assign(src.dereference().with_location(loc.clone()), loc.clone()),
+                Stmt::goto(tcx.find_label(&target), loc.clone()),
+            ],
+            loc,
+        )
     }
 }
 
@@ -386,10 +402,13 @@ impl<'tcx> GotocHook<'tcx> for PtrWrite {
         let target = target.unwrap();
         let dst = fargs.remove(0);
         let src = fargs.remove(0);
-        Stmt::block(vec![
-            dst.dereference().assign(src).with_location(loc.clone()),
-            Stmt::goto(tcx.find_label(&target), loc),
-        ])
+        Stmt::block(
+            vec![
+                dst.dereference().assign(src, loc.clone()).with_location(loc.clone()),
+                Stmt::goto(tcx.find_label(&target), loc.clone()),
+            ],
+            loc,
+        )
     }
 }
 
@@ -414,14 +433,18 @@ impl<'tcx> GotocHook<'tcx> for RustAlloc {
         match (assign_to, target) {
             (Some(p), Some(target)) => {
                 let size = fargs.remove(0);
-                Stmt::block(vec![
-                    tcx.codegen_place(&p).goto_expr.assign(
-                        BuiltinFn::Malloc
-                            .call(vec![size], loc)
-                            .cast_to(Type::unsigned_int(8).to_pointer()),
-                    ),
-                    Stmt::goto(tcx.find_label(&target), Location::none()),
-                ])
+                Stmt::block(
+                    vec![
+                        tcx.codegen_place(&p).goto_expr.assign(
+                            BuiltinFn::Malloc
+                                .call(vec![size], loc.clone())
+                                .cast_to(Type::unsigned_int(8).to_pointer()),
+                            loc,
+                        ),
+                        Stmt::goto(tcx.find_label(&target), Location::none()),
+                    ],
+                    Location::none(),
+                )
             }
             _ => unreachable!(),
         }
@@ -449,10 +472,15 @@ impl<'tcx> GotocHook<'tcx> for RustDealloc {
         match target {
             Some(target) => {
                 let ptr = fargs.remove(0);
-                Stmt::block(vec![
-                    BuiltinFn::Free.call(vec![ptr.cast_to(Type::void_pointer())], loc).as_stmt(),
-                    Stmt::goto(tcx.find_label(&target), Location::none()),
-                ])
+                Stmt::block(
+                    vec![
+                        BuiltinFn::Free
+                            .call(vec![ptr.cast_to(Type::void_pointer())], loc.clone())
+                            .as_stmt(loc.clone()),
+                        Stmt::goto(tcx.find_label(&target), Location::none()),
+                    ],
+                    loc,
+                )
             }
             _ => unreachable!(),
         }
@@ -483,14 +511,18 @@ impl<'tcx> GotocHook<'tcx> for RustRealloc {
         fargs.remove(0); // old_size
         fargs.remove(0); // align
         let size = fargs.remove(0);
-        Stmt::block(vec![
-            tcx.codegen_place(&p).goto_expr.assign(
-                BuiltinFn::Realloc
-                    .call(vec![ptr, size], loc.clone())
-                    .cast_to(Type::unsigned_int(8).to_pointer()),
-            ),
-            Stmt::goto(tcx.find_label(&target), loc),
-        ])
+        Stmt::block(
+            vec![
+                tcx.codegen_place(&p).goto_expr.assign(
+                    BuiltinFn::Realloc
+                        .call(vec![ptr, size], loc.clone())
+                        .cast_to(Type::unsigned_int(8).to_pointer()),
+                    loc.clone(),
+                ),
+                Stmt::goto(tcx.find_label(&target), loc.clone()),
+            ],
+            loc,
+        )
     }
 }
 
@@ -515,14 +547,18 @@ impl<'tcx> GotocHook<'tcx> for RustAllocZeroed {
         let p = assign_to.unwrap();
         let target = target.unwrap();
         let size = fargs.remove(0);
-        Stmt::block(vec![
-            tcx.codegen_place(&p).goto_expr.assign(
-                BuiltinFn::Calloc
-                    .call(vec![Type::size_t().one(), size], loc.clone())
-                    .cast_to(Type::unsigned_int(8).to_pointer()),
-            ),
-            Stmt::goto(tcx.find_label(&target), loc),
-        ])
+        Stmt::block(
+            vec![
+                tcx.codegen_place(&p).goto_expr.assign(
+                    BuiltinFn::Calloc
+                        .call(vec![Type::size_t().one(), size], loc.clone())
+                        .cast_to(Type::unsigned_int(8).to_pointer()),
+                    loc.clone(),
+                ),
+                Stmt::goto(tcx.find_label(&target), loc.clone()),
+            ],
+            loc,
+        )
     }
 }
 
@@ -555,9 +591,12 @@ impl<'tcx> GotocHook<'tcx> for SliceFromRawPart {
         let code = tcx
             .codegen_place(&p)
             .goto_expr
-            .assign(Expr::struct_expr_from_values(pt, vec![data, len], &tcx.symbol_table))
+            .assign(
+                Expr::struct_expr_from_values(pt, vec![data, len], &tcx.symbol_table),
+                loc.clone(),
+            )
             .with_location(loc.clone());
-        Stmt::block(vec![code, Stmt::goto(tcx.find_label(&target), loc)])
+        Stmt::block(vec![code, Stmt::goto(tcx.find_label(&target), loc.clone())], loc)
     }
 }
 
diff --git a/compiler/rustc_codegen_llvm/src/gotoc/intrinsic.rs b/compiler/rustc_codegen_llvm/src/gotoc/intrinsic.rs
index 51e648a0449c..429599cb1e2e 100644
--- a/compiler/rustc_codegen_llvm/src/gotoc/intrinsic.rs
+++ b/compiler/rustc_codegen_llvm/src/gotoc/intrinsic.rs
@@ -179,9 +179,9 @@ impl<'tcx> GotocCtx<'tcx> {
                 let decl_stmt = Stmt::decl(tmp.clone(), Some(var1.to_owned()), loc.clone());
                 let var2 = fargs.remove(0);
                 let op_expr = (var1.clone()).$op(var2).with_location(loc.clone());
-                let assign_stmt = (var1.clone()).assign(op_expr);
+                let assign_stmt = (var1.clone()).assign(op_expr, loc.clone());
                 let res_stmt = self.codegen_expr_to_place(p, tmp.clone());
-                Stmt::atomic_block(vec![decl_stmt, assign_stmt, res_stmt])
+                Stmt::atomic_block(vec![decl_stmt, assign_stmt, res_stmt], loc)
             }};
         }
 
@@ -449,12 +449,19 @@ impl<'tcx> GotocCtx<'tcx> {
         let divisor_is_minus_one =
             if btyp.is_signed(mm) { b.clone().eq(btyp.one().neg()) } else { Expr::bool_false() };
         let division_does_not_overflow = dividend_is_int_min.and(divisor_is_minus_one).not();
-        Stmt::block(vec![
-            Stmt::assert(division_is_exact, "exact_div arguments divide exactly", loc.clone()),
-            Stmt::assert(divisor_is_nonzero, "exact_div divisor is nonzero", loc.clone()),
-            Stmt::assert(division_does_not_overflow, "exact_div division does not overflow", loc),
-            self.codegen_expr_to_place(p, a.div(b)),
-        ])
+        Stmt::block(
+            vec![
+                Stmt::assert(division_is_exact, "exact_div arguments divide exactly", loc.clone()),
+                Stmt::assert(divisor_is_nonzero, "exact_div divisor is nonzero", loc.clone()),
+                Stmt::assert(
+                    division_does_not_overflow,
+                    "exact_div division does not overflow",
+                    loc.clone(),
+                ),
+                self.codegen_expr_to_place(p, a.div(b)),
+            ],
+            loc,
+        )
     }
 
     /// An atomic load simply returns the value referenced
@@ -476,9 +483,9 @@ impl<'tcx> GotocCtx<'tcx> {
             intrinsic
         );
         let var1_ref = fargs.remove(0);
-        let var1 = var1_ref.dereference().with_location(loc);
+        let var1 = var1_ref.dereference().with_location(loc.clone());
         let res_stmt = self.codegen_expr_to_place(p, var1);
-        Stmt::atomic_block(vec![res_stmt])
+        Stmt::atomic_block(vec![res_stmt], loc)
     }
 
     /// An atomic compare-and-exchange updates the value referenced in
@@ -513,7 +520,7 @@ impl<'tcx> GotocCtx<'tcx> {
         let var2 = fargs.remove(0).with_location(loc.clone());
         let var3 = fargs.remove(0).with_location(loc.clone());
         let eq_expr = (var1.clone()).eq(var2.clone());
-        let assign_stmt = (var1.clone()).assign(var3);
+        let assign_stmt = (var1.clone()).assign(var3, loc.clone());
         let cond_update_stmt = Stmt::if_then_else(eq_expr, assign_stmt, None, loc.clone());
         let place_type = self.place_ty(p);
         let res_type = self.codegen_ty(place_type);
@@ -521,7 +528,7 @@ impl<'tcx> GotocCtx<'tcx> {
             Expr::struct_expr_from_values(res_type, vec![tmp, Expr::c_true()], &self.symbol_table)
                 .with_location(loc.clone());
         let res_stmt = self.codegen_expr_to_place(p, tuple_expr);
-        Stmt::atomic_block(vec![decl_stmt, cond_update_stmt, res_stmt])
+        Stmt::atomic_block(vec![decl_stmt, cond_update_stmt, res_stmt], loc)
     }
 
     /// An atomic store updates the value referenced in
@@ -550,9 +557,9 @@ impl<'tcx> GotocCtx<'tcx> {
         let tmp = self.gen_temp_variable(var1.typ().clone(), loc.clone()).to_expr();
         let decl_stmt = Stmt::decl(tmp.clone(), Some(var1.to_owned()), loc.clone());
         let var2 = fargs.remove(0).with_location(loc.clone());
-        let assign_stmt = (var1.clone()).assign(var2);
+        let assign_stmt = (var1.clone()).assign(var2, loc.clone());
         let res_stmt = self.codegen_expr_to_place(p, tmp.clone());
-        Stmt::atomic_block(vec![decl_stmt, assign_stmt, res_stmt])
+        Stmt::atomic_block(vec![decl_stmt, assign_stmt, res_stmt], loc)
     }
 
     /// Atomic no-ops (e.g., atomic_fence) are transformed into SKIP statements
@@ -561,8 +568,8 @@ impl<'tcx> GotocCtx<'tcx> {
             "RMC does not support concurrency for now. {} treated as a sequential operation.",
             intrinsic
         );
-        let skip_stmt = Stmt::skip(loc);
-        Stmt::atomic_block(vec![skip_stmt])
+        let skip_stmt = Stmt::skip(loc.clone());
+        Stmt::atomic_block(vec![skip_stmt], loc)
     }
 
     /// ptr_offset_from returns the offset between two pointers
@@ -577,14 +584,17 @@ impl<'tcx> GotocCtx<'tcx> {
         let b = fargs.remove(0);
         let pointers_to_same_object = a.clone().same_object(b.clone());
 
-        Stmt::block(vec![
-            Stmt::assert(
-                pointers_to_same_object,
-                "ptr_offset_from: pointers point to same object",
-                loc,
-            ),
-            self.codegen_expr_to_place(p, a.sub(b)),
-        ])
+        Stmt::block(
+            vec![
+                Stmt::assert(
+                    pointers_to_same_object,
+                    "ptr_offset_from: pointers point to same object",
+                    loc.clone(),
+                ),
+                self.codegen_expr_to_place(p, a.sub(b)),
+            ],
+            loc,
+        )
     }
 
     /// A transmute is a bitcast from the argument type to the return type.
diff --git a/compiler/rustc_codegen_llvm/src/gotoc/metadata.rs b/compiler/rustc_codegen_llvm/src/gotoc/metadata.rs
index 76a9bdaeb564..b8a24ac9d375 100644
--- a/compiler/rustc_codegen_llvm/src/gotoc/metadata.rs
+++ b/compiler/rustc_codegen_llvm/src/gotoc/metadata.rs
@@ -444,7 +444,7 @@ impl<'tcx> GotocCtx<'tcx> {
             Symbol::function(
                 &fn_name,
                 Type::code(vec![], Type::constructor()),
-                Some(Stmt::block(vec![body])), //TODO is this block needed?
+                Some(Stmt::block(vec![body], Location::none())), //TODO is this block needed?
                 Location::none(),
             )
             .with_is_file_local(true)
@@ -479,7 +479,7 @@ impl<'tcx> GotocCtx<'tcx> {
             ),
             // Assume false to block any further exploration of this path.
             Stmt::assume(Expr::bool_false(), loc.clone()),
-            t.nondet().as_stmt().with_location(loc.clone()), //TODO assume rust validity contraints
+            t.nondet().as_stmt(loc.clone()).with_location(loc.clone()), //TODO assume rust validity contraints
         ];
 
         Expr::statement_expression(body, t).with_location(loc)
diff --git a/compiler/rustc_codegen_llvm/src/gotoc/mod.rs b/compiler/rustc_codegen_llvm/src/gotoc/mod.rs
index a23a5ccc1863..62859df6f68a 100644
--- a/compiler/rustc_codegen_llvm/src/gotoc/mod.rs
+++ b/compiler/rustc_codegen_llvm/src/gotoc/mod.rs
@@ -114,7 +114,7 @@ impl<'tcx> GotocCtx<'tcx> {
 
             let loc = self.codegen_span2(&mir.span);
             let stmts = std::mem::replace(&mut self.current_fn_mut().block, vec![]);
-            let body = Stmt::block(stmts).with_location(loc);
+            let body = Stmt::block(stmts, loc);
             self.symbol_table.update_fn_declaration_with_definition(&name, body);
         }
         self.reset_current_fn();
diff --git a/compiler/rustc_codegen_llvm/src/gotoc/operand.rs b/compiler/rustc_codegen_llvm/src/gotoc/operand.rs
index 9d0fc122c803..60d99481412e 100644
--- a/compiler/rustc_codegen_llvm/src/gotoc/operand.rs
+++ b/compiler/rustc_codegen_llvm/src/gotoc/operand.rs
@@ -273,13 +273,15 @@ impl<'tcx> GotocCtx<'tcx> {
             let var = tcx.gen_function_local_variable(2, &func_name, cgt.clone()).to_expr();
             let body = vec![
                 Stmt::decl(var.clone(), None, Location::none()),
-                var.clone().member("case", &tcx.symbol_table).assign(param.to_expr()),
-                var.clone().ret(),
+                var.clone()
+                    .member("case", &tcx.symbol_table)
+                    .assign(param.to_expr(), Location::none()),
+                var.clone().ret(Location::none()),
             ];
             Symbol::function(
                 &func_name,
                 Type::code(vec![param.to_function_parameter()], cgt),
-                Some(Stmt::block(body)),
+                Some(Stmt::block(body, Location::none())),
                 Location::none(),
             )
         });
@@ -474,10 +476,13 @@ impl<'tcx> GotocCtx<'tcx> {
         );
         let fn_name = Self::initializer_fn_name(&name);
         let temp_var = self.gen_function_local_variable(0, &fn_name, alloc_typ_ref).to_expr();
-        let body = Stmt::block(vec![
-            Stmt::decl(temp_var.clone(), Some(val), Location::none()),
-            var.assign(temp_var.transmute_to(var_typ, &self.symbol_table)),
-        ]);
+        let body = Stmt::block(
+            vec![
+                Stmt::decl(temp_var.clone(), Some(val), Location::none()),
+                var.assign(temp_var.transmute_to(var_typ, &self.symbol_table), Location::none()),
+            ],
+            Location::none(),
+        );
         self.register_initializer(&name, body);
 
         self.alloc_map.insert(alloc, name);
@@ -525,13 +530,14 @@ impl<'tcx> GotocCtx<'tcx> {
             let var = tcx.gen_function_local_variable(2, &fname, cgt.clone()).to_expr();
             let body = vec![
                 Stmt::decl(var.clone(), None, Location::none()),
-                tcx.codegen_get_niche(var.clone(), offset, target_ty).assign(param.to_expr()),
-                var.ret(),
+                tcx.codegen_get_niche(var.clone(), offset, target_ty)
+                    .assign(param.to_expr(), Location::none()),
+                var.ret(Location::none()),
             ];
             Symbol::function(
                 &fname,
                 Type::code(vec![param.to_function_parameter()], cgt),
-                Some(Stmt::block(body)),
+                Some(Stmt::block(body, Location::none())),
                 Location::none(),
             )
         });
diff --git a/compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs b/compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs
index a40d897dab77..358f57aef75d 100644
--- a/compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs
+++ b/compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs
@@ -184,21 +184,25 @@ impl<'tcx> GotocCtx<'tcx> {
                 Stmt::decl(idx.clone(), Some(Type::size_t().zero()), Location::none()),
             ];
 
-            let lbody = Stmt::block(vec![
-                tcx.codegen_idx_array(res.clone(), idx.clone()).assign(inp.to_expr()),
-            ]);
+            let lbody = Stmt::block(
+                vec![
+                    tcx.codegen_idx_array(res.clone(), idx.clone())
+                        .assign(inp.to_expr(), Location::none()),
+                ],
+                Location::none(),
+            );
             body.push(Stmt::for_loop(
                 Stmt::skip(Location::none()),
                 idx.clone().lt(tcx.codegen_const(sz, None)),
-                idx.postincr().as_stmt(),
+                idx.postincr().as_stmt(Location::none()),
                 lbody,
                 Location::none(),
             ));
-            body.push(res.ret());
+            body.push(res.ret(Location::none()));
             Symbol::function(
                 &func_name,
                 Type::code(vec![inp.to_function_parameter()], res_t),
-                Some(Stmt::block(body)),
+                Some(Stmt::block(body, Location::none())),
                 Location::none(),
             )
         });
@@ -820,7 +824,7 @@ impl<'tcx> GotocCtx<'tcx> {
                     vtable_fields,
                     &ctx.symbol_table,
                 );
-                let body = var.assign(vtable);
+                let body = var.assign(vtable, Location::none());
                 Some(body)
             },
         )
diff --git a/compiler/rustc_codegen_llvm/src/gotoc/statement.rs b/compiler/rustc_codegen_llvm/src/gotoc/statement.rs
index 2c33d55e564b..a03fb5a68d2e 100644
--- a/compiler/rustc_codegen_llvm/src/gotoc/statement.rs
+++ b/compiler/rustc_codegen_llvm/src/gotoc/statement.rs
@@ -45,9 +45,9 @@ impl<'tcx> GotocCtx<'tcx> {
                     let p = Place::from(mir::RETURN_PLACE);
                     let v = self.codegen_place(&p).goto_expr;
                     if self.place_ty(&p).is_bool() {
-                        v.cast_to(Type::c_bool()).ret()
+                        v.cast_to(Type::c_bool()).ret(loc)
                     } else {
-                        v.ret()
+                        v.ret(loc)
                     }
                 }
             }
@@ -65,15 +65,18 @@ impl<'tcx> GotocCtx<'tcx> {
                     if *expected { r } else { Expr::not(r) }
                 };
 
-                Stmt::block(vec![
-                    cond.cast_to(Type::bool()).if_then_else(
+                Stmt::block(
+                    vec![
+                        cond.cast_to(Type::bool()).if_then_else(
+                            Stmt::goto(self.find_label(target), loc.clone()),
+                            None,
+                            loc.clone(),
+                        ),
+                        Stmt::assert_false(&format!("{:?}", msg), loc.clone()),
                         Stmt::goto(self.find_label(target), loc.clone()),
-                        None,
-                        loc.clone(),
-                    ),
-                    Stmt::assert_false(&format!("{:?}", msg), loc.clone()),
-                    Stmt::goto(self.find_label(target), loc),
-                ])
+                    ],
+                    loc,
+                )
             }
             TerminatorKind::Yield { .. }
             | TerminatorKind::GeneratorDrop
@@ -83,10 +86,10 @@ impl<'tcx> GotocCtx<'tcx> {
                 .codegen_unimplemented(
                     "InlineAsm",
                     Type::empty(),
-                    loc,
+                    loc.clone(),
                     "https://github.com/model-checking/rmc/issues/2",
                 )
-                .as_stmt(),
+                .as_stmt(loc),
         }
     }
 
@@ -107,16 +110,17 @@ impl<'tcx> GotocCtx<'tcx> {
                         Location::none(),
                         "https://github.com/model-checking/rmc/issues/11",
                     )
-                    .as_stmt(),
+                    .as_stmt(Location::none()),
                 InstanceDef::DropGlue(..) => Stmt::skip(Location::none()),
                 _ => {
                     let func = self.codegen_func_expr(instance, None);
-                    func.call(vec![self.codegen_place(location).goto_expr.address_of()]).as_stmt()
+                    func.call(vec![self.codegen_place(location).goto_expr.address_of()])
+                        .as_stmt(Location::none())
                 }
             };
             let goto_target = Stmt::goto(self.find_label(target), Location::none());
             let block = vec![drop_implementation, goto_target];
-            Stmt::block(block)
+            Stmt::block(block, Location::none())
         }
     }
 
@@ -140,20 +144,23 @@ impl<'tcx> GotocCtx<'tcx> {
             ty::Bool => {
                 let jmp: usize = values[0].try_into().unwrap();
                 let jmp2 = if jmp == 0 { 1 } else { 0 };
-                Stmt::block(vec![
-                    v.cast_to(Type::bool()).if_then_else(
+                Stmt::block(
+                    vec![
+                        v.cast_to(Type::bool()).if_then_else(
+                            Stmt::goto(
+                                self.current_fn().labels()[targets[jmp2].index()].clone(),
+                                Location::none(),
+                            ),
+                            None,
+                            Location::none(),
+                        ),
                         Stmt::goto(
-                            self.current_fn().labels()[targets[jmp2].index()].clone(),
+                            self.current_fn().labels()[targets[jmp].index()].clone(),
                             Location::none(),
                         ),
-                        None,
-                        Location::none(),
-                    ),
-                    Stmt::goto(
-                        self.current_fn().labels()[targets[jmp].index()].clone(),
-                        Location::none(),
-                    ),
-                ])
+                    ],
+                    Location::none(),
+                )
             }
             ty::Char | ty::Int(_) | ty::Uint(_) => {
                 let cases = values
@@ -313,19 +320,22 @@ impl<'tcx> GotocCtx<'tcx> {
                 // Actually generate the function call, and store the return value, if any.
                 stmts.append(&mut vec![
                     self.codegen_expr_to_place(&p, funce.call(fargs)).with_location(loc.clone()),
-                    Stmt::goto(self.find_label(&target), loc),
+                    Stmt::goto(self.find_label(&target), loc.clone()),
                 ]);
-                Stmt::block(stmts)
+                Stmt::block(stmts, loc)
             }
             ty::FnPtr(_) => {
                 let (p, target) = destination.unwrap();
                 let func_expr = self.codegen_operand(func).dereference();
                 // Actually generate the function call, and store the return value, if any.
-                Stmt::block(vec![
-                    self.codegen_expr_to_place(&p, func_expr.call(fargs))
-                        .with_location(loc.clone()),
-                    Stmt::goto(self.find_label(&target), loc),
-                ])
+                Stmt::block(
+                    vec![
+                        self.codegen_expr_to_place(&p, func_expr.call(fargs))
+                            .with_location(loc.clone()),
+                        Stmt::goto(self.find_label(&target), loc.clone()),
+                    ],
+                    loc,
+                )
             }
             x => unreachable!("Function call where the function was of unexpected type: {:?}", x),
         }
@@ -336,9 +346,9 @@ impl<'tcx> GotocCtx<'tcx> {
     /// Otherwise, we assign the value of the expression to the place.
     pub fn codegen_expr_to_place(&mut self, p: &Place<'tcx>, e: Expr) -> Stmt {
         if self.place_ty(p).is_unit() {
-            e.as_stmt()
+            e.as_stmt(Location::none())
         } else {
-            self.codegen_place(&p).goto_expr.assign(e)
+            self.codegen_place(&p).goto_expr.assign(e, Location::none())
         }
     }
 
@@ -372,10 +382,13 @@ impl<'tcx> GotocCtx<'tcx> {
                 None => self.codegen_assert_false(arg, loc),
                 Some(alt) => {
                     let loc = self.codegen_span2(&pterm.source_info.span);
-                    Stmt::block(vec![
-                        self.codegen_assert_false(arg, loc),
-                        Stmt::goto(self.find_label(alt), Location::none()),
-                    ])
+                    Stmt::block(
+                        vec![
+                            self.codegen_assert_false(arg, loc.clone()),
+                            Stmt::goto(self.find_label(alt), Location::none()),
+                        ],
+                        loc,
+                    )
                 }
             }
         } else {
@@ -386,7 +399,7 @@ impl<'tcx> GotocCtx<'tcx> {
     // By the time we get this, the string constant has been codegenned.
     // TODO: make this case also use the Stmt::assert_false() constructor
     pub fn codegen_assert_false(&mut self, err: Expr, loc: Location) -> Stmt {
-        BuiltinFn::CProverAssert.call(vec![Expr::bool_false(), err], loc).as_stmt()
+        BuiltinFn::CProverAssert.call(vec![Expr::bool_false(), err], loc.clone()).as_stmt(loc)
     }
 
     pub fn codegen_statement(&mut self, stmt: &Statement<'tcx>) -> Stmt {
@@ -403,13 +416,15 @@ impl<'tcx> GotocCtx<'tcx> {
                     // implicit address of a function pointer, e.g.
                     // let fp: fn() -> i32 = foo;
                     // where the reference is implicit.
-                    self.codegen_place(l).goto_expr.assign(self.codegen_rvalue(r).address_of())
+                    self.codegen_place(l)
+                        .goto_expr
+                        .assign(self.codegen_rvalue(r).address_of(), Location::none())
                 } else if rty.is_bool() {
                     self.codegen_place(l)
                         .goto_expr
-                        .assign(self.codegen_rvalue(r).cast_to(Type::c_bool()))
+                        .assign(self.codegen_rvalue(r).cast_to(Type::c_bool()), Location::none())
                 } else {
-                    self.codegen_place(l).goto_expr.assign(self.codegen_rvalue(r))
+                    self.codegen_place(l).goto_expr.assign(self.codegen_rvalue(r), Location::none())
                 }
             }
             StatementKind::SetDiscriminant { place, variant_index } => {
@@ -430,7 +445,7 @@ impl<'tcx> GotocCtx<'tcx> {
                             self.codegen_place(place)
                                 .goto_expr
                                 .member("case", &self.symbol_table)
-                                .assign(discr)
+                                .assign(discr, Location::none())
                         }
                         TagEncoding::Niche { dataful_variant, niche_variants, niche_start } => {
                             if dataful_variant != variant_index {
@@ -451,7 +466,8 @@ impl<'tcx> GotocCtx<'tcx> {
                                     Expr::int_constant(niche_value, discr_ty.clone())
                                 };
                                 let place = self.codegen_place(place).goto_expr;
-                                self.codegen_get_niche(place, offset, discr_ty).assign(value)
+                                self.codegen_get_niche(place, offset, discr_ty)
+                                    .assign(value, Location::none())
                             } else {
                                 Stmt::skip(Location::none())
                             }
@@ -468,7 +484,7 @@ impl<'tcx> GotocCtx<'tcx> {
                     Location::none(),
                     "https://github.com/model-checking/rmc/issues/2",
                 )
-                .as_stmt(),
+                .as_stmt(Location::none()),
             StatementKind::CopyNonOverlapping(box mir::CopyNonOverlapping {
                 ref src,
                 ref dst,
@@ -482,7 +498,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 let n = sz.mul(count);
                 let dst = dst.cast_to(Type::void_pointer());
                 let e = BuiltinFn::Memcpy.call(vec![dst, src, n], Location::none());
-                e.as_stmt()
+                e.as_stmt(Location::none())
             }
             StatementKind::FakeRead(_)
             | StatementKind::Retag(_, _)
diff --git a/compiler/rustc_codegen_llvm/src/gotoc/stubs/rust_stubber.rs b/compiler/rustc_codegen_llvm/src/gotoc/stubs/rust_stubber.rs
index 509f59b6d6c2..c7df8d24920a 100644
--- a/compiler/rustc_codegen_llvm/src/gotoc/stubs/rust_stubber.rs
+++ b/compiler/rustc_codegen_llvm/src/gotoc/stubs/rust_stubber.rs
@@ -120,10 +120,13 @@ pub trait RustStubber<'tcx> {
         let p = assign_to.unwrap();
         let fn_call = fctn.call(fargs);
         let target = target.unwrap();
-        Stmt::block(vec![
-            tcx.codegen_expr_to_place(&p, fn_call),
-            Stmt::goto(tcx.find_label(&target), Location::none()),
-        ])
+        Stmt::block(
+            vec![
+                tcx.codegen_expr_to_place(&p, fn_call),
+                Stmt::goto(tcx.find_label(&target), Location::none()),
+            ],
+            Location::none(),
+        )
     }
 
     fn find_cbmc_fn(&self, tcx: TyCtxt<'tcx>, stubbed_ty: Ty<'tcx>, name: &str) -> Option<DefId> {