Borrow a pointer-typed field itself when replacing it

[coord-e]

Refs #267

ReborrowVisitor::visit_assign chose its Ref/Box arms from the type of inner_place. When the assigned place does not end in Deref, inner_place is the place itself, so for a Box- or &mut-typed struct or tuple field those arms borrowed the field's pointee:

• c.page = Box::new(5) became a write through the old box. The field was left typed as int, and the next use of the struct aborted (PlaceType::deref unwrap, inconsistent types: got=int, expected=own int).
• c.v = v on a &mut field built mut(<Mut<Int>>, <Int>), which the solver rejects as ill-sorted. Any setter like fn set(c: &mut Cell<'a>, v: &'a mut i64) { c.v = v; } failed the whole crate with a verification Error, even if nothing read the field afterwards.

With this change the pointer arms are taken only when a trailing Deref was actually stripped. A field replacement now falls through to the _ arm, which borrows the field itself, just as a Vec-typed field already does.

Results

Program	Before	After
#267 f1, f2, f4 (Box field replaced, then read)	abort	safe, and the flipped assertion gives Unsat
&mut-field setter (from the comment on #267)	solver Error (ill-sorted term)	safe, and the flipped assertion gives Unsat
#267 f3 (write through the field after replacing it in the same body)	borrowing unbound var	unchanged. This is the #176 path, where the new value's binding is a plain prophecy variable

The setter case still loses the old lender's value (a after set(&mut c, &mut b)). That is #310, which #311 addresses.

Test

Added tests/ui/{pass,fail}/assign_box_field.rs. All 394 UI tests pass locally with Z3 5.0.0 and the pinned PCSat. cargo fmt --check and cargo clippy -D warnings are clean.

🤖 Generated with Claude Code

https://claude.ai/code/session_01Q3oq9H8cDHT88svt78yAmn

---

Generated by Claude Code

[chatgpt-codex-connector]

Codex Review Summary

This comment shows the latest Codex review activity on this pull request.

Review	Status	Commit	Review trigger
📝 Code Review	✅ Completed 2026-10-05T21:58:12.552606Z	e3cbb4c	PR opened

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review" or "@codex security review".

Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings.