diff --git a/CHANGELOG.md b/CHANGELOG.md
new file mode 100644
--- /dev/null
+++ b/CHANGELOG.md
@@ -0,0 +1,3 @@
+# v0.2
+- remove `(exit)` commands at the end of sources
+- make library compatible with `smtlib-backends-0.2`
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-tests.cabal b/smtlib-backends-tests.cabal
new file mode 100644
--- /dev/null
+++ b/smtlib-backends-tests.cabal
@@ -0,0 +1,39 @@
+name:               smtlib-backends-tests
+version:            0.2
+synopsis:           Testing SMT-LIB backends.
+description:
+  This library provides common functions and values used for testing SMT-LIB
+  backends, as provided by the smtlib-backends library.
+
+license:            MIT
+license-file:       LICENSE
+author:             Quentin Aristote
+maintainer:         quentin.aristote@tweag.io
+build-type:         Simple
+category:           SMT, Testing
+cabal-version:      >=1.10
+extra-source-files: CHANGELOG.md
+
+source-repository head
+  type:     git
+  location: https://github.com/tweag/smtlib-backends
+  subdir:   smtlib-backends-tests
+
+source-repository this
+  type:     git
+  location: https://github.com/tweag/smtlib-backends
+  tag:      0.2
+  subdir:   smtlib-backends-tests
+
+library
+  ghc-options:      -Wall -Wunused-packages
+  hs-source-dirs:   src
+  exposed-modules:  SMTLIB.Backends.Tests
+  other-modules:    SMTLIB.Backends.Tests.Sources
+  build-depends:
+      base             >=4.14   && <4.17.0
+    , smtlib-backends  >=0.2    && <0.3
+    , tasty            >=1.4.2  && <1.5
+    , tasty-hunit      >=0.10.0 && <0.11
+
+  default-language: Haskell2010
diff --git a/src/SMTLIB/Backends/Tests.hs b/src/SMTLIB/Backends/Tests.hs
new file mode 100644
--- /dev/null
+++ b/src/SMTLIB/Backends/Tests.hs
@@ -0,0 +1,44 @@
+{-# LANGUAGE OverloadedStrings #-}
+
+-- | A module providing functions useful for testing a backend for SimpleSMT.
+module SMTLIB.Backends.Tests
+  ( testBackend,
+    Src.Source (..),
+    Src.sources,
+  )
+where
+
+import SMTLIB.Backends (Backend, command, initSolver)
+import qualified SMTLIB.Backends.Tests.Sources as Src
+import Test.Tasty
+import Test.Tasty.HUnit
+
+-- | Test a backend by using it to run a list of examples.
+testBackend ::
+  -- | The name of the test group.
+  String ->
+  -- | A list of examples on which to run the backend.
+  [Src.Source] ->
+  -- | A function that should create a backend, run a given
+  -- computation and release the backend's resources.
+  ((Backend -> Assertion) -> Assertion) ->
+  TestTree
+testBackend name sources with =
+  testGroup name $ do
+    lazyMode <- [False, True]
+    return $
+      testGroup
+        ( if lazyMode
+            then "lazy"
+            else "eager"
+        )
+        $ do
+          source <- sources
+          return $
+            testCase (Src.name source) $
+              with $ \backend -> do
+                solver <- initSolver backend lazyMode
+                Src.run source solver
+                -- ensure the sources consisting only of queued commands also run
+                _ <- command solver "(get-info :name)"
+                return ()
diff --git a/src/SMTLIB/Backends/Tests/Sources.hs b/src/SMTLIB/Backends/Tests/Sources.hs
new file mode 100644
--- /dev/null
+++ b/src/SMTLIB/Backends/Tests/Sources.hs
@@ -0,0 +1,178 @@
+{-# LANGUAGE OverloadedStrings #-}
+{-# OPTIONS_GHC -Wno-missing-signatures #-}
+
+module SMTLIB.Backends.Tests.Sources (Source (..), sources) where
+
+import SMTLIB.Backends
+
+-- | A source is a list of SMTLib2 commands, available in several different formats
+-- for testing purposes.
+data Source = Source
+  { -- | The name of the source.
+    name :: String,
+    -- | A computation equivalent to sending the raw content of the source to the
+    -- solver.
+    run :: Solver -> IO ()
+  }
+
+-- | A list of examples SMT-LIB files. Most of them were taken from the official
+-- SMT-LIB website:
+-- https://smtlib.cs.uiowa.edu/examples.shtml
+sources =
+  [ assertions,
+    assignments,
+    boolean,
+    info,
+    integerArithmetic,
+    modelingSequentialCodeSSA,
+    modelingSequentialCodeBitvectors,
+    scopes,
+    sorts,
+    unsatCores,
+    valuesOrModels
+  ]
+
+assertions = Source "assertions" $ \solver -> do
+  command_ solver "(set-option :produce-assertions true)"
+  command_ solver "(set-logic QF_UF)"
+  command_ solver "(declare-const p Bool)"
+  command_ solver "(declare-const q Bool)"
+  command_ solver "(push 1)"
+  command_ solver "(assert (or p q))"
+  command_ solver "(push 1)"
+  command_ solver "(assert (not q))"
+  _ <- command solver "(get-assertions)"
+  command_ solver "(pop 1)"
+  _ <- command solver "(get-assertions)"
+  command_ solver "(pop 1)"
+  _ <- command solver "(get-assertions)"
+  return ()
+
+assignments = Source "assignments" $ \solver -> do
+  command_ solver "(set-option :produce-assignments true)"
+  command_ solver "(set-logic QF_UF)"
+  command_ solver "(declare-const p Bool)"
+  command_ solver "(declare-const q Bool)"
+  command_ solver "(declare-const r Bool)"
+  command_ solver "(assert (not (=(! (and (! p :named P) q) :named PQ) (! r :named R))))"
+  _ <- command solver "(check-sat)"
+  _ <- command solver "(get-assignment)"
+  return ()
+
+boolean = Source "boolean" $ \solver -> do
+  command_ solver "(set-logic QF_UF)"
+  command_ solver "(declare-const p Bool)"
+  command_ solver "(assert (and p (not p)))"
+  _ <- command solver "(check-sat)"
+  return ()
+
+info = Source "info" $ \solver -> do
+  _ <- command solver "(get-info :name)"
+  _ <- command solver "(get-info :version )"
+  _ <- command solver "(get-info :authors )"
+  return ()
+
+integerArithmetic = Source "integer arithmetic" $ \solver -> do
+  command_ solver "(set-logic QF_LIA)"
+  command_ solver "(declare-const x Int)"
+  command_ solver "(declare-const y Int)"
+  command_ solver "(assert (= (- x y) (+ x (- y) 1)))"
+  _ <- command solver "(check-sat)"
+  return ()
+
+modelingSequentialCodeSSA = Source "modeling sequential code (SSA)" $ \solver -> do
+  command_ solver "(set-logic QF_UFLIA)"
+  command_ solver "(set-option :produce-models true)"
+  command_ solver "(declare-fun x (Int) Int)"
+  command_ solver "(declare-fun y (Int) Int)"
+  command_ solver "(declare-fun t (Int) Int)"
+  command_ solver "(assert (= (t 0) (x 0)))"
+  command_ solver "(assert (= (y 1) (t 0)))"
+  command_ solver "(assert (= (x 1) (y 1)))"
+
+  command_ solver "(assert (not (and (= (x 1) (y 0)) (= (y 1) (x 0)))))"
+  _ <- command solver "(check-sat)"
+  _ <- command solver "(get-value ((x 0) (y 0) (x 1) (y 1)))"
+  _ <- command solver "(get-model)"
+  return ()
+
+modelingSequentialCodeBitvectors = Source "modeling sequential code (bitvectors)" $
+  \solver -> do
+    command_ solver "(set-logic QF_BV)"
+    command_ solver "(set-option :produce-models true)"
+    command_ solver "(declare-const x_0 (_ BitVec 32))"
+    command_ solver "(declare-const x_1 (_ BitVec 32))"
+    command_ solver "(declare-const x_2 (_ BitVec 32))"
+    command_ solver "(declare-const y_0 (_ BitVec 32))"
+    command_ solver "(declare-const y_1 (_ BitVec 32))"
+    command_ solver "(assert (= x_1 (bvadd x_0 y_0)))"
+    command_ solver "(assert (= y_1 (bvsub x_1 y_0)))"
+    command_ solver "(assert (= x_2 (bvsub x_1 y_1)))"
+    command_ solver "(assert (not (and (= x_2 y_0) (= y_1 x_0))))"
+    _ <- command solver "(check-sat)"
+    return ()
+
+scopes = Source "scopes" $ \solver -> do
+  command_ solver "(set-logic QF_LIA)"
+  command_ solver "(declare-const x Int)"
+  command_ solver "(declare-const y Int)"
+  command_ solver "(assert (= (+ x (* 2 y)) 20))"
+  command_ solver "(push 1)"
+  command_ solver "(assert (= (- x y) 2))"
+  _ <- command solver "(check-sat)"
+  command_ solver "(pop 1)"
+  command_ solver "(push 1)"
+  command_ solver "(assert (= (- x y) 3))"
+  _ <- command solver "(check-sat)"
+  command_ solver "(pop 1)"
+  return ()
+
+sorts = Source "sorts" $ \solver -> do
+  command_ solver "(set-logic QF_UF)"
+  command_ solver "(declare-sort A 0)"
+  command_ solver "(declare-const a A)"
+  command_ solver "(declare-const b A)"
+  command_ solver "(declare-const c A)"
+  command_ solver "(declare-const d A)"
+  command_ solver "(declare-const e A)"
+  command_ solver "(assert (or (= c a)(= c b)))"
+  command_ solver "(assert (or (= d a)(= d b)))"
+  command_ solver "(assert (or (= e a)(= e b)))"
+  command_ solver "(push 1)"
+  command_ solver "(assert (distinct c d))"
+  _ <- command solver "(check-sat)"
+  command_ solver "(pop 1)"
+  command_ solver "(push 1)"
+  command_ solver "(assert (distinct c d e))"
+  _ <- command solver "(check-sat)"
+  command_ solver "(pop 1)"
+  return ()
+
+unsatCores = Source "unsat cores" $ \solver -> do
+  command_ solver "(set-option :produce-unsat-cores true)"
+  command_ solver "(set-logic QF_UF)"
+  command_ solver "(declare-const p Bool)"
+  command_ solver "(declare-const q Bool)"
+  command_ solver "(declare-const r Bool)"
+  command_ solver "(declare-const s Bool)"
+  command_ solver "(declare-const t Bool)"
+  command_ solver "(assert (! (=> p q) :named PQ))"
+  command_ solver "(assert (! (=> q r) :named QR))"
+  command_ solver "(assert (! (=> r s) :named RS))"
+  command_ solver "(assert (! (=> s t) :named ST))"
+  command_ solver "(assert (! (not (=> q s)) :named NQS))"
+  _ <- command solver "(check-sat)"
+  _ <- command solver "(get-unsat-core)"
+  return ()
+
+valuesOrModels = Source "values or models" $ \solver -> do
+  command_ solver "(set-option :produce-models true)"
+  command_ solver "(set-logic QF_LIA)"
+  command_ solver "(declare-const x Int)"
+  command_ solver "(declare-const y Int)"
+  command_ solver "(assert (= (+ x (* 2 y)) 20))"
+  command_ solver "(assert (= (- x y) 2))"
+  _ <- command solver "(check-sat)"
+  _ <- command solver "(get-value (x y))"
+  _ <- command solver "(get-model)"
+  return ()