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,7 +166,9 @@
 import Text.Read(readMaybe)
 import Data.Ratio((%), numerator, denominator)
 import Numeric(showHex, readHex, showFFloat)
-import System.Mem.Weak(addFinalizer)
+import Foreign.Concurrent(newForeignPtr)
+import Foreign.ForeignPtr(withForeignPtr)
+import Foreign.Ptr(nullPtr)
 
 
 -- | Results of checking for satisfiability.
@@ -337,13 +339,13 @@
 
      -- Close `stdin` when the Haskell Solver object is GC-ed, so that
      -- we close `stdin` and the solver process exits.
-     addFinalizer responses (closeHandle hIn)
+     finalizer <- newForeignPtr nullPtr (closeHandle hIn)
 
      let solver =
            Solver
-             { command = runCommand hIn responses
-             , stop = stopSolver hIn exitResult
-             , forceStop = forceStopSolver h exitResult
+             { command = keepAlive finalizer . runCommand hIn responses
+             , stop = keepAlive finalizer (stopSolver hIn exitResult)
+             , forceStop = keepAlive finalizer (forceStopSolver h exitResult)
              }
 
      setOption solver ":print-success" "true"
@@ -389,6 +391,9 @@
     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:             1.0
+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