diff --git a/CHANGELOG.md b/CHANGELOG.md
new file mode 100644
--- /dev/null
+++ b/CHANGELOG.md
@@ -0,0 +1,11 @@
+see also the changelogs of `smtlib-backends-tests`, `smtlib-backends-process` and 
+`smtlib-backends-z3`
+
+# v0.2
+- split the `Process` module into its own library
+- rename `SMTLIB.Backends`'s `ackCommand` to `command_`
+- remove logging abilities
+  - the user can always surround `command` or `command_` with their own logging
+    functions
+- improve read-me
+
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,21 @@
+MIT License
+
+Copyright (c) Tweag I/O Limited.
+
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to deal
+in the Software without restriction, including without limitation the rights
+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all
+copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+SOFTWARE.
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,3 @@
+import Distribution.Simple
+
+main = defaultMain
diff --git a/smtlib-backends.cabal b/smtlib-backends.cabal
new file mode 100644
--- /dev/null
+++ b/smtlib-backends.cabal
@@ -0,0 +1,39 @@
+name:               smtlib-backends
+version:            0.2
+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.
+
+license:            MIT
+license-file:       LICENSE
+author:             Quentin Aristote
+maintainer:         quentin.aristote@tweag.io
+build-type:         Simple
+category:           SMT
+cabal-version:      >=1.10
+extra-source-files: CHANGELOG.md
+
+source-repository head
+  type:     git
+  location: https://github.com/tweag/smtlib-backends
+
+source-repository this
+  type:     git
+  location: https://github.com/tweag/smtlib-backends
+  tag:      0.2
+
+library
+  hs-source-dirs:   src
+  ghc-options:      -Wall -Wunused-packages
+  exposed-modules:  SMTLIB.Backends
+  other-extensions: Safe
+  build-depends:
+      base        >=4.14    && <4.17.0
+    , bytestring  >=0.10.12 && <0.11
+
+  default-language: Haskell2010
diff --git a/src/SMTLIB/Backends.hs b/src/SMTLIB/Backends.hs
new file mode 100644
--- /dev/null
+++ b/src/SMTLIB/Backends.hs
@@ -0,0 +1,128 @@
+{-# LANGUAGE OverloadedStrings #-}
+
+module SMTLIB.Backends (Backend (..), Solver, initSolver, command, command_) where
+
+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.List (intersperse)
+import Prelude hiding (log)
+
+-- | The type of solver backends. SMTLib2 commands are sent to a backend which
+-- processes them and outputs the solver's response.
+data Backend = Backend
+  { -- | Send a command to the backend.
+    send :: Builder -> IO LBS.ByteString
+  }
+
+type Queue = IORef Builder
+
+-- | 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, ())
+
+-- | 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)
+
+-- | 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 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.
+--
+-- 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.
+data Solver = Solver
+  { -- | The backend processing the commands.
+    backend :: Backend,
+    -- | An optional queue to write commands that are to be sent to the solver lazily.
+    queue :: Maybe Queue
+  }
+
+-- | 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.
+initSolver ::
+  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
+  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
+      setOption solver "print-success" "true"
+  setOption solver "produce-models" "true"
+  return solver
+
+-- | 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.
+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
+
+-- | 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.
+command_ :: Solver -> Builder -> IO ()
+command_ solver cmd =
+  case queue solver of
+    Nothing -> do
+      res <- send (backend solver) cmd
+      if trim res == "success"
+        then return ()
+        else
+          fail $
+            unlines
+              [ "Unexpected result from the SMT solver:",
+                "  Expected: success",
+                "  Got: " ++ show res
+              ]
+    Just q -> putQueue q cmd
+  where
+    trim = LBS.dropWhile isSpace . LBS.reverse . LBS.dropWhile isSpace . LBS.reverse
+
+setOption :: Solver -> Builder -> Builder -> IO ()
+setOption solver name value = command_ solver $ list ["set-option", ":" <> name, value]
+
+list :: [Builder] -> Builder
+list bs = "(" <> mconcat (intersperse " " bs) <> ")"