fix: Actually add explanation for intersection

bclement-ocp · Mar 29, 2024 · 83dd9d7 · 83dd9d7
1 parent 812b2fb
commit 83dd9d7
Showing 1 changed file with 3 additions and 3 deletions.
diff --git a/src/lib/reasoners/bitv_rel.ml b/src/lib/reasoners/bitv_rel.ml
@@ -99,9 +99,9 @@ module Interval_domain : Rel_utils.Domain with type t = Intervals.t = struct
     | _ -> assert false
 
   let intersect ~ex x y =
-    try
-      Intervals.intersect x y
-    with Inconsistent ex' ->
+    match Intervals.intersect x y with
+    | xy -> Intervals.add_explanation xy ex
+    | exception Inconsistent ex' ->
       raise @@ Inconsistent (Ex.union ex ex')
 
   let lognot sz int =