From 94ad32dc61109756800565c36a1a02bdd078217d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Basile=20Cl=C3=A9ment?= <basile.clement@ocamlpro.com>
Date: Wed, 24 Jul 2024 12:28:45 +0200
Subject: [PATCH] subst must always trigger or we miss simplifications

---
 src/lib/reasoners/rel_utils.ml | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

diff --git a/src/lib/reasoners/rel_utils.ml b/src/lib/reasoners/rel_utils.ml
index 805556487..e1bddf666 100644
--- a/src/lib/reasoners/rel_utils.ml
+++ b/src/lib/reasoners/rel_utils.ml
@@ -1082,10 +1082,8 @@ struct
     let nrr_nf = NF.normal_form nrr in
     let nrrd = find_or_default nrr_nf t in
     let nnrrd = D.intersect nrrd rrd in
-    let t =
-      if D.equal nnrrd rrd then t
-      else { t with triggers = W.Set.union ws t.triggers }
-    in
+    (* Always trigger to ensure we check for simplifications. *)
+    let t = { t with triggers = W.Set.union ws t.triggers } in
     let t =
       match nrr_nf with
       | Constant _ -> t