diff --git a/library/kani/src/models/mod.rs b/library/kani/src/models/mod.rs
index e11e15e4f709..774b6968ee93 100644
--- a/library/kani/src/models/mod.rs
+++ b/library/kani/src/models/mod.rs
@@ -247,7 +247,7 @@ mod test {
     }
 
     #[repr(simd)]
-    #[derive(Clone, Debug)]
+    #[derive(Copy, Clone, Debug)]
     struct CustomMask<T, const LANES: usize>([T; LANES]);
 
     /// Check that the bitmask model can handle odd size SIMD arrays.
@@ -276,15 +276,14 @@ mod test {
     /// Compare the value returned by our model and the simd_bitmask intrinsic.
     fn check_bitmask<T, U, E, const LANES: usize>(mask: T)
     where
-        T: Clone,
+        T: Clone + Copy,
         U: PartialEq + Debug,
         E: kani_intrinsic::MaskElement,
         [u8; kani_intrinsic::mask_len(LANES)]: Sized,
     {
-        assert_eq!(
-            unsafe { kani_intrinsic::simd_bitmask::<_, U, E, LANES>(mask.clone()) },
-            unsafe { simd_bitmask::<T, U>(mask) }
-        );
+        assert_eq!(unsafe { kani_intrinsic::simd_bitmask::<_, U, E, LANES>(mask) }, unsafe {
+            simd_bitmask::<T, U>(mask)
+        });
     }
 
     /// Similar to portable simd_harness.
diff --git a/rust-toolchain.toml b/rust-toolchain.toml
index b68d04d7cbbc..af3af69e4885 100644
--- a/rust-toolchain.toml
+++ b/rust-toolchain.toml
@@ -2,5 +2,5 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 [toolchain]
-channel = "nightly-2025-07-21"
+channel = "nightly-2025-07-24"
 components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]
diff --git a/tests/expected/intrinsics/simd-arith-overflows/main.rs b/tests/expected/intrinsics/simd-arith-overflows/main.rs
index 28be8e309774..b1ee692ac00b 100644
--- a/tests/expected/intrinsics/simd-arith-overflows/main.rs
+++ b/tests/expected/intrinsics/simd-arith-overflows/main.rs
@@ -7,7 +7,7 @@ use std::intrinsics::simd::{simd_add, simd_mul, simd_sub};
 
 #[repr(simd)]
 #[allow(non_camel_case_types)]
-#[derive(Clone, Copy, PartialEq, Eq, Debug)]
+#[derive(Clone, Copy)]
 pub struct i8x2([i8; 2]);
 
 #[kani::proof]
diff --git a/tests/expected/intrinsics/simd-cmp-result-type-is-diff-size/main.rs b/tests/expected/intrinsics/simd-cmp-result-type-is-diff-size/main.rs
index fd4dd40b17b8..b2c88f170889 100644
--- a/tests/expected/intrinsics/simd-cmp-result-type-is-diff-size/main.rs
+++ b/tests/expected/intrinsics/simd-cmp-result-type-is-diff-size/main.rs
@@ -8,19 +8,25 @@ use std::intrinsics::simd::simd_eq;
 
 #[repr(simd)]
 #[allow(non_camel_case_types)]
-#[derive(Clone, Copy, PartialEq, Eq)]
+#[derive(Clone, Copy)]
 pub struct i64x2([i64; 2]);
 
 #[repr(simd)]
 #[allow(non_camel_case_types)]
-#[derive(Clone, Copy, PartialEq, Eq)]
+#[derive(Clone, Copy)]
 pub struct u64x2([u64; 2]);
 
 #[repr(simd)]
 #[allow(non_camel_case_types)]
-#[derive(Clone, Copy, PartialEq, Eq)]
+#[derive(Clone, Copy)]
 pub struct u32x4([u32; 4]);
 
