diff --git a/ci/rust-toolchain b/ci/rust-toolchain
index a49a9c7e7b..8ec00e1cb2 100644
--- a/ci/rust-toolchain
+++ b/ci/rust-toolchain
@@ -1,3 +1,3 @@
 [toolchain]
-channel = "nightly-2023-10-20"
+channel = "nightly-2024-01-31"
 components = [ "rustfmt", "rustc-dev", "llvm-tools" ]
diff --git a/creusot-contracts/src/lib.rs b/creusot-contracts/src/lib.rs
index fd324b72dc..ab030ea0a9 100644
--- a/creusot-contracts/src/lib.rs
+++ b/creusot-contracts/src/lib.rs
@@ -203,8 +203,6 @@ mod macros {
     /// This means you cannot `#[open]` a body which refers to a `pub(crate)` symbol.
     pub use creusot_contracts_dummy::open;
 
-    pub use creusot_contracts_proc::DeepModel;
-
     pub use creusot_contracts_proc::Resolve;
 }
 
@@ -251,6 +249,7 @@ pub mod resolve;
 pub mod util;
 pub mod well_founded;
 
+pub use macros::*;
 // We add some common things at the root of the creusot-contracts library
 pub use crate::{
     logic::{IndexLogic as _, Int, OrdLogic, Seq},
@@ -297,3 +296,7 @@ macro_rules! vec {
     );
     ($($x:expr,)*) => (vec![$($x),*])
 }
+
+// #[logic]
+// #[open]
+// pub fn foo() -> bool { true }
diff --git a/creusot-rustc/src/main.rs b/creusot-rustc/src/main.rs
index d8d3c4fb52..bb4d67837b 100644
--- a/creusot-rustc/src/main.rs
+++ b/creusot-rustc/src/main.rs
@@ -14,9 +14,9 @@ extern crate log;
 use creusot::callbacks::*;
 use options::CreusotArgs;
 use rustc_driver::{RunCompiler, DEFAULT_LOCALE_RESOURCES};
-use rustc_errors::emitter::EmitterWriter;
+use rustc_errors::emitter::HumanEmitter;
 use rustc_interface::interface::try_print_query_stack;
-use rustc_session::{config::ErrorOutputType, EarlyErrorHandler};
+use rustc_session::{config::ErrorOutputType, EarlyDiagCtxt};
 use std::{env, panic, panic::PanicInfo, process::Command};
 
 const BUG_REPORT_URL: &'static str = &"https://github.com/xldenis/creusot/issues/new";
