fix: Actually add explanation for intersection

OCamlPro · Mar 22, 2024 · c7ad3c9 · c7ad3c9
1 parent 809cfa1
commit c7ad3c9
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 =