[SMT-LIB] SMT doubt

Daniela da Cruz danieladacruz at gmail.com
Tue Jan 6 12:45:47 EST 2009

Sorry, was the wrong attachement.
Now the correct.

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

More information about the SMT-LIB mailing list