diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
index fc88333f8325..b64725f9324d 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
@@ -1226,14 +1226,16 @@ impl<'tcx> GotocCtx<'tcx> {
             // `simd_shuffle4`) is type-checked
             match farg_types[2].kind() {
                 ty::Array(ty, len) if matches!(ty.kind(), ty::Uint(ty::UintTy::U32)) => {
-                    len.try_eval_usize(self.tcx, ty::ParamEnv::reveal_all()).unwrap_or_else(|| {
-                        self.tcx.sess.span_err(
-                            span.unwrap(),
-                            "could not evaluate shuffle index array length",
-                        );
-                        // Return a dummy value
-                        u64::MIN
-                    })
+                    len.try_eval_target_usize(self.tcx, ty::ParamEnv::reveal_all()).unwrap_or_else(
+                        || {
+                            self.tcx.sess.span_err(
+                                span.unwrap(),
+                                "could not evaluate shuffle index array length",
+                            );
+                            // Return a dummy value
+                            u64::MIN
+                        },
+                    )
                 }
                 _ => {
                     let err_msg = format!(
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
index e17cd7f3031a..29d636cc4150 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
@@ -144,7 +144,7 @@ impl<'tcx> GotocCtx<'tcx> {
     ) -> Expr {
         let res_t = self.codegen_ty(res_ty);
         let op_expr = self.codegen_operand(op);
-        let width = sz.try_eval_usize(self.tcx, ty::ParamEnv::reveal_all()).unwrap();
+        let width = sz.try_eval_target_usize(self.tcx, ty::ParamEnv::reveal_all()).unwrap();
         Expr::struct_expr(
             res_t,
             btree_string_map![("0", op_expr.array_constant(width))],
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
index 8508febbeb22..fb217e747371 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
@@ -777,7 +777,7 @@ impl<'tcx> GotocCtx<'tcx> {
             }
             ty::Foreign(defid) => self.codegen_foreign(ty, *defid),
             ty::Array(et, len) => {
-                let evaluated_len = len.try_eval_usize(self.tcx, self.param_env()).unwrap();
+                let evaluated_len = len.try_eval_target_usize(self.tcx, self.param_env()).unwrap();
                 let array_name = format!("[{}; {evaluated_len}]", self.ty_mangled_name(*et));
                 let array_pretty_name = format!("[{}; {evaluated_len}]", self.ty_pretty_name(*et));
                 // wrap arrays into struct so that one can take advantage of struct copy in C
@@ -902,7 +902,7 @@ impl<'tcx> GotocCtx<'tcx> {
     fn codegen_alignment_padding(
         &self,
         size: Size,
-        layout: &LayoutS<VariantIdx>,
+        layout: &LayoutS,
         idx: usize,
     ) -> Option<DatatypeComponent> {
         let align = Size::from_bits(layout.align.abi.bits());
@@ -927,7 +927,7 @@ impl<'tcx> GotocCtx<'tcx> {
     fn codegen_struct_fields(
         &mut self,
         flds: Vec<(String, Ty<'tcx>)>,
-        layout: &LayoutS<VariantIdx>,
+        layout: &LayoutS,
         initial_offset: Size,
     ) -> Vec<DatatypeComponent> {
         match &layout.fields {
@@ -1385,7 +1385,7 @@ impl<'tcx> GotocCtx<'tcx> {
         &mut self,
         variant: &VariantDef,
         subst: &'tcx InternalSubsts<'tcx>,
-        layout: &LayoutS<VariantIdx>,
+        layout: &LayoutS,
         initial_offset: Size,
     ) -> Vec<DatatypeComponent> {
         let flds: Vec<_> =
@@ -1554,7 +1554,7 @@ impl<'tcx> GotocCtx<'tcx> {
         ty: Ty<'tcx>,
         adtdef: &'tcx AdtDef,
         subst: &'tcx InternalSubsts<'tcx>,
-        variants: &IndexVec<VariantIdx, LayoutS<VariantIdx>>,
+        variants: &IndexVec<VariantIdx, LayoutS>,
     ) -> Type {
         let non_zst_count = variants.iter().filter(|layout| layout.size.bytes() > 0).count();
         let mangled_name = self.ty_mangled_name(ty);
@@ -1573,7 +1573,7 @@ impl<'tcx> GotocCtx<'tcx> {
 
     pub(crate) fn variant_min_offset(
         &self,
-        variants: &IndexVec<VariantIdx, LayoutS<VariantIdx>>,
+        variants: &IndexVec<VariantIdx, LayoutS>,
     ) -> Option<Size> {
         variants
             .iter()
@@ -1657,7 +1657,7 @@ impl<'tcx> GotocCtx<'tcx> {
         pretty_name: InternedString,
         def: &'tcx AdtDef,
         subst: &'tcx InternalSubsts<'tcx>,
-        layouts: &IndexVec<VariantIdx, LayoutS<VariantIdx>>,
+        layouts: &IndexVec<VariantIdx, LayoutS>,
         initial_offset: Size,
     ) -> Vec<DatatypeComponent> {
         def.variants()
@@ -1689,7 +1689,7 @@ impl<'tcx> GotocCtx<'tcx> {
         pretty_name: InternedString,
         case: &VariantDef,
         subst: &'tcx InternalSubsts<'tcx>,
-        variant: &LayoutS<VariantIdx>,
+        variant: &LayoutS,
         initial_offset: Size,
     ) -> Type {
         let case_name = format!("{name}::{}", case.name);
diff --git a/kani-compiler/src/session.rs b/kani-compiler/src/session.rs
index 9b83d55a8c34..99d7b7239d05 100644
--- a/kani-compiler/src/session.rs
+++ b/kani-compiler/src/session.rs
@@ -7,7 +7,7 @@ use crate::parser;
 use clap::ArgMatches;
 use rustc_errors::{
     emitter::Emitter, emitter::HumanReadableErrorType, fallback_fluent_bundle, json::JsonEmitter,
-    ColorConfig, Diagnostic,
+    ColorConfig, Diagnostic, TerminalUrl,
 };
 use std::panic;
 use std::str::FromStr;
@@ -57,6 +57,7 @@ static JSON_PANIC_HOOK: LazyLock<Box<dyn Fn(&panic::PanicInfo<'_>) + Sync + Send
                 None,
                 false,
                 false,
+                TerminalUrl::No,
             );
             let diagnostic = Diagnostic::new(rustc_errors::Level::Bug, msg);
             emitter.emit_diagnostic(&diagnostic);
diff --git a/rust-toolchain.toml b/rust-toolchain.toml
index 4747ffef5d2d..aeae6f8d56ca 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-02-05"
+channel = "nightly-2023-02-16"
 components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]