diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
index e70662d4ff2a..3412cba290d2 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
@@ -649,7 +649,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 pretty_ty(actual)
             ),
         );
-        self.tcx.sess.abort_if_errors();
+        self.tcx.dcx().abort_if_errors();
         unreachable!("Rustc should have aborted already")
     }
 
@@ -1303,7 +1303,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 u64::MIN
             })
         };
-        self.tcx.sess.abort_if_errors();
+        self.tcx.dcx().abort_if_errors();
         n
     }
 
@@ -1432,7 +1432,7 @@ impl<'tcx> GotocCtx<'tcx> {
             );
             utils::span_err(self.tcx, span, err_msg);
         }
-        self.tcx.sess.abort_if_errors();
+        self.tcx.dcx().abort_if_errors();
 
         self.codegen_expr_to_place_stable(p, vec.index_array(index))
     }
@@ -1472,7 +1472,7 @@ impl<'tcx> GotocCtx<'tcx> {
             );
             utils::span_err(self.tcx, span, err_msg);
         }
-        self.tcx.sess.abort_if_errors();
+        self.tcx.dcx().abort_if_errors();
 
         // Type checker should have ensured it's a vector type
         let elem_ty = cbmc_ret_ty.base_type().unwrap().clone();
@@ -1550,7 +1550,7 @@ impl<'tcx> GotocCtx<'tcx> {
             );
             utils::span_err(self.tcx, span, err_msg);
         }
-        self.tcx.sess.abort_if_errors();
+        self.tcx.dcx().abort_if_errors();
 
         // Create the vector comparison expression
         let e = f(arg1, arg2, ret_typ);
@@ -1773,7 +1773,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 cond.ternary(t, e)
             })
             .collect();
-        self.tcx.sess.abort_if_errors();
+        self.tcx.dcx().abort_if_errors();
         let cbmc_ret_ty = self.codegen_ty_stable(rust_ret_type);
         self.codegen_expr_to_place_stable(p, Expr::vector_expr(cbmc_ret_ty, elems))
     }
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
index 661d6da38b6d..bdddd8ce9f26 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
@@ -411,7 +411,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 }
                 sig
             }
-            ty::Coroutine(did, args, _) => self.coroutine_sig(did, fntyp, args),
+            ty::Coroutine(did, args) => self.coroutine_sig(did, fntyp, args),
             _ => unreachable!("Can't get function signature of type: {:?}", fntyp),
         })
     }
diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs
index 129143937105..8b21093f4667 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs
@@ -417,10 +417,10 @@ fn check_target(session: &Session) {
             it is {}",
             &session.target.llvm_target
         );
-        session.err(err_msg);
+        session.dcx().err(err_msg);
     }
 
-    session.abort_if_errors();
+    session.dcx().abort_if_errors();
 }
 
 fn check_options(session: &Session) {
@@ -433,27 +433,27 @@ fn check_options(session: &Session) {
             let err_msg = format!(
                 "Kani requires the target architecture option `min_global_align` to be 1, but it is {align}."
             );
-            session.err(err_msg);
+            session.dcx().err(err_msg);
         }
         _ => (),
     }
 
     if session.target.options.endian != Endian::Little {
-        session.err("Kani requires the target architecture option `endian` to be `little`.");
+        session.dcx().err("Kani requires the target architecture option `endian` to be `little`.");
     }
 
     if !session.overflow_checks() {
-        session.err("Kani requires overflow checks in order to provide a sound analysis.");
+        session.dcx().err("Kani requires overflow checks in order to provide a sound analysis.");
     }
 
     if session.panic_strategy() != PanicStrategy::Abort {
-        session.err(
+        session.dcx().err(
             "Kani can only handle abort panic strategy (-C panic=abort). See for more details \
         https://github.com/model-checking/kani/issues/692",
         );
     }
 
-    session.abort_if_errors();
+    session.dcx().abort_if_errors();
 }
 
 /// Return a struct that contains information about the codegen results as expected by `rustc`.
@@ -503,8 +503,8 @@ fn symbol_table_to_gotoc(tcx: &TyCtxt, base_path: &Path) -> PathBuf {
             "Failed to generate goto model:\n\tsymtab2gb failed on file {}.",
             input_filename.display()
         );
