Merge pull request #691 from lsrcz/master

Fix the zombie solver processes mentioned in #477

Data/SBV/Control/Utils.hs

@@ -38,6 +38,7 @@ module Data.SBV.Control.Utils (
      , timeout, queryDebug, retrieveResponse, recoverKindedValue, runProofOn, executeQuery
      ) where
 
+import Control.Exception (finally)
 import Data.List  (sortBy, sortOn, elemIndex, partition, groupBy, tails, intercalate, nub, sort, isPrefixOf, isSuffixOf)
 
 import Data.Char      (isPunctuation, isSpace, isDigit)
@@ -1898,7 +1899,12 @@ executeQuery queryContext (QueryT userQuery) = do
 
                   liftIO $ writeIORef (runMode st) $ SMTMode qc IRun isSAT cfg
 
-                  lift $ join $ liftIO $ backend cfg' st (show pgm) $ extractIO . runReaderT userQuery
+                  lift $ join $ liftIO $
+                    finally (extractIO $ join $ liftIO $ backend cfg' st (show pgm) $ extractIO . runReaderT userQuery) $ do
+                      qs <- readIORef $ rQueryState st
+                      case qs of
+                        Nothing                         -> return ()
+                        Just QueryState{queryTerminate} -> queryTerminate
 
         -- Already in a query, in theory we can just continue, but that causes use-case issues
         -- so we reject it. TODO: Review if we should actually support this. The issue arises with

Data/SBV/Core/Symbolic.hs

@@ -1967,13 +1967,6 @@ runSymbolicInState st (SymbolicT c) = do
                  = contextMismatchError (sbvContext st) ctx Nothing Nothing
 
    mapM_ check $ nub $ G.universeBi res
-
-   -- Clean-up after ourselves
-   qs <- liftIO $ readIORef $ rQueryState st
-   case qs of
-     Nothing                         -> return ()
-     Just QueryState{queryTerminate} -> liftIO queryTerminate
-
    return (r, res)
 
 -- | Grab the program from a running symbolic simulation state.

Data/SBV/Utils/ExtractIO.hs

@@ -32,7 +32,7 @@ class MonadIO m => ExtractIO m where
 
 -- | Trivial IO extraction for 'IO'.
 instance ExtractIO IO where
-    extractIO = pure
+    extractIO = fmap pure
 
 -- | IO extraction for 'MaybeT'.
 instance ExtractIO m => ExtractIO (MaybeT m) where