Remember to stop the solver when done.  Also more debugging.
Bugfix: avoid non-termination.

When we compute new derived work, we need to check that the result
is not already in the inert set.   If we don't do this, we keep finding
the same constraints over and over again, if they don't do anything to the
inert set.