[SMT-LIB] SMT doubt

[Daniela da Cruz]

Hi.
I'm new in the SMT language and I'm facing some problems with respect to the
understanding
of notation.
I send in attachement a file that I write to prove a set of formulas.
I've two questions:
1. There is necessary to negate each formula?
2. When we are reasoning over arrays, there it makes sense to define the
size of the array as a variable
(for example, the variable "length" with value 100). If so, how I do it?

Thanks
best regards
daniela
-------------- next part --------------
A non-text attachment was scrubbed...
Name: maxarray-1.c
Type: application/octet-stream
Size: 452 bytes
Desc: not available
Url : /pipermail/smt-lib/attachments/20090106/bdbff93f/maxarray-1.obj