diff --git a/compiler/noirc_evaluator/src/ssa/validation/rc_invariant/call.rs b/compiler/noirc_evaluator/src/ssa/validation/rc_invariant/call.rs
index 2dbbc9ac06f..589b72f7f7b 100644
--- a/compiler/noirc_evaluator/src/ssa/validation/rc_invariant/call.rs
+++ b/compiler/noirc_evaluator/src/ssa/validation/rc_invariant/call.rs
@@ -11,6 +11,10 @@
 //! [`super::array_set`], seeded from call arguments instead of `array_set`
 //! sources, and gated on whether the callee can modify its arguments (mirroring
 //! `can_modify_args` in `ssa_gen`).
+//!
+//! It additionally checks a relation only visible at the call site: whether two
+//! argument positions of one call denote the same storage with no protecting
+//! `inc_rc` (see [`check_co_aliased_arguments`]).
 
 use rustc_hash::{FxHashMap as HashMap, FxHashSet as HashSet};
 
@@ -20,7 +24,8 @@ use crate::{
         ir::{
             basic_block::BasicBlockId,
             function::{Function, FunctionId},
-            instruction::{Instruction, Intrinsic, TerminatorInstruction},
+            instruction::{Instruction, InstructionId, Intrinsic, TerminatorInstruction},
+            types::Type,
             value::{Value, ValueId},
         },
         opt::pure::Purity,
@@ -126,11 +131,114 @@ fn verify_function(function: &Function, needs_check: &impl Fn(FunctionId) -> boo
                         .get_instruction_call_stack(hit.instruction),
                 });
             }
+
+            check_co_aliased_arguments(function, &ctx, arguments, block_id, idx, instruction_id)?;
+        }
+    }
+    Ok(())
+}
+
+/// Reject a `call` in which two argument positions may denote the same array
+/// storage with no protecting `inc_rc`.
+///
+/// The per-argument forward walk in [`verify_function`] looks for an aliased
+/// read *in the caller, after the call*, so it cannot see the hazard where the
+/// same buffer reaches the callee twice — as the same value in two positions
+/// (`f(v, v)`), or once as an array value and once as the pointee of a
+/// reference (the shape `ssa_gen` emits for `f(&mut x, x)`). The callee can
+/// then mutate one handle in place at reference count 1 and observe (e.g.
+/// return) the pre-mutation contents through the other, entirely inside the
+/// callee — where the two parameters are unrelated values and the shared-buffer
+/// relation is invisible to the intraprocedural alias engine. The relation is
+/// only established here, at the call site, so this is where it must be checked
+/// (noir-lang/noir-claude#1563).
+///
+/// Each argument position is resolved to the storage it denotes at the call:
+/// an array-typed argument to itself, and a reference argument to the value
+/// its in-block reaching `store` wrote, when there is one (after
+/// `mem2reg_brillig` the emitted shape keeps that `store` in the call's own
+/// block; a pointee established elsewhere is not traced — a false negative,
+/// never a false positive). Two *reference* arguments sharing a pointee are
+/// not flagged: a write through a reference is ordinary reference semantics,
+/// visible through every alias of the reference by design, not a copy-on-write
+/// violation — so a pair must include at least one array-value position.
+///
+/// Whether a pair denotes one buffer, and whether that buffer is protected, is
+/// decided per path by [`Context::pair_has_unprotected_shared_storage`]: a
+/// pair is flagged only when some backward path resolves both positions to the
+/// same storage with no `inc_rc` crossed on it. A whole-call relation is not
+/// path-sensitive enough — a branch-local `inc_rc` protecting the only sharing
+/// path, or two branches passing one buffer through *different* positions,
+/// must both be accepted.
+fn check_co_aliased_arguments(
+    function: &Function,
+    ctx: &Context,
+    arguments: &[ValueId],
+    block_id: BasicBlockId,
+    call_idx: usize,
+    call_id: InstructionId,
+) -> RtResult<()> {
+    // For each argument position: `is_value` (an array value, as opposed to a
+    // reference whose pointee was resolved) and the storage the position
+    // denotes. `None` when the position denotes no array storage we can
+    // resolve.
+    let storages: Vec<Option<(bool, ValueId)>> = arguments
+        .iter()
+        .map(|&arg| match function.dfg.type_of_value(arg).as_ref() {
+            typ if typ.is_array() => Some((true, arg)),
+            Type::Reference(element, _) if element.contains_an_array() => {
+                let pointee = in_block_reaching_store(function, block_id, call_idx, arg)?;
+                Some((false, pointee))
+            }
+            _ => None,
+        })
+        .collect();
+
+    for (i, i_storage) in storages.iter().enumerate() {
+        let Some((i_is_value, i_value)) = i_storage else { continue };
+        for (j, j_storage) in storages.iter().enumerate().skip(i + 1) {
+            let Some((j_is_value, j_value)) = j_storage else { continue };
+            if !i_is_value && !j_is_value {
+                continue;
+            }
+            if !ctx.pair_has_unprotected_shared_storage(*i_value, *j_value, block_id, call_idx) {
+                continue;
+            }
+            let message = format!(
+                "call in function {} passes the same array storage through two arguments \
+                 ({} and {}) with no preceding `inc_rc`; if the callee mutates it in place \
+                 through one of them, the mutation would be observable through the other",
+                function.name(),
+                arguments[i],
+                arguments[j],
+            );
+            let call_stack = function.dfg.get_instruction_call_stack(call_id);
+            return Err(RuntimeError::CallArgAliasViolation {
+                message,
+                call_stack: call_stack.clone(),
+                aliased_use_call_stack: call_stack,
+            });
         }
     }
     Ok(())
 }
 
