diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml index c2eb2f3aa5f..2c75e0f7b94 100644 --- 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 index 2bf5bd31c3f..bc8ad5ac0a0 100644 --- 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