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.
Edited by Nian-Ze Lee