diff --git a/kani-compiler/kani_queries/src/lib.rs b/kani-compiler/kani_queries/src/lib.rs
index cfb0cff3c8ea..b3993595eb00 100644
--- a/kani-compiler/kani_queries/src/lib.rs
+++ b/kani-compiler/kani_queries/src/lib.rs
@@ -15,7 +15,7 @@ use {
     std::sync::{Arc, Mutex},
 };
 
-#[derive(Debug, Clone, Copy, AsRefStr, EnumString, EnumVariantNames, PartialEq, Eq)]
+#[derive(Debug, Default, Clone, Copy, AsRefStr, EnumString, EnumVariantNames, PartialEq, Eq)]
 #[strum(serialize_all = "snake_case")]
 pub enum ReachabilityType {
     /// Start the cross-crate reachability analysis from all harnesses in the local crate.
@@ -23,6 +23,7 @@ pub enum ReachabilityType {
     /// Use standard rustc monomorphizer algorithm.
     Legacy,
     /// Don't perform any reachability analysis. This will skip codegen for this crate.
+    #[default]
     None,
     /// Start the cross-crate reachability analysis from all public functions in the local crate.
     PubFns,
@@ -30,12 +31,6 @@ pub enum ReachabilityType {
     Tests,
 }
 
-impl Default for ReachabilityType {
-    fn default() -> Self {
-        ReachabilityType::None
-    }
-}
-
 pub trait UserInput {
     fn set_emit_vtable_restrictions(&mut self, restrictions: bool);
     fn get_emit_vtable_restrictions(&self) -> bool;
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
index 910a842e61d0..fc88333f8325 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
@@ -365,7 +365,9 @@ impl<'tcx> GotocCtx<'tcx> {
             "add_with_overflow" => codegen_op_with_overflow!(add_overflow_result),
             "arith_offset" => self.codegen_offset(intrinsic, instance, fargs, p, loc),
             "assert_inhabited" => self.codegen_assert_intrinsic(instance, intrinsic, span),
-            "assert_uninit_valid" => self.codegen_assert_intrinsic(instance, intrinsic, span),
+            "assert_mem_uninitialized_valid" => {
+                self.codegen_assert_intrinsic(instance, intrinsic, span)
+            }
             "assert_zero_valid" => self.codegen_assert_intrinsic(instance, intrinsic, span),
             // https://doc.rust-lang.org/core/intrinsics/fn.assume.html
             // Informs the optimizer that a condition is always true.
@@ -781,9 +783,11 @@ impl<'tcx> GotocCtx<'tcx> {
             );
         }
 
+        let param_env_and_layout = ty::ParamEnv::reveal_all().and(layout);
+
         // Then we check if the type allows "raw" initialization for the cases
         // where memory is zero-initialized or entirely uninitialized
-        if intrinsic == "assert_zero_valid" && !self.tcx.permits_zero_init(layout) {
+        if intrinsic == "assert_zero_valid" && !self.tcx.permits_zero_init(param_env_and_layout) {
             return self.codegen_fatal_error(
                 PropertyClass::SafetyCheck,
                 &format!("attempted to zero-initialize type `{ty}`, which is invalid"),
@@ -791,7 +795,8 @@ impl<'tcx> GotocCtx<'tcx> {
             );
         }
 
-        if intrinsic == "assert_uninit_valid" && !self.tcx.permits_uninit_init(layout) {
+        if intrinsic == "assert_uninit_valid" && !self.tcx.permits_uninit_init(param_env_and_layout)
+        {
             return self.codegen_fatal_error(
                 PropertyClass::SafetyCheck,
                 &format!("attempted to leave type `{ty}` uninitialized, which is invalid"),
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs
index 97d0c225c963..67801f747acc 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs
@@ -243,7 +243,8 @@ impl<'tcx> GotocCtx<'tcx> {
         match t {
             TypeOrVariant::Type(t) => {
                 match t.kind() {
-                    ty::Bool
+                    ty::Alias(..)
+                    | ty::Bool
                     | ty::Char
                     | ty::Int(_)
                     | ty::Uint(_)
@@ -254,10 +255,8 @@ impl<'tcx> GotocCtx<'tcx> {
                     | ty::GeneratorWitness(..)
                     | ty::Foreign(..)
                     | ty::Dynamic(..)
-                    | ty::Projection(_)
                     | ty::Bound(..)
                     | ty::Placeholder(..)
-                    | ty::Opaque(..)
                     | ty::Param(_)
                     | ty::Infer(_)
                     | ty::Error(_) => unreachable!("type {:?} does not have a field", t),
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
index 75ee1a0e65f7..dbae4073451b 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
@@ -97,12 +97,13 @@ impl<'tcx> GotocCtx<'tcx> {
                                 let niche_value =
                                     variant_index.as_u32() - niche_variants.start().as_u32();
                                 let niche_value = (niche_value as u128).wrapping_add(*niche_start);
-                                let value =
-                                    if niche_value == 0 && tag.primitive() == Primitive::Pointer {
-                                        discr_ty.null()
-                                    } else {
-                                        Expr::int_constant(niche_value, discr_ty.clone())
-                                    };
+                                let value = if niche_value == 0
+                                    && matches!(tag.primitive(), Primitive::Pointer(_))
+                                {
+                                    discr_ty.null()
+                                } else {
+                                    Expr::int_constant(niche_value, discr_ty.clone())
+                                };
                                 let place = unwrap_or_return_codegen_unimplemented_stmt!(
                                     self,
                                     self.codegen_place(place)
@@ -145,7 +146,8 @@ impl<'tcx> GotocCtx<'tcx> {
             | StatementKind::Retag(_, _)
             | StatementKind::AscribeUserType(_, _)
             | StatementKind::Nop
-            | StatementKind::Coverage { .. } => Stmt::skip(location),
+            | StatementKind::Coverage { .. }
+            | StatementKind::ConstEvalCounter => Stmt::skip(location),
         }
         .with_location(location)
     }
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
index f315e1795fa9..278f246161eb 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
@@ -358,20 +358,41 @@ impl<'tcx> GotocCtx<'tcx> {
         // `Generator::resume(...) -> GeneratorState` function in case we
         // have an ordinary generator, or the `Future::poll(...) -> Poll`
         // function in case this is a special generator backing an async construct.
-        let ret_ty = if self.tcx.generator_is_async(*did) {
-            let state_did = self.tcx.require_lang_item(LangItem::Poll, None);
-            let state_adt_ref = self.tcx.adt_def(state_did);
-            let state_substs = self.tcx.intern_substs(&[sig.return_ty.into()]);
-            self.tcx.mk_adt(state_adt_ref, state_substs)
+        let tcx = self.tcx;
+        let (resume_ty, ret_ty) = if tcx.generator_is_async(*did) {
+            // 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.intern_substs(&[sig.return_ty.into()]);
+            let ret_ty = tcx.mk_adt(poll_adt_ref, poll_substs);
+
+            // We have to replace the `ResumeTy` that is used for type and borrow checking
+            // with `&mut Context<'_>` which is used in codegen.
+            #[cfg(debug_assertions)]
+            {
+                if let ty::Adt(resume_ty_adt, _) = sig.resume_ty.kind() {
+                    let expected_adt = tcx.adt_def(tcx.require_lang_item(LangItem::ResumeTy, None));
+                    assert_eq!(*resume_ty_adt, expected_adt);
+                } else {
+                    panic!("expected `ResumeTy`, found `{:?}`", sig.resume_ty);
+                };
+            }
+            let context_mut_ref = tcx.mk_task_context();
+
+            (context_mut_ref, ret_ty)
         } else {
-            let state_did = self.tcx.require_lang_item(LangItem::GeneratorState, None);
-            let state_adt_ref = self.tcx.adt_def(state_did);
-            let state_substs = self.tcx.intern_substs(&[sig.yield_ty.into(), sig.return_ty.into()]);
-            self.tcx.mk_adt(state_adt_ref, state_substs)
+            // 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.intern_substs(&[sig.yield_ty.into(), sig.return_ty.into()]);
+            let ret_ty = tcx.mk_adt(state_adt_ref, state_substs);
+
+            (sig.resume_ty, ret_ty)
         };
+
         ty::Binder::bind_with_vars(
-            self.tcx.mk_fn_sig(
-                [env_ty, sig.resume_ty].iter(),
+            tcx.mk_fn_sig(
+                [env_ty, resume_ty].iter(),
                 &ret_ty,
                 false,
                 Unsafety::Normal,
@@ -813,7 +834,7 @@ impl<'tcx> GotocCtx<'tcx> {
                     )
                 }
             }
-            ty::Projection(_) | ty::Opaque(_, _) => {
+            ty::Alias(..) => {
                 unreachable!("Type should've been normalized already")
             }
 
@@ -821,7 +842,11 @@ impl<'tcx> GotocCtx<'tcx> {
             ty::Bound(_, _) | ty::Param(_) => unreachable!("monomorphization bug"),
 
             // type checking remnants which shouldn't be reachable
-            ty::GeneratorWitness(_) | ty::Infer(_) | ty::Placeholder(_) | ty::Error(_) => {
+            ty::GeneratorWitness(_)
+            | ty::GeneratorWitnessMIR(_, _)
+            | ty::Infer(_)
+            | ty::Placeholder(_)
+            | ty::Error(_) => {
                 unreachable!("remnants of type checking")
             }
         }
@@ -1226,7 +1251,7 @@ impl<'tcx> GotocCtx<'tcx> {
             ty::Dynamic(..) | ty::Slice(_) | ty::Str => {
                 unreachable!("Should have generated a fat pointer")
             }
-            ty::Projection(_) | ty::Opaque(..) => {
+            ty::Alias(..) => {
                 unreachable!("Should have been removed by normalization")
             }
 
@@ -1259,6 +1284,7 @@ impl<'tcx> GotocCtx<'tcx> {
             ty::Bound(_, _) => todo!("{:?} {:?}", pointee_type, pointee_type.kind()),
             ty::Error(_) => todo!("{:?} {:?}", pointee_type, pointee_type.kind()),
             ty::GeneratorWitness(_) => todo!("{:?} {:?}", pointee_type, pointee_type.kind()),
+            ty::GeneratorWitnessMIR(_, _) => todo!("{:?} {:?}", pointee_type, pointee_type.kind()),
             ty::Infer(_) => todo!("{:?} {:?}", pointee_type, pointee_type.kind()),
             ty::Param(_) => todo!("{:?} {:?}", pointee_type, pointee_type.kind()),
             ty::Placeholder(_) => todo!("{:?} {:?}", pointee_type, pointee_type.kind()),
@@ -1609,7 +1635,7 @@ impl<'tcx> GotocCtx<'tcx> {
 
             Primitive::F32 => self.tcx.types.f32,
             Primitive::F64 => self.tcx.types.f64,
-            Primitive::Pointer => {
+            Primitive::Pointer(_) => {
                 self.tcx.mk_ptr(ty::TypeAndMut { ty: self.tcx.types.u8, mutbl: Mutability::Not })
             }
         }
diff --git a/kani-compiler/src/kani_middle/coercion.rs b/kani-compiler/src/kani_middle/coercion.rs
index 799ba3b4766c..71ddd457e075 100644
--- a/kani-compiler/src/kani_middle/coercion.rs
+++ b/kani-compiler/src/kani_middle/coercion.rs
@@ -17,7 +17,7 @@ use rustc_hir::lang_items::LangItem;
 use rustc_middle::traits::{ImplSource, ImplSourceUserDefinedData};
 use rustc_middle::ty::adjustment::CustomCoerceUnsized;
 use rustc_middle::ty::TypeAndMut;
-use rustc_middle::ty::{self, ParamEnv, TraitRef, Ty, TyCtxt};
+use rustc_middle::ty::{self, ParamEnv, Ty, TyCtxt};
 use rustc_span::symbol::Symbol;
 use tracing::trace;
 
@@ -213,10 +213,9 @@ fn custom_coerce_unsize_info<'tcx>(
 ) -> CustomCoerceUnsized {
     let def_id = tcx.require_lang_item(LangItem::CoerceUnsized, None);
 
-    let trait_ref = ty::Binder::dummy(TraitRef {
-        def_id,
-        substs: tcx.mk_substs_trait(source_ty, [target_ty.into()]),
-    });
+    let trait_ref = ty::Binder::dummy(
+        tcx.mk_trait_ref(def_id, tcx.mk_substs_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/resolve.rs b/kani-compiler/src/kani_middle/resolve.rs
index 514a73510031..3586a0b04dfa 100644
--- a/kani-compiler/src/kani_middle/resolve.rs
+++ b/kani-compiler/src/kani_middle/resolve.rs
@@ -116,7 +116,7 @@ fn to_path(tcx: TyCtxt, current_module: LocalDefId, name: &str) -> Option<Path>
             let current_module_hir_id = tcx.hir().local_def_id_to_hir_id(current_module);
             let crate_root = match tcx.hir().parent_iter(current_module_hir_id).last() {
                 None => current_module,
-                Some((hir_id, _)) => tcx.hir().local_def_id(hir_id),
+                Some((hir_id, _)) => hir_id.owner.def_id,
             };
             return Some(Path::new(
                 Base::LocalModule { id: crate_root, may_be_external_path },
@@ -139,7 +139,7 @@ fn to_path(tcx: TyCtxt, current_module: LocalDefId, name: &str) -> Option<Path>
             tracing::debug!("Unable to normalize path `{name}`: too many `super` qualifiers");
             None
         })?;
-        base_module = tcx.hir().local_def_id(parent);
+        base_module = parent.owner.def_id;
     }
 
     Some(Path::new(Base::LocalModule { id: base_module, may_be_external_path }, segments))
diff --git a/kani-compiler/src/kani_middle/stubbing/annotations.rs b/kani-compiler/src/kani_middle/stubbing/annotations.rs
index 16079efde4c5..cc4befdcae5d 100644
--- a/kani-compiler/src/kani_middle/stubbing/annotations.rs
+++ b/kani-compiler/src/kani_middle/stubbing/annotations.rs
@@ -40,7 +40,7 @@ impl Callbacks for CollectorCallbacks {
         _compiler: &Compiler,
         queries: &'tcx Queries<'tcx>,
     ) -> Compilation {
-        queries.global_ctxt().unwrap().peek_mut().enter(|tcx| {
+        queries.global_ctxt().unwrap().enter(|tcx| {
             for item in tcx.hir_crate_items(()).items() {
                 let local_def_id = item.owner_id.def_id;
                 let def_id = local_def_id.to_def_id();
diff --git a/rust-toolchain.toml b/rust-toolchain.toml
index aa6a41cddcbb..a173312be9b8 100644
--- a/rust-toolchain.toml
+++ b/rust-toolchain.toml
@@ -2,5 +2,5 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 [toolchain]
-channel = "nightly-2022-12-11"
+channel = "nightly-2023-02-03"
 components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]
diff --git a/tests/cargo-kani/vecdeque-cve/src/abstract_vecdeque.rs b/tests/cargo-kani/vecdeque-cve/src/abstract_vecdeque.rs
index c128b57dbb59..8bcc44742ed9 100644
--- a/tests/cargo-kani/vecdeque-cve/src/abstract_vecdeque.rs
+++ b/tests/cargo-kani/vecdeque-cve/src/abstract_vecdeque.rs
@@ -275,8 +275,8 @@ impl AbstractRawVec {
 
 fn handle_reserve(result: Result<(), TryReserveError>) {
     match result.map_err(|e| e.kind()) {
-        Err(CapacityOverflow) => capacity_overflow(),
-        Err(AllocError) => handle_alloc_error(),
+        Err(TryReserveErrorKind::CapacityOverflow) => capacity_overflow(),
+        Err(TryReserveErrorKind::AllocError) => handle_alloc_error(),
         Ok(()) => { /* yay */ }
     }
 }
diff --git a/tests/ui/code-location/expected b/tests/ui/code-location/expected
index 20d7f40879bc..1d188e17314a 100644
--- a/tests/ui/code-location/expected
+++ b/tests/ui/code-location/expected
@@ -1,6 +1,6 @@
 module/mod.rs:10:5 in function module::not_empty
 main.rs:13:5 in function same_file
 /toolchains/
-alloc/src/vec/mod.rs:3054:81 in function <std::vec::Vec<i32> as std::ops::Drop>::drop
+alloc/src/vec/mod.rs:3059:81 in function <std::vec::Vec<i32> as std::ops::Drop>::drop
 
 VERIFICATION:- SUCCESSFUL