Added post processing fix to overcome shortcoming in array assignment. Part of the translation problem arises because Event-B does not allow expressions on the LHS of assignment, as seen in a C array assignment, a[i] = v . This makes it difficult to translate from a := a <+ {i|->v} to the above. The matcher matches the assignment _ := _ first, and the LHS is an identifier, which is not what is required for output.