So that we can easily replace the type of objects that are being used.

These methods generate new state(s) that are modified
by the read/write. We did this this way so that we can
later easily extend the code to support symbolic memory
where we can return a set of states that stem from one read/write.

Assing the solver to state, so that we can later create a new
incremental instance to each state if needed.