diff --git a/RELEASE_NOTES.md b/RELEASE_NOTES.md
index 1b2ead337..0e6acba9c 100644
--- a/RELEASE_NOTES.md
+++ b/RELEASE_NOTES.md
@@ -1,11 +1,17 @@
 RELEASE NOTES
 
-Version 4.next
-================
-- Planned features
-  - sat.euf 
-    - CDCL core for SMT queries. It extends the SAT engine with theory solver plugins.
-  - add global incremental pre-processing for the legacy core.
+
+Version 4.17.0
+==============
+- A FiniteSets theory solver
+  FiniteSets is a theory with a sort (FiniteSet S) for base sort S.
+  Inhabitants of (FiniteSet S) are finite sets of elements over S.
+  The main operations are creating empty sets, singleton sets, union, intersection, set difference, ranges of integers, subset modulo a predicate.
+  Constraints are: membership, subset.
+  The size of a set is obtained using set.size.
+  It is possible to map a function over elements of a set using set.map.
+  Support for set.range, set.map is partial.
+  Support for set.size exists, but is without any optimization. The source code contains comments on ways to make it more efficient. File a GitHub issue if you want to contribute.s
 
 Version 4.16.0
 ==============