Coercion support: &[T;N] → &[T] unsize coercion builds length-N slice model

Add PointerCoercion::Unsize arm in rvalue_type(): reads N from the MIR
source type before consuming the operand, then wraps the array place type
in a (Array<Int,T>, N) tuple to produce the slice model with concrete length.

Paired tests: pass accesses index 3 on a 4-element slice (safe), fail
accesses index 4 → Unsat.

https://claude.ai/code/session_01BV92ggaKvAp7oNknvVmGsM

Author: claude

src/analyze/basic_block.rs

@@ -659,6 +659,27 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
                 };
                 PlaceType::with_ty_and_term(func_ty.vacuous(), chc::Term::null())
             }
+            Rvalue::Cast(
+                mir::CastKind::PointerCoercion(mir_ty::adjustment::PointerCoercion::Unsize, _),
+                operand,
+                _ty,
+            ) => {
+                // &[T; N] → &[T]: build the slice model (Array<Int,T>, N).
+                // Read MIR type before consuming operand.
+                let src_mir_ty = operand.ty(&self.local_decls, self.tcx);
+                let mir_ty::TyKind::Ref(_, inner_mir_ty, _) = src_mir_ty.kind() else {
+                    unimplemented!("Unsize coercion of non-reference: {:?}", src_mir_ty)
+                };
+                let mir_ty::TyKind::Array(_, len_const) = inner_mir_ty.kind() else {
+                    unimplemented!("Unsize coercion of non-array reference: {:?}", inner_mir_ty)
+                };
+                let n = len_const
+                    .try_to_target_usize(self.tcx)
+                    .expect("array length must be a known constant");
+                let arr_pty = self.operand_type(operand).deref();
+                let n_pty = PlaceType::with_ty_and_term(rty::Type::int(), chc::Term::int(n as i64));
+                PlaceType::tuple(vec![arr_pty.boxed(), n_pty.boxed()]).immut()
+            }
             Rvalue::Discriminant(place) => {
                 let place = self.elaborate_place(&place);
                 let ty = self.env.place_type(place);

tests/ui/fail/array_literal_2.rs

@@ -0,0 +1,8 @@
+//@error-in-other-file: Unsat
+//@compile-flags: -C debug-assertions=off
+
+fn main() {
+    let arr = [0i32, 0, 0, 0];
+    let s: &[i32] = &arr;
+    let _ = s[4];
+}

tests/ui/pass/array_literal_2.rs

@@ -0,0 +1,8 @@
+//@check-pass
+//@compile-flags: -C debug-assertions=off
+
+fn main() {
+    let arr = [0i32, 0, 0, 0];
+    let s: &[i32] = &arr;
+    let _ = s[3];
+}