+impl u32x4 {
+    fn into_array(self) -> [u32; 4] {
+        unsafe { std::mem::transmute(self) }
+    }
+}
+
 #[kani::proof]
 fn main() {
     let x = u64x2([0, 0]);
@@ -28,7 +34,7 @@ fn main() {
 
     unsafe {
         let invalid_simd: u32x4 = simd_eq(x, y);
-        assert!(invalid_simd == u32x4([u32::MAX, u32::MAX, 0, 0]));
+        assert!(invalid_simd.into_array() == u32x4([u32::MAX, u32::MAX, 0, 0]).into_array());
         // ^^^^ The code above fails to type-check in Rust with the error:
         // ```
         // error[E0511]: invalid monomorphization of `simd_eq` intrinsic: expected
diff --git a/tests/expected/intrinsics/simd-div-div-zero/main.rs b/tests/expected/intrinsics/simd-div-div-zero/main.rs
index 0765e0fd0755..c560b50f90f0 100644
--- a/tests/expected/intrinsics/simd-div-div-zero/main.rs
+++ b/tests/expected/intrinsics/simd-div-div-zero/main.rs
@@ -7,7 +7,7 @@ use std::intrinsics::simd::simd_div;
 
 #[repr(simd)]
 #[allow(non_camel_case_types)]
-#[derive(Clone, Copy, PartialEq, Eq)]
+#[derive(Clone, Copy)]
 pub struct i32x2([i32; 2]);
 
 #[kani::proof]
diff --git a/tests/expected/intrinsics/simd-div-rem-overflow/expected b/tests/expected/intrinsics/simd-div-rem-overflow/expected
index 9c1a0aa96774..27828cf8268c 100644
--- a/tests/expected/intrinsics/simd-div-rem-overflow/expected
+++ b/tests/expected/intrinsics/simd-div-rem-overflow/expected
@@ -1,8 +1,8 @@
 FAILURE\
 attempt to compute simd_div which would overflow
 UNREACHABLE\
-assertion failed: quotients.0[0] == quotients.0[1]
+assertion failed: quotients.into_array()[0] == quotients.into_array()[1]
 FAILURE\
 attempt to compute simd_rem which would overflow
 UNREACHABLE\
-assertion failed: remainders.0[0] == remainders.0[1]
\ No newline at end of file
+assertion failed: remainders.into_array()[0] == remainders.into_array()[1]
diff --git a/tests/expected/intrinsics/simd-div-rem-overflow/main.rs b/tests/expected/intrinsics/simd-div-rem-overflow/main.rs
index 117fd6bffe95..7e22c12896b2 100644
--- a/tests/expected/intrinsics/simd-div-rem-overflow/main.rs
+++ b/tests/expected/intrinsics/simd-div-rem-overflow/main.rs
@@ -7,9 +7,15 @@ use std::intrinsics::simd::{simd_div, simd_rem};
 
 #[repr(simd)]
 #[allow(non_camel_case_types)]
-#[derive(Clone, Copy, PartialEq, Eq)]
+#[derive(Clone, Copy)]
 pub struct i32x2([i32; 2]);
 
+impl i32x2 {
+    fn into_array(self) -> [i32; 2] {
+        unsafe { std::mem::transmute(self) }
+    }
+}
+
 unsafe fn do_simd_div(dividends: i32x2, divisors: i32x2) -> i32x2 {
     simd_div(dividends, divisors)
 }
@@ -25,7 +31,7 @@ fn test_simd_div_overflow() {
     let divisor = -1;
     let divisors = i32x2([divisor, divisor]);
     let quotients = unsafe { do_simd_div(dividends, divisors) };
-    assert_eq!(quotients.0[0], quotients.0[1]);
+    assert_eq!(quotients.into_array()[0], quotients.into_array()[1]);
 }
 
 #[kani::proof]
@@ -35,5 +41,5 @@ fn test_simd_rem_overflow() {
     let divisor = -1;
     let divisors = i32x2([divisor, divisor]);
     let remainders = unsafe { do_simd_rem(dividends, divisors) };
-    assert_eq!(remainders.0[0], remainders.0[1]);
+    assert_eq!(remainders.into_array()[0], remainders.into_array()[1]);
 }
diff --git a/tests/expected/intrinsics/simd-extract-wrong-type/main.rs b/tests/expected/intrinsics/simd-extract-wrong-type/main.rs
index 9af6b5279ec6..2eb1a146d923 100644
--- a/tests/expected/intrinsics/simd-extract-wrong-type/main.rs
+++ b/tests/expected/intrinsics/simd-extract-wrong-type/main.rs
@@ -9,7 +9,7 @@ use std::intrinsics::simd::simd_extract;
 
 #[repr(simd)]
 #[allow(non_camel_case_types)]
-#[derive(Clone, Copy, PartialEq, Eq)]
+#[derive(Clone, Copy)]
 pub struct i64x2([i64; 2]);
 
 #[kani::proof]
diff --git a/tests/expected/intrinsics/simd-insert-wrong-type/main.rs b/tests/expected/intrinsics/simd-insert-wrong-type/main.rs
index 8a0853cc7945..5ef04e6961ba 100644
--- a/tests/expected/intrinsics/simd-insert-wrong-type/main.rs
+++ b/tests/expected/intrinsics/simd-insert-wrong-type/main.rs
@@ -9,7 +9,7 @@ use std::intrinsics::simd::simd_insert;
 
 #[repr(simd)]
 #[allow(non_camel_case_types)]
-#[derive(Clone, Copy, PartialEq, Eq)]
+#[derive(Clone, Copy)]
 pub struct i64x2([i64; 2]);
 
 #[kani::proof]
diff --git a/tests/expected/intrinsics/simd-rem-div-zero/main.rs b/tests/expected/intrinsics/simd-rem-div-zero/main.rs
index 7ed9bd2968cd..99d6475dc91e 100644
--- a/tests/expected/intrinsics/simd-rem-div-zero/main.rs
+++ b/tests/expected/intrinsics/simd-rem-div-zero/main.rs
@@ -7,7 +7,7 @@ use std::intrinsics::simd::simd_rem;
 
 #[repr(simd)]
 #[allow(non_camel_case_types)]
-#[derive(Clone, Copy, PartialEq, Eq)]
+#[derive(Clone, Copy)]
 pub struct i32x2([i32; 2]);
 
 #[kani::proof]
diff --git a/tests/expected/intrinsics/simd-result-type-is-float/main.rs b/tests/expected/intrinsics/simd-result-type-is-float/main.rs
index 2d7892a1a537..48a31f6dc3a8 100644
--- a/tests/expected/intrinsics/simd-result-type-is-float/main.rs
+++ b/tests/expected/intrinsics/simd-result-type-is-float/main.rs
@@ -8,24 +8,30 @@ use std::intrinsics::simd::simd_eq;
 
 #[repr(simd)]
 #[allow(non_camel_case_types)]
-#[derive(Clone, Copy, PartialEq, Eq)]
+#[derive(Clone, Copy)]
 pub struct i64x2([i64; 2]);
 
 #[repr(simd)]
 #[allow(non_camel_case_types)]
-#[derive(Clone, Copy, PartialEq, Eq)]
+#[derive(Clone, Copy)]
 pub struct u64x2([u64; 2]);
 
 #[repr(simd)]
 #[allow(non_camel_case_types)]
-#[derive(Clone, Copy, PartialEq, Eq)]
+#[derive(Clone, Copy)]
 pub struct u32x4([u32; 4]);
 
 #[repr(simd)]
 #[allow(non_camel_case_types)]
-#[derive(Clone, Copy, PartialEq)]
+#[derive(Clone, Copy)]
 pub struct f32x2([f32; 2]);
 
+impl f32x2 {
+    fn into_array(self) -> [f32; 2] {
+        unsafe { std::mem::transmute(self) }
+    }
+}
+
 #[kani::proof]
 fn main() {
     let x = u64x2([0, 0]);
@@ -33,7 +39,7 @@ fn main() {
 
     unsafe {
         let invalid_simd: f32x2 = simd_eq(x, y);
-        assert!(invalid_simd == f32x2([0.0, -1.0]));
+        assert!(invalid_simd.into_array() == f32x2([0.0, -1.0]).into_array());
         // ^^^^ The code above fails to type-check in Rust with the error:
         // ```
         // error[E0511]: invalid monomorphization of `simd_eq` intrinsic: expected return type with integer elements, found `f32x2` with non-integer `f32`
diff --git a/tests/expected/intrinsics/simd-shl-shift-negative/main.rs b/tests/expected/intrinsics/simd-shl-shift-negative/main.rs
index f18a9ba14190..2449eea07ff0 100644
--- a/tests/expected/intrinsics/simd-shl-shift-negative/main.rs
+++ b/tests/expected/intrinsics/simd-shl-shift-negative/main.rs
@@ -7,7 +7,7 @@ use std::intrinsics::simd::simd_shl;
 
 #[repr(simd)]
 #[allow(non_camel_case_types)]
-#[derive(Clone, Copy, PartialEq, Eq)]
+#[derive(Clone, Copy)]
 pub struct i32x2([i32; 2]);
 
 #[kani::proof]
diff --git a/tests/expected/intrinsics/simd-shl-shift-too-large/main.rs b/tests/expected/intrinsics/simd-shl-shift-too-large/main.rs
index 75b73a5b81f1..40ffcc781674 100644
--- a/tests/expected/intrinsics/simd-shl-shift-too-large/main.rs
+++ b/tests/expected/intrinsics/simd-shl-shift-too-large/main.rs
@@ -7,7 +7,7 @@ use std::intrinsics::simd::simd_shl;
 
 #[repr(simd)]
 #[allow(non_camel_case_types)]
-#[derive(Clone, Copy, PartialEq, Eq)]
+#[derive(Clone, Copy)]
 pub struct i32x2([i32; 2]);
 
 #[kani::proof]
diff --git a/tests/expected/intrinsics/simd-shr-shift-negative/main.rs b/tests/expected/intrinsics/simd-shr-shift-negative/main.rs
index f46a91b37c21..c73842c24f3f 100644
--- a/tests/expected/intrinsics/simd-shr-shift-negative/main.rs
+++ b/tests/expected/intrinsics/simd-shr-shift-negative/main.rs
@@ -7,7 +7,7 @@ use std::intrinsics::simd::simd_shr;
 
 #[repr(simd)]
 #[allow(non_camel_case_types)]
-#[derive(Clone, Copy, PartialEq, Eq)]
+#[derive(Clone, Copy)]
 pub struct i32x2([i32; 2]);
 
 #[kani::proof]
diff --git a/tests/expected/intrinsics/simd-shr-shift-too-large/main.rs b/tests/expected/intrinsics/simd-shr-shift-too-large/main.rs
index cdcfce0cf755..1b66e682b2a0 100644
--- a/tests/expected/intrinsics/simd-shr-shift-too-large/main.rs
+++ b/tests/expected/intrinsics/simd-shr-shift-too-large/main.rs
@@ -7,7 +7,7 @@ use std::intrinsics::simd::simd_shr;
 
 #[repr(simd)]
 #[allow(non_camel_case_types)]
-#[derive(Clone, Copy, PartialEq, Eq)]
+#[derive(Clone, Copy)]
 pub struct i32x2([i32; 2]);
 
 #[kani::proof]
diff --git a/tests/expected/intrinsics/simd-shuffle-indexes-out/main.rs b/tests/expected/intrinsics/simd-shuffle-indexes-out/main.rs
index a9da5c773743..461d89260f29 100644
--- a/tests/expected/intrinsics/simd-shuffle-indexes-out/main.rs
+++ b/tests/expected/intrinsics/simd-shuffle-indexes-out/main.rs
@@ -8,7 +8,7 @@ use std::intrinsics::simd::simd_shuffle;
 
 #[repr(simd)]
 #[allow(non_camel_case_types)]
-#[derive(Clone, Copy, PartialEq, Eq)]
+#[derive(Clone, Copy)]
 pub struct i64x2([i64; 2]);
 
 #[repr(simd)]
diff --git a/tests/expected/intrinsics/simd-shuffle-result-type-is-diff-size/main.rs b/tests/expected/intrinsics/simd-shuffle-result-type-is-diff-size/main.rs
index 3936f39ed318..d695c3f84c43 100644
--- a/tests/expected/intrinsics/simd-shuffle-result-type-is-diff-size/main.rs
+++ b/tests/expected/intrinsics/simd-shuffle-result-type-is-diff-size/main.rs
@@ -8,12 +8,12 @@ use std::intrinsics::simd::simd_shuffle;
 
 #[repr(simd)]
 #[allow(non_camel_case_types)]
-#[derive(Clone, Copy, PartialEq, Eq)]
+#[derive(Clone, Copy)]
 pub struct i64x2([i64; 2]);
 
 #[repr(simd)]
 #[allow(non_camel_case_types)]
-#[derive(Clone, Copy, PartialEq, Eq)]
+#[derive(Clone, Copy)]
 pub struct i64x4([i64; 4]);
 
 #[repr(simd)]
diff --git a/tests/expected/intrinsics/simd-shuffle-result-type-is-diff-type/main.rs b/tests/expected/intrinsics/simd-shuffle-result-type-is-diff-type/main.rs
index 7f8c511a96e5..e96fd7e7a173 100644
--- a/tests/expected/intrinsics/simd-shuffle-result-type-is-diff-type/main.rs
+++ b/tests/expected/intrinsics/simd-shuffle-result-type-is-diff-type/main.rs
@@ -8,12 +8,12 @@ use std::intrinsics::simd::simd_shuffle;
 
 #[repr(simd)]
 #[allow(non_camel_case_types)]
-#[derive(Clone, Copy, PartialEq)]
+#[derive(Clone, Copy)]
 pub struct i64x2([i64; 2]);
 
 #[repr(simd)]
 #[allow(non_camel_case_types)]
-#[derive(Clone, Copy, PartialEq)]
+#[derive(Clone, Copy)]
 pub struct f64x2([f64; 2]);
 
 #[repr(simd)]
diff --git a/tests/kani/Intrinsics/SIMD/Compare/float.rs b/tests/kani/Intrinsics/SIMD/Compare/float.rs
index 6c69d142ff7d..f193ffd5d86c 100644
--- a/tests/kani/Intrinsics/SIMD/Compare/float.rs
+++ b/tests/kani/Intrinsics/SIMD/Compare/float.rs
@@ -7,23 +7,29 @@ use std::intrinsics::simd::*;
 
 #[repr(simd)]
 #[allow(non_camel_case_types)]
-#[derive(Clone, Copy, PartialEq)]
+#[derive(Clone, Copy)]
 pub struct f64x2([f64; 2]);
 
 #[repr(simd)]
 #[allow(non_camel_case_types)]
-#[derive(Clone, Copy, PartialEq)]
+#[derive(Clone, Copy)]
 pub struct i64x2([i64; 2]);
 
 #[repr(simd)]
 #[allow(non_camel_case_types)]
-#[derive(Clone, Copy, PartialEq)]
+#[derive(Clone, Copy)]
 pub struct i32x2([i32; 2]);
 
+impl i32x2 {
+    fn into_array(self) -> [i32; 2] {
+        unsafe { std::mem::transmute(self) }
+    }
+}
+
 macro_rules! assert_cmp {
     ($res_cmp: ident, $simd_cmp: ident, $x: expr, $y: expr, $($res: expr),+) => {
         let $res_cmp: i32x2 = $simd_cmp($x, $y);
-        assert!($res_cmp == i32x2($($res),+))
+        assert!($res_cmp.into_array() == i32x2($($res),+).into_array())
     };
 }
 
diff --git a/tests/kani/Intrinsics/SIMD/Compare/result_type_is_same_size.rs b/tests/kani/Intrinsics/SIMD/Compare/result_type_is_same_size.rs
index 584a5e07876a..3d1baaa4ad07 100644
--- a/tests/kani/Intrinsics/SIMD/Compare/result_type_is_same_size.rs
+++ b/tests/kani/Intrinsics/SIMD/Compare/result_type_is_same_size.rs
@@ -8,19 +8,31 @@ use std::intrinsics::simd::simd_eq;
 
 #[repr(simd)]
 #[allow(non_camel_case_types)]
-#[derive(Clone, Copy, PartialEq, Eq)]
+#[derive(Clone, Copy)]
 pub struct i64x2([i64; 2]);
 
+impl i64x2 {
+    fn into_array(self) -> [i64; 2] {
+        unsafe { std::mem::transmute(self) }
+    }
+}
+
 #[repr(simd)]
 #[allow(non_camel_case_types)]
-#[derive(Clone, Copy, PartialEq, Eq)]
+#[derive(Clone, Copy)]
 pub struct u64x2([u64; 2]);
 
 #[repr(simd)]
 #[allow(non_camel_case_types)]
-#[derive(Clone, Copy, PartialEq, Eq)]
+#[derive(Clone, Copy)]
 pub struct u32x2([u32; 2]);
 
+impl u32x2 {
+    fn into_array(self) -> [u32; 2] {
+        unsafe { std::mem::transmute(self) }
+    }
+}
+
 #[kani::proof]
 fn main() {
     let x = u64x2([0, 0]);
@@ -28,9 +40,9 @@ fn main() {
 
     unsafe {
         let w: i64x2 = simd_eq(x, y);
-        assert!(w == i64x2([-1, 0]));
+        assert!(w.into_array() == i64x2([-1, 0]).into_array());
 
         let z: u32x2 = simd_eq(x, y);
-        assert!(z == u32x2([u32::MAX, 0]));
+        assert!(z.into_array() == u32x2([u32::MAX, 0]).into_array());
     }
 }
diff --git a/tests/kani/Intrinsics/SIMD/Compare/signed.rs b/tests/kani/Intrinsics/SIMD/Compare/signed.rs
index 671078bad2d4..ce08749dd7de 100644
--- a/tests/kani/Intrinsics/SIMD/Compare/signed.rs
+++ b/tests/kani/Intrinsics/SIMD/Compare/signed.rs
@@ -7,13 +7,19 @@ use std::intrinsics::simd::*;
 
 #[repr(simd)]
 #[allow(non_camel_case_types)]
-#[derive(Clone, Copy, PartialEq, Eq)]
+#[derive(Clone, Copy)]
 pub struct i64x2([i64; 2]);
 
+impl i64x2 {
+    fn into_array(self) -> [i64; 2] {
+        unsafe { std::mem::transmute(self) }
+    }
+}
+
 macro_rules! assert_cmp {
     ($res_cmp: ident, $simd_cmp: ident, $x: expr, $y: expr, $($res: expr),+) => {
         let $res_cmp: i64x2 = $simd_cmp($x, $y);
-        assert!($res_cmp == i64x2($($res),+))
+        assert!($res_cmp.into_array() == i64x2($($res),+).into_array())
     };
 }
 
diff --git a/tests/kani/Intrinsics/SIMD/Compare/unsigned.rs b/tests/kani/Intrinsics/SIMD/Compare/unsigned.rs
index b2943b36ab71..13c83406ac56 100644
--- a/tests/kani/Intrinsics/SIMD/Compare/unsigned.rs
+++ b/tests/kani/Intrinsics/SIMD/Compare/unsigned.rs
@@ -7,13 +7,19 @@ use std::intrinsics::simd::*;
 
 #[repr(simd)]
 #[allow(non_camel_case_types)]
-#[derive(Clone, Copy, PartialEq, Eq)]
+#[derive(Clone, Copy)]
 pub struct u64x2([u64; 2]);
 
+impl u64x2 {
+    fn into_array(self) -> [u64; 2] {
+        unsafe { std::mem::transmute(self) }
+    }
+}
+
 macro_rules! assert_cmp {
     ($res_cmp: ident, $simd_cmp: ident, $x: expr, $y: expr, $($res: expr),+) => {
         let $res_cmp: u64x2 = $simd_cmp($x, $y);
-        assert!($res_cmp == u64x2($($res),+))
+        assert!($res_cmp.into_array() == u64x2($($res),+).into_array())
     };
 }
 
diff --git a/tests/kani/Intrinsics/SIMD/Construction/main.rs b/tests/kani/Intrinsics/SIMD/Construction/main.rs
index 92c5a167dc15..24948068ae1e 100644
--- a/tests/kani/Intrinsics/SIMD/Construction/main.rs
+++ b/tests/kani/Intrinsics/SIMD/Construction/main.rs
@@ -8,17 +8,23 @@ use std::intrinsics::simd::{simd_extract, simd_insert};
 
 #[repr(simd)]
 #[allow(non_camel_case_types)]
-#[derive(Clone, Copy, PartialEq, Eq)]
+#[derive(Clone, Copy)]
 pub struct i64x2([i64; 2]);
 
+impl i64x2 {
+    fn into_array(self) -> [i64; 2] {
+        unsafe { std::mem::transmute(self) }
+    }
+}
+
 #[kani::proof]
 fn main() {
     let y = i64x2([0, 1]);
     let z = i64x2([1, 2]);
 
     // Indexing into the vectors
-    assert!(z.0[0] == 1);
-    assert!(z.0[1] == 2);
+    assert!(z.into_array()[0] == 1);
+    assert!(z.into_array()[1] == 2);
 
     {
         // Intrinsic indexing
@@ -31,9 +37,9 @@ fn main() {
         // Intrinsic updating
         let m = unsafe { simd_insert(y, 0, 1_i64) };
         let n = unsafe { simd_insert(y, 1, 5_i64) };
-        assert!(m.0[0] == 1 && m.0[1] == 1);
-        assert!(n.0[0] == 0 && n.0[1] == 5);
+        assert!(m.into_array()[0] == 1 && m.into_array()[1] == 1);
+        assert!(n.into_array()[0] == 0 && n.into_array()[1] == 5);
         // Original unchanged
-        assert!(y.0[0] == 0 && y.0[1] == 1);
+        assert!(y.into_array()[0] == 0 && y.into_array()[1] == 1);
     }
 }
diff --git a/tests/kani/Intrinsics/SIMD/Operators/arith.rs b/tests/kani/Intrinsics/SIMD/Operators/arith.rs
index 33a8ba65b538..71dff8eb4944 100644
--- a/tests/kani/Intrinsics/SIMD/Operators/arith.rs
+++ b/tests/kani/Intrinsics/SIMD/Operators/arith.rs
@@ -8,9 +8,15 @@ use std::intrinsics::simd::{simd_add, simd_mul, simd_sub};
 
 #[repr(simd)]
 #[allow(non_camel_case_types)]
-#[derive(Clone, Copy, PartialEq, Eq)]
+#[derive(Clone, Copy)]
 pub struct i8x2([i8; 2]);
 
+impl i8x2 {
+    fn into_array(self) -> [i8; 2] {
+        unsafe { std::mem::transmute(self) }
+    }
+}
+
 macro_rules! verify_no_overflow {
     ($cf: ident, $uf: ident) => {{
         let a: i8 = kani::any();
@@ -20,8 +26,8 @@ macro_rules! verify_no_overflow {
         let simd_a = i8x2([a, a]);
         let simd_b = i8x2([b, b]);
         let unchecked: i8x2 = unsafe { $uf(simd_a, simd_b) };
-        assert!(checked.unwrap() == unchecked.0[0]);
-        assert!(checked.unwrap() == unchecked.0[1]);
+        assert!(checked.unwrap() == unchecked.into_array()[0]);
+        assert!(checked.unwrap() == unchecked.into_array()[1]);
     }};
 }
 
diff --git a/tests/kani/Intrinsics/SIMD/Operators/bitmask.rs b/tests/kani/Intrinsics/SIMD/Operators/bitmask.rs
index 6992408436b9..118c4f757672 100644
--- a/tests/kani/Intrinsics/SIMD/Operators/bitmask.rs
+++ b/tests/kani/Intrinsics/SIMD/Operators/bitmask.rs
@@ -9,11 +9,10 @@
 #![feature(repr_simd, core_intrinsics)]
 #![feature(generic_const_exprs)]
 #![feature(portable_simd)]
-use std::fmt::Debug;
 use std::intrinsics::simd::simd_bitmask;
 
 #[repr(simd)]
-#[derive(Clone, Debug)]
+#[derive(Clone, Copy)]
 struct CustomMask<const LANES: usize>([i32; LANES]);
 
 impl<const LANES: usize> CustomMask<LANES> {
@@ -48,7 +47,7 @@ fn check_u8() {
 #[kani::proof]
 fn check_unsigned_bitmask() {
     let mask = kani::any::<CustomMask<8>>();
-    let bitmask = unsafe { simd_bitmask::<_, u8>(mask.clone()) };
+    let bitmask = unsafe { simd_bitmask::<_, u8>(mask) };
     assert_eq!(bitmask.count_ones() as usize, mask.as_array().iter().filter(|e| **e == -1).count());
     assert_eq!(bitmask.count_zeros() as usize, mask.as_array().iter().filter(|e| **e == 0).count());
 }
diff --git a/tests/kani/Intrinsics/SIMD/Operators/bitshift.rs b/tests/kani/Intrinsics/SIMD/Operators/bitshift.rs
index 09a19fa7b29a..720de328d1a7 100644
--- a/tests/kani/Intrinsics/SIMD/Operators/bitshift.rs
+++ b/tests/kani/Intrinsics/SIMD/Operators/bitshift.rs
@@ -8,14 +8,26 @@ use std::intrinsics::simd::{simd_shl, simd_shr};
 
 #[repr(simd)]
 #[allow(non_camel_case_types)]
-#[derive(Clone, Copy, PartialEq, Eq)]
+#[derive(Clone, Copy)]
 pub struct i32x2([i32; 2]);
 
+impl i32x2 {
+    fn into_array(self) -> [i32; 2] {
+        unsafe { std::mem::transmute(self) }
+    }
+}
+
 #[repr(simd)]
 #[allow(non_camel_case_types)]
-#[derive(Clone, Copy, PartialEq, Eq)]
+#[derive(Clone, Copy)]
 pub struct u32x2([u32; 2]);
 
+impl u32x2 {
+    fn into_array(self) -> [u32; 2] {
+        unsafe { std::mem::transmute(self) }
+    }
+}
+
 #[kani::proof]
 fn test_simd_shl() {
     let value = kani::any();
@@ -26,7 +38,7 @@ fn test_simd_shl() {
     let shifts = i32x2([shift, shift]);
     let normal_result = value << shift;
     let simd_result = unsafe { simd_shl(values, shifts) };
-    assert_eq!(normal_result, simd_result.0[0]);
+    assert_eq!(normal_result, simd_result.into_array()[0]);
 }
 
 #[kani::proof]
@@ -39,7 +51,7 @@ fn test_simd_shr_signed() {
     let shifts = i32x2([shift, shift]);
     let normal_result = value >> shift;
     let simd_result = unsafe { simd_shr(values, shifts) };
-    assert_eq!(normal_result, simd_result.0[0]);
+    assert_eq!(normal_result, simd_result.into_array()[0]);
 }
 
 #[kani::proof]
@@ -51,5 +63,5 @@ fn test_simd_shr_unsigned() {
     let shifts = u32x2([shift, shift]);
     let normal_result = value >> shift;
     let simd_result = unsafe { simd_shr(values, shifts) };
-    assert_eq!(normal_result, simd_result.0[0]);
+    assert_eq!(normal_result, simd_result.into_array()[0]);
 }
diff --git a/tests/kani/Intrinsics/SIMD/Operators/bitwise.rs b/tests/kani/Intrinsics/SIMD/Operators/bitwise.rs
index a9aaa96f75e5..fee3682d1bc2 100644
--- a/tests/kani/Intrinsics/SIMD/Operators/bitwise.rs
+++ b/tests/kani/Intrinsics/SIMD/Operators/bitwise.rs
@@ -13,44 +13,92 @@ use std::intrinsics::simd::{simd_and, simd_or, simd_xor};
 
 #[repr(simd)]
 #[allow(non_camel_case_types)]
-#[derive(Clone, Copy, PartialEq, Eq)]
+#[derive(Clone, Copy)]
 pub struct i8x2([i8; 2]);
 
+impl i8x2 {
+    fn into_array(self) -> [i8; 2] {
+        unsafe { std::mem::transmute(self) }
+    }
+}
+
 #[repr(simd)]
 #[allow(non_camel_case_types)]
-#[derive(Clone, Copy, PartialEq, Eq)]
+#[derive(Clone, Copy)]
 pub struct i16x2([i16; 2]);
 
+impl i16x2 {
+    fn into_array(self) -> [i16; 2] {
+        unsafe { std::mem::transmute(self) }
+    }
+}
+
 #[repr(simd)]
 #[allow(non_camel_case_types)]
-#[derive(Clone, Copy, PartialEq, Eq)]
+#[derive(Clone, Copy)]
 pub struct i32x2([i32; 2]);
 
+impl i32x2 {
+    fn into_array(self) -> [i32; 2] {
+        unsafe { std::mem::transmute(self) }
+    }
+}
+
 #[repr(simd)]
 #[allow(non_camel_case_types)]
-#[derive(Clone, Copy, PartialEq, Eq)]
+#[derive(Clone, Copy)]
 pub struct i64x2([i64; 2]);
 
+impl i64x2 {
+    fn into_array(self) -> [i64; 2] {
+        unsafe { std::mem::transmute(self) }
+    }
+}
+
 #[repr(simd)]
 #[allow(non_camel_case_types)]
-#[derive(Clone, Copy, PartialEq, Eq)]
+#[derive(Clone, Copy)]
 pub struct u8x2([u8; 2]);
 
+impl u8x2 {
+    fn into_array(self) -> [u8; 2] {
+        unsafe { std::mem::transmute(self) }
+    }
+}
+
 #[repr(simd)]
 #[allow(non_camel_case_types)]
-#[derive(Clone, Copy, PartialEq, Eq)]
+#[derive(Clone, Copy)]
 pub struct u16x2([u16; 2]);
 
+impl u16x2 {
+    fn into_array(self) -> [u16; 2] {
+        unsafe { std::mem::transmute(self) }
+    }
+}
+
 #[repr(simd)]
 #[allow(non_camel_case_types)]
-#[derive(Clone, Copy, PartialEq, Eq)]
+#[derive(Clone, Copy)]
 pub struct u32x2([u32; 2]);
 
+impl u32x2 {
+    fn into_array(self) -> [u32; 2] {
+        unsafe { std::mem::transmute(self) }
+    }
+}
+
 #[repr(simd)]
 #[allow(non_camel_case_types)]
-#[derive(Clone, Copy, PartialEq, Eq)]
+#[derive(Clone, Copy)]
 pub struct u64x2([u64; 2]);
 
+impl u64x2 {
+    fn into_array(self) -> [u64; 2] {
+        unsafe { std::mem::transmute(self) }
+    }
+}
+
 macro_rules! compare_simd_op_with_normal_op {
     ($simd_op: ident, $normal_op: tt, $simd_type: ident) => {
         let tup_x: (_,_) = kani::any();
@@ -58,8 +106,8 @@ macro_rules! compare_simd_op_with_normal_op {
         let x = $simd_type([tup_x.0, tup_x.1]);
         let y = $simd_type([tup_y.0, tup_y.1]);
         let res_and = unsafe { $simd_op(x, y) };
-        assert_eq!(tup_x.0 $normal_op tup_y.0, res_and.0[0]);
-        assert_eq!(tup_x.1 $normal_op tup_y.1, res_and.0[1]);
+        assert_eq!(tup_x.0 $normal_op tup_y.0, res_and.into_array()[0]);
+        assert_eq!(tup_x.1 $normal_op tup_y.1, res_and.into_array()[1]);
     };
 }
 
diff --git a/tests/kani/Intrinsics/SIMD/Operators/division.rs b/tests/kani/Intrinsics/SIMD/Operators/division.rs
index d48968342ca4..bc15258387a9 100644
--- a/tests/kani/Intrinsics/SIMD/Operators/division.rs
+++ b/tests/kani/Intrinsics/SIMD/Operators/division.rs
@@ -8,9 +8,15 @@ use std::intrinsics::simd::{simd_div, simd_rem};
 
 #[repr(simd)]
 #[allow(non_camel_case_types)]
-#[derive(Clone, Copy, PartialEq, Eq)]
+#[derive(Clone, Copy)]
 pub struct i32x2([i32; 2]);
 
+impl i32x2 {
+    fn into_array(self) -> [i32; 2] {
+        unsafe { std::mem::transmute(self) }
+    }
+}
+
 #[kani::proof]
 fn test_simd_div() {
     let dividend = kani::any();
@@ -22,7 +28,7 @@ fn test_simd_div() {
     let divisors = i32x2([divisor, divisor]);
     let normal_result = dividend / divisor;
     let simd_result = unsafe { simd_div(dividends, divisors) };
-    assert_eq!(normal_result, simd_result.0[0]);
+    assert_eq!(normal_result, simd_result.into_array()[0]);
 }
 
 #[kani::proof]
@@ -36,5 +42,5 @@ fn test_simd_rem() {
     let divisors = i32x2([divisor, divisor]);
     let normal_result = dividend % divisor;
     let simd_result = unsafe { simd_rem(dividends, divisors) };
-    assert_eq!(normal_result, simd_result.0[0]);
+    assert_eq!(normal_result, simd_result.into_array()[0]);
 }
diff --git a/tests/kani/Intrinsics/SIMD/Operators/division_float.rs b/tests/kani/Intrinsics/SIMD/Operators/division_float.rs
index d61bd81f1f87..de962dcb321f 100644
--- a/tests/kani/Intrinsics/SIMD/Operators/division_float.rs
+++ b/tests/kani/Intrinsics/SIMD/Operators/division_float.rs
@@ -7,16 +7,25 @@ use std::intrinsics::simd::simd_div;
 
 #[repr(simd)]
 #[allow(non_camel_case_types)]
-#[derive(Clone, Copy, PartialEq, kani::Arbitrary)]
+#[derive(Clone, Copy, kani::Arbitrary)]
 pub struct f32x2([f32; 2]);
 
+impl f32x2 {
+    fn into_array(self) -> [f32; 2] {
+        unsafe { std::mem::transmute(self) }
+    }
+}
+
 impl f32x2 {
     fn new_with(f: impl Fn() -> f32) -> Self {
         f32x2([f(), f()])
     }
 
     fn non_simd_div(self, divisors: Self) -> Self {
-        f32x2([self.0[0] / divisors.0[0], self.0[1] / divisors.0[1]])
+        f32x2([
+            self.into_array()[0] / divisors.into_array()[0],
+            self.into_array()[1] / divisors.into_array()[1],
+        ])
     }
 }
 
@@ -32,5 +41,5 @@ fn test_simd_div() {
     });
     let normal_results = dividends.non_simd_div(divisors);
     let simd_results = unsafe { simd_div(dividends, divisors) };
-    assert_eq!(normal_results, simd_results);
+    assert_eq!(normal_results.into_array(), simd_results.into_array());
 }
diff --git a/tests/kani/Intrinsics/SIMD/Operators/remainder_float_fixme.rs b/tests/kani/Intrinsics/SIMD/Operators/remainder_float_fixme.rs
index e64498e20242..3cd046d7e309 100644
--- a/tests/kani/Intrinsics/SIMD/Operators/remainder_float_fixme.rs
+++ b/tests/kani/Intrinsics/SIMD/Operators/remainder_float_fixme.rs
@@ -7,16 +7,25 @@ use std::intrinsics::simd::simd_rem;
 
 #[repr(simd)]
 #[allow(non_camel_case_types)]
-#[derive(Clone, Copy, PartialEq, kani::Arbitrary)]
-pub struct f32x2(f32, f32);
+#[derive(Clone, Copy, kani::Arbitrary)]
+pub struct f32x2([f32; 2]);
+
+impl f32x2 {
+    fn into_array(self) -> [f32; 2] {
+        unsafe { std::mem::transmute(self) }
+    }
+}
 
 impl f32x2 {
     fn new_with(f: impl Fn() -> f32) -> Self {
-        f32x2(f(), f())
+        f32x2([f(), f()])
     }
 
     fn non_simd_rem(self, divisors: Self) -> Self {
-        f32x2(self.0 % divisors.0, self.1 % divisors.1)
+        f32x2([
+            self.into_array()[0] % divisors.into_array()[0],
+            self.into_array()[1] % divisors.into_array()[1],
+        ])
     }
 }
 
@@ -32,5 +41,5 @@ fn test_simd_rem() {
     });
     let normal_results = dividends.non_simd_rem(divisors);
     let simd_results = unsafe { simd_rem(dividends, divisors) };
-    assert_eq!(normal_results, simd_results);
+    assert_eq!(normal_results.into_array(), simd_results.into_array());
 }
diff --git a/tests/kani/Intrinsics/SIMD/Shuffle/main.rs b/tests/kani/Intrinsics/SIMD/Shuffle/main.rs
index b20c16be5877..5033244cad15 100644
--- a/tests/kani/Intrinsics/SIMD/Shuffle/main.rs
+++ b/tests/kani/Intrinsics/SIMD/Shuffle/main.rs
@@ -8,14 +8,26 @@ use std::intrinsics::simd::simd_shuffle;
 
 #[repr(simd)]
 #[allow(non_camel_case_types)]
-#[derive(Clone, Copy, PartialEq, Eq)]
+#[derive(Clone, Copy)]
 pub struct i64x2([i64; 2]);
 
+impl i64x2 {
+    fn into_array(self) -> [i64; 2] {
+        unsafe { std::mem::transmute(self) }
+    }
+}
+
 #[repr(simd)]
 #[allow(non_camel_case_types)]
-#[derive(Clone, Copy, PartialEq, Eq)]
+#[derive(Clone, Copy)]
 pub struct i64x4([i64; 4]);
 
+impl i64x4 {
+    fn into_array(self) -> [i64; 4] {
+        unsafe { std::mem::transmute(self) }
+    }
+}
+
 #[repr(simd)]
 struct SimdShuffleIdx<const LEN: usize>([u32; LEN]);
 
@@ -26,23 +38,23 @@ fn main() {
         let z = i64x2([1, 2]);
         const I: SimdShuffleIdx<2> = SimdShuffleIdx([1, 2]);
         let x: i64x2 = unsafe { simd_shuffle(y, z, I) };
-        assert!(x.0[0] == 1);
-        assert!(x.0[1] == 1);
+        assert!(x.into_array()[0] == 1);
+        assert!(x.into_array()[1] == 1);
     }
     {
         let y = i64x2([0, 1]);
         let z = i64x2([1, 2]);
         const I: SimdShuffleIdx<2> = SimdShuffleIdx([1, 2]);
         let x: i64x2 = unsafe { simd_shuffle(y, z, I) };
-        assert!(x.0[0] == 1);
-        assert!(x.0[1] == 1);
+        assert!(x.into_array()[0] == 1);
+        assert!(x.into_array()[1] == 1);
     }
     {
         let a = i64x4([1, 2, 3, 4]);
         let b = i64x4([5, 6, 7, 8]);
         const I: SimdShuffleIdx<4> = SimdShuffleIdx([1, 3, 5, 7]);
         let c: i64x4 = unsafe { simd_shuffle(a, b, I) };
-        assert!(c == i64x4([2, 4, 6, 8]));
+        assert!(c.into_array() == i64x4([2, 4, 6, 8]).into_array());
     }
 }
 
diff --git a/tests/kani/SIMD/array_simd_repr.rs b/tests/kani/SIMD/array_simd_repr.rs
index 076427415091..c74ca4e9d7a8 100644
--- a/tests/kani/SIMD/array_simd_repr.rs
+++ b/tests/kani/SIMD/array_simd_repr.rs
@@ -6,9 +6,27 @@
 #![feature(repr_simd)]
 
 #[repr(simd)]
-#[derive(Clone, PartialEq, Eq, PartialOrd, kani::Arbitrary)]
+#[derive(Clone, Copy, kani::Arbitrary)]
 pub struct i64x2([i64; 2]);
 
+impl i64x2 {
+    fn into_array(self) -> [i64; 2] {
+        unsafe { std::mem::transmute(self) }
+    }
+}
+
+impl std::cmp::PartialEq for i64x2 {
+    fn eq(&self, other: &Self) -> bool {
+        self.into_array() == other.into_array()
+    }
+}
+
+impl std::cmp::PartialOrd for i64x2 {
+    fn partial_cmp(&self, other: &Self) -> Option<std::cmp::Ordering> {
+        self.into_array().partial_cmp(&other.into_array())
+    }
+}
+
 #[kani::proof]
 fn check_diff() {
     let x = i64x2([1, 2]);
@@ -19,18 +37,38 @@ fn check_diff() {
 #[kani::proof]
 fn check_ge() {
     let x: i64x2 = kani::any();
-    kani::assume(x.0[0] > 0);
-    kani::assume(x.0[1] > 0);
+    kani::assume(x.into_array()[0] > 0);
+    kani::assume(x.into_array()[1] > 0);
     assert!(x > i64x2([0, 0]));
 }
 
-#[derive(Clone, Debug)]
+#[derive(Copy)]
 #[repr(simd)]
 struct CustomSimd<T, const LANES: usize>([T; LANES]);
 
+impl<T: Copy, const LANES: usize> Clone for CustomSimd<T, LANES> {
+    fn clone(&self) -> Self {
+        *self
+    }
+}
+
+impl<T, const LANES: usize> CustomSimd<T, LANES> {
+    fn as_array(&self) -> &[T; LANES] {
+        let p: *const Self = self;
+        unsafe { &*p.cast::<[T; LANES]>() }
+    }
+
+    fn into_array(self) -> [T; LANES]
+    where
+        T: Copy,
+    {
+        *self.as_array()
+    }
+}
+
 #[kani::proof]
 fn simd_vec() {
     let simd = CustomSimd([0u8; 10]);
     let idx: usize = kani::any_where(|x: &usize| *x < 10);
-    assert_eq!(simd.0[idx], 0);
+    assert_eq!(simd.into_array()[idx], 0);
 }
diff --git a/tests/kani/SIMD/generic_access.rs b/tests/kani/SIMD/generic_access.rs
index 805eeaa403ea..7428624a2ce1 100644
--- a/tests/kani/SIMD/generic_access.rs
+++ b/tests/kani/SIMD/generic_access.rs
@@ -10,13 +10,34 @@ mod array_based {
     use super::*;
 
     #[repr(simd)]
+    #[derive(Copy)]
     struct CustomSimd<T: SimdElement, const LANES: usize>([T; LANES]);
 
+    impl<T: SimdElement, const LANES: usize> Clone for CustomSimd<T, LANES> {
+        fn clone(&self) -> Self {
+            *self
+        }
+    }
+
+    impl<T: SimdElement, const LANES: usize> CustomSimd<T, LANES> {
+        fn as_array(&self) -> &[T; LANES] {
+            let p: *const Self = self;
+            unsafe { &*p.cast::<[T; LANES]>() }
+        }
+
+        fn into_array(self) -> [T; LANES]
+        where
+            T: Copy,
+        {
+            *self.as_array()
+        }
+    }
+
     fn check_fields<T: SimdElement + PartialEq, const LANES: usize>(
         simd: CustomSimd<T, LANES>,
         expected: [T; LANES],
     ) {
-        assert_eq!(simd.0, expected);
+        assert_eq!(simd.into_array(), expected);
     }
 
     #[kani::proof]
@@ -31,14 +52,35 @@ mod fields_based {
     use super::*;
 
     #[repr(simd)]
+    #[derive(Copy)]
     struct CustomSimd<T: SimdElement>([T; 2]);
 
+    impl<T: SimdElement> Clone for CustomSimd<T> {
+        fn clone(&self) -> Self {
+            *self
+        }
+    }
+
+    impl<T: SimdElement> CustomSimd<T> {
+        fn as_array(&self) -> &[T; 2] {
+            let p: *const Self = self;
+            unsafe { &*p.cast::<[T; 2]>() }
+        }
+
+        fn into_array(self) -> [T; 2]
+        where
+            T: Copy,
+        {
+            *self.as_array()
+        }
+    }
+
     fn check_fields<T: SimdElement + PartialEq, const LANES: usize>(
         simd: CustomSimd<T>,
         expected: [T; LANES],
     ) {
-        assert_eq!(simd.0[0], expected[0]);
-        assert_eq!(simd.0[1], expected[1])
+        assert_eq!(simd.into_array()[0], expected[0]);
+        assert_eq!(simd.into_array()[1], expected[1])
     }
 
     #[kani::proof]
diff --git a/tests/kani/SIMD/multi_field_simd.rs b/tests/kani/SIMD/multi_field_simd.rs
index c8cdd848c69e..3f54fda38429 100644
--- a/tests/kani/SIMD/multi_field_simd.rs
+++ b/tests/kani/SIMD/multi_field_simd.rs
@@ -9,20 +9,38 @@
 #![feature(repr_simd)]
 
 #[repr(simd)]
-#[derive(PartialEq, Eq, PartialOrd, kani::Arbitrary)]
+#[derive(Clone, Copy, kani::Arbitrary)]
 pub struct i64x2([i64; 2]);
 
+impl i64x2 {
+    fn into_array(self) -> [i64; 2] {
+        unsafe { std::mem::transmute(self) }
+    }
+}
+
+impl std::cmp::PartialEq for i64x2 {
+    fn eq(&self, other: &Self) -> bool {
+        self.into_array() == other.into_array()
+    }
+}
+
+impl std::cmp::PartialOrd for i64x2 {
+    fn partial_cmp(&self, other: &Self) -> Option<std::cmp::Ordering> {
+        self.into_array().partial_cmp(&other.into_array())
+    }
+}
+
 #[kani::proof]
 fn check_diff() {
     let x = i64x2([1, 2]);
     let y = i64x2([3, 4]);
-    assert!(x != y);
+    assert!(x.into_array() != y.into_array());
 }
 
 #[kani::proof]
 fn check_ge() {
     let x: i64x2 = kani::any();
-    kani::assume(x.0[0] > 0);
-    kani::assume(x.0[1] > 0);
+    kani::assume(x.into_array()[0] > 0);
+    kani::assume(x.into_array()[1] > 0);
     assert!(x > i64x2([0, 0]));
 }
diff --git a/tests/kani/SIMD/simd_bitmask_equiv.rs b/tests/kani/SIMD/simd_bitmask_equiv.rs
index d6f5f589fb41..5ac2c8928d2a 100644
--- a/tests/kani/SIMD/simd_bitmask_equiv.rs
+++ b/tests/kani/SIMD/simd_bitmask_equiv.rs
@@ -7,9 +7,7 @@
 // This test checks the equivalence of Kani's old and new implementations of the
 // `simd_bitmask` intrinsic
 
-use std::fmt::Debug;
-
-pub trait MaskElement: PartialEq + Debug {
+pub trait MaskElement: PartialEq {
     const TRUE: Self;
     const FALSE: Self;
 }
@@ -56,7 +54,7 @@ where
 }
 
 #[repr(simd)]
-#[derive(Clone, Debug)]
+#[derive(Clone, Copy)]
 struct CustomMask<const LANES: usize>([i32; LANES]);
 
 impl<const LANES: usize> kani::Arbitrary for CustomMask<LANES>
diff --git a/tests/kani/SIMD/simd_float_ops.rs b/tests/kani/SIMD/simd_float_ops.rs
index dbb6d77260b6..941b6e1c0538 100644
--- a/tests/kani/SIMD/simd_float_ops.rs
+++ b/tests/kani/SIMD/simd_float_ops.rs
@@ -8,7 +8,7 @@ use std::intrinsics::simd::simd_add;
 use std::simd::f32x4;
 
 #[repr(simd)]
-#[derive(Clone, PartialEq, kani::Arbitrary)]
+#[derive(Copy, Clone, kani::Arbitrary)]
 pub struct f32x2([f32; 2]);
 
 impl f32x2 {
@@ -23,7 +23,7 @@ fn check_sum() {
     let b = kani::any::<f32x2>();
     kani::assume(b.as_array()[0].is_normal());
     kani::assume(b.as_array()[1].is_normal());
-    let sum = unsafe { simd_add(a.clone(), b.clone()) };
+    let sum = unsafe { simd_add(a, b) };
     assert_eq!(sum.as_array(), b.as_array());
 }