Add QF_AUFLIRA logic
Model arrays in sequential code

Use QF_AUFLIRA logic to model Internal<T[]>. Note that QF_AUFLIRA
is not listed among the official SMT theories [1] but it is (at
least) currently supported by CVC4 and Z3.

As an optimization, we represent individual array elements
as long as none of the used array indexes are symbolic.

[1] http://www.smt-lib.org/