diff --git a/rust-toolchain.toml b/rust-toolchain.toml
index 1177a1ec6809..934515867187 100644
--- a/rust-toolchain.toml
+++ b/rust-toolchain.toml
@@ -2,5 +2,5 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 [toolchain]
-channel = "nightly-2024-09-11"
+channel = "nightly-2024-09-12"
 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 fc710645fd66..28be8e309774 100644
--- a/tests/expected/intrinsics/simd-arith-overflows/main.rs
+++ b/tests/expected/intrinsics/simd-arith-overflows/main.rs
@@ -8,14 +8,14 @@ use std::intrinsics::simd::{simd_add, simd_mul, simd_sub};
 #[repr(simd)]
 #[allow(non_camel_case_types)]
 #[derive(Clone, Copy, PartialEq, Eq, Debug)]
-pub struct i8x2(i8, i8);
+pub struct i8x2([i8; 2]);
 
 #[kani::proof]
 fn main() {
     let a = kani::any();
     let b = kani::any();
-    let simd_a = i8x2(a, a);
-    let simd_b = i8x2(b, b);
+    let simd_a = i8x2([a, a]);
+    let simd_b = i8x2([b, b]);
 
     unsafe {
         let _ = simd_add(simd_a, simd_b);
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 f84cf1d8b9aa..fd4dd40b17b8 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
@@ -9,26 +9,26 @@ use std::intrinsics::simd::simd_eq;
 #[repr(simd)]
 #[allow(non_camel_case_types)]
 #[derive(Clone, Copy, PartialEq, Eq)]
-pub struct i64x2(i64, i64);
+pub struct i64x2([i64; 2]);
 
 #[repr(simd)]
 #[allow(non_camel_case_types)]
 #[derive(Clone, Copy, PartialEq, Eq)]
-pub struct u64x2(u64, u64);
+pub struct u64x2([u64; 2]);
 
 #[repr(simd)]
 #[allow(non_camel_case_types)]
 #[derive(Clone, Copy, PartialEq, Eq)]
-pub struct u32x4(u32, u32, u32, u32);
+pub struct u32x4([u32; 4]);
 
 #[kani::proof]
 fn main() {
-    let x = u64x2(0, 0);
-    let y = u64x2(0, 1);
+    let x = u64x2([0, 0]);
+    let y = u64x2([0, 1]);
 
     unsafe {
         let invalid_simd: u32x4 = simd_eq(x, y);
-        assert!(invalid_simd == u32x4(u32::MAX, u32::MAX, 0, 0));
+        assert!(invalid_simd == u32x4([u32::MAX, u32::MAX, 0, 0]));
         // ^^^^ 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 148ae62a252c..0765e0fd0755 100644
--- a/tests/expected/intrinsics/simd-div-div-zero/main.rs
+++ b/tests/expected/intrinsics/simd-div-div-zero/main.rs
@@ -8,13 +8,13 @@ use std::intrinsics::simd::simd_div;
 #[repr(simd)]
 #[allow(non_camel_case_types)]
 #[derive(Clone, Copy, PartialEq, Eq)]
-pub struct i32x2(i32, i32);
+pub struct i32x2([i32; 2]);
 
 #[kani::proof]
 fn test_simd_div() {
     let dividend = kani::any();
-    let dividends = i32x2(dividend, dividend);
+    let dividends = i32x2([dividend, dividend]);
     let divisor = 0;
-    let divisors = i32x2(divisor, divisor);
+    let divisors = i32x2([divisor, divisor]);
     let _ = unsafe { simd_div(dividends, divisors) };
 }
diff --git a/tests/expected/intrinsics/simd-div-rem-overflow/expected b/tests/expected/intrinsics/simd-div-rem-overflow/expected
index 156854c7dcdc..9c1a0aa96774 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 == quotients.1
+assertion failed: quotients.0[0] == quotients.0[1]
 FAILURE\
 attempt to compute simd_rem which would overflow
 UNREACHABLE\
-assertion failed: remainders.0 == remainders.1
\ No newline at end of file
+assertion failed: remainders.0[0] == remainders.0[1]
\ No newline at end of file
diff --git a/tests/expected/intrinsics/simd-div-rem-overflow/main.rs b/tests/expected/intrinsics/simd-div-rem-overflow/main.rs
index 5f49e7db6154..117fd6bffe95 100644
--- a/tests/expected/intrinsics/simd-div-rem-overflow/main.rs
+++ b/tests/expected/intrinsics/simd-div-rem-overflow/main.rs
@@ -8,7 +8,7 @@ use std::intrinsics::simd::{simd_div, simd_rem};
 #[repr(simd)]
 #[allow(non_camel_case_types)]
 #[derive(Clone, Copy, PartialEq, Eq)]
-pub struct i32x2(i32, i32);
+pub struct i32x2([i32; 2]);
 
 unsafe fn do_simd_div(dividends: i32x2, divisors: i32x2) -> i32x2 {
     simd_div(dividends, divisors)
@@ -21,19 +21,19 @@ unsafe fn do_simd_rem(dividends: i32x2, divisors: i32x2) -> i32x2 {
 #[kani::proof]
 fn test_simd_div_overflow() {
     let dividend = i32::MIN;
-    let dividends = i32x2(dividend, dividend);
+    let dividends = i32x2([dividend, dividend]);
     let divisor = -1;
-    let divisors = i32x2(divisor, divisor);
+    let divisors = i32x2([divisor, divisor]);
     let quotients = unsafe { do_simd_div(dividends, divisors) };
-    assert_eq!(quotients.0, quotients.1);
+    assert_eq!(quotients.0[0], quotients.0[1]);
 }
 
 #[kani::proof]
 fn test_simd_rem_overflow() {
     let dividend = i32::MIN;
-    let dividends = i32x2(dividend, dividend);
+    let dividends = i32x2([dividend, dividend]);
     let divisor = -1;
-    let divisors = i32x2(divisor, divisor);
+    let divisors = i32x2([divisor, divisor]);
     let remainders = unsafe { do_simd_rem(dividends, divisors) };
-    assert_eq!(remainders.0, remainders.1);
+    assert_eq!(remainders.0[0], remainders.0[1]);
 }
diff --git a/tests/expected/intrinsics/simd-extract-wrong-type/main.rs b/tests/expected/intrinsics/simd-extract-wrong-type/main.rs
index b8fb5a3ffc6f..9af6b5279ec6 100644
--- a/tests/expected/intrinsics/simd-extract-wrong-type/main.rs
+++ b/tests/expected/intrinsics/simd-extract-wrong-type/main.rs
@@ -10,11 +10,11 @@ use std::intrinsics::simd::simd_extract;
 #[repr(simd)]
 #[allow(non_camel_case_types)]
 #[derive(Clone, Copy, PartialEq, Eq)]
-pub struct i64x2(i64, i64);
+pub struct i64x2([i64; 2]);
 
 #[kani::proof]
 fn main() {
-    let y = i64x2(0, 1);
+    let y = i64x2([0, 1]);
     let res: i32 = unsafe { simd_extract(y, 1) };
     // ^^^^ The code above fails to type-check in Rust with the error:
     // ```
diff --git a/tests/expected/intrinsics/simd-insert-wrong-type/main.rs b/tests/expected/intrinsics/simd-insert-wrong-type/main.rs
index 6c4946a051b6..8a0853cc7945 100644
--- a/tests/expected/intrinsics/simd-insert-wrong-type/main.rs
+++ b/tests/expected/intrinsics/simd-insert-wrong-type/main.rs
@@ -10,11 +10,11 @@ use std::intrinsics::simd::simd_insert;
 #[repr(simd)]
 #[allow(non_camel_case_types)]
 #[derive(Clone, Copy, PartialEq, Eq)]
-pub struct i64x2(i64, i64);
+pub struct i64x2([i64; 2]);
 
 #[kani::proof]
 fn main() {
-    let y = i64x2(0, 1);
+    let y = i64x2([0, 1]);
     let _ = unsafe { simd_insert(y, 0, 1) };
     // ^^^^ The code above fails to type-check in Rust with the error:
     // ```
diff --git a/tests/expected/intrinsics/simd-rem-div-zero/main.rs b/tests/expected/intrinsics/simd-rem-div-zero/main.rs
index 4393808ac039..7ed9bd2968cd 100644
--- a/tests/expected/intrinsics/simd-rem-div-zero/main.rs
+++ b/tests/expected/intrinsics/simd-rem-div-zero/main.rs
@@ -8,13 +8,13 @@ use std::intrinsics::simd::simd_rem;
 #[repr(simd)]
 #[allow(non_camel_case_types)]
 #[derive(Clone, Copy, PartialEq, Eq)]
-pub struct i32x2(i32, i32);
+pub struct i32x2([i32; 2]);
 
 #[kani::proof]
 fn test_simd_rem() {
     let dividend = kani::any();
-    let dividends = i32x2(dividend, dividend);
+    let dividends = i32x2([dividend, dividend]);
     let divisor = 0;
-    let divisors = i32x2(divisor, divisor);
+    let divisors = i32x2([divisor, divisor]);
     let _ = unsafe { simd_rem(dividends, divisors) };
 }
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 01286de9cdd8..2d7892a1a537 100644
--- a/tests/expected/intrinsics/simd-result-type-is-float/main.rs
+++ b/tests/expected/intrinsics/simd-result-type-is-float/main.rs
@@ -9,31 +9,31 @@ use std::intrinsics::simd::simd_eq;
 #[repr(simd)]
 #[allow(non_camel_case_types)]
 #[derive(Clone, Copy, PartialEq, Eq)]
-pub struct i64x2(i64, i64);
+pub struct i64x2([i64; 2]);
 
 #[repr(simd)]
 #[allow(non_camel_case_types)]
 #[derive(Clone, Copy, PartialEq, Eq)]
-pub struct u64x2(u64, u64);
+pub struct u64x2([u64; 2]);
 
 #[repr(simd)]
 #[allow(non_camel_case_types)]
 #[derive(Clone, Copy, PartialEq, Eq)]
-pub struct u32x4(u32, u32, u32, u32);
+pub struct u32x4([u32; 4]);
 
 #[repr(simd)]
 #[allow(non_camel_case_types)]
 #[derive(Clone, Copy, PartialEq)]
-pub struct f32x2(f32, f32);
+pub struct f32x2([f32; 2]);
 
 #[kani::proof]
 fn main() {
-    let x = u64x2(0, 0);
-    let y = u64x2(0, 1);
+    let x = u64x2([0, 0]);
+    let y = u64x2([0, 1]);
 
     unsafe {
         let invalid_simd: f32x2 = simd_eq(x, y);
-        assert!(invalid_simd == f32x2(0.0, -1.0));
+        assert!(invalid_simd == f32x2([0.0, -1.0]));
         // ^^^^ 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 2b7b2a418e19..f18a9ba14190 100644
--- a/tests/expected/intrinsics/simd-shl-shift-negative/main.rs
+++ b/tests/expected/intrinsics/simd-shl-shift-negative/main.rs
@@ -8,14 +8,14 @@ use std::intrinsics::simd::simd_shl;
 #[repr(simd)]
 #[allow(non_camel_case_types)]
 #[derive(Clone, Copy, PartialEq, Eq)]
-pub struct i32x2(i32, i32);
+pub struct i32x2([i32; 2]);
 
 #[kani::proof]
 fn test_simd_shl() {
     let value = kani::any();
-    let values = i32x2(value, value);
+    let values = i32x2([value, value]);
     let shift = kani::any();
     kani::assume(shift < 32);
-    let shifts = i32x2(shift, shift);
+    let shifts = i32x2([shift, shift]);
     let _result = unsafe { simd_shl(values, shifts) };
 }
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 dada7a5a8b84..75b73a5b81f1 100644
--- a/tests/expected/intrinsics/simd-shl-shift-too-large/main.rs
+++ b/tests/expected/intrinsics/simd-shl-shift-too-large/main.rs
@@ -8,14 +8,14 @@ use std::intrinsics::simd::simd_shl;
 #[repr(simd)]
 #[allow(non_camel_case_types)]
 #[derive(Clone, Copy, PartialEq, Eq)]
-pub struct i32x2(i32, i32);
+pub struct i32x2([i32; 2]);
 
 #[kani::proof]
 fn test_simd_shl() {
     let value = kani::any();
-    let values = i32x2(value, value);
+    let values = i32x2([value, value]);
     let shift = kani::any();
     kani::assume(shift >= 0);
-    let shifts = i32x2(shift, shift);
+    let shifts = i32x2([shift, shift]);
     let _result = unsafe { simd_shl(values, shifts) };
 }
diff --git a/tests/expected/intrinsics/simd-shr-shift-negative/main.rs b/tests/expected/intrinsics/simd-shr-shift-negative/main.rs
index dc38955099a2..f46a91b37c21 100644
--- a/tests/expected/intrinsics/simd-shr-shift-negative/main.rs
+++ b/tests/expected/intrinsics/simd-shr-shift-negative/main.rs
@@ -8,14 +8,14 @@ use std::intrinsics::simd::simd_shr;
 #[repr(simd)]
 #[allow(non_camel_case_types)]
 #[derive(Clone, Copy, PartialEq, Eq)]
-pub struct i32x2(i32, i32);
+pub struct i32x2([i32; 2]);
 
 #[kani::proof]
 fn test_simd_shr() {
     let value = kani::any();
-    let values = i32x2(value, value);
+    let values = i32x2([value, value]);
     let shift = kani::any();
     kani::assume(shift < 32);
-    let shifts = i32x2(shift, shift);
+    let shifts = i32x2([shift, shift]);
     let _result = unsafe { simd_shr(values, shifts) };
 }
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 70ae0ad0da45..cdcfce0cf755 100644
--- a/tests/expected/intrinsics/simd-shr-shift-too-large/main.rs
+++ b/tests/expected/intrinsics/simd-shr-shift-too-large/main.rs
@@ -8,14 +8,14 @@ use std::intrinsics::simd::simd_shr;
 #[repr(simd)]
 #[allow(non_camel_case_types)]
 #[derive(Clone, Copy, PartialEq, Eq)]
-pub struct i32x2(i32, i32);
+pub struct i32x2([i32; 2]);
 
 #[kani::proof]
 fn test_simd_shr() {
     let value = kani::any();
-    let values = i32x2(value, value);
+    let values = i32x2([value, value]);
     let shift = kani::any();
     kani::assume(shift >= 0);
-    let shifts = i32x2(shift, shift);
+    let shifts = i32x2([shift, shift]);
     let _result = unsafe { simd_shr(values, shifts) };
 }
diff --git a/tests/expected/intrinsics/simd-shuffle-indexes-out/main.rs b/tests/expected/intrinsics/simd-shuffle-indexes-out/main.rs
index 0f7c42d2d46c..b89f40369853 100644
--- a/tests/expected/intrinsics/simd-shuffle-indexes-out/main.rs
+++ b/tests/expected/intrinsics/simd-shuffle-indexes-out/main.rs
@@ -9,12 +9,12 @@ use std::intrinsics::simd::simd_shuffle;
 #[repr(simd)]
 #[allow(non_camel_case_types)]
 #[derive(Clone, Copy, PartialEq, Eq)]
-pub struct i64x2(i64, i64);
+pub struct i64x2([i64; 2]);
 
 #[kani::proof]
 fn main() {
-    let y = i64x2(0, 1);
-    let z = i64x2(1, 2);
+    let y = i64x2([0, 1]);
+    let z = i64x2([1, 2]);
     // Only [0, 3] are valid indexes, 4 is out of bounds
     const I: [u32; 2] = [1, 4];
     let _: i64x2 = unsafe { simd_shuffle(y, z, I) };
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 6345f5516101..3fe534f3bc08 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
@@ -9,17 +9,17 @@ use std::intrinsics::simd::simd_shuffle;
 #[repr(simd)]
 #[allow(non_camel_case_types)]
 #[derive(Clone, Copy, PartialEq, Eq)]
-pub struct i64x2(i64, i64);
+pub struct i64x2([i64; 2]);
 
 #[repr(simd)]
 #[allow(non_camel_case_types)]
 #[derive(Clone, Copy, PartialEq, Eq)]
-pub struct i64x4(i64, i64, i64, i64);
+pub struct i64x4([i64; 4]);
 
 #[kani::proof]
 fn main() {
-    let y = i64x2(0, 1);
-    let z = i64x2(1, 2);
+    let y = i64x2([0, 1]);
+    let z = i64x2([1, 2]);
     const I: [u32; 4] = [1, 2, 1, 2];
     let x: i64x2 = unsafe { simd_shuffle(y, z, I) };
     // ^^^^ The code above fails to type-check in Rust with the error:
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 81f176700152..8c7cd5245cbe 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
@@ -9,17 +9,17 @@ use std::intrinsics::simd::simd_shuffle;
 #[repr(simd)]
 #[allow(non_camel_case_types)]
 #[derive(Clone, Copy, PartialEq)]
-pub struct i64x2(i64, i64);
+pub struct i64x2([i64; 2]);
 
 #[repr(simd)]
 #[allow(non_camel_case_types)]
 #[derive(Clone, Copy, PartialEq)]
-pub struct f64x2(f64, f64);
+pub struct f64x2([f64; 2]);
 
 #[kani::proof]
 fn main() {
-    let y = i64x2(0, 1);
-    let z = i64x2(1, 2);
+    let y = i64x2([0, 1]);
+    let z = i64x2([1, 2]);
     const I: [u32; 2] = [1, 2];
     let x: f64x2 = unsafe { simd_shuffle(y, z, I) };
     // ^^^^ The code above fails to type-check in Rust with the error:
diff --git a/tests/kani/Intrinsics/SIMD/Compare/float.rs b/tests/kani/Intrinsics/SIMD/Compare/float.rs
index cc5765ef226b..6c69d142ff7d 100644
--- a/tests/kani/Intrinsics/SIMD/Compare/float.rs
+++ b/tests/kani/Intrinsics/SIMD/Compare/float.rs
@@ -8,17 +8,17 @@ use std::intrinsics::simd::*;
 #[repr(simd)]
 #[allow(non_camel_case_types)]
 #[derive(Clone, Copy, PartialEq)]
-pub struct f64x2(f64, f64);
+pub struct f64x2([f64; 2]);
 
 #[repr(simd)]
 #[allow(non_camel_case_types)]
 #[derive(Clone, Copy, PartialEq)]
-pub struct i64x2(i64, i64);
+pub struct i64x2([i64; 2]);
 
 #[repr(simd)]
 #[allow(non_camel_case_types)]
 #[derive(Clone, Copy, PartialEq)]
-pub struct i32x2(i32, i32);
+pub struct i32x2([i32; 2]);
 
 macro_rules! assert_cmp {
     ($res_cmp: ident, $simd_cmp: ident, $x: expr, $y: expr, $($res: expr),+) => {
@@ -29,21 +29,21 @@ macro_rules! assert_cmp {
 
 #[kani::proof]
 fn main() {
-    let x = f64x2(0.0, 0.0);
-    let y = f64x2(0.0, 1.0);
+    let x = f64x2([0.0, 0.0]);
+    let y = f64x2([0.0, 1.0]);
 
     unsafe {
-        assert_cmp!(res_eq, simd_eq, x, x, -1, -1);
-        assert_cmp!(res_eq, simd_eq, x, y, -1, 0);
-        assert_cmp!(res_ne, simd_ne, x, x, 0, 0);
-        assert_cmp!(res_ne, simd_ne, x, y, 0, -1);
-        assert_cmp!(res_lt, simd_lt, x, x, 0, 0);
-        assert_cmp!(res_lt, simd_lt, x, y, 0, -1);
-        assert_cmp!(res_le, simd_le, x, x, -1, -1);
-        assert_cmp!(res_le, simd_le, x, y, -1, -1);
-        assert_cmp!(res_gt, simd_gt, x, x, 0, 0);
-        assert_cmp!(res_gt, simd_gt, x, y, 0, 0);
-        assert_cmp!(res_ge, simd_ge, x, x, -1, -1);
-        assert_cmp!(res_ge, simd_ge, x, y, -1, 0);
+        assert_cmp!(res_eq, simd_eq, x, x, [-1, -1]);
+        assert_cmp!(res_eq, simd_eq, x, y, [-1, 0]);
+        assert_cmp!(res_ne, simd_ne, x, x, [0, 0]);
+        assert_cmp!(res_ne, simd_ne, x, y, [0, -1]);
+        assert_cmp!(res_lt, simd_lt, x, x, [0, 0]);
+        assert_cmp!(res_lt, simd_lt, x, y, [0, -1]);
+        assert_cmp!(res_le, simd_le, x, x, [-1, -1]);
+        assert_cmp!(res_le, simd_le, x, y, [-1, -1]);
+        assert_cmp!(res_gt, simd_gt, x, x, [0, 0]);
+        assert_cmp!(res_gt, simd_gt, x, y, [0, 0]);
+        assert_cmp!(res_ge, simd_ge, x, x, [-1, -1]);
+        assert_cmp!(res_ge, simd_ge, x, y, [-1, 0]);
     }
 }
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 d3582057fd00..584a5e07876a 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
@@ -9,28 +9,28 @@ use std::intrinsics::simd::simd_eq;
 #[repr(simd)]
 #[allow(non_camel_case_types)]
 #[derive(Clone, Copy, PartialEq, Eq)]
-pub struct i64x2(i64, i64);
+pub struct i64x2([i64; 2]);
 
 #[repr(simd)]
 #[allow(non_camel_case_types)]
 #[derive(Clone, Copy, PartialEq, Eq)]
-pub struct u64x2(u64, u64);
+pub struct u64x2([u64; 2]);
 
 #[repr(simd)]
 #[allow(non_camel_case_types)]
 #[derive(Clone, Copy, PartialEq, Eq)]
-pub struct u32x2(u32, u32);
+pub struct u32x2([u32; 2]);
 
 #[kani::proof]
 fn main() {
-    let x = u64x2(0, 0);
-    let y = u64x2(0, 1);
+    let x = u64x2([0, 0]);
+    let y = u64x2([0, 1]);
 
     unsafe {
         let w: i64x2 = simd_eq(x, y);
-        assert!(w == i64x2(-1, 0));
+        assert!(w == i64x2([-1, 0]));
 
         let z: u32x2 = simd_eq(x, y);
-        assert!(z == u32x2(u32::MAX, 0));
+        assert!(z == u32x2([u32::MAX, 0]));
     }
 }
diff --git a/tests/kani/Intrinsics/SIMD/Compare/signed.rs b/tests/kani/Intrinsics/SIMD/Compare/signed.rs
index cfd781fa64c7..671078bad2d4 100644
--- a/tests/kani/Intrinsics/SIMD/Compare/signed.rs
+++ b/tests/kani/Intrinsics/SIMD/Compare/signed.rs
@@ -8,7 +8,7 @@ use std::intrinsics::simd::*;
 #[repr(simd)]
 #[allow(non_camel_case_types)]
 #[derive(Clone, Copy, PartialEq, Eq)]
-pub struct i64x2(i64, i64);
+pub struct i64x2([i64; 2]);
 
 macro_rules! assert_cmp {
     ($res_cmp: ident, $simd_cmp: ident, $x: expr, $y: expr, $($res: expr),+) => {
@@ -23,21 +23,21 @@ macro_rules! assert_cmp {
 //  * No bits set (e.g., 0 in signed integers) if the result is true
 #[kani::proof]
 fn main() {
-    let x = i64x2(0, 0);
-    let y = i64x2(0, 1);
+    let x = i64x2([0, 0]);
+    let y = i64x2([0, 1]);
 
     unsafe {
-        assert_cmp!(res_eq, simd_eq, x, x, -1, -1);
-        assert_cmp!(res_eq, simd_eq, x, y, -1, 0);
-        assert_cmp!(res_ne, simd_ne, x, x, 0, 0);
-        assert_cmp!(res_ne, simd_ne, x, y, 0, -1);
-        assert_cmp!(res_lt, simd_lt, x, x, 0, 0);
-        assert_cmp!(res_lt, simd_lt, x, y, 0, -1);
-        assert_cmp!(res_le, simd_le, x, x, -1, -1);
-        assert_cmp!(res_le, simd_le, x, y, -1, -1);
-        assert_cmp!(res_gt, simd_gt, x, x, 0, 0);
-        assert_cmp!(res_gt, simd_gt, x, y, 0, 0);
-        assert_cmp!(res_ge, simd_ge, x, x, -1, -1);
-        assert_cmp!(res_ge, simd_ge, x, y, -1, 0);
+        assert_cmp!(res_eq, simd_eq, x, x, [-1, -1]);
+        assert_cmp!(res_eq, simd_eq, x, y, [-1, 0]);
+        assert_cmp!(res_ne, simd_ne, x, x, [0, 0]);
+        assert_cmp!(res_ne, simd_ne, x, y, [0, -1]);
+        assert_cmp!(res_lt, simd_lt, x, x, [0, 0]);
+        assert_cmp!(res_lt, simd_lt, x, y, [0, -1]);
+        assert_cmp!(res_le, simd_le, x, x, [-1, -1]);
+        assert_cmp!(res_le, simd_le, x, y, [-1, -1]);
+        assert_cmp!(res_gt, simd_gt, x, x, [0, 0]);
+        assert_cmp!(res_gt, simd_gt, x, y, [0, 0]);
+        assert_cmp!(res_ge, simd_ge, x, x, [-1, -1]);
+        assert_cmp!(res_ge, simd_ge, x, y, [-1, 0]);
     }
 }
diff --git a/tests/kani/Intrinsics/SIMD/Compare/unsigned.rs b/tests/kani/Intrinsics/SIMD/Compare/unsigned.rs
index ee39f750c8a2..b2943b36ab71 100644
--- a/tests/kani/Intrinsics/SIMD/Compare/unsigned.rs
+++ b/tests/kani/Intrinsics/SIMD/Compare/unsigned.rs
@@ -8,7 +8,7 @@ use std::intrinsics::simd::*;
 #[repr(simd)]
 #[allow(non_camel_case_types)]
 #[derive(Clone, Copy, PartialEq, Eq)]
-pub struct u64x2(u64, u64);
+pub struct u64x2([u64; 2]);
 
 macro_rules! assert_cmp {
     ($res_cmp: ident, $simd_cmp: ident, $x: expr, $y: expr, $($res: expr),+) => {
@@ -23,21 +23,21 @@ macro_rules! assert_cmp {
 //  * No bits set (e.g., 0 in signed integers) if the result is true
 #[kani::proof]
 fn main() {
-    let x = u64x2(0, 0);
-    let y = u64x2(0, 1);
+    let x = u64x2([0, 0]);
+    let y = u64x2([0, 1]);
 
     unsafe {
-        assert_cmp!(res_eq, simd_eq, x, x, u64::MAX, u64::MAX);
-        assert_cmp!(res_eq, simd_eq, x, y, u64::MAX, 0);
-        assert_cmp!(res_ne, simd_ne, x, x, 0, 0);
-        assert_cmp!(res_ne, simd_ne, x, y, 0, u64::MAX);
-        assert_cmp!(res_lt, simd_lt, x, x, 0, 0);
-        assert_cmp!(res_lt, simd_lt, x, y, 0, u64::MAX);
-        assert_cmp!(res_le, simd_le, x, x, u64::MAX, u64::MAX);
-        assert_cmp!(res_le, simd_le, x, y, u64::MAX, u64::MAX);
-        assert_cmp!(res_gt, simd_gt, x, x, 0, 0);
-        assert_cmp!(res_gt, simd_gt, x, y, 0, 0);
-        assert_cmp!(res_ge, simd_ge, x, x, u64::MAX, u64::MAX);
-        assert_cmp!(res_ge, simd_ge, x, y, u64::MAX, 0);
+        assert_cmp!(res_eq, simd_eq, x, x, [u64::MAX, u64::MAX]);
+        assert_cmp!(res_eq, simd_eq, x, y, [u64::MAX, 0]);
+        assert_cmp!(res_ne, simd_ne, x, x, [0, 0]);
+        assert_cmp!(res_ne, simd_ne, x, y, [0, u64::MAX]);
+        assert_cmp!(res_lt, simd_lt, x, x, [0, 0]);
+        assert_cmp!(res_lt, simd_lt, x, y, [0, u64::MAX]);
+        assert_cmp!(res_le, simd_le, x, x, [u64::MAX, u64::MAX]);
+        assert_cmp!(res_le, simd_le, x, y, [u64::MAX, u64::MAX]);
+        assert_cmp!(res_gt, simd_gt, x, x, [0, 0]);
+        assert_cmp!(res_gt, simd_gt, x, y, [0, 0]);
+        assert_cmp!(res_ge, simd_ge, x, x, [u64::MAX, u64::MAX]);
+        assert_cmp!(res_ge, simd_ge, x, y, [u64::MAX, 0]);
     }
 }
diff --git a/tests/kani/Intrinsics/SIMD/Construction/main.rs b/tests/kani/Intrinsics/SIMD/Construction/main.rs
index 5de3ae20d868..92c5a167dc15 100644
--- a/tests/kani/Intrinsics/SIMD/Construction/main.rs
+++ b/tests/kani/Intrinsics/SIMD/Construction/main.rs
@@ -9,16 +9,16 @@ use std::intrinsics::simd::{simd_extract, simd_insert};
 #[repr(simd)]
 #[allow(non_camel_case_types)]
 #[derive(Clone, Copy, PartialEq, Eq)]
-pub struct i64x2(i64, i64);
+pub struct i64x2([i64; 2]);
 
 #[kani::proof]
 fn main() {
-    let y = i64x2(0, 1);
-    let z = i64x2(1, 2);
+    let y = i64x2([0, 1]);
+    let z = i64x2([1, 2]);
 
     // Indexing into the vectors
-    assert!(z.0 == 1);
-    assert!(z.1 == 2);
+    assert!(z.0[0] == 1);
+    assert!(z.0[1] == 2);
 
     {
         // Intrinsic indexing
@@ -31,9 +31,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 == 1 && m.1 == 1);
-        assert!(n.0 == 0 && n.1 == 5);
+        assert!(m.0[0] == 1 && m.0[1] == 1);
+        assert!(n.0[0] == 0 && n.0[1] == 5);
         // Original unchanged
-        assert!(y.0 == 0 && y.1 == 1);
+        assert!(y.0[0] == 0 && y.0[1] == 1);
     }
 }
diff --git a/tests/kani/Intrinsics/SIMD/Operators/arith.rs b/tests/kani/Intrinsics/SIMD/Operators/arith.rs
index d9f442a659ba..33a8ba65b538 100644
--- a/tests/kani/Intrinsics/SIMD/Operators/arith.rs
+++ b/tests/kani/Intrinsics/SIMD/Operators/arith.rs
@@ -9,7 +9,7 @@ use std::intrinsics::simd::{simd_add, simd_mul, simd_sub};
 #[repr(simd)]
 #[allow(non_camel_case_types)]
 #[derive(Clone, Copy, PartialEq, Eq)]
-pub struct i8x2(i8, i8);
+pub struct i8x2([i8; 2]);
 
 macro_rules! verify_no_overflow {
     ($cf: ident, $uf: ident) => {{
@@ -17,11 +17,11 @@ macro_rules! verify_no_overflow {
         let b: i8 = kani::any();
         let checked = a.$cf(b);
         kani::assume(checked.is_some());
-        let simd_a = i8x2(a, a);
-        let simd_b = i8x2(b, b);
+        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);
-        assert!(checked.unwrap() == unchecked.1);
+        assert!(checked.unwrap() == unchecked.0[0]);
+        assert!(checked.unwrap() == unchecked.0[1]);
     }};
 }
 
diff --git a/tests/kani/Intrinsics/SIMD/Operators/bitshift.rs b/tests/kani/Intrinsics/SIMD/Operators/bitshift.rs
index fa2cd3c52cd6..09a19fa7b29a 100644
--- a/tests/kani/Intrinsics/SIMD/Operators/bitshift.rs
+++ b/tests/kani/Intrinsics/SIMD/Operators/bitshift.rs
@@ -9,47 +9,47 @@ use std::intrinsics::simd::{simd_shl, simd_shr};
 #[repr(simd)]
 #[allow(non_camel_case_types)]
 #[derive(Clone, Copy, PartialEq, Eq)]
-pub struct i32x2(i32, i32);
+pub struct i32x2([i32; 2]);
 
 #[repr(simd)]
 #[allow(non_camel_case_types)]
 #[derive(Clone, Copy, PartialEq, Eq)]
-pub struct u32x2(u32, u32);
+pub struct u32x2([u32; 2]);
 
 #[kani::proof]
 fn test_simd_shl() {
     let value = kani::any();
-    let values = i32x2(value, value);
+    let values = i32x2([value, value]);
     let shift = kani::any();
     kani::assume(shift >= 0);
     kani::assume(shift < 32);
-    let shifts = i32x2(shift, shift);
+    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);
+    assert_eq!(normal_result, simd_result.0[0]);
 }
 
 #[kani::proof]
 fn test_simd_shr_signed() {
     let value = kani::any();
-    let values = i32x2(value, value);
+    let values = i32x2([value, value]);
     let shift = kani::any();
     kani::assume(shift >= 0);
     kani::assume(shift < 32);
-    let shifts = i32x2(shift, shift);
+    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);
+    assert_eq!(normal_result, simd_result.0[0]);
 }
 
 #[kani::proof]
 fn test_simd_shr_unsigned() {
     let value = kani::any();
-    let values = u32x2(value, value);
+    let values = u32x2([value, value]);
     let shift = kani::any();
     kani::assume(shift < 32);
-    let shifts = u32x2(shift, shift);
+    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);
+    assert_eq!(normal_result, simd_result.0[0]);
 }
diff --git a/tests/kani/Intrinsics/SIMD/Operators/bitwise.rs b/tests/kani/Intrinsics/SIMD/Operators/bitwise.rs
index b18410088f18..a9aaa96f75e5 100644
--- a/tests/kani/Intrinsics/SIMD/Operators/bitwise.rs
+++ b/tests/kani/Intrinsics/SIMD/Operators/bitwise.rs
@@ -14,52 +14,52 @@ use std::intrinsics::simd::{simd_and, simd_or, simd_xor};
 #[repr(simd)]
 #[allow(non_camel_case_types)]
 #[derive(Clone, Copy, PartialEq, Eq)]
-pub struct i8x2(i8, i8);
+pub struct i8x2([i8; 2]);
 
 #[repr(simd)]
 #[allow(non_camel_case_types)]
 #[derive(Clone, Copy, PartialEq, Eq)]
-pub struct i16x2(i16, i16);
+pub struct i16x2([i16; 2]);
 
 #[repr(simd)]
 #[allow(non_camel_case_types)]
 #[derive(Clone, Copy, PartialEq, Eq)]
-pub struct i32x2(i32, i32);
+pub struct i32x2([i32; 2]);
 
 #[repr(simd)]
 #[allow(non_camel_case_types)]
 #[derive(Clone, Copy, PartialEq, Eq)]
-pub struct i64x2(i64, i64);
+pub struct i64x2([i64; 2]);
 
 #[repr(simd)]
 #[allow(non_camel_case_types)]
 #[derive(Clone, Copy, PartialEq, Eq)]
-pub struct u8x2(u8, u8);
+pub struct u8x2([u8; 2]);
 
 #[repr(simd)]
 #[allow(non_camel_case_types)]
 #[derive(Clone, Copy, PartialEq, Eq)]
-pub struct u16x2(u16, u16);
+pub struct u16x2([u16; 2]);
 
 #[repr(simd)]
 #[allow(non_camel_case_types)]
 #[derive(Clone, Copy, PartialEq, Eq)]
-pub struct u32x2(u32, u32);
+pub struct u32x2([u32; 2]);
 
 #[repr(simd)]
 #[allow(non_camel_case_types)]
 #[derive(Clone, Copy, PartialEq, Eq)]
-pub struct u64x2(u64, u64);
+pub struct u64x2([u64; 2]);
 
 macro_rules! compare_simd_op_with_normal_op {
     ($simd_op: ident, $normal_op: tt, $simd_type: ident) => {
         let tup_x: (_,_) = kani::any();
         let tup_y: (_,_) = kani::any();
-        let x = $simd_type(tup_x.0, tup_x.1);
-        let y = $simd_type(tup_y.0, tup_y.1);
+        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);
-        assert_eq!(tup_x.1 $normal_op tup_y.1, res_and.1);
+        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]);
     };
 }
 
diff --git a/tests/kani/Intrinsics/SIMD/Operators/division.rs b/tests/kani/Intrinsics/SIMD/Operators/division.rs
index e1e8dab39cca..d48968342ca4 100644
--- a/tests/kani/Intrinsics/SIMD/Operators/division.rs
+++ b/tests/kani/Intrinsics/SIMD/Operators/division.rs
@@ -9,32 +9,32 @@ use std::intrinsics::simd::{simd_div, simd_rem};
 #[repr(simd)]
 #[allow(non_camel_case_types)]
 #[derive(Clone, Copy, PartialEq, Eq)]
-pub struct i32x2(i32, i32);
+pub struct i32x2([i32; 2]);
 
 #[kani::proof]
 fn test_simd_div() {
     let dividend = kani::any();
-    let dividends = i32x2(dividend, dividend);
+    let dividends = i32x2([dividend, dividend]);
     let divisor = kani::any();
     // Narrow down the divisor interval so the operation doesn't overflow and
     // the test finishes in a short time
     kani::assume(divisor > 0 && divisor < 5);
-    let divisors = i32x2(divisor, divisor);
+    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);
+    assert_eq!(normal_result, simd_result.0[0]);
 }
 
 #[kani::proof]
 fn test_simd_rem() {
     let dividend = kani::any();
-    let dividends = i32x2(dividend, dividend);
+    let dividends = i32x2([dividend, dividend]);
     let divisor = kani::any();
     // Narrow down the divisor interval so the operation doesn't overflow and
     // the test finishes in a short time
     kani::assume(divisor > 0 && divisor < 5);
-    let divisors = i32x2(divisor, divisor);
+    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);
+    assert_eq!(normal_result, simd_result.0[0]);
 }
diff --git a/tests/kani/Intrinsics/SIMD/Operators/division_float.rs b/tests/kani/Intrinsics/SIMD/Operators/division_float.rs
index 711b67b87116..d61bd81f1f87 100644
--- a/tests/kani/Intrinsics/SIMD/Operators/division_float.rs
+++ b/tests/kani/Intrinsics/SIMD/Operators/division_float.rs
@@ -8,15 +8,15 @@ use std::intrinsics::simd::simd_div;
 #[repr(simd)]
 #[allow(non_camel_case_types)]
 #[derive(Clone, Copy, PartialEq, kani::Arbitrary)]
-pub struct f32x2(f32, f32);
+pub struct f32x2([f32; 2]);
 
 impl f32x2 {
     fn new_with(f: impl Fn() -> f32) -> Self {
-        f32x2(f(), f())
+        f32x2([f(), f()])
     }
 
     fn non_simd_div(self, divisors: Self) -> Self {
-        f32x2(self.0 / divisors.0, self.1 / divisors.1)
+        f32x2([self.0[0] / divisors.0[0], self.0[1] / divisors.0[1]])
     }
 }
 
diff --git a/tests/kani/Intrinsics/SIMD/Shuffle/main.rs b/tests/kani/Intrinsics/SIMD/Shuffle/main.rs
index 9b6870e40004..a105a3b1d81e 100644
--- a/tests/kani/Intrinsics/SIMD/Shuffle/main.rs
+++ b/tests/kani/Intrinsics/SIMD/Shuffle/main.rs
@@ -9,45 +9,45 @@ use std::intrinsics::simd::simd_shuffle;
 #[repr(simd)]
 #[allow(non_camel_case_types)]
 #[derive(Clone, Copy, PartialEq, Eq)]
-pub struct i64x2(i64, i64);
+pub struct i64x2([i64; 2]);
 
 #[repr(simd)]
 #[allow(non_camel_case_types)]
 #[derive(Clone, Copy, PartialEq, Eq)]
-pub struct i64x4(i64, i64, i64, i64);
+pub struct i64x4([i64; 4]);
 
 #[kani::proof]
 fn main() {
     {
-        let y = i64x2(0, 1);
-        let z = i64x2(1, 2);
+        let y = i64x2([0, 1]);
+        let z = i64x2([1, 2]);
         const I: [u32; 2] = [1, 2];
         let x: i64x2 = unsafe { simd_shuffle(y, z, I) };
-        assert!(x.0 == 1);
-        assert!(x.1 == 1);
+        assert!(x.0[0] == 1);
+        assert!(x.0[1] == 1);
     }
     {
-        let y = i64x2(0, 1);
-        let z = i64x2(1, 2);
+        let y = i64x2([0, 1]);
+        let z = i64x2([1, 2]);
         const I: [u32; 2] = [1, 2];
         let x: i64x2 = unsafe { simd_shuffle(y, z, I) };
-        assert!(x.0 == 1);
-        assert!(x.1 == 1);
+        assert!(x.0[0] == 1);
+        assert!(x.0[1] == 1);
     }
     {
-        let a = i64x4(1, 2, 3, 4);
-        let b = i64x4(5, 6, 7, 8);
+        let a = i64x4([1, 2, 3, 4]);
+        let b = i64x4([5, 6, 7, 8]);
         const I: [u32; 4] = [1, 3, 5, 7];
         let c: i64x4 = unsafe { simd_shuffle(a, b, I) };
-        assert!(c == i64x4(2, 4, 6, 8));
+        assert!(c == i64x4([2, 4, 6, 8]));
     }
 }
 
 #[kani::proof]
 fn check_shuffle() {
     {
-        let y = i64x2(0, 1);
-        let z = i64x2(1, 2);
+        let y = i64x2([0, 1]);
+        let z = i64x2([1, 2]);
         const I: [u32; 4] = [1, 2, 0, 3];
         let _x: i64x4 = unsafe { simd_shuffle(y, z, I) };
     }
diff --git a/tests/kani/SIMD/generic_access.rs b/tests/kani/SIMD/generic_access.rs
index 280175a781c6..805eeaa403ea 100644
--- a/tests/kani/SIMD/generic_access.rs
+++ b/tests/kani/SIMD/generic_access.rs
@@ -31,20 +31,20 @@ mod fields_based {
     use super::*;
 
     #[repr(simd)]
-    struct CustomSimd<T: SimdElement>(T, T);
+    struct CustomSimd<T: SimdElement>([T; 2]);
 
     fn check_fields<T: SimdElement + PartialEq, const LANES: usize>(
         simd: CustomSimd<T>,
         expected: [T; LANES],
     ) {
-        assert_eq!(simd.0, expected[0]);
-        assert_eq!(simd.1, expected[1])
+        assert_eq!(simd.0[0], expected[0]);
+        assert_eq!(simd.0[1], expected[1])
     }
 
     #[kani::proof]
     fn check_field_access() {
         let data: [u8; 16] = kani::any();
-        let vec = CustomSimd(data[0], data[1]);
+        let vec = CustomSimd([data[0], data[1]]);
         check_fields(vec, data);
     }
 }
diff --git a/tests/kani/SIMD/multi_field_simd.rs b/tests/kani/SIMD/multi_field_simd.rs
index d54cf1a07bdb..c8cdd848c69e 100644
--- a/tests/kani/SIMD/multi_field_simd.rs
+++ b/tests/kani/SIMD/multi_field_simd.rs
@@ -10,19 +10,19 @@
 
 #[repr(simd)]
 #[derive(PartialEq, Eq, PartialOrd, kani::Arbitrary)]
-pub struct i64x2(i64, i64);
+pub struct i64x2([i64; 2]);
 
 #[kani::proof]
 fn check_diff() {
-    let x = i64x2(1, 2);
-    let y = i64x2(3, 4);
+    let x = i64x2([1, 2]);
+    let y = i64x2([3, 4]);
     assert!(x != y);
 }
 
 #[kani::proof]
 fn check_ge() {
     let x: i64x2 = kani::any();
-    kani::assume(x.0 > 0);
-    kani::assume(x.1 > 0);
-    assert!(x > i64x2(0, 0));
+    kani::assume(x.0[0] > 0);
+    kani::assume(x.0[1] > 0);
+    assert!(x > i64x2([0, 0]));
 }