diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
index 554ba6a03a61..7eef6b877523 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
@@ -504,7 +504,10 @@ impl<'tcx> GotocCtx<'tcx> {
             "nearbyintf32" => codegen_simple_intrinsic!(Nearbyintf),
             "nearbyintf64" => codegen_simple_intrinsic!(Nearbyint),
             "needs_drop" => codegen_intrinsic_const!(),
-            "offset" => self.codegen_offset(intrinsic, instance, fargs, p, loc),
+            // As of https://github.com/rust-lang/rust/pull/110822 the `offset` intrinsic is lowered to `mir::BinOp::Offset`
+            "offset" => unreachable!(
+                "Expected `core::intrinsics::unreachable` to be handled by `BinOp::OffSet`"
+            ),
             "powf32" => unstable_codegen!(codegen_simple_intrinsic!(Powf)),
             "powf64" => unstable_codegen!(codegen_simple_intrinsic!(Pow)),
             "powif32" => unstable_codegen!(codegen_simple_intrinsic!(Powif)),
@@ -1729,7 +1732,7 @@ impl<'tcx> GotocCtx<'tcx> {
     /// Returns a tuple with:
     ///  * The result expression of the computation.
     ///  * An assertion statement to ensure the operation has not overflowed.
-    fn count_in_bytes(
+    pub fn count_in_bytes(
         &mut self,
         count: Expr,
         ty: Ty<'tcx>,
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
index 6fc139b9d5f2..9e2ece638f29 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
@@ -18,7 +18,7 @@ use cbmc::MachineModel;
 use cbmc::{btree_string_map, InternString, InternedString};
 use num::bigint::BigInt;
 use rustc_abi::FieldIdx;
-use rustc_index::vec::IndexVec;
+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::layout::LayoutOf;
@@ -294,6 +294,7 @@ impl<'tcx> GotocCtx<'tcx> {
 
     fn codegen_rvalue_binary_op(
         &mut self,
+        ty: Ty<'tcx>,
         op: &BinOp,
         e1: &Operand<'tcx>,
         e2: &Operand<'tcx>,
@@ -317,7 +318,32 @@ impl<'tcx> GotocCtx<'tcx> {
             BinOp::Offset => {
                 let ce1 = self.codegen_operand(e1);
                 let ce2 = self.codegen_operand(e2);
-                ce1.plus(ce2)
+
+                // Check that computing `offset` in bytes would not overflow
+                let (offset_bytes, bytes_overflow_check) = self.count_in_bytes(
+                    ce2.clone().cast_to(Type::ssize_t()),
+                    ty,
+                    Type::ssize_t(),
+                    "offset",
+                    loc,
+                );
+
+                // Check that the computation would not overflow an `isize` which is UB:
+                // https://doc.rust-lang.org/std/primitive.pointer.html#method.offset
+                // These checks may allow a wrapping-around behavior in CBMC:
+                // https://github.com/model-checking/kani/issues/1150
+                let overflow_res = ce1.clone().cast_to(Type::ssize_t()).add_overflow(offset_bytes);
+                let overflow_check = self.codegen_assert_assume(
+                    overflow_res.overflowed.not(),
+                    PropertyClass::ArithmeticOverflow,
+                    "attempt to compute offset which would overflow",
+                    loc,
+                );
+                let res = ce1.clone().plus(ce2);
+                Expr::statement_expression(
+                    vec![bytes_overflow_check, overflow_check, res.as_stmt(loc)],
+                    ce1.typ().clone(),
+                )
             }
         }
     }
@@ -548,7 +574,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 self.codegen_operand(operand).transmute_to(goto_typ, &self.symbol_table)
             }
             Rvalue::BinaryOp(op, box (ref e1, ref e2)) => {
-                self.codegen_rvalue_binary_op(op, e1, e2, loc)
+                self.codegen_rvalue_binary_op(res_ty, op, e1, e2, loc)
             }
             Rvalue::CheckedBinaryOp(op, box (ref e1, ref e2)) => {
                 self.codegen_rvalue_checked_binary_op(op, e1, e2, res_ty)
@@ -560,6 +586,10 @@ impl<'tcx> GotocCtx<'tcx> {
                     NullOp::SizeOf => Expr::int_constant(layout.size.bytes_usize(), Type::size_t())
                         .with_size_of_annotation(self.codegen_ty(t)),
                     NullOp::AlignOf => Expr::int_constant(layout.align.abi.bytes(), Type::size_t()),
+                    NullOp::OffsetOf(fields) => Expr::int_constant(
+                        layout.offset_of_subfield(self, fields.iter().map(|f| f.index())).bytes(),
+                        Type::size_t(),
+                    ),
                 }
             }
             Rvalue::ShallowInitBox(ref operand, content_ty) => {
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
index 8459c2581381..2816732f1c4d 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
@@ -7,7 +7,7 @@ use cbmc::utils::aggr_tag;
 use cbmc::{InternString, InternedString};
 use rustc_ast::ast::Mutability;
 use rustc_hir::{LangItem, Unsafety};
-use rustc_index::vec::IndexVec;
+use rustc_index::IndexVec;
 use rustc_middle::mir::{HasLocalDecls, Local, Operand, Place, Rvalue};
 use rustc_middle::ty::layout::LayoutOf;
 use rustc_middle::ty::print::with_no_trimmed_paths;
@@ -666,7 +666,7 @@ impl<'tcx> GotocCtx<'tcx> {
             }
             _ => {
                 // This hash is documented to be the same no matter the crate context
-                let id_u64 = self.tcx.type_id_hash(t);
+                let id_u64 = self.tcx.type_id_hash(t).as_u64();
                 format!("_{id_u64}").intern()
             }
         }
diff --git a/kani-compiler/src/kani_middle/metadata.rs b/kani-compiler/src/kani_middle/metadata.rs
index e293c95e2cd8..03e163699d2e 100644
--- a/kani-compiler/src/kani_middle/metadata.rs
+++ b/kani-compiler/src/kani_middle/metadata.rs
@@ -8,7 +8,7 @@ use std::path::Path;
 use crate::kani_middle::attributes::test_harness_name;
 use kani_metadata::{ArtifactType, HarnessAttributes, HarnessMetadata};
 use rustc_hir::def_id::DefId;
-use rustc_middle::ty::{Instance, InstanceDef, TyCtxt, WithOptConstParam};
+use rustc_middle::ty::{Instance, InstanceDef, TyCtxt};
 
 use super::{attributes::extract_harness_attributes, SourceLocation};
 
@@ -24,7 +24,7 @@ pub fn gen_proof_metadata(tcx: TyCtxt, def_id: DefId, base_name: &Path) -> Harne
         tcx.symbol_name(Instance::mono(tcx, def_id)).to_string()
     };
 
-    let body = tcx.instance_mir(InstanceDef::Item(WithOptConstParam::unknown(def_id)));
+    let body = tcx.instance_mir(InstanceDef::Item(def_id));
     let loc = SourceLocation::new(tcx, &body.span);
     let file_stem = format!("{}_{mangled_name}", base_name.file_stem().unwrap().to_str().unwrap());
     let model_file = base_name.with_file_name(file_stem).with_extension(ArtifactType::SymTabGoto);
@@ -52,7 +52,7 @@ pub fn gen_test_metadata<'tcx>(
 ) -> HarnessMetadata {
     let pretty_name = test_harness_name(tcx, test_desc);
     let mangled_name = tcx.symbol_name(test_fn).to_string();
-    let body = tcx.instance_mir(InstanceDef::Item(WithOptConstParam::unknown(test_desc)));
+    let body = tcx.instance_mir(InstanceDef::Item(test_desc));
     let loc = SourceLocation::new(tcx, &body.span);
     let file_stem = format!("{}_{mangled_name}", base_name.file_stem().unwrap().to_str().unwrap());
     let model_file = base_name.with_file_name(file_stem).with_extension(ArtifactType::SymTabGoto);
diff --git a/kani-compiler/src/kani_middle/reachability.rs b/kani-compiler/src/kani_middle/reachability.rs
index c35fdfe18df5..4d32a09f7d28 100644
--- a/kani-compiler/src/kani_middle/reachability.rs
+++ b/kani-compiler/src/kani_middle/reachability.rs
@@ -31,7 +31,7 @@ use rustc_middle::span_bug;
 use rustc_middle::ty::adjustment::PointerCast;
 use rustc_middle::ty::{
     Closure, ClosureKind, ConstKind, Instance, InstanceDef, ParamEnv, Ty, TyCtxt, TyKind,
-    TypeFoldable, VtblEntry, WithOptConstParam,
+    TypeFoldable, VtblEntry,
 };
 
 use crate::kani_middle::coercion;
@@ -111,7 +111,7 @@ where
         let def_kind = tcx.def_kind(def_id);
         if matches!(def_kind, DefKind::Const) && predicate(tcx, def_id) {
             let instance = Instance::mono(tcx, def_id);
-            let body = tcx.instance_mir(InstanceDef::Item(WithOptConstParam::unknown(def_id)));
+            let body = tcx.instance_mir(InstanceDef::Item(def_id));
             let mut collector =
                 MonoItemsFnCollector { tcx, body, instance, collected: FxHashSet::default() };
             collector.visit_body(body);
diff --git a/kani-compiler/src/kani_middle/stubbing/transform.rs b/kani-compiler/src/kani_middle/stubbing/transform.rs
index a609e5e9b0b6..49111c749b25 100644
--- a/kani-compiler/src/kani_middle/stubbing/transform.rs
+++ b/kani-compiler/src/kani_middle/stubbing/transform.rs
@@ -118,8 +118,10 @@ pub fn mk_rustc_arg(stub_mapping: &FxHashMap<DefPathHash, DefPathHash>) -> Strin
     // as an association list.
     let mut pairs = Vec::new();
     for (k, v) in stub_mapping {
-        let kparts = k.0.as_value();
-        let vparts = v.0.as_value();
+        let (k_a, k_b) = k.0.split();
+        let kparts = (k_a.as_u64(), k_b.as_u64());
+        let (v_a, v_b) = v.0.split();
+        let vparts = (v_a.as_u64(), v_b.as_u64());
         pairs.push((kparts, vparts));
     }
     // Store our serialized mapping as a fake LLVM argument (safe to do since
diff --git a/kani-driver/src/cbmc_property_renderer.rs b/kani-driver/src/cbmc_property_renderer.rs
index d50672ec4208..8da67dae7ab1 100644
--- a/kani-driver/src/cbmc_property_renderer.rs
+++ b/kani-driver/src/cbmc_property_renderer.rs
@@ -535,7 +535,7 @@ fn has_unwinding_assertion_failures(properties: &Vec<Property>) -> bool {
 /// definition.
 fn modify_undefined_function_checks(mut properties: Vec<Property>) -> (Vec<Property>, bool) {
     let mut has_unknown_location_checks = false;
-    for mut prop in &mut properties {
+    for prop in &mut properties {
         if let Some(function) = &prop.source_location.function
             && prop.description == DEFAULT_ASSERTION
             && prop.source_location.file.is_none()
diff --git a/rust-toolchain.toml b/rust-toolchain.toml
index 968c1e04951e..d0ad632b38ef 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-04-16"
+channel = "nightly-2023-04-29"
 components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]
diff --git a/tests/expected/offset-from-bytes-overflow/main.rs b/tests/expected/offset-from-bytes-overflow/main.rs
index 37b05090161a..32ffb433036c 100644
--- a/tests/expected/offset-from-bytes-overflow/main.rs
+++ b/tests/expected/offset-from-bytes-overflow/main.rs
@@ -9,7 +9,7 @@ use std::convert::TryInto;
 fn main() {
     let v: &[u128] = &[0; 10];
     let v_0: *const u128 = &v[0];
-    let high_offset = usize::MAX / (std::mem::size_of::<u128>() * 2);
+    let high_offset = usize::MAX / (std::mem::size_of::<u128>());
     unsafe {
         let v_wrap: *const u128 = v_0.add(high_offset.try_into().unwrap());
         let _ = v_wrap.offset_from(v_0);
diff --git a/tests/expected/offset-i32-fail/main.rs b/tests/expected/offset-i32-fail/main.rs
index cb50eca3387e..b41fb9442584 100644
--- a/tests/expected/offset-i32-fail/main.rs
+++ b/tests/expected/offset-i32-fail/main.rs
@@ -12,6 +12,6 @@ fn test_offset() {
     let ptr: *const i32 = arr.as_ptr();
 
     unsafe {
-        let x = *offset(ptr, 3);
+        let x = *offset(ptr, 3isize);
     }
 }
diff --git a/tests/expected/offset-overflow/main.rs b/tests/expected/offset-overflow/main.rs
index 2f99eeba2668..55b79df854cc 100644
--- a/tests/expected/offset-overflow/main.rs
+++ b/tests/expected/offset-overflow/main.rs
@@ -12,6 +12,6 @@ fn test_offset_overflow() {
     let ptr: *const u8 = s.as_ptr();
 
     unsafe {
-        let _ = offset(ptr, isize::MAX);
+        let _d = offset(ptr, isize::MAX / 8);
     }
 }
diff --git a/tests/expected/offset-u8-fail/main.rs b/tests/expected/offset-u8-fail/main.rs
index 825497adb903..031095c7386b 100644
--- a/tests/expected/offset-u8-fail/main.rs
+++ b/tests/expected/offset-u8-fail/main.rs
@@ -12,6 +12,6 @@ fn test_offset() {
     let ptr: *const u8 = s.as_ptr();
 
     unsafe {
-        let x = *offset(ptr, 3) as char;
+        let x = *offset(ptr, 3isize) as char;
     }
 }
diff --git a/tests/kani/Intrinsics/Offset/offset_i32_ok.rs b/tests/kani/Intrinsics/Offset/offset_i32_ok.rs
index ef3e00a623f6..da7449b1fa28 100644
--- a/tests/kani/Intrinsics/Offset/offset_i32_ok.rs
+++ b/tests/kani/Intrinsics/Offset/offset_i32_ok.rs
@@ -11,10 +11,10 @@ fn test_offset() {
     let ptr: *const i32 = arr.as_ptr();
 
     unsafe {
-        assert_eq!(*offset(ptr, 0), 1);
-        assert_eq!(*offset(ptr, 1), 2);
-        assert_eq!(*offset(ptr, 2), 3);
-        assert_eq!(*offset(ptr, 2).sub(1), 2);
+        assert_eq!(*offset(ptr, 0isize), 1);
+        assert_eq!(*offset(ptr, 1isize), 2);
+        assert_eq!(*offset(ptr, 2isize), 3);
+        assert_eq!(*offset(ptr, 2isize).sub(1), 2);
 
         // This wouldn't be okay because it's
         // more than one byte past the object
@@ -24,8 +24,8 @@ fn test_offset() {
         // that goes 1 element behind the original one
         let other_ptr: *const i32 = ptr.add(1);
 
-        assert_eq!(*offset(other_ptr, 0), 2);
-        assert_eq!(*offset(other_ptr, 1), 3);
-        assert_eq!(*offset(other_ptr, 1).sub(1), 2);
+        assert_eq!(*offset(other_ptr, 0isize), 2);
+        assert_eq!(*offset(other_ptr, 1isize), 3);
+        assert_eq!(*offset(other_ptr, 1isize).sub(1), 2);
     }
 }
diff --git a/tests/kani/Intrinsics/Offset/offset_u8_ok.rs b/tests/kani/Intrinsics/Offset/offset_u8_ok.rs
index ab3f2dc31535..6df94ae44494 100644
--- a/tests/kani/Intrinsics/Offset/offset_u8_ok.rs
+++ b/tests/kani/Intrinsics/Offset/offset_u8_ok.rs
@@ -11,21 +11,21 @@ fn test_offset() {
     let ptr: *const u8 = s.as_ptr();
 
     unsafe {
-        assert_eq!(*offset(ptr, 0) as char, '1');
-        assert_eq!(*offset(ptr, 1) as char, '2');
-        assert_eq!(*offset(ptr, 2) as char, '3');
-        assert_eq!(*offset(ptr, 2).sub(1) as char, '2');
+        assert_eq!(*offset(ptr, 0isize) as char, '1');
+        assert_eq!(*offset(ptr, 1isize) as char, '2');
+        assert_eq!(*offset(ptr, 2isize) as char, '3');
+        assert_eq!(*offset(ptr, 2isize).sub(1) as char, '2');
 
         // This is okay because it's one byte past the object,
         // but dereferencing it is UB
-        let _x = offset(ptr, 3);
+        let _x = offset(ptr, 3isize);
 
         // Check that the results are the same with a pointer
         // that goes 1 element behind the original one
         let other_ptr: *const u8 = ptr.add(1);
 
-        assert_eq!(*offset(other_ptr, 0) as char, '2');
-        assert_eq!(*offset(other_ptr, 1) as char, '3');
-        assert_eq!(*offset(other_ptr, 1).sub(1) as char, '2');
+        assert_eq!(*offset(other_ptr, 0isize) as char, '2');
+        assert_eq!(*offset(other_ptr, 1isize) as char, '3');
+        assert_eq!(*offset(other_ptr, 1isize).sub(1) as char, '2');
     }
 }
diff --git a/tests/script-based-pre/check-output/singlefile.rs b/tests/script-based-pre/check-output/singlefile.rs
index 3c47e1e8c522..5581ab1fdb8b 100644
--- a/tests/script-based-pre/check-output/singlefile.rs
+++ b/tests/script-based-pre/check-output/singlefile.rs
@@ -11,6 +11,7 @@ pub fn main() {
     monomorphize::<usize>();
     let x = [true; 2];
     let ref_to_str = &"";
+    assert!(ref_to_str.is_empty());
     let test_enum = TestEnum::Variant1(true);
 }