Filter out-of-invariant exclusion list elements in IntDomTuple invariant

goblint · Jun 19, 2024 · 06f8f4b · 06f8f4b
1 parent 39f6c2d
commit 06f8f4b
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 1 deletion.
diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml
@@ -3803,6 +3803,8 @@ module IntDomTupleImpl = struct
         let min = minimal x in
         let max = maximal x in
         let ns = Option.map fst (to_excl_list x) |? [] in
+        let ns = Option.map_default (fun min -> List.filter (Z.geq min) ns) ns min in
+        let ns = Option.map_default (fun max -> List.filter (Z.leq max) ns) ns max in
         Invariant.(
           IntInvariant.of_interval_opt e ik (min, max) &&
           IntInvariant.of_excl_list e ik ns &&

diff --git a/tests/regression/witness/int.t/run.t b/tests/regression/witness/int.t/run.t
@@ -29,7 +29,7 @@
       column: 5
       function: main
     location_invariant:
-      string: (51 <= i && i <= 99) && (i != 0 && (51 <= i && i <= 99))
+      string: (51 <= i && i <= 99) && (51 <= i && i <= 99)
       type: assertion
       format: C
   - entry_type: location_invariant