Panic: "borrowing unbound var" when writing through a reassigned `&mut` local

[coord-e]

Summary

Analyzing a function that reassigns a &mut-typed local (a second assignment to a let mut r) and then writes through it (*r = ...) panics with borrowing unbound var in Env::borrow_var (src/refine/env.rs:1005). The reassignment leaves the reference local without a flow binding, so when ReborrowVisitor elaborates the later write into a reborrow of *r, borrow_var finds no binding for the local and the .expect("borrowing unbound var") fires.

This is valid, safe Rust — the program below never panics at runtime (b == 20 holds) — yet it crashes the analyzer instead of verifying.

Reproduction (minimal)

fn main() {
 let mut a = 1;
 let mut b = 2;
 let mut r = &mut a;
 r = &mut b; // reassign the &mut local
 *r = 20; // write through it -> ICE
 assert!(b == 20);
}

$ cargo run --quiet -- -Adead_code -C debug-assertions=false repro.rs
thread 'rustc' panicked at src/refine/env.rs:1005:39:
borrowing unbound var
stack backtrace:
 ...
 4: thrust::refine::env::Env<T>::borrow_var
 at ./src/refine/env.rs:1005:39
 5: thrust::refine::env::Env<T>::borrow_place
 at ./src/refine/env.rs:1047:14
 6: thrust::analyze::basic_block::Analyzer::borrow_place_
 at ./src/analyze/basic_block.rs:1046:18
 7: thrust::analyze::basic_block::visitor::reborrow::ReborrowVisitor::insert_reborrow
 at ./src/analyze/basic_block/visitor/reborrow.rs:28:42
 8: <...ReborrowVisitor as ...MutVisitor>::visit_assign
 at ./src/analyze/basic_block/visitor/reborrow.rs:78:38
 ...

What does / does not trigger it

Variant	Result
r = &mut b; *r = 20; (reassign, then write)	panic
r = &mut a; *r = 5; (reassign to the same target, then write)	panic
r = &mut b; let v = *r; (reassign, then read only)	verifies fine
if cond { r = &mut b; } *r = 20; (reassign in a separate basic block)	verifies fine (correctly rejects false asserts, accepts true ones)
let mut x = 1; x = 2; x = 3; (reassigning a non-reference mut local)	verifies fine

So reassigning &mut locals is otherwise a working, supported feature — the conditional form is both sound and complete. The crash is specific to a straight-line reassignment of a reference-typed local followed by a write through it in the same basic block.

MIR

The optimized MIR of main (r is _3):

bb0: {
 _1 = const 1_i32;
 _2 = const 2_i32;
 _3 = &mut _1; // let mut r = &mut a
 _4 = &mut _2; // temp = &mut b
 _3 = copy _4; // r = temp <-- reassignment of the &mut local
 (*_3) = const 20_i32;// *r = 20 <-- write through it
 _5 = copy _2;
 switchInt(move _5) -> [20: bb2, otherwise: bb1];
}

Analysis

ReborrowVisitor::visit_assign handles the reassignment _3 = copy _4 via the mutable-local branch (src/analyze/basic_block/visitor/reborrow.rs:51):

if place.projection.is_empty() && self.analyzer.is_mut_local(place.local) {
 let ty = self.analyzer.local_decls[place.local].ty;
 let new_local = self.insert_borrow(place.local.into(), ty); // borrow _3's slot
 ...
}

_3 is let mut and already defined (from _3 = &mut _1), so this branch rewrites the reassignment into a write through a fresh borrow of _3's slot. After this rewrite, _3 no longer carries a Mut flow binding that points at the new referent _2.

When the subsequent write (*_3) = 20 is visited, visit_assign elaborates the mutable deref into a reborrow of *_3, which walks borrow_place(*_3) → borrow_var(_3):

fn borrow_var(&mut self, var: Var, prophecy: TempVarIdx) -> PlaceType {
 match *self.flow_binding(var).expect("borrowing unbound var") { // env.rs:1005 — None here
 ...

flow_binding(_3) is None, so the .expect panics. A read of *_3 does not go through the reborrow/borrow_var path (the operand is i32-typed, so visit_operand short-circuits), which is why reading through the reassigned reference does not crash.

The underlying gap seems to be that reassigning a reference-typed mut local does not re-establish (or preserve) the local's Mut/Box flow binding pointing at the new referent, whereas the cross-basic-block form ends up with a correct binding.

Relationship to #125 / #40

Both are also ... unbound var ICEs but are distinct:

• Panic: "deref unbound var" when reborrowing a &mut field out of an aggregate parameter #125 (deref unbound var in locate_place) is about reborrowing a &mut field out of an aggregate parameter; here the local is a plain &mut local and the panic is borrowing unbound var in borrow_var, triggered by reassignment, not by aggregate parameters.
• Passing a mutable reference of an empty tuple to a function causes a panic #40 (unbound var t1 in clause_builder) is about passing &mut () (empty tuple).

Neither involves reassigning a &mut local. This reproduction still panics on main @ af7cd99.

Environment

• thrust @ af7cd99
• rustc nightly-2025-09-08 (per rust-toolchain.toml)
• z3 4.16.0