also watch result of constraint

bclement-ocp · Jul 19, 2024 · 8053e0c · 8053e0c
1 parent f3563f1
commit 8053e0c
Showing 1 changed file with 7 additions and 4 deletions.
diff --git a/src/lib/reasoners/bitv_rel.ml b/src/lib/reasoners/bitv_rel.ml
@@ -1124,14 +1124,17 @@ let extract_constraints terms domain int_domain uf r t =
         and ry, exy = Uf.find uf y in
         let c = mk r rx ry in
         let ex = Ex.union exx exy in
+        let ex_c = explained ~ex c in
         let domain =
-          Bitlist_domains.watch (explained ~ex c) rx @@
-          Bitlist_domains.watch (explained ~ex c) ry @@
+          Bitlist_domains.watch ex_c rx @@
+          Bitlist_domains.watch ex_c ry @@
+          Bitlist_domains.watch ex_c r @@
           domain
         in
         let int_domain =
-          Interval_domains.watch (explained ~ex c) rx @@
-          Interval_domains.watch (explained ~ex c) ry @@
+          Interval_domains.watch ex_c rx @@
+          Interval_domains.watch ex_c ry @@
+          Interval_domains.watch ex_c r @@
           int_domain
         in
         terms, domain, int_domain