Add memory axioms to partial string model

Recall that a program is defined to be the downward closure of a
set of finite partial strings with respect to the partial string
refinement ordering. In essence, this gives an over-approximation
of the computation of a real world program.

We can make this abstraction more precise by adapting the CAV'13
memory axioms. Note that this precision gain can be only achieved
on the right-hand side of the refinement check. This has do with
the fact that the check whether "X" refines "Y" is equivalent to
checking that for all partial string "x" in "X", there exists a
partial string "y" in "Y" such that "x" refines "y".

Nevertheless, the fact that we can integrate the memory axioms in
our partial string model is significant for bug finding purposes.