There are two cases where the assert in gotoc statement assignment is failing [0]

1. When the types are wrapped (e.g. in a Cell) array types when one has an explicit length (e.g., [T;N]) and the other is inferred ([T;_]). E.g.: StructTag("tag-std::cell::RefCell<[bool; 16]>") and StructTag("tag-std::cell::RefCell<[bool; _]>")

2. When the types are closures. E.g., Pointer { typ: StructTag("tag-[[email protected]:536:13: 546:14]") } and Pointer { typ: StructTag("tag-[[email protected]:503:13: 509:14]") }

The root cause is the naming of these symbol associated with these types.

[0] https://github.com/model-checking/rmc/blob/main-151-2021-04-16/compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/stmt.rs#L153