diff --git a/CHANGES b/CHANGES
--- a/CHANGES
+++ b/CHANGES
@@ -1,3 +1,4 @@
+0.9.7: `newSolverNotify` has a callback when solver quits
 0.9.6: Suport for quoated symbols and recursive functions
 0.9.5: Expose `loadString`
 0.9.4: Add `toInt` and `toReal`
diff --git a/SimpleSMT.hs b/SimpleSMT.hs
--- a/SimpleSMT.hs
+++ b/SimpleSMT.hs
@@ -7,6 +7,7 @@
     -- * Basic Solver Interface
     Solver(..)
   , newSolver
+  , newSolverNotify
   , ackCommand
   , simpleCommand
   , simpleCommandMaybe
@@ -151,7 +152,7 @@
 import System.Exit(ExitCode)
 import qualified Control.Exception as X
 import Control.Concurrent(forkIO)
-import Control.Monad(forever,when)
+import Control.Monad(forever,when,void)
 import Text.Read(readMaybe)
 import Data.Ratio((%), numerator, denominator)
 import Numeric(showHex, readHex, showFFloat)
@@ -254,7 +255,15 @@
              [String]     {- ^ Arguments -}             ->
              Maybe Logger {- ^ Optional logging here -} ->
              IO Solver
-newSolver exe opts mbLog =
+newSolver n xs l = newSolverNotify n xs l Nothing
+
+newSolverNotify ::
+  String        {- ^ Executable -}            ->
+  [String]      {- ^ Arguments -}             ->
+  Maybe Logger  {- ^ Optional logging here -} ->
+  Maybe (ExitCode -> IO ()) {- ^ Do this when the solver exits -} ->
+  IO Solver
+newSolverNotify exe opts mbLog mbOnExit =
   do (hIn, hOut, hErr, h) <- runInteractiveProcess exe opts Nothing Nothing
 
      let info a = case mbLog of
@@ -265,6 +274,10 @@
                                info ("[stderr] " ++ errs))
                     `X.catch` \X.SomeException {} -> return ()
 
+     case mbOnExit of
+       Nothing -> pure ()
+       Just this -> void (forkIO (this =<< waitForProcess h))
+
      getResponse <-
        do txt <- hGetContents hOut                  -- Read *all* output
           ref <- newIORef (unfoldr readSExpr txt)  -- Parse, and store result
@@ -288,6 +301,7 @@
 
          stop =
            do cmd (List [Atom "exit"])
+                `X.catch` (\X.SomeException{} -> pure ())
               ec <- waitForProcess h
               X.catch (do hClose hIn
                           hClose hOut
diff --git a/simple-smt.cabal b/simple-smt.cabal
--- a/simple-smt.cabal
+++ b/simple-smt.cabal
@@ -1,5 +1,5 @@
 name:                simple-smt
-version:             0.9.6
+version:             0.9.7
 synopsis:            A simple way to interact with an SMT solver process.
 description:         A simple way to interact with an SMT solver process.
 license:             BSD3