@@ -37,10 +37,10 @@ fn report_panic(info: &PanicInfo) {
     let fallback_bundle =
         rustc_errors::fallback_fluent_bundle(DEFAULT_LOCALE_RESOURCES.to_vec(), false);
 
-    let emitter = Box::new(EmitterWriter::stderr(rustc_errors::ColorConfig::Auto, fallback_bundle));
-    let handler = rustc_errors::Handler::with_emitter(emitter);
+    let emitter = Box::new(HumanEmitter::stderr(rustc_errors::ColorConfig::Auto, fallback_bundle));
+    let handler = rustc_errors::DiagCtxt::with_emitter(emitter);
 
-    let mut diagnostic = handler.struct_note_without_error("Creusot has panic-ed!");
+    let mut diagnostic = handler.struct_note("Creusot has panic-ed!");
     diagnostic.note("Oops, that shouldn't have happened, sorry about that.");
     diagnostic.note(format!("Please report this bug over here: {}", BUG_REPORT_URL));
 
@@ -58,7 +58,7 @@ struct DefaultCallbacks;
 impl rustc_driver::Callbacks for DefaultCallbacks {}
 
 fn main() {
-    let handler = EarlyErrorHandler::new(ErrorOutputType::default());
+    let handler = EarlyDiagCtxt::new(ErrorOutputType::default());
     rustc_driver::init_rustc_env_logger(&handler);
     env_logger::init();
     lazy_static::initialize(&ICE_HOOK);
@@ -107,6 +107,7 @@ fn setup_plugin() {
         args.push("-Zcrate-attr=feature(rustc_attrs)".to_owned());
         args.push("-Zcrate-attr=feature(unsized_fn_params)".to_owned());
         args.push("--allow=internal_features".to_owned());
+        args.push("-Zdump-mir=speccleanup".to_owned());
         args.extend(["--cfg", "creusot"].into_iter().map(str::to_owned));
         debug!("creusot args={:?}", args);
 
@@ -137,7 +138,7 @@ fn _emit_warning(text: String) {
     let fallback_bundle =
         rustc_errors::fallback_fluent_bundle(DEFAULT_LOCALE_RESOURCES.to_vec(), false);
 
-    let emitter = Box::new(EmitterWriter::stderr(rustc_errors::ColorConfig::Auto, fallback_bundle));
-    let handler = rustc_errors::Handler::with_emitter(emitter);
+    let emitter = Box::new(HumanEmitter::stderr(rustc_errors::ColorConfig::Auto, fallback_bundle));
+    let handler = rustc_errors::DiagCtxt::with_emitter(emitter);
     handler.warn(text);
 }
diff --git a/creusot/src/analysis.rs b/creusot/src/analysis.rs
index ae5f464433..70f2309d8d 100644
--- a/creusot/src/analysis.rs
+++ b/creusot/src/analysis.rs
@@ -112,7 +112,7 @@ pub(crate) fn categorize(context: PlaceContext) -> Option<DefUse> {
         // cross suspension points so this behavior is unproblematic.
         PlaceContext::MutatingUse(MutatingUseContext::Borrow) |
         PlaceContext::NonMutatingUse(NonMutatingUseContext::SharedBorrow) |
-        PlaceContext::NonMutatingUse(NonMutatingUseContext::ShallowBorrow) |
+        PlaceContext::NonMutatingUse(NonMutatingUseContext::FakeBorrow) |
         PlaceContext::NonMutatingUse(NonMutatingUseContext::PlaceMention) |
         PlaceContext::MutatingUse(MutatingUseContext::AddressOf) |
         PlaceContext::NonMutatingUse(NonMutatingUseContext::AddressOf) |
diff --git a/creusot/src/analysis/frozen_locals.rs b/creusot/src/analysis/frozen_locals.rs
index 3717b458a7..4c3be0ef90 100644
--- a/creusot/src/analysis/frozen_locals.rs
+++ b/creusot/src/analysis/frozen_locals.rs
@@ -185,7 +185,7 @@ impl<'tcx> dataflow::GenKillAnalysis<'tcx> for Borrows<'_, 'tcx> {
 
     fn before_terminator_effect(
         &mut self,
-        _trans: &mut impl GenKill<Self::Idx>,
+        _trans: &mut Self::Domain,
         _terminator: &mir::Terminator<'tcx>,
         _location: Location,
     ) {
@@ -213,7 +213,7 @@ impl<'tcx> dataflow::GenKillAnalysis<'tcx> for Borrows<'_, 'tcx> {
 
     fn call_return_effect(
         &mut self,
-        _trans: &mut impl GenKill<Self::Idx>,
+        _trans: &mut Self::Domain,
         _block: mir::BasicBlock,
         _return_places: CallReturnPlaces<'_, 'tcx>,
     ) {
diff --git a/creusot/src/analysis/init_locals.rs b/creusot/src/analysis/init_locals.rs
index 06c9656a82..1023597205 100644
--- a/creusot/src/analysis/init_locals.rs
+++ b/creusot/src/analysis/init_locals.rs
@@ -54,7 +54,7 @@ impl<'tcx> GenKillAnalysis<'tcx> for MaybeInitializedLocals {
 
     fn call_return_effect(
         &mut self,
-        trans: &mut impl GenKill<Self::Idx>,
+        trans: &mut Self::Domain,
         _block: BasicBlock,
         return_places: CallReturnPlaces<'_, 'tcx>,
     ) {
@@ -108,7 +108,7 @@ where
                 NonMutatingUseContext::Inspect
                 | NonMutatingUseContext::Copy
                 | NonMutatingUseContext::SharedBorrow
-                | NonMutatingUseContext::ShallowBorrow
+                | NonMutatingUseContext::FakeBorrow
                 | NonMutatingUseContext::AddressOf
                 | NonMutatingUseContext::PlaceMention
                 | NonMutatingUseContext::Projection,
diff --git a/creusot/src/analysis/liveness_no_drop.rs b/creusot/src/analysis/liveness_no_drop.rs
index 0d481cafa3..1f1f9283d3 100644
--- a/creusot/src/analysis/liveness_no_drop.rs
+++ b/creusot/src/analysis/liveness_no_drop.rs
@@ -55,7 +55,7 @@ impl<'tcx> GenKillAnalysis<'tcx> for MaybeLiveExceptDrop {
 
     fn call_return_effect(
         &mut self,
-        trans: &mut impl GenKill<Self::Idx>,
+        trans: &mut Self::Domain,
         _block: mir::BasicBlock,
         return_places: CallReturnPlaces<'_, 'tcx>,
     ) {
@@ -186,7 +186,7 @@ impl DefUse {
                 | NonMutatingUseContext::Copy
                 | NonMutatingUseContext::Inspect
                 | NonMutatingUseContext::Move
-                | NonMutatingUseContext::ShallowBorrow
+                | NonMutatingUseContext::FakeBorrow
                 | NonMutatingUseContext::SharedBorrow
                 | NonMutatingUseContext::PlaceMention,
             ) => Some(DefUse::Use),
diff --git a/creusot/src/analysis/not_final_places.rs b/creusot/src/analysis/not_final_places.rs
index 849c7f6a51..28219cb3e8 100644
--- a/creusot/src/analysis/not_final_places.rs
+++ b/creusot/src/analysis/not_final_places.rs
@@ -478,7 +478,7 @@ impl<'tcx> GenKillAnalysis<'tcx> for NotFinalPlaces<'tcx> {
 
     fn call_return_effect(
         &mut self,
-        _trans: &mut impl GenKill<Self::Idx>,
+        _trans: &mut Self::Domain,
         _block: BasicBlock,
         _return_places: CallReturnPlaces<'_, 'tcx>,
     ) {
@@ -496,7 +496,7 @@ impl<'tcx> GenKillAnalysis<'tcx> for NotFinalPlaces<'tcx> {
 
     fn before_terminator_effect(
         &mut self,
-        trans: &mut impl GenKill<Self::Idx>,
+        trans: &mut Self::Domain,
         terminator: &mir::Terminator<'tcx>,
         location: Location,
     ) {
diff --git a/creusot/src/analysis/uninit_locals.rs b/creusot/src/analysis/uninit_locals.rs
index 1ef0f8d47d..9cf8e99a70 100644
--- a/creusot/src/analysis/uninit_locals.rs
+++ b/creusot/src/analysis/uninit_locals.rs
@@ -55,7 +55,7 @@ impl<'tcx> GenKillAnalysis<'tcx> for MaybeUninitializedLocals {
 
     fn call_return_effect(
         &mut self,
-        trans: &mut impl GenKill<Self::Idx>,
+        trans: &mut Self::Domain,
         _block: BasicBlock,
         return_places: CallReturnPlaces<'_, 'tcx>,
     ) {
@@ -106,7 +106,7 @@ where
                 NonMutatingUseContext::Inspect
                 | NonMutatingUseContext::Copy
                 | NonMutatingUseContext::SharedBorrow
-                | NonMutatingUseContext::ShallowBorrow
+                | NonMutatingUseContext::FakeBorrow
                 | NonMutatingUseContext::AddressOf
                 | NonMutatingUseContext::PlaceMention
                 | NonMutatingUseContext::Projection,
diff --git a/creusot/src/backend.rs b/creusot/src/backend.rs
index f04ad83442..94c8783f5e 100644
--- a/creusot/src/backend.rs
+++ b/creusot/src/backend.rs
@@ -258,9 +258,9 @@ impl<'tcx> Why3Generator<'tcx> {
             self.translate(adt_did);
         }
 
-        let (modl, deps) = ty_inv::build_inv_module(self, inv_kind);
+        let deps = ty_inv::build_inv_module(self, inv_kind);
         self.dependencies.insert(tid, deps);
-        self.functions.insert(tid, TranslatedItem::TyInv { modl });
+        self.functions.insert(tid, TranslatedItem::TyInv {});
     }
 
     // pub(crate) fn item(&self, def_id: DefId) -> Option<&TranslatedItem> {
@@ -413,7 +413,7 @@ pub(crate) fn closure_generic_decls(
     mut def_id: DefId,
 ) -> impl Iterator<Item = Decl> + '_ {
     loop {
-        if tcx.is_closure(def_id) {
+        if tcx.is_closure_or_coroutine(def_id) {
             def_id = tcx.parent(def_id);
         } else {
             break;
diff --git a/creusot/src/backend/clone_map.rs b/creusot/src/backend/clone_map.rs
index db49c5e224..9720e26827 100644
--- a/creusot/src/backend/clone_map.rs
+++ b/creusot/src/backend/clone_map.rs
@@ -140,7 +140,7 @@ impl<'tcx> Namer<'tcx> for CloneMap<'tcx> {
     fn ty(&mut self, def_id: DefId, subst: GenericArgsRef<'tcx>) -> QName {
         let mut node = DepNode::new(self.tcx, (def_id, subst));
 
-        if self.tcx.is_closure(def_id) {
+        if self.tcx.is_closure_or_coroutine(def_id) {
             node = DepNode::Type(Ty::new_closure(self.tcx, def_id, subst));
         }
 
@@ -282,8 +282,10 @@ impl<'tcx> CloneNames<'tcx> {
     }
     fn insert(&mut self, key: DepNode<'tcx>) -> Kind {
         *self.names.entry(key).or_insert_with(|| {
-            if let DepNode::Type(ty) = key && !matches!(ty.kind(), TyKind::Alias(_, _)) {
-                let kind =  if let Some((did, _)) = key.did() {
+            if let DepNode::Type(ty) = key
+                && !matches!(ty.kind(), TyKind::Alias(_, _))
+            {
+                let kind = if let Some((did, _)) = key.did() {
                     let name = Symbol::intern(&*module_name(self.tcx, did));
                     Kind::Named(name)
                 } else {
diff --git a/creusot/src/backend/clone_map/elaborator.rs b/creusot/src/backend/clone_map/elaborator.rs
index 5d6ac35cc8..3cb767715d 100644
--- a/creusot/src/backend/clone_map/elaborator.rs
+++ b/creusot/src/backend/clone_map/elaborator.rs
@@ -289,7 +289,7 @@ impl<'tcx> Namer<'tcx> for SymNamer<'tcx> {
     fn ty(&mut self, def_id: DefId, subst: GenericArgsRef<'tcx>) -> QName {
         let mut node = DepNode::new(self.tcx, (def_id, subst));
 
-        if self.tcx.is_closure(def_id) {
+        if self.tcx.is_closure_or_coroutine(def_id) {
             node = DepNode::Type(Ty::new_closure(self.tcx, def_id, subst));
         }
 
diff --git a/creusot/src/backend/clone_map/expander.rs b/creusot/src/backend/clone_map/expander.rs
index e438c952b6..db5c69289f 100644
--- a/creusot/src/backend/clone_map/expander.rs
+++ b/creusot/src/backend/clone_map/expander.rs
@@ -214,7 +214,9 @@ impl<'a, 'tcx> Expander<'a, 'tcx> {
             TyInvKind::from_ty(ctx.tcx, ty).unwrap_or(TyInvKind::Trivial)
         };
 
-        if let TransId::TyInv(self_kind) = self.self_id && self_kind == inv_kind {
+        if let TransId::TyInv(self_kind) = self.self_id
+            && self_kind == inv_kind
+        {
             return;
         }
 
@@ -238,7 +240,8 @@ impl<'a, 'tcx> Expander<'a, 'tcx> {
 
         // Dont clone laws into the trait / impl which defines them.
         if let Some(self_item) = ctx.tcx.opt_associated_item(self_did)
-            && self_item.container_id(ctx.tcx) == item.container_id(ctx.tcx) {
+            && self_item.container_id(ctx.tcx) == item.container_id(ctx.tcx)
+        {
             return;
         }
 
diff --git a/creusot/src/backend/dependency.rs b/creusot/src/backend/dependency.rs
index 7daaac6aa9..53197b1030 100644
--- a/creusot/src/backend/dependency.rs
+++ b/creusot/src/backend/dependency.rs
@@ -212,8 +212,9 @@ fn resolve_item<'tcx>(
     param_env: ParamEnv<'tcx>,
 ) -> Dependency<'tcx> {
     let resolved = if tcx.trait_of_item(item).is_some()
-        && let Some(resolved) = traits::resolve_opt(tcx, param_env, item, substs) {
-            resolved
+        && let Some(resolved) = traits::resolve_opt(tcx, param_env, item, substs)
+    {
+        resolved
     } else {
         (item, substs)
     };
diff --git a/creusot/src/backend/optimization.rs b/creusot/src/backend/optimization.rs
index 20d5b42561..551b1b77c3 100644
--- a/creusot/src/backend/optimization.rs
+++ b/creusot/src/backend/optimization.rs
@@ -274,14 +274,16 @@ impl<'tcx> SimplePropagator<'tcx> {
         match s {
             Statement::Assignment(_, r, _) => self.visit_rvalue(r),
             Statement::Resolve(_, _, p) => {
-              if let Some(l) = p.as_symbol() && self.dead.contains(&l) {
-
-              }
+                if let Some(l) = p.as_symbol()
+                    && self.dead.contains(&l)
+                {}
             }
             Statement::Assertion { cond, msg: _ } => self.visit_term(cond),
-            Statement::Call(_, _, _, args, _) => args.iter_mut().for_each(|a| self.visit_operand(a)),
-            Statement::AssumeBorrowInv(_) => {},
-            Statement::AssertTyInv( _) => {},
+            Statement::Call(_, _, _, args, _) => {
+                args.iter_mut().for_each(|a| self.visit_operand(a))
+            }
+            Statement::AssumeBorrowInv(_) => {}
+            Statement::AssertTyInv(_) => {}
         }
     }
 
@@ -312,10 +314,12 @@ impl<'tcx> SimplePropagator<'tcx> {
     fn visit_operand(&mut self, op: &mut Operand<'tcx>) {
         match op {
             Operand::Move(p) | Operand::Copy(p) => {
-              if let Some(l) = p.as_symbol() && let Some(v) = self.prop.remove(&l) {
-                *op = v;
-              }
-            },
+                if let Some(l) = p.as_symbol()
+                    && let Some(v) = self.prop.remove(&l)
+                {
+                    *op = v;
+                }
+            }
             Operand::Constant(_) => {}
         }
     }
diff --git a/creusot/src/backend/program.rs b/creusot/src/backend/program.rs
index 521b292ab1..ebfa18f730 100644
--- a/creusot/src/backend/program.rs
+++ b/creusot/src/backend/program.rs
@@ -128,7 +128,7 @@ pub(crate) fn translate_closure<'tcx>(
     ctx: &mut Why3Generator<'tcx>,
     def_id: DefId,
 ) -> (CloneSummary<'tcx>, Module, Option<Module>) {
-    assert!(ctx.is_closure(def_id));
+    assert!(ctx.is_closure_or_coroutine(def_id));
     let (summary, func) = translate_function(ctx, def_id);
     (summary, closure_ty(ctx, def_id), func)
 }
@@ -146,7 +146,7 @@ pub(crate) fn translate_function<'tcx, 'sess>(
     };
     let body = to_why(ctx, &mut names, body_ids[0]);
 
-    if ctx.tcx.is_closure(def_id) {
+    if ctx.tcx.is_closure_or_coroutine(def_id) {
         closure_aux_defs(ctx, def_id)
     };
 
@@ -206,7 +206,7 @@ fn lower_promoted<'tcx>(
     body_id: BodyId,
 ) -> Decl {
     let promoted = promoted::translate_promoted(ctx, body_id);
-    let (sig, fmir) = promoted.unwrap_or_else(|e| e.emit(ctx.tcx.sess));
+    let (sig, fmir) = promoted.unwrap_or_else(|e| e.emit(ctx.tcx));
 
     let mut sig = sig_to_why3(ctx, names, &sig, body_id.def_id());
     sig.name = format!("promoted{:?}", body_id.promoted.unwrap().as_usize()).into();
@@ -791,7 +791,7 @@ fn func_call_to_why3<'tcx>(
     let mut args: Vec<_> = args.into_iter().map(|a| a.to_why(ctx, names, locals)).collect();
     let fname = names.value(id, subst);
 
-    let exp = if ctx.is_closure(id) {
+    let exp = if ctx.is_closure_or_coroutine(id) {
         assert!(args.len() == 2, "closures should only have two arguments (env, args)");
 
         let real_sig = ctx.signature_unclosure(subst.as_closure().sig(), Unsafety::Normal);
diff --git a/creusot/src/backend/ty.rs b/creusot/src/backend/ty.rs
index 0e1ad3eabc..c143040ec8 100644
--- a/creusot/src/backend/ty.rs
+++ b/creusot/src/backend/ty.rs
@@ -15,7 +15,7 @@ use rustc_middle::ty::{
     GenericArgsRef, ParamEnv, Ty, TyCtxt, TyKind,
 };
 use rustc_span::{Span, Symbol, DUMMY_SP};
-use rustc_type_ir::sty::TyKind::*;
+use rustc_type_ir::TyKind::*;
 use std::collections::VecDeque;
 use why3::{
     declaration::{
@@ -455,7 +455,7 @@ pub(crate) fn ty_param_names(
     mut def_id: DefId,
 ) -> impl Iterator<Item = Ident> + '_ {
     loop {
-        if tcx.is_closure(def_id) {
+        if tcx.is_closure_or_coroutine(def_id) {
             def_id = tcx.parent(def_id);
         } else {
             break;
diff --git a/creusot/src/backend/ty_inv.rs b/creusot/src/backend/ty_inv.rs
index 29e0faadcb..a1af5f0c58 100644
--- a/creusot/src/backend/ty_inv.rs
+++ b/creusot/src/backend/ty_inv.rs
@@ -18,7 +18,7 @@ use rustc_macros::{TypeFoldable, TypeVisitable};
 use rustc_middle::ty::{GenericArg, GenericArgsRef, ParamEnv, Ty, TyCtxt, TyKind};
 use rustc_span::{Symbol, DUMMY_SP};
 use why3::{
-    declaration::{Axiom, Decl, Module, TyDecl},
+    declaration::{Axiom, Decl, TyDecl},
     exp::{Exp, Trigger},
     Ident,
 };
@@ -403,7 +403,7 @@ impl<'tcx> InvariantElaborator<'tcx> {
 pub(crate) fn build_inv_module<'tcx>(
     ctx: &mut Why3Generator<'tcx>,
     inv_kind: TyInvKind,
-) -> (Module, CloneSummary<'tcx>) {
+) -> CloneSummary<'tcx> {
     let mut names = CloneMap::new(ctx.tcx, TransId::TyInv(inv_kind));
     let generics = inv_kind.generics(ctx.tcx);
     let inv_axiom =
@@ -434,7 +434,7 @@ pub(crate) fn build_inv_module<'tcx>(
 
     decls.push(Decl::Axiom(inv_axiom));
 
-    (Module { name: util::inv_module_name(ctx.tcx, inv_kind), decls }, summary)
+    summary
 }
 
 fn axiom_name(ctx: &Why3Generator<'_>, inv_kind: TyInvKind) -> Ident {
diff --git a/creusot/src/callbacks.rs b/creusot/src/callbacks.rs
index 64c510ad89..9a87179901 100644
--- a/creusot/src/callbacks.rs
+++ b/creusot/src/callbacks.rs
@@ -2,7 +2,7 @@ use rustc_borrowck::consumers::{BodyWithBorrowckFacts, ConsumerOptions};
 use rustc_driver::{Callbacks, Compilation};
 use rustc_hir::def_id::LocalDefId;
 use rustc_interface::{interface::Compiler, Config, Queries};
-use rustc_middle::ty::TyCtxt;
+use rustc_middle::{mir::dump_mir, ty::TyCtxt};
 
 use std::{cell::RefCell, collections::HashMap, thread_local};
 
@@ -35,6 +35,14 @@ impl Callbacks for ToWhy {
                 tcx.alloc_steal_mir(mir)
             };
 
+            providers.mir_drops_elaborated_and_const_checked = |tcx, def_id| {
+                let mir = (rustc_interface::DEFAULT_QUERY_PROVIDERS
+                    .mir_drops_elaborated_and_const_checked)(tcx, def_id);
+                let mut mir = mir.steal();
+                remove_ghost_closures(tcx, &mut mir);
+                tcx.alloc_steal_mir(mir)
+            };
+
             providers.mir_borrowck = |tcx, def_id| {
                 let opts = ConsumerOptions::RegionInferenceContext;
 
@@ -74,7 +82,7 @@ impl Callbacks for ToWhy {
             let _ = crate::translation::after_analysis(ctx);
         });
 
-        c.session().abort_if_errors();
+        c.sess.dcx().abort_if_errors();
 
         if self.opts.in_cargo {
             Compilation::Continue
diff --git a/creusot/src/cleanup_spec_closures.rs b/creusot/src/cleanup_spec_closures.rs
index f009d0cf70..a62ca9b0bf 100644
--- a/creusot/src/cleanup_spec_closures.rs
+++ b/creusot/src/cleanup_spec_closures.rs
@@ -3,8 +3,8 @@ use rustc_hir::def_id::DefId;
 use rustc_index::{Idx, IndexVec};
 use rustc_middle::{
     mir::{
-        visit::MutVisitor, AggregateKind, BasicBlock, BasicBlockData, Body, Local, Location,
-        Rvalue, SourceInfo, Terminator, TerminatorKind,
+        dump_mir, visit::MutVisitor, AggregateKind, BasicBlock, BasicBlockData, Body, Local,
+        Location, Rvalue, SourceInfo, StatementKind, Terminator, TerminatorKind,
     },
     ty::TyCtxt,
 };
@@ -18,11 +18,13 @@ use crate::util;
 /// To prevent the closures from intererring with the borrow checking of the surrounding environment, we replace the MIR body of the closure with an empty loop and remove all of the arguments to the closure in the surrounding MIR.
 pub(crate) fn cleanup_spec_closures<'tcx>(tcx: TyCtxt<'tcx>, def_id: DefId, body: &mut Body<'tcx>) {
     trace!("cleanup_spec_closures: {:?}", def_id);
+
     if util::no_mir(tcx, def_id) {
         trace!("replacing function body");
         *body.basic_blocks_mut() = make_loop(tcx);
         body.var_debug_info = Vec::new();
     } else {
+        // dump_mir(tcx, false, "speccleanup", &"before", &body, |_, _| Ok(()));
         let mut cleanup = NoTranslateNoMoves { tcx, unused: IndexSet::new() };
         cleanup.visit_body(body);
 
@@ -32,12 +34,11 @@ pub(crate) fn cleanup_spec_closures<'tcx>(tcx: TyCtxt<'tcx>, def_id: DefId, body
         updater.visit_body(body);
 
         body.local_decls.shrink_to_fit();
+        dump_mir(tcx, false, "speccleanup", &"after", &body, |_, _| Ok(()));
     }
 }
 
 fn cleanup_statements<'tcx>(body: &mut Body<'tcx>, unused: &IndexSet<Local>) {
-    use rustc_middle::mir::StatementKind;
-
     for data in body.basic_blocks_mut() {
         data.statements.retain(|statement| match &statement.kind {
             StatementKind::StorageLive(local) | StatementKind::StorageDead(local) => {
@@ -89,6 +90,7 @@ impl<'tcx> MutVisitor<'tcx> for NoTranslateNoMoves<'tcx> {
                             if let Some(loc) = place.as_local() {
                                 self.unused.insert(loc);
                             }
+                            // *p = Operand::Copy(place);
                         }
                     });
                     *substs = IndexVec::new();
@@ -137,3 +139,32 @@ impl<'tcx> MutVisitor<'tcx> for LocalUpdater<'tcx> {
         *l = self.map[*l].unwrap();
     }
 }
+
+pub fn remove_ghost_closures<'tcx>(tcx: TyCtxt<'tcx>, body: &mut Body<'tcx>) {
+    struct RemoveGhostItems<'tcx> {
+        tcx: TyCtxt<'tcx>,
+    }
+
+    impl<'tcx> MutVisitor<'tcx> for RemoveGhostItems<'tcx> {
+        fn tcx<'a>(&'a self) -> TyCtxt<'tcx> {
+            self.tcx
+        }
+
+        fn visit_statement(
+            &mut self,
+            statement: &mut rustc_middle::mir::Statement<'tcx>,
+            _: Location,
+        ) {
+            let StatementKind::Assign(box (_, rhs)) = &statement.kind else { return };
+            let Rvalue::Aggregate(box AggregateKind::Closure(def_id, _), _) = rhs else {
+                return;
+            };
+            if util::is_no_translate(self.tcx, *def_id) || util::is_snapshot_closure(self.tcx, *def_id)
+            {
+                statement.kind = StatementKind::Nop
+            }
+        }
+    }
+
+    RemoveGhostItems { tcx }.visit_body(body);
+}
diff --git a/creusot/src/ctx.rs b/creusot/src/ctx.rs
index 69832951a8..14c0b526be 100644
--- a/creusot/src/ctx.rs
+++ b/creusot/src/ctx.rs
@@ -21,7 +21,7 @@ use crate::{
 };
 use indexmap::{IndexMap, IndexSet};
 use rustc_borrowck::consumers::BodyWithBorrowckFacts;
-use rustc_errors::{DiagnosticBuilder, DiagnosticId};
+use rustc_errors::{DiagnosticBuilder, FatalAbort};
 use rustc_hir::{
     def::DefKind,
     def_id::{DefId, LocalDefId},
@@ -168,7 +168,7 @@ impl<'tcx, 'sess> TranslationCtx<'tcx> {
         if util::has_body(self, def_id) {
             if !self.terms.contains_key(&def_id) {
                 let mut term = pearlite::pearlite(self, def_id.expect_local())
-                    .unwrap_or_else(|e| e.emit(self.tcx.sess));
+                    .unwrap_or_else(|e| e.emit(self.tcx));
                 pearlite::normalize(self.tcx, self.param_env(def_id), &mut term);
 
                 self.terms.insert(def_id, term);
@@ -228,19 +228,13 @@ impl<'tcx, 'sess> TranslationCtx<'tcx> {
     }
 
     pub(crate) fn crash_and_error(&self, span: Span, msg: &str) -> ! {
-        self.tcx.sess.span_fatal_with_code(
-            span,
-            msg.to_string(),
-            DiagnosticId::Error(String::from("creusot")),
-        )
+        // TODO: try to add a code back in
+        self.tcx.dcx().span_fatal(span, msg.to_string())
     }
 
-    pub(crate) fn fatal_error(&self, span: Span, msg: &str) -> DiagnosticBuilder<'tcx, !> {
-        self.tcx.sess.struct_span_fatal_with_code(
-            span,
-            msg.to_string(),
-            DiagnosticId::Error(String::from("creusot")),
-        )
+    pub(crate) fn fatal_error(&self, span: Span, msg: &str) -> DiagnosticBuilder<'tcx, FatalAbort> {
+        // TODO: try to add a code back in
+        self.tcx.dcx().struct_span_fatal(span, msg.to_string())
     }
 
     pub(crate) fn error(
@@ -248,23 +242,11 @@ impl<'tcx, 'sess> TranslationCtx<'tcx> {
         span: Span,
         msg: &str,
     ) -> DiagnosticBuilder<'tcx, rustc_errors::ErrorGuaranteed> {
-        self.tcx.sess.struct_span_err_with_code(
-            span,
-            msg.to_string(),
-            DiagnosticId::Error(String::from("creusot")),
-        )
+        self.tcx.dcx().struct_span_err(span, msg.to_string())
     }
 
     pub(crate) fn warn(&self, span: Span, msg: &str) -> DiagnosticBuilder<'tcx, ()> {
-        self.tcx.sess.struct_span_warn_with_code(
-            span,
-            msg.to_string(),
-            DiagnosticId::Lint {
-                name: String::from("creusot"),
-                has_future_breakage: false,
-                is_force_warn: false,
-            },
-        )
+        self.tcx.dcx().struct_span_warn(span, msg.to_string())
     }
 
     fn add_binding_group(&mut self, def_ids: &IndexSet<DefId>) {
@@ -395,10 +377,10 @@ impl<'tcx, 'sess> TranslationCtx<'tcx> {
 
     pub(crate) fn check_purity(&mut self, def_id: LocalDefId) {
         let (thir, expr) =
-            self.tcx.thir_body(def_id).unwrap_or_else(|_| Error::from(CrErr).emit(self.tcx.sess));
+            self.tcx.thir_body(def_id).unwrap_or_else(|_| Error::from(CrErr).emit(self.tcx));
         let thir = thir.borrow();
         if thir.exprs.is_empty() {
-            Error::new(self.tcx.def_span(def_id), "type checking failed").emit(self.tcx.sess);
+            Error::new(self.tcx.def_span(def_id), "type checking failed").emit(self.tcx);
         }
 
         let def_id = def_id.to_def_id();
diff --git a/creusot/src/error.rs b/creusot/src/error.rs
index 120546c709..4aea329ad8 100644
--- a/creusot/src/error.rs
+++ b/creusot/src/error.rs
@@ -1,5 +1,4 @@
-use rustc_errors::DiagnosticId;
-use rustc_session::Session;
+use rustc_middle::ty::TyCtxt;
 use rustc_span::{Span, DUMMY_SP};
 
 pub type CreusotResult<T> = Result<T, Error>;
@@ -16,8 +15,9 @@ impl Error {
         Error { span, msg: msg.into() }
     }
 
-    pub(crate) fn emit(self, sess: &Session) -> ! {
-        sess.span_fatal_with_code(self.span, self.msg, DiagnosticId::Error(String::from("creusot")))
+    pub(crate) fn emit(self, tcx: TyCtxt) -> ! {
+        // TODO: try to add a code back in
+        tcx.dcx().span_fatal(self.span, self.msg)
     }
 }
 
diff --git a/creusot/src/extended_location.rs b/creusot/src/extended_location.rs
index cfff054da4..b0eb85562b 100644
--- a/creusot/src/extended_location.rs
+++ b/creusot/src/extended_location.rs
@@ -1,6 +1,5 @@
 use rustc_middle::mir::Location;
-use rustc_mir_dataflow::{self as dataflow, Analysis, AnalysisResults, Results, ResultsCursor};
-use std::borrow::Borrow;
+use rustc_mir_dataflow::{self as dataflow, Analysis, ResultsCursor};
 
 // Dataflow locations
 #[derive(Debug, Copy, Clone)]
@@ -35,12 +34,10 @@ impl ExtendedLocation {
         }
     }
 
-    pub(crate) fn seek_to<'tcx, A, R, D>(self, cursor: &mut ResultsCursor<'_, 'tcx, A, R>)
+    pub(crate) fn seek_to<'tcx, A, D>(self, cursor: &mut ResultsCursor<'_, 'tcx, A>)
     where
         A: Analysis<'tcx, Direction = D>,
         D: Dir,
-        R: AnalysisResults<'tcx, A>,
-        R: Borrow<Results<'tcx, A>>,
     {
         use ExtendedLocation::*;
         if D::is_forward() {
diff --git a/creusot/src/lints/experimental_types.rs b/creusot/src/lints/experimental_types.rs
index c2bc6c3516..54f29c0f74 100644
--- a/creusot/src/lints/experimental_types.rs
+++ b/creusot/src/lints/experimental_types.rs
@@ -40,20 +40,20 @@ impl<'tcx> LateLintPass<'tcx> for Experimental {
         }
 
         if is_str_ty(cx, e) {
-            cx.struct_span_lint(
+            cx.opt_span_lint(
                 EXPERIMENTAL,
-                e.span,
+                Some(e.span),
                 "support for string types is limited and experimental",
-                |lint| lint,
+                |_lint| (),
             );
         }
 
         if is_dyn_ty(cx, e) {
-            cx.struct_span_lint(
+            cx.opt_span_lint(
                 EXPERIMENTAL,
-                e.span,
+                Some(e.span),
                 "support for trait objects (dyn) is limited and experimental",
-                |lint| lint,
+                |_lint| (),
             );
         }
     }
diff --git a/creusot/src/lints/resolve_trait.rs b/creusot/src/lints/resolve_trait.rs
index c90aa1199f..b4585fceb5 100644
--- a/creusot/src/lints/resolve_trait.rs
+++ b/creusot/src/lints/resolve_trait.rs
@@ -21,11 +21,11 @@ fn resolve_trait_loaded(tcx: TyCtxt) -> bool {
 impl<'tcx> LateLintPass<'tcx> for ResolveTrait {
     fn check_crate(&mut self, cx: &LateContext<'tcx>) {
         if !resolve_trait_loaded(cx.tcx) {
-            cx.struct_span_lint(
+            cx.opt_span_lint(
                 RESOLVE_TRAIT,
-                DUMMY_SP,
+                Some(DUMMY_SP),
                 "the `creusot_contracts` crate is not loaded. You will not be able to verify any code using Creusot until you do so.",
-                |lint| lint,
+                |_lint| (),
             );
         }
     }
diff --git a/creusot/src/metadata.rs b/creusot/src/metadata.rs
index 8fc502ae6e..d3a96ae1a7 100644
--- a/creusot/src/metadata.rs
+++ b/creusot/src/metadata.rs
@@ -154,7 +154,7 @@ pub(crate) fn dump_exports(ctx: &TranslationCtx, out: &Option<String>) {
     debug!("dump_exports={:?}", out_filename);
 
     dump_binary_metadata(ctx.tcx, &out_filename, ctx.metadata()).unwrap_or_else(|err| {
-        panic!("could not save metadata path=`{:?}` error={}", out_filename, err)
+        panic!("could not save metadata path=`{:?}` error={}", out_filename, err.1)
     });
 }
 
@@ -162,7 +162,7 @@ fn dump_binary_metadata<'tcx>(
     tcx: TyCtxt<'tcx>,
     path: &Path,
     dep_info: BinaryMetadata<'tcx>,
-) -> Result<(), std::io::Error> {
+) -> Result<(), (PathBuf, std::io::Error)> {
     encode_metadata(tcx, path, dep_info)
 }
 
diff --git a/creusot/src/run_why3.rs b/creusot/src/run_why3.rs
index 705c100d6a..123f7c54ee 100644
--- a/creusot/src/run_why3.rs
+++ b/creusot/src/run_why3.rs
@@ -91,7 +91,7 @@ pub(super) fn run_why3<'tcx>(ctx: &Why3Generator<'tcx>, file: Option<PathBuf>) {
                             writeln!(msg, "Term: {}", expr_to_string(&term)).unwrap();
                             let cterm = cterm_to_ast(&model.value.value_concrete_term);
                             writeln!(msg, "Concrete Term: {}", expr_to_string(&cterm)).unwrap();
-                            ctx.sess.span_note_without_error(span.unwrap_or_default(), msg)
+                            ctx.dcx().span_note(span.unwrap_or_default(), msg)
                         }
                     }
                 }
@@ -141,14 +141,16 @@ impl SpanMap {
         opts: &Options,
         span: Span,
     ) -> Option<why3::declaration::Attribute> {
-        if let Some(cmd) = &opts.why3_cmd && matches!(cmd.sub, Why3Sub::Prove) {
+        if let Some(cmd) = &opts.why3_cmd
+            && matches!(cmd.sub, Why3Sub::Prove)
+        {
             let data = span.data();
             Some(why3::declaration::Attribute::Span(
                 "rustc_span".into(),
                 data.lo.0 as usize,
                 data.hi.0 as usize,
                 self.encode_span_data((data.ctxt, data.parent)),
-                0
+                0,
             ))
         } else {
             None
@@ -202,7 +204,6 @@ fn fun<'a>(args: impl IntoIterator<Item = &'a str>, body: Expr) -> Expr {
         binder: rustc_ast::ClosureBinder::NotPresent,
         capture_clause: rustc_ast::CaptureBy::Ref,
         constness: rustc_ast::Const::No,
-        asyncness: rustc_ast::Async::No,
         movability: rustc_ast::Movability::Movable,
         fn_decl: P(rustc_ast::FnDecl {
             inputs: args
@@ -221,6 +222,7 @@ fn fun<'a>(args: impl IntoIterator<Item = &'a str>, body: Expr) -> Expr {
         body: P(body),
         fn_decl_span: DUMMY_SP,
         fn_arg_span: DUMMY_SP,
+        coroutine_kind: None,
     })))
 }
 
diff --git a/creusot/src/translated_item.rs b/creusot/src/translated_item.rs
index 7b586cfbb8..7a167de7f7 100644
--- a/creusot/src/translated_item.rs
+++ b/creusot/src/translated_item.rs
@@ -26,9 +26,7 @@ pub enum TranslatedItem {
         modl: Vec<Module>,
         accessors: IndexMap<DefId, IndexMap<DefId, Decl>>,
     },
-    TyInv {
-        modl: Module,
-    },
+    TyInv {},
 }
 
 impl<'a> TranslatedItem {
diff --git a/creusot/src/translation.rs b/creusot/src/translation.rs
index eb7886735a..27da2433ee 100644
--- a/creusot/src/translation.rs
+++ b/creusot/src/translation.rs
@@ -81,7 +81,7 @@ pub(crate) fn after_analysis(ctx: TranslationCtx) -> Result<(), Box<dyn Error>>
     debug!("after_analysis_translate: {:?}", start.elapsed());
     let start = Instant::now();
 
-    if why3.sess.has_errors().is_some() {
+    if why3.dcx().has_errors().is_some() {
         return Err(Box::new(CrErr));
     }
 
@@ -121,7 +121,9 @@ pub(crate) fn after_analysis(ctx: TranslationCtx) -> Result<(), Box<dyn Error>>
         let tcx = why3.tcx;
         let modules = why3.modules();
         let modules = modules.flat_map(|(id, item)| {
-            if let TransId::Item(did) = id && tcx.def_path_str(did).contains(matcher) {
+            if let TransId::Item(did) = id
+                && tcx.def_path_str(did).contains(matcher)
+            {
                 item.modules()
             } else {
                 Box::new(std::iter::empty())
diff --git a/creusot/src/translation/constant.rs b/creusot/src/translation/constant.rs
index 9f0c9860c3..4523478c04 100644
--- a/creusot/src/translation/constant.rs
+++ b/creusot/src/translation/constant.rs
@@ -72,9 +72,10 @@ pub(crate) fn from_ty_const<'tcx>(
 ) -> Term<'tcx> {
     // Check if a constant is builtin and thus should not be evaluated further
     // Builtin constants are given a body which panics
-    if let ConstKind::Unevaluated(u) = c.kind() &&
-       let Some(_) = get_builtin(ctx.tcx, u.def) {
-            return Term { kind: TermKind::Lit(Literal::Function(u.def, u.args)), ty: c.ty(), span}
+    if let ConstKind::Unevaluated(u) = c.kind()
+        && let Some(_) = get_builtin(ctx.tcx, u.def)
+    {
+        return Term { kind: TermKind::Lit(Literal::Function(u.def, u.args)), ty: c.ty(), span };
     };
 
     if let ConstKind::Param(_) = c.kind() {
@@ -93,7 +94,7 @@ fn try_to_bits<'tcx, C: ToBits<'tcx>>(
     c: C,
 ) -> Literal<'tcx> {
     use rustc_middle::ty::{FloatTy, IntTy, UintTy};
-    use rustc_type_ir::sty::TyKind::{Bool, Float, FnDef, Int, Uint};
+    use rustc_type_ir::TyKind::{Bool, Float, FnDef, Int, Uint};
     match ty.kind() {
         Int(ity) => {
             let bits = c.get_bits(ctx.tcx, env, ty).unwrap();
diff --git a/creusot/src/translation/external.rs b/creusot/src/translation/external.rs
index c5cb9bf3f5..1ff9132d1d 100644
--- a/creusot/src/translation/external.rs
+++ b/creusot/src/translation/external.rs
@@ -69,16 +69,26 @@ pub(crate) fn extract_extern_specs_from_item<'tcx>(
     let mut inner_subst = GenericArgs::identity_for_item(ctx.tcx, id).to_vec();
     let outer_subst = GenericArgs::identity_for_item(ctx.tcx, def_id.to_def_id());
 
+    // FIXME(xavier): Handle this better.
+    // "Host effects" are related to the wip effects feature of Rust. For the moment let's just ignore them.
+    let has_host_effect = ctx.generics_of(id).host_effect_index.is_some();
+    if has_host_effect {
+        inner_subst.pop();
+    }
     // FIXME(xavier): I don't remember the original reason for introducing this...
     let extra_parameters = inner_subst.len() - outer_subst.len();
 
     // Move Self_ to the front of the list like rustc does for real trait impls (not expressible in surface rust).
     // This only matters when we also have lifetime parameters.
     let self_pos = outer_subst.iter().position(|e| {
-        if
-        let GenericArgKind::Type(t) = e.unpack() &&
-        let TyKind::Param(t) = t.kind() &&
-        t.name.as_str().starts_with("Self") { true } else { false }
+        if let GenericArgKind::Type(t) = e.unpack()
+            && let TyKind::Param(t) = t.kind()
+            && t.name.as_str().starts_with("Self")
+        {
+            true
+        } else {
+            false
+        }
     });
 
     if let Some(ix) = self_pos {
@@ -125,7 +135,7 @@ pub(crate) fn extract_extern_specs_from_item<'tcx>(
         }
     }
 
-    errors.into_iter().for_each(|mut e| e.emit());
+    errors.into_iter().for_each(|e| e.emit());
 
     let subst = ctx.mk_args(&subst);
 
@@ -165,7 +175,7 @@ impl<'a, 'tcx> thir::visit::Visitor<'a, 'tcx> for ExtractExternItems<'a, 'tcx> {
         self.thir
     }
 
-    fn visit_expr(&mut self, expr: &Expr<'tcx>) {
+    fn visit_expr(&mut self, expr: &'a Expr<'tcx>) {
         if let ExprKind::Call { ty, .. } = expr.kind {
             if let TyKind::FnDef(id, subst) = ty.kind() {
                 self.items.insert((*id, subst));
diff --git a/creusot/src/translation/function.rs b/creusot/src/translation/function.rs
index 127f643d80..32b9ea8ec4 100644
--- a/creusot/src/translation/function.rs
+++ b/creusot/src/translation/function.rs
@@ -205,7 +205,9 @@ impl<'body, 'tcx> BodyTranslator<'body, 'tcx> {
 
             self.translate_terminator(bbd.terminator(), loc);
 
-            if let Some(resolver) = &mut self.resolver && bbd.terminator().successors().next().is_none() {
+            if let Some(resolver) = &mut self.resolver
+                && bbd.terminator().successors().next().is_none()
+            {
                 let mut resolved = resolver.need_resolve_locals_before(loc);
                 resolved.remove(Local::from_usize(0)); // do not resolve return local
                 self.resolve_locals(resolved);
@@ -336,7 +338,7 @@ impl<'body, 'tcx> BodyTranslator<'body, 'tcx> {
     }
 
     fn resolve_locals(&mut self, mut locals: BitSet<Local>) {
-        locals.subtract(&self.erased_locals.to_hybrid());
+        locals.subtract(&self.erased_locals);
 
         // TODO determine resolution order based on outlives relation
         let locals = locals.iter().collect::<Vec<_>>();
@@ -468,7 +470,7 @@ pub(crate) fn closure_contract<'tcx>(
     ctx: &mut TranslationCtx<'tcx>,
     def_id: DefId,
 ) -> ClosureContract<'tcx> {
-    let TyKind::Closure(_, subst) = ctx.tcx.type_of(def_id).instantiate_identity().kind() else {
+    let TyKind::Closure(_, subst) = ctx.type_of(def_id).instantiate_identity().kind() else {
         unreachable!()
     };
 
@@ -535,7 +537,9 @@ pub(crate) fn closure_contract<'tcx>(
 
     post_sig.inputs.push((Symbol::intern("result"), DUMMY_SP, result_ty));
 
-    let env_ty = ctx.closure_env_ty(def_id, subst, ctx.lifetimes.re_erased).unwrap().peel_refs();
+    let env_ty = ctx
+        .closure_env_ty(ctx.type_of(def_id).instantiate_identity(), kind, ctx.lifetimes.re_erased)
+        .peel_refs();
     let self_ty = env_ty;
 
     let precond = {
@@ -702,7 +706,9 @@ pub(crate) fn closure_unnest<'tcx>(
     def_id: DefId,
     subst: GenericArgsRef<'tcx>,
 ) -> Term<'tcx> {
-    let env_ty = tcx.closure_env_ty(def_id, subst, tcx.lifetimes.re_erased).unwrap().peel_refs();
+    let ty = Ty::new_closure(tcx, def_id, subst);
+    let kind = subst.as_closure().kind();
+    let env_ty = tcx.closure_env_ty(ty, kind, tcx.lifetimes.re_erased).peel_refs();
 
     let self_ = Term::var(Symbol::intern("self"), env_ty);
 
diff --git a/creusot/src/translation/function/statement.rs b/creusot/src/translation/function/statement.rs
index ac596ec0a2..2e63fd0e54 100644
--- a/creusot/src/translation/function/statement.rs
+++ b/creusot/src/translation/function/statement.rs
@@ -34,7 +34,9 @@ impl<'tcx> BodyTranslator<'_, 'tcx> {
 
                 // if the lhs local becomes resolved during the assignment,
                 // we cannot resolve it afterwards.
-                if let Some(resolved_during) = &mut resolved_during && !pl.is_indirect() {
+                if let Some(resolved_during) = &mut resolved_during
+                    && !pl.is_indirect()
+                {
                     resolved_during.remove(pl.local);
                 }
             }
@@ -52,11 +54,10 @@ impl<'tcx> BodyTranslator<'_, 'tcx> {
             }
             Deinit(_) => unreachable!("Deinit unsupported"),
             PlaceMention(_) => {}
-            ConstEvalCounter => {}
-            // No assembly!
-            // LlvmInlineAsm(_) => self
-            //     .ctx
-            //     .crash_and_error(statement.source_info.span, "inline assembly is not supported"),
+            ConstEvalCounter => {} // No assembly!
+                                   // LlvmInlineAsm(_) => self
+                                   //     .ctx
+                                   //     .crash_and_error(statement.source_info.span, "inline assembly is not supported"),
         }
 
         if let Some(resolved_during) = resolved_during {
@@ -85,7 +86,7 @@ impl<'tcx> BodyTranslator<'_, 'tcx> {
                 }
             },
             Rvalue::Ref(_, ss, pl) => match ss {
-                Shared | Shallow => {
+                Shared | Fake => {
                     if self.erased_locals.contains(pl.local) {
                         return;
                     }
@@ -172,7 +173,9 @@ impl<'tcx> BodyTranslator<'_, 'tcx> {
             ),
 
             Rvalue::Cast(CastKind::PointerCoercion(PointerCoercion::Unsize), op, ty) => {
-                if let Some(t) = ty.builtin_deref(true) && t.ty.is_slice() {
+                if let Some(t) = ty.builtin_deref(true)
+                    && t.ty.is_slice()
+                {
                     // treat &[T; N] to &[T] casts as normal assignments
                     RValue::Operand(self.translate_operand(op))
                 } else {
diff --git a/creusot/src/translation/function/terminator.rs b/creusot/src/translation/function/terminator.rs
index d73786d91b..0cdb141f22 100644
--- a/creusot/src/translation/function/terminator.rs
+++ b/creusot/src/translation/function/terminator.rs
@@ -95,7 +95,7 @@ impl<'tcx> BodyTranslator<'_, 'tcx> {
                 }
 
                 let mut func_args: Vec<_> =
-                    args.iter().map(|arg| self.translate_operand(arg)).collect();
+                    args.iter().map(|arg| self.translate_operand(&arg.node)).collect();
 
                 if func_args.is_empty() {
                     // TODO: Remove this, push the 0-ary handling down to why3 backend
@@ -167,7 +167,7 @@ impl<'tcx> BodyTranslator<'_, 'tcx> {
             FalseUnwind { real_target, .. } => {
                 self.emit_terminator(mk_goto(*real_target));
             }
-            UnwindResume | Yield { .. } | GeneratorDrop | InlineAsm { .. } => {
+            CoroutineDrop | UnwindResume | Yield { .. } | InlineAsm { .. } => {
                 unreachable!("{:?}", terminator.kind)
             }
         }
diff --git a/creusot/src/translation/pearlite.rs b/creusot/src/translation/pearlite.rs
index 5b8dedb97d..be6d4558ff 100644
--- a/creusot/src/translation/pearlite.rs
+++ b/creusot/src/translation/pearlite.rs
@@ -368,21 +368,25 @@ impl<'a, 'tcx> ThirTerm<'a, 'tcx> {
             ExprKind::Literal { lit, neg } => {
                 let lit = match lit.node {
                     LitKind::Bool(b) => Literal::Bool(b),
-                    LitKind::Int(u, lty) => match lty {
-                        LitIntType::Signed(ity) => {
-                            let val = if neg { (u as i128).wrapping_neg() } else { u as i128 };
-                            Literal::MachSigned(val, int_ty(ity))
-                        }
-                        LitIntType::Unsigned(uty) => Literal::MachUnsigned(u, uint_ty(uty)),
-                        LitIntType::Unsuffixed => match ty.kind() {
-                            TyKind::Int(ity) => {
+                    LitKind::Int(u, lty) => {
+                        let u = u.get();
+                        match lty {
+                            LitIntType::Signed(ity) => {
                                 let val = if neg { (u as i128).wrapping_neg() } else { u as i128 };
-                                Literal::MachSigned(val, *ity)
+                                Literal::MachSigned(val, int_ty(ity))
                             }
-                            TyKind::Uint(uty) => Literal::MachUnsigned(u, *uty),
-                            _ => unreachable!(),
-                        },
-                    },
+                            LitIntType::Unsigned(uty) => Literal::MachUnsigned(u, uint_ty(uty)),
+                            LitIntType::Unsuffixed => match ty.kind() {
+                                TyKind::Int(ity) => {
+                                    let val =
+                                        if neg { (u as i128).wrapping_neg() } else { u as i128 };
+                                    Literal::MachSigned(val, *ity)
+                                }
+                                TyKind::Uint(uty) => Literal::MachUnsigned(u, *uty),
+                                _ => unreachable!(),
+                            },
+                        }
+                    }
                     _ => unimplemented!("Unsupported literal"),
                 };
                 Ok(Term { ty, span, kind: TermKind::Lit(lit) })
@@ -1607,7 +1611,7 @@ fn print_thir_expr<'tcx>(
         ExprKind::Borrow { borrow_kind, arg } => {
             match borrow_kind {
                 BorrowKind::Shared => write!(fmt, "& ")?,
-                BorrowKind::Shallow => write!(fmt, "&shallow ")?,
+                BorrowKind::Fake => write!(fmt, "&fake ")?,
                 BorrowKind::Mut { .. } => write!(fmt, "&mut ")?,
             };
 
diff --git a/creusot/src/translation/pearlite/normalize.rs b/creusot/src/translation/pearlite/normalize.rs
index d448bf1ba0..dcd2b0bcae 100644
--- a/creusot/src/translation/pearlite/normalize.rs
+++ b/creusot/src/translation/pearlite/normalize.rs
@@ -70,51 +70,115 @@ fn optimize_builtin<'tcx>(
     let builtin_attr = get_builtin(tcx, def_id);
 
     if builtin_attr == Some(Symbol::intern("add_int")) {
-        Some(TermKind::Binary { op: BinOp::Add, lhs: Box::new(args.remove(0)), rhs: Box::new(args.remove(0)) })
+        Some(TermKind::Binary {
+            op: BinOp::Add,
+            lhs: Box::new(args.remove(0)),
+            rhs: Box::new(args.remove(0)),
+        })
     } else if builtin_attr == Some(Symbol::intern("sub_int")) {
-        Some(TermKind::Binary { op: BinOp::Sub, lhs: Box::new(args.remove(0)), rhs: Box::new(args.remove(0)) })
+        Some(TermKind::Binary {
+            op: BinOp::Sub,
+            lhs: Box::new(args.remove(0)),
+            rhs: Box::new(args.remove(0)),
+        })
     } else if builtin_attr == Some(Symbol::intern("mul_int")) {
-        Some(TermKind::Binary { op: BinOp::Mul, lhs: Box::new(args.remove(0)), rhs: Box::new(args.remove(0)) })
+        Some(TermKind::Binary {
+            op: BinOp::Mul,
+            lhs: Box::new(args.remove(0)),
+            rhs: Box::new(args.remove(0)),
+        })
     } else if builtin_attr == Some(Symbol::intern("div_int")) {
-        Some(TermKind::Binary { op: BinOp::Div, lhs: Box::new(args.remove(0)), rhs: Box::new(args.remove(0)) })
+        Some(TermKind::Binary {
+            op: BinOp::Div,
+            lhs: Box::new(args.remove(0)),
+            rhs: Box::new(args.remove(0)),
+        })
     } else if builtin_attr == Some(Symbol::intern("rem_int")) {
-        Some(TermKind::Binary { op: BinOp::Rem, lhs: Box::new(args.remove(0)), rhs: Box::new(args.remove(0)) })
+        Some(TermKind::Binary {
+            op: BinOp::Rem,
+            lhs: Box::new(args.remove(0)),
+            rhs: Box::new(args.remove(0)),
+        })
     } else if builtin_attr == Some(Symbol::intern("neg_int")) {
         Some(TermKind::Unary { op: pearlite::UnOp::Neg, arg: Box::new(args.remove(0)) })
     } else if builtin_attr == Some(Symbol::intern("int.Int.(<=)")) {
-        Some(TermKind::Binary { op: BinOp::Le, lhs: Box::new(args.remove(0)), rhs: Box::new(args.remove(0)) })
+        Some(TermKind::Binary {
+            op: BinOp::Le,
+            lhs: Box::new(args.remove(0)),
+            rhs: Box::new(args.remove(0)),
+        })
     } else if builtin_attr == Some(Symbol::intern("int.Int.(<)")) {
-        Some(TermKind::Binary { op: BinOp::Lt, lhs: Box::new(args.remove(0)), rhs: Box::new(args.remove(0)) })
+        Some(TermKind::Binary {
+            op: BinOp::Lt,
+            lhs: Box::new(args.remove(0)),
+            rhs: Box::new(args.remove(0)),
+        })
     } else if builtin_attr == Some(Symbol::intern("int.Int.(>=)")) {
-        Some(TermKind::Binary { op: BinOp::Ge, lhs: Box::new(args.remove(0)), rhs: Box::new(args.remove(0)) })
+        Some(TermKind::Binary {
+            op: BinOp::Ge,
+            lhs: Box::new(args.remove(0)),
+            rhs: Box::new(args.remove(0)),
+        })
     } else if builtin_attr == Some(Symbol::intern("int.Int.(>)")) {
-        Some(TermKind::Binary { op: BinOp::Gt, lhs: Box::new(args.remove(0)), rhs: Box::new(args.remove(0)) })
+        Some(TermKind::Binary {
+            op: BinOp::Gt,
+            lhs: Box::new(args.remove(0)),
+            rhs: Box::new(args.remove(0)),
+        })
     } else if builtin_attr == Some(Symbol::intern("==")) {
-        Some(TermKind::Binary { op: BinOp::Eq, lhs: Box::new(args.remove(0)), rhs: Box::new(args.remove(0)) })
+        Some(TermKind::Binary {
+            op: BinOp::Eq,
+            lhs: Box::new(args.remove(0)),
+            rhs: Box::new(args.remove(0)),
+        })
     } else if builtin_attr == Some(Symbol::intern("!=")) {
-        Some(TermKind::Binary { op: BinOp::Ne, lhs: Box::new(args.remove(0)), rhs: Box::new(args.remove(0)) })
-    } else if builtin_attr == Some(Symbol::intern("prelude.UInt8.to_int")) && let TermKind::Lit(Literal::MachUnsigned(c, _)) = args[0].kind {
+        Some(TermKind::Binary {
+            op: BinOp::Ne,
+            lhs: Box::new(args.remove(0)),
+            rhs: Box::new(args.remove(0)),
+        })
+    } else if builtin_attr == Some(Symbol::intern("prelude.UInt8.to_int"))
+        && let TermKind::Lit(Literal::MachUnsigned(c, _)) = args[0].kind
+    {
         Some(TermKind::Lit(Literal::Integer(c as i128)))
-    } else if builtin_attr == Some(Symbol::intern("prelude.UInt16.to_int")) && let TermKind::Lit(Literal::MachUnsigned(c, _)) = args[0].kind {
+    } else if builtin_attr == Some(Symbol::intern("prelude.UInt16.to_int"))
+        && let TermKind::Lit(Literal::MachUnsigned(c, _)) = args[0].kind
+    {
         Some(TermKind::Lit(Literal::Integer(c as i128)))
-    } else if builtin_attr == Some(Symbol::intern("prelude.UInt32.to_int")) && let TermKind::Lit(Literal::MachUnsigned(c, _)) = args[0].kind {
+    } else if builtin_attr == Some(Symbol::intern("prelude.UInt32.to_int"))
+        && let TermKind::Lit(Literal::MachUnsigned(c, _)) = args[0].kind
+    {
         Some(TermKind::Lit(Literal::Integer(c as i128)))
-    } else if builtin_attr == Some(Symbol::intern("prelude.UInt64.to_int")) && let TermKind::Lit(Literal::MachUnsigned(c, _)) = args[0].kind {
+    } else if builtin_attr == Some(Symbol::intern("prelude.UInt64.to_int"))
+        && let TermKind::Lit(Literal::MachUnsigned(c, _)) = args[0].kind
+    {
         Some(TermKind::Lit(Literal::Integer(c as i128)))
-    } else if builtin_attr == Some(Symbol::intern("prelude.UInt128.to_int")) && let TermKind::Lit(Literal::MachUnsigned(c, _)) = args[0].kind {
+    } else if builtin_attr == Some(Symbol::intern("prelude.UInt128.to_int"))
+        && let TermKind::Lit(Literal::MachUnsigned(c, _)) = args[0].kind
+    {
         if c > isize::MAX as u128 {
             panic!("integer constant too large")
         }
         Some(TermKind::Lit(Literal::Integer(c as i128)))
-    } else if builtin_attr == Some(Symbol::intern("prelude.Int8.to_int")) && let TermKind::Lit(Literal::MachSigned(c, _)) = args[0].kind {
+    } else if builtin_attr == Some(Symbol::intern("prelude.Int8.to_int"))
+        && let TermKind::Lit(Literal::MachSigned(c, _)) = args[0].kind
+    {
         Some(TermKind::Lit(Literal::Integer(c as i128)))
-    } else if builtin_attr == Some(Symbol::intern("prelude.Int16.to_int")) && let TermKind::Lit(Literal::MachSigned(c, _)) = args[0].kind {
+    } else if builtin_attr == Some(Symbol::intern("prelude.Int16.to_int"))
+        && let TermKind::Lit(Literal::MachSigned(c, _)) = args[0].kind
+    {
         Some(TermKind::Lit(Literal::Integer(c as i128)))
-    } else if builtin_attr == Some(Symbol::intern("prelude.Int32.to_int")) && let TermKind::Lit(Literal::MachSigned(c, _)) = args[0].kind {
+    } else if builtin_attr == Some(Symbol::intern("prelude.Int32.to_int"))
+        && let TermKind::Lit(Literal::MachSigned(c, _)) = args[0].kind
+    {
         Some(TermKind::Lit(Literal::Integer(c as i128)))
-    } else if builtin_attr == Some(Symbol::intern("prelude.Int64.to_int")) && let TermKind::Lit(Literal::MachSigned(c, _)) = args[0].kind {
+    } else if builtin_attr == Some(Symbol::intern("prelude.Int64.to_int"))
+        && let TermKind::Lit(Literal::MachSigned(c, _)) = args[0].kind
+    {
         Some(TermKind::Lit(Literal::Integer(c as i128)))
-    } else if builtin_attr == Some(Symbol::intern("prelude.Int128.to_int")) && let TermKind::Lit(Literal::MachSigned(c, _)) = args[0].kind {
+    } else if builtin_attr == Some(Symbol::intern("prelude.Int128.to_int"))
+        && let TermKind::Lit(Literal::MachSigned(c, _)) = args[0].kind
+    {
         Some(TermKind::Lit(Literal::Integer(c as i128)))
     } else if builtin_attr == Some(Symbol::intern("identity")) {
         Some(args.remove(0).kind)
diff --git a/creusot/src/translation/specification.rs b/creusot/src/translation/specification.rs
index b6c3427c8c..77324c8802 100644
--- a/creusot/src/translation/specification.rs
+++ b/creusot/src/translation/specification.rs
@@ -376,29 +376,24 @@ impl<'a, 'tcx> thir::visit::Visitor<'a, 'tcx> for PurityVisitor<'a, 'tcx> {
         self.thir
     }
 
-    fn visit_expr(&mut self, expr: &thir::Expr<'tcx>) {
+    fn visit_expr(&mut self, expr: &'a thir::Expr<'tcx>) {
         match expr.kind {
             ExprKind::Call { fun, .. } => {
                 if let &ty::FnDef(func_did, _) = self.thir[fun].ty.kind() {
                     let fn_purity = self.purity(fun, func_did);
                     if !self.context.can_call(fn_purity) && !is_overloaded_item(self.tcx, func_did)
                     {
-                        self.tcx.sess.span_err_with_code(
+                        let msg =
+                            format!("called {fn_purity:?} function in {:?} context", self.context);
+
+                        self.tcx.dcx().span_err(
                             self.thir[fun].span,
-                            format!(
-                                "called {fn_purity} function {:?} in {} context",
-                                self.tcx.def_path_str(func_did),
-                                self.context,
-                            ),
-                            rustc_errors::DiagnosticId::Error(String::from("creusot")),
+                            format!("{} {:?}", msg, self.tcx.def_path_str(func_did)),
                         );
                     }
                 } else if self.context != Purity::Program {
-                    self.tcx.sess.span_fatal_with_code(
-                        expr.span,
-                        "non function call in logical context",
-                        rustc_errors::DiagnosticId::Error(String::from("creusot")),
-                    )
+                    // TODO Add a "code" back in
+                    self.tcx.dcx().span_fatal(expr.span, "non function call in logical context")
                 }
             }
             ExprKind::Closure(box ClosureExpr { closure_id, .. }) => {
@@ -409,7 +404,7 @@ impl<'a, 'tcx> thir::visit::Visitor<'a, 'tcx> for PurityVisitor<'a, 'tcx> {
                 let (thir, expr) = self
                     .tcx
                     .thir_body(closure_id)
-                    .unwrap_or_else(|_| Error::from(CrErr).emit(self.tcx.sess));
+                    .unwrap_or_else(|_| Error::from(CrErr).emit(self.tcx));
                 let thir = thir.borrow();
 
                 thir::visit::walk_expr(
diff --git a/creusot/src/translation/traits.rs b/creusot/src/translation/traits.rs
index 2b542893cf..4804ddaeb8 100644
--- a/creusot/src/translation/traits.rs
+++ b/creusot/src/translation/traits.rs
@@ -316,9 +316,12 @@ pub(crate) fn still_specializable<'tcx>(
     substs: GenericArgsRef<'tcx>,
 ) -> bool {
     if let Some(trait_id) = tcx.trait_of_item(def_id) {
-        let is_final = if let Some(ImplSource::UserDefined(ud)) = resolve_impl_source_opt(tcx, param_env, def_id, substs) {
-            let trait_def =  tcx.trait_def(trait_id);
-            let leaf = trait_def.ancestors(tcx, ud.impl_def_id).unwrap().leaf_def(tcx, def_id).unwrap();
+        let is_final = if let Some(ImplSource::UserDefined(ud)) =
+            resolve_impl_source_opt(tcx, param_env, def_id, substs)
+        {
+            let trait_def = tcx.trait_def(trait_id);
+            let leaf =
+                trait_def.ancestors(tcx, ud.impl_def_id).unwrap().leaf_def(tcx, def_id).unwrap();
 
             leaf.is_final()
         } else {
@@ -327,7 +330,9 @@ pub(crate) fn still_specializable<'tcx>(
 
         let trait_generics = substs.truncate_to(tcx, tcx.generics_of(trait_id));
         !is_final && trait_generics.still_further_specializable()
-    } else if let Some(impl_id) = tcx.impl_of_method(def_id) && tcx.trait_id_of_impl(impl_id).is_some() {
+    } else if let Some(impl_id) = tcx.impl_of_method(def_id)
+        && tcx.trait_id_of_impl(impl_id).is_some()
+    {
         let is_final = tcx.defaultness(def_id).is_final();
         let trait_ref = tcx.impl_trait_ref(impl_id).unwrap();
         !is_final && trait_ref.instantiate(tcx, substs).still_further_specializable()
diff --git a/creusot/src/util.rs b/creusot/src/util.rs
index 808a5dad66..7f073a2bf6 100644
--- a/creusot/src/util.rs
+++ b/creusot/src/util.rs
@@ -67,7 +67,9 @@ pub(crate) fn is_snapshot_closure(tcx: TyCtxt, def_id: DefId) -> bool {
 }
 
 pub(crate) fn snapshot_closure_id<'tcx>(tcx: TyCtxt<'tcx>, ty: Ty<'tcx>) -> Option<DefId> {
-    if let TyKind::Closure(def_id, _) = ty.peel_refs().kind() && is_snapshot_closure(tcx, *def_id) {
+    if let TyKind::Closure(def_id, _) = ty.peel_refs().kind()
+        && is_snapshot_closure(tcx, *def_id)
+    {
         Some(*def_id)
     } else {
         None
@@ -151,7 +153,7 @@ pub(crate) fn why3_attrs(tcx: TyCtxt, def_id: DefId) -> Vec<why3::declaration::A
 }
 
 pub(crate) fn param_def_id(tcx: TyCtxt, def_id: LocalDefId) -> LocalDefId {
-    if is_spec(tcx, def_id.to_def_id()) && tcx.is_closure(def_id.to_def_id()) {
+    if is_spec(tcx, def_id.to_def_id()) && tcx.is_closure_or_coroutine(def_id.to_def_id()) {
         tcx.parent(def_id.to_def_id()).expect_local()
     } else {
         def_id
@@ -164,7 +166,7 @@ pub(crate) fn should_translate(tcx: TyCtxt, mut def_id: DefId) -> bool {
             return false;
         }
 
-        if tcx.is_closure(def_id) {
+        if tcx.is_closure_or_coroutine(def_id) {
             def_id = tcx.parent(def_id);
         } else {
             return true;
@@ -389,9 +391,8 @@ pub(crate) fn inputs_and_output<'tcx>(
     tcx: TyCtxt<'tcx>,
     def_id: DefId,
 ) -> (impl Iterator<Item = (symbol::Ident, Ty<'tcx>)>, Ty<'tcx>) {
-    let (inputs, output): (Box<dyn Iterator<Item = (rustc_span::symbol::Ident, _)>>, _) = match tcx
-        .type_of(def_id)
-        .instantiate_identity()
+    let ty = tcx.type_of(def_id).instantiate_identity();
+    let (inputs, output): (Box<dyn Iterator<Item = (rustc_span::symbol::Ident, _)>>, _) = match ty
         .kind()
     {
         TyKind::FnDef(..) => {
@@ -403,7 +404,7 @@ pub(crate) fn inputs_and_output<'tcx>(
         TyKind::Closure(_, subst) => {
             let sig = tcx.signature_unclosure(subst.as_closure().sig(), Unsafety::Normal);
             let sig = tcx.normalize_erasing_late_bound_regions(tcx.param_env(def_id), sig);
-            let env_ty = tcx.closure_env_ty(def_id, subst, tcx.lifetimes.re_erased).unwrap();
+            let env_ty = tcx.closure_env_ty(ty, subst.as_closure().kind(), tcx.lifetimes.re_erased);
 
             // I wish this could be called "self"
             let closure_env = (symbol::Ident::empty(), env_ty);
@@ -454,12 +455,16 @@ pub(crate) fn pre_sig_of<'tcx>(
         });
     }
 
-    if let TyKind::Closure(_, subst) = ctx.tcx.type_of(def_id).instantiate_identity().kind() {
+    let fn_ty = ctx.tcx.type_of(def_id).instantiate_identity();
+
+    if let TyKind::Closure(_, subst) = fn_ty.kind() {
         let self_ = Symbol::intern("_1");
         let mut pre_subst = closure_capture_subst(ctx.tcx, def_id, subst, None, self_);
 
         let mut s = HashMap::new();
-        let env_ty = ctx.closure_env_ty(def_id, subst, ctx.lifetimes.re_erased).unwrap();
+        let kind = subst.as_closure().kind();
+
+        let env_ty = ctx.closure_env_ty(fn_ty, kind, ctx.lifetimes.re_erased);
         s.insert(
             self_,
             if env_ty.is_ref() { Term::var(self_, env_ty).cur() } else { Term::var(self_, env_ty) },
@@ -470,8 +475,6 @@ pub(crate) fn pre_sig_of<'tcx>(
             pre.subst(&s);
         }
 
-        let kind = subst.as_closure().kind();
-
         if kind == ClosureKind::FnMut {
             let args = subst.as_closure().sig().inputs().skip_binder()[0];
             let unnest_subst =
@@ -749,7 +752,7 @@ pub(crate) fn closure_capture_subst<'tcx>(
     self_name: Symbol,
 ) -> ClosureSubst<'tcx> {
     let mut fun_def_id = def_id;
-    while tcx.is_closure(fun_def_id) {
+    while tcx.is_closure_or_coroutine(fun_def_id) {
         fun_def_id = tcx.parent(fun_def_id);
     }