diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,11 +1,40 @@
-see also the changelogs of `smtlib-backends-tests`, `smtlib-backends-process` and 
-`smtlib-backends-z3`
+# Changelog
 
-# v0.2
+All notable changes to the smtlib-backends library will be documented in this
+file.
+
+The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/),
+and this project adheres to [PVP versioning](https://pvp.haskell.org/).
+
+The same stands for the changelogs of
+[smtlib-backends-tests](smtlib-backends-tests/CHANGELOG.md),
+[smtlib-backends-process](smtlib-backends-process/CHANGELOG.md) and
+[smtlib-backends-z3](smtlib-backends-z3/CHANGELOG.md), except the version
+numbers simply follow that of `smtlib-backends`.
+
+## v0.3 _(2023-02-03)_
+
+### Added
+- **(breaking change)** add a datatype `Backends.QueuingFlag` to set the queuing
+  mode
+  - the `initSolver` function now takes this datatype as argument instead of a
+    boolean
+- **(breaking change)** add a `send_` method to the `Backends.Backend` datatype
+  for sending commands with no output
+- add a `Backends.flushQueue` function for forcing the content of the queue to
+  be evaluated
+
+### Changed
+- **(breaking change)** make the queuing functions thread-unsafe but faster
+
+## v0.2 _(2022-12-16)_
+
+### Changed
 - split the `Process` module into its own library
 - rename `SMTLIB.Backends`'s `ackCommand` to `command_`
+- improve read-me
+
+### Removed
 - remove logging abilities
   - the user can always surround `command` or `command_` with their own logging
     functions
-- improve read-me
-
diff --git a/smtlib-backends.cabal b/smtlib-backends.cabal
--- a/smtlib-backends.cabal
+++ b/smtlib-backends.cabal
@@ -1,13 +1,13 @@
 name:               smtlib-backends
-version:            0.2
+version:            0.3
 synopsis:
   Low-level functions for SMT-LIB-based interaction with SMT solvers. 
 
 description:
   This library provides an extensible interface for interacting with SMT solvers
-  using SMT-LIB. The smtlib-backends-process provides a backend that runs solvers
-  as external processes, and the smtlib-backends-z3 package provides a backend that
-  uses inlined calls to Z3's C API.
+  using SMT-LIB. The smtlib-backends-process package provides a backend that
+  runs solvers as external processes, and the smtlib-backends-z3 package
+  provides a backend that uses inlined calls to Z3's C API.
 
 license:            MIT
 license-file:       LICENSE
@@ -25,7 +25,7 @@
 source-repository this
   type:     git
   location: https://github.com/tweag/smtlib-backends
-  tag:      0.2
+  tag:      0.3
 
 library
   hs-source-dirs:   src
@@ -33,7 +33,7 @@
   exposed-modules:  SMTLIB.Backends
   other-extensions: Safe
   build-depends:
-      base        >=4.14    && <4.17.0
-    , bytestring  >=0.10.12 && <0.11
+      base        >=4.14    && <4.18
+    , bytestring  >=0.10.12 && <0.12
 
   default-language: Haskell2010
diff --git a/src/SMTLIB/Backends.hs b/src/SMTLIB/Backends.hs
--- a/src/SMTLIB/Backends.hs
+++ b/src/SMTLIB/Backends.hs
@@ -1,11 +1,21 @@
 {-# LANGUAGE OverloadedStrings #-}
 
-module SMTLIB.Backends (Backend (..), Solver, initSolver, command, command_) where
+module SMTLIB.Backends
+  ( Backend (..),
+    QueuingFlag (..),
+    Solver,
+    initSolver,
+    command,
+    command_,
+    flushQueue,
+  )
+where
 
+import Control.Monad ((<=<))
 import Data.ByteString.Builder (Builder)
 import qualified Data.ByteString.Lazy.Char8 as LBS
 import Data.Char (isSpace)
-import Data.IORef (IORef, atomicModifyIORef, newIORef)
+import Data.IORef (IORef, modifyIORef, newIORef, readIORef, writeIORef)
 import Data.List (intersperse)
 import Prelude hiding (log)
 
@@ -13,45 +23,60 @@
 -- processes them and outputs the solver's response.
 data Backend = Backend
   { -- | Send a command to the backend.
-    send :: Builder -> IO LBS.ByteString
+    -- While the implementation depends on the backend, this function is usually
+    -- *not* thread-safe.
+    send :: Builder -> IO LBS.ByteString,
+    -- | Send a command that doesn't produce any response to the backend.
+    -- The backend may implement this by not reading the output and leaving it
+    -- for a later read, or reading the output and discarding it immediately.
+    -- Hence this method should only be used when the command does not produce
+    -- any response to be outputted.
+    -- Again, this function may not be thread-safe.
+    send_ :: Builder -> IO ()
   }
 
 type Queue = IORef Builder
 
+-- | A boolean-equivalent datatype indicating whether to enable queuing.
+data QueuingFlag = Queuing | NoQueuing
+
 -- | Push a command on the solver's queue of commands to evaluate.
 -- The command must not produce any output when evaluated, unless it is the last
 -- command added before the queue is flushed.
-putQueue :: Queue -> Builder -> IO ()
-putQueue q cmd = atomicModifyIORef q $ \cmds ->
-  (cmds <> cmd, ())
+-- For a fixed queue, this function is *not* thread-safe.
+put :: Queue -> Builder -> IO ()
+put q cmd = modifyIORef q (<> cmd)
 
 -- | Empty the queue of commands to evaluate and return its content as a bytestring
 -- builder.
-flushQueue :: Queue -> IO Builder
-flushQueue q = atomicModifyIORef q $ \cmds ->
-  (mempty, cmds)
+-- For a fixed queue, this function is *not* thread-safe.
+flush :: Queue -> IO Builder
+flush q = do
+  cmds <- readIORef q
+  writeIORef q mempty
+  return cmds
 
--- | A solver is essentially a wrapper around a solver backend. It also comes with
--- a function for logging the solver's activity, and an optional queue of commands
--- to send to the backend.
+-- | A solver is essentially a wrapper around a solver backend. It also comes an
+-- optional queue of commands to send to the backend.
 --
--- A solver can either be in eager mode or lazy mode. In eager mode, the queue of
--- commands isn't used and the commands are sent to the backend immediately. In
--- lazy mode, commands whose output are not strictly necessary for the rest of the
--- computation (typically the ones whose output should just be "success") and that
--- are sent through 'command_' are not sent to the backend immediately, but
--- rather written on the solver's queue. When a command whose output is actually
--- necessary needs to be sent, the queue is flushed and sent as a batch to the
--- backend.
+-- A solver can either be in 'Queuing' mode or 'NoQueuing' mode. In 'NoQueuing'
+-- mode, the queue of commands isn't used and the commands are sent to the
+-- backend immediately. In 'Queuing' mode, commands whose output are not
+-- strictly necessary for the rest of the computation (typically the ones whose
+-- output should just be @success@) and that are sent through 'command_' are not
+-- sent to the backend immediately, but rather written on the solver's queue.
+-- When a command whose output is actually necessary needs to be sent, the queue
+-- is flushed and sent as a batch to the backend.
 --
--- Lazy mode should be faster as there usually is a non-negligible constant
--- overhead in sending a command to the backend. But since the commands are sent by
--- batches, a command sent to the solver will only produce an error when the queue
--- is flushed, i.e. when a command with interesting output is sent. You thus
--- probably want to stick with eager mode when debugging. Moreover, when commands
--- are sent by batches, only the last command in the batch may produce an output
--- for parsing to work properly. Hence the ":print-success" option is disabled in
--- lazy mode, and this should not be overriden manually.
+-- 'Queuing' mode should be faster as there usually is a non-negligible constant
+-- overhead in sending a command to the backend. But since the commands are sent
+-- by batches, a command sent to the solver will only produce an error when the
+-- queue is flushed, i.e. when a command with interesting output is sent. You
+-- thus probably want to stick with 'NoQueuing' mode when debugging. Moreover,
+-- when commands are sent by batches, only the last command in the batch may
+-- produce an output for parsing to work properly. Hence the @:print-success@
+-- option is disabled in 'Queuing' mode, and this should not be overriden
+-- manually.
 data Solver = Solver
   { -- | The backend processing the commands.
     backend :: Backend,
@@ -61,29 +86,31 @@
 
 -- | Create a new solver and initialize it with some options so that it behaves
 -- correctly for our use.
--- In particular, the "print-success" option is disabled in lazy mode. This should
--- not be overriden manually.
+-- In particular, the "print-success" option is disabled in 'Queuing' mode. This
+-- should not be overriden manually.
 initSolver ::
+  -- | whether to enable 'Queuing' mode (see 'Solver' for the meaning of this
+  -- flag)
+  QueuingFlag ->
+  -- | the solver backend
   Backend ->
-  -- | whether to enable lazy mode (see 'Solver' for the meaning of this flag)
-  Bool ->
   IO Solver
-initSolver solverBackend lazy = do
-  solverQueue <-
-    if lazy
-      then do
-        ref <- newIORef mempty
-        return $ Just ref
-      else return Nothing
+initSolver queuing solverBackend = do
+  solverQueue <- case queuing of
+    Queuing -> do
+      ref <- newIORef mempty
+      return $ Just ref
+    NoQueuing -> return Nothing
   let solver = Solver solverBackend solverQueue
-  if lazy
-    then return ()
-    else -- this should not be enabled when the queue is used, as it messes with parsing
-    -- the outputs of commands that are actually interesting
-    -- TODO checking for correctness and enabling laziness can be made compatible
-    -- but it would require the solver backends to return several outputs at once
-    -- alternatively, we may consider that the user wanting both features should
-    -- implement their own backend that deals with this
+  case queuing of
+    Queuing -> return ()
+    NoQueuing ->
+      -- this should not be enabled when the queue is used, as it messes with parsing
+      -- the outputs of commands that are actually interesting
+      -- TODO checking for correctness and enabling laziness can be made compatible
+      -- but it would require the solver backends to return several outputs at once
+      -- alternatively, we may consider that the user wanting both features should
+      -- implement their own backend that deals with this
       setOption solver "print-success" "true"
   setOption solver "produce-models" "true"
   return solver
@@ -91,18 +118,20 @@
 -- | Have the solver evaluate a SMT-LIB command.
 -- This forces the queued commands to be evaluated as well, but their results are
 -- *not* checked for correctness.
+-- For a fixed backend, this function is *not* thread-safe.
 command :: Solver -> Builder -> IO LBS.ByteString
 command solver cmd = do
   send (backend solver)
     =<< case queue solver of
-      Nothing -> return $ cmd
-      Just q -> (<> cmd) <$> flushQueue q
+      Nothing -> return cmd
+      Just q -> (<> cmd) <$> flush q
 
 -- | A command with no interesting result.
--- In eager mode, the result is checked for correctness.
--- In lazy mode, (unless the queue is flushed and evaluated
--- right after) the command must not produce any output when evaluated, and
--- its output is thus in particular not checked for correctness.
+-- In 'NoQueuing' mode, the result is checked for correctness. In 'Queuing'
+-- mode, (unless the queue is flushed and evaluated right after) the command
+-- must not produce any output when evaluated, and its output is thus in
+-- particular not checked for correctness. For a fixed backend, this function is
+-- *not* thread-safe.
 command_ :: Solver -> Builder -> IO ()
 command_ solver cmd =
   case queue solver of
@@ -117,9 +146,14 @@
                 "  Expected: success",
                 "  Got: " ++ show res
               ]
-    Just q -> putQueue q cmd
+    Just q -> put q cmd
   where
     trim = LBS.dropWhile isSpace . LBS.reverse . LBS.dropWhile isSpace . LBS.reverse
+
+-- | Force the content of the queue to be sent to the solver.
+-- Only useful in queuing mode, does nothing in non-queuing mode.
+flushQueue :: Solver -> IO ()
+flushQueue solver = maybe (return ()) (send_ (backend solver) <=< flush) $ queue solver
 
 setOption :: Solver -> Builder -> Builder -> IO ()
 setOption solver name value = command_ solver $ list ["set-option", ":" <> name, value]