+/// The value most recently stored through `address` in `block_id` before the
+/// instruction at `call_idx` — the reference's in-block reaching definition —
+/// or `None` when the block contains no such store.
+fn in_block_reaching_store(
+    function: &Function,
+    block_id: BasicBlockId,
+    call_idx: usize,
+    address: ValueId,
+) -> Option<ValueId> {
+    let instructions = function.dfg[block_id].instructions();
+    instructions[..call_idx].iter().rev().find_map(|id| match &function.dfg[*id] {
+        Instruction::Store { address: a, value } if *a == address => Some(*value),
+        _ => None,
+    })
+}
+
 /// Whether a call to the callee referenced by `func` needs its array arguments
 /// checked — i.e. the callee may mutate an argument in place or return an alias
 /// of one. Mirrors `ssa_gen`'s `can_modify_args`: foreign calls only read their
@@ -692,4 +800,207 @@ mod tests {
             "a scalar store cannot mutate an array argument, so the reused arg is not a hazard",
         );
     }
+
+    /// Regression for noir-lang/noir-claude#1563. The same buffer reaches the
+    /// callee through **two argument positions of one call**: `v1` is a `&mut`
+    /// reference whose pointee (the dominating `store v0 at v1`) is also passed
+    /// by value as the second argument, with no `inc_rc` protecting it. The
+    /// callee mutates the buffer in place through the reference (RC is 1) and
+    /// returns its by-value parameter, so the pre-mutation snapshot the
+    /// by-value argument is supposed to be is observably corrupted — running
+    /// this SSA yields `([9,2], [9,2])` where its SSA-level meaning is
+    /// `([9,2], [1,2])`. The verifier must reject: checking each argument in
+    /// isolation misses it, because the caller never reads `v0` after the call
+    /// (the aliased read is the callee's `return` of the sibling argument).
+    /// This is the SSA shape `ssa_gen` emitted for `f(&mut x, x)` before the
+    /// ownership pass learned to clone a by-value argument that aliases a
+    /// `&mut` argument of the same call (noir-lang/noir-claude#1553).
+    #[test]
+    fn end_to_end_mut_ref_arg_pointing_at_by_value_arg_of_same_call_is_rejected() {
+        let src = r#"
+            brillig(inline) fn main f0 {
+              b0():
+                v0 = make_array [Field 1, Field 2] : [Field; 2]
+                v1 = allocate -> &mut [Field; 2]
+                store v0 at v1
+                v2, v3 = call f1(v1, v0) -> ([Field; 2], [Field; 2])
+                return v2, v3
+            }
+            brillig(inline) fn f f1 {
+              b0(v0: &mut [Field; 2], v1: [Field; 2]):
+                v2 = load v0 -> [Field; 2]
+                v3 = array_set v2, index u32 0, value Field 9
+                store v3 at v0
+                inc_rc v3
+                return v1, v3
+            }"#;
+        assert_verifier_rejects(src);
+    }
+
+    /// Companion of
+    /// [`end_to_end_mut_ref_arg_pointing_at_by_value_arg_of_same_call_is_rejected`]
+    /// with no reference anywhere: the **same array value occupies two argument
+    /// positions** (`call f1(v0, v0)`), the callee mutates one in place at RC 1
+    /// and returns the other, corrupted. This pins that the missing relation is
+    /// between argument positions as such, not something introduced by the
+    /// `&mut` argument. The frontend does not emit this shape (a reused
+    /// by-value argument is always cloned), so it is reachable from hand-written
+    /// SSA only; it must still be rejected.
+    #[test]
+    fn end_to_end_same_array_in_two_argument_positions_is_rejected() {
+        let src = r#"
+            brillig(inline) fn main f0 {
+              b0():
+                v0 = make_array [Field 1, Field 2] : [Field; 2]
+                v1, v2 = call f1(v0, v0) -> ([Field; 2], [Field; 2])
+                return v1, v2
+            }
+            brillig(inline) fn f f1 {
+              b0(v0: [Field; 2], v1: [Field; 2]):
+                v2 = array_set v0, index u32 0, value Field 9
+                inc_rc v2
+                return v1, v2
+            }"#;
+        assert_verifier_rejects(src);
+    }
+
+    /// The well-formed counterpart of
+    /// [`end_to_end_mut_ref_arg_pointing_at_by_value_arg_of_same_call_is_rejected`]:
+    /// the `inc_rc v0` the ownership pass emits for the by-value sibling of a
+    /// `&mut` argument is present before the call, so the callee's in-place
+    /// write copies (RC is 2) and the by-value parameter keeps its snapshot.
+    /// Accepted — this pins that the co-aliased-arguments check credits the
+    /// protecting `inc_rc` instead of flagging every call that passes a buffer
+    /// through two positions.
+    #[test]
+    fn end_to_end_mut_ref_arg_pointing_at_protected_by_value_arg_is_accepted() {
+        let src = r#"
+            brillig(inline) fn main f0 {
+              b0():
+                v0 = make_array [Field 1, Field 2] : [Field; 2]
+                v1 = allocate -> &mut [Field; 2]
+                store v0 at v1
+                inc_rc v0
+                v2, v3 = call f1(v1, v0) -> ([Field; 2], [Field; 2])
+                return v2, v3
+            }
+            brillig(inline) fn f f1 {
+              b0(v0: &mut [Field; 2], v1: [Field; 2]):
+                v2 = load v0 -> [Field; 2]
+                v3 = array_set v2, index u32 0, value Field 9
+                store v3 at v0
+                inc_rc v3
+                return v1, v3
+            }"#;
+        assert_verifier_accepts_because(
+            src,
+            "the by-value sibling of the &mut argument is protected by a preceding inc_rc",
+        );
+    }
+
+    /// Regression for the `valid_after_pass` fuzzer seed `0x96293a520000f025`.
+    /// Two block parameters of a join reach a call as sibling arguments. On the
+    /// branch that passes the *same* array in both positions, the frontend's
+    /// clones are present as `inc_rc`s in that branch — protection delivered
+    /// per path, from a predecessor that does not dominate the join. On the
+    /// other branch the two positions carry distinct fresh arrays and need no
+    /// protection. Well-formed on every path, so the co-aliased-arguments
+    /// check must accept: a dominance-only `inc_rc` search rejects this SSA.
+    #[test]
+    fn end_to_end_join_passing_shared_array_with_branch_local_inc_rc_is_accepted() {
+        let src = r#"
+            brillig(inline) fn main f0 {
+              b0(v0: u1):
+                jmpif v0 then: b1(), else: b2()
+              b1():
+                v2 = make_array [Field 1, Field 2] : [Field; 2]
+                v3 = make_array [Field 3, Field 4] : [Field; 2]
+                jmp b3(v2, v3)
+              b2():
+                v4 = make_array [Field 5, Field 6] : [Field; 2]
+                inc_rc v4
+                inc_rc v4
+                jmp b3(v4, v4)
+              b3(v5: [Field; 2], v6: [Field; 2]):
+                v7, v8 = call f1(v5, v6) -> ([Field; 2], [Field; 2])
+                return v7, v8
+            }
+            brillig(inline) fn f f1 {
+              b0(v0: [Field; 2], v1: [Field; 2]):
+                v2 = array_set v0, index u32 0, value Field 9
+                inc_rc v2
+                return v1, v2
+            }"#;
+        assert_verifier_accepts_because(
+            src,
+            "the only path passing one buffer through both positions bumps it in that branch",
+        );
+    }
+
+    /// The unprotected counterpart of
+    /// [`end_to_end_join_passing_shared_array_with_branch_local_inc_rc_is_accepted`]:
+    /// the branch that passes the same array through both positions carries no
+    /// `inc_rc`, so on that path the callee's in-place mutation is observable
+    /// through the sibling argument. Must be rejected.
+    #[test]
+    fn end_to_end_join_passing_shared_array_without_inc_rc_is_rejected() {
+        let src = r#"
+            brillig(inline) fn main f0 {
+              b0(v0: u1):
+                jmpif v0 then: b1(), else: b2()
+              b1():
+                v2 = make_array [Field 1, Field 2] : [Field; 2]
+                v3 = make_array [Field 3, Field 4] : [Field; 2]
+                jmp b3(v2, v3)
+              b2():
+                v4 = make_array [Field 5, Field 6] : [Field; 2]
+                jmp b3(v4, v4)
+              b3(v5: [Field; 2], v6: [Field; 2]):
+                v7, v8 = call f1(v5, v6) -> ([Field; 2], [Field; 2])
+                return v7, v8
+            }
+            brillig(inline) fn f f1 {
+              b0(v0: [Field; 2], v1: [Field; 2]):
+                v2 = array_set v0, index u32 0, value Field 9
+                inc_rc v2
+                return v1, v2
+            }"#;
+        assert_verifier_rejects(src);
+    }
+
+    /// A join whose branches pass one array through *different* positions —
+    /// `(v2, v3)` on one arm, `(v4, v2)` on the other. `v2` reaches both
+    /// argument positions, but never both on the same path, so no path hands
+    /// the callee one buffer twice and there is nothing to protect: each
+    /// branch-local use of `v2` is that branch's last use and is legitimately
+    /// moved without a clone. The check must accept — relating the positions'
+    /// backward alias sets without path sensitivity rejects this SSA.
+    #[test]
+    fn end_to_end_join_passing_array_through_different_positions_per_branch_is_accepted() {
+        let src = r#"
+            brillig(inline) fn main f0 {
+              b0(v0: u1):
+                v2 = make_array [Field 1, Field 2] : [Field; 2]
+                jmpif v0 then: b1(), else: b2()
+              b1():
+                v3 = make_array [Field 3, Field 4] : [Field; 2]
+                jmp b3(v2, v3)
+              b2():
+                v4 = make_array [Field 5, Field 6] : [Field; 2]
+                jmp b3(v4, v2)
+              b3(v5: [Field; 2], v6: [Field; 2]):
+                v7, v8 = call f1(v5, v6) -> ([Field; 2], [Field; 2])
+                return v7, v8
+            }
+            brillig(inline) fn f f1 {
+              b0(v0: [Field; 2], v1: [Field; 2]):
+                v2 = array_set v0, index u32 0, value Field 9
+                inc_rc v2
+                return v1, v2
+            }"#;
+        assert_verifier_accepts_because(
+            src,
+            "no single path passes the same buffer through two argument positions",
+        );
+    }
 }
