[SMT-LIB] Unary operator ~

Albert Oliveras Llunell oliveras at lsi.upc.edu
Sun Aug 9 06:00:41 EDT 2009


Dear Daniela,

the problem is with parenthesis.
Instead of using it in expressions like

(>= ~b a )

you should parenthesize it like

(>= (~ b) a)

Regards
Albert


> Hello all.
>
> I've a problem with the unary operator ~ (from that I've read I think it
> corresponds to the minus unary operator).
> When I try to use this operator, it gives me an error: ERROR: could not
> locate id ~b at 23:10.
> It seems that when using that operator, it does not recognize what
> follows...
> I already tried also to use with parenthesis but I obtain another error:
> ERROR: No arguments supplied to arithmetical operator
>
> Can anyone help me?
> I send the file that I'm trying in attachment.
>
> Thanks
> regards
> daniela
>   
> ------------------------------------------------------------------------
>
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib
>   



More information about the SMT-LIB mailing list