Make verify_into_array actually exercise Box::into_array

The previous body called b.try_into(), which goes through the
TryFrom<Box<[T]>> for Box<[T;N]> impl (which uses
boxed_slice_as_array_unchecked, not into_array). The TryFrom path is
already covered separately by verify_try_from_slice_to_array.

Now the harness calls b.into_array() directly and asserts on the
recovered array contents, providing direct coverage of the
Box::<[T]>::into_array spec function (Challenge 29).

Author: Samuelsills

library/alloc/src/boxed.rs

@@ -2305,8 +2305,10 @@ mod verify {
     #[kani::proof]
     fn verify_into_array() {
         let b: Box<[i32]> = Box::from([1, 2, 3]);
-        let r: Result<Box<[i32; 3]>, _> = b.try_into();
-        assert!(r.is_ok());
+        let opt: Option<Box<[i32; 3]>> = b.into_array();
+        assert!(opt.is_some());
+        let arr = opt.unwrap();
+        assert!(arr[0] == 1 && arr[1] == 2 && arr[2] == 3);
     }
 
     #[kani::proof]