changed state to maintain a seq of string rather than just a string so
that previous translations are cached
added base choice to array lookup that ensures the concrete index is
distinct from the set of symbolic indices.  Consider the case where an
update is performed on single element array, then a concrete lookup is
done on the prestate array, then the concrete lookup is done on the
current array.  The orig semantics returned the value materialized in
the prestate.