diff --git a/cprover_bindings/src/goto_program/expr.rs b/cprover_bindings/src/goto_program/expr.rs
index 3a6da89239b5..4031d08fa9aa 100644
--- a/cprover_bindings/src/goto_program/expr.rs
+++ b/cprover_bindings/src/goto_program/expr.rs
@@ -1410,7 +1410,7 @@ impl Expr {
         ArithmeticOverflowResult { result, overflowed }
     }
 
-    /// Uses CBMC's [binop]-with-overflow operation that performs a single arithmetic
+    /// Uses CBMC's \[binop\]-with-overflow operation that performs a single arithmetic
     /// operation
     /// `struct (T, bool) overflow(binop, self, e)` where `T` is the type of `self`
     /// Pseudocode:
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/foreign_function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/foreign_function.rs
index a102fb5fcd7b..52b6ef0cc821 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/foreign_function.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/foreign_function.rs
@@ -110,16 +110,15 @@ impl<'tcx> GotocCtx<'tcx> {
             .args
             .iter()
             .enumerate()
-            .filter_map(|(idx, arg)| {
-                (!arg.is_ignore()).then(|| {
-                    let arg_name = format!("{fn_name}::param_{idx}");
-                    let base_name = format!("param_{idx}");
-                    let arg_type = self.codegen_ty(arg.layout.ty);
-                    let sym = Symbol::variable(&arg_name, &base_name, arg_type.clone(), loc)
-                        .with_is_parameter(true);
-                    self.symbol_table.insert(sym);
-                    arg_type.as_parameter(Some(arg_name.into()), Some(base_name.into()))
-                })
+            .filter(|&(_, arg)| (!arg.is_ignore()))
+            .map(|(idx, arg)| {
+                let arg_name = format!("{fn_name}::param_{idx}");
+                let base_name = format!("param_{idx}");
+                let arg_type = self.codegen_ty(arg.layout.ty);
+                let sym = Symbol::variable(&arg_name, &base_name, arg_type.clone(), loc)
+                    .with_is_parameter(true);
+                self.symbol_table.insert(sym);
+                arg_type.as_parameter(Some(arg_name.into()), Some(base_name.into()))
             })
             .collect();
         let ret_type = self.codegen_ty(fn_abi.ret.layout.ty);
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs
index 800ec8219e40..77d68af745ae 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs
@@ -187,7 +187,7 @@ impl<'tcx> GotocCtx<'tcx> {
 
         let tupe = sig.inputs().last().unwrap();
         let args = match tupe.kind() {
-            ty::Tuple(substs) => *substs,
+            ty::Tuple(args) => *args,
             _ => unreachable!("a function's spread argument must be a tuple"),
         };
         let starting_idx = sig.inputs().len();
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
index 0f4279a97a14..10fe28caf9bd 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
@@ -245,7 +245,7 @@ impl<'tcx> GotocCtx<'tcx> {
 
         macro_rules! codegen_size_align {
             ($which: ident) => {{
-                let tp_ty = instance.substs.type_at(0);
+                let tp_ty = instance.args.type_at(0);
                 let arg = fargs.remove(0);
                 let size_align = self.size_and_align_of_dst(tp_ty, arg);
                 self.codegen_expr_to_place(p, size_align.$which)
@@ -422,7 +422,7 @@ impl<'tcx> GotocCtx<'tcx> {
             "cttz" => codegen_count_intrinsic!(cttz, true),
             "cttz_nonzero" => codegen_count_intrinsic!(cttz, false),
             "discriminant_value" => {
-                let ty = instance.substs.type_at(0);
+                let ty = instance.args.type_at(0);
                 let e = self.codegen_get_discriminant(fargs.remove(0).dereference(), ty, ret_ty);
                 self.codegen_expr_to_place(p, e)
             }
@@ -764,7 +764,7 @@ impl<'tcx> GotocCtx<'tcx> {
         intrinsic: &str,
         span: Option<Span>,
     ) -> Stmt {
-        let ty = instance.substs.type_at(0);
+        let ty = instance.args.type_at(0);
         let layout = self.layout_of(ty);
         // Note: We follow the pattern seen in `codegen_panic_intrinsic` from `rustc_codegen_ssa`
         // https://github.com/rust-lang/rust/blob/master/compiler/rustc_codegen_ssa/src/mir/block.rs
@@ -1034,7 +1034,7 @@ impl<'tcx> GotocCtx<'tcx> {
         let offset = fargs.remove(0);
 
         // Check that computing `offset` in bytes would not overflow
-        let ty = self.monomorphize(instance.substs.type_at(0));
+        let ty = self.monomorphize(instance.args.type_at(0));
         let (offset_bytes, bytes_overflow_check) =
             self.count_in_bytes(offset.clone(), ty, Type::ssize_t(), intrinsic, loc);
 
@@ -1184,7 +1184,7 @@ impl<'tcx> GotocCtx<'tcx> {
         p: &Place<'tcx>,
         loc: Location,
     ) -> Stmt {
-        let ty = self.monomorphize(instance.substs.type_at(0));
+        let ty = self.monomorphize(instance.args.type_at(0));
         let dst = fargs.remove(0).cast_to(Type::void_pointer());
         let val = fargs.remove(0).cast_to(Type::void_pointer());
         let layout = self.layout_of(ty);
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs
index 49761a8656a3..3c46404f71bc 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs
@@ -139,7 +139,7 @@ impl<'tcx> GotocCtx<'tcx> {
             }
             ConstValue::ZeroSized => match lit_ty.kind() {
                 // Rust "function items" (not closures, not function pointers, see `codegen_fndef`)
-                ty::FnDef(d, substs) => self.codegen_fndef(*d, substs, span),
+                ty::FnDef(d, args) => self.codegen_fndef(*d, args, span),
                 _ => Expr::init_unit(self.codegen_ty(lit_ty), &self.symbol_table),
             },
         }
@@ -693,11 +693,11 @@ impl<'tcx> GotocCtx<'tcx> {
     pub fn codegen_fndef(
         &mut self,
         d: DefId,
-        substs: ty::subst::SubstsRef<'tcx>,
+        args: ty::GenericArgsRef<'tcx>,
         span: Option<&Span>,
     ) -> Expr {
         let instance =
-            Instance::resolve(self.tcx, ty::ParamEnv::reveal_all(), d, substs).unwrap().unwrap();
+            Instance::resolve(self.tcx, ty::ParamEnv::reveal_all(), d, args).unwrap().unwrap();
         self.codegen_fn_item(instance, span)
     }
 
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs
index e24af9d9ecb1..fbb9cc90cdaa 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs
@@ -368,7 +368,7 @@ impl<'tcx> GotocCtx<'tcx> {
     fn codegen_local_fndef(&mut self, ty: ty::Ty<'tcx>) -> Option<Expr> {
         match ty.kind() {
             // A local that is itself a FnDef, like Fn::call_once
-            ty::FnDef(defid, substs) => Some(self.codegen_fndef(*defid, substs, None)),
+            ty::FnDef(defid, args) => Some(self.codegen_fndef(*defid, args, None)),
             // A local can be pointer to a FnDef, like Fn::call and Fn::call_mut
             ty::RawPtr(inner) => self
                 .codegen_local_fndef(inner.ty)
@@ -513,14 +513,14 @@ impl<'tcx> GotocCtx<'tcx> {
                 // https://rust-lang.github.io/rfcs/2359-subslice-pattern-syntax.html
                 match before.mir_typ().kind() {
                     ty::Array(ty, len) => {
-                        let len = len.kind().try_to_target_usize(self.tcx).unwrap();
+                        let len = len.try_to_target_usize(self.tcx).unwrap();
                         let subarray_len = if from_end {
                             // `to` counts from the end of the array
                             len - to - from
                         } else {
                             to - from
                         };
-                        let typ = self.tcx.mk_array(*ty, subarray_len);
+                        let typ = Ty::new_array(self.tcx, *ty, subarray_len);
                         let goto_typ = self.codegen_ty(typ);
                         // unimplemented
                         Err(UnimplementedData::new(
@@ -542,9 +542,9 @@ impl<'tcx> GotocCtx<'tcx> {
                         } else {
                             Expr::int_constant(to - from, Type::size_t())
                         };
-                        let typ = self.tcx.mk_slice(*elemt);
+                        let typ = Ty::new_slice(self.tcx, *elemt);
                         let typ_and_mut = TypeAndMut { ty: typ, mutbl: Mutability::Mut };
-                        let ptr_typ = self.tcx.mk_ptr(typ_and_mut);
+                        let ptr_typ = Ty::new_ptr(self.tcx, typ_and_mut);
                         let goto_type = self.codegen_ty(ptr_typ);
 
                         let index = Expr::int_constant(from, Type::ssize_t());
@@ -704,7 +704,7 @@ impl<'tcx> GotocCtx<'tcx> {
         match before.mir_typ().kind() {
             //TODO, ask on zulip if we can ever have from_end here?
             ty::Array(elemt, length) => {
-                let length = length.kind().try_to_target_usize(self.tcx).unwrap();
+                let length = length.try_to_target_usize(self.tcx).unwrap();
                 assert!(length >= min_length);
                 let idx = if from_end { length - offset } else { offset };
                 let idxe = Expr::int_constant(idx, Type::ssize_t());
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
index bfb3313a5ae9..f57f42137574 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
@@ -20,7 +20,7 @@ use num::bigint::BigInt;
 use rustc_abi::FieldIdx;
 use rustc_index::IndexVec;
 use rustc_middle::mir::{AggregateKind, BinOp, CastKind, NullOp, Operand, Place, Rvalue, UnOp};
-use rustc_middle::ty::adjustment::PointerCast;
+use rustc_middle::ty::adjustment::PointerCoercion;
 use rustc_middle::ty::layout::LayoutOf;
 use rustc_middle::ty::{self, Instance, IntTy, Ty, TyCtxt, UintTy, VtblEntry};
 use rustc_target::abi::{FieldsShape, Size, TagEncoding, VariantIdx, Variants};
@@ -706,7 +706,7 @@ impl<'tcx> GotocCtx<'tcx> {
                     "https://github.com/model-checking/kani/issues/1784",
                 )
             }
-            Rvalue::Cast(CastKind::Pointer(k), e, t) => {
+            Rvalue::Cast(CastKind::PointerCoercion(k), e, t) => {
                 let t = self.monomorphize(*t);
                 self.codegen_pointer_cast(k, e, t, loc)
             }
@@ -738,7 +738,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 // See https://github.com/rust-lang/compiler-team/issues/460 for more details.
                 let operand = self.codegen_operand(operand);
                 let t = self.monomorphize(*content_ty);
-                let box_ty = self.tcx.mk_box(t);
+                let box_ty = Ty::new_box(self.tcx, t);
                 let box_ty = self.codegen_ty(box_ty);
                 let cbmc_t = self.codegen_ty(t);
                 let box_contents = operand.cast_to(cbmc_t.to_pointer());
@@ -991,22 +991,22 @@ impl<'tcx> GotocCtx<'tcx> {
     }
 
     /// "Pointer casts" are particular kinds of pointer-to-pointer casts.
-    /// See the [`PointerCast`] type for specifics.
+    /// See the [`PointerCoercion`] type for specifics.
     /// Note that this does not include all casts involving pointers,
     /// many of which are instead handled by [`Self::codegen_misc_cast`] instead.
     fn codegen_pointer_cast(
         &mut self,
-        k: &PointerCast,
+        k: &PointerCoercion,
         operand: &Operand<'tcx>,
         t: Ty<'tcx>,
         loc: Location,
     ) -> Expr {
         debug!(cast=?k, op=?operand, ?loc, "codegen_pointer_cast");
         match k {
-            PointerCast::ReifyFnPointer => match self.operand_ty(operand).kind() {
-                ty::FnDef(def_id, substs) => {
+            PointerCoercion::ReifyFnPointer => match self.operand_ty(operand).kind() {
+                ty::FnDef(def_id, args) => {
                     let instance =
-                        Instance::resolve(self.tcx, ty::ParamEnv::reveal_all(), *def_id, substs)
+                        Instance::resolve(self.tcx, ty::ParamEnv::reveal_all(), *def_id, args)
                             .unwrap()
                             .unwrap();
                     // We need to handle this case in a special way because `codegen_operand` compiles FnDefs to dummy structs.
@@ -1015,24 +1015,20 @@ impl<'tcx> GotocCtx<'tcx> {
                 }
                 _ => unreachable!(),
             },
-            PointerCast::UnsafeFnPointer => self.codegen_operand(operand),
-            PointerCast::ClosureFnPointer(_) => {
-                if let ty::Closure(def_id, substs) = self.operand_ty(operand).kind() {
-                    let instance = Instance::resolve_closure(
-                        self.tcx,
-                        *def_id,
-                        substs,
-                        ty::ClosureKind::FnOnce,
-                    )
-                    .expect("failed to normalize and resolve closure during codegen")
-                    .polymorphize(self.tcx);
+            PointerCoercion::UnsafeFnPointer => self.codegen_operand(operand),
+            PointerCoercion::ClosureFnPointer(_) => {
+                if let ty::Closure(def_id, args) = self.operand_ty(operand).kind() {
+                    let instance =
+                        Instance::resolve_closure(self.tcx, *def_id, args, ty::ClosureKind::FnOnce)
+                            .expect("failed to normalize and resolve closure during codegen")
+                            .polymorphize(self.tcx);
                     self.codegen_func_expr(instance, None).address_of()
                 } else {
                     unreachable!("{:?} cannot be cast to a fn ptr", operand)
                 }
             }
-            PointerCast::MutToConstPointer => self.codegen_operand(operand),
-            PointerCast::ArrayToPointer => {
+            PointerCoercion::MutToConstPointer => self.codegen_operand(operand),
+            PointerCoercion::ArrayToPointer => {
                 // TODO: I am not sure whether it is correct or not.
                 //
                 // some reasoning is as follows.
@@ -1054,7 +1050,7 @@ impl<'tcx> GotocCtx<'tcx> {
                     _ => unreachable!(),
                 }
             }
-            PointerCast::Unsize => {
+            PointerCoercion::Unsize => {
                 let src_goto_expr = self.codegen_operand(operand);
                 let src_mir_type = self.operand_ty(operand);
                 let dst_mir_type = t;
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/static_var.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/static_var.rs
index e71bea1f2066..13e4a5402e06 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/static_var.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/static_var.rs
@@ -7,7 +7,7 @@ use crate::codegen_cprover_gotoc::GotocCtx;
 use cbmc::goto_program::Symbol;
 use rustc_hir::def_id::DefId;
 use rustc_middle::mir::mono::MonoItem;
-use rustc_middle::ty::{subst::InternalSubsts, Instance};
+use rustc_middle::ty::{GenericArgs, Instance};
 use tracing::debug;
 
 impl<'tcx> GotocCtx<'tcx> {
@@ -28,10 +28,10 @@ impl<'tcx> GotocCtx<'tcx> {
         // Unique mangled monomorphized name.
         let symbol_name = item.symbol_name(self.tcx).to_string();
         // Pretty name which may include function name.
-        let pretty_name = Instance::new(def_id, InternalSubsts::empty()).to_string();
+        let pretty_name = Instance::new(def_id, GenericArgs::empty()).to_string();
         debug!(?symbol_name, ?pretty_name, "declare_static {}", item);
 
-        let typ = self.codegen_ty(self.tcx.type_of(def_id).subst_identity());
+        let typ = self.codegen_ty(self.tcx.type_of(def_id).instantiate_identity());
         let span = self.tcx.def_span(def_id);
         let location = self.codegen_span(&span);
         let symbol = Symbol::static_variable(symbol_name.clone(), symbol_name, typ, location)
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
index 881dec1765f9..b1384d68013f 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
@@ -12,9 +12,9 @@ use rustc_middle::mir::{HasLocalDecls, Local, Operand, Place, Rvalue};
 use rustc_middle::ty::layout::LayoutOf;
 use rustc_middle::ty::print::with_no_trimmed_paths;
 use rustc_middle::ty::print::FmtPrinter;
-use rustc_middle::ty::subst::InternalSubsts;
+use rustc_middle::ty::GenericArgsRef;
 use rustc_middle::ty::{
-    self, AdtDef, Const, FloatTy, GeneratorSubsts, Instance, IntTy, PolyFnSig, Ty, TyCtxt, TyKind,
+    self, AdtDef, Const, FloatTy, GeneratorArgs, Instance, IntTy, PolyFnSig, Ty, TyCtxt, TyKind,
     UintTy, VariantDef, VtblEntry,
 };
 use rustc_middle::ty::{List, TypeFoldable};
@@ -263,7 +263,7 @@ impl<'tcx> GotocCtx<'tcx> {
         let fn_sig = sig.skip_binder();
         if let Some((tupe, prev_args)) = fn_sig.inputs().split_last() {
             let args = match *tupe.kind() {
-                ty::Tuple(substs) => substs,
+                ty::Tuple(args) => args,
                 _ => unreachable!("the final argument of a closure must be a tuple"),
             };
 
@@ -288,14 +288,10 @@ impl<'tcx> GotocCtx<'tcx> {
         sig
     }
 
-    fn closure_sig(
-        &self,
-        def_id: DefId,
-        substs: ty::subst::SubstsRef<'tcx>,
-    ) -> ty::PolyFnSig<'tcx> {
-        let sig = self.monomorphize(substs.as_closure().sig());
+    fn closure_sig(&self, def_id: DefId, args: ty::GenericArgsRef<'tcx>) -> ty::PolyFnSig<'tcx> {
+        let sig = self.monomorphize(args.as_closure().sig());
 
-        // In addition to `def_id` and `substs`, we need to provide the kind of region `env_region`
+        // In addition to `def_id` and `args`, we need to provide the kind of region `env_region`
         // in `closure_env_ty`, which we can build from the bound variables as follows
         let bound_vars = self.tcx.mk_bound_variable_kinds_from_iter(
             sig.bound_vars().iter().chain(iter::once(ty::BoundVariableKind::Region(ty::BrEnv))),
@@ -305,7 +301,7 @@ impl<'tcx> GotocCtx<'tcx> {
             kind: ty::BoundRegionKind::BrEnv,
         };
         let env_region = ty::Region::new_late_bound(self.tcx, ty::INNERMOST, br);
-        let env_ty = self.tcx.closure_env_ty(def_id, substs, env_region).unwrap();
+        let env_ty = self.tcx.closure_env_ty(def_id, args, env_region).unwrap();
 
         let sig = sig.skip_binder();
 
@@ -334,9 +330,9 @@ impl<'tcx> GotocCtx<'tcx> {
         &self,
         did: &DefId,
         ty: Ty<'tcx>,
-        substs: ty::subst::SubstsRef<'tcx>,
+        args: ty::GenericArgsRef<'tcx>,
     ) -> ty::PolyFnSig<'tcx> {
-        let sig = substs.as_generator().poly_sig();
+        let sig = args.as_generator().poly_sig();
 
         let bound_vars = self.tcx.mk_bound_variable_kinds_from_iter(
             sig.bound_vars().iter().chain(iter::once(ty::BoundVariableKind::Region(ty::BrEnv))),
@@ -346,12 +342,12 @@ impl<'tcx> GotocCtx<'tcx> {
             kind: ty::BoundRegionKind::BrEnv,
         };
         let env_region = ty::ReLateBound(ty::INNERMOST, br);
-        let env_ty = self.tcx.mk_mut_ref(ty::Region::new_from_kind(self.tcx, env_region), ty);
+        let env_ty = Ty::new_mut_ref(self.tcx, ty::Region::new_from_kind(self.tcx, env_region), ty);
 
         let pin_did = self.tcx.require_lang_item(LangItem::Pin, None);
         let pin_adt_ref = self.tcx.adt_def(pin_did);
-        let pin_substs = self.tcx.mk_substs(&[env_ty.into()]);
-        let env_ty = self.tcx.mk_adt(pin_adt_ref, pin_substs);
+        let pin_args = self.tcx.mk_args(&[env_ty.into()]);
+        let env_ty = Ty::new_adt(self.tcx, pin_adt_ref, pin_args);
 
         let sig = sig.skip_binder();
         // The `FnSig` and the `ret_ty` here is for a generators main
@@ -363,8 +359,9 @@ impl<'tcx> GotocCtx<'tcx> {
             // The signature should be `Future::poll(_, &mut Context<'_>) -> Poll<Output>`
             let poll_did = tcx.require_lang_item(LangItem::Poll, None);
             let poll_adt_ref = tcx.adt_def(poll_did);
-            let poll_substs = tcx.mk_substs(&[sig.return_ty.into()]);
-            let ret_ty = tcx.mk_adt(poll_adt_ref, poll_substs);
+            let poll_args = tcx.mk_args(&[sig.return_ty.into()]);
+            // TODO figure out where this one went
+            let ret_ty = Ty::new_adt(tcx, poll_adt_ref, poll_args);
 
             // We have to replace the `ResumeTy` that is used for type and borrow checking
             // with `&mut Context<'_>` which is used in codegen.
@@ -377,15 +374,15 @@ impl<'tcx> GotocCtx<'tcx> {
                     panic!("expected `ResumeTy`, found `{:?}`", sig.resume_ty);
                 };
             }
-            let context_mut_ref = tcx.mk_task_context();
+            let context_mut_ref = Ty::new_task_context(tcx);
 
             (context_mut_ref, ret_ty)
         } else {
             // The signature should be `Generator::resume(_, Resume) -> GeneratorState<Yield, Return>`
             let state_did = tcx.require_lang_item(LangItem::GeneratorState, None);
             let state_adt_ref = tcx.adt_def(state_did);
-            let state_substs = tcx.mk_substs(&[sig.yield_ty.into(), sig.return_ty.into()]);
-            let ret_ty = tcx.mk_adt(state_adt_ref, state_substs);
+            let state_args = tcx.mk_args(&[sig.yield_ty.into(), sig.return_ty.into()]);
+            let ret_ty = Ty::new_adt(tcx, state_adt_ref, state_args);
 
             (sig.resume_ty, ret_ty)
         };
@@ -414,7 +411,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 }
                 sig
             }
-            ty::Generator(did, substs, _) => self.generator_sig(did, fntyp, substs),
+            ty::Generator(did, args, _) => self.generator_sig(did, fntyp, args),
             _ => unreachable!("Can't get function signature of type: {:?}", fntyp),
         })
     }
@@ -660,7 +657,7 @@ impl<'tcx> GotocCtx<'tcx> {
         // linked C libraries
         // https://github.com/model-checking/kani/issues/450
         match t.kind() {
-            TyKind::Adt(def, substs) if substs.is_empty() && def.repr().c() => {
+            TyKind::Adt(def, args) if args.is_empty() && def.repr().c() => {
                 // For non-generic #[repr(C)] types, use the literal path instead of mangling it.
                 self.tcx.def_path_str(def.did()).intern()
             }
@@ -784,9 +781,9 @@ impl<'tcx> GotocCtx<'tcx> {
             ty::Slice(e) => self.codegen_ty(*e).flexible_array_of(),
             ty::Str => Type::unsigned_int(8).flexible_array_of(),
             ty::Ref(_, t, _) | ty::RawPtr(ty::TypeAndMut { ty: t, .. }) => self.codegen_ty_ref(*t),
-            ty::FnDef(def_id, substs) => {
+            ty::FnDef(def_id, args) => {
                 let instance =
-                    Instance::resolve(self.tcx, ty::ParamEnv::reveal_all(), *def_id, substs)
+                    Instance::resolve(self.tcx, ty::ParamEnv::reveal_all(), *def_id, args)
                         .unwrap()
                         .unwrap();
                 self.codegen_fndef_type(instance)
@@ -982,9 +979,9 @@ impl<'tcx> GotocCtx<'tcx> {
     /// A closure is a struct of all its environments. That is, a closure is
     /// just a tuple with a unique type identifier, so that Fn related traits
     /// can find its impl.
-    fn codegen_ty_closure(&mut self, t: Ty<'tcx>, substs: ty::subst::SubstsRef<'tcx>) -> Type {
+    fn codegen_ty_closure(&mut self, t: Ty<'tcx>, args: ty::GenericArgsRef<'tcx>) -> Type {
         self.ensure_struct(self.ty_mangled_name(t), self.ty_pretty_name(t), |ctx, _| {
-            ctx.codegen_ty_tuple_like(t, substs.as_closure().upvar_tys().collect())
+            ctx.codegen_ty_tuple_like(t, args.as_closure().upvar_tys().to_vec())
         })
     }
 
@@ -1091,7 +1088,7 @@ impl<'tcx> GotocCtx<'tcx> {
             };
             let mut fields = vec![direct_fields];
             for var_idx in variants.indices() {
-                let variant_name = GeneratorSubsts::variant_name(var_idx).into();
+                let variant_name = GeneratorArgs::variant_name(var_idx).into();
                 fields.push(DatatypeComponent::Field {
                     name: ctx.generator_variant_name(var_idx),
                     typ: ctx.codegen_generator_variant_struct(
@@ -1156,7 +1153,7 @@ impl<'tcx> GotocCtx<'tcx> {
     }
 
     pub fn generator_variant_name(&self, var_idx: VariantIdx) -> InternedString {
-        format!("generator_variant_{}", GeneratorSubsts::variant_name(var_idx)).into()
+        format!("generator_variant_{}", GeneratorArgs::variant_name(var_idx)).into()
     }
 
     pub fn generator_field_name(&self, field_idx: usize) -> InternedString {
@@ -1346,7 +1343,7 @@ impl<'tcx> GotocCtx<'tcx> {
         &mut self,
         ty: Ty<'tcx>,
         def: &'tcx AdtDef,
-        subst: &'tcx InternalSubsts<'tcx>,
+        subst: &'tcx GenericArgsRef<'tcx>,
     ) -> Type {
         self.ensure_struct(self.ty_mangled_name(ty), self.ty_pretty_name(ty), |ctx, _| {
             let variant = &def.variants().raw[0];
@@ -1359,7 +1356,7 @@ impl<'tcx> GotocCtx<'tcx> {
     fn codegen_variant_struct_fields(
         &mut self,
         variant: &VariantDef,
-        subst: &'tcx InternalSubsts<'tcx>,
+        subst: &'tcx GenericArgsRef<'tcx>,
         layout: &LayoutS,
         initial_offset: Size,
     ) -> Vec<DatatypeComponent> {
@@ -1373,7 +1370,7 @@ impl<'tcx> GotocCtx<'tcx> {
         &mut self,
         ty: Ty<'tcx>,
         def: &'tcx AdtDef,
-        subst: &'tcx InternalSubsts<'tcx>,
+        subst: &'tcx GenericArgsRef<'tcx>,
     ) -> Type {
         self.ensure_union(self.ty_mangled_name(ty), self.ty_pretty_name(ty), |ctx, _| {
             def.variants().raw[0]
@@ -1425,7 +1422,7 @@ impl<'tcx> GotocCtx<'tcx> {
         &mut self,
         ty: Ty<'tcx>,
         adtdef: &'tcx AdtDef,
-        subst: &'tcx InternalSubsts<'tcx>,
+        subst: &'tcx GenericArgsRef<'tcx>,
     ) -> Type {
         let pretty_name = self.ty_pretty_name(ty);
         // variants appearing in source code (in source code order)
@@ -1528,7 +1525,7 @@ impl<'tcx> GotocCtx<'tcx> {
         &mut self,
         ty: Ty<'tcx>,
         adtdef: &'tcx AdtDef,
-        subst: &'tcx InternalSubsts<'tcx>,
+        subst: &'tcx GenericArgsRef<'tcx>,
         variants: &IndexVec<VariantIdx, LayoutS>,
     ) -> Type {
         let non_zst_count = variants.iter().filter(|layout| layout.size.bytes() > 0).count();
@@ -1609,9 +1606,10 @@ impl<'tcx> GotocCtx<'tcx> {
 
             Primitive::F32 => self.tcx.types.f32,
             Primitive::F64 => self.tcx.types.f64,
-            Primitive::Pointer(_) => {
-                self.tcx.mk_ptr(ty::TypeAndMut { ty: self.tcx.types.u8, mutbl: Mutability::Not })
-            }
+            Primitive::Pointer(_) => Ty::new_ptr(
+                self.tcx,
+                ty::TypeAndMut { ty: self.tcx.types.u8, mutbl: Mutability::Not },
+            ),
         }
     }
 
@@ -1631,7 +1629,7 @@ impl<'tcx> GotocCtx<'tcx> {
         name: InternedString,
         pretty_name: InternedString,
         def: &'tcx AdtDef,
-        subst: &'tcx InternalSubsts<'tcx>,
+        subst: &'tcx GenericArgsRef<'tcx>,
         layouts: &IndexVec<VariantIdx, LayoutS>,
         initial_offset: Size,
     ) -> Vec<DatatypeComponent> {
@@ -1663,7 +1661,7 @@ impl<'tcx> GotocCtx<'tcx> {
         name: InternedString,
         pretty_name: InternedString,
         case: &VariantDef,
-        subst: &'tcx InternalSubsts<'tcx>,
+        subst: &'tcx GenericArgsRef<'tcx>,
         variant: &LayoutS,
         initial_offset: Size,
     ) -> Type {
@@ -1772,7 +1770,7 @@ impl<'tcx> GotocCtx<'tcx> {
             // Codegen the type replacing the non-zst field.
             let new_name = self.ty_mangled_name(*curr).to_string() + "::WithDataPtr";
             let new_pretty_name = format!("{}::WithDataPtr", self.ty_pretty_name(*curr));
-            if let ty::Adt(adt_def, adt_substs) = curr.kind() {
+            if let ty::Adt(adt_def, adt_args) = curr.kind() {
                 let fields = &adt_def.variants().get(VariantIdx::from_u32(0)).unwrap().fields;
                 self.ensure_struct(new_name, new_pretty_name, |ctx, s_name| {
                     let fields_shape = ctx.layout_of(*curr).layout.fields();
@@ -1781,7 +1779,7 @@ impl<'tcx> GotocCtx<'tcx> {
                         .map(|idx| {
                             let idx = idx.into();
                             let name = fields[idx].name.to_string().intern();
-                            let field_ty = fields[idx].ty(ctx.tcx, adt_substs);
+                            let field_ty = fields[idx].ty(ctx.tcx, adt_args);
                             let typ = if !ctx.is_zst(field_ty) {
                                 last_type.clone()
                             } else {
@@ -1812,11 +1810,11 @@ impl<'tcx> GotocCtx<'tcx> {
         }
 
         let mut typ = struct_type;
-        while let ty::Adt(adt_def, adt_substs) = typ.kind() {
+        while let ty::Adt(adt_def, adt_args) = typ.kind() {
             assert_eq!(adt_def.variants().len(), 1, "Expected a single-variant ADT. Found {typ:?}");
             let fields = &adt_def.variants().get(VariantIdx::from_u32(0)).unwrap().fields;
             let last_field = fields.last_index().expect("Trait should be the last element.");
-            typ = fields[last_field].ty(self.tcx, adt_substs);
+            typ = fields[last_field].ty(self.tcx, adt_args);
         }
         if typ.is_trait() { Some(typ) } else { None }
     }
@@ -1859,7 +1857,7 @@ impl<'tcx> GotocCtx<'tcx> {
             type Item = (String, Ty<'tcx>);
 
             fn next(&mut self) -> Option<Self::Item> {
-                if let ty::Adt(adt_def, adt_substs) = self.curr.kind() {
+                if let ty::Adt(adt_def, adt_args) = self.curr.kind() {
                     assert_eq!(
                         adt_def.variants().len(),
                         1,
@@ -1870,8 +1868,8 @@ impl<'tcx> GotocCtx<'tcx> {
                     let fields = &adt_def.variants().get(VariantIdx::from_u32(0)).unwrap().fields;
                     let mut non_zsts = fields
                         .iter()
-                        .filter(|field| !ctx.is_zst(field.ty(ctx.tcx, adt_substs)))
-                        .map(|non_zst| (non_zst.name.to_string(), non_zst.ty(ctx.tcx, adt_substs)));
+                        .filter(|field| !ctx.is_zst(field.ty(ctx.tcx, adt_args)))
+                        .map(|non_zst| (non_zst.name.to_string(), non_zst.ty(ctx.tcx, adt_args)));
                     let (name, next) = non_zsts.next().expect("Expected one non-zst field.");
                     self.curr = next;
                     assert!(non_zsts.next().is_none(), "Expected only one non-zst field.");
diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs
index a89e5035f2a2..f30ed663338a 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs
@@ -232,7 +232,7 @@ impl CodegenBackend for GotocCodegenBackend {
                 // Cross-crate collecting of all items that are reachable from the crate harnesses.
                 let harnesses = queries.target_harnesses();
                 let mut items: HashSet<DefPathHash> = HashSet::with_capacity(harnesses.len());
-                items.extend(harnesses.into_iter());
+                items.extend(harnesses);
                 let harnesses =
                     filter_crate_items(tcx, |_, def_id| items.contains(&tcx.def_path_hash(def_id)));
                 for harness in harnesses {
@@ -321,7 +321,7 @@ impl CodegenBackend for GotocCodegenBackend {
         match ongoing_codegen.downcast::<(CodegenResults, FxIndexMap<WorkProductId, WorkProduct>)>()
         {
             Ok(val) => Ok(*val),
-            Err(val) => panic!("unexpected error: {:?}", val.type_id()),
+            Err(val) => panic!("unexpected error: {:?}", (*val).type_id()),
         }
     }
 
@@ -571,9 +571,9 @@ impl<'tcx> GotoCodegenResults<'tcx> {
         metadata: Option<HarnessMetadata>,
     ) {
         let mut items = items;
-        self.harnesses.extend(metadata.into_iter());
-        self.concurrent_constructs.extend(gcx.concurrent_constructs.into_iter());
-        self.unsupported_constructs.extend(gcx.unsupported_constructs.into_iter());
+        self.harnesses.extend(metadata);
+        self.concurrent_constructs.extend(gcx.concurrent_constructs);
+        self.unsupported_constructs.extend(gcx.unsupported_constructs);
         self.items.append(&mut items);
     }
 
diff --git a/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs b/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs
index a2c3ea3518e9..98f6f533cd12 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs
@@ -54,9 +54,7 @@ impl<'tcx> GotocCtx<'tcx> {
 
     /// A human readable name in Rust for reference, should not be used as a key.
     pub fn readable_instance_name(&self, instance: Instance<'tcx>) -> String {
-        with_no_trimmed_paths!(
-            self.tcx.def_path_str_with_substs(instance.def_id(), instance.substs)
-        )
+        with_no_trimmed_paths!(self.tcx.def_path_str_with_args(instance.def_id(), instance.args))
     }
 
     /// The actual function name used in the symbol table
diff --git a/kani-compiler/src/kani_middle/coercion.rs b/kani-compiler/src/kani_middle/coercion.rs
index 42f3cfb0a702..0f4be88bc29e 100644
--- a/kani-compiler/src/kani_middle/coercion.rs
+++ b/kani-compiler/src/kani_middle/coercion.rs
@@ -174,7 +174,7 @@ impl<'tcx> Iterator for CoerceUnsizedIterator<'tcx> {
         let src_ty = self.src_ty.take().unwrap();
         let dst_ty = self.dst_ty.take().unwrap();
         let field = match (&src_ty.kind(), &dst_ty.kind()) {
-            (&ty::Adt(src_def, src_substs), &ty::Adt(dst_def, dst_substs)) => {
+            (&ty::Adt(src_def, src_args), &ty::Adt(dst_def, dst_args)) => {
                 // Handle smart pointers by using CustomCoerceUnsized to find the field being
                 // coerced.
                 assert_eq!(src_def, dst_def);
@@ -186,8 +186,8 @@ impl<'tcx> Iterator for CoerceUnsizedIterator<'tcx> {
                     custom_coerce_unsize_info(self.tcx, src_ty, dst_ty);
                 assert!(coerce_index.as_usize() < src_fields.len());
 
-                self.src_ty = Some(src_fields[coerce_index].ty(self.tcx, src_substs));
-                self.dst_ty = Some(dst_fields[coerce_index].ty(self.tcx, dst_substs));
+                self.src_ty = Some(src_fields[coerce_index].ty(self.tcx, src_args));
+                self.dst_ty = Some(dst_fields[coerce_index].ty(self.tcx, dst_args));
                 Some(src_fields[coerce_index].name)
             }
             _ => {
@@ -213,11 +213,7 @@ fn custom_coerce_unsize_info<'tcx>(
 ) -> CustomCoerceUnsized {
     let def_id = tcx.require_lang_item(LangItem::CoerceUnsized, None);
 
-    let trait_ref = ty::Binder::dummy(TraitRef::new(
-        tcx,
-        def_id,
-        tcx.mk_substs_trait(source_ty, [target_ty.into()]),
-    ));
+    let trait_ref = TraitRef::new(tcx, def_id, tcx.mk_args_trait(source_ty, [target_ty.into()]));
 
     match tcx.codegen_select_candidate((ParamEnv::reveal_all(), trait_ref)) {
         Ok(ImplSource::UserDefined(ImplSourceUserDefinedData { impl_def_id, .. })) => {
diff --git a/kani-compiler/src/kani_middle/reachability.rs b/kani-compiler/src/kani_middle/reachability.rs
index a3110426dc57..7f1daf98ecca 100644
--- a/kani-compiler/src/kani_middle/reachability.rs
+++ b/kani-compiler/src/kani_middle/reachability.rs
@@ -28,7 +28,7 @@ use rustc_middle::mir::{
     Body, CastKind, Constant, ConstantKind, Location, Rvalue, Terminator, TerminatorKind,
 };
 use rustc_middle::span_bug;
-use rustc_middle::ty::adjustment::PointerCast;
+use rustc_middle::ty::adjustment::PointerCoercion;
 use rustc_middle::ty::{
     Closure, ClosureKind, ConstKind, EarlyBinder, Instance, InstanceDef, ParamEnv, Ty, TyCtxt,
     TyKind, TypeFoldable, VtblEntry,
@@ -355,7 +355,11 @@ impl<'a, 'tcx> MirVisitor<'tcx> for MonoItemsFnCollector<'a, 'tcx> {
         trace!(rvalue=?*rvalue, "visit_rvalue");
 
         match *rvalue {
-            Rvalue::Cast(CastKind::Pointer(PointerCast::Unsize), ref operand, target) => {
+            Rvalue::Cast(
+                CastKind::PointerCoercion(PointerCoercion::Unsize),
+                ref operand,
+                target,
+            ) => {
                 // Check if the conversion include casting a concrete type to a trait type.
                 // If so, collect items from the impl `Trait for Concrete {}`.
                 let target_ty = self.monomorphize(target);
@@ -367,7 +371,11 @@ impl<'a, 'tcx> MirVisitor<'tcx> for MonoItemsFnCollector<'a, 'tcx> {
                     self.collect_vtable_methods(base_coercion.src_ty, base_coercion.dst_ty);
                 }
             }
-            Rvalue::Cast(CastKind::Pointer(PointerCast::ReifyFnPointer), ref operand, _) => {
+            Rvalue::Cast(
+                CastKind::PointerCoercion(PointerCoercion::ReifyFnPointer),
+                ref operand,
+                _,
+            ) => {
                 let fn_ty = operand.ty(self.body, self.tcx);
                 let fn_ty = self.monomorphize(fn_ty);
                 if let TyKind::FnDef(def_id, substs) = *fn_ty.kind() {
@@ -383,7 +391,11 @@ impl<'a, 'tcx> MirVisitor<'tcx> for MonoItemsFnCollector<'a, 'tcx> {
                     unreachable!("Expected FnDef type, but got: {:?}", fn_ty);
                 }
             }
-            Rvalue::Cast(CastKind::Pointer(PointerCast::ClosureFnPointer(_)), ref operand, _) => {
+            Rvalue::Cast(
+                CastKind::PointerCoercion(PointerCoercion::ClosureFnPointer(_)),
+                ref operand,
+                _,
+            ) => {
                 let source_ty = operand.ty(self.body, self.tcx);
                 let source_ty = self.monomorphize(source_ty);
                 match *source_ty.kind() {
@@ -461,7 +473,7 @@ impl<'a, 'tcx> MirVisitor<'tcx> for MonoItemsFnCollector<'a, 'tcx> {
 
         let tcx = self.tcx;
         match terminator.kind {
-            TerminatorKind::Call { ref func, ref args, .. } => {
+            TerminatorKind::Call { ref func, args: ref outer_args, .. } => {
                 let callee_ty = func.ty(self.body, tcx);
                 let fn_ty = self.monomorphize(callee_ty);
                 if let TyKind::FnDef(def_id, substs) = *fn_ty.kind() {
@@ -479,7 +491,7 @@ impl<'a, 'tcx> MirVisitor<'tcx> for MonoItemsFnCollector<'a, 'tcx> {
                                 // implement the same traits as those in the
                                 // original function/method. A trait mismatch shows
                                 // up here, when we try to resolve a trait method
-                                let generic_ty = args[0].ty(self.body, tcx).peel_refs();
+                                let generic_ty = outer_args[0].ty(self.body, tcx).peel_refs();
                                 let receiver_ty = tcx.subst_and_normalize_erasing_regions(
                                     substs,
                                     ParamEnv::reveal_all(),
diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs
index 867142537cae..bc927559ecb5 100644
--- a/kani-driver/src/args/mod.rs
+++ b/kani-driver/src/args/mod.rs
@@ -448,7 +448,7 @@ impl CheckArgs {
 ///
 /// We currently define a bunch of cargo specific arguments as part of the overall arguments,
 /// however, they are invalid in the Kani standalone usage. Explicitly check them for now.
-/// TODO: Remove this as part of https://github.com/model-checking/kani/issues/1831
+/// TODO: Remove this as part of <https://github.com/model-checking/kani/issues/1831>
 fn check_no_cargo_opt(is_set: bool, name: &str) -> Result<(), Error> {
     if is_set {
         Err(Error::raw(
diff --git a/kani-driver/src/assess/scan.rs b/kani-driver/src/assess/scan.rs
index 88bd8f643266..17a3a56e2171 100644
--- a/kani-driver/src/assess/scan.rs
+++ b/kani-driver/src/assess/scan.rs
@@ -201,10 +201,16 @@ fn scan_cargo_projects(path: PathBuf, accumulator: &mut Vec<PathBuf>) {
         return;
     }
     // Errors are silently skipped entirely here
-    let Ok(entries) = std::fs::read_dir(path) else { return; };
+    let Ok(entries) = std::fs::read_dir(path) else {
+        return;
+    };
     for entry in entries {
-        let Ok(entry) = entry else { continue; };
-        let Ok(typ) = entry.file_type() else { continue; };
+        let Ok(entry) = entry else {
+            continue;
+        };
+        let Ok(typ) = entry.file_type() else {
+            continue;
+        };
         // symlinks are not `is_dir()`
         if typ.is_dir() {
             scan_cargo_projects(entry.path(), accumulator)
diff --git a/kani-driver/src/call_cargo.rs b/kani-driver/src/call_cargo.rs
index 82186e96a44e..6bd6a0c35f38 100644
--- a/kani-driver/src/call_cargo.rs
+++ b/kani-driver/src/call_cargo.rs
@@ -346,8 +346,7 @@ fn map_kani_artifact(rustc_artifact: cargo_metadata::Artifact) -> Option<Artifac
     let result = rustc_artifact.filenames.iter().find_map(|path| {
         if path.extension() == Some("rmeta") {
             let file_stem = path.file_stem()?.strip_prefix("lib")?;
-            let parent =
-                path.parent().map(|p| p.as_std_path().to_path_buf()).unwrap_or(PathBuf::new());
+            let parent = path.parent().map(|p| p.as_std_path().to_path_buf()).unwrap_or_default();
             let mut meta_path = parent.join(file_stem);
             meta_path.set_extension(ArtifactType::Metadata);
             trace!(rmeta=?path, kani_meta=?meta_path.display(), "map_kani_artifact");
diff --git a/library/kani_macros/src/lib.rs b/library/kani_macros/src/lib.rs
index 858efc6388d0..509fd78c03ee 100644
--- a/library/kani_macros/src/lib.rs
+++ b/library/kani_macros/src/lib.rs
@@ -22,11 +22,12 @@ use regular as attr_impl;
 
 /// Marks a Kani proof harness
 ///
-/// For async harnesses, this will call [`block_on`] to drive the future to completion (see its documentation for more information).
+/// For async harnesses, this will call [`block_on`](https://model-checking.github.io/kani/crates/doc/kani/futures/fn.block_on.html) to drive the future to completion (see its documentation for more information).
 ///
 /// If you want to spawn tasks in an async harness, you have to pass a schedule to the `#[kani::proof]` attribute,
 /// e.g. `#[kani::proof(schedule = kani::RoundRobin::default())]`.
-/// This will wrap the async function in a call to [`block_on_with_spawn`] (see its documentation for more information).
+///
+/// This will wrap the async function in a call to [`block_on_with_spawn`](https://model-checking.github.io/kani/crates/doc/kani/futures/fn.block_on_with_spawn.html) (see its documentation for more information).
 #[proc_macro_error]
 #[proc_macro_attribute]
 pub fn proof(attr: TokenStream, item: TokenStream) -> TokenStream {
@@ -51,7 +52,7 @@ pub fn should_panic(attr: TokenStream, item: TokenStream) -> TokenStream {
 }
 
 /// Set Loop unwind limit for proof harnesses
-/// The attribute '#[kani::unwind(arg)]' can only be called alongside '#[kani::proof]'.
+/// The attribute `#[kani::unwind(arg)]` can only be called alongside `#[kani::proof]`.
 /// arg - Takes in a integer value (u32) that represents the unwind value for the harness.
 #[proc_macro_attribute]
 pub fn unwind(attr: TokenStream, item: TokenStream) -> TokenStream {
@@ -71,7 +72,8 @@ pub fn stub(attr: TokenStream, item: TokenStream) -> TokenStream {
 }
 
 /// Select the SAT solver to use with CBMC for this harness
-/// The attribute `#[kani::solver(arg)]` can only be used alongside `#[kani::proof]``
+///
+/// The attribute `#[kani::solver(arg)]` can only be used alongside `#[kani::proof]`.
 ///
 /// arg - name of solver, e.g. kissat
 #[proc_macro_attribute]
diff --git a/rust-toolchain.toml b/rust-toolchain.toml
index f672b2397f5a..be6cd2da995c 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-07-01"
+channel = "nightly-2023-08-04"
 components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]
diff --git a/src/os_hacks.rs b/src/os_hacks.rs
index c8102e272595..e4a7fb9a6a4c 100644
--- a/src/os_hacks.rs
+++ b/src/os_hacks.rs
@@ -106,7 +106,9 @@ pub fn setup_os_hacks(kani_dir: &Path, os: &Info) -> Result<()> {
 fn setup_nixos_patchelf(kani_dir: &Path) -> Result<()> {
     // Encode our assumption that we're working on x86 here, because when we add ARM
     // support, we need to look for a different path.
-    assert!(env!("TARGET") == "x86_64-unknown-linux-gnu");
+    // Prevents clippy error.
+    let target = "x86_64-unknown-linux-gnu";
+    assert!(env!("TARGET") == target);
     if Path::new("/lib64/ld-linux-x86-64.so.2").exists() {
         // if the expected path exists, I guess things are fine?
         return Ok(());
diff --git a/tests/expected/slice_c_str/c_str.rs b/tests/expected/slice_c_str/c_str_fixme.rs
similarity index 89%
rename from tests/expected/slice_c_str/c_str.rs
rename to tests/expected/slice_c_str/c_str_fixme.rs
index 9fa2feedc6ea..894746772100 100644
--- a/tests/expected/slice_c_str/c_str.rs
+++ b/tests/expected/slice_c_str/c_str_fixme.rs
@@ -1,6 +1,6 @@
 #![feature(rustc_private)]
 #![feature(c_str_literals)]
-
+//! FIXME: <https://github.com/rust-lang/rust/issues/113333>
 extern crate libc;
 use libc::c_char;
 
diff --git a/tools/bookrunner/librustdoc/doctest.rs b/tools/bookrunner/librustdoc/doctest.rs
index 5d11ea7ec55b..3ec16ce7141c 100644
--- a/tools/bookrunner/librustdoc/doctest.rs
+++ b/tools/bookrunner/librustdoc/doctest.rs
@@ -110,7 +110,7 @@ pub fn make_test(
             );
 
             // FIXME(misdreavus): pass `-Z treat-err-as-bug` to the doctest parser
-            let handler = Handler::with_emitter(false, None, Box::new(emitter));
+            let handler = Handler::with_emitter(Box::new(emitter));
             let sess = ParseSess::with_span_handler(handler, sm);
 
             let mut found_main = false;
diff --git a/tools/compiletest/src/json.rs b/tools/compiletest/src/json.rs
index 299d81578eb3..ec1de29aa640 100644
--- a/tools/compiletest/src/json.rs
+++ b/tools/compiletest/src/json.rs
@@ -59,18 +59,19 @@ pub fn extract_rendered(output: &str) -> String {
                     } else {
                         Some(format!(
                             "Future incompatibility report: {}",
-                            report
-                                .future_incompat_report
-                                .into_iter()
-                                .map(|item| {
-                                    format!(
-                                        "Future breakage diagnostic:\n{}",
-                                        item.diagnostic
-                                            .rendered
-                                            .unwrap_or_else(|| "Not rendered".to_string())
-                                    )
-                                })
-                                .collect::<String>()
+                            report.future_incompat_report.into_iter().fold(
+                                String::new(),
+                                |mut output, item| {
+                                    use std::fmt::Write;
+                                    let _ = write!(output, "Future breakage diagnostic:\n");
+                                    let s = item
+                                        .diagnostic
+                                        .rendered
+                                        .unwrap_or_else(|| "Not rendered".to_string());
+                                    let _ = write!(output, "{s}");
+                                    output
+                                }
+                            )
                         ))
                     }
                 } else if serde_json::from_str::<ArtifactNotification>(line).is_ok() {