diff --git a/src/cdomains/intDomain.ml b/src/cdomains/intDomain.ml index 748df62300..3bc84ae676 100644 --- a/src/cdomains/intDomain.ml +++ b/src/cdomains/intDomain.ml @@ -3274,6 +3274,7 @@ struct let invariant_ikind e ik x = match x with + | x when is_top x -> Invariant.top () | Some (c, m) when m =: Ints_t.zero -> if get_bool "witness.invariant.exact" then let c = Ints_t.to_bigint c in