MEVALP1 leaking assumption



On 2013-03-15, Stavros Macrakis <macrakis at alum.mit.edu> wrote:

> Not sure I understand what you're proposing. Won't that break
>
>     [ asksign(x), sign(x), sign(x) ] ?
>
> The scope of asksign is supposed to be one top-level interaction.

OK, I won't change 'asksign' ... hey, look at that, it's documented!

Is there a rationale for 'sign' leaving stuff in the assume database?

best

Robert Dodier