diff --git a/SimpleSMT.hs b/SimpleSMT.hs
--- a/SimpleSMT.hs
+++ b/SimpleSMT.hs
@@ -166,6 +166,7 @@
 import Text.Read(readMaybe)
 import Data.Ratio((%), numerator, denominator)
 import Numeric(showHex, readHex, showFFloat)
+import System.Mem.Weak(addFinalizer)
 
 
 -- | Results of checking for satisfiability.
@@ -319,63 +320,75 @@
           }) =
   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.
+     addFinalizer responses (closeHandle hIn)
 
-         cleanup =
-           X.catch (do hClose hIn
-                       hClose hOut
-                       hClose hErr)
-                   (solverLogExcn log)
+     let solver =
+           Solver
+             { command = runCommand hIn responses
+             , stop = stopSolver hIn exitResult
+             , forceStop = 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
 
 -- | 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
 synopsis:            A simple way to interact with an SMT solver process.
 description:         A simple way to interact with an SMT solver process.
 license:             BSD3