Allocate new arrays for `write` only when necessary

In our current implementation, a copy of the array is allocated for each write. This could introduce some redundancy in our generated code. For example, we only need 1 (or even 0) array copy for 5 consecutive writes instead of 5, since no other operations try to access the old array in between.

BTOR2 array operations can be classified into 3 categories.

• State assignment: init, next
• Write: write
• Access: read, ite, eq, neq

If there is no access between writes, a copy is not needed.