diff --git a/CHANGELOG.md b/CHANGELOG.md
new file mode 100644
--- /dev/null
+++ b/CHANGELOG.md
@@ -0,0 +1,3 @@
+# v0.2
+- make test-suite compatible with `smtlib-backends-0.2`
+- add usage examples in the test-suite
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-z3.cabal b/smtlib-backends-z3.cabal
new file mode 100644
--- /dev/null
+++ b/smtlib-backends-z3.cabal
@@ -0,0 +1,68 @@
+name:               smtlib-backends-z3
+version:            0.2
+synopsis:           An SMT-LIB backend implemented using Z3's C API.
+description:
+  This library implements an SMT-LIB backend (in the sense of the smtlib-backends
+  package) using inlined calls to Z3's C API. It is thus in particular faster
+  than the standard backends relying on running solvers as external processes, as
+  the OS doesn't need to spawn processes and handle pipes between them.
+
+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
+  subdir:   smtlib-backends-z3
+
+source-repository this
+  type:     git
+  location: https://github.com/tweag/smtlib-backends
+  tag:      0.2
+  subdir:   smtlib-backends-z3
+
+library
+  hs-source-dirs:   src
+  ghc-options:      -Wall -Wunused-packages
+  exposed-modules:  SMTLIB.Backends.Z3
+  build-depends:
+      base             >=4.14    && <4.17.0
+    , bytestring       >=0.10.12 && <0.11
+    , containers       >=0.6.4   && <0.7
+    , inline-c         >=0.9.1   && <0.10
+    , smtlib-backends  >=0.2     && <0.3
+
+  -- inspired from haskell-z3
+  if (os(osx) || os(windows))
+    extra-libraries: z3
+
+  else
+    extra-libraries:
+      gomp
+      z3
+      gomp
+
+  default-language: Haskell2010
+
+test-suite test
+  type:             exitcode-stdio-1.0
+  hs-source-dirs:   tests
+  main-is:          Main.hs
+  other-modules:    Examples
+  ghc-options:      -threaded -Wall -Wunused-packages
+  build-depends:
+      base
+    , bytestring
+    , smtlib-backends
+    , smtlib-backends-tests
+    , smtlib-backends-z3
+    , tasty
+    , tasty-hunit
+
+  default-language: Haskell2010
diff --git a/src/SMTLIB/Backends/Z3.hs b/src/SMTLIB/Backends/Z3.hs
new file mode 100644
--- /dev/null
+++ b/src/SMTLIB/Backends/Z3.hs
@@ -0,0 +1,103 @@
+{-# LANGUAGE EmptyDataDecls #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE QuasiQuotes #-}
+{-# LANGUAGE TemplateHaskell #-}
+
+-- | A module providing a backend that sends commands to Z3 using its C API.
+module SMTLIB.Backends.Z3
+  ( Handle,
+    new,
+    close,
+    with,
+    toBackend,
+  )
+where
+
+import Control.Exception (bracket)
+import Data.ByteString.Builder.Extra
+  ( defaultChunkSize,
+    smallChunkSize,
+    toLazyByteStringWith,
+    untrimmedStrategy,
+  )
+import qualified Data.ByteString.Char8 as BS
+import qualified Data.ByteString.Lazy.Char8 as LBS
+import qualified Data.Map as M
+import Foreign.ForeignPtr (ForeignPtr, finalizeForeignPtr, newForeignPtr)
+import Foreign.Ptr (Ptr)
+import qualified Language.C.Inline as C
+import qualified Language.C.Inline.Context as C
+import qualified Language.C.Inline.Unsafe as CU
+import qualified Language.C.Types as C
+import SMTLIB.Backends (Backend (..))
+
+data LogicalContext
+
+C.context
+  ( C.baseCtx
+      <> C.fptrCtx
+      <> C.bsCtx
+      <> mempty
+        { C.ctxTypesTable =
+            M.singleton (C.TypeName "Z3_context") [t|Ptr LogicalContext|]
+        }
+  )
+C.include "z3.h"
+
+data Handle = Handle
+  { -- | A black-box representing the internal state of the solver.
+    context :: ForeignPtr LogicalContext
+  }
+
+-- | Create a new solver instance.
+new :: IO Handle
+new = do
+  let ctxFinalizer =
+        [C.funPtr| void free_context(Z3_context ctx) {
+                 Z3_del_context(ctx);
+                 } |]
+
+  {-
+  We set the error handler to ignore errors. That way if an error happens it doesn't
+  cause the whole program to crash, and the error message is simply transmitted to
+  the Haskell layer inside the output of the 'send' method.
+  -}
+  ctx <-
+    newForeignPtr ctxFinalizer
+      =<< [CU.block| Z3_context {
+                 Z3_config cfg = Z3_mk_config();
+                 Z3_context ctx = Z3_mk_context(cfg);
+                 Z3_del_config(cfg);
+
+                 void ignore_error(Z3_context c, Z3_error_code e) {}
+                 Z3_set_error_handler(ctx, ignore_error);
+
+                 return ctx;
+                 } |]
+  return $ Handle ctx
+
+-- | Release the resources associated with a Z3 instance.
+close :: Handle -> IO ()
+close = finalizeForeignPtr . context
+
+-- | Create a Z3 instance, use it to run a computation and release its resources.
+with :: (Handle -> IO a) -> IO a
+with = bracket new close
+
+-- | Create a solver backend out of a Z3 instance.
+toBackend :: Handle -> Backend
+toBackend handle =
+  Backend $ \cmd -> do
+    let ctx = context handle
+    let cmd' =
+          LBS.toStrict $
+            toLazyByteStringWith
+              (untrimmedStrategy smallChunkSize defaultChunkSize)
+              "\NUL"
+              cmd
+    LBS.fromStrict
+      <$> ( BS.packCString
+              =<< [CU.exp| const char* {
+               Z3_eval_smtlib2_string($fptr-ptr:(Z3_context ctx), $bs-ptr:cmd')
+               }|]
+          )
diff --git a/tests/Examples.hs b/tests/Examples.hs
new file mode 100644
--- /dev/null
+++ b/tests/Examples.hs
@@ -0,0 +1,29 @@
+{-# LANGUAGE OverloadedStrings #-}
+
+module Examples (examples) where
+
+import SMTLIB.Backends (command, initSolver)
+import qualified SMTLIB.Backends.Z3 as Z3
+import Test.Tasty
+import Test.Tasty.HUnit
+
+-- | The examples for the 'Z3' backend (using Z3 as a library).
+examples :: [TestTree]
+examples =
+  [testCase "basic use" basicUse]
+
+-- | Basic use of the 'Z3' backend.
+basicUse :: IO ()
+basicUse =
+  -- 'Z3.with' runs a computation using the 'Z3' backend
+  Z3.with $ \handle -> do
+    -- first, we make the z3 handle into an actual backend
+    let backend = Z3.toBackend handle
+    -- then, we create a solver out of the backend
+    -- we enable queuing (it's faster !)
+    solver <- initSolver backend True
+    -- we send a basic command to the solver and ignore the response
+    -- we can write the command as a simple string because we have enabled the
+    -- OverloadedStrings pragma
+    _ <- command solver "(get-info :name)"
+    return ()
diff --git a/tests/Main.hs b/tests/Main.hs
new file mode 100644
--- /dev/null
+++ b/tests/Main.hs
@@ -0,0 +1,26 @@
+{-# LANGUAGE OverloadedStrings #-}
+
+import qualified Data.ByteString.Lazy.Char8 as LBS
+import Examples (examples)
+import SMTLIB.Backends
+import SMTLIB.Backends.Tests
+import qualified SMTLIB.Backends.Z3 as Z3
+import Test.Tasty
+import Test.Tasty.HUnit
+
+main :: IO ()
+main = do
+  defaultMain $
+    testGroup "Tests" $
+      [ testBackend "Basic examples" validSources z3,
+        testGroup "API usage examples" examples,
+        testBackend "Error handling" failingSources z3
+      ]
+  where
+    z3 todo = Z3.with $ todo . Z3.toBackend
+    validSources = filter (\source -> name source `notElem` ["assertions", "unsat cores"]) sources
+    failingSources =
+      [ Source "invalid command" $ \solver -> do
+          result <- command solver "this is not a valid command!!!"
+          assertBool ("Expecting error message, got: " ++ LBS.unpack result) $ "(error" `LBS.isPrefixOf` result
+      ]