Introduce T.int for integers. Previous T.int is called T.bigint. Improve T.rat.
Implement SMT arrays.