diff --git a/kani-driver/src/call_single_file.rs b/kani-driver/src/call_single_file.rs
index 7cbe150427e9..411dabb5270e 100644
--- a/kani-driver/src/call_single_file.rs
+++ b/kani-driver/src/call_single_file.rs
@@ -140,7 +140,10 @@ impl KaniSession {
         }
 
         if self.args.common_args.unstable_features.contains(UnstableFeature::UninitChecks) {
-            flags.push("--ub-check=uninit".into())
+            // Automatically enable shadow memory, since the version of uninitialized memory checks
+            // without non-determinism depends on it.
+            flags.push("-Z ghost-state".into());
+            flags.push("--ub-check=uninit".into());
         }
 
         if self.args.ignore_locals_lifetime {
diff --git a/tests/expected/uninit/access-padding-uninit/access-padding-uninit.rs b/tests/expected/uninit/access-padding-uninit/access-padding-uninit.rs
index d6e735e219ad..8e65b95aefa2 100644
--- a/tests/expected/uninit/access-padding-uninit/access-padding-uninit.rs
+++ b/tests/expected/uninit/access-padding-uninit/access-padding-uninit.rs
@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: -Z ghost-state -Z uninit-checks
+// kani-flags: -Z uninit-checks
 
 use std::ptr::addr_of;
 
diff --git a/tests/expected/uninit/access-padding-via-cast/access-padding-via-cast.rs b/tests/expected/uninit/access-padding-via-cast/access-padding-via-cast.rs
index b73bebc827bc..1604625fc54c 100644
--- a/tests/expected/uninit/access-padding-via-cast/access-padding-via-cast.rs
+++ b/tests/expected/uninit/access-padding-via-cast/access-padding-via-cast.rs
@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: -Z ghost-state -Z uninit-checks
+// kani-flags: -Z uninit-checks
 
 use std::ptr;
 #[repr(C)]
diff --git a/tests/expected/uninit/alloc-to-slice/alloc-to-slice.rs b/tests/expected/uninit/alloc-to-slice/alloc-to-slice.rs
index 01bf17ca4e67..318f234c31be 100644
--- a/tests/expected/uninit/alloc-to-slice/alloc-to-slice.rs
+++ b/tests/expected/uninit/alloc-to-slice/alloc-to-slice.rs
@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: -Z ghost-state -Z uninit-checks
+// kani-flags: -Z uninit-checks
 
 use std::alloc::{alloc, Layout};
 use std::slice::from_raw_parts;
diff --git a/tests/expected/uninit/atomic/atomic.rs b/tests/expected/uninit/atomic/atomic.rs
index b3a632ddc67e..63c85af41a3f 100644
--- a/tests/expected/uninit/atomic/atomic.rs
+++ b/tests/expected/uninit/atomic/atomic.rs
@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: -Z ghost-state -Z uninit-checks
+// kani-flags: -Z uninit-checks
 
 #![feature(core_intrinsics)]
 
diff --git a/tests/expected/uninit/intrinsics/intrinsics.rs b/tests/expected/uninit/intrinsics/intrinsics.rs
index c5e0181b27b9..aa8a89b7b959 100644
--- a/tests/expected/uninit/intrinsics/intrinsics.rs
+++ b/tests/expected/uninit/intrinsics/intrinsics.rs
@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: -Z ghost-state -Z uninit-checks
+// kani-flags: -Z uninit-checks
 //! Checks that Kani supports memory initialization checks via intrinsics.
 
 #![feature(core_intrinsics)]
diff --git a/tests/expected/uninit/vec-read-bad-len/vec-read-bad-len.rs b/tests/expected/uninit/vec-read-bad-len/vec-read-bad-len.rs
index 9778bb11a277..f5cae82c5350 100644
--- a/tests/expected/uninit/vec-read-bad-len/vec-read-bad-len.rs
+++ b/tests/expected/uninit/vec-read-bad-len/vec-read-bad-len.rs
@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: -Z ghost-state -Z uninit-checks
+// kani-flags: -Z uninit-checks
 
 use std::ops::Index;
 
diff --git a/tests/expected/uninit/vec-read-semi-init/vec-read-semi-init.rs b/tests/expected/uninit/vec-read-semi-init/vec-read-semi-init.rs
index 4330f5f53023..2e007cabaced 100644
--- a/tests/expected/uninit/vec-read-semi-init/vec-read-semi-init.rs
+++ b/tests/expected/uninit/vec-read-semi-init/vec-read-semi-init.rs
@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: -Z ghost-state -Z uninit-checks
+// kani-flags: -Z uninit-checks
 
 /// Checks that Kani catches an attempt to read uninitialized memory from a semi-initialized vector.
 #[kani::proof]
diff --git a/tests/expected/uninit/vec-read-uninit/vec-read-uninit.rs b/tests/expected/uninit/vec-read-uninit/vec-read-uninit.rs
index c322b4d33bb2..e6daf80cd5e3 100644
--- a/tests/expected/uninit/vec-read-uninit/vec-read-uninit.rs
+++ b/tests/expected/uninit/vec-read-uninit/vec-read-uninit.rs
@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: -Z ghost-state -Z uninit-checks
+// kani-flags: -Z uninit-checks
 
 /// Checks that Kani catches an attempt to read uninitialized memory from an uninitialized vector.
 #[kani::proof]
diff --git a/tests/kani/Uninit/access-padding-enum-diverging-variants.rs b/tests/kani/Uninit/access-padding-enum-diverging-variants.rs
index 7feb493a5b3f..fae491c40622 100644
--- a/tests/kani/Uninit/access-padding-enum-diverging-variants.rs
+++ b/tests/kani/Uninit/access-padding-enum-diverging-variants.rs
@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: -Z ghost-state -Z uninit-checks
+// kani-flags: -Z uninit-checks
 
 use std::ptr;
 use std::ptr::addr_of;
diff --git a/tests/kani/Uninit/access-padding-enum-multiple-variants.rs b/tests/kani/Uninit/access-padding-enum-multiple-variants.rs
index fb8fae06ca59..dd6942252cb2 100644
--- a/tests/kani/Uninit/access-padding-enum-multiple-variants.rs
+++ b/tests/kani/Uninit/access-padding-enum-multiple-variants.rs
@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: -Z ghost-state -Z uninit-checks
+// kani-flags: -Z uninit-checks
 
 use std::ptr;
 use std::ptr::addr_of;
diff --git a/tests/kani/Uninit/access-padding-enum-single-field.rs b/tests/kani/Uninit/access-padding-enum-single-field.rs
index c283b603f705..63f7f6043905 100644
--- a/tests/kani/Uninit/access-padding-enum-single-field.rs
+++ b/tests/kani/Uninit/access-padding-enum-single-field.rs
@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: -Z ghost-state -Z uninit-checks
+// kani-flags: -Z uninit-checks
 
 use std::ptr;
 use std::ptr::addr_of;
diff --git a/tests/kani/Uninit/access-padding-enum-single-variant.rs b/tests/kani/Uninit/access-padding-enum-single-variant.rs
index f33cfe7ce6fb..bb87d36d26c8 100644
--- a/tests/kani/Uninit/access-padding-enum-single-variant.rs
+++ b/tests/kani/Uninit/access-padding-enum-single-variant.rs
@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: -Z ghost-state -Z uninit-checks
+// kani-flags: -Z uninit-checks
 
 use std::ptr;
 use std::ptr::addr_of;
diff --git a/tests/kani/Uninit/access-padding-init.rs b/tests/kani/Uninit/access-padding-init.rs
index d98af78ea91c..7523622a6106 100644
--- a/tests/kani/Uninit/access-padding-init.rs
+++ b/tests/kani/Uninit/access-padding-init.rs
@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: -Z ghost-state -Z uninit-checks
+// kani-flags: -Z uninit-checks
 
 use std::ptr::addr_of;
 
diff --git a/tests/kani/Uninit/alloc-to-slice.rs b/tests/kani/Uninit/alloc-to-slice.rs
index 195ebf9488fd..863d3b40b390 100644
--- a/tests/kani/Uninit/alloc-to-slice.rs
+++ b/tests/kani/Uninit/alloc-to-slice.rs
@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: -Z ghost-state -Z uninit-checks
+// kani-flags: -Z uninit-checks
 
 use std::alloc::{alloc, Layout};
 
diff --git a/tests/kani/Uninit/alloc-zeroed-to-slice.rs b/tests/kani/Uninit/alloc-zeroed-to-slice.rs
index f4eaad598716..d00ca4c6abff 100644
--- a/tests/kani/Uninit/alloc-zeroed-to-slice.rs
+++ b/tests/kani/Uninit/alloc-zeroed-to-slice.rs
@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: -Z ghost-state -Z uninit-checks
+// kani-flags: -Z uninit-checks
 
 use std::alloc::{alloc_zeroed, Layout};
 use std::slice::from_raw_parts;
diff --git a/tests/kani/Uninit/atomic.rs b/tests/kani/Uninit/atomic.rs
index 6de5460d57ca..376f365d408c 100644
--- a/tests/kani/Uninit/atomic.rs
+++ b/tests/kani/Uninit/atomic.rs
@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: -Z ghost-state -Z uninit-checks
+// kani-flags: -Z uninit-checks
 
 use std::sync::atomic::{AtomicUsize, Ordering};
 
diff --git a/tests/kani/Uninit/struct-padding-and-arr-init.rs b/tests/kani/Uninit/struct-padding-and-arr-init.rs
index 63e245415c21..c67b1177bfa3 100644
--- a/tests/kani/Uninit/struct-padding-and-arr-init.rs
+++ b/tests/kani/Uninit/struct-padding-and-arr-init.rs
@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: -Z ghost-state -Z uninit-checks
+// kani-flags: -Z uninit-checks
 
 use std::ptr::addr_of_mut;
 
diff --git a/tests/kani/Uninit/vec-read-init.rs b/tests/kani/Uninit/vec-read-init.rs
index c4a418db93e5..78812c59830e 100644
--- a/tests/kani/Uninit/vec-read-init.rs
+++ b/tests/kani/Uninit/vec-read-init.rs
@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: -Z ghost-state -Z uninit-checks
+// kani-flags: -Z uninit-checks
 
 #[kani::proof]
 fn vec_read_init() {