diff --git a/charon/Cargo.lock b/charon/Cargo.lock
index 999ef7ae1..8729ce1d0 100644
--- a/charon/Cargo.lock
+++ b/charon/Cargo.lock
@@ -787,7 +787,7 @@ checksum = "bf151400ff0baff5465007dd2f3e717f3fe502074ca563069ce3a6629d07b289"
 [[package]]
 name = "hax-adt-into"
 version = "0.2.0"
-source = "git+https://github.com/cryspen/hax?branch=main#cdfc20db1abab9ec36e2c7bcfacf0ac8d52c85fd"
+source = "git+https://github.com/cryspen/hax?branch=main#0275a2b0cda11871b3761b09c2a07d467a5baf1f"
 dependencies = [
  "itertools 0.11.0",
  "proc-macro2",
@@ -798,7 +798,7 @@ dependencies = [
 [[package]]
 name = "hax-frontend-exporter"
 version = "0.2.0"
-source = "git+https://github.com/cryspen/hax?branch=main#cdfc20db1abab9ec36e2c7bcfacf0ac8d52c85fd"
+source = "git+https://github.com/cryspen/hax?branch=main#0275a2b0cda11871b3761b09c2a07d467a5baf1f"
 dependencies = [
  "extension-traits",
  "hax-adt-into",
@@ -815,7 +815,7 @@ dependencies = [
 [[package]]
 name = "hax-frontend-exporter-options"
 version = "0.2.0"
-source = "git+https://github.com/cryspen/hax?branch=main#cdfc20db1abab9ec36e2c7bcfacf0ac8d52c85fd"
+source = "git+https://github.com/cryspen/hax?branch=main#0275a2b0cda11871b3761b09c2a07d467a5baf1f"
 dependencies = [
  "hax-adt-into",
  "schemars",
diff --git a/charon/src/ast/ullbc_ast_utils.rs b/charon/src/ast/ullbc_ast_utils.rs
index 749d2f0d9..8fa8f0ef7 100644
--- a/charon/src/ast/ullbc_ast_utils.rs
+++ b/charon/src/ast/ullbc_ast_utils.rs
@@ -39,9 +39,20 @@ impl Terminator {
             comments_before: vec![],
         }
     }
+    pub fn goto(span: Span, target: BlockId) -> Self {
+        Self::new(span, RawTerminator::Goto { target })
+    }
 }
 
 impl BlockData {
+    /// Build a block that's just a goto terminator.
+    pub fn new_goto(span: Span, target: BlockId) -> Self {
+        BlockData {
+            statements: vec![],
+            terminator: Terminator::goto(span, target),
+        }
+    }
+
     pub fn targets(&self) -> Vec<BlockId> {
         match &self.terminator.content {
             RawTerminator::Goto { target } => {
diff --git a/charon/src/ast/visitor.rs b/charon/src/ast/visitor.rs
index 0d79b971c..b734e8393 100644
--- a/charon/src/ast/visitor.rs
+++ b/charon/src/ast/visitor.rs
@@ -141,7 +141,7 @@ impl<K: Any, T: AstVisitable> AstVisitable for IndexMap<K, T> {
     // Types that are ignored when encountered.
     skip(
         AbortKind, BinOp, BorrowKind, ConstantExpr, ConstGeneric, FieldId, FieldProjKind,
-        FunDeclId, FunIdOrTraitMethodRef, GenericArgs, GlobalDeclRef, IntegerTy, Locals,
+        FunDeclId, FunIdOrTraitMethodRef, GenericArgs, GlobalDeclRef, IntegerTy,
         NullOp, RefKind, ScalarValue, Span, Ty, TypeDeclId, TypeId, UnOp, VariantId, LocalId,
     ),
     // Types that we unconditionally explore.
@@ -150,7 +150,7 @@ impl<K: Any, T: AstVisitable> AstVisitable for IndexMap<K, T> {
         llbc_ast::ExprBody, llbc_ast::RawStatement, llbc_ast::Switch,
         ullbc_ast::BlockData, ullbc_ast::ExprBody, ullbc_ast::RawStatement,
         ullbc_ast::RawTerminator, ullbc_ast::SwitchTargets,
-        Body, Opaque,
+        Body, Opaque, Locals, Local,
         for<T: BodyVisitable> Box<T>,
         for<T: BodyVisitable> Option<T>,
         for<T: BodyVisitable, E: BodyVisitable> Result<T, E>,
diff --git a/charon/src/bin/charon-driver/translate/get_mir.rs b/charon/src/bin/charon-driver/translate/get_mir.rs
index ee8fbeaca..2631eadc6 100644
--- a/charon/src/bin/charon-driver/translate/get_mir.rs
+++ b/charon/src/bin/charon-driver/translate/get_mir.rs
@@ -5,7 +5,6 @@ use std::rc::Rc;
 use hax_frontend_exporter as hax;
 use hax_frontend_exporter::{HasMirSetter, HasOwnerIdSetter};
 use rustc_hir as hir;
-use rustc_hir::def_id::DefId;
 use rustc_middle::mir::Body;
 use rustc_middle::ty::TyCtxt;
 
@@ -17,7 +16,7 @@ use super::translate_ctx::TranslateCtx;
 impl TranslateCtx<'_> {
     pub fn get_mir(
         &mut self,
-        def_id: DefId,
+        def_id: &hax::DefId,
         span: Span,
     ) -> Result<Option<hax::MirBody<()>>, Error> {
         let tcx = self.tcx;
@@ -25,6 +24,7 @@ impl TranslateCtx<'_> {
         Ok(match get_mir_for_def_id_and_level(tcx, def_id, mir_level) {
             Some(body) => {
                 // Here, we have to create a MIR state, which contains the body.
+                let def_id = def_id.underlying_rust_def_id();
                 let body = Rc::new(body);
                 let state = self
                     .hax_state
@@ -42,50 +42,59 @@ impl TranslateCtx<'_> {
 
 /// Query the MIR for a function at a specific level. Return `None` in the case of a foreign body
 /// with no MIR available.
-fn get_mir_for_def_id_and_level(
-    tcx: TyCtxt<'_>,
-    def_id: DefId,
+fn get_mir_for_def_id_and_level<'tcx>(
+    tcx: TyCtxt<'tcx>,
+    def_id: &hax::DefId,
     level: MirLevel,
-) -> Option<Body<'_>> {
-    // Below: we **clone** the bodies to make sure we don't have issues with
-    // locked values (we had in the past).
-    if let Some(local_def_id) = def_id.as_local() {
-        match level {
-            MirLevel::Built => {
-                let body = tcx.mir_built(local_def_id);
-                if !body.is_stolen() {
-                    return Some(body.borrow().clone());
+) -> Option<Body<'tcx>> {
+    let rust_def_id = def_id.underlying_rust_def_id();
+    match def_id.promoted_id() {
+        None => {
+            // Below: we **clone** the bodies to make sure we don't have issues with
+            // locked values (we had in the past).
+            if let Some(local_def_id) = rust_def_id.as_local() {
+                match level {
+                    MirLevel::Built => {
+                        let body = tcx.mir_built(local_def_id);
+                        if !body.is_stolen() {
+                            return Some(body.borrow().clone());
+                        }
+                    }
+                    MirLevel::Promoted => {
+                        let (body, _) = tcx.mir_promoted(local_def_id);
+                        if !body.is_stolen() {
+                            return Some(body.borrow().clone());
+                        }
+                    }
+                    MirLevel::Optimized => {}
                 }
+                // We fall back to optimized MIR if the requested body was stolen.
             }
-            MirLevel::Promoted => {
-                let (body, _) = tcx.mir_promoted(local_def_id);
-                if !body.is_stolen() {
-                    return Some(body.borrow().clone());
-                }
-            }
-            MirLevel::Optimized => {}
+
+            // There are only two MIRs we can fetch for non-local bodies: CTFE mir for globals and const
+            // fns, and optimized MIR for functions.
+            //
+            // We pass `-Zalways-encode-mir` so that we get MIR for all the dependencies we compiled
+            // ourselves. This doesn't apply to the stdlib; there we only get MIR for const items and
+            // generic or inlineable functions.
+            let is_global = rust_def_id.as_local().is_some_and(|local_def_id| {
+                matches!(
+                    tcx.hir_body_owner_kind(local_def_id),
+                    hir::BodyOwnerKind::Const { .. } | hir::BodyOwnerKind::Static(_)
+                )
+            });
+            let body = if tcx.is_mir_available(rust_def_id) && !is_global {
+                tcx.optimized_mir(rust_def_id).clone()
+            } else if tcx.is_ctfe_mir_available(rust_def_id) {
+                tcx.mir_for_ctfe(rust_def_id).clone()
+            } else {
+                return None;
+            };
+            Some(body)
+        }
+        Some(promoted_id) => {
+            let promoted_id = promoted_id.as_rust_promoted_id();
+            Some(hax::get_promoted_mir(tcx, rust_def_id, promoted_id))
         }
-        // We fall back to optimized MIR if the requested body was stolen.
     }
-
-    // There are only two MIRs we can fetch for non-local bodies: CTFE mir for globals and const
-    // fns, and optimized MIR for functions.
-    //
-    // We pass `-Zalways-encode-mir` so that we get MIR for all the dependencies we compiled
-    // ourselves. This doesn't apply to the stdlib; there we only get MIR for const items and
-    // generic or inlineable functions.
-    let is_global = def_id.as_local().is_some_and(|local_def_id| {
-        matches!(
-            tcx.hir_body_owner_kind(local_def_id),
-            hir::BodyOwnerKind::Const { .. } | hir::BodyOwnerKind::Static(_)
-        )
-    });
-    let body = if tcx.is_mir_available(def_id) && !is_global {
-        tcx.optimized_mir(def_id).clone()
-    } else if tcx.is_ctfe_mir_available(def_id) {
-        tcx.mir_for_ctfe(def_id).clone()
-    } else {
-        return None;
-    };
-    Some(body)
 }
diff --git a/charon/src/bin/charon-driver/translate/resolve_path.rs b/charon/src/bin/charon-driver/translate/resolve_path.rs
index 23fd4b7dd..58e02bc39 100644
--- a/charon/src/bin/charon-driver/translate/resolve_path.rs
+++ b/charon/src/bin/charon-driver/translate/resolve_path.rs
@@ -84,11 +84,11 @@ pub fn def_path_def_ids<'a, 'tcx>(
             items = items
                 .into_iter()
                 .flat_map(|def_id| {
-                    let hax_def: Arc<hax::FullDef> = def_id.sinto(s);
+                    let hax_def: Arc<hax::FullDef> = def_id.sinto(s).full_def(s);
                     hax_def.nameable_children(s)
                 })
                 .filter(|(child_name, _)| *child_name == segment_str)
-                .map(|(_, def_id)| def_id.to_rust_def_id())
+                .filter_map(|(_, def_id)| def_id.as_rust_def_id())
                 .collect();
         }
         if items.is_empty() {
diff --git a/charon/src/bin/charon-driver/translate/translate_bodies.rs b/charon/src/bin/charon-driver/translate/translate_bodies.rs
index 4ad743f5c..20ec8b1e2 100644
--- a/charon/src/bin/charon-driver/translate/translate_bodies.rs
+++ b/charon/src/bin/charon-driver/translate/translate_bodies.rs
@@ -358,23 +358,33 @@ impl BodyTransCtx<'_, '_, '_> {
                 Ok((Operand::Move(p), ty))
             }
             hax::Operand::Constant(const_op) => match &const_op.kind {
-                hax::ConstOperandKind::Value(constant)
-                | hax::ConstOperandKind::Promoted(_, Some(constant)) => {
+                hax::ConstOperandKind::Value(constant) => {
                     let constant = self.translate_constant_expr_to_constant_expr(span, constant)?;
                     let ty = constant.ty.clone();
                     Ok((Operand::Const(constant), ty))
                 }
-                hax::ConstOperandKind::Promoted(promoted, None) => {
+                hax::ConstOperandKind::Promoted {
+                    def_id,
+                    args,
+                    impl_exprs,
+                } => {
+                    let ty = self.translate_ty(span, &const_op.ty)?;
                     // A promoted constant that could not be evaluated.
-                    // TODO: translate as a Global, then inline in a pass. will need to shift
-                    // locals and block ids.
-                    // TODO: disable hax's `inline_anon_const` so we also get that for inline
-                    // consts too.
-                    raise_error!(
-                        self,
-                        span,
-                        "Cannot translate unevaluated constant: {promoted:?}"
-                    )
+                    let global_id = self.register_global_decl_id(span, def_id);
+                    let constant = ConstantExpr {
+                        value: RawConstantExpr::Global(GlobalDeclRef {
+                            id: global_id,
+                            generics: self.translate_generic_args(
+                                span,
+                                args,
+                                impl_exprs,
+                                None,
+                                GenericsSource::item(global_id),
+                            )?,
+                        }),
+                        ty: ty.clone(),
+                    };
+                    Ok((Operand::Const(constant), ty))
                 }
             },
         }
@@ -1107,8 +1117,7 @@ impl BodyTransCtx<'_, '_, '_> {
         span: Span,
     ) -> Result<Result<Body, Opaque>, Error> {
         // Retrieve the body
-        let rust_id = def.rust_def_id();
-        let Some(body) = self.t_ctx.get_mir(rust_id, span)? else {
+        let Some(body) = self.t_ctx.get_mir(&def.def_id, span)? else {
             return Ok(Err(Opaque));
         };
 
diff --git a/charon/src/bin/charon-driver/translate/translate_crate_to_ullbc.rs b/charon/src/bin/charon-driver/translate/translate_crate_to_ullbc.rs
index cf22dc18b..42b1e882d 100644
--- a/charon/src/bin/charon-driver/translate/translate_crate_to_ullbc.rs
+++ b/charon/src/bin/charon-driver/translate/translate_crate_to_ullbc.rs
@@ -5,7 +5,6 @@ use charon_lib::transform::TransformCtx;
 use hax::FullDefKind;
 use hax_frontend_exporter::{self as hax, SInto};
 use itertools::Itertools;
-use rustc_hir::def_id::DefId;
 use rustc_middle::ty::TyCtxt;
 use std::cell::RefCell;
 use std::path::PathBuf;
@@ -59,6 +58,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> {
             | Ctor { .. }
             | Field { .. }
             | InlineConst { .. }
+            | PromotedConst { .. }
             | LifetimeParam { .. }
             | OpaqueTy { .. }
             | SyntheticCoroutineBody { .. }
@@ -105,28 +105,28 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> {
         Ok(())
     }
 
-    pub(crate) fn translate_item(&mut self, item_src: TransItemSource) {
+    pub(crate) fn translate_item(&mut self, item_src: &TransItemSource) {
         let trans_id = self.id_map.get(&item_src).copied();
-        let rust_id = item_src.to_def_id();
-        self.with_def_id(rust_id, trans_id, |mut ctx| {
-            let span = ctx.def_span(rust_id);
+        let def_id = item_src.as_def_id();
+        self.with_def_id(def_id, trans_id, |mut ctx| {
+            let span = ctx.def_span(def_id);
             // Catch cycles
             let res = {
                 // Stopgap measure because there are still many panics in charon and hax.
                 let mut ctx = std::panic::AssertUnwindSafe(&mut ctx);
-                std::panic::catch_unwind(move || ctx.translate_item_aux(rust_id, trans_id))
+                std::panic::catch_unwind(move || ctx.translate_item_aux(def_id, trans_id))
             };
             match res {
                 Ok(Ok(())) => return,
                 // Translation error
                 Ok(Err(_)) => {
-                    register_error!(ctx, span, "Item `{rust_id:?}` caused errors; ignoring.")
+                    register_error!(ctx, span, "Item `{def_id:?}` caused errors; ignoring.")
                 }
                 // Panic
                 Err(_) => register_error!(
                     ctx,
                     span,
-                    "Thread panicked when extracting item `{rust_id:?}`."
+                    "Thread panicked when extracting item `{def_id:?}`."
                 ),
             };
         })
@@ -134,11 +134,11 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> {
 
     pub(crate) fn translate_item_aux(
         &mut self,
-        rust_id: DefId,
+        def_id: &hax::DefId,
         trans_id: Option<AnyTransId>,
     ) -> Result<(), Error> {
         // Translate the meta information
-        let name = self.def_id_to_name(rust_id)?;
+        let name = self.hax_def_id_to_name(def_id)?;
         if let Some(trans_id) = trans_id {
             self.translated.item_names.insert(trans_id, name.clone());
         }
@@ -147,11 +147,11 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> {
             // Don't even start translating the item. In particular don't call `hax_def` on it.
             return Ok(());
         }
-        let def = self.hax_def(rust_id)?;
+        let def = self.hax_def(def_id)?;
         let item_meta = self.translate_item_meta(&def, name, opacity);
 
         // Initialize the body translation context
-        let bt_ctx = ItemTransCtx::new(rust_id, trans_id, self);
+        let bt_ctx = ItemTransCtx::new(def_id.clone(), trans_id, self);
         match trans_id {
             Some(AnyTransId::Type(id)) => {
                 let ty = bt_ctx.translate_type(id, item_meta, &def)?;
@@ -265,8 +265,8 @@ pub fn translate<'tcx, 'ctx>(
     // from Rust ids to translated ids.
     while let Some(item_src) = ctx.items_to_translate.pop_first() {
         trace!("About to translate item: {:?}", item_src);
-        if ctx.processed.insert(item_src) {
-            ctx.translate_item(item_src);
+        if ctx.processed.insert(item_src.clone()) {
+            ctx.translate_item(&item_src);
         }
     }
 
diff --git a/charon/src/bin/charon-driver/translate/translate_ctx.rs b/charon/src/bin/charon-driver/translate/translate_ctx.rs
index 5e394272d..15b8362d8 100644
--- a/charon/src/bin/charon-driver/translate/translate_ctx.rs
+++ b/charon/src/bin/charon-driver/translate/translate_ctx.rs
@@ -9,7 +9,6 @@ use hax_frontend_exporter::SInto;
 use hax_frontend_exporter::{self as hax, DefPathItem};
 use itertools::Itertools;
 use macros::VariantIndexArity;
-use rustc_hir::def_id::DefId;
 use rustc_middle::ty::TyCtxt;
 use std::borrow::Cow;
 use std::cell::RefCell;
@@ -28,23 +27,23 @@ pub(crate) use charon_lib::errors::{
 /// The id of an untranslated item. Note that a given `DefId` may show up as multiple different
 /// item sources, e.g. a constant will have both a `Global` version (for the constant itself) and a
 /// `FunDecl` one (for its initializer function).
-#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash, VariantIndexArity)]
+#[derive(Clone, Debug, PartialEq, Eq, Hash, VariantIndexArity)]
 pub enum TransItemSource {
-    Global(DefId),
-    TraitDecl(DefId),
-    TraitImpl(DefId),
-    Fun(DefId),
-    Type(DefId),
+    Global(hax::DefId),
+    TraitDecl(hax::DefId),
+    TraitImpl(hax::DefId),
+    Fun(hax::DefId),
+    Type(hax::DefId),
 }
 
 impl TransItemSource {
-    pub(crate) fn to_def_id(&self) -> DefId {
+    pub(crate) fn as_def_id(&self) -> &hax::DefId {
         match self {
             TransItemSource::Global(id)
             | TransItemSource::TraitDecl(id)
             | TransItemSource::TraitImpl(id)
             | TransItemSource::Fun(id)
-            | TransItemSource::Type(id) => *id,
+            | TransItemSource::Type(id) => id,
         }
     }
 }
@@ -53,8 +52,8 @@ impl TransItemSource {
     /// Value with which we order values.
     fn sort_key(&self) -> impl Ord {
         let (variant_index, _) = self.variant_index_arity();
-        let def_id = self.to_def_id();
-        (def_id.krate, def_id.index, variant_index)
+        let def_id = self.as_def_id();
+        (def_id.index, variant_index)
     }
 }
 
@@ -99,9 +98,9 @@ pub struct TranslateCtx<'tcx> {
     /// The declaration we've already processed (successfully or not).
     pub processed: HashSet<TransItemSource>,
     /// Cache the names to compute them only once each.
-    pub cached_names: HashMap<DefId, Name>,
+    pub cached_names: HashMap<hax::DefId, Name>,
     /// Cache the `ItemMeta`s to compute them only once each.
-    pub cached_item_metas: HashMap<DefId, ItemMeta>,
+    pub cached_item_metas: HashMap<hax::DefId, ItemMeta>,
 }
 
 /// A level of binding for type-level variables. Each item has a top-level binding level
@@ -219,7 +218,7 @@ impl BindingLevel {
 pub(crate) struct ItemTransCtx<'tcx, 'ctx> {
     /// The definition we are currently extracting.
     /// TODO: this duplicates the field of [ErrorCtx]
-    pub def_id: DefId,
+    pub def_id: hax::DefId,
     /// The id of the definition we are currently extracting, if there is one.
     pub item_id: Option<AnyTransId>,
     /// The translation context containing the top-level definitions/ids.
@@ -291,9 +290,9 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> {
     fn path_elem_for_def(
         &mut self,
         span: Span,
-        def: &hax::DefId,
+        def_id: &hax::DefId,
     ) -> Result<Option<PathElem>, Error> {
-        let path_elem = def.path_item();
+        let path_elem = def_id.path_item();
         // Disambiguator disambiguates identically-named (but distinct) identifiers. This happens
         // notably with macros and inherent impl blocks.
         let disambiguator = Disambiguator::new(path_elem.disambiguator as usize);
@@ -311,7 +310,6 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> {
             | DefPathItem::ValueNs(symbol)
             | DefPathItem::MacroNs(symbol) => Some(PathElem::Ident(symbol, disambiguator)),
             DefPathItem::Impl => {
-                let def_id = def.to_rust_def_id();
                 let full_def = self.hax_def(def_id)?;
                 // Two cases, depending on whether the impl block is
                 // a "regular" impl block (`impl Foo { ... }`) or a trait
@@ -322,7 +320,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> {
                         // We need to convert the type, which may contain quantified
                         // substs and bounds. In order to properly do so, we introduce
                         // a body translation context.
-                        let mut bt_ctx = ItemTransCtx::new(def_id, None, self);
+                        let mut bt_ctx = ItemTransCtx::new(def_id.clone(), None, self);
                         bt_ctx.translate_def_generics(span, &full_def)?;
                         let ty = bt_ctx.translate_ty(span, &ty)?;
                         ImplElem::Ty(Binder {
@@ -353,10 +351,13 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> {
             // Do nothing, the constructor of a struct/variant has the same name as the
             // struct/variant.
             DefPathItem::Ctor => None,
-            DefPathItem::Use => Some(PathElem::Ident("<use>".to_string(), disambiguator)),
+            DefPathItem::Use => Some(PathElem::Ident("{use}".to_string(), disambiguator)),
             DefPathItem::AnonConst => Some(PathElem::Ident("{const}".to_string(), disambiguator)),
+            DefPathItem::PromotedConst => Some(PathElem::Ident(
+                "{promoted_const}".to_string(),
+                disambiguator,
+            )),
             _ => {
-                let def_id = def.to_rust_def_id();
                 raise_error!(
                     self,
                     span,
@@ -408,33 +409,28 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> {
     /// The names we will generate for `foo` and `bar` are:
     /// `[Ident("test"), Ident("bla"), Ident("Foo"), Impl(impl<T> Ty<T>, Disambiguator(0)), Ident("foo")]`
     /// `[Ident("test"), Ident("bla"), Ident("Foo"), Impl(impl<T> Ty<T>, Disambiguator(1)), Ident("bar")]`
-    pub fn hax_def_id_to_name(&mut self, def: &hax::DefId) -> Result<Name, Error> {
-        let def_id = def.to_rust_def_id();
+    pub fn hax_def_id_to_name(&mut self, def_id: &hax::DefId) -> Result<Name, Error> {
         if let Some(name) = self.cached_names.get(&def_id) {
             return Ok(name.clone());
         }
         trace!("Computing name for `{def_id:?}`");
 
-        let parent_name = if let Some(parent) = &def.parent {
+        let parent_name = if let Some(parent) = &def_id.parent {
             self.hax_def_id_to_name(parent)?
         } else {
             Name { name: Vec::new() }
         };
         let span = self.def_span(def_id);
         let mut name = parent_name;
-        if let Some(path_elem) = self.path_elem_for_def(span, &def)? {
+        if let Some(path_elem) = self.path_elem_for_def(span, &def_id)? {
             name.name.push(path_elem);
         }
 
         trace!("Computed name for `{def_id:?}`: `{name:?}`");
-        self.cached_names.insert(def_id, name.clone());
+        self.cached_names.insert(def_id.clone(), name.clone());
         Ok(name)
     }
 
-    pub fn def_id_to_name(&mut self, def_id: DefId) -> Result<Name, Error> {
-        self.hax_def_id_to_name(&def_id.sinto(&self.hax_state))
-    }
-
     /// Translates `T` into `U` using `hax`'s `SInto` trait, catching any hax panics.
     pub fn catch_sinto<S, T, U>(&mut self, s: &S, span: Span, x: &T) -> Result<U, Error>
     where
@@ -443,17 +439,12 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> {
         catch_sinto(s, &mut *self.errors.borrow_mut(), &self.translated, span, x)
     }
 
-    pub fn hax_def(&mut self, def_id: impl Into<DefId>) -> Result<Arc<hax::FullDef>, Error> {
-        let def_id: DefId = def_id.into();
+    pub fn hax_def(&mut self, def_id: &hax::DefId) -> Result<Arc<hax::FullDef>, Error> {
         let span = self.def_span(def_id);
         // Hax takes care of caching the translation.
-        catch_sinto(
-            &self.hax_state,
-            &mut *self.errors.borrow_mut(),
-            &self.translated,
-            span,
-            &def_id,
-        )
+        let unwind_safe_s = std::panic::AssertUnwindSafe(&self.hax_state);
+        std::panic::catch_unwind(move || def_id.full_def(*unwind_safe_s))
+            .or_else(|_| raise_error!(self, span, "Hax panicked when translating `{def_id:?}`."))
     }
 
     pub(crate) fn translate_attr_info(&mut self, def: &hax::FullDef) -> AttrInfo {
@@ -496,7 +487,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> {
         name: Name,
         name_opacity: ItemOpacity,
     ) -> ItemMeta {
-        if let Some(item_meta) = self.cached_item_metas.get(&def.rust_def_id()) {
+        if let Some(item_meta) = self.cached_item_metas.get(&def.def_id) {
             return item_meta.clone();
         }
         let span = def.source_span.as_ref().unwrap_or(&def.span);
@@ -527,7 +518,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> {
             lang_item,
         };
         self.cached_item_metas
-            .insert(def.rust_def_id(), item_meta.clone());
+            .insert(def.def_id.clone(), item_meta.clone());
         item_meta
     }
 
@@ -647,11 +638,8 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> {
         }
     }
 
-    pub(crate) fn def_span(&mut self, def_id: impl Into<DefId>) -> Span {
-        let def_id = def_id.into();
-        let def_kind = hax::get_def_kind(self.tcx, def_id);
-        let span = hax::get_def_span(self.tcx, def_id, def_kind);
-        let span = span.sinto(&self.hax_state);
+    pub(crate) fn def_span(&mut self, def_id: &hax::DefId) -> Span {
+        let span = def_id.def_span(&self.hax_state);
         self.translate_span_from_hax(&span)
     }
 
@@ -745,13 +733,13 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> {
                     }
                 };
                 // Add the id to the queue of declarations to translate
-                self.id_map.insert(id, trans_id);
-                self.reverse_id_map.insert(trans_id, id);
+                self.id_map.insert(id.clone(), trans_id);
+                self.reverse_id_map.insert(trans_id, id.clone());
                 self.translated.all_ids.insert(trans_id);
                 // Store the name early so the name matcher can identify paths. We can't to it for
                 // trait impls because they register themselves when computing their name.
                 if !matches!(id, TransItemSource::TraitImpl(_)) {
-                    if let Ok(name) = self.def_id_to_name(id.to_def_id()) {
+                    if let Ok(name) = self.hax_def_id_to_name(id.as_def_id()) {
                         self.translated.item_names.insert(trans_id, name);
                     }
                 }
@@ -760,7 +748,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> {
         };
         self.errors
             .borrow_mut()
-            .register_dep_source(src, item_id, id.to_def_id().is_local());
+            .register_dep_source(src, item_id, id.as_def_id().is_local);
         item_id
     }
 
@@ -770,17 +758,17 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> {
         src: &Option<DepSource>,
         id: TransItemSource,
     ) -> AnyTransId {
-        self.items_to_translate.insert(id);
+        self.items_to_translate.insert(id.clone());
         self.register_id_no_enqueue(src, id)
     }
 
     pub(crate) fn register_type_decl_id(
         &mut self,
         src: &Option<DepSource>,
-        id: impl Into<DefId>,
+        id: &hax::DefId,
     ) -> TypeDeclId {
         *self
-            .register_and_enqueue_id(src, TransItemSource::Type(id.into()))
+            .register_and_enqueue_id(src, TransItemSource::Type(id.clone()))
             .as_type()
             .unwrap()
     }
@@ -788,10 +776,10 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> {
     pub(crate) fn register_fun_decl_id(
         &mut self,
         src: &Option<DepSource>,
-        id: impl Into<DefId>,
+        id: &hax::DefId,
     ) -> FunDeclId {
         *self
-            .register_and_enqueue_id(src, TransItemSource::Fun(id.into()))
+            .register_and_enqueue_id(src, TransItemSource::Fun(id.clone()))
             .as_fun()
             .unwrap()
     }
@@ -799,10 +787,10 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> {
     pub(crate) fn register_trait_decl_id(
         &mut self,
         src: &Option<DepSource>,
-        id: impl Into<DefId>,
+        id: &hax::DefId,
     ) -> TraitDeclId {
         *self
-            .register_and_enqueue_id(src, TransItemSource::TraitDecl(id.into()))
+            .register_and_enqueue_id(src, TransItemSource::TraitDecl(id.clone()))
             .as_trait_decl()
             .unwrap()
     }
@@ -810,9 +798,8 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> {
     pub(crate) fn register_trait_impl_id(
         &mut self,
         src: &Option<DepSource>,
-        id: impl Into<DefId>,
+        id: &hax::DefId,
     ) -> TraitImplId {
-        let id = id.into();
         // Register the corresponding trait early so we can filter on its name.
         if let Ok(def) = self.hax_def(id) {
             let hax::FullDefKind::TraitImpl { trait_pred, .. } = def.kind() else {
@@ -823,7 +810,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> {
         }
 
         *self
-            .register_and_enqueue_id(src, TransItemSource::TraitImpl(id))
+            .register_and_enqueue_id(src, TransItemSource::TraitImpl(id.clone()))
             .as_trait_impl()
             .unwrap()
     }
@@ -831,17 +818,17 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> {
     pub(crate) fn register_global_decl_id(
         &mut self,
         src: &Option<DepSource>,
-        id: impl Into<DefId>,
+        id: &hax::DefId,
     ) -> GlobalDeclId {
         *self
-            .register_and_enqueue_id(src, TransItemSource::Global(id.into()))
+            .register_and_enqueue_id(src, TransItemSource::Global(id.clone()))
             .as_global()
             .unwrap()
     }
 
     pub(crate) fn with_def_id<F, T>(
         &mut self,
-        def_id: DefId,
+        def_id: &hax::DefId,
         item_id: Option<AnyTransId>,
         f: F,
     ) -> T
@@ -850,7 +837,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> {
     {
         let mut errors = self.errors.borrow_mut();
         let current_def_id = mem::replace(&mut errors.def_id, item_id);
-        let current_def_id_is_local = mem::replace(&mut errors.def_id_is_local, def_id.is_local());
+        let current_def_id_is_local = mem::replace(&mut errors.def_id_is_local, def_id.is_local);
         drop(errors); // important: release the refcell "lock"
         let ret = f(self);
         let mut errors = self.errors.borrow_mut();
@@ -863,7 +850,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> {
 impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> {
     /// Create a new `ExecContext`.
     pub(crate) fn new(
-        def_id: DefId,
+        def_id: hax::DefId,
         item_id: Option<AnyTransId>,
         t_ctx: &'ctx mut TranslateCtx<'tcx>,
     ) -> Self {
@@ -886,11 +873,11 @@ impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> {
         self.t_ctx.translate_span_from_hax(rspan)
     }
 
-    pub(crate) fn hax_def(&mut self, def_id: impl Into<DefId>) -> Result<Arc<hax::FullDef>, Error> {
-        self.t_ctx.hax_def(def_id.into())
+    pub(crate) fn hax_def(&mut self, def_id: &hax::DefId) -> Result<Arc<hax::FullDef>, Error> {
+        self.t_ctx.hax_def(def_id)
     }
 
-    pub(crate) fn def_span(&mut self, def_id: impl Into<DefId>) -> Span {
+    pub(crate) fn def_span(&mut self, def_id: &hax::DefId) -> Span {
         self.t_ctx.def_span(def_id)
     }
 
@@ -899,12 +886,12 @@ impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> {
         self.t_ctx.register_id_no_enqueue(&src, id)
     }
 
-    pub(crate) fn register_type_decl_id(&mut self, span: Span, id: impl Into<DefId>) -> TypeDeclId {
+    pub(crate) fn register_type_decl_id(&mut self, span: Span, id: &hax::DefId) -> TypeDeclId {
         let src = self.make_dep_source(span);
         self.t_ctx.register_type_decl_id(&src, id)
     }
 
-    pub(crate) fn register_fun_decl_id(&mut self, span: Span, id: impl Into<DefId>) -> FunDeclId {
+    pub(crate) fn register_fun_decl_id(&mut self, span: Span, id: &hax::DefId) -> FunDeclId {
         let src = self.make_dep_source(span);
         self.t_ctx.register_fun_decl_id(&src, id)
     }
@@ -912,41 +899,29 @@ impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> {
     pub(crate) fn register_fun_decl_id_no_enqueue(
         &mut self,
         span: Span,
-        id: impl Into<DefId>,
+        id: &hax::DefId,
     ) -> FunDeclId {
-        self.register_id_no_enqueue(span, TransItemSource::Fun(id.into()))
+        self.register_id_no_enqueue(span, TransItemSource::Fun(id.clone()))
             .as_fun()
             .copied()
             .unwrap()
     }
 
-    pub(crate) fn register_global_decl_id(
-        &mut self,
-        span: Span,
-        id: impl Into<DefId>,
-    ) -> GlobalDeclId {
+    pub(crate) fn register_global_decl_id(&mut self, span: Span, id: &hax::DefId) -> GlobalDeclId {
         let src = self.make_dep_source(span);
         self.t_ctx.register_global_decl_id(&src, id)
     }
 
     /// Returns an [Option] because we may ignore some builtin or auto traits
     /// like [core::marker::Sized] or [core::marker::Sync].
-    pub(crate) fn register_trait_decl_id(
-        &mut self,
-        span: Span,
-        id: impl Into<DefId>,
-    ) -> TraitDeclId {
+    pub(crate) fn register_trait_decl_id(&mut self, span: Span, id: &hax::DefId) -> TraitDeclId {
         let src = self.make_dep_source(span);
         self.t_ctx.register_trait_decl_id(&src, id)
     }
 
     /// Returns an [Option] because we may ignore some builtin or auto traits
     /// like [core::marker::Sized] or [core::marker::Sync].
-    pub(crate) fn register_trait_impl_id(
-        &mut self,
-        span: Span,
-        id: impl Into<DefId>,
-    ) -> TraitImplId {
+    pub(crate) fn register_trait_impl_id(&mut self, span: Span, id: &hax::DefId) -> TraitImplId {
         let src = self.make_dep_source(span);
         self.t_ctx.register_trait_impl_id(&src, id)
     }
@@ -1158,7 +1133,7 @@ impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> {
     pub(crate) fn make_dep_source(&self, span: Span) -> Option<DepSource> {
         Some(DepSource {
             src_id: self.item_id?,
-            span: self.def_id.is_local().then_some(span),
+            span: self.def_id.is_local.then_some(span),
         })
     }
 }
diff --git a/charon/src/bin/charon-driver/translate/translate_functions_to_ullbc.rs b/charon/src/bin/charon-driver/translate/translate_functions_to_ullbc.rs
index 04db12bc9..b231647f4 100644
--- a/charon/src/bin/charon-driver/translate/translate_functions_to_ullbc.rs
+++ b/charon/src/bin/charon-driver/translate/translate_functions_to_ullbc.rs
@@ -138,6 +138,7 @@ impl ItemTransCtx<'_, '_> {
             | hax::FullDefKind::AssocConst { ty, .. }
             | hax::FullDefKind::AnonConst { ty, .. }
             | hax::FullDefKind::InlineConst { ty, .. }
+            | hax::FullDefKind::PromotedConst { ty, .. }
             | hax::FullDefKind::Static { ty, .. } => {
                 let sig = hax::TyFnSig {
                     inputs: vec![],
@@ -397,6 +398,7 @@ impl ItemTransCtx<'_, '_> {
                 | hax::FullDefKind::AssocConst { .. }
                 | hax::FullDefKind::AnonConst { .. }
                 | hax::FullDefKind::InlineConst { .. }
+                | hax::FullDefKind::PromotedConst { .. }
                 | hax::FullDefKind::Static { .. }
         );
         let is_global_initializer =
@@ -477,6 +479,7 @@ impl ItemTransCtx<'_, '_> {
             | hax::FullDefKind::AssocConst { ty, .. }
             | hax::FullDefKind::AnonConst { ty, .. }
             | hax::FullDefKind::InlineConst { ty, .. }
+            | hax::FullDefKind::PromotedConst { ty, .. }
             | hax::FullDefKind::Static { ty, .. } => ty,
             _ => panic!("Unexpected def for constant: {def:?}"),
         };
@@ -487,9 +490,9 @@ impl ItemTransCtx<'_, '_> {
             hax::FullDefKind::Const { .. } | hax::FullDefKind::AssocConst { .. } => {
                 GlobalKind::NamedConst
             }
-            hax::FullDefKind::AnonConst { .. } | hax::FullDefKind::InlineConst { .. } => {
-                GlobalKind::AnonConst
-            }
+            hax::FullDefKind::AnonConst { .. }
+            | hax::FullDefKind::InlineConst { .. }
+            | hax::FullDefKind::PromotedConst { .. } => GlobalKind::AnonConst,
             _ => panic!("Unexpected def for constant: {def:?}"),
         };
 
diff --git a/charon/src/bin/charon-driver/translate/translate_traits.rs b/charon/src/bin/charon-driver/translate/translate_traits.rs
index 15216010a..39d626af1 100644
--- a/charon/src/bin/charon-driver/translate/translate_traits.rs
+++ b/charon/src/bin/charon-driver/translate/translate_traits.rs
@@ -253,8 +253,8 @@ impl ItemTransCtx<'_, '_> {
             use hax::ImplAssocItemValue::*;
             let name = TraitItemName(impl_item.name.clone());
             let item_def = impl_item.def(); // The impl item or the corresponding trait default.
-            let item_span = self.def_span(item_def.rust_def_id());
-            let item_def_id = item_def.rust_def_id();
+            let item_span = self.def_span(&item_def.def_id);
+            let item_def_id = &item_def.def_id;
             match item_def.kind() {
                 hax::FullDefKind::AssocFn { .. } => {
                     match &impl_item.value {
diff --git a/charon/src/bin/charon-driver/translate/translate_types.rs b/charon/src/bin/charon-driver/translate/translate_types.rs
index 9c20d2cd2..9b7581850 100644
--- a/charon/src/bin/charon-driver/translate/translate_types.rs
+++ b/charon/src/bin/charon-driver/translate/translate_types.rs
@@ -621,6 +621,7 @@ impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> {
             | FullDefKind::AssocConst { .. }
             | FullDefKind::AnonConst { .. }
             | FullDefKind::InlineConst { .. }
+            | FullDefKind::PromotedConst { .. }
             | FullDefKind::Closure { .. }
             | FullDefKind::Ctor { .. }
             | FullDefKind::Variant { .. } => {
@@ -672,6 +673,7 @@ impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> {
                 | FullDefKind::AssocConst { .. }
                 | FullDefKind::AnonConst { .. }
                 | FullDefKind::InlineConst { .. }
+                | FullDefKind::PromotedConst { .. }
                 | FullDefKind::Static { .. } => PredicateOrigin::WhereClauseOnFn,
                 FullDefKind::TraitImpl { .. } | FullDefKind::InherentImpl { .. } => {
                     PredicateOrigin::WhereClauseOnImpl
diff --git a/charon/src/ids/generator.rs b/charon/src/ids/generator.rs
index 9b917f6bb..12d1922f4 100644
--- a/charon/src/ids/generator.rs
+++ b/charon/src/ids/generator.rs
@@ -19,14 +19,25 @@ impl<I: Idx> Generator<I> {
         }
     }
 
+    /// Get a fresh id from this generator.
     pub fn fresh_id(&mut self) -> I {
-        let index = I::from_usize(self.counter);
+        let index = self.next_id();
+        self.advance(1);
+        index
+    }
+
+    /// Get the next id that would be emitted by `fresh_id`.
+    pub fn next_id(&self) -> I {
+        I::from_usize(self.counter)
+    }
+
+    /// Move the generator forward by the given delta.
+    pub fn advance(&mut self, by: usize) {
         // The release version of the code doesn't check for overflows.
         // As the max usize is very large, overflows are extremely
         // unlikely. Still, it is extremely important for our code that
         // no overflows happen on the index counters.
-        self.counter = self.counter.checked_add(1).unwrap();
-        index
+        self.counter = self.counter.checked_add(by).unwrap();
     }
 }
 
diff --git a/charon/src/ids/vector.rs b/charon/src/ids/vector.rs
index dbc354e25..d7e85c2e7 100644
--- a/charon/src/ids/vector.rs
+++ b/charon/src/ids/vector.rs
@@ -11,6 +11,7 @@ use index_vec::{Idx, IdxSliceIndex, IndexVec};
 use serde::{Deserialize, Serialize, Serializer};
 use std::{
     iter::{FromIterator, IntoIterator},
+    mem,
     ops::{ControlFlow, Deref, Index, IndexMut},
 };
 
@@ -264,15 +265,29 @@ where
         self.vector.indices()
     }
 
-    pub fn retain(&mut self, mut f: impl FnMut(&mut T) -> bool) {
-        self.vector.iter_mut().for_each(|opt| {
-            if let Some(x) = opt {
-                if !f(x) {
-                    *opt = None;
-                    self.elem_count -= 1;
+    /// Remove matching items and return and iterator over the removed items. This is lazy: items
+    /// are only removed as the iterator is consumed.
+    pub fn extract<'a, F: FnMut(&mut T) -> bool>(
+        &'a mut self,
+        mut f: F,
+    ) -> impl Iterator<Item = (I, T)> + use<'a, I, T, F> {
+        let elem_count = &mut self.elem_count;
+        self.vector
+            .iter_mut_enumerated()
+            .filter_map(move |(i, opt)| {
+                if f(opt.as_mut()?) {
+                    *elem_count -= 1;
+                    let elem = mem::replace(opt, None)?;
+                    Some((i, elem))
+                } else {
+                    None
                 }
-            }
-        });
+            })
+    }
+
+    /// Remove the elements that don't match the predicate.
+    pub fn retain(&mut self, mut f: impl FnMut(&mut T) -> bool) {
+        self.extract(|x| !f(x)).for_each(drop);
     }
 
     /// Like `Vec::split_off`.
diff --git a/charon/src/transform/inline_promoted_consts.rs b/charon/src/transform/inline_promoted_consts.rs
new file mode 100644
index 000000000..50ecd8cdd
--- /dev/null
+++ b/charon/src/transform/inline_promoted_consts.rs
@@ -0,0 +1,95 @@
+use std::{collections::HashMap, mem};
+
+use super::{ctx::UllbcPass, TransformCtx};
+use crate::{ids::Generator, ullbc_ast::*};
+
+pub struct Transform;
+impl UllbcPass for Transform {
+    fn transform_ctx(&self, ctx: &mut TransformCtx) {
+        // Currently the only anon consts that are not already evaluated are promoted consts. If
+        // that changes, we'll have to restrict this pass to the consts that can be inlined into a
+        // body.
+
+        // Map each anon const id to its initializer, and remove both from `translated`.
+        let anon_consts: HashMap<GlobalDeclId, ExprBody> = ctx
+            .translated
+            .global_decls
+            .extract(|gdecl| matches!(gdecl.global_kind, GlobalKind::AnonConst))
+            .filter_map(|(id, gdecl)| {
+                let fdecl = ctx.translated.fun_decls.remove(gdecl.init)?;
+                let body = fdecl.body.ok()?;
+                let body = body.to_unstructured()?;
+                Some((id, body))
+            })
+            .collect();
+
+        ctx.for_each_fun_decl(|_ctx, decl| {
+            if let Ok(outer_body) = &mut decl.body {
+                let outer_body = outer_body.as_unstructured_mut().unwrap();
+                for block_id in outer_body.body.all_indices() {
+                    // Subtle: This generator must be managed to correctly track the indices that will
+                    // be generated when pushing onto `outer_body.body`.
+                    let mut bid_generator =
+                        Generator::new_with_init_value(outer_body.body.next_id());
+                    let start_new_bodies = bid_generator.next_id();
+                    let Some(block) = outer_body.body.get_mut(block_id) else {
+                        continue;
+                    };
+                    let mut new_blocks = vec![];
+                    block.dyn_visit_in_body_mut(|op: &mut Operand| {
+                        if let Operand::Const(c) = op
+                            && let RawConstantExpr::Global(gref) = &mut c.value
+                            && let Some(inner_body) = anon_consts.get(&gref.id)
+                        {
+                            // We inline the required body by shifting its local ids and block ids
+                            // and adding its blocks to the outer body. The inner body's return
+                            // local becomes a normal local that we can read from. We redirect some
+                            // gotos so that the inner body is executed before the current block.
+                            let mut inner_body = inner_body.clone().substitute(&gref.generics);
+
+                            let return_local = outer_body.locals.locals.next_id();
+                            inner_body.dyn_visit_in_body_mut(|l: &mut LocalId| {
+                                *l += return_local;
+                            });
+
+                            let start_block = bid_generator.next_id();
+                            bid_generator.advance(inner_body.body.elem_count());
+                            let end_block = bid_generator.next_id();
+                            inner_body.dyn_visit_in_body_mut(|b: &mut BlockId| {
+                                *b += start_block;
+                            });
+                            // Make all returns point to `end_block`. This block doesn't exist yet,
+                            // it will either be the start block of another inner body, or the
+                            // current outer block that we'll push at the end.
+                            inner_body.body.dyn_visit_in_body_mut(|t: &mut Terminator| {
+                                if let RawTerminator::Return = t.content {
+                                    t.content = RawTerminator::Goto { target: end_block };
+                                }
+                            });
+
+                            outer_body
+                                .locals
+                                .locals
+                                .extend(inner_body.locals.locals.into_iter());
+                            new_blocks.extend(inner_body.body);
+                            *op = Operand::Move(outer_body.locals.place_for_var(return_local));
+                        }
+                    });
+                    if !new_blocks.is_empty() {
+                        // Instead of the current block, start evaluating the new bodies.
+                        let block = mem::replace(
+                            block,
+                            BlockData::new_goto(Span::dummy(), start_new_bodies),
+                        );
+                        // Add the new blocks. They've been set up so that each new inner body
+                        // returns to what follows it in the sequence. Hence the last added body
+                        // points to the not-yet-existing block at `start_new_bodies`
+                        outer_body.body.extend(new_blocks.into_iter());
+                        // Push the current block to be executed after the newly-added ones.
+                        outer_body.body.push(block);
+                    }
+                }
+            }
+        });
+    }
+}
diff --git a/charon/src/transform/mod.rs b/charon/src/transform/mod.rs
index 03a050d47..74de69246 100644
--- a/charon/src/transform/mod.rs
+++ b/charon/src/transform/mod.rs
@@ -10,6 +10,7 @@ pub mod hide_marker_traits;
 pub mod index_intermediate_assigns;
 pub mod index_to_function_calls;
 pub mod inline_local_panic_functions;
+pub mod inline_promoted_consts;
 pub mod insert_assign_return_unit;
 pub mod insert_storage_lives;
 pub mod lift_associated_item_clauses;
@@ -65,6 +66,8 @@ pub static INITIAL_CLEANUP_PASSES: &[Pass] = &[
 
 /// Body cleanup passes on the ullbc.
 pub static ULLBC_PASSES: &[Pass] = &[
+    // Inline promoted consts into their parent bodies.
+    UnstructuredBody(&inline_promoted_consts::Transform),
     // # Micro-pass: merge single-origin gotos into their parent. This drastically reduces the
     // graph size of the CFG.
     UnstructuredBody(&merge_goto_chains::Transform),
diff --git a/charon/tests/ui/simple/multiple-promoteds.out b/charon/tests/ui/simple/multiple-promoteds.out
new file mode 100644
index 000000000..fb7e82eb5
--- /dev/null
+++ b/charon/tests/ui/simple/multiple-promoteds.out
@@ -0,0 +1,87 @@
+# Final LLBC before serialization:
+
+pub fn core::ops::arith::{impl core::ops::arith::Add<&'_0 (u32)> for &'_1 (u32)}#27::add<'_0, '_1>(@1: &'_1 (u32), @2: &'_0 (u32)) -> u32
+
+fn test_crate::six() -> u32
+{
+    let @0: u32; // return
+    let x@1: &'_ (u32); // local
+    let y@2: &'_ (u32); // local
+    let @3: &'_ (u32); // anonymous local
+    let @4: &'_ (u32); // anonymous local
+    let @5: &'_ (u32); // anonymous local
+    let @6: &'_ (u32); // anonymous local
+    let @7: &'_ (u32); // anonymous local
+    let @8: u32; // anonymous local
+    let @9: (u32, bool); // anonymous local
+    let @10: &'_ (u32); // anonymous local
+    let @11: u32; // anonymous local
+    let @12: (u32, bool); // anonymous local
+
+    storage_live(@5)
+    storage_live(@6)
+    storage_live(@7)
+    storage_live(@8)
+    storage_live(@9)
+    storage_live(@10)
+    storage_live(@11)
+    storage_live(@12)
+    storage_live(x@1)
+    @9 := const (0 : u32) checked.+ const (1 : u32)
+    @8 := move ((@9).0)
+    @7 := &@8
+    @6 := move (@7)
+    x@1 := &*(@6)
+    storage_live(y@2)
+    @12 := const (2 : u32) checked.+ const (3 : u32)
+    @11 := move ((@12).0)
+    @10 := &@11
+    @5 := move (@10)
+    y@2 := &*(@5)
+    storage_live(@3)
+    @3 := copy (x@1)
+    storage_live(@4)
+    @4 := copy (y@2)
+    @0 := core::ops::arith::{impl core::ops::arith::Add<&'_0 (u32)> for &'_1 (u32)}#27::add<'_, '_>(move (@3), move (@4))
+    storage_dead(@4)
+    storage_dead(@3)
+    storage_dead(y@2)
+    storage_dead(x@1)
+    return
+}
+
+#[lang_item("sized")]
+pub trait core::marker::Sized<Self>
+
+#[lang_item("add")]
+pub trait core::ops::arith::Add<Self, Rhs>
+{
+    parent_clause0 : [@TraitClause0]: core::marker::Sized<Rhs>
+    parent_clause1 : [@TraitClause1]: core::marker::Sized<Self::Output>
+    type Output
+    fn add = core::ops::arith::Add::add<Self, Rhs>
+}
+
+#[lang_item("add")]
+pub fn core::ops::arith::Add::add<Self, Rhs>(@1: Self, @2: Rhs) -> Self::Output
+
+impl core::ops::arith::{impl core::ops::arith::Add<&'_0 (u32)> for &'_1 (u32)}#27<'_0, '_1> : core::ops::arith::Add<&'_1 (u32), &'_0 (u32)>
+{
+    parent_clause0 = core::marker::Sized<&'_ (u32)>
+    parent_clause1 = core::marker::Sized<u32>
+    type Output = u32
+    fn add = core::ops::arith::{impl core::ops::arith::Add<&'_0 (u32)> for &'_1 (u32)}#27::add<'_0, '_1>
+}
+
+pub fn core::ops::arith::{impl core::ops::arith::Add<u32> for u32}#3::add(@1: u32, @2: u32) -> u32
+
+impl core::ops::arith::{impl core::ops::arith::Add<u32> for u32}#3 : core::ops::arith::Add<u32, u32>
+{
+    parent_clause0 = core::marker::Sized<u32>
+    parent_clause1 = core::marker::Sized<u32>
+    type Output = u32
+    fn add = core::ops::arith::{impl core::ops::arith::Add<u32> for u32}#3::add
+}
+
+
+
diff --git a/charon/tests/ui/simple/multiple-promoteds.rs b/charon/tests/ui/simple/multiple-promoteds.rs
new file mode 100644
index 000000000..a384cd53e
--- /dev/null
+++ b/charon/tests/ui/simple/multiple-promoteds.rs
@@ -0,0 +1,6 @@
+//@ charon-args=--mir_optimized
+fn six() -> u32 {
+    let x = &(0 + 1);
+    let y = &(2 + 3);
+    x + y
+}
diff --git a/charon/tests/ui/simple/nested-inline-const.out b/charon/tests/ui/simple/nested-inline-const.out
new file mode 100644
index 000000000..7cbc14456
--- /dev/null
+++ b/charon/tests/ui/simple/nested-inline-const.out
@@ -0,0 +1,17 @@
+# Final LLBC before serialization:
+
+fn test_crate::main()
+{
+    let @0: (); // return
+    let @1: i32; // anonymous local
+
+    storage_live(@1)
+    @1 := const (1 : i32) + const (9 : i32)
+    storage_dead(@1)
+    @0 := ()
+    @0 := ()
+    return
+}
+
+
+
diff --git a/charon/tests/ui/simple/nested-inline-const.rs b/charon/tests/ui/simple/nested-inline-const.rs
new file mode 100644
index 000000000..7c97dd0c6
--- /dev/null
+++ b/charon/tests/ui/simple/nested-inline-const.rs
@@ -0,0 +1,3 @@
+fn main() {
+    let _ = 1 + const { 2 + const { 3 + 4 } };
+}
diff --git a/charon/tests/ui/simple/promoted-closure-no-warns.out b/charon/tests/ui/simple/promoted-closure-no-warns.out
index ec62af9e5..ca78b29c7 100644
--- a/charon/tests/ui/simple/promoted-closure-no-warns.out
+++ b/charon/tests/ui/simple/promoted-closure-no-warns.out
@@ -16,17 +16,17 @@ pub fn test_crate::foo() -> &'static (test_crate::foo::closure)
     let @1: &'_ (test_crate::foo::closure); // anonymous local
     let @2: &'_ (test_crate::foo::closure); // anonymous local
     let @3: &'_ (test_crate::foo::closure); // anonymous local
-    let @4: test_crate::foo::closure; // anonymous local
-    let @5: &'_ (test_crate::foo::closure); // anonymous local
+    let @4: &'_ (test_crate::foo::closure); // anonymous local
+    let @5: test_crate::foo::closure; // anonymous local
 
     storage_live(@3)
     storage_live(@4)
     storage_live(@5)
+    @5 := {test_crate::foo::closure} {}
+    @4 := &@5
     storage_live(@1)
     storage_live(@2)
-    @4 := const (Opaque(Unhandled type))
-    @5 := &@4
-    @3 := move (@5)
+    @3 := move (@4)
     @2 := &*(@3)
     @1 := &*(@2)
     @0 := &*(@1)
diff --git a/charon/tests/ui/simple/promoted-closure.out b/charon/tests/ui/simple/promoted-closure.out
index dcc53a12b..ca78b29c7 100644
--- a/charon/tests/ui/simple/promoted-closure.out
+++ b/charon/tests/ui/simple/promoted-closure.out
@@ -1,7 +1,39 @@
-error: Unsupported constant: "Unhandled type"
- --> tests/ui/simple/promoted-closure.rs:4:5
-  |
-4 |     &|x: u32| x
-  |     ^^^^^^^^^^^
+# Final LLBC before serialization:
+
+fn test_crate::foo::closure<'_0>(@1: &'_0 (()), @2: u32) -> u32
+{
+    let @0: u32; // return
+    let state@1: &'_0 (()); // arg #1
+    let x@2: u32; // arg #2
+
+    @0 := copy (x@2)
+    return
+}
+
+pub fn test_crate::foo() -> &'static (test_crate::foo::closure)
+{
+    let @0: &'_ (test_crate::foo::closure); // return
+    let @1: &'_ (test_crate::foo::closure); // anonymous local
+    let @2: &'_ (test_crate::foo::closure); // anonymous local
+    let @3: &'_ (test_crate::foo::closure); // anonymous local
+    let @4: &'_ (test_crate::foo::closure); // anonymous local
+    let @5: test_crate::foo::closure; // anonymous local
+
+    storage_live(@3)
+    storage_live(@4)
+    storage_live(@5)
+    @5 := {test_crate::foo::closure} {}
+    @4 := &@5
+    storage_live(@1)
+    storage_live(@2)
+    @3 := move (@4)
+    @2 := &*(@3)
+    @1 := &*(@2)
+    @0 := &*(@1)
+    storage_dead(@2)
+    storage_dead(@1)
+    return
+}
+
+
 
-ERROR Charon failed to translate this code (1 errors)
diff --git a/charon/tests/ui/simple/promoted-closure.rs b/charon/tests/ui/simple/promoted-closure.rs
index f9c978ec3..e3e5aba04 100644
--- a/charon/tests/ui/simple/promoted-closure.rs
+++ b/charon/tests/ui/simple/promoted-closure.rs
@@ -1,4 +1,3 @@
-//@ known-failure
 //@ charon-args=--mir_optimized
 pub fn foo() -> &'static impl Fn(u32) -> u32 {
     &|x: u32| x
diff --git a/charon/tests/ui/simple/promoted-in-generic-fn.out b/charon/tests/ui/simple/promoted-in-generic-fn.out
index da81876ce..e1156b897 100644
--- a/charon/tests/ui/simple/promoted-in-generic-fn.out
+++ b/charon/tests/ui/simple/promoted-in-generic-fn.out
@@ -1,7 +1,37 @@
-error: Cannot translate unevaluated constant: PromotedConstant { def_id: test_crate::f, promoted_id: PromotedId { id: 0 }, args: [Type(Ty { kind: Node { id: Id { id: 8 }, value: Param(ParamTy { index: 0, name: "T" }) } })], mir: MirBody { span: Span { lo: Loc { line: 5, col: 12 }, hi: Loc { line: 5, col: 27 }, filename: Real(LocalPath("tests/ui/simple/promoted-in-generic-fn.rs")), rust_span_data: Some(tests/ui/simple/promoted-in-generic-fn.rs:5:13: 5:28 (#0)) }, local_decls: IndexVec { raw: [LocalDecl { mutability: true, ty: Ty { kind: Node { id: Id { id: 11 }, value: Ref(Region { kind: ReErased }, Ty { kind: Node { id: Id { id: 10 }, value: Uint(Usize) } }, false) } }, source_info: SourceInfo { span: Span { lo: Loc { line: 5, col: 12 }, hi: Loc { line: 5, col: 27 }, filename: Real(LocalPath("tests/ui/simple/promoted-in-generic-fn.rs")), rust_span_data: Some(tests/ui/simple/promoted-in-generic-fn.rs:5:13: 5:28 (#0)) }, scope: SourceScope(0) }, name: None }, LocalDecl { mutability: true, ty: Ty { kind: Node { id: Id { id: 10 }, value: Uint(Usize) } }, source_info: SourceInfo { span: Span { lo: Loc { line: 5, col: 13 }, hi: Loc { line: 5, col: 27 }, filename: Real(LocalPath("tests/ui/simple/promoted-in-generic-fn.rs")), rust_span_data: Some(tests/ui/simple/promoted-in-generic-fn.rs:5:14: 5:28 (#0)) }, scope: SourceScope(0) }, name: None }], _marker: PhantomData<fn(&hax_frontend_exporter::types::mir::Local)> }, arg_count: 0, basic_blocks: IndexVec { raw: [BasicBlockData { statements: [], terminator: Some(Terminator { source_info: SourceInfo { span: Span { lo: Loc { line: 5, col: 13 }, hi: Loc { line: 5, col: 27 }, filename: Real(LocalPath("tests/ui/simple/promoted-in-generic-fn.rs")), rust_span_data: Some(tests/ui/simple/promoted-in-generic-fn.rs:5:14: 5:28 (#0)) }, scope: SourceScope(0) }, kind: Call { fun: Static { def_id: core::mem::size_of, trait_info: None, generics: [Type(Ty { kind: Node { id: Id { id: 8 }, value: Param(ParamTy { index: 0, name: "T" }) } })], trait_refs: [ImplExpr { trait: Binder { value: TraitRef { def_id: core::marker::Sized, generic_args: [Type(Ty { kind: Node { id: Id { id: 8 }, value: Param(ParamTy { index: 0, name: "T" }) } })] }, bound_vars: [] }, impl: LocalBound { predicate_id: PredicateId(14649509712428509623), index: 0, trait: Binder { value: TraitRef { def_id: core::marker::Sized, generic_args: [Type(Ty { kind: Node { id: Id { id: 8 }, value: Param(ParamTy { index: 0, name: "T" }) } })] }, bound_vars: [] }, path: [] } }] }, late_bound_generics: [], args: [], destination: Place { ty: Ty { kind: Node { id: Id { id: 10 }, value: Uint(Usize) } }, kind: Local(Local(1)) }, target: Some(BasicBlock(1)), unwind: UnwindAction { todo: "Continue" }, fn_span: Span { lo: Loc { line: 5, col: 13 }, hi: Loc { line: 5, col: 27 }, filename: Real(LocalPath("tests/ui/simple/promoted-in-generic-fn.rs")), rust_span_data: Some(tests/ui/simple/promoted-in-generic-fn.rs:5:14: 5:28 (#0)) } } }), is_cleanup: false }, BasicBlockData { statements: [Statement { source_info: SourceInfo { span: Span { lo: Loc { line: 5, col: 12 }, hi: Loc { line: 5, col: 27 }, filename: Real(LocalPath("tests/ui/simple/promoted-in-generic-fn.rs")), rust_span_data: Some(tests/ui/simple/promoted-in-generic-fn.rs:5:13: 5:28 (#0)) }, scope: SourceScope(0) }, kind: Assign((Place { ty: Ty { kind: Node { id: Id { id: 11 }, value: Ref(Region { kind: ReErased }, Ty { kind: Node { id: Id { id: 10 }, value: Uint(Usize) } }, false) } }, kind: Local(Local(0)) }, Ref(Region { kind: ReErased }, Shared, Place { ty: Ty { kind: Node { id: Id { id: 10 }, value: Uint(Usize) } }, kind: Local(Local(1)) }))) }], terminator: Some(Terminator { source_info: SourceInfo { span: Span { lo: Loc { line: 5, col: 12 }, hi: Loc { line: 5, col: 27 }, filename: Real(LocalPath("tests/ui/simple/promoted-in-generic-fn.rs")), rust_span_data: Some(tests/ui/simple/promoted-in-generic-fn.rs:5:13: 5:28 (#0)) }, scope: SourceScope(0) }, kind: Return }), is_cleanup: false }], _marker: PhantomData<fn(&hax_frontend_exporter::types::mir::BasicBlock)> }, source_scopes: IndexVec { raw: [SourceScopeData { span: Span { lo: Loc { line: 3, col: 0 }, hi: Loc { line: 6, col: 1 }, filename: Real(LocalPath("tests/ui/simple/promoted-in-generic-fn.rs")), rust_span_data: Some(tests/ui/simple/promoted-in-generic-fn.rs:3:1: 6:2 (#0)) }, parent_scope: None, inlined_parent_scope: None }], _marker: PhantomData<fn(&hax_frontend_exporter::types::mir::SourceScope)> }, tainted_by_errors: None, _kind: PhantomData<()> } }
- --> tests/ui/simple/promoted-in-generic-fn.rs:5:13
-  |
-5 |     let _ = &size_of::<T>();
-  |             ^^^^^^^^^^^^^^^
+# Final LLBC before serialization:
+
+#[lang_item("sized")]
+pub trait core::marker::Sized<Self>
+
+#[lang_item("mem_size_of")]
+pub fn core::mem::size_of<T>() -> usize
+where
+    [@TraitClause0]: core::marker::Sized<T>,
+
+fn test_crate::f<T>()
+where
+    [@TraitClause0]: core::marker::Sized<T>,
+{
+    let @0: (); // return
+    let @1: &'_ (usize); // anonymous local
+    let @2: &'_ (usize); // anonymous local
+    let @3: &'_ (usize); // anonymous local
+    let @4: usize; // anonymous local
+
+    storage_live(@2)
+    storage_live(@3)
+    storage_live(@4)
+    // This can't be evaluated generically.
+    @4 := core::mem::size_of<T>[@TraitClause0]()
+    @3 := &@4
+    storage_live(@1)
+    @2 := move (@3)
+    @1 := &*(@2)
+    storage_dead(@1)
+    @0 := ()
+    @0 := ()
+    return
+}
+
+
 
-ERROR Charon failed to translate this code (1 errors)
diff --git a/charon/tests/ui/simple/promoted-in-generic-fn.rs b/charon/tests/ui/simple/promoted-in-generic-fn.rs
index 5dd5d5493..a5258da45 100644
--- a/charon/tests/ui/simple/promoted-in-generic-fn.rs
+++ b/charon/tests/ui/simple/promoted-in-generic-fn.rs
@@ -1,4 +1,3 @@
-//@ known-failure
 //@ charon-args=--mir_promoted
 fn f<T>() {
     // This can't be evaluated generically.
diff --git a/charon/tests/ui/simple/promoted-literal-addition-overflow.out b/charon/tests/ui/simple/promoted-literal-addition-overflow.out
index 4390c2362..59980d1cf 100644
--- a/charon/tests/ui/simple/promoted-literal-addition-overflow.out
+++ b/charon/tests/ui/simple/promoted-literal-addition-overflow.out
@@ -1,29 +1,35 @@
 # Final LLBC before serialization:
 
+pub fn core::num::{u32}#8::MAX() -> u32
+
+pub const core::num::{u32}#8::MAX: u32 = core::num::{u32}#8::MAX()
+
 fn test_crate::overflow() -> &'static (u32)
 {
     let @0: &'_ (u32); // return
     let @1: &'_ (u32); // anonymous local
     let @2: &'_ (u32); // anonymous local
-    let @3: u32; // anonymous local
-    let @4: &'_ (u32); // anonymous local
+    let @3: &'_ (u32); // anonymous local
+    let @4: u32; // anonymous local
+    let @5: (u32, bool); // anonymous local
+    let @6: u32; // anonymous local
 
     storage_live(@2)
     storage_live(@3)
     storage_live(@4)
+    storage_live(@5)
+    storage_live(@6)
     storage_live(@1)
-    @3 := const (0 : u32)
-    @4 := &@3
-    @2 := move (@4)
+    @6 := core::num::{u32}#8::MAX
+    @5 := move (@6) checked.+ const (1 : u32)
+    @4 := move ((@5).0)
+    @3 := &@4
+    @2 := move (@3)
     @1 := &*(@2)
     @0 := &*(@1)
     storage_dead(@1)
     return
 }
 
-pub fn core::num::{u32}#8::MAX() -> u32
-
-pub const core::num::{u32}#8::MAX: u32 = core::num::{u32}#8::MAX()
-
 
 
diff --git a/charon/tests/ui/simple/promoted-literal-addition.out b/charon/tests/ui/simple/promoted-literal-addition.out
index e1df056ee..ae0cecad9 100644
--- a/charon/tests/ui/simple/promoted-literal-addition.out
+++ b/charon/tests/ui/simple/promoted-literal-addition.out
@@ -5,16 +5,19 @@ fn test_crate::two() -> &'static (u32)
     let @0: &'_ (u32); // return
     let @1: &'_ (u32); // anonymous local
     let @2: &'_ (u32); // anonymous local
-    let @3: u32; // anonymous local
-    let @4: &'_ (u32); // anonymous local
+    let @3: &'_ (u32); // anonymous local
+    let @4: u32; // anonymous local
+    let @5: (u32, bool); // anonymous local
 
     storage_live(@2)
     storage_live(@3)
     storage_live(@4)
+    storage_live(@5)
     storage_live(@1)
-    @3 := const (2 : u32)
-    @4 := &@3
-    @2 := move (@4)
+    @5 := const (1 : u32) checked.+ const (1 : u32)
+    @4 := move ((@5).0)
+    @3 := &@4
+    @2 := move (@3)
     @1 := &*(@2)
     @0 := &*(@1)
     storage_dead(@1)
diff --git a/charon/tests/ui/simple/promoted-u32-slice.out b/charon/tests/ui/simple/promoted-u32-slice.out
index a03369da1..fc2feeb2e 100644
--- a/charon/tests/ui/simple/promoted-u32-slice.out
+++ b/charon/tests/ui/simple/promoted-u32-slice.out
@@ -6,17 +6,17 @@ pub fn test_crate::foo() -> &'static (Slice<u32>)
     let @1: &'_ (Array<u32, 4 : usize>); // anonymous local
     let @2: &'_ (Array<u32, 4 : usize>); // anonymous local
     let @3: &'_ (Array<u32, 4 : usize>); // anonymous local
-    let @4: Array<u32, 4 : usize>; // anonymous local
-    let @5: &'_ (Array<u32, 4 : usize>); // anonymous local
+    let @4: &'_ (Array<u32, 4 : usize>); // anonymous local
+    let @5: Array<u32, 4 : usize>; // anonymous local
 
     storage_live(@3)
     storage_live(@4)
     storage_live(@5)
+    @5 := [const (0 : u32), const (1 : u32), const (2 : u32), const (3 : u32)]
+    @4 := &@5
     storage_live(@1)
     storage_live(@2)
-    @4 := [const (0 : u32), const (1 : u32), const (2 : u32), const (3 : u32)]
-    @5 := &@4
-    @3 := move (@5)
+    @3 := move (@4)
     @2 := &*(@3)
     @1 := &*(@2)
     @0 := @ArrayToSliceShared<'_, u32, 4 : usize>(move (@1))
diff --git a/charon/tests/ui/simple/ptr_to_promoted.out b/charon/tests/ui/simple/ptr_to_promoted.out
index 7936587c2..d7f1ca8ad 100644
--- a/charon/tests/ui/simple/ptr_to_promoted.out
+++ b/charon/tests/ui/simple/ptr_to_promoted.out
@@ -8,17 +8,17 @@ fn test_crate::main()
     let @3: usize; // anonymous local
     let @4: *const u8; // anonymous local
     let @5: &'_ (u8); // anonymous local
-    let @6: u8; // anonymous local
-    let @7: &'_ (u8); // anonymous local
+    let @6: &'_ (u8); // anonymous local
+    let @7: u8; // anonymous local
 
     storage_live(@5)
     storage_live(@6)
     storage_live(@7)
+    @7 := const (0 : u8)
+    @6 := &@7
     storage_live(x@1)
     storage_live(@2)
-    @6 := const (0 : u8)
-    @7 := &@6
-    @5 := move (@7)
+    @5 := move (@6)
     @2 := &*(@5)
     x@1 := &raw const *(@2)
     storage_dead(@2)
diff --git a/charon/tests/ui/simple/slice_index_range.out b/charon/tests/ui/simple/slice_index_range.out
index 0178d54de..e74465cbd 100644
--- a/charon/tests/ui/simple/slice_index_range.out
+++ b/charon/tests/ui/simple/slice_index_range.out
@@ -395,19 +395,19 @@ pub fn core::fmt::{core::fmt::Arguments<'a>}#4::new_const<'a, const N : usize>(@
     let pieces@1: &'_ (Array<&'_ (Str), const N : usize>); // arg #1
     let @2: &'_ (Slice<&'_ (Str)>); // anonymous local
     let @3: &'_ (Slice<core::fmt::rt::Argument<'_>>); // anonymous local
-    let @4: Array<core::fmt::rt::Argument<'_>, 0 : usize>; // anonymous local
-    let @5: &'_ (Array<core::fmt::rt::Argument<'_>, 0 : usize>); // anonymous local
+    let @4: &'_ (Array<core::fmt::rt::Argument<'_>, 0 : usize>); // anonymous local
+    let @5: Array<core::fmt::rt::Argument<'_>, 0 : usize>; // anonymous local
     let @6: core::option::Option<&'_ (Slice<core::fmt::rt::Placeholder>)>[core::marker::Sized<&'_ (Slice<core::fmt::rt::Placeholder>)>]; // anonymous local
 
     storage_live(@4)
     storage_live(@5)
     storage_live(@6)
+    @5 := []
+    @4 := &@5
     storage_live(@2)
     @2 := @ArrayToSliceShared<'_, &'_ (Str), const N : usize>(copy (pieces@1))
     storage_live(@3)
-    @4 := []
-    @5 := &@4
-    @3 := @ArrayToSliceShared<'_, core::fmt::rt::Argument<'_>, 0 : usize>(move (@5))
+    @3 := @ArrayToSliceShared<'_, core::fmt::rt::Argument<'_>, 0 : usize>(move (@4))
     @6 := core::option::Option::None {  }
     @0 := core::fmt::Arguments { pieces: move (@2), fmt: move (@6), args: move (@3) }
     storage_dead(@3)
@@ -809,18 +809,18 @@ fn core::slice::index::slice_end_index_overflow_fail() -> !
     let @2: &'_ (Array<&'_ (Str), 1 : usize>); // anonymous local
     let @3: &'_ (Array<&'_ (Str), 1 : usize>); // anonymous local
     let @4: &'_ (Array<&'_ (Str), 1 : usize>); // anonymous local
-    let @5: Array<&'_ (Str), 1 : usize>; // anonymous local
-    let @6: &'_ (Array<&'_ (Str), 1 : usize>); // anonymous local
+    let @5: &'_ (Array<&'_ (Str), 1 : usize>); // anonymous local
+    let @6: Array<&'_ (Str), 1 : usize>; // anonymous local
 
     storage_live(@4)
     storage_live(@5)
     storage_live(@6)
+    @6 := [const ("attempted to index slice up to maximum usize")]
+    @5 := &@6
     storage_live(@1)
     storage_live(@2)
     storage_live(@3)
-    @5 := [const ("attempted to index slice up to maximum usize")]
-    @6 := &@5
-    @4 := move (@6)
+    @4 := move (@5)
     @3 := &*(@4)
     @2 := &*(@3)
     @1 := core::fmt::{core::fmt::Arguments<'a>}#4::new_const<'_, 1 : usize>(move (@2))