Strange results from assume (maybe a bug?) ad asksign
Subject: Strange results from assume (maybe a bug?) ad asksign
From: Stavros Macrakis
Date: Sat, 27 Dec 2008 15:24:26 -0500
On Sat, Dec 27, 2008 at 2:48 PM, Alexey Beshenov <al at beshenov.ru> wrote:
> "assume(x>a and x<b)" will just make "is(x>y)" return "true" for y<=a,
> return "false" for y>=b, and return "unknown" otherwise (I'm not sure
> it was intended). I guess now there is no way to declare bounds for a
> variable correctly through the "assume" mechanism.
>
I'm not sure I understand what the problem is here. What would you expect
is(x>y) to return if y is not <= a or >= b?
-s