From dcc9d61d6e5213475fc092c723c12b9a14b6d0d9 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Fri, 21 Jun 2024 13:07:01 +0000
Subject: [PATCH] fixup! Codegen storage markers as assignments to
 __CPROVER_dead_object

---
 tests/expected/shadow/unsupported_num_objects/test.rs | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/tests/expected/shadow/unsupported_num_objects/test.rs b/tests/expected/shadow/unsupported_num_objects/test.rs
index f60d0020e989..4b0690686b23 100644
--- a/tests/expected/shadow/unsupported_num_objects/test.rs
+++ b/tests/expected/shadow/unsupported_num_objects/test.rs
@@ -15,14 +15,14 @@ fn check_max_objects<const N: usize>() {
     // - the NULL pointer whose object ID is 0, and
     // - the object ID for `i`
     while i < N {
-        let x = i;
-        assert_eq!(kani::mem::pointer_object(&x as *const usize), i + 2);
+        let x : Box<usize> = Box::new(i);
+        assert_eq!(kani::mem::pointer_object(&*x as *const usize), 2 * i + 2);
         i += 1;
     }
 
     // create a new object whose ID is `N` + 2
     let x = 42;
-    assert_eq!(kani::mem::pointer_object(&x as *const i32), N + 2);
+    assert_eq!(kani::mem::pointer_object(&x as *const i32), 2 * N + 2);
     // the following call to `set` would fail if the object ID for `x` exceeds
     // the maximum allowed by Kani's shadow memory model
     unsafe {
@@ -32,10 +32,10 @@ fn check_max_objects<const N: usize>() {
 
 #[kani::proof]
 fn check_max_objects_pass() {
-    check_max_objects::<1021>();
+    check_max_objects::<510>();
 }
 
 #[kani::proof]
 fn check_max_objects_fail() {
-    check_max_objects::<1022>();
+    check_max_objects::<511>();
 }