Fix the zombie solver processes mentioned in #477

[lsrcz]

I encountered the same issue as mentioned in #477, and this pull request tries to fix it. I do not fully understand the codebase, so please carefully review my changes.

I believe that the root cause of the issue is that the queryTerminate (i.e., the cleanUp function defined in runSolver) is skipped when an exception happens before it but after the solver has been started by the runSolver call.

This pull request moves the termination of the solver to executeQuery function, and terminates it immediately after we finished all the interaction with the solver. In this function, we have the handy ExtractIO class, which allows us to do the clean up no matter whether an exception is raised with finally.

The ExtractIO instance for IO is also buggy, though. It violates the law mentioned in the comment. This pull request also fixes it, and the fix is required for the clean up to work.

sbv/Data/SBV/Utils/ExtractIO.hs

Lines 29 to 31 in ddd2c87

	class MonadIO m => ExtractIO m where
	-- | Law: the @m a@ yielded by 'IO' is pure with respect to 'IO'.
	extractIO :: m a -> IO (m a)

After doing these changes, I observed no zombie or long-running processes after killing a thread running sbv.

[LeventErkok]

Great! Unfortunately I’m away from any decent computing device till about May 15th. I’ll take a look at that time.

I’m happy to merge to mainline if you’ve an urgent need. Let me know.

[lsrcz]

No hurry, I can rely on my own patched version for now.