From 6d1d83b1866224cb57eadddcd035f228e65c69f5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Basile=20Cl=C3=A9ment?= Date: Fri, 10 May 2024 09:45:24 +0200 Subject: [PATCH] Soundness fix (again) --- src/lib/reasoners/bitv_rel.ml | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/src/lib/reasoners/bitv_rel.ml b/src/lib/reasoners/bitv_rel.ml index 8d1f93909f..c6569b2f79 100644 --- 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) ->