diff --git a/kani-compiler/src/kani_middle/transform/loop_contracts.rs b/kani-compiler/src/kani_middle/transform/loop_contracts.rs
index 8ce1b819ac8d..70932fab6d1e 100644
--- a/kani-compiler/src/kani_middle/transform/loop_contracts.rs
+++ b/kani-compiler/src/kani_middle/transform/loop_contracts.rs
@@ -301,10 +301,20 @@ impl LoopContractPass {
             let mut firstprj_nthprj: HashMap<usize, usize> = HashMap::new();
             firstprj_nthprj.insert(firstvar, nthvar);
 
+            // Only user variables (pattern bindings) are paired up with their nthpat
+            // counterparts. Compiler-generated temporaries (e.g. the deref temporaries
+            // that destructuring patterns like `&x` introduce) must not be paired:
+            // their assignments are kept in place (with the rvalue redirected to
+            // nthvar) so that later statements reading them remain well-defined.
+            // Note: before rust-lang/rust#145513 such temporaries were assigned via
+            // `Rvalue::CopyForDeref` and thus never matched the `Rvalue::Use` pattern
+            // below; nowadays they are plain `Rvalue::Use(Operand::Copy)` assignments.
+            let user_vars = self.get_user_defined_variables(body);
             for fstmt in firstprj_stmts_copy.iter() {
                 if let StatementKind::Assign(fprjplace, frval) = &fstmt.kind
                     && let Rvalue::Use(Operand::Copy(firstpatplace)) = frval
                     && firstpatplace.local == firstvar
+                    && user_vars.contains(&fprjplace.local)
                 {
                     let firstprj = fprjplace.local;
                     for istmt in nthprj_stmts_copy.iter() {
@@ -342,17 +352,29 @@ impl LoopContractPass {
                         match frval {
                             Rvalue::Use(Operand::Copy(firstpatplace)) => {
                                 if firstpatplace.local == firstvar {
-                                    let nthprj = firstprj_nthprj.get(&fprjplace.local).unwrap();
                                     let mut nthpatplace = firstpatplace.clone();
                                     nthpatplace.local = nthvar;
                                     let newrval = Rvalue::Use(Operand::Copy(nthpatplace));
-                                    new_stmt.kind = StatementKind::Assign(
-                                        Place {
-                                            local: *nthprj,
-                                            projection: fprjplace.projection.clone(),
-                                        },
-                                        newrval,
-                                    );
+                                    if let Some(nthprj) = firstprj_nthprj.get(&fprjplace.local) {
+                                        // A user pattern binding: redirect the assignment to
+                                        // the corresponding nthpat projection variable.
+                                        new_stmt.kind = StatementKind::Assign(
+                                            Place {
+                                                local: *nthprj,
+                                                projection: fprjplace.projection.clone(),
+                                            },
+                                            newrval,
+                                        );
+                                    } else {
+                                        // A compiler-generated temporary (e.g. a deref
+                                        // temporary, `Rvalue::CopyForDeref` before
+                                        // rust-lang/rust#145513): keep the assigned place and
+                                        // only redirect the rvalue to read from nthvar, so
+                                        // that following statements dereferencing the
+                                        // temporary keep working.
+                                        new_stmt.kind =
+                                            StatementKind::Assign(fprjplace.clone(), newrval);
+                                    }
                                 }
                             }
                             Rvalue::CopyForDeref(firstpatplace) => {
diff --git a/tests/expected/loop-contract/for_loop_ref_pattern.expected b/tests/expected/loop-contract/for_loop_ref_pattern.expected
new file mode 100644
index 000000000000..89aecbbeea58
--- /dev/null
+++ b/tests/expected/loop-contract/for_loop_ref_pattern.expected
@@ -0,0 +1,9 @@
+lookup.loop_invariant_base.1\
+	 - Status: SUCCESS\
+	 - Description: "Check invariant before entry for loop lookup.0"
+
+check_ref_pattern_deref_temp.assertion.1\
+	 - Status: SUCCESS\
+	 - Description: "assertion failed: n <= 2"
+
+VERIFICATION:- SUCCESSFUL
diff --git a/tests/expected/loop-contract/for_loop_ref_pattern.rs b/tests/expected/loop-contract/for_loop_ref_pattern.rs
new file mode 100644
index 000000000000..f6f2f3151bd8
--- /dev/null
+++ b/tests/expected/loop-contract/for_loop_ref_pattern.rs
@@ -0,0 +1,50 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// kani-flags: -Z loop-contracts
+
+//! Check for-loop invariant for a loop whose pattern destructures the
+//! iterator element through a reference, e.g. `for (i, &p) in ...`.
+//! Such patterns introduce compiler-generated deref temporaries in the
+//! pattern-binding block. Those temporaries used to be assigned via
+//! `Rvalue::CopyForDeref`, which rust-lang/rust#145513 turned into plain
+//! copies, and the loop-contract transformation has to keep their
+//! assignments in place instead of treating them like pattern bindings
+//! (see https://github.com/model-checking/kani/issues/4658).
+//! This is a regression test for the spurious "dereference failure"
+//! checks Kani used to emit for this pattern; it is modelled after
+//! `number_of_digits_decimal_left_shift` in the Rust standard library.
+
+#![feature(proc_macro_hygiene)]
+#![feature(stmt_expr_attributes)]
+
+const TABLE: [u8; 16] = [5, 2, 5, 1, 2, 5, 6, 2, 5, 3, 1, 2, 5, 1, 5, 6];
+
+fn lookup(digits: &[u8; 16], num_digits: usize, a: usize, b: usize) -> usize {
+    let num_new_digits: usize = 2;
+    let pow5 = &TABLE[a..];
+
+    #[kani::loop_invariant(num_new_digits > 1)]
+    for (i, &p5) in pow5.iter().enumerate().take(b - a) {
+        if i >= num_digits {
+            return num_new_digits - 1;
+        } else if digits[i] == p5 {
+            continue;
+        } else if digits[i] < p5 {
+            return num_new_digits - 1;
+        } else {
+            return num_new_digits;
+        }
+    }
+    num_new_digits
+}
+
+#[kani::proof]
+fn check_ref_pattern_deref_temp() {
+    let digits: [u8; 16] = kani::any();
+    let num_digits: usize = kani::any_where(|x| *x <= 16);
+    let a: usize = kani::any_where(|x| *x < 8);
+    let b: usize = kani::any_where(|x| *x >= a && *x <= 16);
+    let n = lookup(&digits, num_digits, a, b);
+    assert!(n <= 2);
+}