[SMT-LIB] SMT: arrays doubt

[Daniela da Cruz]

Hello all.
I'm relatively new in SMT and I'm studying the arrays.
However, when I have been looking for the Swap implementation (in Java+JML),
I saw that it makes use of the method "length" defined
by Java language.
Can anyone tell me how this is translated to SMT? And how it supposed to
translate something like "arr[i]"? Should I use some specific theory?

Thanks in advance

Best regards,
daniela