diff --git a/infer/src/IR/IntLit.ml b/infer/src/IR/IntLit.ml
index f9e45d4dd..341e746c6 100644
--- a/infer/src/IR/IntLit.ml
+++ b/infer/src/IR/IntLit.ml
@@ -63,6 +63,8 @@ let to_int (_, i, _) = Int64.to_int i
 
 let to_int_exn (_, i, _) = Int64.to_int_exn i
 
+let to_big_int (_, i, _) = Z.of_int64 i
+
 let to_float (_, i, _) = Int64.to_float i
 
 let null = (false, 0L, true)
diff --git a/infer/src/IR/IntLit.mli b/infer/src/IR/IntLit.mli
index 9125632dd..097a54195 100644
--- a/infer/src/IR/IntLit.mli
+++ b/infer/src/IR/IntLit.mli
@@ -91,6 +91,8 @@ val to_int : t -> int option
 
 val to_int_exn : t -> int
 
+val to_big_int : t -> Z.t
+
 val to_float : t -> float
 
 val to_signed : t -> t option
diff --git a/infer/src/bufferoverrun/bounds.ml b/infer/src/bufferoverrun/bounds.ml
index 90da2af90..cade9dbcb 100644
--- a/infer/src/bufferoverrun/bounds.ml
+++ b/infer/src/bufferoverrun/bounds.ml
@@ -42,9 +42,9 @@ module SymLinear = struct
   let le : t -> t -> bool =
    fun x y ->
     let le_one_pair s v1_opt v2_opt =
-      let v1 = NonZeroInt.opt_to_int v1_opt in
-      let v2 = NonZeroInt.opt_to_int v2_opt in
-      Int.equal v1 v2 || (Symb.Symbol.is_unsigned s && v1 <= v2)
+      let v1 = NonZeroInt.opt_to_big_int v1_opt in
+      let v2 = NonZeroInt.opt_to_big_int v2_opt in
+      Z.(equal v1 v2) || (Symb.Symbol.is_unsigned s && v1 <= v2)
     in
     M.for_all2 ~f:le_one_pair x y
 
@@ -64,17 +64,17 @@ module SymLinear = struct
   let eq : t -> t -> bool =
    fun x y ->
     let eq_pair _ (coeff1 : NonZeroInt.t option) (coeff2 : NonZeroInt.t option) =
-      [%compare.equal: int option] (coeff1 :> int option) (coeff2 :> int option)
+      [%compare.equal: Z.t option] (coeff1 :> Z.t option) (coeff2 :> Z.t option)
     in
     M.for_all2 ~f:eq_pair x y
 
 
   let pp1 : F.formatter -> Symb.Symbol.t * NonZeroInt.t -> unit =
    fun fmt (s, c) ->
-    let c = (c :> int) in
-    if Int.equal c 1 then Symb.Symbol.pp fmt s
-    else if Int.equal c (-1) then F.fprintf fmt "-%a" Symb.Symbol.pp s
-    else F.fprintf fmt "%dx%a" c Symb.Symbol.pp s
+    let c = (c :> Z.t) in
+    if Z.(equal c one) then Symb.Symbol.pp fmt s
+    else if Z.(equal c minus_one) then F.fprintf fmt "-%a" Symb.Symbol.pp s
+    else F.fprintf fmt "%ax%a" Z.pp_print c Symb.Symbol.pp s
 
 
   let pp : F.formatter -> t -> unit =
@@ -106,7 +106,7 @@ module SymLinear = struct
   let one_symbol_of_coeff : NonZeroInt.t -> t -> Symb.Symbol.t option =
    fun coeff x ->
     match M.is_singleton x with
-    | Some (k, v) when Int.equal (v :> int) (coeff :> int) ->
+    | Some (k, v) when Z.equal (v :> Z.t) (coeff :> Z.t) ->
         Some k
     | _ ->
         None
@@ -153,9 +153,9 @@ module SymLinear = struct
 
   (* we can give integer bounds (obviously 0) only when all symbols are unsigned *)
 
-  let int_lb x = if is_ge_zero x then Some 0 else None
+  let big_int_lb x = if is_ge_zero x then Some Z.zero else None
 
-  let int_ub x = if is_le_zero x then Some 0 else None
+  let big_int_ub x = if is_le_zero x then Some Z.zero else None
 
   (** When two following symbols are from the same path, simplify what would lead to a zero sum. E.g. 2 * x.lb - x.ub = x.lb *)
   let simplify_bound_ends_from_paths : t -> t =
@@ -198,7 +198,7 @@ module Bound = struct
 
     let neg = function Plus -> Minus | Minus -> Plus
 
-    let eval_int x i1 i2 = match x with Plus -> i1 + i2 | Minus -> i1 - i2
+    let eval_big_int x i1 i2 = match x with Plus -> Z.(i1 + i2) | Minus -> Z.(i1 - i2)
 
     let pp ~need_plus : F.formatter -> t -> unit =
      fun fmt -> function
@@ -217,7 +217,7 @@ module Bound = struct
 
     let neg = function Min -> Max | Max -> Min
 
-    let eval_int x i1 i2 = match x with Min -> min i1 i2 | Max -> max i1 i2
+    let eval_big_int x i1 i2 = match x with Min -> Z.min i1 i2 | Max -> Z.max i1 i2
 
     let pp : F.formatter -> t -> unit =
      fun fmt -> function Min -> F.pp_print_string fmt "min" | Max -> F.pp_print_string fmt "max"
@@ -227,8 +227,8 @@ module Bound = struct
      e.g. `MinMax (1, Minus, Max, 2, s)` means "1 - max (2, s)". *)
   type t =
     | MInf
-    | Linear of int * SymLinear.t
-    | MinMax of int * Sign.t * MinMax.t * int * Symb.Symbol.t
+    | Linear of Z.t * SymLinear.t
+    | MinMax of Z.t * Sign.t * MinMax.t * Z.t * Symb.Symbol.t
     | PInf
   [@@deriving compare]
 
@@ -241,24 +241,26 @@ module Bound = struct
     | PInf ->
         F.pp_print_string fmt "+oo"
     | Linear (c, x) ->
-        if SymLinear.is_zero x then F.pp_print_int fmt c
-        else if Int.equal c 0 then SymLinear.pp fmt x
-        else F.fprintf fmt "%a + %d" SymLinear.pp x c
+        if SymLinear.is_zero x then Z.pp_print fmt c
+        else if Z.(equal c zero) then SymLinear.pp fmt x
+        else F.fprintf fmt "%a + %a" SymLinear.pp x Z.pp_print c
     | MinMax (c, sign, m, d, x) ->
-        if Int.equal c 0 then (Sign.pp ~need_plus:false) fmt sign
-        else F.fprintf fmt "%d%a" c (Sign.pp ~need_plus:true) sign ;
-        F.fprintf fmt "%a(%d, %a)" MinMax.pp m d Symb.Symbol.pp x
+        if Z.(equal c zero) then (Sign.pp ~need_plus:false) fmt sign
+        else F.fprintf fmt "%a%a" Z.pp_print c (Sign.pp ~need_plus:true) sign ;
+        F.fprintf fmt "%a(%a, %a)" MinMax.pp m Z.pp_print d Symb.Symbol.pp x
 
 
   let of_bound_end = function Symb.BoundEnd.LowerBound -> MInf | Symb.BoundEnd.UpperBound -> PInf
 
