diff --git a/CHANGELOG.md b/CHANGELOG.md
index 6073b0d6..18112e88 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,5 +1,10 @@
 # CHANGES
 
+## 0.9
+
+- feat: allow the theory to ask for some literals to be decided on
+- feat: allow to set the default polarity of variables at creation time
+
 ## 0.8.3
 
 - support containers 3.0
diff --git a/msat-bin.opam b/msat-bin.opam
index a1224fc5..99259285 100644
--- a/msat-bin.opam
+++ b/msat-bin.opam
@@ -2,7 +2,7 @@ opam-version: "2.0"
 name: "msat-bin"
 synopsis: "SAT solver binary based on the msat library"
 license: "Apache"
-version: "0.8.3"
+version: "0.9"
 author: ["Simon Cruanes" "Guillaume Bury"]
 maintainer: ["guillaume.bury@gmail.com" "simon.cruanes.2007@m4x.org"]
 build: [
diff --git a/msat.opam b/msat.opam
index b3d1bd80..8b99d2b8 100644
--- a/msat.opam
+++ b/msat.opam
@@ -2,7 +2,7 @@ opam-version: "2.0"
 name: "msat"
 synopsis: "Library containing a SAT solver that can be parametrized by a theory"
 license: "Apache"
-version: "0.8.3"
+version: "0.9"
 author: ["Simon Cruanes" "Guillaume Bury"]
 maintainer: ["guillaume.bury@gmail.com" "simon.cruanes.2007@m4x.org"]
 build: [