It may be the case that the fields in fields and oldFields of a transaction do not match, because of the way data storage is handled. To avoid issues with Apalache, due to missing state-variable assignments, we should use Gen-based initialization to mitigate this.
It may be the case that the fields in
fieldsandoldFieldsof a transaction do not match, because of the way data storage is handled. To avoid issues with Apalache, due to missing state-variable assignments, we should useGen-based initialization to mitigate this.