-        tcx.sess.err(err_msg);
-        tcx.sess.abort_if_errors();
+        tcx.dcx().err(err_msg);
+        tcx.dcx().abort_if_errors();
     };
     output_filename
 }
@@ -607,7 +607,7 @@ impl GotoCodegenResults {
             msg += "\nVerification will fail if one or more of these constructs is reachable.";
             msg += "\nSee https://model-checking.github.io/kani/rust-feature-support.html for more \
             details.";
-            tcx.sess.warn(msg);
+            tcx.dcx().warn(msg);
         }
 
         if !self.concurrent_constructs.is_empty() {
@@ -618,7 +618,7 @@ impl GotoCodegenResults {
             for (construct, locations) in self.concurrent_constructs.iter() {
                 writeln!(&mut msg, "    - {construct} ({})", locations.len()).unwrap();
             }
-            tcx.sess.warn(msg);
+            tcx.dcx().warn(msg);
         }
 
         // Print some compilation stats.
diff --git a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs
index 4a30837ae812..10ee6a876588 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs
@@ -360,7 +360,7 @@ impl<'tcx> FnAbiOfHelpers<'tcx> for GotocCtx<'tcx> {
         fn_abi_request: FnAbiRequest<'tcx>,
     ) -> ! {
         if let FnAbiError::Layout(LayoutError::SizeOverflow(_)) = err {
-            self.tcx.sess.emit_fatal(respan(span, err))
+            self.tcx.dcx().emit_fatal(respan(span, err))
         } else {
             match fn_abi_request {
                 FnAbiRequest::OfFnPtr { sig, extra_args } => {
diff --git a/kani-compiler/src/codegen_cprover_gotoc/utils/utils.rs b/kani-compiler/src/codegen_cprover_gotoc/utils/utils.rs
index 22c763a00c5d..d81839ea097c 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/utils/utils.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/utils/utils.rs
@@ -194,5 +194,5 @@ impl<'tcx> GotocCtx<'tcx> {
 }
 
 pub fn span_err(tcx: TyCtxt, span: Span, msg: String) {
-    tcx.sess.span_err(rustc_internal::internal(span), msg);
+    tcx.dcx().span_err(rustc_internal::internal(span), msg);
 }
diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs
index 6fee2f110ae4..3bfef9a409f4 100644
--- a/kani-compiler/src/kani_middle/attributes.rs
+++ b/kani-compiler/src/kani_middle/attributes.rs
@@ -140,7 +140,7 @@ impl<'tcx> KaniAttributes<'tcx> {
         match self.map.get(&kind)?.as_slice() {
             [one] => Some(one),
             _ => {
-                self.tcx.sess.err(format!(
+                self.tcx.dcx().err(format!(
                     "Too many {} attributes on {}, expected 0 or 1",
                     kind.as_ref(),
                     self.tcx.def_path_debug_str(self.item)
@@ -164,7 +164,7 @@ impl<'tcx> KaniAttributes<'tcx> {
             .map(|attr| {
                 let name = expect_key_string_value(self.tcx.sess, attr)?;
                 let ok = self.resolve_sibling(name.as_str()).map_err(|e| {
-                    self.tcx.sess.span_err(
+                    self.tcx.dcx().span_err(
                         attr.span,
                         format!("Failed to resolve replacement function {}: {e}", name.as_str()),
                     )
@@ -184,7 +184,7 @@ impl<'tcx> KaniAttributes<'tcx> {
             let name = expect_key_string_value(self.tcx.sess, target)?;
             self.resolve_sibling(name.as_str()).map(|ok| (name, ok, target.span)).map_err(
                 |resolve_err| {
-                    self.tcx.sess.span_err(
+                    self.tcx.dcx().span_err(
                         target.span,
                         format!(
                             "Failed to resolve checking function {} because {resolve_err}",
@@ -233,7 +233,7 @@ impl<'tcx> KaniAttributes<'tcx> {
         // Check that all attributes are correctly used and well formed.
         let is_harness = self.is_harness();
         for (&kind, attrs) in self.map.iter() {
-            let local_error = |msg| self.tcx.sess.span_err(attrs[0].span, msg);
+            let local_error = |msg| self.tcx.dcx().span_err(attrs[0].span, msg);
 
             if !is_harness && kind.is_harness_only() {
                 local_error(format!(
@@ -319,9 +319,9 @@ impl<'tcx> KaniAttributes<'tcx> {
                     kind.as_ref()
                 );
                 if let Some(attr) = self.map.get(&kind).unwrap().first() {
-                    self.tcx.sess.span_err(attr.span, msg);
+                    self.tcx.dcx().span_err(attr.span, msg);
                 } else {
-                    self.tcx.sess.err(msg);
+                    self.tcx.dcx().err(msg);
                 }
             }
         }
@@ -343,7 +343,7 @@ impl<'tcx> KaniAttributes<'tcx> {
     fn report_unstable_forbidden(&self, unstable_attr: &UnstableAttribute) -> ErrorGuaranteed {
         let fn_name = self.tcx.def_path_str(self.item);
         self.tcx
-            .sess
+            .dcx()
             .struct_err(format!(
                 "Use of unstable feature `{}`: {}",
                 unstable_attr.feature, unstable_attr.reason
@@ -397,7 +397,7 @@ impl<'tcx> KaniAttributes<'tcx> {
                 KaniAttributeKind::CheckedWith
                 | KaniAttributeKind::IsContractGenerated
                 | KaniAttributeKind::ReplacedWith => {
-                    self.tcx.sess.span_err(self.tcx.def_span(self.item), format!("Contracts are not supported on harnesses. (Found the kani-internal contract attribute `{}`)", kind.as_ref()));
+                    self.tcx.dcx().span_err(self.tcx.def_span(self.item), format!("Contracts are not supported on harnesses. (Found the kani-internal contract attribute `{}`)", kind.as_ref()));
                 }
             };
             harness
@@ -405,7 +405,7 @@ impl<'tcx> KaniAttributes<'tcx> {
     }
 
     fn handle_proof_for_contract(&self, harness: &mut HarnessAttributes) {
-        let sess = self.tcx.sess;
+        let dcx = self.tcx.dcx();
         let (name, id, span) = match self.interpret_the_for_contract_attribute() {
             None => unreachable!(
                 "impossible, was asked to handle `proof_for_contract` but didn't find such an attribute."
@@ -415,7 +415,7 @@ impl<'tcx> KaniAttributes<'tcx> {
         };
         let Some(Ok(replacement_name)) = KaniAttributes::for_item(self.tcx, id).checked_with()
         else {
-            sess.struct_span_err(
+            dcx.struct_span_err(
                 span,
                 format!(
                     "Failed to check contract: Function `{}` has no contract.",
@@ -430,7 +430,7 @@ impl<'tcx> KaniAttributes<'tcx> {
     }
 
     fn handle_stub_verified(&self, harness: &mut HarnessAttributes) {
-        let sess = self.tcx.sess;
+        let dcx = self.tcx.dcx();
         for contract in self.interpret_stub_verified_attribute() {
             let Ok((name, def_id, span)) = contract else {
                 // This error has already been emitted so we can ignore it now.
@@ -441,7 +441,7 @@ impl<'tcx> KaniAttributes<'tcx> {
             let replacement_name = match KaniAttributes::for_item(self.tcx, def_id).replaced_with()
             {
                 None => {
-                    sess.struct_span_err(
+                    dcx.struct_span_err(
                         span,
                         format!(
                             "Failed to generate verified stub: Function `{}` has no contract.",
@@ -475,13 +475,14 @@ impl<'tcx> KaniAttributes<'tcx> {
         let tcx = self.tcx;
         expect_no_args(tcx, KaniAttributeKind::Proof, proof_attribute);
         if tcx.def_kind(self.item) != DefKind::Fn {
-            tcx.sess.span_err(span, "the `proof` attribute can only be applied to functions");
+            tcx.dcx().span_err(span, "the `proof` attribute can only be applied to functions");
         } else if tcx.generics_of(self.item).requires_monomorphization(tcx) {
-            tcx.sess.span_err(span, "the `proof` attribute cannot be applied to generic functions");
+            tcx.dcx()
+                .span_err(span, "the `proof` attribute cannot be applied to generic functions");
         } else {
             let instance = Instance::mono(tcx, self.item);
             if !super::fn_abi(tcx, instance).args.is_empty() {
-                tcx.sess.span_err(span, "functions used as harnesses cannot have any arguments");
+                tcx.dcx().span_err(span, "functions used as harnesses cannot have any arguments");
             }
         }
     }
@@ -548,7 +549,9 @@ fn expect_key_string_value(
 ) -> Result<rustc_span::Symbol, ErrorGuaranteed> {
     let span = attr.span;
     let AttrArgs::Eq(_, it) = &attr.get_normal_item().args else {
-        return Err(sess.span_err(span, "Expected attribute of the form #[attr = \"value\"]"));
+        return Err(sess
+            .dcx()
+            .span_err(span, "Expected attribute of the form #[attr = \"value\"]"));
     };
     let maybe_str = match it {
         AttrArgsEq::Ast(expr) => {
@@ -556,16 +559,16 @@ fn expect_key_string_value(
                 match LitKind::from_token_lit(tok) {
                     Ok(l) => l.str(),
                     Err(err) => {
-                        return Err(sess.span_err(
+                        return Err(sess.dcx().span_err(
                             span,
                             format!("Invalid string literal on right hand side of `=` {err:?}"),
                         ));
                     }
                 }
             } else {
-                return Err(
-                    sess.span_err(span, "Expected literal string as right hand side of `=`")
-                );
+                return Err(sess
+                    .dcx()
+                    .span_err(span, "Expected literal string as right hand side of `=`"));
             }
         }
         AttrArgsEq::Hir(lit) => lit.kind.str(),
@@ -573,7 +576,7 @@ fn expect_key_string_value(
     if let Some(str) = maybe_str {
         Ok(str)
     } else {
-        Err(sess.span_err(span, "Expected literal string as right hand side of `=`"))
+        Err(sess.dcx().span_err(span, "Expected literal string as right hand side of `=`"))
     }
 }
 
@@ -586,7 +589,7 @@ fn expect_single<'a>(
         .first()
         .expect(&format!("expected at least one attribute {} in {attributes:?}", kind.as_ref()));
     if attributes.len() > 1 {
-        tcx.sess.span_err(
+        tcx.dcx().span_err(
             attr.span,
             format!("only one '#[kani::{}]' attribute is allowed per harness", kind.as_ref()),
         );
@@ -616,7 +619,7 @@ struct UnstableAttrParseError<'a> {
 impl<'a> UnstableAttrParseError<'a> {
     /// Report the error in a friendly format.
     fn report(&self, tcx: TyCtxt) -> ErrorGuaranteed {
-        tcx.sess
+        tcx.dcx()
             .struct_span_err(
                 self.attr.span,
                 format!("failed to parse `#[kani::unstable]`: {}", self.reason),
@@ -660,7 +663,7 @@ impl<'a> TryFrom<&'a Attribute> for UnstableAttribute {
 
 fn expect_no_args(tcx: TyCtxt, kind: KaniAttributeKind, attr: &Attribute) {
     if !attr.is_word() {
-        tcx.sess
+        tcx.dcx()
             .struct_span_err(attr.span, format!("unexpected argument for `{}`", kind.as_ref()))
             .help("remove the extra argument")
             .emit();
@@ -673,7 +676,7 @@ fn parse_unwind(tcx: TyCtxt, attr: &Attribute) -> Option<u32> {
     match parse_integer(attr) {
         None => {
             // There are no integers or too many arguments given to the attribute
-            tcx.sess.span_err(
+            tcx.dcx().span_err(
                 attr.span,
                 "invalid argument for `unwind` attribute, expected an integer",
             );
@@ -683,7 +686,7 @@ fn parse_unwind(tcx: TyCtxt, attr: &Attribute) -> Option<u32> {
             if let Ok(val) = unwind_integer_value.try_into() {
                 Some(val)
             } else {
-                tcx.sess.span_err(attr.span, "value above maximum permitted value - u32::MAX");
+                tcx.dcx().span_err(attr.span, "value above maximum permitted value - u32::MAX");
                 None
             }
         }
@@ -695,7 +698,7 @@ fn parse_stubs(tcx: TyCtxt, harness: DefId, attributes: &[&Attribute]) -> Vec<St
     let check_resolve = |attr: &Attribute, name: &str| {
         let result = resolve::resolve_fn(tcx, current_module.to_local_def_id(), name);
         if let Err(err) = result {
-            tcx.sess.span_err(attr.span, format!("failed to resolve `{name}`: {err}"));
+            tcx.dcx().span_err(attr.span, format!("failed to resolve `{name}`: {err}"));
         }
     };
     attributes
@@ -708,7 +711,7 @@ fn parse_stubs(tcx: TyCtxt, harness: DefId, attributes: &[&Attribute]) -> Vec<St
                     Some(Stub { original: orig.clone(), replacement: replace.clone() })
                 }
                 _ => {
-                    tcx.sess.span_err(
+                    tcx.dcx().span_err(
                         attr.span,
                         format!(
                             "attribute `kani::stub` takes two path arguments; found {}",
@@ -719,7 +722,7 @@ fn parse_stubs(tcx: TyCtxt, harness: DefId, attributes: &[&Attribute]) -> Vec<St
                 }
             },
             Err(error_span) => {
-                tcx.sess.span_err(
+                tcx.dcx().span_err(
                     error_span,
                         "attribute `kani::stub` takes two path arguments; found argument that is not a path",
                 );
@@ -734,7 +737,7 @@ fn parse_solver(tcx: TyCtxt, attr: &Attribute) -> Option<CbmcSolver> {
     // <https://github.com/model-checking/kani/issues/2192>
     const ATTRIBUTE: &str = "#[kani::solver]";
     let invalid_arg_err = |attr: &Attribute| {
-        tcx.sess.span_err(
+        tcx.dcx().span_err(
                 attr.span,
                 format!("invalid argument for `{ATTRIBUTE}` attribute, expected one of the supported solvers (e.g. `kissat`) or a SAT solver binary (e.g. `bin=\"<SAT_SOLVER_BINARY>\"`)")
             )
@@ -742,7 +745,7 @@ fn parse_solver(tcx: TyCtxt, attr: &Attribute) -> Option<CbmcSolver> {
 
     let attr_args = attr.meta_item_list().unwrap();
     if attr_args.len() != 1 {
-        tcx.sess.span_err(
+        tcx.dcx().span_err(
             attr.span,
             format!(
                 "the `{ATTRIBUTE}` attribute expects a single argument. Got {} arguments.",
@@ -766,7 +769,7 @@ fn parse_solver(tcx: TyCtxt, attr: &Attribute) -> Option<CbmcSolver> {
             match solver {
                 Ok(solver) => Some(solver),
                 Err(_) => {
-                    tcx.sess.span_err(attr.span, format!("unknown solver `{ident_str}`"));
+                    tcx.dcx().span_err(attr.span, format!("unknown solver `{ident_str}`"));
                     None
                 }
             }
@@ -873,7 +876,7 @@ fn attr_kind(tcx: TyCtxt, attr: &Attribute) -> Option<KaniAttributeKind> {
                 KaniAttributeKind::try_from(ident_str.as_str())
                     .map_err(|err| {
                         debug!(?err, "attr_kind_failed");
-                        tcx.sess.span_err(attr.span, format!("unknown attribute `{ident_str}`"));
+                        tcx.dcx().span_err(attr.span, format!("unknown attribute `{ident_str}`"));
                         err
                     })
                     .ok()
diff --git a/kani-compiler/src/kani_middle/mod.rs b/kani-compiler/src/kani_middle/mod.rs
index 5d1b148b963f..4ccac4f485fe 100644
--- a/kani-compiler/src/kani_middle/mod.rs
+++ b/kani-compiler/src/kani_middle/mod.rs
@@ -57,15 +57,15 @@ pub fn check_crate_items(tcx: TyCtxt, ignore_asm: bool) {
                     `--enable-unstable --ignore-global-asm` to suppress this error \
                     (**Verification results may be impacted**).",
                 );
-                tcx.sess.err(error_msg);
+                tcx.dcx().err(error_msg);
             } else {
-                tcx.sess.warn(format!(
+                tcx.dcx().warn(format!(
                     "Ignoring global ASM in crate {krate}. Verification results may be impacted.",
                 ));
             }
         }
     }
-    tcx.sess.abort_if_errors();
+    tcx.dcx().abort_if_errors();
 }
 
 /// Check that all given items are supported and there's no misconfiguration.
@@ -97,7 +97,7 @@ pub fn check_reachable_items(tcx: TyCtxt, queries: &QueryDb, items: &[MonoItem])
             }
         }
     }
-    tcx.sess.abort_if_errors();
+    tcx.dcx().abort_if_errors();
 }
 
 /// A basic check that ensures a function with a contract does not receive
@@ -122,7 +122,7 @@ fn check_is_contract_safe(tcx: TyCtxt, instance: Instance) {
         fn visit_ty(&mut self, ty: &Ty) -> std::ops::ControlFlow<Self::Break> {
             if (self.is_prohibited)(*ty) {
                 // TODO make this more user friendly
-                self.tcx.sess.err(format!(
+                self.tcx.dcx().err(format!(
                     "{} contains a {}pointer ({}). This is prohibited for functions with contracts, \
                     as they cannot yet reason about the pointer behavior.", self.r#where, self.what,
                     pretty_ty(ty.kind())));
@@ -166,7 +166,7 @@ fn check_is_contract_safe(tcx: TyCtxt, instance: Instance) {
 
     for var in &bound_fn_sig.bound_vars {
         if let BoundVariableKind::Ty(t) = var {
-            tcx.sess.span_err(
+            tcx.dcx().span_err(
                 rustc_internal::internal(instance.def.span()),
                 format!("Found a bound type variable {t:?} after monomorphization"),
             );
@@ -293,7 +293,7 @@ impl<'tcx> FnAbiOfHelpers<'tcx> for CompilerHelpers<'tcx> {
         fn_abi_request: FnAbiRequest<'tcx>,
     ) -> ! {
         if let FnAbiError::Layout(LayoutError::SizeOverflow(_)) = err {
-            self.tcx.sess.emit_fatal(respan(span, err))
+            self.tcx.dcx().emit_fatal(respan(span, err))
         } else {
             match fn_abi_request {
                 FnAbiRequest::OfFnPtr { sig, extra_args } => {
diff --git a/kani-compiler/src/kani_middle/reachability.rs b/kani-compiler/src/kani_middle/reachability.rs
index 024434f6ac2f..424077a622f9 100644
--- a/kani-compiler/src/kani_middle/reachability.rs
+++ b/kani-compiler/src/kani_middle/reachability.rs
@@ -53,7 +53,7 @@ pub fn collect_reachable_items(tcx: TyCtxt, starting_points: &[MonoItem]) -> Vec
         .dump_dot(tcx)
         .unwrap_or_else(|e| tracing::error!("Failed to dump call graph: {e}"));
 
-    tcx.sess.abort_if_errors();
+    tcx.dcx().abort_if_errors();
     // Sort the result so code generation follows deterministic order.
     // This helps us to debug the code, but it also provides the user a good experience since the
     // order of the errors and warnings is stable.
@@ -412,7 +412,7 @@ impl<'a, 'tcx> MirVisitor for MonoItemsFnCollector<'a, 'tcx> {
                                 let receiver_ty = args.0[0].expect_ty();
                                 let sep = callee.rfind("::").unwrap();
                                 let trait_ = &callee[..sep];
-                                self.tcx.sess.span_err(
+                                self.tcx.dcx().span_err(
                                     rustc_internal::internal(terminator.span),
                                     format!(
                                         "`{}` doesn't implement \
diff --git a/kani-compiler/src/kani_middle/stubbing/annotations.rs b/kani-compiler/src/kani_middle/stubbing/annotations.rs
index a8554cf9e2a2..52b994ab97d2 100644
--- a/kani-compiler/src/kani_middle/stubbing/annotations.rs
+++ b/kani-compiler/src/kani_middle/stubbing/annotations.rs
@@ -25,7 +25,7 @@ fn stub_def_ids(tcx: TyCtxt, harness: LocalDefId, stub: &Stub) -> Option<(DefId,
                 Some(def_id)
             }
             Err(err) => {
-                tcx.sess
+                tcx.dcx()
                     .span_err(tcx.def_span(harness), format!("failed to resolve `{name}`: {err}"));
                 None
             }
@@ -50,7 +50,7 @@ pub fn update_stub_mapping(
         let other_opt = stub_pairs.insert(orig_hash, stub_hash);
         if let Some(other) = other_opt {
             if other != stub_hash {
-                tcx.sess.span_err(
+                tcx.dcx().span_err(
                     tcx.def_span(harness),
                     format!(
                         "duplicate stub mapping: {} mapped to {} and {}",
diff --git a/kani-compiler/src/kani_middle/stubbing/mod.rs b/kani-compiler/src/kani_middle/stubbing/mod.rs
index 9b83ae2f2415..9dda0144eda4 100644
--- a/kani-compiler/src/kani_middle/stubbing/mod.rs
+++ b/kani-compiler/src/kani_middle/stubbing/mod.rs
@@ -109,7 +109,7 @@ impl<'tcx> MirVisitor for StubConstChecker<'tcx> {
                         tcx.def_path_str(trait_),
                         self.source.name()
                     );
-                    tcx.sess.span_err(rustc_internal::internal(location.span()), msg);
+                    tcx.dcx().span_err(rustc_internal::internal(location.span()), msg);
                     self.is_valid = false;
                 }
             }
diff --git a/kani-compiler/src/kani_middle/stubbing/transform.rs b/kani-compiler/src/kani_middle/stubbing/transform.rs
index a455a8d5e7ca..ff845b188dca 100644
--- a/kani-compiler/src/kani_middle/stubbing/transform.rs
+++ b/kani-compiler/src/kani_middle/stubbing/transform.rs
@@ -101,7 +101,7 @@ fn check_compatibility<'a, 'tcx>(
 ) -> bool {
     // Check whether the arities match.
     if old_body.arg_count != stub_body.arg_count {
-        tcx.sess.span_err(
+        tcx.dcx().span_err(
             tcx.def_span(stub_def_id),
             format!(
                 "arity mismatch: original function/method `{}` takes {} argument(s), stub `{}` takes {}",
@@ -117,7 +117,7 @@ fn check_compatibility<'a, 'tcx>(
     let old_num_generics = tcx.generics_of(old_def_id).count();
     let stub_num_generics = tcx.generics_of(stub_def_id).count();
     if old_num_generics != stub_num_generics {
-        tcx.sess.span_err(
+        tcx.dcx().span_err(
             tcx.def_span(stub_def_id),
             format!(
                 "mismatch in the number of generic parameters: original function/method `{}` takes {} generic parameters(s), stub `{}` takes {}",
@@ -146,7 +146,7 @@ fn check_compatibility<'a, 'tcx>(
             } else {
                 format!("type of parameter {} differs", i - 1)
             };
-            tcx.sess.span_err(
+            tcx.dcx().span_err(
                 new_arg.source_info.span,
                 format!(
                     "{prefix}: stub `{}` has type `{}` where original function/method `{}` has type `{}`",
diff --git a/rust-toolchain.toml b/rust-toolchain.toml
index fe2513be9b06..620fdc1efa29 100644
--- a/rust-toolchain.toml
+++ b/rust-toolchain.toml
@@ -2,5 +2,5 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 [toolchain]
-channel = "nightly-2023-12-20"
+channel = "nightly-2024-01-08"
 components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]
diff --git a/tools/bookrunner/librustdoc/doctest.rs b/tools/bookrunner/librustdoc/doctest.rs
index 01fc395046f2..cf0fdc106e38 100644
--- a/tools/bookrunner/librustdoc/doctest.rs
+++ b/tools/bookrunner/librustdoc/doctest.rs
@@ -65,7 +65,7 @@ pub fn make_test(
     // crate already is included.
     let result = rustc_driver::catch_fatal_errors(|| {
         rustc_span::create_session_if_not_set_then(edition, |_| {
-            use rustc_errors::emitter::{Emitter, EmitterWriter};
+            use rustc_errors::emitter::{Emitter, HumanEmitter};
             use rustc_errors::DiagCtxt;
             use rustc_parse::maybe_new_parser_from_source_str;
             use rustc_parse::parser::ForceCollect;
@@ -81,11 +81,11 @@ pub fn make_test(
 
             let fallback_bundle =
                 rustc_errors::fallback_fluent_bundle(DEFAULT_LOCALE_RESOURCES.to_vec(), false);
-            supports_color = EmitterWriter::stderr(ColorConfig::Auto, fallback_bundle.clone())
+            supports_color = HumanEmitter::stderr(ColorConfig::Auto, fallback_bundle.clone())
                 .diagnostic_width(Some(80))
                 .supports_color();
 
-            let emitter = EmitterWriter::new(Box::new(io::sink()), fallback_bundle);
+            let emitter = HumanEmitter::new(Box::new(io::sink()), fallback_bundle);
 
             // FIXME(misdreavus): pass `-Z treat-err-as-bug` to the doctest parser
             let handler = DiagCtxt::with_emitter(Box::new(emitter));