[SMT-LIB] SMT: arrays doubt

Daniela da Cruz danieladacruz at gmail.com
Sat Oct 4 10:46:59 EDT 2008

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,

More information about the SMT-LIB mailing list