From a3e133a2f6576326f1c32bb8fcd8e4c3a3200d8c Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Wed, 30 Sep 2026 22:44:57 +0000
Subject: [PATCH] Support array repeat expressions (`Rvalue::Repeat`)

Type `[x; N]` as a sequence of `N` copies of `x`, expanding it the same
way the array literal arm does. The count must evaluate to a concrete
constant.

Closes #305

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01FWDbM7FpNXVukbHmQcGNoH
---
 src/analyze/basic_block.rs    | 18 ++++++++++++++++++
 tests/ui/fail/array_repeat.rs | 10 ++++++++++
 tests/ui/pass/array_repeat.rs | 10 ++++++++++
 3 files changed, 38 insertions(+)
 create mode 100644 tests/ui/fail/array_repeat.rs
 create mode 100644 tests/ui/pass/array_repeat.rs

diff --git a/src/analyze/basic_block.rs b/src/analyze/basic_block.rs
index 38bba814..97cc7f89 100644
--- a/src/analyze/basic_block.rs
+++ b/src/analyze/basic_block.rs
@@ -731,6 +731,24 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
                     _ => unimplemented!("aggregate kind: {:?}", kind),
                 }
             }
+            Rvalue::Repeat(operand, count) => {
+                // TODO: Stop embedding knowledge of `<[T; N] as Model>::Ty` in the analyzer
+                let count = count
+                    .try_to_target_usize(self.tcx)
+                    .expect("array repeat count must be a known constant");
+                let mir_elem_ty = operand.ty(&self.body.local_decls, self.tcx);
+                let elem_ty = self.type_builder.build(mir_elem_ty).vacuous();
+                let mut builder = PlaceTypeBuilder::default();
+                let (_, elem_term) = builder.subsume(self.operand_type(operand));
+                let mut seq = chc::Term::seq_empty(elem_ty.to_sort());
+                for _ in 0..count {
+                    seq = seq.seq_concat(elem_term.clone().seq_unit());
+                }
+                builder.build(
+                    rty::Type::Seq(Box::new(rty::RefinedType::unrefined(elem_ty))),
+                    seq,
+                )
+            }
             Rvalue::Cast(
                 mir::CastKind::PointerCoercion(
                     mir_ty::adjustment::PointerCoercion::ReifyFnPointer,
diff --git a/tests/ui/fail/array_repeat.rs b/tests/ui/fail/array_repeat.rs
new file mode 100644
index 00000000..f966f528
--- /dev/null
+++ b/tests/ui/fail/array_repeat.rs
@@ -0,0 +1,10 @@
+//@error-in-other-file: Unsat
+//@compile-flags: -C debug-assertions=off
+//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper
+
+fn main() {
+    let arr = [7i32; 4];
+    let s: &[i32] = &arr;
+    assert!(s.len() == 4);
+    assert!(s[3] == 8);
+}
diff --git a/tests/ui/pass/array_repeat.rs b/tests/ui/pass/array_repeat.rs
new file mode 100644
index 00000000..23cb430b
--- /dev/null
+++ b/tests/ui/pass/array_repeat.rs
@@ -0,0 +1,10 @@
+//@check-pass
+//@compile-flags: -C debug-assertions=off
+//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper
+
+fn main() {
+    let arr = [7i32; 4];
+    let s: &[i32] = &arr;
+    assert!(s.len() == 4);
+    assert!(s[3] == 7);
+}