robdockins

Thank you for doing this. This library is indeed _very_ on the back burner, as there doesn't appear to be much general interest.

I see that I've let some compatibility fixes go ignored for a bit, I'll deal with that.

I think turning `fail` into `error` isn't the right fix in the majority of these cases. We probably actually want to turn most of the functions with a `Moand` constraint...

This looks like a better fix to me. I'll work on finding some time soon (this weekend probably) to merge this and put up a new release.

Thanks for putting these up here. I haven't had an opportunity to look at it yet, but when I find some time, I'll take a look at what it would...

Sure, I can come up with a test case. However, the larger context is quite a bit less self-contained. What I'm doing involves symbolic execution of programs and I use...

I was working on a small example to demonstrated the desired behavior. Somewhat to my surprise, STP already behaves as though `global-declarations` is set. [STP-online-quickstart.txt](https://github.com/stp/stp/files/4939062/STP-online-quickstart.txt)

> If you don't have `global-declarations` and you `pop` a previous symbol, do you expect to able to have the ability to create a symbol with a different type? That...

Here is a similar example using `(reset-assertions)`, which is accepted, e.g., by Z3 but fails for STP. [quickstart-alt.txt](https://github.com/stp/stp/files/4939302/quickstart-alt.txt)

I think the current stream-based interpretation is fine, as long as we also remember the associated quantifier. I don't know that I would necessarily expect a run-time interpretation of these...