I read this as mut1 and mut2 both being downgraded to shared references because they aren't used to mutate anymore. I'd imagine that's not what's actually happening though?
No - that they are both &mut _ indicates that a mutable reference is being acquired regardless of whether or not they’re used for any mutation. Possibly the compiler could automatically lower to a shared reference if it detects no mutation access locally but there may be design reasons why that’s impossible (+ you can’t have a mutable and a shared reference simultaneously anyway so downgrading to shared would still be disallowed)