Emma Zhong

> particularly that a similar information in the mid function, with the edges in hyper edge reordered, does not seem to be triggering this problem Why does removing the `mid`...

This sounds crazy but if you add another layer, the issue goes away... ```move /// This module defines a minimal Coin and Balance. module NamedAddr::BasicCoin { use std::vector; struct HasVector...

I wonder if there's anywhere where we reverse the order of edges by doing something like popping elements from the back and inserting them in the reverse order.

There's a place where we `reverse` the path when constructing a hyper edge: https://github.com/move-language/move/blob/main/language/move-prover/bytecode/src/borrow_analysis.rs#L271. I suspect there's something off here.

> having these index edges (seemingly, as I am not sure about that) connecting non-vector type nodes in the propagated hyper edges is a real problem It is a problem...

I think the `$t1` in `inner` and `mid` are different things? In `inner`, `$t1` is of type `vector`, and is the field of `$t0`. In `mid`, `$t1` is the return...

> neither $t0 nor $t1 in mid is a vector type: $t0|has_vector: &mut m1::HasVector and $t1: &mut m1::HasAnotherVector Right, but `$t0` has a field `v` that is a vector type....

> Have you debug print the dst_ty in the match dest_ty which causes the issue (sorry if I missed it)? `dst_ty` is `HasVector`. @awelc you can print the type with...

> The hyper edge becomes a part of the WriteBack operation and when the WriteBack operation is being translated in the Boogie backend's bytecode translator ([translate_writeback function](https://github.com/move-language/move/blob/c9bce5832193fef28dfd680b6f91c5ced15e0ff2/language/move-prover/boogie-backend/src/bytecode_translator.rs#L1552)), only the first...

> If index edge is first, though, translate_write_back_update will receive the existing original (non-vector) destination type, which will crash the prover in this case (outer function): Exactly. The correct order...