Add a new test that narrow down the issue

My current hypothesis is that this could be an issue with simd_shuffle

tests/kani/SIMD/portable_simd.rs

@@ -4,7 +4,7 @@
 //! Ensure we have basic support of portable SIMD.
 #![feature(portable_simd)]
 
-use std::simd::{mask32x4, u64x16};
+use std::simd::{mask32x4, u32x4, u64x16};
 
 #[kani::proof]
 fn check_sum_any() {
@@ -23,3 +23,11 @@ fn check_mask() {
     let bitmask = mask.to_bitmask();
     assert_eq!(bitmask, 0b1010);
 }
+
+#[kani::proof]
+fn check_resize() {
+    let x = u32x4::from_array([0, 1, 2, 3]);
+    assert_eq!(x.resize::<8>(9).to_array(), [0, 1, 2, 3, 9, 9, 9, 9]);
+    assert_eq!(x.resize::<2>(9).to_array(), [0, 1]);
+
+}