From a6a766b5f5a6ed654c66c68be19b2ea2f68d190d Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Sun, 12 Jun 2016 16:56:51 -0700
Subject: [PATCH] Refactor Sil.Int into separate IntLit module

Summary:
This diff refactors Sil.Int, which represents integer literals, into a
separate module IntLit.  There are no dependencies forcing Sil.Int to
be a submodule of Sil, and it is also no simpler as a submodule.

Reviewed By: cristianoc

Differential Revision: D3422910

fbshipit-source-id: 63013f2
---
 infer/src/IR/IntLit.re                       | 139 +++++++++++++++++
 infer/src/IR/IntLit.rei                      |  97 ++++++++++++
 infer/src/IR/Sil.re                          | 152 ++----------------
 infer/src/IR/Sil.rei                         |  53 +------
 infer/src/backend/abs.ml                     |   4 +-
 infer/src/backend/absarray.ml                |   3 +-
 infer/src/backend/autounit.ml                |  84 +++++-----
 infer/src/backend/buckets.ml                 |   4 +-
 infer/src/backend/dom.ml                     |  50 +++---
 infer/src/backend/dotty.ml                   |   3 +-
 infer/src/backend/errdesc.ml                 |   2 +-
 infer/src/backend/errdesc.mli                |   2 +-
 infer/src/backend/localise.ml                |   6 +-
 infer/src/backend/localise.mli               |   4 +-
 infer/src/backend/modelBuiltins.ml           |   8 +-
 infer/src/backend/prop.ml                    | 154 +++++++++----------
 infer/src/backend/prop.mli                   |   4 +-
 infer/src/backend/prover.ml                  | 107 ++++++-------
 infer/src/backend/prover.mli                 |   4 +-
 infer/src/backend/rearrange.ml               |   2 +-
 infer/src/backend/symExec.ml                 |  24 +--
 infer/src/backend/tabulation.ml              |   2 +-
 infer/src/checkers/checkTraceCallSequence.ml |   6 +-
 infer/src/clang/cArithmetic_trans.ml         |  12 +-
 infer/src/clang/cTrans.ml                    |  22 +--
 infer/src/clang/cTrans_utils.ml              |   4 +-
 infer/src/clang/cType_to_sil_type.ml         |   2 +-
 infer/src/eradicate/typeCheck.ml             |   8 +-
 infer/src/harness/inhabit.ml                 |   6 +-
 infer/src/java/jTrans.ml                     |  18 +--
 infer/src/llvm/lTrans.ml                     |   4 +-
 infer/src/unit/analyzerTester.ml             |   2 +-
 32 files changed, 535 insertions(+), 457 deletions(-)
 create mode 100644 infer/src/IR/IntLit.re
 create mode 100644 infer/src/IR/IntLit.rei

diff --git a/infer/src/IR/IntLit.re b/infer/src/IR/IntLit.re
new file mode 100644
index 000000000..1a73aa8cd
--- /dev/null
+++ b/infer/src/IR/IntLit.re
@@ -0,0 +1,139 @@
+/*
+ * vim: set ft=rust:
+ * vim: set ft=reason:
+ *
+ * Copyright (c) 2009 - 2013 Monoidics ltd.
+ * Copyright (c) 2013 - present Facebook, Inc.
+ * All rights reserved.
+ *
+ * This source code is licensed under the BSD style license found in the
+ * LICENSE file in the root directory of this source tree. An additional grant
+ * of patent rights can be found in the PATENTS file in the same directory.
+ */
+
+open! Utils;
+
+let module F = Format;
+
+
+/** signed and unsigned integer literals */
+/* the first bool indicates whether this is an unsigned value,
+   and the second whether it is a pointer */
+type t = (bool, Int64.t, bool);
+
+let area u i =>
+  switch (i < 0L, u) {
+  | (true, false) => 1 /* only representable as signed */
+  | (false, _) => 2 /* in the intersection between signed and unsigned */
+  | (true, true) => 3 /* only representable as unsigned */
+  };
+
+let to_signed (unsigned, i, ptr) =>
+  if (area unsigned i == 3) {
+    None
+  } else {
+    Some
+      /* not representable as signed */
+      (false, i, ptr)
+  };
+
+let compare (unsigned1, i1, _) (unsigned2, i2, _) => {
+  let n = bool_compare unsigned1 unsigned2;
+  if (n != 0) {
+    n
+  } else {
+    Int64.compare i1 i2
+  }
+};
+
+let compare_value (unsigned1, i1, _) (unsigned2, i2, _) => {
+  let area1 = area unsigned1 i1;
+  let area2 = area unsigned2 i2;
+  let n = int_compare area1 area2;
+  if (n != 0) {
+    n
+  } else {
+    Int64.compare i1 i2
+  }
+};
+
+let eq i1 i2 => compare_value i1 i2 == 0;
+
+let neq i1 i2 => compare_value i1 i2 != 0;
+
+let leq i1 i2 => compare_value i1 i2 <= 0;
+
+let lt i1 i2 => compare_value i1 i2 < 0;
+
+let geq i1 i2 => compare_value i1 i2 >= 0;
+
+let gt i1 i2 => compare_value i1 i2 > 0;
+
+let of_int64 i => (false, i, false);
+
+let of_int32 i => of_int64 (Int64.of_int32 i);
+
+let of_int64_unsigned i unsigned => (unsigned, i, false);
+
+let of_int i => of_int64 (Int64.of_int i);
+
+let to_int (_, i, _) => Int64.to_int i;
+
+let null = (false, 0L, true);
+
+let zero = of_int 0;
+
+let one = of_int 1;
+
+let two = of_int 2;
+
+let minus_one = of_int (-1);
+
+let isone (_, i, _) => i == 1L;
+
+let iszero (_, i, _) => i == 0L;
+
+let isnull (_, i, ptr) => i == 0L && ptr;
+
+let isminusone (unsigned, i, _) => not unsigned && i == (-1L);
+
+let isnegative (unsigned, i, _) => not unsigned && i < 0L;
+
+let neg (unsigned, i, ptr) => (unsigned, Int64.neg i, ptr);
+
+let lift binop (unsigned1, i1, ptr1) (unsigned2, i2, ptr2) => (
+  unsigned1 || unsigned2,
+  binop i1 i2,
+  ptr1 || ptr2
+);
+
+let lift1 unop (unsigned, i, ptr) => (unsigned, unop i, ptr);
+
+let add i1 i2 => lift Int64.add i1 i2;
+
+let mul i1 i2 => lift Int64.mul i1 i2;
+
+let div i1 i2 => lift Int64.div i1 i2;
+
+let rem i1 i2 => lift Int64.rem i1 i2;
+
+let logand i1 i2 => lift Int64.logand i1 i2;
+
+let logor i1 i2 => lift Int64.logor i1 i2;
+
+let logxor i1 i2 => lift Int64.logxor i1 i2;
+
+let lognot i => lift1 Int64.lognot i;
+
+let sub i1 i2 => add i1 (neg i2);
+
+let pp f (unsigned, n, ptr) =>
+  if (ptr && n == 0L) {
+    F.fprintf f "null"
+  } else if unsigned {
+    F.fprintf f "%Lu" n
+  } else {
+    F.fprintf f "%Ld" n
+  };
+
+let to_string i => pp_to_string pp i;
diff --git a/infer/src/IR/IntLit.rei b/infer/src/IR/IntLit.rei
new file mode 100644
index 000000000..342e6b2de
--- /dev/null
+++ b/infer/src/IR/IntLit.rei
@@ -0,0 +1,97 @@
+/*
+ * vim: set ft=rust:
+ * vim: set ft=reason:
+ *
+ * Copyright (c) 2009 - 2013 Monoidics ltd.
+ * Copyright (c) 2013 - present Facebook, Inc.
+ * All rights reserved.
+ *
+ * This source code is licensed under the BSD style license found in the
+ * LICENSE file in the root directory of this source tree. An additional grant
+ * of patent rights can be found in the PATENTS file in the same directory.
+ */
+
+open! Utils;
+
+let module F = Format;
+
+
+/** signed and unsigned integer literals */
+type t;
+
+let add: t => t => t;
+
+
+/** compare integers ignoring the distinction between pointers and non-pointers */
+let compare: t => t => int;
+
+
+/** compare the value of the integers, notice this is different from const compare,
+    which distinguished between signed and unsigned +1 */
+let compare_value: t => t => int;
+
+let div: t => t => t;
+
+let eq: t => t => bool;
+
+let of_int: int => t;
+
+let of_int32: int32 => t;
+
+let of_int64: int64 => t;
+
+let of_int64_unsigned: int64 => bool => t;
+
+let geq: t => t => bool;
+
+let gt: t => t => bool;
+
+let isminusone: t => bool;
+
+let isnegative: t => bool;
+
+let isnull: t => bool;
+
+let isone: t => bool;
+
+let iszero: t => bool;
+
+let leq: t => t => bool;
+
+let logand: t => t => t;
+
+let lognot: t => t;
+
+let logor: t => t => t;
+
+let logxor: t => t => t;
+
+let lt: t => t => bool;
+
+let minus_one: t;
+
+let mul: t => t => t;
+
+let neg: t => t;
+
+let neq: t => t => bool;
+
+let null: t; /** null behaves like zero except for the function isnull */
+
+let one: t;
+
+let pp: F.formatter => t => unit;
+
+let rem: t => t => t;
+
+let sub: t => t => t;
+
+let to_int: t => int;
+
+let to_signed: t => option t; /** convert to signed if the value is representable */
+
+let to_string: t => string;
+
+let two: t;
+
+let zero: t;
diff --git a/infer/src/IR/Sil.re b/infer/src/IR/Sil.re
index da4cbb4cb..77c10ac7e 100644
--- a/infer/src/IR/Sil.re
+++ b/infer/src/IR/Sil.re
@@ -510,130 +510,6 @@ let module Subtype = {
 };
 
 
