diff --git a/CHANGES b/CHANGES
--- a/CHANGES
+++ b/CHANGES
@@ -1,3 +1,5 @@
+1.0.1: Fix premature solver finalization in optimized code
+1.0:   Stop the external solver when the Solver object is garbage collected
 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`
diff --git a/SimpleSMT.hs b/SimpleSMT.hs
--- a/SimpleSMT.hs
+++ b/SimpleSMT.hs
@@ -166,6 +166,9 @@
 import Text.Read(readMaybe)
 import Data.Ratio((%), numerator, denominator)
 import Numeric(showHex, readHex, showFFloat)
+import Foreign.Concurrent(newForeignPtr)
+import Foreign.ForeignPtr(withForeignPtr)
+import Foreign.Ptr(nullPtr)
 
 
 -- | Results of checking for satisfiability.
@@ -319,63 +322,78 @@
           }) =
   do (hIn, hOut, hErr, h) <- runInteractiveProcess exe opts Nothing Nothing
 
+     -- Drain stderr
      _ <- forkIO $ forever (do errs <- hGetLine hErr
                                solverLogStdErr log errs)
                     `X.catch` \X.SomeException {} -> return ()
 
-     getResponse <-
-       do txt <- hGetContents hOut                  -- Read *all* output
-          ref <- newIORef (unfoldr readSExpr txt)  -- Parse, and store result
-          return $ atomicModifyIORef ref $ \xs ->
-                      case xs of
-                        []     -> (xs, Nothing)
-                        y : ys -> (ys, Just y)
+     -- Parse responses (lazy)
+     txt <- hGetContents hOut                       -- Read *all* output
+     responses <- newIORef (unfoldr readSExpr txt) -- Parse, and store result
 
-     let cmd c = do let txt = showsSExpr c ""
-                    solverLogSend log c
-                    hPutStrLn hIn txt
-                    hFlush hIn
+     -- Wait for the solver to exit
+     exitResult <- newEmptyMVar
+     _ <- forkFinally
+            (observeExit h hIn hOut hErr)
+            (putMVar exitResult)
 
-         command c =
-           do cmd c
-              mb <- getResponse
-              case mb of
-                Just res -> do solverLogRecv log res
-                               return res
-                Nothing  -> fail "Missing response from solver"
+     -- Close `stdin` when the Haskell Solver object is GC-ed, so that
+     -- we close `stdin` and the solver process exits.
+     finalizer <- newForeignPtr nullPtr (closeHandle hIn)
 
-         cleanup =
-           X.catch (do hClose hIn
-                       hClose hOut
-                       hClose hErr)
-                   (solverLogExcn log)
+     let solver =
+           Solver
+             { command = keepAlive finalizer . runCommand hIn responses
+             , stop = keepAlive finalizer (stopSolver hIn exitResult)
+             , forceStop = keepAlive finalizer (forceStopSolver h exitResult)
+             }
 
-         observeExit =
-           do ec <- waitForProcess h
-              (case mbOnExit of
-                 Nothing -> pure ()
-                 Just this -> this ec)
-                `X.finally` cleanup
-              return ec
+     setOption solver ":print-success" "true"
+     setOption solver ":produce-models" "true"
 
-     exitResult <- newEmptyMVar
-     _ <- forkFinally observeExit (putMVar exitResult)
+     return solver
+  where
+  send hIn c =
+    do let txt = showsSExpr c ""
+       solverLogSend log c
+       hPutStrLn hIn txt
+       hFlush hIn
 
-     let waitForExit = either X.throwIO pure =<< readMVar exitResult
+  runCommand hIn responses c =
+    do send hIn c
+       mb <- atomicModifyIORef responses $ \xs ->
+               case xs of
+                 []     -> (xs, Nothing)
+                 y : ys -> (ys, Just y)
+       case mb of
+         Just res -> do solverLogRecv log res
+                        return res
+         Nothing  -> fail "Missing response from solver"
 
-         forceStop = terminateProcess h *> waitForExit
+  closeHandle handle =
+    X.catch (hClose handle) (solverLogExcn log)
 
-         stop =
-           do cmd (List [Atom "exit"])
-                `X.catch` (\X.SomeException{} -> pure ())
-              waitForExit
+  observeExit h hIn hOut hErr =
+    do ec <- waitForProcess h
+       (case mbOnExit of
+          Nothing -> pure ()
+          Just this -> this ec)
+         `X.finally` mapM_ closeHandle [hIn, hOut, hErr]
+       return ec
 
-         solver = Solver { .. }
+  waitForExit exitResult =
+    either X.throwIO pure =<< readMVar exitResult
 
-     setOption solver ":print-success" "true"
-     setOption solver ":produce-models" "true"
+  forceStopSolver h exitResult =
+    terminateProcess h *> waitForExit exitResult
 
-     return solver
+  stopSolver hIn exitResult =
+    do send hIn (List [Atom "exit"])
+         `X.catch` (\X.SomeException{} -> pure ())
+       waitForExit exitResult
+
+  keepAlive finalizer action =
+    withForeignPtr finalizer (\_ -> action)
 
 -- | Options for configuring how to start, stop, and interact with an SMT
 -- solver process.
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.9
+version:             1.0.1
 synopsis:            A simple way to interact with an SMT solver process.
 description:         A simple way to interact with an SMT solver process.
 license:             BSD3
@@ -24,6 +24,14 @@
   main-is: DiffSEXp.hs
   hs-source-dirs: exe
   build-depends: base, containers, simple-smt, simple-get-opt
+
+test-suite finalizer
+  type: exitcode-stdio-1.0
+  default-language: Haskell2010
+  main-is: Finalizer.hs
+  hs-source-dirs: test
+  ghc-options: -threaded
+  build-depends: base, simple-smt
 
 source-repository head
   type: git
diff --git a/test/Finalizer.hs b/test/Finalizer.hs
new file mode 100644
--- /dev/null
+++ b/test/Finalizer.hs
@@ -0,0 +1,142 @@
+{-# OPTIONS_GHC -O2 #-}
+
+module Main (main) where
+
+import Control.Concurrent.MVar
+  ( MVar, newEmptyMVar, putMVar, takeMVar )
+import Control.Exception (evaluate)
+import Control.Monad (unless, when)
+import System.Environment (getArgs, getExecutablePath)
+import System.Exit (ExitCode)
+import System.IO (hFlush, hPutStrLn, isEOF, stderr, stdout)
+import System.Mem (performGC)
+import System.Timeout (timeout)
+
+import SimpleSMT
+
+
+eofMessage :: String
+eofMessage = "fake solver: stdin closed"
+
+
+prematureFinalizerWindow :: Int
+prematureFinalizerWindow = 50000
+
+
+operationTimeout :: Int
+operationTimeout = 2000000
+
+
+main :: IO ()
+main =
+  do args <- getArgs
+     case args of
+       ["--solver"] -> fakeSolver
+       _ -> testFinalizer
+
+
+testFinalizer :: IO ()
+testFinalizer =
+  do exe <- getExecutablePath
+
+     -- Keeping projected Solver operations alive must keep the external
+     -- process alive too.
+     progress "Test 1: live solver operations prevent finalization"
+     exited <- newEmptyMVar
+     solver <- within "starting the first solver" $
+       newSolverNotify exe ["--solver"] Nothing
+         (Just (\ec ->
+                  do progress ("First solver exited: " ++ show ec)
+                     putMVar exited ec))
+     run <- evaluate (command solver)
+     finish <- evaluate (stop solver)
+
+     progress "  Forcing GC while projected operations are still live"
+     performGC
+
+     prematureExit <- timeout prematureFinalizerWindow (takeMVar exited)
+     case prematureExit of
+       Just _ -> fail "Solver finalizer ran while its operations were live"
+       Nothing -> progress "  Solver remained alive"
+
+     progress "  Sending check-sat after GC"
+     result <- within "waiting for check-sat" $
+       run (List [Atom "check-sat"])
+     unless (result == Atom "sat") $
+       fail ("Unexpected check-sat response: " ++ show result)
+     progress "  Stopping the first solver explicitly"
+     _ <- within "stopping the first solver" finish
+
+     -- Once the Solver and its operations are unreachable, its finalizer
+     -- must close stdin and allow the external process to exit.
+     progress "Test 2: unreachable solver is finalized"
+     finalized <- newEmptyMVar
+     sawEOF <- newEmptyMVar
+     within "using the second solver" $
+       useAndForgetSolver exe sawEOF finalized
+     progress "  Dropped the solver; forcing GC"
+     performGC
+
+     finalResult <- timeout operationTimeout $
+       do takeMVar sawEOF
+          takeMVar finalized
+     case finalResult of
+       Just _ -> progress "  Solver observed EOF and exited"
+       Nothing ->
+         fail "Solver finalizer did not close stdin and terminate the process"
+
+     progress "Finalizer tests passed"
+
+
+{-# NOINLINE useAndForgetSolver #-}
+useAndForgetSolver :: FilePath -> MVar () -> MVar ExitCode -> IO ()
+useAndForgetSolver exe sawEOF exited =
+  do let logger =
+           noSolverLogger
+             { solverLogStdErr = \message ->
+                 when (message == eofMessage) $
+                   do progress "  Fake solver observed EOF"
+                      putMVar sawEOF ()
+             }
+         config =
+           (defaultConfig exe ["--solver"])
+             { solverOnExit =
+                 Just (\ec ->
+                         do progress ("  Second solver exited: " ++ show ec)
+                            putMVar exited ec)
+             , solverLogger = logger
+             }
+     solver <- newSolverWithConfig config
+     result <- command solver (List [Atom "check-sat"])
+     unless (result == Atom "sat") $
+       fail ("Unexpected check-sat response: " ++ show result)
+
+
+fakeSolver :: IO ()
+fakeSolver =
+  do eof <- isEOF
+     if eof
+       then hPutStrLn stderr eofMessage
+       else do request <- getLine
+               case request of
+                 "(exit)" -> pure ()
+                 "(check-sat)" -> respond "sat" >> fakeSolver
+                 _ -> respond "success" >> fakeSolver
+  where
+  respond response =
+    do putStrLn response
+       hFlush stdout
+
+
+within :: String -> IO a -> IO a
+within description action =
+  do result <- timeout operationTimeout action
+     case result of
+       Just value -> pure value
+       Nothing -> fail ("Timed out " ++ description)
+
+
+progress :: String -> IO ()
+progress message =
+  do putStrLn message
+     hFlush stdout