MEVALP1 leaking assumption



On 2013-03-12, Barton Willis <willisb at unk.edu> wrote:

> Maybe the CL function clearsign isn't being called to clean up the
> fact database?  Actually all the calls to sign + csign in simplifying
> functions frighten me--each call to sign potentially changes the fact
> database. And the call to clearsign seems to be in the main read,
> evaluate, print loop.

Thanks for the hint -- indeed the problem is that facts introduced by
sign functions aren't getting cleaned up. 

I've patch $SIGN so that it calls CLEARSIGN. $CSIGN calls $SIGN so it
now cleans up too. I guess I'll do $ASKSIGN too. Incidentally the test
suite is happy with the change to $SIGN.

I'm pretty sure other sign functions (SIGN1, maybe others) are used as
entry points, but I think it's reasonable to put the clean up only in
the top-level sign functions.

best

Robert Dodier