From edc56795305e4de44e0dfe86af20edcd3fd83527 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 31 Jan 2025 09:49:16 -0800
Subject: [PATCH] updated release notes

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 RELEASE_NOTES.md | 1 +
 1 file changed, 1 insertion(+)

diff --git a/RELEASE_NOTES.md b/RELEASE_NOTES.md
index 71c5ea881..c4090cc3d 100644
--- a/RELEASE_NOTES.md
+++ b/RELEASE_NOTES.md
@@ -14,6 +14,7 @@ Versoin 4.14.0
 ==============
 - [SLS modulo theories](https://microsoft.github.io/z3guide/programming/Local%20Search/) engine v1 release.
 - API for accessing term [depth and groundness](https://github.com/Z3Prover/z3/pull/7479).
+- Two fixes to relevancy propagation thanks to Can Cebeci. Two instacnes where literals lemmas and axioms were not marked relevant and therefore not propagated to other theories. Theory lemmas are replayed during backjumping and have are now by default marked relevant. 
 - A new API for solving LRA variables modulo constraints.
 - Performance and bug fixes.