diff --git a/compiler/noirc_evaluator/src/ssa/validation/rc_invariant/mod.rs b/compiler/noirc_evaluator/src/ssa/validation/rc_invariant/mod.rs
index 552330de971..ef7f4668df5 100644
--- a/compiler/noirc_evaluator/src/ssa/validation/rc_invariant/mod.rs
+++ b/compiler/noirc_evaluator/src/ssa/validation/rc_invariant/mod.rs
@@ -996,6 +996,181 @@ impl<'f> Context<'f> {
         }
     }
 
+    /// Whether some backward path from the call at `(call_block, call_idx)`
+    /// resolves `a` and `b` — the storages two argument positions of that call
+    /// denote — to the **same** buffer without crossing an `inc_rc` on it.
+    ///
+    /// This is the path-sensitive relation the co-aliased-arguments check
+    /// needs. Relating the two positions' backward alias *sets* is not enough,
+    /// for both directions of error:
+    ///
+    /// - a join may pass one buffer through both positions on one branch and
+    ///   protect it with a branch-local `inc_rc` that dominates nothing (the
+    ///   `valid_after_pass` fuzzer seed `0x96293a520000f025`), and
+    /// - a join may pass one buffer through *different* positions per branch
+    ///   (`(a, x)` on one arm, `(y, a)` on the other), so the sets intersect
+    ///   even though no single path carries the buffer twice.
+    ///
+    /// The walk threads the *pair* `(a, b)` backward over `(block, a, b)`
+    /// states, mirroring [`Context::compute_uncovered_values`]: across a
+    /// block-parameter edge each side follows the predecessor's argument, and
+    /// an `array_set` result continues with its array operand (the result
+    /// shares the operand's storage). Walls and sinks, in the order checked:
+    ///
+    /// - **`inc_rc` on either name** in the current block (limited to bumps
+    ///   before the call in the call's own block): covered. If the two names
+    ///   denote one buffer on this path, either bump protects it; if they
+    ///   don't, there is no hazard on this path to begin with.
+    /// - **Names equal, defined here or entry reached**: one buffer reaches
+    ///   both positions with no bump crossed — an uncovered terminal.
+    /// - **Names distinct and one is defined here** (non-`array_set`): the
+    ///   two positions carry distinct storages on this path — covered. (Two
+    ///   distinct names for one buffer via un-threaded relations, e.g. an
+    ///   `array_get` extraction, are not modeled — consistent with the rest
+    ///   of the alias engine, a false negative but never a false positive.)
+    /// - **Names distinct at an entry block**: distinct roots — covered.
+    ///
+    /// An unresolvable edge argument is conservatively an uncovered terminal.
+    /// Phase 2 propagates "uncovered" to a fixed point exactly like
+    /// [`Context::compute_uncovered_values`]; a cycle with no uncovered
+    /// terminal stays covered.
+    fn pair_has_unprotected_shared_storage(
+        &self,
+        a: ValueId,
+        b: ValueId,
+        call_block: BasicBlockId,
+        call_idx: usize,
+    ) -> bool {
+        struct Node {
+            successors: Vec<(BasicBlockId, ValueId, ValueId)>,
+            uncovered_terminal: bool,
+        }
+
+        let inc_rc_in_block = |value: ValueId, block: BasicBlockId, limit: Option<usize>| {
+            self.inc_rc_locations.get(&value).is_some_and(|locations| {
+                locations
+                    .iter()
+                    .any(|&(rc_block, i)| rc_block == block && limit.is_none_or(|limit| i < limit))
+            })
+        };
+
+        // The instruction defining `value` in `block`, if any.
+        let def_in_block = |value: ValueId, block: BasicBlockId| -> Option<&Instruction> {
+            let &(def_block, def_idx) = self.array_value_defs.get(&value)?;
+            (def_block == block)
+                .then(|| &self.function.dfg[self.function.dfg[block].instructions()[def_idx]])
+        };
+
+        // Phase 1: build the backward threading graph over (block, a, b) states.
+        let mut graph: HashMap<(BasicBlockId, ValueId, ValueId), Node> = HashMap::default();
+        let mut worklist: Vec<(BasicBlockId, ValueId, ValueId, Option<usize>)> =
+            vec![(call_block, a, b, Some(call_idx))];
+
+        while let Some((block, a, b, seed_idx)) = worklist.pop() {
+            if graph.contains_key(&(block, a, b)) {
+                continue;
+            }
+
+            // Wall: a bump on either name protects the buffer if the names
+            // coincide, and if they don't there is no hazard on this path.
+            if inc_rc_in_block(a, block, seed_idx) || inc_rc_in_block(b, block, seed_idx) {
+                graph.insert((block, a, b), Node { successors: vec![], uncovered_terminal: false });
+                continue;
+            }
+
+            // An `array_set` result shares its operand's storage; continue
+            // threading the pair with the operand.
+            if let Some(Instruction::ArraySet { array, .. }) = def_in_block(a, block) {
+                let array = *array;
+                graph.insert(
+                    (block, a, b),
+                    Node { successors: vec![(block, array, b)], uncovered_terminal: false },
+                );
+                worklist.push((block, array, b, seed_idx));
+                continue;
+            }
+            if let Some(Instruction::ArraySet { array, .. }) = def_in_block(b, block) {
+                let array = *array;
+                graph.insert(
+                    (block, a, b),
+                    Node { successors: vec![(block, a, array)], uncovered_terminal: false },
+                );
+                worklist.push((block, a, array, seed_idx));
+                continue;
+            }
+
+            if a == b {
+                // One name, both positions. If its storage originates here (a
+                // non-threadable definition) or the walk reached an entry with
+                // no bump crossed, this path hands the callee one buffer twice
+                // unprotected.
+                let defined_here = def_in_block(a, block).is_some();
+                let mut preds = self.cfg.predecessors(block).peekable();
+                if defined_here || preds.peek().is_none() {
+                    graph.insert(
+                        (block, a, b),
+                        Node { successors: vec![], uncovered_terminal: true },
+                    );
+                    continue;
+                }
+            } else if def_in_block(a, block).is_some() || def_in_block(b, block).is_some() {
+                // Distinct names and one storage originates here: the other
+                // name cannot resolve to it further back, so this path carries
+                // two distinct buffers.
+                graph.insert((block, a, b), Node { successors: vec![], uncovered_terminal: false });
+                continue;
+            }
+
+            let preds: Vec<BasicBlockId> = self.cfg.predecessors(block).collect();
+            if preds.is_empty() {
+                // Entry reached with distinct names: distinct roots (the `a ==
+                // b` entry case is an uncovered terminal above).
+                graph.insert((block, a, b), Node { successors: vec![], uncovered_terminal: false });
+                continue;
+            }
+
+            let params = self.function.dfg.block_parameters(block);
+            let a_pos = params.iter().position(|&p| p == a);
+            let b_pos = params.iter().position(|&p| p == b);
+            let mut successors = Vec::new();
+            let mut uncovered_terminal = false;
+            for &pred in &preds {
+                let resolve = |pos: Option<usize>, value: ValueId| match pos {
+                    Some(i) => self.edge_arg(pred, block, i),
+                    None => Some(value),
+                };
+                match (resolve(a_pos, a), resolve(b_pos, b)) {
+                    (Some(next_a), Some(next_b)) => {
+                        successors.push((pred, next_a, next_b));
+                        worklist.push((pred, next_a, next_b, None));
+                    }
+                    // An unresolvable edge argument: conservatively treat as
+                    // uncovered rather than silently dropping the path.
+                    _ => uncovered_terminal = true,
+                }
+            }
+            graph.insert((block, a, b), Node { successors, uncovered_terminal });
+        }
+
+        // Phase 2: propagate "uncovered" from terminals to a fixed point.
+        let mut uncovered: HashSet<(BasicBlockId, ValueId, ValueId)> =
+            graph.iter().filter(|(_, n)| n.uncovered_terminal).map(|(k, _)| *k).collect();
+        let mut changed = true;
+        while changed {
+            changed = false;
+            for (state, node) in &graph {
+                if !uncovered.contains(state)
+                    && node.successors.iter().any(|s| uncovered.contains(s))
+                {
+                    uncovered.insert(*state);
+                    changed = true;
+                }
+            }
+        }
+
+        uncovered.contains(&(call_block, a, b))
+    }
+
     /// Run the coverage narrowing + forward reachable-use walk for a single
     /// potential in-place mutation of `source` at `(block, idx)` (the
     /// instruction `mutator_id`). Returns the aliased use that would observe
