Soundness fix (again)

OCamlPro · May 10, 2024 · 6d1d83b · 6d1d83b
1 parent d6d52e7
commit 6d1d83b
Showing 1 changed file with 3 additions and 4 deletions.
diff --git a/src/lib/reasoners/bitv_rel.ml b/src/lib/reasoners/bitv_rel.ml
@@ -96,10 +96,9 @@ module Interval_domain : Rel_utils.Domain with type t = Intervals.Int.t = struct
       Fmt.invalid_arg "unknown: only bit-vector types are supported; got %a"
         Ty.print ty
 
-  let intersect ~ex x y =
+  let intersect x y =
     match Intervals.Int.intersect x y with
-    | Empty ex' ->
-      raise @@ Inconsistent (Ex.union ex ex')
+    | Empty ex -> raise @@ Inconsistent ex
     | NonEmpty u -> u
 
   let lognot sz int =
@@ -125,7 +124,7 @@ module Interval_domain : Rel_utils.Domain with type t = Intervals.Int.t = struct
           let acc = match bv with
             | Bitv.Cte z ->
               (* Nothing to update, but still check for consistency *)
-              ignore @@ intersect ~ex:Ex.empty int (point z);
+              ignore @@ intersect int (point z);
               acc
             | Other s -> fold_signed f s sz int acc
             | Ext (r, r_size, i, j) ->