The specifications have some branches that depend on the mint being initialised to a valid value, which is only valid if field is_initialized is 0 or 1 and it errors otherwise.
Our cheatcode that sets the symbolic state restricts the state to $0 ≤ is\_initialized ≤ 1$ which means we will never explore the error branch. (Same for concrete / random execution)
The solution is to expand this to the full range of u8
The specifications have some branches that depend on the mint being initialised to a valid value, which is only valid if field is_initialized is 0 or 1 and it errors otherwise.
Our cheatcode that sets the symbolic state restricts the state to$0 ≤ is\_initialized ≤ 1$ which means we will never explore the error branch. (Same for concrete / random execution)
The solution is to expand this to the full range of
u8