-/** module for signed and unsigned integers */
-let module Int: {
-  type t;
-  let add: t => t => t;
-  let compare: t => t => int;
-  let compare_value: t => t => int;
-  let div: t => t => t;
-  let eq: t => t => bool;
-  let of_int: int => t;
-  let of_int32: int32 => t;
-  let of_int64: int64 => t;
-  let of_int64_unsigned: int64 => bool => t;
-  let geq: t => t => bool;
-  let gt: t => t => bool;
-  let isminusone: t => bool;
-  let isone: t => bool;
-  let isnegative: t => bool;
-  let isnull: t => bool;
-  let iszero: t => bool;
-  let leq: t => t => bool;
-  let logand: t => t => t;
-  let lognot: t => t;
-  let logor: t => t => t;
-  let logxor: t => t => t;
-  let lt: t => t => bool;
-  let minus_one: t;
-  let mul: t => t => t;
-  let neg: t => t;
-  let neq: t => t => bool;
-  let null: t;
-  let one: t;
-  let pp: Format.formatter => t => unit;
-  let rem: t => t => t;
-  let sub: t => t => t;
-  let to_int: t => int;
-  let to_signed: t => option t;
-  let to_string: t => string;
-  let two: t;
-  let zero: t;
-} = {
-  /* the first bool indicates whether this is an unsigned value,
-     and the second whether it is a pointer */
-  type t = (bool, Int64.t, bool);
-  let area u i =>
-    switch (i < 0L, u) {
-    | (true, false) => 1 /* only representable as signed */
-    | (false, _) => 2 /* in the intersection between signed and unsigned */
-    | (true, true) => 3 /* only representable as unsigned */
-    };
-  let to_signed (unsigned, i, ptr) =>
-    if (area unsigned i == 3) {
-      None
-    } else {
-      Some
-        /* not representable as signed */
-        (false, i, ptr)
-    };
-  let compare (unsigned1, i1, _) (unsigned2, i2, _) => {
-    let n = bool_compare unsigned1 unsigned2;
-    if (n != 0) {
-      n
-    } else {
-      Int64.compare i1 i2
-    }
-  };
-  let compare_value (unsigned1, i1, _) (unsigned2, i2, _) => {
-    let area1 = area unsigned1 i1;
-    let area2 = area unsigned2 i2;
-    let n = int_compare area1 area2;
-    if (n != 0) {
-      n
-    } else {
-      Int64.compare i1 i2
-    }
-  };
-  let eq i1 i2 => compare_value i1 i2 == 0;
-  let neq i1 i2 => compare_value i1 i2 != 0;
-  let leq i1 i2 => compare_value i1 i2 <= 0;
-  let lt i1 i2 => compare_value i1 i2 < 0;
-  let geq i1 i2 => compare_value i1 i2 >= 0;
-  let gt i1 i2 => compare_value i1 i2 > 0;
-  let of_int64 i => (false, i, false);
-  let of_int32 i => of_int64 (Int64.of_int32 i);
-  let of_int64_unsigned i unsigned => (unsigned, i, false);
-  let of_int i => of_int64 (Int64.of_int i);
-  let to_int (_, i, _) => Int64.to_int i;
-  let null = (false, 0L, true);
-  let zero = of_int 0;
-  let one = of_int 1;
-  let two = of_int 2;
-  let minus_one = of_int (-1);
-  let isone (_, i, _) => i == 1L;
-  let iszero (_, i, _) => i == 0L;
-  let isnull (_, i, ptr) => i == 0L && ptr;
-  let isminusone (unsigned, i, _) => not unsigned && i == (-1L);
-  let isnegative (unsigned, i, _) => not unsigned && i < 0L;
-  let neg (unsigned, i, ptr) => (unsigned, Int64.neg i, ptr);
-  let lift binop (unsigned1, i1, ptr1) (unsigned2, i2, ptr2) => (
-    unsigned1 || unsigned2,
-    binop i1 i2,
-    ptr1 || ptr2
-  );
-  let lift1 unop (unsigned, i, ptr) => (unsigned, unop i, ptr);
-  let add i1 i2 => lift Int64.add i1 i2;
-  let mul i1 i2 => lift Int64.mul i1 i2;
-  let div i1 i2 => lift Int64.div i1 i2;
-  let rem i1 i2 => lift Int64.rem i1 i2;
-  let logand i1 i2 => lift Int64.logand i1 i2;
-  let logor i1 i2 => lift Int64.logor i1 i2;
-  let logxor i1 i2 => lift Int64.logxor i1 i2;
-  let lognot i => lift1 Int64.lognot i;
-  let sub i1 i2 => add i1 (neg i2);
-  let pp f (unsigned, n, ptr) =>
-    if (ptr && n == 0L) {
-      F.fprintf f "null"
-    } else if unsigned {
-      F.fprintf f "%Lu" n
-    } else {
-      F.fprintf f "%Ld" n
-    };
-  let to_string i => pp_to_string pp i;
-};
-
-
 /** Flags for a procedure call */
 type call_flags = {
   cf_virtual: bool,
@@ -720,7 +596,7 @@ and attribute_category =
 and closure = {name: Procname.t, captured_vars: list (exp, Pvar.t, typ)}
 /** Constants */
 and const =
-  | Cint of Int.t /** integer constants */
+  | Cint of IntLit.t /** integer constants */
   | Cfun of Procname.t /** function names */
   | Cstr of string /** string constants */
   | Cfloat of float /** float constants */
@@ -742,7 +618,7 @@ and struct_typ = {
   struct_annotations: item_annotation /** annotations */
 }
 /** statically determined length of an array type, if any */
-and static_length = option Int.t
+and static_length = option IntLit.t
 /** dynamically determined length of an array value, if any */
 and dynamic_length = option exp
 /** types for sil (structured) expressions */
@@ -1005,9 +881,9 @@ let typ_strip_ptr =
 
 let zero_value_of_numerical_type typ =>
   switch typ {
-  | Tint _ => Const (Cint Int.zero)
+  | Tint _ => Const (Cint IntLit.zero)
   | Tfloat _ => Const (Cfloat 0.0)
-  | Tptr _ => Const (Cint Int.null)
+  | Tptr _ => Const (Cint IntLit.null)
   | _ => assert false
   };
 
@@ -1033,12 +909,12 @@ let fld_equal fld1 fld2 => fld_compare fld1 fld2 == 0;
 
 let exp_is_zero =
   fun
-  | Const (Cint n) => Int.iszero n
+  | Const (Cint n) => IntLit.iszero n
   | _ => false;
 
 let exp_is_null_literal =
   fun
-  | Const (Cint n) => Int.isnull n
+  | Const (Cint n) => IntLit.isnull n
   | _ => false;
 
 let exp_is_this =
@@ -1062,7 +938,7 @@ let ikind_is_unsigned =
   | IULongLong => true
   | _ => false;
 
-let int_of_int64_kind i ik => Int.of_int64_unsigned i (ikind_is_unsigned ik);
+let int_of_int64_kind i ik => IntLit.of_int64_unsigned i (ikind_is_unsigned ik);
 
 let unop_compare o1 o2 =>
   switch (o1, o2) {
@@ -1414,7 +1290,7 @@ let const_kind_equal c1 c2 => {
 
 let rec const_compare (c1: const) (c2: const) :int =>
   switch (c1, c2) {
-  | (Cint i1, Cint i2) => Int.compare i1 i2
+  | (Cint i1, Cint i2) => IntLit.compare i1 i2
   | (Cint _, _) => (-1)
   | (_, Cint _) => 1
   | (Cfun fn1, Cfun fn2) => Procname.compare fn1 fn2
@@ -2311,7 +2187,7 @@ and attribute_to_string pe =>
   | Aunsubscribed_observer => "UNSUBSCRIBED_OBSERVER"
 and pp_const pe f =>
   fun
-  | Cint i => Int.pp f i
+  | Cint i => IntLit.pp f i
   | Cfun fn =>
     switch pe.pe_kind {
     | PP_HTML => F.fprintf f "_fun_%s" (Escape.escape_xml (Procname.to_string fn))
@@ -2629,7 +2505,7 @@ let d_instr_list (il: list instr) => L.add_print_action (L.PTinstr_list, Obj.rep
 let pp_atom pe0 f a => {
   let (pe, changed) = color_pre_wrapper pe0 f a;
   switch a {
-  | Aeq (BinOp op e1 e2) (Const (Cint i)) when Int.isone i =>
+  | Aeq (BinOp op e1 e2) (Const (Cint i)) when IntLit.isone i =>
     switch pe.pe_kind {
     | PP_TEXT
     | PP_HTML => F.fprintf f "%a" (pp_exp pe) (BinOp op e1 e2)
@@ -3400,19 +3276,19 @@ let exp_float v => Const (Cfloat v);
 
 
 /** Integer constant 0 */
-let exp_zero = exp_int Int.zero;
+let exp_zero = exp_int IntLit.zero;
 
 
 /** Null constant */
-let exp_null = exp_int Int.null;
+let exp_null = exp_int IntLit.null;
 
 
 /** Integer constant 1 */
-let exp_one = exp_int Int.one;
+let exp_one = exp_int IntLit.one;
 
 
 /** Integer constant -1 */
-let exp_minus_one = exp_int Int.minus_one;
+let exp_minus_one = exp_int IntLit.minus_one;
 
 
 /** Create integer constant corresponding to the boolean value */
diff --git a/infer/src/IR/Sil.rei b/infer/src/IR/Sil.rei
index ecef79342..bcfc95214 100644
--- a/infer/src/IR/Sil.rei
+++ b/infer/src/IR/Sil.rei
@@ -168,49 +168,6 @@ let module Subtype: {
 };
 
 
-/** module for signed and unsigned integers */
-let module Int: {
-  type t;
-  let add: t => t => t;
-
-  /** compare the value of the integers, notice this is different from const compare,
-      which distinguished between signed and unsigned +1 */
-  let compare_value: t => t => int;
-  let div: t => t => t;
-  let eq: t => t => bool;
-  let of_int: int => t;
-  let of_int32: int32 => t;
-  let of_int64: int64 => t;
-  let geq: t => t => bool;
-  let gt: t => t => bool;
-  let isminusone: t => bool;
-  let isnegative: t => bool;
-  let isnull: t => bool;
-  let isone: t => bool;
-  let iszero: t => bool;
-  let leq: t => t => bool;
-  let logand: t => t => t;
-  let lognot: t => t;
-  let logor: t => t => t;
-  let logxor: t => t => t;
-  let lt: t => t => bool;
-  let minus_one: t;
-  let mul: t => t => t;
-  let neg: t => t;
-  let neq: t => t => bool;
-  let null: t; /** null behaves like zero except for the function isnull */
-  let one: t;
-  let pp: F.formatter => t => unit;
-  let rem: t => t => t;
-  let sub: t => t => t;
-  let to_int: t => int;
-  let to_signed: t => option t; /** convert to signed if the value is representable */
-  let to_string: t => string;
-  let two: t;
-  let zero: t;
-};
-
-
 /** Flags for a procedure call */
 type call_flags = {
   cf_virtual: bool,
@@ -293,7 +250,7 @@ and attribute_category =
 and closure = {name: Procname.t, captured_vars: list (exp, Pvar.t, typ)}
 /** Constants */
 and const =
-  | Cint of Int.t /** integer constants */
+  | Cint of IntLit.t /** integer constants */
   | Cfun of Procname.t /** function names */
   | Cstr of string /** string constants */
   | Cfloat of float /** float constants */
@@ -315,7 +272,7 @@ and struct_typ = {
   struct_annotations: item_annotation /** annotations */
 }
 /** statically determined length of an array type, if any */
-and static_length = option Int.t
+and static_length = option IntLit.t
 /** dynamically determined length of an array value, if any */
 and dynamic_length = option exp
 /** Types for sil (structured) expressions. */
@@ -674,9 +631,9 @@ let ikind_is_char: ikind => bool;
 let ikind_is_unsigned: ikind => bool;
 
 
-/** Convert an int64 into an Int.t given the kind:
+/** Convert an int64 into an IntLit.t given the kind:
     the int64 is interpreted as unsigned according to the kind */
-let int_of_int64_kind: int64 => ikind => Int.t;
+let int_of_int64_kind: int64 => ikind => IntLit.t;
 
 
 /** Comparision for ptr_kind */
@@ -1181,7 +1138,7 @@ let exp_minus_one: exp;
 
 
 /** Create integer constant */
-let exp_int: Int.t => exp;
+let exp_int: IntLit.t => exp;
 
 
 /** Create float constant */
diff --git a/infer/src/backend/abs.ml b/infer/src/backend/abs.ml
index e9a63edd5..a8ccdb98c 100644
--- a/infer/src/backend/abs.ml
+++ b/infer/src/backend/abs.ml
@@ -781,7 +781,7 @@ let abstract_pure_part p ~(from_abstract_footprint: bool) =
            | Sil.Aeq (Sil.Const (Sil.Cint i), Sil.BinOp (Sil.Lt, _, _))
            | Sil.Aeq (Sil.BinOp (Sil.Lt, _, _), Sil.Const (Sil.Cint i))
            | Sil.Aeq (Sil.Const (Sil.Cint i), Sil.BinOp (Sil.Le, _, _))
-           | Sil.Aeq (Sil.BinOp (Sil.Le, _, _), Sil.Const (Sil.Cint i)) when Sil.Int.isone i ->
+           | Sil.Aeq (Sil.BinOp (Sil.Le, _, _), Sil.Const (Sil.Cint i)) when IntLit.isone i ->
                a :: pi
            | Sil.Aeq (Sil.Var name, e) when not (Ident.is_primed name) ->
                (match e with
@@ -930,7 +930,7 @@ let should_raise_objc_leak hpred =
   match hpred with
   | Sil.Hpointsto(_, Sil.Estruct((fn, Sil.Eexp( (Sil.Const (Sil.Cint i)), _)):: _, _),
                   Sil.Sizeof (typ, _, _))
-    when Ident.fieldname_is_hidden fn && Sil.Int.gt i Sil.Int.zero (* counter > 0 *) ->
+    when Ident.fieldname_is_hidden fn && IntLit.gt i IntLit.zero (* counter > 0 *) ->
       Mleak_buckets.should_raise_objc_leak typ
   | _ -> None
 
diff --git a/infer/src/backend/absarray.ml b/infer/src/backend/absarray.ml
index f274cbebf..abda08c79 100644
--- a/infer/src/backend/absarray.ml
+++ b/infer/src/backend/absarray.ml
@@ -578,7 +578,8 @@ let remove_redundant_elements prop =
       modified := true;
       false in
     match e, se with
-    | Sil.Const (Sil.Cint i), Sil.Eexp (Sil.Var id, _) when (not fp_part || Sil.Int.iszero i) && Ident.is_normal id = false && occurs_at_most_once id ->
+    | Sil.Const (Sil.Cint i), Sil.Eexp (Sil.Var id, _)
+      when (not fp_part || IntLit.iszero i) && not (Ident.is_normal id) && occurs_at_most_once id ->
         remove () (* unknown value can be removed in re-execution mode or if the index is zero *)
     | Sil.Var id, Sil.Eexp _ when Ident.is_normal id = false && occurs_at_most_once id ->
         remove () (* index unknown can be removed *)
diff --git a/infer/src/backend/autounit.ml b/infer/src/backend/autounit.ml
index 6f4b19133..d9e4317cd 100644
--- a/infer/src/backend/autounit.ml
+++ b/infer/src/backend/autounit.ml
@@ -15,24 +15,24 @@ open! Utils
 module L = Logging
 module F = Format
 
-let (++) = Sil.Int.add
-let (--) = Sil.Int.sub
+let (++) = IntLit.add
+let (--) = IntLit.sub
 
 module IdMap = Map.Make (Ident) (** maps from identifiers *)
 
 (** Constraint solving module *)
 module Constraint : sig
   (** Collect constraints on [vars] from [pi], and return a satisfying instantiation *)
-  val solve_from_pure : Sil.atom list -> Ident.t list -> Sil.Int.t IdMap.t
+  val solve_from_pure : Sil.atom list -> Ident.t list -> IntLit.t IdMap.t
 end = struct
   (** flag for debug mode of the module *)
   let debug = false
 
   (** denote a range of values [bottom] <= val <= [top], except [excluded] *)
   type range =
-    { mutable bottom: Sil.Int.t option; (** lower bound *)
-      mutable excluded: Sil.Int.t list; (** individual values not in range *)
-      mutable top: Sil.Int.t option; (** upper bound *) }
+    { mutable bottom: IntLit.t option; (** lower bound *)
+      mutable excluded: IntLit.t list; (** individual values not in range *)
+      mutable top: IntLit.t option; (** upper bound *) }
 
   type eval = range IdMap.t (** evaluation for variables *)
 
@@ -44,8 +44,9 @@ end = struct
   let pp_range id fmt rng =
     let pp_opt fmt = function
       | None -> F.fprintf fmt "_"
-      | Some n -> Sil.Int.pp fmt n in
-    F.fprintf fmt "%a <= %a <= %a [%a]" pp_opt rng.bottom (Ident.pp pe_text) id pp_opt rng.top (pp_comma_seq Sil.Int.pp) rng.excluded
+      | Some n -> IntLit.pp fmt n in
+    F.fprintf fmt "%a <= %a <= %a [%a]"
+      pp_opt rng.bottom (Ident.pp pe_text) id pp_opt rng.top (pp_comma_seq IntLit.pp) rng.excluded
 
   (** pretty print an evaluation *)
   let pp_eval fmt ev =
@@ -64,22 +65,22 @@ end = struct
   let gt_bottom i r =
     match r.bottom with
     | None -> true
-    | Some j -> Sil.Int.gt i j
+    | Some j -> IntLit.gt i j
 
   let geq_bottom i r =
     match r.bottom with
     | None -> true
-    | Some j -> Sil.Int.geq i j
+    | Some j -> IntLit.geq i j
 
   let lt_top i r =
     match r.top with
     | None -> true
-    | Some j -> Sil.Int.lt i j
+    | Some j -> IntLit.lt i j
 
   let leq_top i r =
     match r.top with
     | None -> true
-    | Some j -> Sil.Int.leq i j
+    | Some j -> IntLit.leq i j
 
   (** normalize [r]: the excluded elements must be strictly between bottom and top *)
   let normalize r =
@@ -87,17 +88,17 @@ end = struct
     let rec normalize_bottom () = match r.bottom with
       | None -> ()
       | Some i ->
-          if IList.mem Sil.Int.eq i r.excluded then begin
-            r.excluded <- IList.filter (Sil.Int.neq i) r.excluded;
-            r.bottom <- Some (i ++ Sil.Int.one);
+          if IList.mem IntLit.eq i r.excluded then begin
+            r.excluded <- IList.filter (IntLit.neq i) r.excluded;
+            r.bottom <- Some (i ++ IntLit.one);
             normalize_bottom ()
           end in
     let rec normalize_top () = match r.top with
       | None -> ()
       | Some i ->
-          if IList.mem Sil.Int.eq i r.excluded then begin
-            r.excluded <- IList.filter (Sil.Int.neq i) r.excluded;
-            r.top <- Some (i -- Sil.Int.one);
+          if IList.mem IntLit.eq i r.excluded then begin
+            r.excluded <- IList.filter (IntLit.neq i) r.excluded;
+            r.top <- Some (i -- IntLit.one);
             normalize_top ()
           end in
     normalize_bottom ();
@@ -112,7 +113,7 @@ end = struct
 
   (** exclude one element from the range *)
   let add_excluded r id i =
-    if geq_bottom i r && leq_top i r && not (IList.mem Sil.Int.eq i r.excluded)
+    if geq_bottom i r && leq_top i r && not (IList.mem IntLit.eq i r.excluded)
     then begin
       r.excluded <- i :: r.excluded;
       normalize r;
@@ -143,42 +144,49 @@ end = struct
     let found = ref None in
     let num_iter = IList.length rng.excluded in
     let try_candidate candidate =
-      if geq_bottom candidate rng && leq_top candidate rng && not (IList.mem Sil.Int.eq candidate rng.excluded)
-      then (found := Some candidate; rng.bottom <- Some candidate; rng.top <- Some candidate; rng.excluded <- []) in
+      if geq_bottom candidate rng
+      && leq_top candidate rng
+      && not (IList.mem IntLit.eq candidate rng.excluded)
+      then (
+        found := Some candidate;
+        rng.bottom <- Some candidate;
+        rng.top <- Some candidate;
+        rng.excluded <- []
+      ) in
     let search_up () =
-      let base = match rng.bottom with None -> Sil.Int.zero | Some n -> n in
+      let base = match rng.bottom with None -> IntLit.zero | Some n -> n in
       for i = 0 to num_iter do
         if !found = None then
-          let candidate = Sil.Int.add base (Sil.Int.of_int i) in
+          let candidate = IntLit.add base (IntLit.of_int i) in
           try_candidate candidate
       done in
     let search_down () =
-      let base = match rng.top with None -> Sil.Int.zero | Some n -> n in
+      let base = match rng.top with None -> IntLit.zero | Some n -> n in
       for i = 0 to num_iter do
         if !found = None then
-          let candidate = Sil.Int.sub base (Sil.Int.of_int i) in
+          let candidate = IntLit.sub base (IntLit.of_int i) in
           try_candidate candidate
       done in
     search_up ();
     if !found = None then search_down ();
     if !found = None then
       (L.err "Constraint Error: empty range %a@." (pp_range id) rng;
-       rng.top <- Some Sil.Int.zero;
-       rng.bottom <- Some Sil.Int.zero;
+       rng.top <- Some IntLit.zero;
+       rng.bottom <- Some IntLit.zero;
        rng.excluded <- [])
 
   (** return the solution if the id is solved (has unique solution) *)
   let solved ev id =
     let rng = IdMap.find id ev in
     match rng.bottom, rng.top with
-    | Some n1, Some n2 when Sil.Int.eq n1 n2 -> Some n1
+    | Some n1, Some n2 when IntLit.eq n1 n2 -> Some n1
     | _ -> None
 
   let rec pi_iter do_le do_lt do_neq pi =
     let do_atom a = match a with
-      | Sil.Aeq (Sil.BinOp (Sil.Le, e1, e2), Sil.Const (Sil.Cint i)) when Sil.Int.isone i ->
+      | Sil.Aeq (Sil.BinOp (Sil.Le, e1, e2), Sil.Const (Sil.Cint i)) when IntLit.isone i ->
           do_le e1 e2
-      | Sil.Aeq (Sil.BinOp (Sil.Lt, e1, e2), Sil.Const (Sil.Cint i)) when Sil.Int.isone i ->
+      | Sil.Aeq (Sil.BinOp (Sil.Lt, e1, e2), Sil.Const (Sil.Cint i)) when IntLit.isone i ->
           do_lt e1 e2
       | Sil.Aeq _ -> ()
       | Sil.Aneq (e1, e2) ->
@@ -203,10 +211,10 @@ end = struct
       | Some _, Some n -> add_bottom rng id n
       | _ -> () in
     let (+++) n1_op n2_op = match n1_op, n2_op with
-      | Some n1, Some n2 -> Some (Sil.Int.add n1 n2)
+      | Some n1, Some n2 -> Some (IntLit.add n1 n2)
       | _ -> None in
     let (---) n1_op n2_op = match n1_op, n2_op with
-      | Some n1, Some n2 -> Some (Sil.Int.sub n1 n2)
+      | Some n1, Some n2 -> Some (IntLit.sub n1 n2)
       | _ -> None in
     let do_le e1 e2 = match e1, e2 with
       | Sil.Var id, Sil.Const (Sil.Cint n) ->
@@ -226,12 +234,12 @@ end = struct
     let do_lt e1 e2 = match e1, e2 with
       | Sil.Const (Sil.Cint n), Sil.Var id ->
           let rng = IdMap.find id ev in
-          add_bottom rng id (n ++ Sil.Int.one)
+          add_bottom rng id (n ++ IntLit.one)
       | Sil.Const (Sil.Cint n), Sil.BinOp (Sil.PlusA, Sil.Var id1, Sil.Var id2) ->
           let rng1 = IdMap.find id1 ev in
           let rng2 = IdMap.find id2 ev in
-          update_bottom rng1 id1 (Some (n ++ Sil.Int.one) --- rng2.top);
-          update_bottom rng2 id2 (Some (n ++ Sil.Int.one) --- rng1.top)
+          update_bottom rng1 id1 (Some (n ++ IntLit.one) --- rng2.top);
+          update_bottom rng2 id2 (Some (n ++ IntLit.one) --- rng1.top)
       | _ -> if debug then assert false in
     let rec do_neq e1 e2 = match e1, e2 with
       | Sil.Var id, Sil.Const (Sil.Cint n)
@@ -511,13 +519,13 @@ let gen_init_vars code solutions idmap =
     if not alloc then
       let const = match typ with
         | Sil.Tint _ | Sil.Tvoid ->
-            get_const id (Sil.Cint Sil.Int.zero)
+            get_const id (Sil.Cint IntLit.zero)
         | Sil.Tfloat _ ->
             Sil.Cfloat 0.0
         | Sil.Tptr _ ->
-            get_const id (Sil.Cint Sil.Int.zero)
+            get_const id (Sil.Cint IntLit.zero)
         | Sil.Tfun _ ->
-            Sil.Cint Sil.Int.zero
+            Sil.Cint IntLit.zero
         | typ ->
             L.err "do_vinfo type undefined: %a@." (Sil.pp_typ_full pe) typ;
             assert false in
diff --git a/infer/src/backend/buckets.ml b/infer/src/backend/buckets.ml
index 36293d8f9..298c811af 100644
--- a/infer/src/backend/buckets.ml
+++ b/infer/src/backend/buckets.ml
@@ -72,14 +72,14 @@ let check_access access_opt de_opt =
     let formal_param_used_in_call = ref false in
     let has_call_or_sets_null node =
       let rec exp_is_null exp = match exp with
-        | Sil.Const (Sil.Cint n) -> Sil.Int.iszero n
+        | Sil.Const (Sil.Cint n) -> IntLit.iszero n
         | Sil.Cast (_, e) -> exp_is_null e
         | Sil.Var _
         | Sil.Lvar _ ->
             begin
               match State.get_const_map () node exp with
               | Some (Sil.Cint n) ->
-                  Sil.Int.iszero n
+                  IntLit.iszero n
               | _ -> false
             end
         | _ -> false in
diff --git a/infer/src/backend/dom.ml b/infer/src/backend/dom.ml
index e3c2d625d..6f2875ec8 100644
--- a/infer/src/backend/dom.ml
+++ b/infer/src/backend/dom.ml
@@ -15,8 +15,8 @@ open! Utils
 module L = Logging
 module F = Format
 
-let (++) = Sil.Int.add
-let (--) = Sil.Int.sub
+let (++) = IntLit.add
+let (--) = IntLit.sub
 
 (** {2 Utility functions for ids} *)
 
@@ -466,14 +466,14 @@ end = struct
     let ineq_upper = Prop.mk_inequality (Sil.BinOp(Sil.Le, e, upper)) in
     ineq_lower:: ineq_upper:: acc
 
-  let minus2_to_2 = IList.map Sil.Int.of_int [-2; -1; 0; 1; 2]
+  let minus2_to_2 = IList.map IntLit.of_int [-2; -1; 0; 1; 2]
 
   let get_induced_pi () =
     let t_sorted = IList.sort entry_compare !t in
 
     let add_and_chk_eq e1 e1' n =
       match e1, e1' with
-      | Sil.Const (Sil.Cint n1), Sil.Const (Sil.Cint n1') -> Sil.Int.eq (n1 ++ n) n1'
+      | Sil.Const (Sil.Cint n1), Sil.Const (Sil.Cint n1') -> IntLit.eq (n1 ++ n) n1'
       | _ -> false in
     let add_and_gen_eq e e' n =
       let e_plus_n = Sil.BinOp(Sil.PlusA, e, Sil.exp_int n) in
@@ -500,7 +500,8 @@ end = struct
     let f_ineqs acc (e1, e2, e) =
       match e1, e2 with
       | Sil.Const (Sil.Cint n1), Sil.Const (Sil.Cint n2) ->
-          let strict_lower1, upper1 = if Sil.Int.leq n1 n2 then (n1 -- Sil.Int.one, n2) else (n2 -- Sil.Int.one, n1) in
+          let strict_lower1, upper1 =
+            if IntLit.leq n1 n2 then (n1 -- IntLit.one, n2) else (n2 -- IntLit.one, n1) in
           let e_strict_lower1 = Sil.exp_int strict_lower1 in
           let e_upper1 = Sil.exp_int upper1 in
           get_induced_atom acc e_strict_lower1 e_upper1 e
@@ -592,12 +593,12 @@ end = struct
     let f v = match v, side with
       | (Sil.BinOp (Sil.PlusA, e1', Sil.Const (Sil.Cint i)), e2, e'), Lhs
         when Sil.exp_equal e e1' ->
-          let c' = Sil.exp_int (Sil.Int.neg i) in
+          let c' = Sil.exp_int (IntLit.neg i) in
           let v' = (e1', Sil.BinOp(Sil.PlusA, e2, c'), Sil.BinOp (Sil.PlusA, e', c')) in
           res := v'::!res
       | (e1, Sil.BinOp (Sil.PlusA, e2', Sil.Const (Sil.Cint i)), e'), Rhs
         when Sil.exp_equal e e2' ->
-          let c' = Sil.exp_int (Sil.Int.neg i) in
+          let c' = Sil.exp_int (IntLit.neg i) in
           let v' = (Sil.BinOp(Sil.PlusA, e1, c'), e2', Sil.BinOp (Sil.PlusA, e', c')) in
           res := v'::!res
       | _ -> () in
@@ -723,13 +724,13 @@ end = struct
 
         | Sil.Aeq(Sil.BinOp(Sil.Le, e, e'), Sil.Const (Sil.Cint i))
         | Sil.Aeq(Sil.Const (Sil.Cint i), Sil.BinOp(Sil.Le, e, e'))
-          when Sil.Int.isone i && (exp_contains_only_normal_ids e') ->
+          when IntLit.isone i && (exp_contains_only_normal_ids e') ->
             let construct e0 = Prop.mk_inequality (Sil.BinOp(Sil.Le, e0, e')) in
             build_other_atoms construct side e
 
         | Sil.Aeq(Sil.BinOp(Sil.Lt, e', e), Sil.Const (Sil.Cint i))
         | Sil.Aeq(Sil.Const (Sil.Cint i), Sil.BinOp(Sil.Lt, e', e))
-          when Sil.Int.isone i && (exp_contains_only_normal_ids e') ->
+          when IntLit.isone i && (exp_contains_only_normal_ids e') ->
             let construct e0 = Prop.mk_inequality (Sil.BinOp(Sil.Lt, e', e0)) in
             build_other_atoms construct side e
 
@@ -975,7 +976,7 @@ and length_partial_join len1 len2 = match len1, len2 with
   | _ -> exp_partial_join len1 len2
 
 and static_length_partial_join l1 l2 =
-  option_partial_join (fun len1 len2 -> if Sil.Int.eq len1 len2 then Some len1 else None) l1 l2
+  option_partial_join (fun len1 len2 -> if IntLit.eq len1 len2 then Some len1 else None) l1 l2
 
 and dynamic_length_partial_join l1 l2 =
   option_partial_join (fun len1 len2 -> Some (length_partial_join len1 len2)) l1 l2
@@ -1548,8 +1549,12 @@ let rec sigma_partial_meet' (sigma_acc: Prop.sigma) (sigma1_in: Prop.sigma) (sig
 let sigma_partial_meet (sigma1: Prop.sigma) (sigma2: Prop.sigma) : Prop.sigma =
   sigma_partial_meet' [] sigma1 sigma2
 
-let widening_top = Sil.Int.of_int64 Int64.max_int -- Sil.Int.of_int 1000 (* nearly max_int but not so close to overflow *)
-let widening_bottom = Sil.Int.of_int64 Int64.min_int ++ Sil.Int.of_int 1000 (* nearly min_int but not so close to underflow *)
+let widening_top =
+  (* nearly max_int but not so close to overflow *)
+  IntLit.of_int64 Int64.max_int -- IntLit.of_int 1000
+let widening_bottom =
+  (* nearly min_int but not so close to underflow *)
+  IntLit.of_int64 Int64.min_int ++ IntLit.of_int 1000
 
 (** {2 Join and Meet for Pi} *)
 let pi_partial_join mode
@@ -1566,24 +1571,24 @@ let pi_partial_join mode
     let len_list = ref [] in
     let do_hpred = function
       | Sil.Hpointsto (_, Sil.Earray (Sil.Const (Sil.Cint n), _, _), _) ->
-          (if Sil.Int.geq n Sil.Int.one then len_list := n :: !len_list)
+          (if IntLit.geq n IntLit.one then len_list := n :: !len_list)
       | _ -> () in
     IList.iter do_hpred (Prop.get_sigma prop);
     !len_list in
   let bounds =
     let bounds1 = get_array_len ep1 in
     let bounds2 = get_array_len ep2 in
-    let bounds_sorted = IList.sort Sil.Int.compare_value (bounds1@bounds2) in
-    IList.rev (IList.remove_duplicates Sil.Int.compare_value bounds_sorted) in
+    let bounds_sorted = IList.sort IntLit.compare_value (bounds1@bounds2) in
+    IList.rev (IList.remove_duplicates IntLit.compare_value bounds_sorted) in
   let widening_atom a =
     (* widening heuristic for upper bound: take the length of some array, -2 and -1 *)
     match Prop.atom_exp_le_const a, bounds with
     | Some (e, n), len :: _ ->
-        let first_try = Sil.Int.sub len Sil.Int.one in
-        let second_try = Sil.Int.sub len Sil.Int.two in
+        let first_try = IntLit.sub len IntLit.one in
+        let second_try = IntLit.sub len IntLit.two in
         let bound =
-          if Sil.Int.leq n first_try then
-            if Sil.Int.leq n second_try then second_try else first_try
+          if IntLit.leq n first_try then
+            if IntLit.leq n second_try then second_try else first_try
           else widening_top in
         let a' = Prop.mk_inequality (Sil.BinOp(Sil.Le, e, Sil.exp_int bound)) in
         Some a'
@@ -1596,18 +1601,19 @@ let pi_partial_join mode
           match Prop.atom_const_lt_exp a with
           | None -> None
           | Some (n, e) ->
-              let bound = if Sil.Int.leq Sil.Int.minus_one n then Sil.Int.minus_one else widening_bottom in
+              let bound =
+                if IntLit.leq IntLit.minus_one n then IntLit.minus_one else widening_bottom in
               let a' = Prop.mk_inequality (Sil.BinOp(Sil.Lt, Sil.exp_int bound, e)) in
               Some a'
         end in
   let is_stronger_le e n a =
     match Prop.atom_exp_le_const a with
     | None -> false
-    | Some (e', n') -> Sil.exp_equal e e' && Sil.Int.lt n' n in
+    | Some (e', n') -> Sil.exp_equal e e' && IntLit.lt n' n in
   let is_stronger_lt n e a =
     match Prop.atom_const_lt_exp a with
     | None -> false
-    | Some (n', e') -> Sil.exp_equal e e' && Sil.Int.lt n n' in
+    | Some (n', e') -> Sil.exp_equal e e' && IntLit.lt n n' in
   let join_atom_check_pre p a =
     (* check for atoms in pre mode: fail if the negation is implied by the other side *)
     let not_a = Prop.atom_negate a in
diff --git a/infer/src/backend/dotty.ml b/infer/src/backend/dotty.ml
index af548c053..cd15eebb6 100644
--- a/infer/src/backend/dotty.ml
+++ b/infer/src/backend/dotty.ml
@@ -327,7 +327,8 @@ let rec dotty_mk_node pe sigma =
 
 let set_exps_neq_zero pi =
   let f = function
-    | Sil.Aneq (e, Sil.Const (Sil.Cint i)) when Sil.Int.iszero i -> exps_neq_zero := e :: !exps_neq_zero
+    | Sil.Aneq (e, Sil.Const (Sil.Cint i)) when IntLit.iszero i ->
+        exps_neq_zero := e :: !exps_neq_zero
     | _ -> () in
   exps_neq_zero := [];
   IList.iter f pi
diff --git a/infer/src/backend/errdesc.ml b/infer/src/backend/errdesc.ml
index 4e8b05aab..8ee289d81 100644
--- a/infer/src/backend/errdesc.ml
+++ b/infer/src/backend/errdesc.ml
@@ -175,7 +175,7 @@ let rec find_boolean_assignment node pvar true_branch : Cfg.Node.t option =
   let find_instr n =
     let filter = function
       | Sil.Set (Sil.Lvar _pvar, _, Sil.Const (Sil.Cint i), _) when Pvar.equal pvar _pvar ->
-          Sil.Int.iszero i <> true_branch
+          IntLit.iszero i <> true_branch
       | _ -> false in
     IList.exists filter (Cfg.Node.get_instrs n) in
   match Cfg.Node.get_preds node with
diff --git a/infer/src/backend/errdesc.mli b/infer/src/backend/errdesc.mli
index 164d83485..98fbc95d6 100644
--- a/infer/src/backend/errdesc.mli
+++ b/infer/src/backend/errdesc.mli
@@ -90,7 +90,7 @@ val explain_condition_is_assignment : Location.t -> Localise.error_desc
 
 (** explain a condition which is always true or false *)
 val explain_condition_always_true_false :
-  Sil.Int.t -> Sil.exp -> Cfg.Node.t -> Location.t -> Localise.error_desc
+  IntLit.t -> Sil.exp -> Cfg.Node.t -> Location.t -> Localise.error_desc
 
 (** explain the escape of a stack variable address from its scope *)
 val explain_stack_variable_address_escape :
diff --git a/infer/src/backend/localise.ml b/infer/src/backend/localise.ml
index 0b7a7b53f..a20d7321c 100644
--- a/infer/src/backend/localise.ml
+++ b/infer/src/backend/localise.ml
@@ -372,13 +372,13 @@ let deref_str_array_bound size_opt index_opt =
   let tags = Tags.create () in
   let size_str_opt = match size_opt with
     | Some n ->
-        let n_str = Sil.Int.to_string n in
+        let n_str = IntLit.to_string n in
         Tags.add tags Tags.array_size n_str;
         Some ("of size " ^ n_str)
     | None -> None in
   let index_str = match index_opt with
     | Some n ->
-        let n_str = Sil.Int.to_string n in
+        let n_str = IntLit.to_string n in
         Tags.add tags Tags.array_index n_str;
         "index " ^ n_str
     | None -> "an index" in
@@ -594,7 +594,7 @@ let desc_condition_always_true_false i cond_str_opt loc =
   let value = match cond_str_opt with
     | None -> ""
     | Some s -> s in
-  let tt_ff = if Sil.Int.iszero i then "false" else "true" in
+  let tt_ff = if IntLit.iszero i then "false" else "true" in
   Tags.add tags Tags.value value;
   let description = Format.sprintf
       "Boolean condition %s is always %s %s"
diff --git a/infer/src/backend/localise.mli b/infer/src/backend/localise.mli
index 2b57e6dd0..7ff4f3677 100644
--- a/infer/src/backend/localise.mli
+++ b/infer/src/backend/localise.mli
@@ -156,7 +156,7 @@ val deref_str_freed : Sil.res_action -> deref_str
 val deref_str_dangling : Sil.dangling_kind option -> deref_str
 
 (** dereference strings for an array out of bound access *)
-val deref_str_array_bound : Sil.Int.t option -> Sil.Int.t option -> deref_str
+val deref_str_array_bound : IntLit.t option -> IntLit.t option -> deref_str
 
 (** dereference strings for an uninitialized access whose lhs has the given attribute *)
 val deref_str_uninitialized : Sil.attribute option -> deref_str
@@ -195,7 +195,7 @@ val desc_comparing_floats_for_equality : Location.t -> error_desc
 
 val desc_condition_is_assignment : Location.t -> error_desc
 
-val desc_condition_always_true_false : Sil.Int.t -> string option -> Location.t -> error_desc
+val desc_condition_always_true_false : IntLit.t -> string option -> Location.t -> error_desc
 
 val desc_deallocate_stack_variable : string -> Procname.t -> Location.t -> error_desc
 
diff --git a/infer/src/backend/modelBuiltins.ml b/infer/src/backend/modelBuiltins.ml
index f53fbd29f..3481f5158 100644
--- a/infer/src/backend/modelBuiltins.ml
+++ b/infer/src/backend/modelBuiltins.ml
@@ -492,7 +492,7 @@ let execute___objc_counter_update
    removed from the list of args. *)
 let get_suppress_npe_flag args =
   match args with
-  | (Sil.Const (Sil.Cint i), Sil.Tint Sil.IBool):: args' when Sil.Int.isone i ->
+  | (Sil.Const (Sil.Cint i), Sil.Tint Sil.IBool):: args' when IntLit.isone i ->
       false, args' (* this is a CFRelease/CFRetain *)
   | _ -> true, args
 
@@ -504,7 +504,7 @@ let execute___objc_retain_impl
   | [(lexp, _)] ->
       let prop = return_result lexp prop_ ret_ids in
       execute___objc_counter_update
-        ~mask_errors (Sil.PlusA) (Sil.Int.one)
+        ~mask_errors (Sil.PlusA) (IntLit.one)
         { builtin_args with Builtin.prop_ = prop; args = args'; }
   | _ -> raise (Exceptions.Wrong_argument_number __POS__)
 
@@ -524,7 +524,7 @@ let execute___objc_release_impl
   : Builtin.ret_typ =
   let mask_errors, args' = get_suppress_npe_flag args in
   execute___objc_counter_update
-    ~mask_errors Sil.MinusA Sil.Int.one
+    ~mask_errors Sil.MinusA IntLit.one
     { builtin_args with Builtin.args = args'; }
 
 let execute___objc_release builtin_args
@@ -906,7 +906,7 @@ let execute___split_get_nth { Builtin.pdesc; prop_; path; ret_ids; args; }
       let n_lexp3, prop = check_arith_norm_exp pname lexp3 prop___ in
       (match n_lexp1, n_lexp2, n_lexp3 with
        | Sil.Const (Sil.Cstr str1), Sil.Const (Sil.Cstr str2), Sil.Const (Sil.Cint n_sil) ->
-           (let n = Sil.Int.to_int n_sil in
+           (let n = IntLit.to_int n_sil in
             try
               let parts = Str.split (Str.regexp_string str2) str1 in
               let n_part = IList.nth parts n in
diff --git a/infer/src/backend/prop.ml b/infer/src/backend/prop.ml
index e2893645e..a1f483b30 100644
--- a/infer/src/backend/prop.ml
+++ b/infer/src/backend/prop.ml
@@ -426,21 +426,21 @@ let sub_normalize sub =
   let sub' = Sil.sub_filter_pair f sub in
   if Sil.sub_equal sub sub' then sub else sub'
 
-let (--) = Sil.Int.sub
-let (++) = Sil.Int.add
+let (--) = IntLit.sub
+let (++) = IntLit.add
 
 let iszero_int_float = function
-  | Sil.Cint i -> Sil.Int.iszero i
+  | Sil.Cint i -> IntLit.iszero i
   | Sil.Cfloat 0.0 -> true
   | _ -> false
 
 let isone_int_float = function
-  | Sil.Cint i -> Sil.Int.isone i
+  | Sil.Cint i -> IntLit.isone i
   | Sil.Cfloat 1.0 -> true
   | _ -> false
 
 let isminusone_int_float = function
-  | Sil.Cint i -> Sil.Int.isminusone i
+  | Sil.Cint i -> IntLit.isminusone i
   | Sil.Cfloat (-1.0) -> true
   | _ -> false
 
@@ -469,7 +469,7 @@ let sym_eval abs e =
     | Sil.UnOp (Sil.LNot, e1, topt) ->
         begin
           match eval e1 with
-          | Sil.Const (Sil.Cint i) when Sil.Int.iszero i ->
+          | Sil.Const (Sil.Cint i) when IntLit.iszero i ->
               Sil.exp_one
           | Sil.Const (Sil.Cint _) ->
               Sil.exp_zero
@@ -484,7 +484,7 @@ let sym_eval abs e =
           | Sil.UnOp (Sil.Neg, e2', _) ->
               e2'
           | Sil.Const (Sil.Cint i) ->
-              Sil.exp_int (Sil.Int.neg i)
+              Sil.exp_int (IntLit.neg i)
           | Sil.Const (Sil.Cfloat v) ->
               Sil.exp_float (-. v)
           | Sil.Var id ->
@@ -498,7 +498,7 @@ let sym_eval abs e =
           | Sil.UnOp(Sil.BNot, e2', _) ->
               e2'
           | Sil.Const (Sil.Cint i) ->
-              Sil.exp_int (Sil.Int.lognot i)
+              Sil.exp_int (IntLit.lognot i)
           | e1' ->
               if abs then Sil.exp_get_undefined false else Sil.UnOp (Sil.BNot, e1', topt)
         end
@@ -506,7 +506,7 @@ let sym_eval abs e =
         begin
           match eval e1, eval e2 with
           | Sil.Const (Sil.Cint n), Sil.Const (Sil.Cint m) ->
-              Sil.exp_bool (Sil.Int.leq n m)
+              Sil.exp_bool (IntLit.leq n m)
           | Sil.Const (Sil.Cfloat v), Sil.Const (Sil.Cfloat w) ->
               Sil.exp_bool (v <= w)
           | Sil.BinOp (Sil.PlusA, e3, Sil.Const (Sil.Cint n)), Sil.Const (Sil.Cint m) ->
@@ -518,14 +518,14 @@ let sym_eval abs e =
         begin
           match eval e1, eval e2 with
           | Sil.Const (Sil.Cint n), Sil.Const (Sil.Cint m) ->
-              Sil.exp_bool (Sil.Int.lt n m)
+              Sil.exp_bool (IntLit.lt n m)
           | Sil.Const (Sil.Cfloat v), Sil.Const (Sil.Cfloat w) ->
               Sil.exp_bool (v < w)
           | Sil.Const (Sil.Cint n), Sil.BinOp (Sil.MinusA, f1, f2) ->
               Sil.BinOp
-                (Sil.Le, Sil.BinOp (Sil.MinusA, f2, f1), Sil.exp_int (Sil.Int.minus_one -- n))
+                (Sil.Le, Sil.BinOp (Sil.MinusA, f2, f1), Sil.exp_int (IntLit.minus_one -- n))
           | Sil.BinOp(Sil.MinusA, f1 , f2), Sil.Const(Sil.Cint n) ->
-              Sil.exp_le (Sil.BinOp(Sil.MinusA, f1 , f2)) (Sil.exp_int (n -- Sil.Int.one))
+              Sil.exp_le (Sil.BinOp(Sil.MinusA, f1 , f2)) (Sil.exp_int (n -- IntLit.one))
           | Sil.BinOp (Sil.PlusA, e3, Sil.Const (Sil.Cint n)), Sil.Const (Sil.Cint m) ->
               Sil.BinOp (Sil.Lt, e3, Sil.exp_int (m -- n))
           | e1', e2' ->
@@ -539,7 +539,7 @@ let sym_eval abs e =
         begin
           match eval e1, eval e2 with
           | Sil.Const (Sil.Cint n), Sil.Const (Sil.Cint m) ->
-              Sil.exp_bool (Sil.Int.eq n m)
+              Sil.exp_bool (IntLit.eq n m)
           | Sil.Const (Sil.Cfloat v), Sil.Const (Sil.Cfloat w) ->
               Sil.exp_bool (v = w)
           | e1', e2' ->
@@ -549,7 +549,7 @@ let sym_eval abs e =
         begin
           match eval e1, eval e2 with
           | Sil.Const (Sil.Cint n), Sil.Const (Sil.Cint m) ->
-              Sil.exp_bool (Sil.Int.neq n m)
+              Sil.exp_bool (IntLit.neq n m)
           | Sil.Const (Sil.Cfloat v), Sil.Const (Sil.Cfloat w) ->
               Sil.exp_bool (v <> w)
           | e1', e2' ->
@@ -559,11 +559,11 @@ let sym_eval abs e =
         let e1' = eval e1 in
         let e2' = eval e2 in
         begin match e1', e2' with
-          | Sil.Const (Sil.Cint i), _ when Sil.Int.iszero i ->
+          | Sil.Const (Sil.Cint i), _ when IntLit.iszero i ->
               e1'
           | Sil.Const (Sil.Cint _), _ ->
               e2'
-          | _, Sil.Const (Sil.Cint i) when Sil.Int.iszero i ->
+          | _, Sil.Const (Sil.Cint i) when IntLit.iszero i ->
               e2'
           | _, Sil.Const (Sil.Cint _) ->
               e1'
@@ -575,11 +575,11 @@ let sym_eval abs e =
         let e2' = eval e2 in
         begin
           match e1', e2' with
-          | Sil.Const (Sil.Cint i), _ when Sil.Int.iszero i ->
+          | Sil.Const (Sil.Cint i), _ when IntLit.iszero i ->
               e2'
           | Sil.Const (Sil.Cint _), _ ->
               e1'
-          | _, Sil.Const (Sil.Cint i) when Sil.Int.iszero i ->
+          | _, Sil.Const (Sil.Cint i) when IntLit.iszero i ->
               e1'
           | _, Sil.Const (Sil.Cint _) ->
               e2'
@@ -601,12 +601,12 @@ let sym_eval abs e =
         let isPlusA = oplus = Sil.PlusA in
         let ominus = if isPlusA then Sil.MinusA else Sil.MinusPI in
         let (+++) x y = match x, y with
-          | _, Sil.Const (Sil.Cint i) when Sil.Int.iszero i -> x
-          | Sil.Const (Sil.Cint i), Sil.Const (Sil.Cint j) -> Sil.Const (Sil.Cint (Sil.Int.add i j))
+          | _, Sil.Const (Sil.Cint i) when IntLit.iszero i -> x
+          | Sil.Const (Sil.Cint i), Sil.Const (Sil.Cint j) -> Sil.Const (Sil.Cint (IntLit.add i j))
           | _ -> Sil.BinOp (oplus, x, y) in
         let (---) x y = match x, y with
-          | _, Sil.Const (Sil.Cint i) when Sil.Int.iszero i -> x
-          | Sil.Const (Sil.Cint i), Sil.Const (Sil.Cint j) -> Sil.Const (Sil.Cint (Sil.Int.sub i j))
+          | _, Sil.Const (Sil.Cint i) when IntLit.iszero i -> x
+          | Sil.Const (Sil.Cint i), Sil.Const (Sil.Cint j) -> Sil.Const (Sil.Cint (IntLit.sub i j))
           | _ -> Sil.BinOp (ominus, x, y) in
         (* test if the extensible array at the end of [typ] has elements of type [elt] *)
         let extensible_array_element_typ_equal elt typ =
@@ -674,7 +674,7 @@ let sym_eval abs e =
           | _, Sil.UnOp (Sil.Neg, f2, _) ->
               eval (e1 +++ f2)
           | _ , Sil.Const(Sil.Cint n) ->
-              eval (e1' +++ (Sil.exp_int (Sil.Int.neg n)))
+              eval (e1' +++ (Sil.exp_int (IntLit.neg n)))
           | Sil.Const _, _ ->
               e1' --- e2'
           | Sil.Var _, Sil.Var _ ->
@@ -703,7 +703,7 @@ let sym_eval abs e =
           | _, Sil.Const c when isminusone_int_float c ->
               eval (Sil.UnOp (Sil.Neg, e1', None))
           | Sil.Const (Sil.Cint n), Sil.Const (Sil.Cint m) ->
-              Sil.exp_int (Sil.Int.mul n m)
+              Sil.exp_int (IntLit.mul n m)
           | Sil.Const (Sil.Cfloat v), Sil.Const (Sil.Cfloat w) ->
               Sil.exp_float (v *. w)
           | Sil.Var _, Sil.Var _ ->
@@ -726,7 +726,7 @@ let sym_eval abs e =
           | _, Sil.Const c when isone_int_float c ->
               e1'
           | Sil.Const (Sil.Cint n), Sil.Const (Sil.Cint m) ->
-              Sil.exp_int (Sil.Int.div n m)
+              Sil.exp_int (IntLit.div n m)
           | Sil.Const (Sil.Cfloat v), Sil.Const (Sil.Cfloat w) ->
               Sil.exp_float (v /.w)
           | Sil.Sizeof (Sil.Tarray (elt, _), Some len, _), Sil.Sizeof (elt2, None, _)
@@ -745,14 +745,14 @@ let sym_eval abs e =
         let e2' = eval e2 in
         begin
           match e1', e2' with
-          | _, Sil.Const (Sil.Cint i) when Sil.Int.iszero i ->
+          | _, Sil.Const (Sil.Cint i) when IntLit.iszero i ->
               Sil.exp_get_undefined false
-          | Sil.Const (Sil.Cint i), _ when Sil.Int.iszero i ->
+          | Sil.Const (Sil.Cint i), _ when IntLit.iszero i ->
               e1'
-          | _, Sil.Const (Sil.Cint i) when Sil.Int.isone i ->
+          | _, Sil.Const (Sil.Cint i) when IntLit.isone i ->
               Sil.exp_zero
           | Sil.Const (Sil.Cint n), Sil.Const (Sil.Cint m) ->
-              Sil.exp_int (Sil.Int.rem n m)
+              Sil.exp_int (IntLit.rem n m)
           | _ ->
               if abs then Sil.exp_get_undefined false else Sil.BinOp (Sil.Mod, e1', e2')
         end
@@ -764,12 +764,12 @@ let sym_eval abs e =
         let e1' = eval e1 in
         let e2' = eval e2 in
         begin match e1', e2' with
-          | Sil.Const (Sil.Cint i), _ when Sil.Int.iszero i ->
+          | Sil.Const (Sil.Cint i), _ when IntLit.iszero i ->
               e1'
-          | _, Sil.Const (Sil.Cint i) when Sil.Int.iszero i ->
+          | _, Sil.Const (Sil.Cint i) when IntLit.iszero i ->
               e2'
           | Sil.Const (Sil.Cint i1), Sil.Const(Sil.Cint i2) ->
-              Sil.exp_int (Sil.Int.logand i1 i2)
+              Sil.exp_int (IntLit.logand i1 i2)
           | _ ->
               if abs then Sil.exp_get_undefined false else Sil.BinOp (Sil.BAnd, e1', e2')
         end
@@ -777,12 +777,12 @@ let sym_eval abs e =
         let e1' = eval e1 in
         let e2' = eval e2 in
         begin match e1', e2' with
-          | Sil.Const (Sil.Cint i), _ when Sil.Int.iszero i ->
+          | Sil.Const (Sil.Cint i), _ when IntLit.iszero i ->
               e2'
-          | _, Sil.Const (Sil.Cint i) when Sil.Int.iszero i ->
+          | _, Sil.Const (Sil.Cint i) when IntLit.iszero i ->
               e1'
           | Sil.Const (Sil.Cint i1), Sil.Const(Sil.Cint i2) ->
-              Sil.exp_int (Sil.Int.logor i1 i2)
+              Sil.exp_int (IntLit.logor i1 i2)
           | _ ->
               if abs then Sil.exp_get_undefined false else Sil.BinOp (Sil.BOr, e1', e2')
         end
@@ -790,12 +790,12 @@ let sym_eval abs e =
         let e1' = eval e1 in
         let e2' = eval e2 in
         begin match e1', e2' with
-          | Sil.Const (Sil.Cint i), _ when Sil.Int.iszero i ->
+          | Sil.Const (Sil.Cint i), _ when IntLit.iszero i ->
               e2'
-          | _, Sil.Const (Sil.Cint i) when Sil.Int.iszero i ->
+          | _, Sil.Const (Sil.Cint i) when IntLit.iszero i ->
               e1'
           | Sil.Const (Sil.Cint i1), Sil.Const(Sil.Cint i2) ->
-              Sil.exp_int (Sil.Int.logxor i1 i2)
+              Sil.exp_int (IntLit.logxor i1 i2)
           | _ ->
               if abs then Sil.exp_get_undefined false else Sil.BinOp (Sil.BXor, e1', e2')
         end
@@ -806,7 +806,7 @@ let sym_eval abs e =
           match e2' with
           | Sil.Const (Sil.Cptr_to_fld (fn, typ)) ->
               eval (Sil.Lfield(e1', fn, typ))
-          | Sil.Const (Sil.Cint i) when Sil.Int.iszero i ->
+          | Sil.Const (Sil.Cint i) when IntLit.iszero i ->
               Sil.exp_zero (* cause a NULL dereference *)
           | _ -> Sil.BinOp (Sil.PtrFld, e1', e2')
         end
@@ -852,21 +852,21 @@ let exp_normalize_noabs sub exp =
 
 (** Return [true] if the atom is an inequality *)
 let atom_is_inequality = function
-  | Sil.Aeq (Sil.BinOp (Sil.Le, _, _), Sil.Const (Sil.Cint i)) when Sil.Int.isone i -> true
-  | Sil.Aeq (Sil.BinOp (Sil.Lt, _, _), Sil.Const (Sil.Cint i)) when Sil.Int.isone i -> true
+  | Sil.Aeq (Sil.BinOp (Sil.Le, _, _), Sil.Const (Sil.Cint i)) when IntLit.isone i -> true
+  | Sil.Aeq (Sil.BinOp (Sil.Lt, _, _), Sil.Const (Sil.Cint i)) when IntLit.isone i -> true
   | _ -> false
 
 (** If the atom is [e<=n] return [e,n] *)
 let atom_exp_le_const = function
   | Sil.Aeq(Sil.BinOp (Sil.Le, e1, Sil.Const (Sil.Cint n)), Sil.Const (Sil.Cint i))
-    when Sil.Int.isone i ->
+    when IntLit.isone i ->
       Some (e1, n)
   | _ -> None
 
 (** If the atom is [n<e] return [n,e] *)
 let atom_const_lt_exp = function
   | Sil.Aeq(Sil.BinOp (Sil.Lt, Sil.Const (Sil.Cint n), e1), Sil.Const (Sil.Cint i))
-    when Sil.Int.isone i ->
+    when IntLit.isone i ->
       Some (n, e1)
   | _ -> None
 
@@ -890,12 +890,12 @@ let mk_inequality e =
            let new_e = Sil.BinOp (Sil.Le, base', new_offset) in
            Sil.Aeq (new_e, Sil.exp_one)
        | Sil.BinOp(Sil.MinusA, Sil.Const (Sil.Cint n'), base') ->
-           let new_offset = Sil.exp_int (n' -- n -- Sil.Int.one) in
+           let new_offset = Sil.exp_int (n' -- n -- IntLit.one) in
            let new_e = Sil.BinOp (Sil.Lt, new_offset, base') in
            Sil.Aeq (new_e, Sil.exp_one)
        | Sil.UnOp(Sil.Neg, new_base, _) ->
            (* In this case, base = -new_base. Construct -n-1 < new_base. *)
-           let new_offset = Sil.exp_int (Sil.Int.zero -- n -- Sil.Int.one) in
+           let new_offset = Sil.exp_int (IntLit.zero -- n -- IntLit.one) in
            let new_e = Sil.BinOp (Sil.Lt, new_offset, new_base) in
            Sil.Aeq (new_e, Sil.exp_one)
        | _ -> Sil.Aeq (e, Sil.exp_one))
@@ -916,12 +916,12 @@ let mk_inequality e =
            let new_e = Sil.BinOp (Sil.Lt, new_offset, base') in
            Sil.Aeq (new_e, Sil.exp_one)
        | Sil.BinOp(Sil.MinusA, Sil.Const (Sil.Cint n'), base') ->
-           let new_offset = Sil.exp_int (n' -- n -- Sil.Int.one) in
+           let new_offset = Sil.exp_int (n' -- n -- IntLit.one) in
            let new_e = Sil.BinOp (Sil.Le, base', new_offset) in
            Sil.Aeq (new_e, Sil.exp_one)
        | Sil.UnOp(Sil.Neg, new_base, _) ->
            (* In this case, base = -new_base. Construct new_base <= -n-1 *)
-           let new_offset = Sil.exp_int (Sil.Int.zero -- n -- Sil.Int.one) in
+           let new_offset = Sil.exp_int (IntLit.zero -- n -- IntLit.one) in
            let new_e = Sil.BinOp (Sil.Le, new_base, new_offset) in
            Sil.Aeq (new_e, Sil.exp_one)
        | _ -> Sil.Aeq (e, Sil.exp_one))
@@ -946,8 +946,8 @@ let inequality_normalize a =
         (pos1@neg2, neg1@pos2, n1 -- n2)
     | Sil.UnOp(Sil.Neg, e1, _) ->
         let pos1, neg1, n1 = exp_to_posnegoff e1 in
-        (neg1, pos1, Sil.Int.zero -- n1)
-    | _ -> [e],[], Sil.Int.zero in
+        (neg1, pos1, IntLit.zero -- n1)
+    | _ -> [e],[], IntLit.zero in
   (** sort and filter out expressions appearing in both the positive and negative part *)
   let normalize_posnegoff (pos, neg, off) =
     let pos' = IList.sort Sil.exp_compare pos in
@@ -969,13 +969,13 @@ let inequality_normalize a =
   let norm_from_exp e =
     match normalize_posnegoff (exp_to_posnegoff e) with
     | [],[], n -> Sil.BinOp(Sil.Le, Sil.exp_int n, Sil.exp_zero)
-    | [], neg, n -> Sil.BinOp(Sil.Lt, Sil.exp_int (n -- Sil.Int.one), exp_list_to_sum neg)
-    | pos, [], n -> Sil.BinOp(Sil.Le, exp_list_to_sum pos, Sil.exp_int (Sil.Int.zero -- n))
+    | [], neg, n -> Sil.BinOp(Sil.Lt, Sil.exp_int (n -- IntLit.one), exp_list_to_sum neg)
+    | pos, [], n -> Sil.BinOp(Sil.Le, exp_list_to_sum pos, Sil.exp_int (IntLit.zero -- n))
     | pos, neg, n ->
         let lhs_e = Sil.BinOp(Sil.MinusA, exp_list_to_sum pos, exp_list_to_sum neg) in
-        Sil.BinOp(Sil.Le, lhs_e, Sil.exp_int (Sil.Int.zero -- n)) in
+        Sil.BinOp(Sil.Le, lhs_e, Sil.exp_int (IntLit.zero -- n)) in
   let ineq = match a with
-    | Sil.Aeq (ineq, Sil.Const (Sil.Cint i)) when Sil.Int.isone i ->
+    | Sil.Aeq (ineq, Sil.Const (Sil.Cint i)) when IntLit.isone i ->
         ineq
     | _ -> assert false in
   match ineq with
@@ -1018,7 +1018,7 @@ let atom_normalize sub a0 =
   let handle_unary_negation e1 e2 =
     match e1, e2 with
     | Sil.UnOp (Sil.LNot, e1', _), Sil.Const (Sil.Cint i)
-    | Sil.Const (Sil.Cint i), Sil.UnOp (Sil.LNot, e1', _) when Sil.Int.iszero i ->
+    | Sil.Const (Sil.Cint i), Sil.UnOp (Sil.LNot, e1', _) when IntLit.iszero i ->
         (e1', Sil.exp_zero, true)
     | _ -> (e1, e2, false) in
   let handle_boolean_operation from_equality e1 e2 =
@@ -1042,9 +1042,9 @@ let atom_normalize sub a0 =
 
 (** Negate an atom *)
 let atom_negate = function
-  | Sil.Aeq (Sil.BinOp (Sil.Le, e1, e2), Sil.Const (Sil.Cint i)) when Sil.Int.isone i ->
+  | Sil.Aeq (Sil.BinOp (Sil.Le, e1, e2), Sil.Const (Sil.Cint i)) when IntLit.isone i ->
       mk_inequality (Sil.exp_lt e2 e1)
-  | Sil.Aeq (Sil.BinOp (Sil.Lt, e1, e2), Sil.Const (Sil.Cint i)) when Sil.Int.isone i ->
+  | Sil.Aeq (Sil.BinOp (Sil.Lt, e1, e2), Sil.Const (Sil.Cint i)) when IntLit.isone i ->
       mk_inequality (Sil.exp_le e2 e1)
   | Sil.Aeq (e1, e2) -> Sil.Aneq (e1, e2)
   | Sil.Aneq (e1, e2) -> Sil.Aeq (e1, e2)
@@ -1217,7 +1217,7 @@ let pi_tighten_ineq pi =
       | _ -> acc in
     IList.fold_left get_disequality_info [] nonineq_list in
   let is_neq e n =
-    IList.exists (fun (e', n') -> Sil.exp_equal e e' && Sil.Int.eq n n') diseq_list in
+    IList.exists (fun (e', n') -> Sil.exp_equal e e' && IntLit.eq n n') diseq_list in
   let le_list_tightened =
     let get_le_inequality_info acc a =
       match atom_exp_le_const a with
@@ -1226,7 +1226,7 @@ let pi_tighten_ineq pi =
     let rec le_tighten le_list_done = function
       | [] -> IList.rev le_list_done
       | (e, n):: le_list_todo -> (* e <= n *)
-          if is_neq e n then le_tighten le_list_done ((e, n -- Sil.Int.one):: le_list_todo)
+          if is_neq e n then le_tighten le_list_done ((e, n -- IntLit.one):: le_list_todo)
           else le_tighten ((e, n):: le_list_done) (le_list_todo) in
     let le_list = IList.rev (IList.fold_left get_le_inequality_info [] ineq_list) in
     le_tighten [] le_list in
@@ -1238,8 +1238,8 @@ let pi_tighten_ineq pi =
     let rec lt_tighten lt_list_done = function
       | [] -> IList.rev lt_list_done
       | (n, e):: lt_list_todo -> (* n < e *)
-          let n_plus_one = n ++ Sil.Int.one in
-          if is_neq e n_plus_one then lt_tighten lt_list_done ((n ++ Sil.Int.one, e):: lt_list_todo)
+          let n_plus_one = n ++ IntLit.one in
+          if is_neq e n_plus_one then lt_tighten lt_list_done ((n ++ IntLit.one, e):: lt_list_todo)
           else lt_tighten ((n, e):: lt_list_done) (lt_list_todo) in
     let lt_list = IList.rev (IList.fold_left get_lt_inequality_info [] ineq_list) in
     lt_tighten [] lt_list in
@@ -1259,10 +1259,10 @@ let pi_tighten_ineq pi =
         | Sil.Aneq(Sil.Const (Sil.Cint n), e)
         | Sil.Aneq(e, Sil.Const (Sil.Cint n)) ->
             (not (IList.exists
-                    (fun (e', n') -> Sil.exp_equal e e' && Sil.Int.lt n' n)
+                    (fun (e', n') -> Sil.exp_equal e e' && IntLit.lt n' n)
                     le_list_tightened)) &&
             (not (IList.exists
-                    (fun (n', e') -> Sil.exp_equal e e' && Sil.Int.leq n n')
+                    (fun (n', e') -> Sil.exp_equal e e' && IntLit.leq n n')
                     lt_list_tightened))
         | _ -> true)
       nonineq_list in
@@ -1272,13 +1272,13 @@ let pi_tighten_ineq pi =
 let rec pi_sorted_remove_redundant = function
   | (Sil.Aeq(Sil.BinOp (Sil.Le, e1, Sil.Const (Sil.Cint n1)), Sil.Const (Sil.Cint i1)) as a1) ::
     Sil.Aeq(Sil.BinOp (Sil.Le, e2, Sil.Const (Sil.Cint n2)), Sil.Const (Sil.Cint i2)) :: rest
-    when Sil.Int.isone i1 && Sil.Int.isone i2 && Sil.exp_equal e1 e2 && Sil.Int.lt n1 n2 ->
+    when IntLit.isone i1 && IntLit.isone i2 && Sil.exp_equal e1 e2 && IntLit.lt n1 n2 ->
       (* second inequality redundant *)
       pi_sorted_remove_redundant (a1 :: rest)
   | Sil.Aeq(Sil.BinOp (Sil.Lt, Sil.Const (Sil.Cint n1), e1), Sil.Const (Sil.Cint i1)) ::
     (Sil.Aeq(Sil.BinOp (Sil.Lt, Sil.Const (Sil.Cint n2), e2), Sil.Const (Sil.Cint i2)) as a2) ::
     rest
-    when Sil.Int.isone i1 && Sil.Int.isone i2 && Sil.exp_equal e1 e2 && Sil.Int.lt n1 n2 ->
+    when IntLit.isone i1 && IntLit.isone i2 && Sil.exp_equal e1 e2 && IntLit.lt n1 n2 ->
       (* first inequality redundant *)
       pi_sorted_remove_redundant (a2 :: rest)
   | a1:: a2:: rest ->
@@ -1311,17 +1311,17 @@ let pi_normalize sub sigma pi0 =
       when Sil.exp_equal e1 e2 ->
         Sil.binop_injective op2 &&
         Sil.binop_is_zero_runit op2 &&
-        not (Sil.const_equal (Sil.Cint Sil.Int.zero) c2)
+        not (Sil.const_equal (Sil.Cint IntLit.zero) c2)
     | Sil.BinOp(op1, e1, Sil.Const(c1)), e2
       when Sil.exp_equal e1 e2 ->
         Sil.binop_injective op1 &&
         Sil.binop_is_zero_runit op1 &&
-        not (Sil.const_equal (Sil.Cint Sil.Int.zero) c1)
+        not (Sil.const_equal (Sil.Cint IntLit.zero) c1)
     | _ -> false in
   let filter_useful_atom =
     let unsigned_exps = lazy (sigma_get_unsigned_exps sigma) in
     function
-    | Sil.Aneq ((Sil.Var _) as e, Sil.Const (Sil.Cint n)) when Sil.Int.isnegative n ->
+    | Sil.Aneq ((Sil.Var _) as e, Sil.Const (Sil.Cint n)) when IntLit.isnegative n ->
         not (IList.exists (Sil.exp_equal e) (Lazy.force unsigned_exps))
     | Sil.Aneq(e1, e2) ->
         not (syntactically_different (e1, e2))
@@ -1681,18 +1681,18 @@ let normalize_and_strengthen_atom (p : normal t) (a : Sil.atom) : Sil.atom =
   let a' = atom_normalize p.sub a in
   match a' with
   | Sil.Aeq (Sil.BinOp (Sil.Le, Sil.Var id, Sil.Const (Sil.Cint n)), Sil.Const (Sil.Cint i))
-    when Sil.Int.isone i ->
-      let lower = Sil.exp_int (n -- Sil.Int.one) in
+    when IntLit.isone i ->
+      let lower = Sil.exp_int (n -- IntLit.one) in
       let a_lower = Sil.Aeq (Sil.BinOp (Sil.Lt, lower, Sil.Var id), Sil.exp_one) in
       if not (IList.mem Sil.atom_equal a_lower p.pi) then a'
       else Sil.Aeq (Sil.Var id, Sil.exp_int n)
   | Sil.Aeq (Sil.BinOp (Sil.Lt, Sil.Const (Sil.Cint n), Sil.Var id), Sil.Const (Sil.Cint i))
-    when Sil.Int.isone i ->
-      let upper = Sil.exp_int (n ++ Sil.Int.one) in
+    when IntLit.isone i ->
+      let upper = Sil.exp_int (n ++ IntLit.one) in
       let a_upper = Sil.Aeq (Sil.BinOp (Sil.Le, Sil.Var id, upper), Sil.exp_one) in
       if not (IList.mem Sil.atom_equal a_upper p.pi) then a'
       else Sil.Aeq (Sil.Var id, upper)
-  | Sil.Aeq (Sil.BinOp (Sil.Ne, e1, e2), Sil.Const (Sil.Cint i)) when Sil.Int.isone i ->
+  | Sil.Aeq (Sil.BinOp (Sil.Ne, e1, e2), Sil.Const (Sil.Cint i)) when IntLit.isone i ->
       Sil.Aneq (e1, e2)
   | _ -> a'
 
@@ -2190,7 +2190,7 @@ let compute_reindexing fav_add get_id_offset list =
   let transform x =
     let id, offset = match get_id_offset x with None -> assert false | Some io -> io in
     let base_new = Sil.Var (Ident.create_fresh Ident.kprimed) in
-    let offset_new = Sil.exp_int (Sil.Int.neg offset) in
+    let offset_new = Sil.exp_int (IntLit.neg offset) in
     let exp_new = Sil.BinOp(Sil.PlusA, base_new, offset_new) in
     (id, exp_new) in
   let reindexing = IList.map transform list_passed in
@@ -2227,7 +2227,7 @@ let prop_rename_array_indices prop =
       match e1, e2 with
       | Sil.BinOp(Sil.PlusA, e1', Sil.Const (Sil.Cint n1')),
         Sil.BinOp(Sil.PlusA, e2', Sil.Const (Sil.Cint n2')) ->
-          not (Sil.exp_equal e1' e2' && Sil.Int.lt n1' n2')
+          not (Sil.exp_equal e1' e2' && IntLit.lt n1' n2')
       | _ -> true in
     let rec select_minimal_indices indices_seen = function
       | [] -> IList.rev indices_seen
@@ -2781,8 +2781,8 @@ let trans_land_lor op ((idl1, stml1), e1) ((idl2, stml2), e2) loc =
       let id = Ident.create_fresh Ident.knormal in
       let prune_instr1, prune_res1, prune_instr2, prune_res2 =
         let cond1, cond2, res = match op with
-          | Sil.LAnd -> e1, Sil.UnOp(Sil.LNot, e1, None), Sil.Int.zero
-          | Sil.LOr -> Sil.UnOp(Sil.LNot, e1, None), e1, Sil.Int.one
+          | Sil.LAnd -> e1, Sil.UnOp(Sil.LNot, e1, None), IntLit.zero
+          | Sil.LOr -> Sil.UnOp(Sil.LNot, e1, None), e1, IntLit.one
           | _ -> assert false in
         let cond_res1 = Sil.BinOp(Sil.Eq, Sil.Var id, e2) in
         let cond_res2 = Sil.BinOp(Sil.Eq, Sil.Var id, Sil.exp_int res) in
@@ -2834,7 +2834,7 @@ let find_equal_formal_path e prop =
 (** translate an if-then-else expression *)
 let trans_if_then_else ((idl1, stml1), e1) ((idl2, stml2), e2) ((idl3, stml3), e3) loc =
   match sym_eval false e1 with
-  | Sil.Const (Sil.Cint i) when Sil.Int.iszero i -> (idl1@idl3, stml1@stml3), e3
+  | Sil.Const (Sil.Cint i) when IntLit.iszero i -> (idl1@idl3, stml1@stml3), e3
   | Sil.Const (Sil.Cint _) -> (idl1@idl2, stml1@stml2), e2
   | _ ->
       let e1not = Sil.UnOp(Sil.LNot, e1, None) in
diff --git a/infer/src/backend/prop.mli b/infer/src/backend/prop.mli
index 7cf63b087..75e297790 100644
--- a/infer/src/backend/prop.mli
+++ b/infer/src/backend/prop.mli
@@ -151,10 +151,10 @@ val mk_inequality : Sil.exp -> Sil.atom
 val atom_is_inequality : Sil.atom -> bool
 
 (** If the atom is [e<=n] return [e,n] *)
-val atom_exp_le_const : Sil.atom -> (Sil.exp * Sil.Int.t) option
+val atom_exp_le_const : Sil.atom -> (Sil.exp * IntLit.t) option
 
 (** If the atom is [n<e] return [n,e] *)
-val atom_const_lt_exp : Sil.atom -> (Sil.Int.t * Sil.exp) option
+val atom_const_lt_exp : Sil.atom -> (IntLit.t * Sil.exp) option
 
 (** Negate an atom *)
 val atom_negate : Sil.atom -> Sil.atom
diff --git a/infer/src/backend/prover.ml b/infer/src/backend/prover.ml
index a2ec12868..79864d241 100644
--- a/infer/src/backend/prover.ml
+++ b/infer/src/backend/prover.ml
@@ -20,10 +20,10 @@ let decrease_indent_when_exception thunk =
   with exn when SymOp.exn_not_failure exn -> (L.d_decrease_indent 1; raise exn)
 
 let compute_max_from_nonempty_int_list l =
-  IList.hd (IList.rev (IList.sort Sil.Int.compare_value l))
+  IList.hd (IList.rev (IList.sort IntLit.compare_value l))
 
 let compute_min_from_nonempty_int_list l =
-  IList.hd (IList.sort Sil.Int.compare_value l)
+  IList.hd (IList.sort IntLit.compare_value l)
 
 let exp_pair_compare (e1, e2) (f1, f2) =
   let c1 = Sil.exp_compare e1 f1 in
@@ -47,8 +47,8 @@ let rec is_java_class = function
 
 (** {2 Ordinary Theorem Proving} *)
 
-let (++) = Sil.Int.add
-let (--) = Sil.Int.sub
+let (++) = IntLit.add
+let (--) = IntLit.sub
 
 (** Reasoning about constraints of the form x-y <= n *)
 
@@ -57,31 +57,31 @@ module DiffConstr : sig
   type t
   val to_leq : t -> Sil.exp * Sil.exp
   val to_lt : t -> Sil.exp * Sil.exp
-  val to_triple : t -> Sil.exp * Sil.exp * Sil.Int.t
+  val to_triple : t -> Sil.exp * Sil.exp * IntLit.t
   val from_leq : t list -> Sil.exp * Sil.exp -> t list
   val from_lt : t list -> Sil.exp * Sil.exp -> t list
   val saturate : t list -> bool * t list
 
 end = struct
 
-  type t = Sil.exp * Sil.exp * Sil.Int.t
+  type t = Sil.exp * Sil.exp * IntLit.t
 
   let compare (e1, e2, n) (f1, f2, m) =
     let c1 = exp_pair_compare (e1, e2) (f1, f2) in
-    if c1 <> 0 then c1 else Sil.Int.compare_value n m
+    if c1 <> 0 then c1 else IntLit.compare_value n m
   let equal entry1 entry2 = compare entry1 entry2 = 0
 
   let to_leq (e1, e2, n) =
     Sil.BinOp(Sil.MinusA, e1, e2), Sil.exp_int n
   let to_lt (e1, e2, n) =
-    Sil.exp_int (Sil.Int.zero -- n -- Sil.Int.one), Sil.BinOp(Sil.MinusA, e2, e1)
+    Sil.exp_int (IntLit.zero -- n -- IntLit.one), Sil.BinOp(Sil.MinusA, e2, e1)
   let to_triple entry = entry
 
   let from_leq acc (e1, e2) =
     match e1, e2 with
     | Sil.BinOp(Sil.MinusA, (Sil.Var id11 as e11), (Sil.Var id12 as e12)), Sil.Const (Sil.Cint n)
       when not (Ident.equal id11 id12) ->
-        (match Sil.Int.to_signed n with
+        (match IntLit.to_signed n with
          | None -> acc (* ignore: constraint algorithm only terminates on signed integers *)
          | Some n' ->
              (e11, e12, n') :: acc)
@@ -90,10 +90,10 @@ end = struct
     match e1, e2 with
     | Sil.Const (Sil.Cint n), Sil.BinOp(Sil.MinusA, (Sil.Var id21 as e21), (Sil.Var id22 as e22))
       when not (Ident.equal id21 id22) ->
-        (match Sil.Int.to_signed n with
+        (match IntLit.to_signed n with
          | None -> acc (* ignore: constraint algorithm only terminates on signed integers *)
          | Some n' ->
-             let m = Sil.Int.zero -- n' -- Sil.Int.one in
+             let m = IntLit.zero -- n' -- IntLit.one in
              (e22, e21, m) :: acc)
     | _ -> acc
 
@@ -102,7 +102,7 @@ end = struct
     | (f1, f2, m):: rest ->
         let equal_e2_f1 = Sil.exp_equal e2 f1 in
         let equal_e1_f2 = Sil.exp_equal e1 f2 in
-        if equal_e2_f1 && equal_e1_f2 && Sil.Int.lt (n ++ m) Sil.Int.zero then
+        if equal_e2_f1 && equal_e1_f2 && IntLit.lt (n ++ m) IntLit.zero then
           true, [] (* constraints are inconsistent *)
         else if equal_e2_f1 && equal_e1_f2 then
           generate constr acc rest
@@ -133,7 +133,7 @@ end = struct
         let e1, e2, n = constr in
         let f1, f2, m = constr' in
         let c1 = exp_pair_compare (e1, e2) (f1, f2) in
-        if c1 = 0 && Sil.Int.lt n m then
+        if c1 = 0 && IntLit.lt n m then
           combine acc_todos acc_seen constraints_new rest'
         else if c1 = 0 then
           combine acc_todos acc_seen rest constraints_old
@@ -212,11 +212,11 @@ module Inequalities : sig
   (** Check [t |- e1<e2]. Result [false] means "don't know". *)
   val check_lt : t -> Sil.exp -> Sil.exp -> bool
 
-  (** Find a Sil.Int.t n such that [t |- e<=n] if possible. *)
-  val compute_upper_bound : t -> Sil.exp -> Sil.Int.t option
+  (** Find a IntLit.t n such that [t |- e<=n] if possible. *)
+  val compute_upper_bound : t -> Sil.exp -> IntLit.t option
 
-  (** Find a Sil.Int.t n such that [t |- n<e] if possible. *)
-  val compute_lower_bound : t -> Sil.exp -> Sil.Int.t option
+  (** Find a IntLit.t n such that [t |- n<e] if possible. *)
+  val compute_lower_bound : t -> Sil.exp -> IntLit.t option
 
   (** Return [true] if a simple inconsistency is detected *)
   val inconsistent : t -> bool
@@ -265,7 +265,7 @@ end = struct
     let have_same_key leq1 leq2 =
       match leq1, leq2 with
       | (e1, Sil.Const (Sil.Cint n1)), (e2, Sil.Const (Sil.Cint n2)) ->
-          Sil.exp_equal e1 e2 && Sil.Int.leq n1 n2
+          Sil.exp_equal e1 e2 && IntLit.leq n1 n2
       | _, _ -> false in
     remove_redundancy have_same_key [] leqs_sorted
   let lts_sort_then_remove_redundancy lts =
@@ -273,7 +273,7 @@ end = struct
     let have_same_key lt1 lt2 =
       match lt1, lt2 with
       | (Sil.Const (Sil.Cint n1), e1), (Sil.Const (Sil.Cint n2), e2) ->
-          Sil.exp_equal e1 e2 && Sil.Int.geq n1 n2
+          Sil.exp_equal e1 e2 && IntLit.geq n1 n2
       | _, _ -> false in
     remove_redundancy have_same_key [] lts_sorted
 
@@ -289,12 +289,12 @@ end = struct
       let umap_add umap e new_upper =
         try
           let old_upper = Sil.ExpMap.find e umap in
-          if Sil.Int.leq old_upper new_upper then umap else Sil.ExpMap.add e new_upper umap
+          if IntLit.leq old_upper new_upper then umap else Sil.ExpMap.add e new_upper umap
         with Not_found -> Sil.ExpMap.add e new_upper umap in
       let lmap_add lmap e new_lower =
         try
           let old_lower = Sil.ExpMap.find e lmap in
-          if Sil.Int.geq old_lower new_lower then lmap else Sil.ExpMap.add e new_lower lmap
+          if IntLit.geq old_lower new_lower then lmap else Sil.ExpMap.add e new_lower lmap
         with Not_found -> Sil.ExpMap.add e new_lower lmap in
       let rec umap_create_from_leqs umap = function
         | [] -> umap
@@ -325,7 +325,7 @@ end = struct
             try
               let e1, e2, n = DiffConstr.to_triple constr (* e2 - e1 > -n-1 *) in
               let lower1 = Sil.ExpMap.find e1 lmap in
-              let new_lower2 = lower1 -- n -- Sil.Int.one in
+              let new_lower2 = lower1 -- n -- IntLit.one in
               let new_lmap = lmap_add lmap e2 new_lower2 in
               lmap_improve_by_difference_constraints new_lmap constrs_rest
             with Not_found ->
@@ -357,9 +357,9 @@ end = struct
     let process_atom = function
       | Sil.Aneq (e1, e2) -> (* != *)
           neqs := (e1, e2) :: !neqs
-      | Sil.Aeq (Sil.BinOp (Sil.Le, e1, e2), Sil.Const (Sil.Cint i)) when Sil.Int.isone i -> (* <= *)
+      | Sil.Aeq (Sil.BinOp (Sil.Le, e1, e2), Sil.Const (Sil.Cint i)) when IntLit.isone i -> (* <= *)
           leqs := (e1, e2) :: !leqs
-      | Sil.Aeq (Sil.BinOp (Sil.Lt, e1, e2), Sil.Const (Sil.Cint i)) when Sil.Int.isone i -> (* < *)
+      | Sil.Aeq (Sil.BinOp (Sil.Lt, e1, e2), Sil.Const (Sil.Cint i)) when IntLit.isone i -> (* < *)
           lts := (e1, e2) :: !lts
       | Sil.Aeq _ -> () in
     IList.iter process_atom pi;
@@ -414,18 +414,19 @@ end = struct
   let check_le { leqs = leqs; lts = lts; neqs = _ } e1 e2 =
     (* L.d_str "check_le "; Sil.d_exp e1; L.d_str " "; Sil.d_exp e2; L.d_ln (); *)
     match e1, e2 with
-    | Sil.Const (Sil.Cint n1), Sil.Const (Sil.Cint n2) -> Sil.Int.leq n1 n2
+    | Sil.Const (Sil.Cint n1), Sil.Const (Sil.Cint n2) -> IntLit.leq n1 n2
     | Sil.BinOp (Sil.MinusA, Sil.Sizeof (t1, None, _), Sil.Sizeof (t2, None, _)),
       Sil.Const(Sil.Cint n2)
-      when Sil.Int.isminusone n2 && type_size_comparable t1 t2 -> (* [ sizeof(t1) - sizeof(t2) <= -1 ] *)
+      when IntLit.isminusone n2 && type_size_comparable t1 t2 ->
+        (* [ sizeof(t1) - sizeof(t2) <= -1 ] *)
         check_type_size_lt t1 t2
     | e, Sil.Const (Sil.Cint n) -> (* [e <= n' <= n |- e <= n] *)
         IList.exists (function
-            | e', Sil.Const (Sil.Cint n') -> Sil.exp_equal e e' && Sil.Int.leq n' n
+            | e', Sil.Const (Sil.Cint n') -> Sil.exp_equal e e' && IntLit.leq n' n
             | _, _ -> false) leqs
     | Sil.Const (Sil.Cint n), e -> (* [ n-1 <= n' < e |- n <= e] *)
         IList.exists (function
-            | Sil.Const (Sil.Cint n'), e' -> Sil.exp_equal e e' && Sil.Int.leq (n -- Sil.Int.one) n'
+            | Sil.Const (Sil.Cint n'), e' -> Sil.exp_equal e e' && IntLit.leq (n -- IntLit.one) n'
             | _, _ -> false) lts
     | _ -> Sil.exp_equal e1 e2
 
@@ -433,14 +434,14 @@ end = struct
   let check_lt { leqs = leqs; lts = lts; neqs = _ } e1 e2 =
     (* L.d_str "check_lt "; Sil.d_exp e1; L.d_str " "; Sil.d_exp e2; L.d_ln (); *)
     match e1, e2 with
-    | Sil.Const (Sil.Cint n1), Sil.Const (Sil.Cint n2) -> Sil.Int.lt n1 n2
+    | Sil.Const (Sil.Cint n1), Sil.Const (Sil.Cint n2) -> IntLit.lt n1 n2
     | Sil.Const (Sil.Cint n), e -> (* [n <= n' < e  |- n < e] *)
         IList.exists (function
-            | Sil.Const (Sil.Cint n'), e' -> Sil.exp_equal e e' && Sil.Int.leq n n'
+            | Sil.Const (Sil.Cint n'), e' -> Sil.exp_equal e e' && IntLit.leq n n'
             | _, _ -> false) lts
     | e, Sil.Const (Sil.Cint n) -> (* [e <= n' <= n-1 |- e < n] *)
         IList.exists (function
-            | e', Sil.Const (Sil.Cint n') -> Sil.exp_equal e e' && Sil.Int.leq n' (n -- Sil.Int.one)
+            | e', Sil.Const (Sil.Cint n') -> Sil.exp_equal e e' && IntLit.leq n' (n -- IntLit.one)
             | _, _ -> false) leqs
     | _ -> false
 
@@ -449,7 +450,7 @@ end = struct
     let e1, e2 = if Sil.exp_compare _e1 _e2 <= 0 then _e1, _e2 else _e2, _e1 in
     IList.exists (exp_pair_eq (e1, e2)) ineq.neqs || check_lt ineq e1 e2 || check_lt ineq e2 e1
 
-  (** Find a Sil.Int.t n such that [t |- e<=n] if possible. *)
+  (** Find a IntLit.t n such that [t |- e<=n] if possible. *)
   let compute_upper_bound { leqs = leqs; lts = _; neqs = _ } e1 =
     match e1 with
     | Sil.Const (Sil.Cint n1) -> Some n1
@@ -465,11 +466,11 @@ end = struct
         if upper_list == [] then None
         else Some (compute_min_from_nonempty_int_list upper_list)
 
-  (** Find a Sil.Int.t n such that [t |- n < e] if possible. *)
+  (** Find a IntLit.t n such that [t |- n < e] if possible. *)
   let compute_lower_bound { leqs = _; lts = lts; neqs = _ } e1 =
     match e1 with
-    | Sil.Const (Sil.Cint n1) -> Some (n1 -- Sil.Int.one)
-    | Sil.Sizeof _ -> Some Sil.Int.zero
+    | Sil.Const (Sil.Cint n1) -> Some (n1 -- IntLit.one)
+    | Sil.Sizeof _ -> Some IntLit.zero
     | _ ->
         let e_lower_list =
           IList.filter (function
@@ -525,11 +526,11 @@ let check_equal prop e1 e2 =
     match n_e1, n_e2 with
     | Sil.BinOp (Sil.PlusA, e1, Sil.Const (Sil.Cint d)), e2
     | e2, Sil.BinOp (Sil.PlusA, e1, Sil.Const (Sil.Cint d)) ->
-        if Sil.exp_equal e1 e2 then Sil.Int.iszero d
+        if Sil.exp_equal e1 e2 then IntLit.iszero d
         else false
-    | Sil.Const c1, Sil.Lindex(Sil.Const c2, Sil.Const (Sil.Cint i)) when Sil.Int.iszero i ->
+    | Sil.Const c1, Sil.Lindex(Sil.Const c2, Sil.Const (Sil.Cint i)) when IntLit.iszero i ->
         Sil.const_equal c1 c2
-    | Sil.Lindex(Sil.Const c1, Sil.Const (Sil.Cint i)), Sil.Const c2 when Sil.Int.iszero i ->
+    | Sil.Lindex(Sil.Const c1, Sil.Const (Sil.Cint i)), Sil.Const c2 when IntLit.iszero i ->
         Sil.const_equal c1 c2
     | _, _ -> false in
   let check_equal_pi () =
@@ -564,11 +565,11 @@ let get_bounds prop _e =
   let e_norm = Prop.exp_normalize_prop prop _e in
   let e_root, off = match e_norm with
     | Sil.BinOp (Sil.PlusA, e, Sil.Const (Sil.Cint n1)) ->
-        e, Sil.Int.neg n1
+        e, IntLit.neg n1
     | Sil.BinOp (Sil.MinusA, e, Sil.Const (Sil.Cint n1)) ->
         e, n1
     | _ ->
-        e_norm, Sil.Int.zero in
+        e_norm, IntLit.zero in
   let ineq = Inequalities.from_prop prop in
   let upper_opt = Inequalities.compute_upper_bound ineq e_root in
   let lower_opt = Inequalities.compute_lower_bound ineq e_root in
@@ -587,18 +588,18 @@ let check_disequal prop e1 e2 =
     | Sil.Const c1, Sil.Const c2 ->
         (Sil.const_kind_equal c1 c2) && not (Sil.const_equal c1 c2)
     | Sil.Const c1, Sil.Lindex(Sil.Const c2, Sil.Const (Sil.Cint d)) ->
-        if Sil.Int.iszero d
+        if IntLit.iszero d
         then not (Sil.const_equal c1 c2) (* offset=0 is no offset *)
         else Sil.const_equal c1 c2 (* same base, different offsets *)
     | Sil.BinOp (Sil.PlusA, e1, Sil.Const (Sil.Cint d1)), Sil.BinOp (Sil.PlusA, e2, Sil.Const (Sil.Cint d2)) ->
-        if Sil.exp_equal e1 e2 then Sil.Int.neq d1 d2
+        if Sil.exp_equal e1 e2 then IntLit.neq d1 d2
         else false
     | Sil.BinOp (Sil.PlusA, e1, Sil.Const (Sil.Cint d)), e2
     | e2, Sil.BinOp (Sil.PlusA, e1, Sil.Const (Sil.Cint d)) ->
-        if Sil.exp_equal e1 e2 then not (Sil.Int.iszero d)
+        if Sil.exp_equal e1 e2 then not (IntLit.iszero d)
         else false
     | Sil.Lindex(Sil.Const c1, Sil.Const (Sil.Cint d)), Sil.Const c2 ->
-        if Sil.Int.iszero d then not (Sil.const_equal c1 c2) else Sil.const_equal c1 c2
+        if IntLit.iszero d then not (Sil.const_equal c1 c2) else Sil.const_equal c1 c2
     | Sil.Lindex(Sil.Const c1, Sil.Const d1), Sil.Lindex (Sil.Const c2, Sil.Const d2) ->
         Sil.const_equal c1 c2 && not (Sil.const_equal d1 d2)
     | _, _ -> false in
@@ -677,14 +678,14 @@ let check_le_normalized prop e1 e2 =
         then Sil.exp_zero, Sil.exp_zero, n
         else f1, f2, n
     | _ ->
-        e1, e2, Sil.Int.zero in
+        e1, e2, IntLit.zero in
   let ineq = Inequalities.from_prop prop in
   let upper_lower_check () =
     let upperL_opt = Inequalities.compute_upper_bound ineq eL in
     let lowerR_opt = Inequalities.compute_lower_bound ineq eR in
     match upperL_opt, lowerR_opt with
     | None, _ | _, None -> false
-    | Some upper1, Some lower2 -> Sil.Int.leq upper1 (lower2 ++ Sil.Int.one ++ off) in
+    | Some upper1, Some lower2 -> IntLit.leq upper1 (lower2 ++ IntLit.one ++ off) in
   (upper_lower_check ())
   || (Inequalities.check_le ineq e1 e2)
   || (check_equal prop e1 e2)
@@ -698,7 +699,7 @@ let check_lt_normalized prop e1 e2 =
     let lower2_opt = Inequalities.compute_lower_bound ineq e2 in
     match upper1_opt, lower2_opt with
     | None, _ | _, None -> false
-    | Some upper1, Some lower2 -> Sil.Int.leq upper1 lower2 in
+    | Some upper1, Some lower2 -> IntLit.leq upper1 lower2 in
   (upper_lower_check ()) || (Inequalities.check_lt ineq e1 e2)
 
 (** Given an atom and a proposition returns a unique identifier.
@@ -730,9 +731,9 @@ let check_atom prop a0 =
   end;
   match a with
   | Sil.Aeq (Sil.BinOp (Sil.Le, e1, e2), Sil.Const (Sil.Cint i))
-    when Sil.Int.isone i -> check_le_normalized prop e1 e2
+    when IntLit.isone i -> check_le_normalized prop e1 e2
   | Sil.Aeq (Sil.BinOp (Sil.Lt, e1, e2), Sil.Const (Sil.Cint i))
-    when Sil.Int.isone i -> check_lt_normalized prop e1 e2
+    when IntLit.isone i -> check_lt_normalized prop e1 e2
   | Sil.Aeq (e1, e2) -> check_equal prop e1 e2
   | Sil.Aneq (e1, e2) -> check_disequal prop e1 e2
 
@@ -776,7 +777,7 @@ let check_inconsistency_two_hpreds prop =
         if Sil.exp_equal iF e || Sil.exp_equal iB e then true
         else f e (hpred:: sigma_seen) sigma_rest
     | Sil.Hlseg (Sil.Lseg_PE, _, e1, Sil.Const (Sil.Cint i), _) as hpred :: sigma_rest
-      when Sil.Int.iszero i ->
+      when IntLit.iszero i ->
         if Sil.exp_equal e1 e then true
         else f e (hpred:: sigma_seen) sigma_rest
     | Sil.Hlseg (Sil.Lseg_PE, _, e1, e2, _) as hpred :: sigma_rest ->
@@ -789,7 +790,7 @@ let check_inconsistency_two_hpreds prop =
           in f e_new [] sigma_new
         else f e (hpred:: sigma_seen) sigma_rest
     | Sil.Hdllseg (Sil.Lseg_PE, _, e1, _, Sil.Const (Sil.Cint i), _, _) as hpred :: sigma_rest
-      when Sil.Int.iszero i ->
+      when IntLit.iszero i ->
         if Sil.exp_equal e1 e then true
         else f e (hpred:: sigma_seen) sigma_rest
     | Sil.Hdllseg (Sil.Lseg_PE, _, e1, _, e3, _, _) as hpred :: sigma_rest ->
@@ -1947,10 +1948,10 @@ and sigma_imply tenv calc_index_frame calc_missing subs prop1 sigma2 : (subst2 *
          | _ -> None)
     | _ -> None in
   let mk_constant_string_hpred s = (* create an hpred from a constant string *)
-    let len = Sil.Int.of_int (1 + String.length s) in
+    let len = IntLit.of_int (1 + String.length s) in
     let root = Sil.Const (Sil.Cstr s) in
     let sexp =
-      let index = Sil.exp_int (Sil.Int.of_int (String.length s)) in
+      let index = Sil.exp_int (IntLit.of_int (String.length s)) in
       match !Config.curr_language with
       | Config.Clang ->
           Sil.Earray
diff --git a/infer/src/backend/prover.mli b/infer/src/backend/prover.mli
index 919c238f9..8fdd956f4 100644
--- a/infer/src/backend/prover.mli
+++ b/infer/src/backend/prover.mli
@@ -59,7 +59,7 @@ val is_root : Prop.normal Prop.t -> exp -> exp -> offset list option
 val expand_hpred_pointer : bool -> Sil.hpred -> bool * bool * Sil.hpred
 
 (** Get upper and lower bounds of an expression, if any *)
-val get_bounds : Prop.normal Prop.t -> Sil.exp -> Sil.Int.t option * Sil.Int.t option
+val get_bounds : Prop.normal Prop.t -> Sil.exp -> IntLit.t option * IntLit.t option
 
 (** {2 Abduction prover} *)
 
@@ -91,7 +91,7 @@ val find_minimum_pure_cover : (Sil.atom list * 'a) list -> (Sil.atom list * 'a)
 (** {2 Compute various lower or upper bounds} *)
 
 (** Computer an upper bound of an expression *)
-val compute_upper_bound_of_exp : Prop.normal Prop.t -> Sil.exp -> Sil.Int.t option
+val compute_upper_bound_of_exp : Prop.normal Prop.t -> Sil.exp -> IntLit.t option
 
 (** {2 Subtype checking} *)
 
diff --git a/infer/src/backend/rearrange.ml b/infer/src/backend/rearrange.ml
index d518e6500..5a9ed5f0d 100644
--- a/infer/src/backend/rearrange.ml
+++ b/infer/src/backend/rearrange.ml
@@ -301,7 +301,7 @@ and array_case_analysis_index pname tenv orig_prop
     IList.exists (fun (i, _) -> Prover.check_equal Prop.prop_emp index i) array_cont in
   let array_is_full =
     match array_len with
-    | Sil.Const (Sil.Cint n') -> Sil.Int.geq (Sil.Int.of_int (IList.length array_cont)) n'
+    | Sil.Const (Sil.Cint n') -> IntLit.geq (IntLit.of_int (IList.length array_cont)) n'
     | _ -> false in
 
   if index_in_array then
diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml
index 6904c7ec0..7179ad811 100644
--- a/infer/src/backend/symExec.ml
+++ b/infer/src/backend/symExec.ml
@@ -35,7 +35,7 @@ let rec unroll_type tenv typ off =
       end
   | Sil.Tarray (typ', _), Sil.Off_index _ ->
       typ'
-  | _, Sil.Off_index (Sil.Const (Sil.Cint i)) when Sil.Int.iszero i ->
+  | _, Sil.Off_index (Sil.Const (Sil.Cint i)) when IntLit.iszero i ->
       typ
   | _ ->
       L.d_strln ".... Invalid Field Access ....";
@@ -314,7 +314,7 @@ let rec prune ~positive condition prop =
   match condition with
   | Sil.Var _ | Sil.Lvar _ ->
       prune_ne ~positive condition Sil.exp_zero prop
-  | Sil.Const (Sil.Cint i) when Sil.Int.iszero i ->
+  | Sil.Const (Sil.Cint i) when IntLit.iszero i ->
       if positive then Propset.empty else Propset.singleton prop
   | Sil.Const (Sil.Cint _) | Sil.Sizeof _ | Sil.Const (Sil.Cstr _) | Sil.Const (Sil.Cclass _) ->
       if positive then Propset.singleton prop else Propset.empty
@@ -327,12 +327,12 @@ let rec prune ~positive condition prop =
   | Sil.UnOp _ ->
       assert false
   | Sil.BinOp (Sil.Eq, e, Sil.Const (Sil.Cint i))
-  | Sil.BinOp (Sil.Eq, Sil.Const (Sil.Cint i), e) when Sil.Int.iszero i && not (Sil.Int.isnull i) ->
+  | Sil.BinOp (Sil.Eq, Sil.Const (Sil.Cint i), e) when IntLit.iszero i && not (IntLit.isnull i) ->
       prune ~positive:(not positive) e prop
   | Sil.BinOp (Sil.Eq, e1, e2) ->
       prune_ne ~positive:(not positive) e1 e2 prop
   | Sil.BinOp (Sil.Ne, e, Sil.Const (Sil.Cint i))
-  | Sil.BinOp (Sil.Ne, Sil.Const (Sil.Cint i), e) when Sil.Int.iszero i && not (Sil.Int.isnull i) ->
+  | Sil.BinOp (Sil.Ne, Sil.Const (Sil.Cint i), e) when IntLit.iszero i && not (IntLit.isnull i) ->
       prune ~positive e prop
   | Sil.BinOp (Sil.Ne, e1, e2) ->
       prune_ne ~positive e1 e2 prop
@@ -392,20 +392,20 @@ let call_should_be_skipped callee_pname summary =
 (** In case of constant string dereference, return the result immediately *)
 let check_constant_string_dereference lexp =
   let string_lookup s n =
-    let c = try Char.code (String.get s (Sil.Int.to_int n)) with Invalid_argument _ -> 0 in
-    Sil.exp_int (Sil.Int.of_int c) in
+    let c = try Char.code (String.get s (IntLit.to_int n)) with Invalid_argument _ -> 0 in
+    Sil.exp_int (IntLit.of_int c) in
   match lexp with
   | Sil.BinOp(Sil.PlusPI, Sil.Const (Sil.Cstr s), e)
   | Sil.Lindex (Sil.Const (Sil.Cstr s), e) ->
       let value = match e with
         | Sil.Const (Sil.Cint n)
-          when Sil.Int.geq n Sil.Int.zero &&
-               Sil.Int.leq n (Sil.Int.of_int (String.length s)) ->
+          when IntLit.geq n IntLit.zero &&
+               IntLit.leq n (IntLit.of_int (String.length s)) ->
             string_lookup s n
         | _ -> Sil.exp_get_undefined false in
       Some value
   | Sil.Const (Sil.Cstr s) ->
-      Some (string_lookup s Sil.Int.zero)
+      Some (string_lookup s IntLit.zero)
   | _ -> None
 
 (** Normalize an expression and check for arithmetic problems *)
@@ -440,7 +440,7 @@ let check_already_dereferenced pname cond prop =
     | Sil.UnOp(Sil.LNot, e, _) ->
         is_check_zero e
     | Sil.BinOp ((Sil.Eq | Sil.Ne), Sil.Const Sil.Cint i, Sil.Var id)
-    | Sil.BinOp ((Sil.Eq | Sil.Ne), Sil.Var id, Sil.Const Sil.Cint i) when Sil.Int.iszero i ->
+    | Sil.BinOp ((Sil.Eq | Sil.Ne), Sil.Var id, Sil.Const Sil.Cint i) when IntLit.iszero i ->
         Some id
     | _ -> None in
   let dereferenced_line = match is_check_zero cond with
@@ -1027,7 +1027,7 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path
         let report_condition_always_true_false i =
           let skip_loop = match ik with
             | Sil.Ik_while | Sil.Ik_for ->
-                not (Sil.Int.iszero i) (* skip wile(1) and for (;1;) *)
+                not (IntLit.iszero i) (* skip wile(1) and for (;1;) *)
             | Sil.Ik_dowhile ->
                 true (* skip do..while *)
             | Sil.Ik_land_lor ->
@@ -1044,7 +1044,7 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path
             let node = State.get_node () in
             let desc = Errdesc.explain_condition_always_true_false i cond node loc in
             let exn =
-              Exceptions.Condition_always_true_false (desc, not (Sil.Int.iszero i), __POS__) in
+              Exceptions.Condition_always_true_false (desc, not (IntLit.iszero i), __POS__) in
             let pre_opt = State.get_normalized_pre (Abs.abstract_no_symop current_pname) in
             Reporting.log_warning current_pname ~pre: pre_opt exn
         | Sil.BinOp ((Sil.Eq | Sil.Ne), lhs, rhs)
diff --git a/infer/src/backend/tabulation.ml b/infer/src/backend/tabulation.ml
index 52c12a5ac..05b583d1e 100644
--- a/infer/src/backend/tabulation.ml
+++ b/infer/src/backend/tabulation.ml
@@ -722,7 +722,7 @@ let combine
       let id_assigned_to_null id =
         let filter = function
           | Sil.Aeq (Sil.Var id', Sil.Const (Sil.Cint i)) ->
-              Ident.equal id id' && Sil.Int.isnull i
+              Ident.equal id id' && IntLit.isnull i
           | _ -> false in
         IList.exists filter split.missing_pi in
       let f (e, inst_opt) = match e, inst_opt with
diff --git a/infer/src/checkers/checkTraceCallSequence.ml b/infer/src/checkers/checkTraceCallSequence.ml
index dc744a9f1..57c6ea34d 100644
--- a/infer/src/checkers/checkTraceCallSequence.ml
+++ b/infer/src/checkers/checkTraceCallSequence.ml
@@ -259,7 +259,7 @@ module BooleanVars = struct
 
     match normalize_instr instr with
     | Sil.Prune (Sil.BinOp (Sil.Eq, _cond_e, Sil.Const (Sil.Cint i)), _, _, _)
-      when Sil.Int.iszero i ->
+      when IntLit.iszero i ->
         let cond_e = Idenv.expand_expr idenv _cond_e in
         let state' = match exp_boolean_var cond_e with
           | Some name ->
@@ -268,7 +268,7 @@ module BooleanVars = struct
           | None -> state in
         state'
     | Sil.Prune (Sil.BinOp (Sil.Ne, _cond_e, Sil.Const (Sil.Cint i)), _, _, _)
-      when Sil.Int.iszero i ->
+      when IntLit.iszero i ->
         let cond_e = Idenv.expand_expr idenv _cond_e in
         let state' = match exp_boolean_var cond_e with
           | Some name ->
@@ -281,7 +281,7 @@ module BooleanVars = struct
         let state' = match exp_boolean_var e1 with
           | Some name ->
               let b_opt = match e2 with
-                | Sil.Const (Sil.Cint i) -> Some (not (Sil.Int.iszero i))
+                | Sil.Const (Sil.Cint i) -> Some (not (IntLit.iszero i))
                 | _ -> None in
               if verbose then
                 begin
diff --git a/infer/src/clang/cArithmetic_trans.ml b/infer/src/clang/cArithmetic_trans.ml
index aa4cc66c6..57eaadfa1 100644
--- a/infer/src/clang/cArithmetic_trans.ml
+++ b/infer/src/clang/cArithmetic_trans.ml
@@ -144,12 +144,12 @@ let unary_operation_instruction uoi e typ loc =
   | `PostInc ->
       let id = Ident.create_fresh Ident.knormal in
       let instr1 = Sil.Letderef (id, e, typ, loc) in
-      let e_plus_1 = Sil.BinOp(Sil.PlusA, Sil.Var id, Sil.Const(Sil.Cint (Sil.Int.one))) in
+      let e_plus_1 = Sil.BinOp(Sil.PlusA, Sil.Var id, Sil.Const(Sil.Cint (IntLit.one))) in
       (Sil.Var id, instr1::[Sil.Set (e, typ, e_plus_1, loc)])
   | `PreInc ->
       let id = Ident.create_fresh Ident.knormal in
       let instr1 = Sil.Letderef (id, e, typ, loc) in
-      let e_plus_1 = Sil.BinOp(Sil.PlusA, Sil.Var id, Sil.Const(Sil.Cint (Sil.Int.one))) in
+      let e_plus_1 = Sil.BinOp(Sil.PlusA, Sil.Var id, Sil.Const(Sil.Cint (IntLit.one))) in
       let exp = if General_utils.is_cpp_translation Config.clang_lang then
           e
         else
@@ -158,12 +158,12 @@ let unary_operation_instruction uoi e typ loc =
   | `PostDec ->
       let id = Ident.create_fresh Ident.knormal in
       let instr1 = Sil.Letderef (id, e, typ, loc) in
-      let e_minus_1 = Sil.BinOp(Sil.MinusA, Sil.Var id, Sil.Const(Sil.Cint (Sil.Int.one))) in
+      let e_minus_1 = Sil.BinOp(Sil.MinusA, Sil.Var id, Sil.Const(Sil.Cint (IntLit.one))) in
       (Sil.Var id, instr1::[Sil.Set (e, typ, e_minus_1, loc)])
   | `PreDec ->
       let id = Ident.create_fresh Ident.knormal in
       let instr1 = Sil.Letderef (id, e, typ, loc) in
-      let e_minus_1 = Sil.BinOp(Sil.MinusA, Sil.Var id, Sil.Const(Sil.Cint (Sil.Int.one))) in
+      let e_minus_1 = Sil.BinOp(Sil.MinusA, Sil.Var id, Sil.Const(Sil.Cint (IntLit.one))) in
       let exp = if General_utils.is_cpp_translation Config.clang_lang then
           e
         else
@@ -220,5 +220,5 @@ let bin_op_to_string boi =
 let sil_const_plus_one const =
   match const with
   | Sil.Const (Sil.Cint n) ->
-      Sil.Const (Sil.Cint (Sil.Int.add n Sil.Int.one))
-  | _ -> Sil.BinOp (Sil.PlusA, const, Sil.Const (Sil.Cint (Sil.Int.one)))
+      Sil.Const (Sil.Cint (IntLit.add n IntLit.one))
+  | _ -> Sil.BinOp (Sil.PlusA, const, Sil.Const (Sil.Cint (IntLit.one)))
diff --git a/infer/src/clang/cTrans.ml b/infer/src/clang/cTrans.ml
index 890e3a392..84c63b8a2 100644
--- a/infer/src/clang/cTrans.ml
+++ b/infer/src/clang/cTrans.ml
@@ -345,7 +345,7 @@ struct
      So we implement it as the constant zero *)
   let gNUNullExpr_trans trans_state expr_info =
     let typ = CTypes_decl.get_type_from_expr_info expr_info trans_state.context.CContext.tenv in
-    let exp = Sil.Const (Sil.Cint (Sil.Int.zero)) in
+    let exp = Sil.Const (Sil.Cint (IntLit.zero)) in
     { empty_res_trans with exps = [(exp, typ)]}
 
   let nullPtrExpr_trans trans_state expr_info =
@@ -366,7 +366,7 @@ struct
 
   let characterLiteral_trans trans_state expr_info n =
     let typ = CTypes_decl.get_type_from_expr_info expr_info trans_state.context.CContext.tenv in
-    let exp = Sil.Const (Sil.Cint (Sil.Int.of_int n)) in
+    let exp = Sil.Const (Sil.Cint (IntLit.of_int n)) in
     { empty_res_trans with exps = [(exp, typ)]}
 
   let floatingLiteral_trans trans_state expr_info float_string =
@@ -381,7 +381,7 @@ struct
     let exp =
       try
         let i = Int64.of_string integer_literal_info.Clang_ast_t.ili_value in
-        let exp = Sil.exp_int (Sil.Int.of_int64 i) in
+        let exp = Sil.exp_int (IntLit.of_int64 i) in
         exp
       with
       | Failure _ ->
@@ -398,7 +398,7 @@ struct
     let zero_opt = match typ with
       | Sil.Tfloat _  | Sil.Tptr _ | Sil.Tint _ -> Some (Sil.zero_value_of_numerical_type typ)
       | Sil.Tvoid -> None
-      | _ -> Some (Sil.Const (Sil.Cint Sil.Int.zero)) in
+      | _ -> Some (Sil.Const (Sil.Cint IntLit.zero)) in
     match zero_opt with
     | Some zero -> { empty_res_trans with exps = [(zero, typ)] }
     | _ -> empty_res_trans
@@ -677,7 +677,7 @@ struct
 
   (* get the sil value of the enum constant from the map or by evaluating it *)
   and get_enum_constant_expr context enum_constant_pointer =
-    let zero = Sil.Const (Sil.Cint Sil.Int.zero) in
+    let zero = Sil.Const (Sil.Cint IntLit.zero) in
     try
       let (prev_enum_constant_opt, sil_exp_opt) =
         Ast_utils.get_enum_constant_exp enum_constant_pointer in
@@ -855,7 +855,7 @@ struct
                  NEED TO BE FIXED\n\n";
               fix_param_exps_mismatch params_stmt params) in
       let act_params = if is_cf_retain_release then
-          (Sil.Const (Sil.Cint Sil.Int.one), Sil.Tint Sil.IBool) :: act_params
+          (Sil.Const (Sil.Cint IntLit.one), Sil.Tint Sil.IBool) :: act_params
         else act_params in
       match
         CTrans_utils.builtin_trans trans_state_pri sil_loc si function_type callee_pname_opt with
@@ -1185,7 +1185,7 @@ struct
       Printing.log_out " No short-circuit condition\n";
       let res_trans_cond =
         if is_null_stmt cond then {
-          empty_res_trans with exps = [(Sil.Const (Sil.Cint Sil.Int.one), (Sil.Tint Sil.IBool))]
+          empty_res_trans with exps = [(Sil.Const (Sil.Cint IntLit.one), (Sil.Tint Sil.IBool))]
         }
         (* Assumption: If it's a null_stmt, it is a loop with no bound, so we set condition to 1 *)
         else
@@ -2034,7 +2034,7 @@ struct
     let (var_exp_inside, typ_inside) = match typ with
       | Sil.Tarray (t, _)
       | Sil.Tptr (t, _) when Sil.is_array_of_cpp_class typ || is_dyn_array ->
-          Sil.Lindex (var_exp, Sil.Const (Sil.Cint (Sil.Int.of_int n))), t
+          Sil.Lindex (var_exp, Sil.Const (Sil.Cint (IntLit.of_int n))), t
       | _ -> var_exp, typ in
     let trans_state' = { trans_state with var_exp_typ = Some (var_exp_inside, typ_inside) } in
     match stmts with
@@ -2085,7 +2085,7 @@ struct
             (match res_trans_size.exps with
              | [(exp, _)] -> Some exp, res_trans_size
              | _ -> None, empty_res_trans)
-        | None -> Some (Sil.Const (Sil.Cint (Sil.Int.minus_one))), empty_res_trans
+        | None -> Some (Sil.Const (Sil.Cint (IntLit.minus_one))), empty_res_trans
       else None, empty_res_trans in
     let res_trans_new = cpp_new_trans trans_state_pri sil_loc typ size_exp_opt in
     let stmt_opt = Ast_utils.get_stmt_opt cxx_new_expr_info.Clang_ast_t.xnei_initializer_expr in
@@ -2099,8 +2099,8 @@ struct
       if is_dyn_array && Sil.is_pointer_to_cpp_class typ then
         let rec create_stmts stmt_opt size_exp_opt =
           match stmt_opt, size_exp_opt with
-          | Some stmt, Some (Sil.Const (Sil.Cint n)) when not (Sil.Int.iszero n) ->
-              let n_minus_1 = Some ((Sil.Const (Sil.Cint (Sil.Int.sub n Sil.Int.one)))) in
+          | Some stmt, Some (Sil.Const (Sil.Cint n)) when not (IntLit.iszero n) ->
+              let n_minus_1 = Some ((Sil.Const (Sil.Cint (IntLit.sub n IntLit.one)))) in
               stmt :: create_stmts stmt_opt n_minus_1
           | _ -> [] in
         let stmts = create_stmts stmt_opt size_exp_opt in
diff --git a/infer/src/clang/cTrans_utils.ml b/infer/src/clang/cTrans_utils.ml
index 623f870c6..f3dc628aa 100644
--- a/infer/src/clang/cTrans_utils.ml
+++ b/infer/src/clang/cTrans_utils.ml
@@ -685,10 +685,10 @@ let var_or_zero_in_init_list tenv e typ ~return_zero:return_zero =
         IList.map (fun (e, t) ->
             IList.flatten (var_or_zero_in_init_list' e t tns)) exp_types
     | Sil.Tarray (arrtyp, Some n) ->
-        let size = Sil.Int.to_int n in
+        let size = IntLit.to_int n in
         let indices = list_range 0 (size - 1) in
         let index_constants =
-          IList.map (fun i -> (Sil.Const (Sil.Cint (Sil.Int.of_int i)))) indices in
+          IList.map (fun i -> (Sil.Const (Sil.Cint (IntLit.of_int i)))) indices in
         let lh_exprs =
           IList.map (fun index_expr -> Sil.Lindex (e, index_expr)) index_constants in
         let lh_types = replicate size arrtyp in
diff --git a/infer/src/clang/cType_to_sil_type.ml b/infer/src/clang/cType_to_sil_type.ml
index 4ebdfaff5..6f85183f4 100644
--- a/infer/src/clang/cType_to_sil_type.ml
+++ b/infer/src/clang/cType_to_sil_type.ml
@@ -63,7 +63,7 @@ let pointer_attribute_of_objc_attribute attr_info =
 
 let rec build_array_type translate_decl tenv type_ptr n_opt =
   let array_type = type_ptr_to_sil_type translate_decl tenv type_ptr in
-  let len = Option.map (fun n -> Sil.Int.of_int64 (Int64.of_int n)) n_opt in
+  let len = Option.map (fun n -> IntLit.of_int64 (Int64.of_int n)) n_opt in
   Sil.Tarray (array_type, len)
 
 and sil_type_of_attr_type translate_decl tenv type_info attr_info =
diff --git a/infer/src/eradicate/typeCheck.ml b/infer/src/eradicate/typeCheck.ml
index a7c72e7e2..06441bd4d 100644
--- a/infer/src/eradicate/typeCheck.ml
+++ b/infer/src/eradicate/typeCheck.ml
@@ -169,7 +169,7 @@ let rec typecheck_expr
       (match TypeState.lookup_id id typestate with
        | Some tr -> TypeState.range_add_locs tr [loc]
        | None -> tr_default)
-  | Sil.Const (Sil.Cint i) when Sil.Int.iszero i ->
+  | Sil.Const (Sil.Cint i) when IntLit.iszero i ->
       let (typ, _, locs) = tr_default in
       if PatternMatch.type_is_class typ
       then (typ, TypeAnnotation.const Annotations.Nullable true (TypeOrigin.Const loc), locs)
@@ -707,7 +707,7 @@ let typecheck_instr
           let do_instr = function
             | Sil.Prune (Sil.BinOp (Sil.Eq, _cond_e, Sil.Const (Sil.Cint i)), _, _, _)
             | Sil.Prune (Sil.BinOp (Sil.Eq, Sil.Const (Sil.Cint i), _cond_e), _, _, _)
-              when Sil.Int.iszero i ->
+              when IntLit.iszero i ->
                 let cond_e = Idenv.expand_expr_temps idenv cond_node _cond_e in
                 begin
                   match convert_complex_exp_to_pvar cond_node false cond_e typestate' loc with
@@ -946,7 +946,7 @@ let typecheck_instr
 
         match c with
         | Sil.BinOp (Sil.Eq, Sil.Const (Sil.Cint i), e)
-        | Sil.BinOp (Sil.Eq, e, Sil.Const (Sil.Cint i)) when Sil.Int.iszero i ->
+        | Sil.BinOp (Sil.Eq, e, Sil.Const (Sil.Cint i)) when IntLit.iszero i ->
             typecheck_expr_for_errors typestate e loc;
             let typestate1, e1, from_call = match from_is_true_on_null e with
               | Some e1 ->
@@ -975,7 +975,7 @@ let typecheck_instr
             end
 
         | Sil.BinOp (Sil.Ne, Sil.Const (Sil.Cint i), e)
-        | Sil.BinOp (Sil.Ne, e, Sil.Const (Sil.Cint i)) when Sil.Int.iszero i ->
+        | Sil.BinOp (Sil.Ne, e, Sil.Const (Sil.Cint i)) when IntLit.iszero i ->
             typecheck_expr_for_errors typestate e loc;
             let typestate1, e1, from_call = match from_instanceof e with
               | Some e1 -> (* (e1 instanceof C) implies (e1 != null) *)
diff --git a/infer/src/harness/inhabit.ml b/infer/src/harness/inhabit.ml
index d2277edf2..be47ad873 100644
--- a/infer/src/harness/inhabit.ml
+++ b/infer/src/harness/inhabit.ml
@@ -85,8 +85,8 @@ let rec inhabit_typ typ cfg env =
   with Not_found ->
     let inhabit_internal typ env = match typ with
       | Sil.Tptr (Sil.Tarray (inner_typ, Some _), Sil.Pk_pointer) ->
-          let len = Sil.Const (Sil.Cint (Sil.Int.one)) in
-          let arr_typ = Sil.Tarray (inner_typ, Some Sil.Int.one) in
+          let len = Sil.Const (Sil.Cint (IntLit.one)) in
+          let arr_typ = Sil.Tarray (inner_typ, Some IntLit.one) in
           inhabit_alloc arr_typ (Some len) typ ModelBuiltins.__new_array env
       | Sil.Tptr (typ, Sil.Pk_pointer) as ptr_to_typ ->
           (* TODO (t4575417): this case does not work correctly for enums, but they are currently
@@ -130,7 +130,7 @@ let rec inhabit_typ typ cfg env =
           let fresh_id = Ident.create_fresh Ident.knormal in
           let read_from_local_instr = Sil.Letderef (fresh_id, fresh_local_exp, ptr_to_typ, env'.pc) in
           (Sil.Var fresh_id, env_add_instr read_from_local_instr env')
-      | Sil.Tint (_) -> (Sil.Const (Sil.Cint (Sil.Int.zero)), env)
+      | Sil.Tint (_) -> (Sil.Const (Sil.Cint (IntLit.zero)), env)
       | Sil.Tfloat (_) -> (Sil.Const (Sil.Cfloat 0.0), env)
       | typ ->
           L.err "Couldn't inhabit typ: %a@." (Sil.pp_typ pe_text) typ;
diff --git a/infer/src/java/jTrans.ml b/infer/src/java/jTrans.ml
index 67e91b6ff..2784d80a1 100644
--- a/infer/src/java/jTrans.ml
+++ b/infer/src/java/jTrans.ml
@@ -169,12 +169,12 @@ let locals_formals program tenv cn impl meth_kind =
 
 let get_constant (c : JBir.const) =
   match c with
-  | `Int i -> Sil.Cint (Sil.Int.of_int32 i)
-  | `ANull -> Sil.Cint Sil.Int.null
+  | `Int i -> Sil.Cint (IntLit.of_int32 i)
+  | `ANull -> Sil.Cint IntLit.null
   | `Class ot -> Sil.Cclass (Ident.string_to_name (JTransType.object_type_to_string ot))
   | `Double f -> Sil.Cfloat f
   | `Float f -> Sil.Cfloat f
-  | `Long i64 -> Sil.Cint (Sil.Int.of_int64 i64)
+  | `Long i64 -> Sil.Cint (IntLit.of_int64 i64)
   | `String jstr -> Sil.Cstr (JBasics.jstr_pp jstr)
 
 let get_binop binop =
@@ -653,14 +653,6 @@ let get_array_length context pc expr_list content_type =
   let array_size = Sil.Sizeof (array_type, array_len, Sil.Subtype.exact) in
   (instrs, array_size)
 
-module Int =
-struct
-  type t = int
-  let compare = (-)
-end
-
-module IntSet = Set.Make(Int)
-
 let detect_loop entry_pc impl =
   let code = (JBir.code impl) in
   let pc_bound = Array.length code in
@@ -1050,7 +1042,7 @@ let rec instruction context pc instr : translation =
           let sil_assume_in_bound =
             let sil_in_bound =
               let sil_positive_index =
-                Sil.BinOp (Sil.Ge, sil_index_expr, Sil.Const (Sil.Cint Sil.Int.zero))
+                Sil.BinOp (Sil.Ge, sil_index_expr, Sil.Const (Sil.Cint IntLit.zero))
               and sil_less_than_length =
                 Sil.BinOp (Sil.Lt, sil_index_expr, sil_length_expr) in
               Sil.BinOp (Sil.LAnd, sil_positive_index, sil_less_than_length) in
@@ -1063,7 +1055,7 @@ let rec instruction context pc instr : translation =
           let sil_assume_out_of_bound =
             let sil_out_of_bound =
               let sil_negative_index =
-                Sil.BinOp (Sil.Lt, sil_index_expr, Sil.Const (Sil.Cint Sil.Int.zero))
+                Sil.BinOp (Sil.Lt, sil_index_expr, Sil.Const (Sil.Cint IntLit.zero))
               and sil_greater_than_length =
                 Sil.BinOp (Sil.Gt, sil_index_expr, sil_length_expr) in
               Sil.BinOp (Sil.LOr, sil_negative_index, sil_greater_than_length) in
diff --git a/infer/src/llvm/lTrans.ml b/infer/src/llvm/lTrans.ml
index 97be414b6..19a645edf 100644
--- a/infer/src/llvm/lTrans.ml
+++ b/infer/src/llvm/lTrans.ml
@@ -24,7 +24,7 @@ let ident_of_variable (var : LAst.variable) : Ident.t = (* TODO: use unique stam
 let trans_variable (var : LAst.variable) : Sil.exp = Sil.Var (ident_of_variable var)
 
 let trans_constant : LAst.constant -> Sil.exp = function
-  | Cint i -> Sil.Const (Sil.Cint (Sil.Int.of_int i))
+  | Cint i -> Sil.Const (Sil.Cint (IntLit.of_int i))
   | Cnull -> Sil.exp_null
 
 let trans_operand : LAst.operand -> Sil.exp = function
@@ -36,7 +36,7 @@ let rec trans_typ : LAst.typ -> Sil.typ = function
   | Tfloat -> Sil.Tfloat Sil.FFloat
   | Tptr tp -> Sil.Tptr (trans_typ tp, Sil.Pk_pointer)
   | Tvector (i, tp)
-  | Tarray (i, tp) -> Sil.Tarray (trans_typ tp, Some (Sil.Int.of_int i))
+  | Tarray (i, tp) -> Sil.Tarray (trans_typ tp, Some (IntLit.of_int i))
   | Tfunc _ -> Sil.Tfun false
   | Tlabel -> raise (ImproperTypeError "Tried to generate Sil type from LLVM label type.")
   | Tmetadata -> raise (ImproperTypeError "Tried to generate Sil type from LLVM metadata type.")
diff --git a/infer/src/unit/analyzerTester.ml b/infer/src/unit/analyzerTester.ml
index baa146c43..eaa8ae29b 100644
--- a/infer/src/unit/analyzerTester.ml
+++ b/infer/src/unit/analyzerTester.ml
@@ -114,7 +114,7 @@ module StructuredSil = struct
     make_set ~rhs_typ ~lhs_exp ~rhs_exp
 
   let var_assign_int lhs rhs =
-    let rhs_exp = Sil.exp_int (Sil.Int.of_int rhs) in
+    let rhs_exp = Sil.exp_int (IntLit.of_int rhs) in
     let rhs_typ = Sil.Tint Sil.IInt in
     var_assign_exp ~rhs_typ lhs rhs_exp