Remove warn_and_top_on_zero from BaseInvariant for division by zero

src/analyses/baseInvariant.ml

@@ -291,12 +291,6 @@ struct
     (* inverse values for binary operation a `op` b == c *)
     (* ikind is the type of a for limiting ranges of the operands a, b. The only binops which can have different types for a, b are Shiftlt, Shiftrt (not handled below; don't use ikind to limit b there). *)
     let inv_bin_int (a, b) ikind c op =
-      let warn_and_top_on_zero x =
-        if ID.equal_to Z.zero x = `Eq then
-          ID.top_of ikind
-        else
-          x
-      in
       let meet_bin a' b'  = id_meet_down ~old:a ~c:a', id_meet_down ~old:b ~c:b' in
       let meet_com oi = (* commutative *)
         try
@@ -320,8 +314,6 @@ struct
         (refine_by a b, refine_by b a)
       | MinusA -> meet_non ID.add ID.sub
       | Div    ->
-        (* If b must be zero, we have must UB *)
-        let b = warn_and_top_on_zero b in
         (* Integer division means we need to add the remainder, so instead of just `a = c*b` we have `a = c*b + a%b`.
          * However, a%b will give [-b+1, b-1] for a=top, but we only want the positive/negative side depending on the sign of c*b.
          * If c*b = 0 or it can be positive or negative, we need the full range for the remainder. *)
@@ -335,8 +327,6 @@ struct
         in
         meet_bin (ID.add (ID.mul b c) rem) (ID.div (ID.sub a rem) c)
       | Mod    -> (* a % b == c *)
-        (* If b must be zero, we have must UB *)
-        let b = warn_and_top_on_zero b in
         (* a' = a/b*b + c and derived from it b' = (a-c)/(a/b)
          * The idea is to formulate a' as quotient * divisor + remainder. *)
         let a' = ID.add (ID.mul (ID.div a b) b) c in