[SMT-LIB] SMT doubt

[Daniela da Cruz]

Sorry, was the wrong attachement.
Now the correct.
daniela

On Tue, Jan 6, 2009 at 5:44 PM, Daniela da Cruz <danieladacruz at gmail.com>wrote:

> 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.smt
Type: application/octet-stream
Size: 2034 bytes
Desc: not available
Url : /pipermail/smt-lib/attachments/20090106/94c1edb6/maxarray-1.obj