"early unsat" bookeeping error

[robdockins]

Yices has an annoying "feature" where it will sometimes return an unsat result as soon as it discovers that the user has asserted an inconsistent set of assumptions, but before the user has called check. In this state, Yices will refuse to accept additional assertions, etc.

To handle this, we explicitly look for these early unsat results and pretend that we are doing work and sending results to yices, etc. until check is called. This is made more complicated by the need to pretend that we are also doing push/pop sequences, all while avoiding interacting with yices until a sufficient number of pops are performed to return to a (potentially) satisfiable state. We have an accounting scheme that mostly works.

However, I've just discovered that the bookeeping doesn't appear to be working correctly if an early unsat is encountered at the very top level of interaction (i.e., we have not done any previous push commands). The result will be a mysterious and unpleasant error reading "user error (Could not pop from empty entry stack.)" indicating that we have violated an internal invariant of the SMTWriter module.