diff --git a/compiler/noirc_frontend/src/ownership/last_uses.rs b/compiler/noirc_frontend/src/ownership/last_uses.rs
index c5f4bcfa96e..7bc54171680 100644
--- a/compiler/noirc_frontend/src/ownership/last_uses.rs
+++ b/compiler/noirc_frontend/src/ownership/last_uses.rs
@@ -411,11 +411,19 @@ impl LastUseContext {
         let conservative = type_contains_reference(&call.return_type)
             || call.arguments.iter().any(arg_can_store_reference);
 
-        for arg in call.arguments.iter().rev() {
+        for (index, arg) in call.arguments.iter().enumerate().rev() {
             if !conservative
                 && let Expression::Unary(unary) = arg
                 && matches!(unary.operator, UnaryOp::Reference { .. })
-                && base_ident_of_field_access(&unary.rhs).is_some()
+                && let Some(base) = base_ident_of_field_access(&unary.rhs)
+                // Even though the reference cannot escape the call, the *other* arguments of
+                // this same call are evaluated and handed to the callee while the reference is
+                // live. If one of them mentions `x` (e.g. `foo(&mut x, x)`), moving that use
+                // would let the callee's writes through the reference be observed through a
+                // by-value argument, so `x` must be treated as aliased.
+                && !call.arguments.iter().enumerate().any(|(other_index, other_arg)| {
+                    other_index != index && local_occurs_in(base, other_arg)
+                })
             {
                 // Track the use of the variable inside the reference (for last-use analysis)
                 // but skip the unary handler, which would mark the variable as aliased.
diff --git a/compiler/noirc_frontend/src/ownership/tests.rs b/compiler/noirc_frontend/src/ownership/tests.rs
index cbc9b945121..28c670d26ce 100644
--- a/compiler/noirc_frontend/src/ownership/tests.rs
+++ b/compiler/noirc_frontend/src/ownership/tests.rs
@@ -1305,6 +1305,34 @@ fn reference_passed_alongside_struct_with_mut_ref_to_ref_prevents_move() {
     ");
 }
 
+#[test]
+fn by_value_arg_aliasing_mut_ref_arg_of_same_call_prevents_move() {
+    // When passing `&mut a` and `a`, `a` needs to be cloned
+    let src = "
+    unconstrained fn main(x: [Field; 2]) -> pub ([Field; 2], [Field; 2]) {
+        let mut a = x;
+        foo(&mut a, a)
+    }
+
+    fn foo(r: &mut [Field; 2], b: [Field; 2]) -> ([Field; 2], [Field; 2]) {
+        (*r)[0] = 99;
+        (*r, b)
+    }
+    ";
+
+    let program = get_monomorphized(src).unwrap();
+    insta::assert_snapshot!(program, @r"
+    unconstrained fn main$f0(x$l0: [Field; 2]) -> pub ([Field; 2], [Field; 2]) {
+        let mut a$l1 = x$l0;
+        foo$f1((&mut a$l1), a$l1.clone())
+    }
+    unconstrained fn foo$f1(r$l2: &mut [Field; 2], b$l3: [Field; 2]) -> ([Field; 2], [Field; 2]) {
+        (*r$l2)[0] = 99;
+        ((*r$l2).clone(), b$l3)
+    }
+    ");
+}
+
 #[test]
 fn call_with_extract_tuple_field_args_does_not_prevent_move() {
     // Mirrors the `try_resize` pattern in UHashMap: `insert(&mut new_map, entry.0, entry.1)`
diff --git a/test_programs/execution_success/ownership_by_value_arg_aliasing_mut_ref_regression/Nargo.toml b/test_programs/execution_success/ownership_by_value_arg_aliasing_mut_ref_regression/Nargo.toml
new file mode 100644
index 00000000000..c8de3e210c1
--- /dev/null
+++ b/test_programs/execution_success/ownership_by_value_arg_aliasing_mut_ref_regression/Nargo.toml
@@ -0,0 +1,6 @@
+[package]
+name = "ownership_by_value_arg_aliasing_mut_ref_regression"
+type = "bin"
+authors = [""]
+
+[dependencies]
diff --git a/test_programs/execution_success/ownership_by_value_arg_aliasing_mut_ref_regression/Prover.toml b/test_programs/execution_success/ownership_by_value_arg_aliasing_mut_ref_regression/Prover.toml
new file mode 100644
index 00000000000..7f7e85105db
--- /dev/null
+++ b/test_programs/execution_success/ownership_by_value_arg_aliasing_mut_ref_regression/Prover.toml
@@ -0,0 +1,4 @@
+a = "1"
+b = "2"
+c = "3"
+i = "0"
diff --git a/test_programs/execution_success/ownership_by_value_arg_aliasing_mut_ref_regression/src/main.nr b/test_programs/execution_success/ownership_by_value_arg_aliasing_mut_ref_regression/src/main.nr
new file mode 100644
index 00000000000..319e07f5691
--- /dev/null
+++ b/test_programs/execution_success/ownership_by_value_arg_aliasing_mut_ref_regression/src/main.nr
@@ -0,0 +1,14 @@
+// Companion test program for the ownership test by_value_arg_aliasing_mut_ref_arg_of_same_call_prevents_move
+
+unconstrained fn f(r: &mut [Field; 3], v: [Field; 3], i: u32) -> ([Field; 3], [Field; 3]) {
+    (*r)[i] = 99;
+    (v, *r)
+}
+
+unconstrained fn main(a: Field, b: Field, c: Field, i: u32) {
+    let mut x = [a, b, c];
+    let (v, r) = f(&mut x, x, i);
+    // `v` must be the pre-write snapshot (the inputs fix `i = 0` and `a = 1`).
+    assert(v[i] == a);
+    assert(r[i] == 99);
+}
diff --git a/tooling/debugger/ignored-tests.txt b/tooling/debugger/ignored-tests.txt
index 96fec7a934d..a0c00b9d421 100644
--- a/tooling/debugger/ignored-tests.txt
+++ b/tooling/debugger/ignored-tests.txt
@@ -26,4 +26,5 @@ brillig_block_mutable_reference_regression
 brillig_block_mutable_reference_inner_ref_regression
 brillig_block_mutable_reference_let_chain_long_regression
 brillig_block_mutable_reference_let_chain_regression
-brillig_block_mutable_reference_index_regression
\ No newline at end of file
+brillig_block_mutable_reference_index_regression
+ownership_by_value_arg_aliasing_mut_ref_regression
\ No newline at end of file
diff --git a/tooling/nargo_cli/tests/snapshots/execution_success/ownership_by_value_arg_aliasing_mut_ref_regression/execute__tests__expanded.snap b/tooling/nargo_cli/tests/snapshots/execution_success/ownership_by_value_arg_aliasing_mut_ref_regression/execute__tests__expanded.snap
new file mode 100644
index 00000000000..00f6a3078c9
--- /dev/null
+++ b/tooling/nargo_cli/tests/snapshots/execution_success/ownership_by_value_arg_aliasing_mut_ref_regression/execute__tests__expanded.snap
@@ -0,0 +1,15 @@
+---
+source: tooling/nargo_cli/tests/execute.rs
+expression: expanded_code
+---
+unconstrained fn f(r: &mut [Field; 3], v: [Field; 3], i: u32) -> ([Field; 3], [Field; 3]) {
+    (*r)[i] = 99_Field;
+    (v, *r)
+}
+
+unconstrained fn main(a: Field, b: Field, c: Field, i: u32) {
+    let mut x: [Field; 3] = [a, b, c];
+    let (v, r): ([Field; 3], [Field; 3]) = f(&mut x, x, i);
+    assert(v[i] == a);
+    assert(r[i] == 99_Field);
+}
diff --git a/tooling/nargo_cli/tests/snapshots/execution_success/ownership_by_value_arg_aliasing_mut_ref_regression/execute__tests__stdout.snap b/tooling/nargo_cli/tests/snapshots/execution_success/ownership_by_value_arg_aliasing_mut_ref_regression/execute__tests__stdout.snap
new file mode 100644
index 00000000000..e86e3de90e1
--- /dev/null
+++ b/tooling/nargo_cli/tests/snapshots/execution_success/ownership_by_value_arg_aliasing_mut_ref_regression/execute__tests__stdout.snap
@@ -0,0 +1,5 @@
+---
+source: tooling/nargo_cli/tests/execute.rs
+expression: stdout
+---
+