[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:
> 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?
> best regards
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 2034 bytes
Desc: not available
Url : /pipermail/smt-lib/attachments/20090106/94c1edb6/maxarray-1.obj
More information about the SMT-LIB