diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -3,6 +3,15 @@
 All notable changes to the smtlib-backends-z3 library will be documented in this
 file.
 
+## next
+
+### Added
+
+## v0.3.1 _(2024-01-29)_
+
+### Added
+- note about `Z3.Config` limitations
+
 ## v0.3 _(2023-02-03)_
 
 ### Added
diff --git a/smtlib-backends-z3.cabal b/smtlib-backends-z3.cabal
--- a/smtlib-backends-z3.cabal
+++ b/smtlib-backends-z3.cabal
@@ -1,5 +1,5 @@
 name:               smtlib-backends-z3
-version:            0.3
+version:            0.3.1
 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
@@ -10,7 +10,9 @@
 license:            MIT
 license-file:       LICENSE
 author:             Quentin Aristote
-maintainer:         quentin.aristote@tweag.io
+maintainer:
+  facundo.dominguez@tweag.io, gabriel.hondet@tweag.io, mathieu.montin@tweag.io
+
 build-type:         Simple
 category:           SMT
 cabal-version:      >=1.10
@@ -29,12 +31,12 @@
 
 library
   hs-source-dirs:   src
-  c-sources: cbits/z3.c
+  c-sources:        cbits/z3.c
   ghc-options:      -Wall -Wunused-packages
   exposed-modules:  SMTLIB.Backends.Z3
   build-depends:
-      base             >=4.14    && <4.18
-    , bytestring       >=0.10.12 && <0.12
+      base             >=4.14    && <4.20
+    , bytestring       >=0.10.12 && <0.13
     , smtlib-backends  >=0.3     && <0.4
 
   -- inspired from haskell-z3
diff --git a/src/SMTLIB/Backends/Z3.hs b/src/SMTLIB/Backends/Z3.hs
--- a/src/SMTLIB/Backends/Z3.hs
+++ b/src/SMTLIB/Backends/Z3.hs
@@ -40,6 +40,19 @@
   { -- | A list of options to set during the solver's initialization.
     -- Each pair is of the form @(paramId, paramValue)@, e.g.
     -- @(":produce-models", "true")@.
+    --
+    -- Note that Z3 has different kinds of parameters, and not all of
+    -- them can be set here. In particular, there are the so called
+    -- global and module parameters with a value that affects
+    -- all solver instances. We have found some of these global
+    -- parameters to be ignored when provided here. You might have more
+    -- luck setting them after starting the solver:
+    --
+    -- > command_ solver "(set-option :parameter_name value)"
+    --
+    -- Or using `Z3_global_param_set` from the Z3 API directly.
+    --
+    -- > foreign import capi unsafe "z3.h Z3_global_param_set" c_Z3_global_param_set :: CString -> CString -> IO ()
     parameters :: [(BS.ByteString, BS.ByteString)]
   }
 
diff --git a/tests/Examples.hs b/tests/Examples.hs
--- a/tests/Examples.hs
+++ b/tests/Examples.hs
@@ -38,26 +38,38 @@
 -- | How to set options at initialization time.
 settingOptions :: IO ()
 settingOptions =
+  Z3.with (Z3.Config [("dump_models2", "true")])
+  -- (Z3.Config [(":produce-unsat-cores", "true")])
+  $
+    \handle2 ->
+      initSolver NoQueuing (Z3.toBackend handle2) >>= \solver2 ->
+
   -- the Z3 C API is special (as a backend) in that some of its options can only be
   -- set when the object representing the state of the solver is created
   -- hence the 'Z3.new' and 'Z3.with' functions allow for setting options at
   -- initialization time
-  Z3.with Z3.defaultConfig
+  Z3.with (Z3.Config [])
   -- (Z3.Config [(":produce-unsat-cores", "true")])
-  $
+   $
     \handle -> do
       -- we don't enable queuing so that commands are checked for correctness
       solver <- initSolver NoQueuing (Z3.toBackend handle)
       -- this is for example the case of the @:produce-assertions@ parameter, and not
       -- the case of the @:print-success@ one
       command_ solver "(set-option :print-success true)"
+ --     command_ solver2 "(set-option :dump_models true)"
+ --     command_ solver "(set-option :dump_models true)"
       -- the following would fail, returning
       -- @
       -- (error "line 1 column 33: error setting ':produce-unsat-cores',
       --         option value cannot be modified after initialization")
       -- @
-      result <- command solver "(set-option :produce-unsat-cores true)"
-      assertBool ("Expecting error message, got: " ++ LBS.unpack result) $ "(error" `LBS.isPrefixOf` result
+--      result <- command solver "(set-option :produce-unsat-cores true)"
+--      assertBool ("Expecting error message, got: " ++ LBS.unpack result) $ "(error" `LBS.isPrefixOf` result
+      command_ solver "(declare-fun x () Int)"
+      command_ solver "(assert (= x 10))"
+      r <- command solver "(check-sat)"
+      print r
       return ()
 
 -- | An example on how to force the content of the queue to be evaluated.