Memory leaks on exception

[rhelmot]

Whenever a check is interrupted by a call to interrupt(), a timeout, or even a memory limit, it seems like z3 leaks an awful lot of memory. Presumably this is because it is managing raw pointers on the stack and they are not being destroyed on unwind. Is this sort of thing considered a bug, or should I be running z3 in a separate process if I want to be able to recover from exceptional cases like this?

[NikolajBjorner]

It is desirable to not leak. Not sure if all bugs can be fixed easily,
but we try to support memory neutrality even with interrupt being invoked.
Z3_interrupt uses code paths also used by timeouts and timeouts are commonly used features.

[nunoplopes]

I'm not aware of any leaks with timeouts or soft memory limits, only hard memory limits. Please file bug reports if you find any (in TO or soft memory limit) as I'm very interested in those.
For hard memory limits, there are just too many leaking paths. Forget about it.