-  let of_int : int -> t = fun n -> Linear (n, SymLinear.empty)
+  let of_int : int -> t = fun n -> Linear (Z.of_int n, SymLinear.empty)
+
+  let of_big_int : Z.t -> t = fun n -> Linear (n, SymLinear.empty)
 
   let minus_one = of_int (-1)
 
   let _255 = of_int 255
 
-  let of_sym : SymLinear.t -> t = fun s -> Linear (0, s)
+  let of_sym : SymLinear.t -> t = fun s -> Linear (Z.zero, s)
 
   let is_symbolic : t -> bool = function
     | MInf | PInf ->
@@ -270,7 +272,7 @@ module Bound = struct
 
 
   let lift_symlinear : (SymLinear.t -> 'a option) -> t -> 'a option =
-   fun f -> function Linear (0, se) -> f se | _ -> None
+   fun f -> function Linear (n, se) when Z.(equal n zero) -> f se | _ -> None
 
 
   let get_one_symbol_opt : t -> Symb.Symbol.t option = lift_symlinear SymLinear.get_one_symbol_opt
@@ -292,10 +294,10 @@ module Bound = struct
   let is_mone_symbol : t -> bool = fun x -> get_mone_symbol_opt x <> None
 
   let mk_MinMax (c, sign, m, d, s) =
-    if Symb.Symbol.is_unsigned s && d <= 0 then
+    if Symb.Symbol.is_unsigned s && Z.(d <= zero) then
       match m with
       | Min ->
-          of_int (Sign.eval_int sign c d)
+          of_big_int (Sign.eval_big_int sign c d)
       | Max -> (
         match sign with
         | Plus ->
@@ -305,59 +307,59 @@ module Bound = struct
     else MinMax (c, sign, m, d, s)
 
 
-  let int_ub_of_minmax = function
+  let big_int_ub_of_minmax = function
     | MinMax (c, Plus, Min, d, _) ->
-        Some (c + d)
+        Some Z.(c + d)
     | MinMax (c, Minus, Max, d, s) when Symb.Symbol.is_unsigned s ->
-        Some (min c (c - d))
+        Some Z.(min c (c - d))
     | MinMax (c, Minus, Max, d, _) ->
-        Some (c - d)
+        Some Z.(c - d)
     | MinMax _ ->
         None
     | MInf | PInf | Linear _ ->
         assert false
 
 
-  let int_lb_of_minmax = function
+  let big_int_lb_of_minmax = function
     | MinMax (c, Plus, Max, d, s) when Symb.Symbol.is_unsigned s ->
-        Some (max c (c + d))
+        Some Z.(max c (c + d))
     | MinMax (c, Plus, Max, d, _) ->
-        Some (c + d)
+        Some Z.(c + d)
     | MinMax (c, Minus, Min, d, _) ->
-        Some (c - d)
+        Some Z.(c - d)
     | MinMax _ ->
         None
     | MInf | PInf | Linear _ ->
         assert false
 
 
-  let int_of_minmax = function
+  let big_int_of_minmax = function
     | Symb.BoundEnd.LowerBound ->
-        int_lb_of_minmax
+        big_int_lb_of_minmax
     | Symb.BoundEnd.UpperBound ->
-        int_ub_of_minmax
+        big_int_ub_of_minmax
 
 
-  let int_lb = function
+  let big_int_lb = function
     | MInf ->
         None
     | PInf ->
         assert false
     | MinMax _ as b ->
-        int_lb_of_minmax b
+        big_int_lb_of_minmax b
     | Linear (c, se) ->
-        SymLinear.int_lb se |> Option.map ~f:(( + ) c)
+        SymLinear.big_int_lb se |> Option.map ~f:(Z.( + ) c)
 
 
-  let int_ub = function
+  let big_int_ub = function
     | MInf ->
         assert false
     | PInf ->
         None
     | MinMax _ as b ->
-        int_ub_of_minmax b
+        big_int_ub_of_minmax b
     | Linear (c, se) ->
-        SymLinear.int_ub se |> Option.map ~f:(( + ) c)
+        SymLinear.big_int_ub se |> Option.map ~f:(Z.( + ) c)
 
 
   let linear_ub_of_minmax = function
@@ -383,7 +385,11 @@ module Bound = struct
 
 
   let le_minmax_by_int x y =
-    match (int_ub_of_minmax x, int_lb_of_minmax y) with Some n, Some m -> n <= m | _, _ -> false
+    match (big_int_ub_of_minmax x, big_int_lb_of_minmax y) with
+    | Some n, Some m ->
+        n <= m
+    | _, _ ->
+        false
 
 
   let le_opt1 le opt_n m = Option.value_map opt_n ~default:false ~f:(fun n -> le n m)
@@ -401,17 +407,17 @@ module Bound = struct
         c0 <= c1 && SymLinear.le x0 x1
     | MinMax (c1, sign1, m1, d1, x1), MinMax (c2, sign2, m2, d2, x2)
       when Sign.equal sign1 sign2 && MinMax.equal m1 m2 ->
-        c1 <= c2 && Int.equal d1 d2 && Symb.Symbol.equal x1 x2
+        c1 <= c2 && Z.equal d1 d2 && Symb.Symbol.equal x1 x2
     | MinMax _, MinMax _ when le_minmax_by_int x y ->
         true
     | MinMax (c1, Plus, Min, _, x1), MinMax (c2, Plus, Max, _, x2)
     | MinMax (c1, Minus, Max, _, x1), MinMax (c2, Minus, Min, _, x2) ->
         c1 <= c2 && Symb.Symbol.equal x1 x2
     | MinMax _, Linear (c, se) ->
-        (SymLinear.is_ge_zero se && le_opt1 Int.( <= ) (int_ub_of_minmax x) c)
+        (SymLinear.is_ge_zero se && le_opt1 Z.leq (big_int_ub_of_minmax x) c)
         || le_opt1 le (linear_ub_of_minmax x) y
     | Linear (c, se), MinMax _ ->
-        (SymLinear.is_le_zero se && le_opt2 Int.( <= ) c (int_lb_of_minmax y))
+        (SymLinear.is_le_zero se && le_opt2 Z.leq c (big_int_lb_of_minmax y))
         || le_opt2 le x (linear_lb_of_minmax y)
     | _, _ ->
         false
@@ -423,9 +429,9 @@ module Bound = struct
     | MInf, Linear _ | MInf, MinMax _ | MInf, PInf | Linear _, PInf | MinMax _, PInf ->
         true
     | Linear (c, x), _ ->
-        le (Linear (c + 1, x)) y
+        le (Linear (Z.succ c, x)) y
     | MinMax (c, sign, min_max, d, x), _ ->
-        le (mk_MinMax (c + 1, sign, min_max, d, x)) y
+        le (mk_MinMax (Z.succ c, sign, min_max, d, x)) y
     | _, _ ->
         false
 
@@ -454,31 +460,31 @@ module Bound = struct
     else
       match (x, y) with
       | Linear (c1, x1), Linear (c2, x2) when SymLinear.is_zero x1 && SymLinear.is_one_symbol x2 ->
-          mk_MinMax (c2, Plus, Min, c1 - c2, SymLinear.get_one_symbol x2)
+          mk_MinMax (c2, Plus, Min, Z.(c1 - c2), SymLinear.get_one_symbol x2)
       | Linear (c1, x1), Linear (c2, x2) when SymLinear.is_one_symbol x1 && SymLinear.is_zero x2 ->
-          mk_MinMax (c1, Plus, Min, c2 - c1, SymLinear.get_one_symbol x1)
+          mk_MinMax (c1, Plus, Min, Z.(c2 - c1), SymLinear.get_one_symbol x1)
       | Linear (c1, x1), Linear (c2, x2) when SymLinear.is_zero x1 && SymLinear.is_mone_symbol x2
         ->
-          mk_MinMax (c2, Minus, Max, c2 - c1, SymLinear.get_mone_symbol x2)
+          mk_MinMax (c2, Minus, Max, Z.(c2 - c1), SymLinear.get_mone_symbol x2)
       | Linear (c1, x1), Linear (c2, x2) when SymLinear.is_mone_symbol x1 && SymLinear.is_zero x2
         ->
-          mk_MinMax (c1, Minus, Max, c1 - c2, SymLinear.get_mone_symbol x1)
+          mk_MinMax (c1, Minus, Max, Z.(c1 - c2), SymLinear.get_mone_symbol x1)
       | MinMax (c1, Plus, Min, d1, s), Linear (c2, se)
       | Linear (c2, se), MinMax (c1, Plus, Min, d1, s)
         when SymLinear.is_zero se ->
-          mk_MinMax (c1, Plus, Min, min d1 (c2 - c1), s)
+          mk_MinMax (c1, Plus, Min, Z.(min d1 (c2 - c1)), s)
       | MinMax (c1, Plus, Max, _, s), Linear (c2, se)
       | Linear (c2, se), MinMax (c1, Plus, Max, _, s)
         when SymLinear.is_zero se ->
-          mk_MinMax (c1, Plus, Min, c2 - c1, s)
+          mk_MinMax (c1, Plus, Min, Z.(c2 - c1), s)
       | MinMax (c1, Minus, Min, _, s), Linear (c2, se)
       | Linear (c2, se), MinMax (c1, Minus, Min, _, s)
         when SymLinear.is_zero se ->
-          mk_MinMax (c1, Minus, Max, c1 - c2, s)
+          mk_MinMax (c1, Minus, Max, Z.(c1 - c2), s)
       | MinMax (c1, Minus, Max, d1, s), Linear (c2, se)
       | Linear (c2, se), MinMax (c1, Minus, Max, d1, s)
         when SymLinear.is_zero se ->
-          mk_MinMax (c1, Minus, Max, max d1 (c1 - c2), s)
+          mk_MinMax (c1, Minus, Max, Z.(max d1 (c1 - c2)), s)
       | MinMax (_, Plus, Min, _, _), MinMax (_, Plus, Max, _, _)
       | MinMax (_, Plus, Min, _, _), MinMax (_, Minus, Min, _, _)
       | MinMax (_, Minus, Max, _, _), MinMax (_, Plus, Max, _, _)
@@ -490,7 +496,7 @@ module Bound = struct
       | MinMax (_, Minus, Min, _, _), MinMax (_, Minus, Max, _, _) ->
           lb ~default (remove_max_int x) y
       | MinMax (c1, Plus, Max, d1, _), MinMax (c2, Plus, Max, d2, _) ->
-          Linear (min (c1 + d1) (c2 + d2), SymLinear.zero)
+          Linear (Z.(min (c1 + d1) (c2 + d2)), SymLinear.zero)
       | _, _ ->
           default
 
@@ -513,15 +519,15 @@ module Bound = struct
     else
       match (x, y) with
       | Linear (c1, x1), Linear (c2, x2) when SymLinear.is_zero x1 && SymLinear.is_one_symbol x2 ->
-          mk_MinMax (c2, Plus, Max, c1 - c2, SymLinear.get_one_symbol x2)
+          mk_MinMax (c2, Plus, Max, Z.(c1 - c2), SymLinear.get_one_symbol x2)
       | Linear (c1, x1), Linear (c2, x2) when SymLinear.is_one_symbol x1 && SymLinear.is_zero x2 ->
-          mk_MinMax (c1, Plus, Max, c2 - c1, SymLinear.get_one_symbol x1)
+          mk_MinMax (c1, Plus, Max, Z.(c2 - c1), SymLinear.get_one_symbol x1)
       | Linear (c1, x1), Linear (c2, x2) when SymLinear.is_zero x1 && SymLinear.is_mone_symbol x2
         ->
-          mk_MinMax (c2, Minus, Min, c2 - c1, SymLinear.get_mone_symbol x2)
+          mk_MinMax (c2, Minus, Min, Z.(c2 - c1), SymLinear.get_mone_symbol x2)
       | Linear (c1, x1), Linear (c2, x2) when SymLinear.is_mone_symbol x1 && SymLinear.is_zero x2
         ->
-          mk_MinMax (c1, Minus, Min, c1 - c2, SymLinear.get_mone_symbol x1)
+          mk_MinMax (c1, Minus, Min, Z.(c1 - c2), SymLinear.get_mone_symbol x1)
       | _, _ ->
           default
 
@@ -534,10 +540,10 @@ module Bound = struct
     | PInf, _ | _, PInf ->
         L.(die InternalError) "Lower bound cannot be +oo."
     | MinMax (n1, Plus, Max, _, s1), Linear (n2, s2)
-      when Int.equal n1 n2 && SymLinear.is_one_symbol_of s1 s2 ->
+      when Z.equal n1 n2 && SymLinear.is_one_symbol_of s1 s2 ->
         y
     | MinMax (n1, Minus, Min, _, s1), Linear (n2, s2)
-      when Int.equal n1 n2 && SymLinear.is_mone_symbol_of s1 s2 ->
+      when Z.equal n1 n2 && SymLinear.is_mone_symbol_of s1 s2 ->
         y
     | _ ->
         if le x y then x else MInf
@@ -549,28 +555,28 @@ module Bound = struct
     | MInf, _ | _, MInf ->
         L.(die InternalError) "Upper bound cannot be -oo."
     | MinMax (n1, Plus, Min, _, s1), Linear (n2, s2)
-      when Int.equal n1 n2 && SymLinear.is_one_symbol_of s1 s2 ->
+      when Z.equal n1 n2 && SymLinear.is_one_symbol_of s1 s2 ->
         y
     | MinMax (n1, Minus, Max, _, s1), Linear (n2, s2)
-      when Int.equal n1 n2 && SymLinear.is_mone_symbol_of s1 s2 ->
+      when Z.equal n1 n2 && SymLinear.is_mone_symbol_of s1 s2 ->
         y
     | _ ->
         if le y x then x else PInf
 
 
-  let zero : t = Linear (0, SymLinear.zero)
+  let zero : t = Linear (Z.zero, SymLinear.zero)
 
-  let one : t = Linear (1, SymLinear.zero)
+  let one : t = Linear (Z.one, SymLinear.zero)
 
-  let mone : t = Linear (-1, SymLinear.zero)
+  let mone : t = Linear (Z.minus_one, SymLinear.zero)
 
-  let is_some_const : int -> t -> bool =
-   fun c x -> match x with Linear (c', y) -> Int.equal c c' && SymLinear.is_zero y | _ -> false
+  let is_some_const : Z.t -> t -> bool =
+   fun c x -> match x with Linear (c', y) -> Z.equal c c' && SymLinear.is_zero y | _ -> false
 
 
-  let is_zero : t -> bool = is_some_const 0
+  let is_zero : t -> bool = is_some_const Z.zero
 
-  let is_const : t -> int option =
+  let is_const : t -> Z.t option =
    fun x -> match x with Linear (c, y) when SymLinear.is_zero y -> Some c | _ -> None
 
 
@@ -582,11 +588,11 @@ module Bound = struct
     | _, _ when is_zero y ->
         x
     | Linear (c1, x1), Linear (c2, x2) ->
-        Linear (c1 + c2, SymLinear.plus x1 x2)
+        Linear (Z.(c1 + c2), SymLinear.plus x1 x2)
     | MinMax (c1, sign, min_max, d1, x1), Linear (c2, x2)
     | Linear (c2, x2), MinMax (c1, sign, min_max, d1, x1)
       when SymLinear.is_zero x2 ->
-        mk_MinMax (c1 + c2, sign, min_max, d1, x1)
+        mk_MinMax (Z.(c1 + c2), sign, min_max, d1, x1)
     | _ ->
         f x y
 
@@ -596,10 +602,10 @@ module Bound = struct
         match (x, y) with
         | MinMax (c1, Plus, Max, d1, _), Linear (c2, x2)
         | Linear (c2, x2), MinMax (c1, Plus, Max, d1, _) ->
-            Linear (c1 + d1 + c2, x2)
+            Linear (Z.(c1 + d1 + c2), x2)
         | MinMax (c1, Minus, Min, d1, _), Linear (c2, x2)
         | Linear (c2, x2), MinMax (c1, Minus, Min, d1, _) ->
-            Linear (c1 - d1 + c2, x2)
+            Linear (Z.(c1 - d1 + c2), x2)
         | _, _ ->
             MInf )
 
@@ -609,10 +615,10 @@ module Bound = struct
         match (x, y) with
         | MinMax (c1, Plus, Min, d1, _), Linear (c2, x2)
         | Linear (c2, x2), MinMax (c1, Plus, Min, d1, _) ->
-            Linear (c1 + d1 + c2, x2)
+            Linear (Z.(c1 + d1 + c2), x2)
         | MinMax (c1, Minus, Max, d1, _), Linear (c2, x2)
         | Linear (c2, x2), MinMax (c1, Minus, Max, d1, _) ->
-            Linear (c1 - d1 + c2, x2)
+            Linear (Z.(c1 - d1 + c2), x2)
         | _, _ ->
             PInf )
 
@@ -627,15 +633,19 @@ module Bound = struct
     | PInf ->
         if NonZeroInt.is_positive n then PInf else MInf
     | Linear (c, x') ->
-        Linear (c * (n :> int), SymLinear.mult_const n x')
+        Linear (Z.(c * (n :> Z.t)), SymLinear.mult_const n x')
     | MinMax _ -> (
         let int_bound =
           let bound_end' =
             if NonZeroInt.is_positive n then bound_end else Symb.BoundEnd.neg bound_end
           in
-          int_of_minmax bound_end' x
+          big_int_of_minmax bound_end' x
         in
-        match int_bound with Some i -> of_int (i * (n :> int)) | None -> of_bound_end bound_end )
+        match int_bound with
+        | Some i ->
+            of_big_int Z.(i * (n :> Z.t))
+        | None ->
+            of_bound_end bound_end )
 
 
   let mult_const_l = mult_const Symb.BoundEnd.LowerBound
@@ -648,9 +658,9 @@ module Bound = struct
     | PInf ->
         MInf
     | Linear (c, x) ->
-        Linear (-c, SymLinear.neg x)
+        Linear (Z.neg c, SymLinear.neg x)
     | MinMax (c, sign, min_max, d, x) ->
-        mk_MinMax (-c, Sign.neg sign, min_max, d, x)
+        mk_MinMax (Z.neg c, Sign.neg sign, min_max, d, x)
 
 
   let div_const : t -> NonZeroInt.t -> t option =
@@ -663,7 +673,7 @@ module Bound = struct
     | Linear (c, x') when NonZeroInt.is_multiple c n -> (
       match SymLinear.exact_div_const_exn x' n with
       | x'' ->
-          Some (Linear (c / (n :> int), x''))
+          Some (Linear (Z.(c / (n :> Z.t)), x''))
       | exception NonZeroInt.DivisionNotExact ->
           None )
     | _ ->
@@ -738,13 +748,13 @@ module Bound = struct
         NonBottom x
     | Linear (c, se) ->
         SymLinear.fold se
-          ~init:(NonBottom (of_int c))
+          ~init:(NonBottom (of_big_int c))
           ~f:(fun acc s coeff -> lift2 (plus subst_pos) acc (get_mult_const s coeff))
     | MinMax (c, sign, min_max, d, s) -> (
       match get s with
       | Bottom ->
-          Option.value_map (int_of_minmax subst_pos x) ~default:Bottom ~f:(fun i ->
-              NonBottom (of_int i) )
+          Option.value_map (big_int_of_minmax subst_pos x) ~default:Bottom ~f:(fun i ->
+              NonBottom (of_big_int i) )
       | NonBottom x' ->
           let res =
             match (sign, min_max, x') with
@@ -753,44 +763,48 @@ module Bound = struct
             | Plus, Max, PInf | Minus, Min, MInf ->
                 PInf
             | sign, Min, PInf | sign, Max, MInf ->
-                of_int (Sign.eval_int sign c d)
+                of_big_int (Sign.eval_big_int sign c d)
             | _, _, Linear (c2, se) -> (
                 if SymLinear.is_zero se then
-                  of_int (Sign.eval_int sign c (MinMax.eval_int min_max d c2))
+                  of_big_int (Sign.eval_big_int sign c (MinMax.eval_big_int min_max d c2))
                 else if SymLinear.is_one_symbol se then
                   mk_MinMax
-                    (Sign.eval_int sign c c2, sign, min_max, d - c2, SymLinear.get_one_symbol se)
+                    ( Sign.eval_big_int sign c c2
+                    , sign
+                    , min_max
+                    , Z.(d - c2)
+                    , SymLinear.get_one_symbol se )
                 else if SymLinear.is_mone_symbol se then
                   mk_MinMax
-                    ( Sign.eval_int sign c c2
+                    ( Sign.eval_big_int sign c c2
                     , Sign.neg sign
                     , MinMax.neg min_max
-                    , c2 - d
+                    , Z.(c2 - d)
                     , SymLinear.get_mone_symbol se )
                 else
-                  match int_of_minmax subst_pos x with
+                  match big_int_of_minmax subst_pos x with
                   | Some i ->
-                      of_int i
+                      of_big_int i
                   | None ->
                       of_bound_end subst_pos )
             | _, _, MinMax (c2, sign2, min_max2, d2, s2) -> (
               match (min_max, sign2, min_max2) with
               | Min, Plus, Min | Max, Plus, Max ->
-                  let c' = Sign.eval_int sign c c2 in
-                  let d' = MinMax.eval_int min_max (d - c2) d2 in
+                  let c' = Sign.eval_big_int sign c c2 in
+                  let d' = MinMax.eval_big_int min_max Z.(d - c2) d2 in
                   mk_MinMax (c', sign, min_max, d', s2)
               | Min, Minus, Max | Max, Minus, Min ->
-                  let c' = Sign.eval_int sign c c2 in
-                  let d' = MinMax.eval_int min_max2 (c2 - d) d2 in
+                  let c' = Sign.eval_big_int sign c c2 in
+                  let d' = MinMax.eval_big_int min_max2 Z.(c2 - d) d2 in
                   mk_MinMax (c', Sign.neg sign, min_max2, d', s2)
               | _ ->
                   let bound_end =
                     match sign with Plus -> subst_pos | Minus -> Symb.BoundEnd.neg subst_pos
                   in
-                  of_int
-                    (Sign.eval_int sign c
-                       (MinMax.eval_int min_max d
-                          (int_of_minmax bound_end x' |> Option.value ~default:d))) )
+                  of_big_int
+                    (Sign.eval_big_int sign c
+                       (MinMax.eval_big_int min_max d
+                          (big_int_of_minmax bound_end x' |> Option.value ~default:d))) )
           in
           NonBottom res )
 
@@ -810,7 +824,7 @@ module Bound = struct
 
   let is_same_symbol b1 b2 =
     match (b1, b2) with
-    | Linear (0, se1), Linear (0, se2) ->
+    | Linear (n1, se1), Linear (n2, se2) when Z.(equal n1 zero) && Z.(equal n2 zero) ->
         SymLinear.is_same_symbol se1 se2
     | _ ->
         None
@@ -836,5 +850,5 @@ module NonNegativeBound = struct
       | None ->
           Symbolic b
       | Some c ->
-          Constant (NonNegativeInt.of_int_exn c) )
+          Constant (NonNegativeInt.of_big_int_exn c) )
 end
diff --git a/infer/src/bufferoverrun/bounds.mli b/infer/src/bufferoverrun/bounds.mli
index e52320caf..4638f449f 100644
--- a/infer/src/bufferoverrun/bounds.mli
+++ b/infer/src/bufferoverrun/bounds.mli
@@ -35,8 +35,8 @@ module Bound : sig
 
   type t =
     | MInf
-    | Linear of int * SymLinear.t
-    | MinMax of int * sign * min_max * int * Symb.Symbol.t
+    | Linear of Z.t * SymLinear.t
+    | MinMax of Z.t * sign * min_max * Z.t * Symb.Symbol.t
     | PInf
 
   val compare : t -> t -> int
@@ -47,6 +47,8 @@ module Bound : sig
 
   val of_int : int -> t
 
+  val of_big_int : Z.t -> t
+
   val minus_one : t
 
   val _255 : t
@@ -63,11 +65,11 @@ module Bound : sig
 
   val is_mone_symbol : t -> bool
 
-  val mk_MinMax : int * sign * min_max * int * Symb.Symbol.t -> t
+  val mk_MinMax : Z.t * sign * min_max * Z.t * Symb.Symbol.t -> t
 
-  val int_lb : t -> int sexp_option
+  val big_int_lb : t -> Z.t sexp_option
 
-  val int_ub : t -> int sexp_option
+  val big_int_ub : t -> Z.t sexp_option
 
   val le : t -> t -> bool
 
@@ -97,7 +99,7 @@ module Bound : sig
 
   val is_zero : t -> bool
 
-  val is_const : t -> int sexp_option
+  val is_const : t -> Z.t sexp_option
 
   val plus_l : t -> t -> t
 
diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml
index 9af1f8b55..25483372b 100644
--- a/infer/src/bufferoverrun/bufferOverrunDomain.ml
+++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml
@@ -132,6 +132,8 @@ module Val = struct
 
   let of_int n = of_itv (Itv.of_int n)
 
+  let of_big_int n = of_itv (Itv.of_big_int n)
+
   let of_loc : Loc.t -> t = fun x -> {bot with powloc= PowLoc.singleton x}
 
   let of_pow_loc : PowLoc.t -> t = fun x -> {bot with powloc= x}
diff --git a/infer/src/bufferoverrun/bufferOverrunDomainRelation.ml b/infer/src/bufferoverrun/bufferOverrunDomainRelation.ml
index dbe4b5031..6b0e9bf5c 100644
--- a/infer/src/bufferoverrun/bufferOverrunDomainRelation.ml
+++ b/infer/src/bufferoverrun/bufferOverrunDomainRelation.ml
@@ -759,11 +759,13 @@ module Make (Manager : Manager_S) = struct
 
     let of_exp_opt ~get_sym_f opt_e : t option = Option.find_map opt_e ~f:(of_exp ~get_sym_f)
 
-    let of_int i = Texpr1.cst Env.empty (Coeff.s_of_int i)
+    let of_big_int i =
+      Texpr1.cst Env.empty (Coeff.s_of_mpq (Mpq.of_mpz (Mpz.of_string (Z.to_string i))))
 
-    let zero = of_int 0
 
-    let one = of_int 1
+    let zero = of_big_int Z.zero
+
+    let one = of_big_int Z.one
 
     let of_sym s = match s with Sym.V x -> Some (of_raw (Texpr1.Var x)) | _ -> None
 
@@ -897,12 +899,12 @@ module Make (Manager : Manager_S) = struct
         Option.value_map (SymExp.of_sym sym) ~default:empty ~f:(fun sym_exp ->
             let tcons_lb =
               Option.map (Itv.Bound.is_const lb) ~f:(fun lb ->
-                  let sym_minus_lb = SymExp.minus sym_exp (SymExp.of_int lb) in
+                  let sym_minus_lb = SymExp.minus sym_exp (SymExp.of_big_int lb) in
                   Tcons1.make sym_minus_lb Tcons1.SUPEQ )
             in
             let tcons_ub =
               Option.map (Itv.Bound.is_const ub) ~f:(fun ub ->
-                  let ub_minus_sym = SymExp.minus (SymExp.of_int ub) sym_exp in
+                  let ub_minus_sym = SymExp.minus (SymExp.of_big_int ub) sym_exp in
                   Tcons1.make ub_minus_sym Tcons1.SUPEQ )
             in
             match (tcons_lb, tcons_ub) with
diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml
index 5c3646b9f..b9799c0a4 100644
--- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml
+++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml
@@ -15,7 +15,7 @@ open BufferOverrunDomain
 
 let eval_const : Const.t -> Val.t = function
   | Const.Cint intlit ->
-      Option.value_map ~default:Val.Itv.top ~f:Val.of_int (IntLit.to_int intlit)
+      Val.of_big_int (IntLit.to_big_int intlit)
   | Const.Cfloat f ->
       f |> int_of_float |> Val.of_int
   | _ ->
diff --git a/infer/src/bufferoverrun/ints.ml b/infer/src/bufferoverrun/ints.ml
index b701e4312..887618079 100644
--- a/infer/src/bufferoverrun/ints.ml
+++ b/infer/src/bufferoverrun/ints.ml
@@ -10,81 +10,86 @@ open! AbstractDomain.Types
 module F = Format
 
 module NonZeroInt = struct
-  type t = int [@@deriving compare]
+  type t = Z.t [@@deriving compare]
 
   exception DivisionNotExact
 
-  let one = 1
+  let one = Z.one
 
-  let minus_one = -1
+  let minus_one = Z.minus_one
 
-  let of_int = function 0 -> None | i -> Some i
+  let of_big_int x = if Z.(equal x zero) then None else Some x
 
-  let opt_to_int = function None -> 0 | Some i -> i
+  let opt_to_big_int = function None -> Z.zero | Some i -> i
 
-  let is_one = Int.equal 1
+  let is_one = Z.equal one
 
-  let is_minus_one = Int.equal (-1)
+  let is_minus_one = Z.equal minus_one
 
-  let is_multiple mul div = Int.equal (mul mod div) 0
+  let is_multiple m d = Z.(equal (m mod d) zero)
 
-  let is_negative x = x < 0
+  let is_negative x = Z.(x < zero)
 
-  let is_positive x = x > 0
+  let is_positive x = Z.(x > zero)
 
-  let ( ~- ) = Int.( ~- )
+  let ( ~- ) = Z.( ~- )
 
-  let ( * ) = Int.( * )
+  let ( * ) = Z.( * )
 
-  let plus x y = of_int (x + y)
+  let plus x y = of_big_int Z.(x + y)
 
   let exact_div_exn num den =
-    if not (is_multiple num den) then raise DivisionNotExact ;
-    num / den
+    let q, r = Z.div_rem num den in
+    if Z.(equal r zero) then q else raise DivisionNotExact
 
 
-  let max = Int.max
+  let max = Z.max
 
-  let min = Int.min
+  let min = Z.min
 end
 
 module NonNegativeInt = struct
-  type t = int [@@deriving compare]
+  type t = Z.t [@@deriving compare]
 
-  let zero = 0
+  let zero = Z.zero
 
-  let one = 1
+  let one = Z.one
 
-  let is_zero = function 0 -> true | _ -> false
+  let is_zero = Z.equal zero
 
-  let is_one = function 1 -> true | _ -> false
+  let is_one = Z.equal one
 
-  let of_int i = if i < 0 then None else Some i
+  let of_big_int i = if Z.(i < zero) then None else Some i
 
   let of_int_exn i =
     assert (i >= 0) ;
+    Z.of_int i
+
+
+  let of_big_int_exn i =
+    assert (Z.(i >= zero)) ;
     i
 
 
-  let ( <= ) ~lhs ~rhs = Int.(lhs <= rhs)
+  let ( <= ) ~lhs ~rhs = lhs <= rhs
 
-  let ( + ) = Int.( + )
+  let ( + ) = Z.( + )
 
-  let ( * ) = Int.( * )
+  let ( * ) = Z.( * )
 
-  let max = Int.max
+  let max = Z.max
 
-  let pp = F.pp_print_int
+  let pp = Z.pp_print
 end
 
 module PositiveInt = struct
   type t = NonNegativeInt.t [@@deriving compare]
 
-  let one = 1
+  let one = Z.one
 
-  let of_int i = if i <= 0 then None else Some i
+  let of_big_int i = if Z.(i <= zero) then None else Some i
 
-  let succ = Int.succ
+  let succ = Z.succ
 
-  let pp = F.pp_print_int
+  let pp = Z.pp_print
 end
diff --git a/infer/src/bufferoverrun/ints.mli b/infer/src/bufferoverrun/ints.mli
index b1ed92d85..b54a11868 100644
--- a/infer/src/bufferoverrun/ints.mli
+++ b/infer/src/bufferoverrun/ints.mli
@@ -9,7 +9,7 @@ open! IStd
 module F = Format
 
 module NonZeroInt : sig
-  type t = private int [@@deriving compare]
+  type t = private Z.t [@@deriving compare]
 
   exception DivisionNotExact
 
@@ -17,15 +17,15 @@ module NonZeroInt : sig
 
   val minus_one : t
 
-  val of_int : int -> t option
+  val of_big_int : Z.t -> t option
 
-  val opt_to_int : t option -> int
+  val opt_to_big_int : t option -> Z.t
 
   val is_one : t -> bool
 
   val is_minus_one : t -> bool
 
-  val is_multiple : int -> t -> bool
+  val is_multiple : Z.t -> t -> bool
 
   val is_negative : t -> bool
 
@@ -45,16 +45,18 @@ module NonZeroInt : sig
 end
 
 module NonNegativeInt : sig
-  type t = private int [@@deriving compare]
+  type t = private Z.t [@@deriving compare]
 
   val zero : t
 
   val one : t
 
-  val of_int : int -> t option
+  val of_big_int : Z.t -> t option
 
   val of_int_exn : int -> t
 
+  val of_big_int_exn : Z.t -> t
+
   val is_zero : t -> bool
 
   val is_one : t -> bool
@@ -75,7 +77,7 @@ module PositiveInt : sig
 
   val one : t
 
-  val of_int : int -> t option
+  val of_big_int : Z.t -> t option
 
   val succ : t -> t
 
diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml
index 2692c955f..fcd6ec2ef 100644
--- a/infer/src/bufferoverrun/itv.ml
+++ b/infer/src/bufferoverrun/itv.ml
@@ -45,12 +45,12 @@ module NonNegativeBound = struct
   let of_bound b = if Bound.le b zero then zero else b
 
   let int_lb b =
-    Bound.int_lb b
-    |> Option.bind ~f:NonNegativeInt.of_int
+    Bound.big_int_lb b
+    |> Option.bind ~f:NonNegativeInt.of_big_int
     |> Option.value ~default:NonNegativeInt.zero
 
 
-  let int_ub b = Bound.int_ub b |> Option.map ~f:NonNegativeInt.of_int_exn
+  let int_ub b = Bound.big_int_ub b |> Option.map ~f:NonNegativeInt.of_big_int_exn
 
   let classify = function
     | Bound.PInf ->
@@ -62,7 +62,7 @@ module NonNegativeBound = struct
       | None ->
           Bounds.Symbolic b
       | Some c ->
-          Bounds.Constant (NonNegativeInt.of_int_exn c) )
+          Bounds.Constant (NonNegativeInt.of_big_int_exn c) )
 
 
   let subst b map =
@@ -198,7 +198,7 @@ module MakePolynomial (S : NonNegativeSymbol) = struct
 
   let mult_const : t -> NonNegativeInt.t -> t =
    fun p c ->
-    match PositiveInt.of_int (c :> int) with None -> zero | Some c -> mult_const_positive p c
+    match PositiveInt.of_big_int (c :> Z.t) with None -> zero | Some c -> mult_const_positive p c
 
 
   (* (c + r * R + s * S + t * T) x s
@@ -301,7 +301,7 @@ module MakePolynomial (S : NonNegativeSymbol) = struct
         (fun s p acc ->
           match S.subst s eval_sym with
           | Constant c -> (
-            match PositiveInt.of_int (c :> int) with
+            match PositiveInt.of_big_int (c :> Z.t) with
             | None ->
                 acc
             | Some c ->
@@ -326,10 +326,10 @@ module MakePolynomial (S : NonNegativeSymbol) = struct
       else ((s, PositiveInt.one), last :: others)
     in
     let pp_coeff fmt (c : NonNegativeInt.t) =
-      if (c :> int) > 1 then F.fprintf fmt "%a * " NonNegativeInt.pp c
+      if Z.((c :> Z.t) > one) then F.fprintf fmt "%a * " NonNegativeInt.pp c
     in
     let pp_exp fmt (e : PositiveInt.t) =
-      if (e :> int) > 1 then F.fprintf fmt "^%a" PositiveInt.pp e
+      if Z.((e :> Z.t) > one) then F.fprintf fmt "^%a" PositiveInt.pp e
     in
     let pp_magic_parentheses pp fmt x =
       let s = F.asprintf "%a" pp x in
@@ -522,6 +522,8 @@ module ItvPure = struct
 
   let of_int n = of_bound (Bound.of_int n)
 
+  let of_big_int n = of_bound (Bound.of_big_int n)
+
   let make_sym : unsigned:bool -> Typ.Procname.t -> SymbolTable.t -> SymbolPath.t -> Counter.t -> t
       =
    fun ~unsigned pname symbol_table path new_sym_num ->
@@ -555,10 +557,10 @@ module ItvPure = struct
 
   let is_nat : t -> bool = function l, Bound.PInf -> Bound.is_zero l | _ -> false
 
-  let is_const : t -> int option =
+  let is_const : t -> Z.t option =
    fun (l, u) ->
     match (Bound.is_const l, Bound.is_const u) with
-    | Some n, Some m when Int.equal n m ->
+    | Some n, Some m when Z.equal n m ->
         Some n
     | _, _ ->
         None
@@ -593,9 +595,9 @@ module ItvPure = struct
 
   let minus : t -> t -> t = fun i1 i2 -> plus i1 (neg i2)
 
-  let mult_const : int -> t -> t =
+  let mult_const : Z.t -> t -> t =
    fun n ((l, u) as itv) ->
-    match NonZeroInt.of_int n with
+    match NonZeroInt.of_big_int n with
     | None ->
         zero
     | Some n ->
@@ -607,9 +609,9 @@ module ItvPure = struct
 
   (* Returns a precise value only when all coefficients are divided by
      n without remainder. *)
-  let div_const : t -> int -> t =
+  let div_const : t -> Z.t -> t =
    fun ((l, u) as itv) n ->
-    match NonZeroInt.of_int n with
+    match NonZeroInt.of_big_int n with
     | None ->
         top
     | Some n ->
@@ -643,34 +645,40 @@ module ItvPure = struct
     match is_const y with
     | None ->
         top
-    | Some 0 ->
+    | Some n when Z.(equal n zero) ->
         x (* x % [0,0] does nothing. *)
     | Some m -> (
       match is_const x with
       | Some n ->
-          of_int (n mod m)
+          of_big_int Z.(n mod m)
       | None ->
-          let abs_m = abs m in
-          if is_ge_zero x then (Bound.zero, Bound.of_int (abs_m - 1))
-          else if is_le_zero x then (Bound.of_int (-abs_m + 1), Bound.zero)
-          else (Bound.of_int (-abs_m + 1), Bound.of_int (abs_m - 1)) )
+          let abs_m = Z.abs m in
+          if is_ge_zero x then (Bound.zero, Bound.of_big_int Z.(abs_m - one))
+          else if is_le_zero x then (Bound.of_big_int Z.(one - abs_m), Bound.zero)
+          else (Bound.of_big_int Z.(one - abs_m), Bound.of_big_int Z.(abs_m - one)) )
 
 
   (* x << [-1,-1] does nothing. *)
   let shiftlt : t -> t -> t =
-   fun x y -> match is_const y with Some n -> mult_const (1 lsl n) x | None -> top
+   fun x y ->
+    Option.value_map (is_const y) ~default:top ~f:(fun n ->
+        match Z.to_int n with
+        | n ->
+            if n < 0 then x else mult_const Z.(one lsl n) x
+        | exception Z.Overflow ->
+            top )
 
 
   (* x >> [-1,-1] does nothing. *)
   let shiftrt : t -> t -> t =
    fun x y ->
     match is_const y with
-    | Some n when Int.( <= ) n 0 ->
+    | Some n when Z.(leq n zero) ->
         x
-    | Some n when n >= 64 ->
+    | Some n when Z.(n >= of_int 64) ->
         zero
-    | Some n ->
-        div_const x (1 lsl n)
+    | Some n -> (
+      match Z.to_int n with n -> div_const x Z.(one lsl n) | exception Z.Overflow -> top )
     | None ->
         top
 
@@ -734,27 +742,27 @@ module ItvPure = struct
     | (l1, Bound.PInf), (_, u2) ->
         (l1, u2)
     | (l1, Bound.Linear (c1, s1)), (_, Bound.Linear (c2, s2)) when Bounds.SymLinear.eq s1 s2 ->
-        (l1, Bound.Linear (min c1 c2, s1))
+        (l1, Bound.Linear (Z.(min c1 c2), s1))
     | (l1, Bound.Linear (c, se)), (_, u) when Bounds.SymLinear.is_zero se && Bound.is_one_symbol u
       ->
-        (l1, Bound.mk_MinMax (0, Bound.Plus, Bound.Min, c, Bound.get_one_symbol u))
+        (l1, Bound.mk_MinMax (Z.zero, Bound.Plus, Bound.Min, c, Bound.get_one_symbol u))
     | (l1, u), (_, Bound.Linear (c, se)) when Bounds.SymLinear.is_zero se && Bound.is_one_symbol u
       ->
-        (l1, Bound.mk_MinMax (0, Bound.Plus, Bound.Min, c, Bound.get_one_symbol u))
+        (l1, Bound.mk_MinMax (Z.zero, Bound.Plus, Bound.Min, c, Bound.get_one_symbol u))
     | (l1, Bound.Linear (c, se)), (_, u) when Bounds.SymLinear.is_zero se && Bound.is_mone_symbol u
       ->
-        (l1, Bound.mk_MinMax (0, Bound.Minus, Bound.Max, -c, Bound.get_mone_symbol u))
+        (l1, Bound.mk_MinMax (Z.zero, Bound.Minus, Bound.Max, Z.neg c, Bound.get_mone_symbol u))
     | (l1, u), (_, Bound.Linear (c, se)) when Bounds.SymLinear.is_zero se && Bound.is_mone_symbol u
       ->
-        (l1, Bound.mk_MinMax (0, Bound.Minus, Bound.Max, -c, Bound.get_mone_symbol u))
+        (l1, Bound.mk_MinMax (Z.zero, Bound.Minus, Bound.Max, Z.neg c, Bound.get_mone_symbol u))
     | (l1, Bound.Linear (c1, se)), (_, Bound.MinMax (c2, Bound.Plus, Bound.Min, d2, se'))
     | (l1, Bound.MinMax (c2, Bound.Plus, Bound.Min, d2, se')), (_, Bound.Linear (c1, se))
       when Bounds.SymLinear.is_zero se ->
-        (l1, Bound.mk_MinMax (c2, Bound.Plus, Bound.Min, min (c1 - c2) d2, se'))
+        (l1, Bound.mk_MinMax (c2, Bound.Plus, Bound.Min, Z.(min (c1 - c2) d2), se'))
     | ( (l1, Bound.MinMax (c1, Bound.Plus, Bound.Min, d1, se1))
       , (_, Bound.MinMax (c2, Bound.Plus, Bound.Min, d2, se2)) )
-      when Int.equal c1 c2 && Symbol.equal se1 se2 ->
-        (l1, Bound.mk_MinMax (c1, Bound.Plus, Bound.Min, min d1 d2, se1))
+      when Z.equal c1 c2 && Symbol.equal se1 se2 ->
+        (l1, Bound.mk_MinMax (c1, Bound.Plus, Bound.Min, Z.min d1 d2, se1))
     | _ ->
         x
 
@@ -765,27 +773,27 @@ module ItvPure = struct
     | (Bound.MInf, u1), (l2, _) ->
         (l2, u1)
     | (Bound.Linear (c1, s1), u1), (Bound.Linear (c2, s2), _) when Bounds.SymLinear.eq s1 s2 ->
-        (Bound.Linear (max c1 c2, s1), u1)
+        (Bound.Linear (Z.max c1 c2, s1), u1)
     | (Bound.Linear (c, se), u1), (l, _) when Bounds.SymLinear.is_zero se && Bound.is_one_symbol l
       ->
-        (Bound.mk_MinMax (0, Bound.Plus, Bound.Max, c, Bound.get_one_symbol l), u1)
+        (Bound.mk_MinMax (Z.zero, Bound.Plus, Bound.Max, c, Bound.get_one_symbol l), u1)
     | (l, u1), (Bound.Linear (c, se), _) when Bounds.SymLinear.is_zero se && Bound.is_one_symbol l
       ->
-        (Bound.mk_MinMax (0, Bound.Plus, Bound.Max, c, Bound.get_one_symbol l), u1)
+        (Bound.mk_MinMax (Z.zero, Bound.Plus, Bound.Max, c, Bound.get_one_symbol l), u1)
     | (Bound.Linear (c, se), u1), (l, _) when Bounds.SymLinear.is_zero se && Bound.is_mone_symbol l
       ->
-        (Bound.mk_MinMax (0, Bound.Minus, Bound.Min, c, Bound.get_mone_symbol l), u1)
+        (Bound.mk_MinMax (Z.zero, Bound.Minus, Bound.Min, c, Bound.get_mone_symbol l), u1)
     | (l, u1), (Bound.Linear (c, se), _) when Bounds.SymLinear.is_zero se && Bound.is_mone_symbol l
       ->
-        (Bound.mk_MinMax (0, Bound.Minus, Bound.Min, c, Bound.get_mone_symbol l), u1)
+        (Bound.mk_MinMax (Z.zero, Bound.Minus, Bound.Min, c, Bound.get_mone_symbol l), u1)
     | (Bound.Linear (c1, se), u1), (Bound.MinMax (c2, Bound.Plus, Bound.Max, d2, se'), _)
     | (Bound.MinMax (c2, Bound.Plus, Bound.Max, d2, se'), u1), (Bound.Linear (c1, se), _)
       when Bounds.SymLinear.is_zero se ->
-        (Bound.mk_MinMax (c2, Bound.Plus, Bound.Max, max (c1 - c2) d2, se'), u1)
+        (Bound.mk_MinMax (c2, Bound.Plus, Bound.Max, Z.(max (c1 - c2) d2), se'), u1)
     | ( (Bound.MinMax (c1, Bound.Plus, Bound.Max, d1, se1), u1)
       , (Bound.MinMax (c2, Bound.Plus, Bound.Max, d2, se2), _) )
-      when Int.equal c1 c2 && Symbol.equal se1 se2 ->
-        (Bound.mk_MinMax (c1, Bound.Plus, Bound.Max, max d1 d2, se1), u1)
+      when Z.equal c1 c2 && Symbol.equal se1 se2 ->
+        (Bound.mk_MinMax (c1, Bound.Plus, Bound.Max, Z.max d1 d2, se1), u1)
     | _ ->
         x
 
@@ -915,11 +923,11 @@ let of_bool = function
 
 let of_int : int -> astate = fun n -> NonBottom (ItvPure.of_int n)
 
-let of_int_lit n = Option.value_map ~default:top ~f:of_int (IntLit.to_int n)
+let of_big_int : Z.t -> astate = fun n -> NonBottom (ItvPure.of_big_int n)
 
-let of_int64 : Int64.t -> astate =
- fun n -> Int64.to_int n |> Option.value_map ~f:of_int ~default:top
+let of_int_lit : IntLit.t -> astate = fun n -> of_big_int (IntLit.to_big_int n)
 
+let of_int64 : Int64.t -> astate = fun n -> of_big_int (Z.of_int64 n)
 
 let is_false : t -> bool = function NonBottom x -> ItvPure.is_false x | Bottom -> false
 
diff --git a/infer/src/bufferoverrun/itv.mli b/infer/src/bufferoverrun/itv.mli
index f55ef7bb5..dee9f58f7 100644
--- a/infer/src/bufferoverrun/itv.mli
+++ b/infer/src/bufferoverrun/itv.mli
@@ -160,6 +160,8 @@ val of_bool : Boolean.t -> t
 
 val of_int : int -> t
 
+val of_big_int : Z.t -> t
+
 val of_int_lit : IntLit.t -> t
 
 val of_int64 : Int64.t -> t
diff --git a/infer/src/dune.common.in b/infer/src/dune.common.in
index e8dd2992d..9421655fd 100644
--- a/infer/src/dune.common.in
+++ b/infer/src/dune.common.in
@@ -71,4 +71,5 @@ let common_libraries =
     ; "unix"
     ; "xmlm"
     ; "yojson"
+    ; "zarith"
     ; "zip" ]
diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/arith.c b/infer/tests/codetoanalyze/c/bufferoverrun/arith.c
index cb96ec5a6..8ef3789dd 100644
--- a/infer/tests/codetoanalyze/c/bufferoverrun/arith.c
+++ b/infer/tests/codetoanalyze/c/bufferoverrun/arith.c
@@ -140,3 +140,31 @@ void integer_overflow_by_multiplication_Bad_FN() {
     arr[z] = 0;
   }
 }
+
+void use_int64_max_Good() {
+  char arr[10];
+  int64_t x = INT64_MAX;
+  int64_t y = INT64_MAX - 5;
+  arr[x - y] = 0;
+}
+
+void use_int64_max_Bad() {
+  char arr[10];
+  int64_t x = INT64_MAX;
+  int64_t y = INT64_MAX - 15;
+  arr[x - y] = 0;
+}
+
+void use_uint64_max_Good() {
+  char arr[10];
+  uint64_t x = UINT64_MAX;
+  uint64_t y = UINT64_MAX - 5;
+  arr[x - y] = 0;
+}
+
+void use_uint64_max_Bad_FN() {
+  char arr[10];
+  uint64_t x = UINT64_MAX;
+  uint64_t y = UINT64_MAX - 15;
+  arr[x - y] = 0;
+}
diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp
index a60d3ed60..3af179fc2 100644
--- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp
+++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp
@@ -6,6 +6,7 @@ codetoanalyze/c/bufferoverrun/arith.c, modulo_signed_neg_Bad, 2, BUFFER_OVERRUN_
 codetoanalyze/c/bufferoverrun/arith.c, plus_linear_min2_Good_FP, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Call,Assignment,Return,ArrayAccess: Offset: [0, 14] Size: 10]
 codetoanalyze/c/bufferoverrun/arith.c, plus_linear_min3_Good_FP, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Call,Assignment,Return,ArrayAccess: Offset: [0, 25] Size: 20]
 codetoanalyze/c/bufferoverrun/arith.c, plus_linear_min_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Call,Assignment,Return,ArrayAccess: Offset: [0, 19] Size: 19]
+codetoanalyze/c/bufferoverrun/arith.c, use_int64_max_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 15 Size: 10]
 codetoanalyze/c/bufferoverrun/array_dynlength.c, init_variable_array, 3, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Offset: [3xlen.lb + 1, 3xlen.ub + 1] Size: [3xlen.lb + 1, 3xlen.ub + 1]]
 codetoanalyze/c/bufferoverrun/array_field.c, array_field_access_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 20 Size: 10]
 codetoanalyze/c/bufferoverrun/array_field.c, decreasing_pointer_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Assignment,Assignment,Assignment,ArrayAccess: Offset: -1 Size: 2]
diff --git a/opam b/opam
index 59dda8b99..725daca69 100644
--- a/opam
+++ b/opam
@@ -50,6 +50,7 @@ depends: [
   "sawja" {>="1.5.4"}
   "sqlite3"
   "xmlm" {>="1.2.0"}
+  "zarith" {>="1.7"}
 ]
 depexts: [
   [ ["ubuntu"] ["python2.7-dev"] ]
diff --git a/opam.lock b/opam.lock
index fe309bd7a..324907357 100644
--- a/opam.lock
+++ b/opam.lock
@@ -92,3 +92,4 @@ typerep = v0.11.0
 variantslib = v0.11.0
 xmlm = 1.3.0
 yojson = 1.4.1
+zarith = 1.7