diff --git a/tests/expected/function-contract/interior-mutability/api/cell.expected b/tests/expected/function-contract/interior-mutability/api/cell.expected
new file mode 100644
index 000000000000..d9b0f5d51e5c
--- /dev/null
+++ b/tests/expected/function-contract/interior-mutability/api/cell.expected
@@ -0,0 +1,6 @@
+assertion\
+- Status: SUCCESS\
+- Description: "|_| im.x.get() < 101"\
+in function modify
+
+VERIFICATION:- SUCCESSFUL
diff --git a/tests/expected/function-contract/interior-mutability/api/cell.rs b/tests/expected/function-contract/interior-mutability/api/cell.rs
new file mode 100644
index 000000000000..671b6b206ef3
--- /dev/null
+++ b/tests/expected/function-contract/interior-mutability/api/cell.rs
@@ -0,0 +1,25 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+
+/// Mutating Cell via `as_ptr` in contracts
+use std::cell::Cell;
+
+/// This struct contains Cell which can be mutated
+struct InteriorMutability {
+    x: Cell<u32>,
+}
+
+#[kani::requires(im.x.get() < 100)]
+#[kani::modifies(im.x.as_ptr())]
+#[kani::ensures(|_| im.x.get() < 101)]
+///im is an immutable reference with interior mutability
+fn modify(im: &InteriorMutability) {
+    im.x.set(im.x.get() + 1)
+}
+
+#[kani::proof_for_contract(modify)]
+fn harness_for_modify() {
+    let im: InteriorMutability = InteriorMutability { x: Cell::new(kani::any()) };
+    modify(&im)
+}
diff --git a/tests/expected/function-contract/interior-mutability/api/cell_stub.expected b/tests/expected/function-contract/interior-mutability/api/cell_stub.expected
new file mode 100644
index 000000000000..b8da35411e53
--- /dev/null
+++ b/tests/expected/function-contract/interior-mutability/api/cell_stub.expected
@@ -0,0 +1,9 @@
+assertion\
+- Status: SUCCESS\
+- Description: "|_| old(im.x.get() + im.x.get()) == im.x.get()"\
+
+assertion\
+- Status: SUCCESS\
+- Description: "|_| old(im.x.get() + im.x.get() + im.x.get() + im.x.get()) == im.x.get()"\
+
+VERIFICATION:- SUCCESSFUL
diff --git a/tests/expected/function-contract/interior-mutability/api/cell_stub.rs b/tests/expected/function-contract/interior-mutability/api/cell_stub.rs
new file mode 100644
index 000000000000..d01ca379655f
--- /dev/null
+++ b/tests/expected/function-contract/interior-mutability/api/cell_stub.rs
@@ -0,0 +1,40 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+
+/// The objective of this test is to show that the contracts for double can be replaced as a stub within the contracts for quadruple.
+/// This shows that we can generate `kani::any()` for Cell.
+use std::cell::Cell;
+
+/// This struct contains Cell which can be mutated
+struct InteriorMutability {
+    x: Cell<u32>,
+}
+
+#[kani::ensures(|_| old(im.x.get() + im.x.get()) == im.x.get())]
+#[kani::requires(im.x.get() < 100)]
+#[kani::modifies(im.x.as_ptr())]
+fn double(im: &InteriorMutability) {
+    im.x.set(im.x.get() + im.x.get())
+}
+
+#[kani::proof_for_contract(double)]
+fn double_harness() {
+    let im: InteriorMutability = InteriorMutability { x: Cell::new(kani::any()) };
+    double(&im);
+}
+
+#[kani::ensures(|_| old(im.x.get() + im.x.get() + im.x.get() + im.x.get()) == im.x.get())]
+#[kani::requires(im.x.get() < 50)]
+#[kani::modifies(im.x.as_ptr())]
+fn quadruple(im: &InteriorMutability) {
+    double(im);
+    double(im)
+}
+
+#[kani::proof_for_contract(quadruple)]
+#[kani::stub_verified(double)]
+fn quadruple_harness() {
+    let im: InteriorMutability = InteriorMutability { x: Cell::new(kani::any()) };
+    quadruple(&im);
+}
diff --git a/tests/expected/function-contract/interior-mutability/api/unsafecell.expected b/tests/expected/function-contract/interior-mutability/api/unsafecell.expected
new file mode 100644
index 000000000000..1646a8a78e7f
--- /dev/null
+++ b/tests/expected/function-contract/interior-mutability/api/unsafecell.expected
@@ -0,0 +1,6 @@
+assertion\
+- Status: SUCCESS\
+- Description: "|_| unsafe{ *im.x.get() } < 101"\
+in function modify
+
+VERIFICATION:- SUCCESSFUL
diff --git a/tests/expected/function-contract/interior-mutability/api/unsafecell.rs b/tests/expected/function-contract/interior-mutability/api/unsafecell.rs
new file mode 100644
index 000000000000..8125e3e3c077
--- /dev/null
+++ b/tests/expected/function-contract/interior-mutability/api/unsafecell.rs
@@ -0,0 +1,24 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+
+use std::cell::UnsafeCell;
+
+/// This struct contains UnsafeCell which can be mutated
+struct InteriorMutability {
+    x: UnsafeCell<u32>,
+}
+
+#[kani::requires(unsafe{*im.x.get()} < 100)]
+#[kani::modifies(im.x.get())]
+#[kani::ensures(|_| unsafe{*im.x.get()} < 101)]
+/// `im` is an immutable reference with interior mutability
+fn modify(im: &InteriorMutability) {
+    unsafe { *im.x.get() += 1 }
+}
+
+#[kani::proof_for_contract(modify)]
+fn harness_for_modify() {
+    let im: InteriorMutability = InteriorMutability { x: UnsafeCell::new(kani::any()) };
+    modify(&im)
+}
diff --git a/tests/expected/function-contract/interior-mutability/whole-struct/cell.expected b/tests/expected/function-contract/interior-mutability/whole-struct/cell.expected
new file mode 100644
index 000000000000..d9b0f5d51e5c
--- /dev/null
+++ b/tests/expected/function-contract/interior-mutability/whole-struct/cell.expected
@@ -0,0 +1,6 @@
+assertion\
+- Status: SUCCESS\
+- Description: "|_| im.x.get() < 101"\
+in function modify
+
+VERIFICATION:- SUCCESSFUL
diff --git a/tests/expected/function-contract/interior-mutability/whole-struct/cell.rs b/tests/expected/function-contract/interior-mutability/whole-struct/cell.rs
new file mode 100644
index 000000000000..9f42f6fa1f6c
--- /dev/null
+++ b/tests/expected/function-contract/interior-mutability/whole-struct/cell.rs
@@ -0,0 +1,25 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+
+/// The objective of this test is to check the modification of a Cell used as interior mutability in an immutable struct
+use std::cell::Cell;
+
+/// This struct contains Cell which can be mutated
+struct InteriorMutability {
+    x: Cell<u32>,
+}
+
+#[kani::requires(im.x.get() < 100)]
+#[kani::modifies(&im.x)]
+#[kani::ensures(|_| im.x.get() < 101)]
+/// `im` is an immutable reference with interior mutability
+fn modify(im: &InteriorMutability) {
+    im.x.set(im.x.get() + 1)
+}
+
+#[kani::proof_for_contract(modify)]
+fn harness_for_modify() {
+    let im: InteriorMutability = InteriorMutability { x: Cell::new(kani::any()) };
+    modify(&im)
+}
diff --git a/tests/expected/function-contract/interior-mutability/whole-struct/oncecell.expected b/tests/expected/function-contract/interior-mutability/whole-struct/oncecell.expected
new file mode 100644
index 000000000000..a367bcd9fb95
--- /dev/null
+++ b/tests/expected/function-contract/interior-mutability/whole-struct/oncecell.expected
@@ -0,0 +1,6 @@
+assertion\
+- Status: SUCCESS\
+- Description: "|_| im.x.get().is_some()"\
+in function modify
+
+VERIFICATION:- SUCCESSFUL
diff --git a/tests/expected/function-contract/interior-mutability/whole-struct/oncecell.rs b/tests/expected/function-contract/interior-mutability/whole-struct/oncecell.rs
new file mode 100644
index 000000000000..6ca32251b60c
--- /dev/null
+++ b/tests/expected/function-contract/interior-mutability/whole-struct/oncecell.rs
@@ -0,0 +1,24 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+
+/// The objective of this test is to check the modification of an OnceCell used as interior mutability in an immutable struct
+use std::cell::OnceCell;
+
+/// This struct contains OnceCell which can be mutated
+struct InteriorMutability {
+    x: OnceCell<u32>,
+}
+
+#[kani::requires(im.x.get().is_none())]
+#[kani::modifies(&im.x)]
+#[kani::ensures(|_| im.x.get().is_some())]
+fn modify(im: &InteriorMutability) {
+    im.x.set(5).expect("")
+}
+
+#[kani::proof_for_contract(modify)]
+fn harness_for_modify() {
+    let im: InteriorMutability = InteriorMutability { x: OnceCell::new() };
+    modify(&im)
+}
diff --git a/tests/expected/function-contract/interior-mutability/whole-struct/refcell.expected b/tests/expected/function-contract/interior-mutability/whole-struct/refcell.expected
new file mode 100644
index 000000000000..225c290a171e
--- /dev/null
+++ b/tests/expected/function-contract/interior-mutability/whole-struct/refcell.expected
@@ -0,0 +1,6 @@
+assertion\
+- Status: SUCCESS\
+- Description: "|_| unsafe{ *im.x.as_ptr() } < 101"\
+in function modify
+
+VERIFICATION:- SUCCESSFUL
diff --git a/tests/expected/function-contract/interior-mutability/whole-struct/refcell.rs b/tests/expected/function-contract/interior-mutability/whole-struct/refcell.rs
new file mode 100644
index 000000000000..1cce5e2364c3
--- /dev/null
+++ b/tests/expected/function-contract/interior-mutability/whole-struct/refcell.rs
@@ -0,0 +1,25 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+
+/// The objective of this test is to check the modification of a RefCell used as interior mutability in an immutable struct
+use std::cell::RefCell;
+
+/// This struct contains Cell which can be mutated
+struct InteriorMutability {
+    x: RefCell<u32>,
+}
+
+#[kani::requires(unsafe{*im.x.as_ptr()} < 100)]
+#[kani::modifies(&im.x)]
+#[kani::ensures(|_| unsafe{*im.x.as_ptr()} < 101)]
+/// `im` is an immutable reference with interior mutability
+fn modify(im: &InteriorMutability) {
+    im.x.replace_with(|&mut old| old + 1);
+}
+
+#[kani::proof_for_contract(modify)]
+fn harness_for_modify() {
+    let im: InteriorMutability = InteriorMutability { x: RefCell::new(kani::any()) };
+    modify(&im)
+}
diff --git a/tests/expected/function-contract/interior-mutability/whole-struct/unsafecell.expected b/tests/expected/function-contract/interior-mutability/whole-struct/unsafecell.expected
new file mode 100644
index 000000000000..1646a8a78e7f
--- /dev/null
+++ b/tests/expected/function-contract/interior-mutability/whole-struct/unsafecell.expected
@@ -0,0 +1,6 @@
+assertion\
+- Status: SUCCESS\
+- Description: "|_| unsafe{ *im.x.get() } < 101"\
+in function modify
+
+VERIFICATION:- SUCCESSFUL
diff --git a/tests/expected/function-contract/interior-mutability/whole-struct/unsafecell.rs b/tests/expected/function-contract/interior-mutability/whole-struct/unsafecell.rs
new file mode 100644
index 000000000000..6adb7b12c8b1
--- /dev/null
+++ b/tests/expected/function-contract/interior-mutability/whole-struct/unsafecell.rs
@@ -0,0 +1,25 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+
+/// The objective of this test is to check the modification of an UnsafeCell used as interior mutability in an immutable struct
+use std::cell::UnsafeCell;
+
+/// This struct contains UnsafeCell which can be mutated
+struct InteriorMutability {
+    x: UnsafeCell<u32>,
+}
+
+#[kani::requires(unsafe{*im.x.get()} < 100)]
+#[kani::modifies(im.x.get())]
+#[kani::ensures(|_| unsafe{*im.x.get()} < 101)]
+/// `im` is an immutable reference with interior mutability
+fn modify(im: &InteriorMutability) {
+    unsafe { *im.x.get() += 1 }
+}
+
+#[kani::proof_for_contract(modify)]
+fn harness_for_modify() {
+    let im: InteriorMutability = InteriorMutability { x: UnsafeCell::new(kani::any()) };
+    modify(&im)
+}