From 3f4453c0685d4a5ecc96bd11a4db7374a07c8524 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Thu, 4 Apr 2024 13:13:48 +0200 Subject: [PATCH] No intersection in `update` We don't need to perform an intersection in `Domain.update` as we always call it on domains that are subsets of the old ones. --- src/lib/reasoners/enum_rel.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/lib/reasoners/enum_rel.ml b/src/lib/reasoners/enum_rel.ml index d6df3f85c6..e311a9d727 100644 --- a/src/lib/reasoners/enum_rel.ml +++ b/src/lib/reasoners/enum_rel.ml @@ -151,14 +151,14 @@ module Domains = struct internal_update r nd t (** [update r d t] replaces the domain of [r] in [t] by [d]. The - representative [r] is marked [changed] after this call. *) + representative [r] is marked [changed] after this call if the domain + [d] isn't equal to the old one. *) let update r d t = let od = get r t in - let nd = Domain.intersect ~ex:Explanation.empty od d in - if Domain.equal od nd then + if Domain.equal od d then t else - internal_update r nd t + internal_update r d t let remove r t = let domains = MX.remove r t.domains in