diff --git a/infer/src/IR/Exp.re b/infer/src/IR/Exp.re
index a6a471ba1..231706953 100644
--- a/infer/src/IR/Exp.re
+++ b/infer/src/IR/Exp.re
@@ -185,3 +185,144 @@ let module Hash = Hashtbl.Make {
   let equal = equal;
   let hash = hash;
 };
+
+let rec is_array_index_of exp1 exp2 =>
+  switch exp1 {
+  | Lindex exp _ => is_array_index_of exp exp2
+  | _ => equal exp1 exp2
+  };
+
+let is_null_literal =
+  fun
+  | Const (Cint n) => IntLit.isnull n
+  | _ => false;
+
+let is_this =
+  fun
+  | Lvar pvar => Pvar.is_this pvar
+  | _ => false;
+
+let is_zero =
+  fun
+  | Const (Cint n) => IntLit.iszero n
+  | _ => false;
+
+
+/** {2 Utility Functions for Expressions} */
+/** Turn an expression representing a type into the type it represents
+    If not a sizeof, return the default type if given, otherwise raise an exception */
+let texp_to_typ default_opt =>
+  fun
+  | Sizeof t _ _ => t
+  | _ => Typ.unsome "texp_to_typ" default_opt;
+
+
+/** Return the root of [lexp]. */
+let rec root_of_lexp lexp =>
+  switch (lexp: t) {
+  | Var _ => lexp
+  | Const _ => lexp
+  | Cast _ e => root_of_lexp e
+  | UnOp _
+  | BinOp _
+  | Exn _
+  | Closure _ => lexp
+  | Lvar _ => lexp
+  | Lfield e _ _ => root_of_lexp e
+  | Lindex e _ => root_of_lexp e
+  | Sizeof _ => lexp
+  };
+
+
+/** Checks whether an expression denotes a location by pointer arithmetic.
+    Currently, catches array - indexing expressions such as a[i] only. */
+let rec pointer_arith =
+  fun
+  | Lfield e _ _ => pointer_arith e
+  | Lindex _ => true
+  | _ => false;
+
+let get_undefined footprint =>
+  Var (
+    Ident.create_fresh (
+      if footprint {
+        Ident.kfootprint
+      } else {
+        Ident.kprimed
+      }
+    )
+  );
+
+
+/** Create integer constant */
+let int i => Const (Cint i);
+
+
+/** Create float constant */
+let float v => Const (Cfloat v);
+
+
+/** Integer constant 0 */
+let zero = int IntLit.zero;
+
+
+/** Null constant */
+let null = int IntLit.null;
+
+
+/** Integer constant 1 */
+let one = int IntLit.one;
+
+
+/** Integer constant -1 */
+let minus_one = int IntLit.minus_one;
+
+
+/** Create integer constant corresponding to the boolean value */
+let bool b =>
+  if b {
+    one
+  } else {
+    zero
+  };
+
+
+/** Create expresstion [e1 == e2] */
+let eq e1 e2 => BinOp Eq e1 e2;
+
+
+/** Create expresstion [e1 != e2] */
+let ne e1 e2 => BinOp Ne e1 e2;
+
+
+/** Create expression [e1 <= e2] */
+let le e1 e2 => BinOp Le e1 e2;
+
+
+/** Create expression [e1 < e2] */
+let lt e1 e2 => BinOp Lt e1 e2;
+
+
+/** Extract the ids and pvars from an expression */
+let get_vars exp => {
+  let rec get_vars_ exp vars =>
+    switch exp {
+    | Lvar pvar => (fst vars, [pvar, ...snd vars])
+    | Var id => ([id, ...fst vars], snd vars)
+    | Cast _ e
+    | UnOp _ e _
+    | Lfield e _ _
+    | Exn e => get_vars_ e vars
+    | BinOp _ e1 e2
+    | Lindex e1 e2 => get_vars_ e1 vars |> get_vars_ e2
+    | Closure {captured_vars} =>
+      IList.fold_left
+        (fun vars_acc (captured_exp, _, _) => get_vars_ captured_exp vars_acc) vars captured_vars
+    | Const (Cint _ | Cfun _ | Cstr _ | Cfloat _ | Cclass _ | Cptr_to_fld _) => vars
+    /* TODO: Sizeof length expressions may contain variables, do not ignore them. */
+    /* | Sizeof _ None _ => vars */
+    /* | Sizeof _ (Some l) _ => get_vars_ l vars */
+    | Sizeof _ _ _ => vars
+    };
+  get_vars_ exp ([], [])
+};
diff --git a/infer/src/IR/Exp.rei b/infer/src/IR/Exp.rei
index efe0e2130..0352bc3c9 100644
--- a/infer/src/IR/Exp.rei
+++ b/infer/src/IR/Exp.rei
@@ -74,3 +74,83 @@ let module Map: Map.S with type key = t;
 
 /** Hashtable with expression keys. */
 let module Hash: Hashtbl.S with type key = t;
+
+
+/** returns true is index is an array index of arr. */
+let is_array_index_of: t => t => bool;
+
+let is_null_literal: t => bool;
+
+
+/** return true if [exp] is the special this/self expression */
+let is_this: t => bool;
+
+let is_zero: t => bool;
+
+
+/** {2 Utility Functions for Expressions} */
+/** Turn an expression representing a type into the type it represents
+    If not a sizeof, return the default type if given, otherwise raise an exception */
+let texp_to_typ: option Typ.t => t => Typ.t;
+
+
+/** Return the root of [lexp]. */
+let root_of_lexp: t => t;
+
+
+/** Get an expression "undefined", the boolean indicates
+    whether the undefined value goest into the footprint */
+let get_undefined: bool => t;
+
+
+/** Checks whether an expression denotes a location using pointer arithmetic.
+    Currently, catches array - indexing expressions such as a[i] only. */
+let pointer_arith: t => bool;
+
+
+/** Integer constant 0 */
+let zero: t;
+
+
+/** Null constant */
+let null: t;
+
+
+/** Integer constant 1 */
+let one: t;
+
+
+/** Integer constant -1 */
+let minus_one: t;
+
+
+/** Create integer constant */
+let int: IntLit.t => t;
+
+
+/** Create float constant */
+let float: float => t;
+
+
+/** Create integer constant corresponding to the boolean value */
+let bool: bool => t;
+
+
+/** Create expresstion [e1 == e2] */
+let eq: t => t => t;
+
+
+/** Create expresstion [e1 != e2] */
+let ne: t => t => t;
+
+
+/** Create expresstion [e1 <= e2] */
+let le: t => t => t;
+
+
+/** Create expression [e1 < e2] */
+let lt: t => t => t;
+
+
+/** Extract the ids and pvars from an expression */
+let get_vars: t => (list Ident.t, list Pvar.t);
diff --git a/infer/src/IR/Sil.re b/infer/src/IR/Sil.re
index 335f442cf..ccbcf6c05 100644
--- a/infer/src/IR/Sil.re
+++ b/infer/src/IR/Sil.re
@@ -312,22 +312,6 @@ let is_static_local_name pname pvar =>
     }
   };
 
-let exp_is_zero =
-  fun
-  | Exp.Const (Cint n) => IntLit.iszero n
-  | _ => false;
-
-let exp_is_null_literal =
-  fun
-  | Exp.Const (Cint n) => IntLit.isnull n
-  | _ => false;
-
-let exp_is_this =
-  fun
-  | Exp.Lvar pvar => Pvar.is_this pvar
-  | _ => false;
-
-
 let path_pos_compare (pn1, nid1) (pn2, nid2) => {
   let n = Procname.compare pn1 pn2;
   if (n != 0) {
@@ -510,20 +494,12 @@ let attribute_compare (att1: attribute) (att2: attribute) :int =>
   | (_, Aunsubscribed_observer) => 1
   };
 
-let rec exp_is_array_index_of exp1 exp2 =>
-  switch exp1 {
-  | Exp.Lindex exp _ => exp_is_array_index_of exp exp2
-  | _ => Exp.equal exp1 exp2
-  };
-
 let ident_exp_compare = pair_compare Ident.compare Exp.compare;
 
 let ident_exp_equal ide1 ide2 => ident_exp_compare ide1 ide2 == 0;
 
 let exp_list_compare = IList.compare Exp.compare;
 
-let exp_list_equal el1 el2 => exp_list_compare el1 el2 == 0;
-
 let attribute_equal att1 att2 => attribute_compare att1 att2 == 0;
 
 
@@ -1795,101 +1771,6 @@ let hpred_list_get_lexps (filter: Exp.t => bool) (hlist: list hpred) :list Exp.t
 };
 
 
-/** {2 Utility Functions for Expressions} */
-/** Turn an expression representing a type into the type it represents
-    If not a sizeof, return the default type if given, otherwise raise an exception */
-let texp_to_typ default_opt =>
-  fun
-  | Exp.Sizeof t _ _ => t
-  | _ => Typ.unsome "texp_to_typ" default_opt;
-
-
-/** Return the root of [lexp]. */
-let rec root_of_lexp lexp =>
-  switch (lexp: Exp.t) {
-  | Var _ => lexp
-  | Const _ => lexp
-  | Cast _ e => root_of_lexp e
-  | UnOp _
-  | BinOp _
-  | Exn _
-  | Closure _ => lexp
-  | Lvar _ => lexp
-  | Lfield e _ _ => root_of_lexp e
-  | Lindex e _ => root_of_lexp e
-  | Sizeof _ => lexp
-  };
-
-
-/** Checks whether an expression denotes a location by pointer arithmetic.
-    Currently, catches array - indexing expressions such as a[i] only. */
-let rec exp_pointer_arith =
-  fun
-  | Exp.Lfield e _ _ => exp_pointer_arith e
-  | Exp.Lindex _ => true
-  | _ => false;
-
-let exp_get_undefined footprint =>
-  Exp.Var (
-    Ident.create_fresh (
-      if footprint {
-        Ident.kfootprint
-      } else {
-        Ident.kprimed
-      }
-    )
-  );
-
-
-/** Create integer constant */
-let exp_int i => Exp.Const (Cint i);
-
-
-/** Create float constant */
-let exp_float v => Exp.Const (Cfloat v);
-
-
-/** Integer constant 0 */
-let exp_zero = exp_int IntLit.zero;
-
-
-/** Null constant */
-let exp_null = exp_int IntLit.null;
-
-
-/** Integer constant 1 */
-let exp_one = exp_int IntLit.one;
-
-
-/** Integer constant -1 */
-let exp_minus_one = exp_int IntLit.minus_one;
-
-
-/** Create integer constant corresponding to the boolean value */
-let exp_bool b =>
-  if b {
-    exp_one
-  } else {
-    exp_zero
-  };
-
-
-/** Create expresstion [e1 == e2] */
-let exp_eq e1 e2 => Exp.BinOp Eq e1 e2;
-
-
-/** Create expresstion [e1 != e2] */
-let exp_ne e1 e2 => Exp.BinOp Ne e1 e2;
-
-
-/** Create expression [e1 <= e2] */
-let exp_le e1 e2 => Exp.BinOp Le e1 e2;
-
-
-/** Create expression [e1 < e2] */
-let exp_lt e1 e2 => Exp.BinOp Lt e1 e2;
-
-
 /** {2 Functions for computing program variables} */
 let rec exp_fpv e =>
   switch (e: Exp.t) {
@@ -3141,33 +3022,6 @@ let hpred_compact sh hpred =>
 
 
 /** {2 Functions for constructing or destructing entities in this module} */
-/** Extract the ids and pvars from an expression */
-let exp_get_vars exp => {
-  let rec exp_get_vars_ exp vars =>
-    switch (exp: Exp.t) {
-    | Lvar pvar => (fst vars, [pvar, ...snd vars])
-    | Var id => ([id, ...fst vars], snd vars)
-    | Cast _ e
-    | UnOp _ e _
-    | Lfield e _ _
-    | Exn e => exp_get_vars_ e vars
-    | BinOp _ e1 e2
-    | Lindex e1 e2 => exp_get_vars_ e1 vars |> exp_get_vars_ e2
-    | Closure {captured_vars} =>
-      IList.fold_left
-        (fun vars_acc (captured_exp, _, _) => exp_get_vars_ captured_exp vars_acc)
-        vars
-        captured_vars
-    | Const (Cint _ | Cfun _ | Cstr _ | Cfloat _ | Cclass _ | Cptr_to_fld _) => vars
-    /* TODO: Sizeof length expressions may contain variables, do not ignore them. */
-    /* | Sizeof _ None _ => vars */
-    /* | Sizeof _ (Some l) _ => exp_get_vars_ l vars */
-    | Sizeof _ _ _ => vars
-    };
-  exp_get_vars_ exp ([], [])
-};
-
-
 /** Compute the offset list of an expression */
 let exp_get_offsets exp => {
   let rec f offlist_past e =>
diff --git a/infer/src/IR/Sil.rei b/infer/src/IR/Sil.rei
index 880f861ce..964c5cb51 100644
--- a/infer/src/IR/Sil.rei
+++ b/infer/src/IR/Sil.rei
@@ -318,14 +318,6 @@ let hpred_compact: sharing_env => hpred => hpred;
 /** {2 Comparision And Inspection Functions} */
 let has_objc_ref_counter: hpred => bool;
 
-let exp_is_zero: Exp.t => bool;
-
-let exp_is_null_literal: Exp.t => bool;
-
-
-/** return true if [exp] is the special this/self expression */
-let exp_is_this: Exp.t => bool;
-
 let path_pos_equal: path_pos => path_pos => bool;
 
 
@@ -384,10 +376,6 @@ let attribute_to_category: attribute => attribute_category;
 
 let attr_is_undef: attribute => bool;
 
-
-/** exp_is_array_index_of index arr returns true is index is an array index of arr. */
-let exp_is_array_index_of: Exp.t => Exp.t => bool;
-
 let exp_typ_compare: (Exp.t, Typ.t) => (Exp.t, Typ.t) => int;
 
 let instr_compare: instr => instr => int;
@@ -398,10 +386,6 @@ let instr_compare: instr => instr => int;
     used in the procedure of [instr2] */
 let instr_compare_structural: instr => instr => Exp.Map.t Exp.t => (int, Exp.Map.t Exp.t);
 
-let exp_list_compare: list Exp.t => list Exp.t => int;
-
-let exp_list_equal: list Exp.t => list Exp.t => bool;
-
 let atom_compare: atom => atom => int;
 
 let atom_equal: atom => atom => bool;
@@ -669,70 +653,6 @@ let atom_list_expmap: (Exp.t => Exp.t) => list atom => list atom;
 let hpred_list_get_lexps: (Exp.t => bool) => list hpred => list Exp.t;
 
 
-/** {2 Utility Functions for Expressions} */
-/** Turn an expression representing a type into the type it represents
-    If not a sizeof, return the default type if given, otherwise raise an exception */
-let texp_to_typ: option Typ.t => Exp.t => Typ.t;
-
-
-/** Return the root of [lexp]. */
-let root_of_lexp: Exp.t => Exp.t;
-
-
-/** Get an expression "undefined", the boolean indicates
-    whether the undefined value goest into the footprint */
-let exp_get_undefined: bool => Exp.t;
-
-
-/** Checks whether an expression denotes a location using pointer arithmetic.
-    Currently, catches array - indexing expressions such as a[i] only. */
-let exp_pointer_arith: Exp.t => bool;
-
-
-/** Integer constant 0 */
-let exp_zero: Exp.t;
-
-
-/** Null constant */
-let exp_null: Exp.t;
-
-
-/** Integer constant 1 */
-let exp_one: Exp.t;
-
-
-/** Integer constant -1 */
-let exp_minus_one: Exp.t;
-
-
-/** Create integer constant */
-let exp_int: IntLit.t => Exp.t;
-
-
-/** Create float constant */
-let exp_float: float => Exp.t;
-
-
-/** Create integer constant corresponding to the boolean value */
-let exp_bool: bool => Exp.t;
-
-
-/** Create expresstion [e1 == e2] */
-let exp_eq: Exp.t => Exp.t => Exp.t;
-
-
-/** Create expresstion [e1 != e2] */
-let exp_ne: Exp.t => Exp.t => Exp.t;
-
-
-/** Create expresstion [e1 <= e2] */
-let exp_le: Exp.t => Exp.t => Exp.t;
-
-
-/** Create expression [e1 < e2] */
-let exp_lt: Exp.t => Exp.t => Exp.t;
-
-
 /** {2 Functions for computing program variables} */
 let exp_fpv: Exp.t => list Pvar.t;
 
@@ -999,10 +919,6 @@ let hpred_replace_exp: list (Exp.t, Exp.t) => hpred => hpred;
 
 
 /** {2 Functions for constructing or destructing entities in this module} */
-/** Extract the ids and pvars from an expression */
-let exp_get_vars: Exp.t => (list Ident.t, list Pvar.t);
-
-
 /** Compute the offset list of an expression */
 let exp_get_offsets: Exp.t => list offset;
 
diff --git a/infer/src/backend/absarray.ml b/infer/src/backend/absarray.ml
index 0496832b5..dab2ec5e5 100644
--- a/infer/src/backend/absarray.ml
+++ b/infer/src/backend/absarray.ml
@@ -182,7 +182,7 @@ end = struct
             match hpred with
             | Sil.Hpointsto (root, se, te) ->
                 let sigma_other = sigma_seen @ sigma_rest in
-                find_offset_sexp sigma_other hpred root [] se (Sil.texp_to_typ None te)
+                find_offset_sexp sigma_other hpred root [] se (Exp.texp_to_typ None te)
             | _ -> ()
           end;
           iterate (hpred:: sigma_seen) sigma_rest in
@@ -194,7 +194,7 @@ end = struct
   (** Get the matched strexp *)
   let get_data ((_ , hpred, syn_offs) : t) = match hpred with
     | Sil.Hpointsto (root, se, te) ->
-        let t = Sil.texp_to_typ None te in
+        let t = Exp.texp_to_typ None te in
         let se', t' = get_strexp_at_syn_offsets se t syn_offs in
         let path' = (root, syn_offs) in
         (path', se', t')
@@ -220,7 +220,7 @@ end = struct
     begin
       match hpred with
       | Sil.Hpointsto (root, se, te) ->
-          let t = Sil.texp_to_typ None te in
+          let t = Exp.texp_to_typ None te in
           let se' = replace_strexp_at_syn_offsets se t syn_offs update in
           Sil.Hpointsto (root, se', te)
       | _ -> assert false
@@ -354,7 +354,7 @@ let generic_strexp_abstract
 (** Return [true] if there's a pointer to the index *)
 let index_is_pointed_to (p: Prop.normal Prop.t) (path: StrexpMatch.path) (index: Exp.t) : bool =
   let indices =
-    let index_plus_one = Exp.BinOp(Binop.PlusA, index, Sil.exp_one) in
+    let index_plus_one = Exp.BinOp(Binop.PlusA, index, Exp.one) in
     [index; index_plus_one] in
   let add_index_to_paths =
     let elist_path = StrexpMatch.path_to_exps path in
@@ -393,8 +393,8 @@ let blur_array_index
       let sigma' = StrexpMatch.replace_index false matched index fresh_index in
       Prop.replace_sigma sigma' p2 in
     let p4 =
-      let index_next = Exp.BinOp(Binop.PlusA, index, Sil.exp_one) in
-      let fresh_index_next = Exp.BinOp (Binop.PlusA, fresh_index, Sil.exp_one) in
+      let index_next = Exp.BinOp(Binop.PlusA, index, Exp.one) in
+      let fresh_index_next = Exp.BinOp (Binop.PlusA, fresh_index, Exp.one) in
       let map = [(index, fresh_index); (index_next, fresh_index_next)] in
       prop_replace_path_index p3 path map in
     Prop.normalize p4
@@ -545,7 +545,7 @@ let check_after_array_abstraction prop =
             check_se root (offs @ [Sil.Off_fld (f, typ)]) typ_f se) fsel in
   let check_hpred = function
     | Sil.Hpointsto (root, se, texp) ->
-        let typ = Sil.texp_to_typ (Some Typ.Tvoid) texp in
+        let typ = Exp.texp_to_typ (Some Typ.Tvoid) texp in
         check_se root [] typ se
     | Sil.Hlseg _ | Sil.Hdllseg _ -> () in
   let check_sigma sigma = IList.iter check_hpred sigma in
diff --git a/infer/src/backend/dom.ml b/infer/src/backend/dom.ml
index 3808a9f4e..e8a10d0ac 100644
--- a/infer/src/backend/dom.ml
+++ b/infer/src/backend/dom.ml
@@ -255,7 +255,7 @@ module CheckJoinPre : InfoLossCheckerSig = struct
     | Exp.Var id when Ident.is_normal id -> IList.length es >= 1
     | Exp.Var _ ->
         if Config.join_cond = 0 then
-          IList.exists (Exp.equal Sil.exp_zero) es
+          IList.exists (Exp.equal Exp.zero) es
         else if Dangling.check side e then
           begin
             let r = IList.exists (fun e' -> not (Dangling.check side_op e')) es in
@@ -457,7 +457,7 @@ end = struct
       let (_, _, e) = IList.find (fun (e1', e2', _) -> Exp.equal e1 e1' && Exp.equal e2 e2') !t in
       e
     with Not_found ->
-      let e = Sil.exp_get_undefined (JoinState.get_footprint ()) in
+      let e = Exp.get_undefined (JoinState.get_footprint ()) in
       t := (e1, e2, e)::!t;
       e
 
@@ -476,7 +476,7 @@ end = struct
       | Exp.Const (Const.Cint n1), Exp.Const (Const.Cint n1') -> IntLit.eq (n1 ++ n) n1'
       | _ -> false in
     let add_and_gen_eq e e' n =
-      let e_plus_n = Exp.BinOp(Binop.PlusA, e, Sil.exp_int n) in
+      let e_plus_n = Exp.BinOp(Binop.PlusA, e, Exp.int n) in
       Prop.mk_eq e_plus_n e' in
     let rec f_eqs_entry ((e1, e2, e) as entry) eqs_acc t_seen = function
       | [] -> eqs_acc, t_seen
@@ -502,8 +502,8 @@ end = struct
       | Exp.Const (Const.Cint n1), Exp.Const (Const.Cint n2) ->
           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
+          let e_strict_lower1 = Exp.int strict_lower1 in
+          let e_upper1 = Exp.int upper1 in
           get_induced_atom acc e_strict_lower1 e_upper1 e
       | _ -> acc in
     IList.fold_left f_ineqs eqs t_minimal
@@ -593,12 +593,12 @@ end = struct
     let f v = match v, side with
       | (Exp.BinOp (Binop.PlusA, e1', Exp.Const (Const.Cint i)), e2, e'), Lhs
         when Exp.equal e e1' ->
-          let c' = Sil.exp_int (IntLit.neg i) in
+          let c' = Exp.int (IntLit.neg i) in
           let v' = (e1', Exp.BinOp(Binop.PlusA, e2, c'), Exp.BinOp (Binop.PlusA, e', c')) in
           res := v'::!res
       | (e1, Exp.BinOp (Binop.PlusA, e2', Exp.Const (Const.Cint i)), e'), Rhs
         when Exp.equal e e2' ->
-          let c' = Sil.exp_int (IntLit.neg i) in
+          let c' = Exp.int (IntLit.neg i) in
           let v' = (Exp.BinOp(Binop.PlusA, e1, c'), e2', Exp.BinOp (Binop.PlusA, e', c')) in
           res := v'::!res
       | _ -> () in
@@ -930,13 +930,13 @@ let rec exp_partial_join (e1: Exp.t) (e2: Exp.t) : Exp.t =
   | Exp.BinOp(Binop.PlusA, Exp.Var id1, Exp.Const (Const.Cint c1)), Exp.Const (Const.Cint c2)
     when can_rename id1 ->
       let c2' = c2 -- c1 in
-      let e_res = Rename.extend (Exp.Var id1) (Sil.exp_int c2') Rename.ExtFresh in
-      Exp.BinOp(Binop.PlusA, e_res, Sil.exp_int c1)
+      let e_res = Rename.extend (Exp.Var id1) (Exp.int c2') Rename.ExtFresh in
+      Exp.BinOp(Binop.PlusA, e_res, Exp.int c1)
   | Exp.Const (Const.Cint c1), Exp.BinOp(Binop.PlusA, Exp.Var id2, Exp.Const (Const.Cint c2))
     when can_rename id2 ->
       let c1' = c1 -- c2 in
-      let e_res = Rename.extend (Sil.exp_int c1') (Exp.Var id2) Rename.ExtFresh in
-      Exp.BinOp(Binop.PlusA, e_res, Sil.exp_int c2)
+      let e_res = Rename.extend (Exp.int c1') (Exp.Var id2) Rename.ExtFresh in
+      Exp.BinOp(Binop.PlusA, e_res, Exp.int c2)
   | Exp.Cast(t1, e1), Exp.Cast(t2, e2) ->
       if not (Typ.equal t1 t2) then (L.d_strln "failure reason 22"; raise IList.Fail)
       else
@@ -1603,11 +1603,11 @@ let pi_partial_join mode
           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 (Exp.BinOp(Binop.Le, e, Sil.exp_int bound)) in
+        let a' = Prop.mk_inequality (Exp.BinOp(Binop.Le, e, Exp.int bound)) in
         Some a'
     | Some (e, _), [] ->
         let bound = widening_top in
-        let a' = Prop.mk_inequality (Exp.BinOp(Binop.Le, e, Sil.exp_int bound)) in
+        let a' = Prop.mk_inequality (Exp.BinOp(Binop.Le, e, Exp.int bound)) in
         Some a'
     | _ ->
         begin
@@ -1616,7 +1616,7 @@ let pi_partial_join mode
           | Some (n, e) ->
               let bound =
                 if IntLit.leq IntLit.minus_one n then IntLit.minus_one else widening_bottom in
-              let a' = Prop.mk_inequality (Exp.BinOp(Binop.Lt, Sil.exp_int bound, e)) in
+              let a' = Prop.mk_inequality (Exp.BinOp(Binop.Lt, Exp.int bound, e)) in
               Some a'
         end in
   let is_stronger_le e n a =
diff --git a/infer/src/backend/dotty.ml b/infer/src/backend/dotty.ml
index 73c5a7fdb..135550442 100644
--- a/infer/src/backend/dotty.ml
+++ b/infer/src/backend/dotty.ml
@@ -180,8 +180,8 @@ let is_source_node_of_exp e node =
 (* make sense for that case *)
 let get_coordinate_and_exp dotnode =
   match dotnode with
-  | Dotnil(coo) -> (coo, Sil.exp_minus_one)
-  | Dotarray (coo, _, _, _, _, _) -> (coo, Sil.exp_minus_one)
+  | Dotnil(coo) -> (coo, Exp.minus_one)
+  | Dotarray (coo, _, _, _, _, _) -> (coo, Exp.minus_one)
   | Dotpointsto (coo, b, _)
   | Dotlseg (coo, b, _, _, _, _)
   | Dotdllseg (coo, b, _, _, _, _, _, _)
@@ -246,19 +246,19 @@ let make_dangling_boxes pe allocated_nodes (sigma_lambda: (Sil.hpred * int) list
     let coo = mk_coordinate n lambda in
     (match hpred with
      | Sil.Hpointsto (_, Sil.Eexp (e, _), _)
-       when not (Exp.equal e Sil.exp_zero)  && !print_full_prop ->
+       when not (Exp.equal e Exp.zero)  && !print_full_prop ->
          let e_color_str = color_to_str (exp_color hpred e) in
          [Dotdangling(coo, e, e_color_str)]
-     | Sil.Hlseg (_, _, _, e2, _) when not (Exp.equal e2 Sil.exp_zero) ->
+     | Sil.Hlseg (_, _, _, e2, _) when not (Exp.equal e2 Exp.zero) ->
          let e2_color_str = color_to_str (exp_color hpred e2) in
          [Dotdangling(coo, e2, e2_color_str)]
      | Sil.Hdllseg (_, _, _, e2, e3, _, _) ->
          let e2_color_str = color_to_str (exp_color hpred e2) in
          let e3_color_str = color_to_str (exp_color hpred e3) in
-         let ll = if not (Exp.equal e2 Sil.exp_zero) then
+         let ll = if not (Exp.equal e2 Exp.zero) then
              [Dotdangling(coo, e2, e2_color_str)]
            else [] in
-         if not (Exp.equal e3 Sil.exp_zero) then Dotdangling(coo, e3, e3_color_str):: ll
+         if not (Exp.equal e3 Exp.zero) then Dotdangling(coo, e3, e3_color_str):: ll
          else ll
      | Sil.Hpointsto (_, _, _)
      | _ -> [] (* arrays and struct do not give danglings*)
@@ -377,7 +377,7 @@ let compute_struct_exp_nodes sigma =
 let get_node_exp n = snd (get_coordinate_and_exp n)
 
 let is_nil e prop =
-  (Exp.equal e Sil.exp_zero) || (Prover.check_equal prop e Sil.exp_zero)
+  (Exp.equal e Exp.zero) || (Prover.check_equal prop e Exp.zero)
 
 (* an edge is in cycle *)
 let in_cycle cycle edge =
@@ -1172,11 +1172,11 @@ let make_set_dangling_nodes allocated_nodes (sigma: Sil.hpred list) =
     VH_dangling(n, e) in
   let get_rhs_predicate hpred =
     (match hpred with
-     | Sil.Hpointsto (_, Sil.Eexp (e, _), _) when not (Exp.equal e Sil.exp_zero) -> [e]
-     | Sil.Hlseg (_, _, _, e2, _) when not (Exp.equal e2 Sil.exp_zero) -> [e2]
+     | Sil.Hpointsto (_, Sil.Eexp (e, _), _) when not (Exp.equal e Exp.zero) -> [e]
+     | Sil.Hlseg (_, _, _, e2, _) when not (Exp.equal e2 Exp.zero) -> [e2]
      | Sil.Hdllseg (_, _, _, e2, e3, _, _) ->
-         if (Exp.equal e2 Sil.exp_zero) then
-           if (Exp.equal e3 Sil.exp_zero) then []
+         if (Exp.equal e2 Exp.zero) then
+           if (Exp.equal e3 Exp.zero) then []
            else [e3]
          else [e2; e3]
      | Sil.Hpointsto (_, _, _)
diff --git a/infer/src/backend/interproc.ml b/infer/src/backend/interproc.ml
index ff861828e..ec74f919b 100644
--- a/infer/src/backend/interproc.ml
+++ b/infer/src/backend/interproc.ml
@@ -282,7 +282,7 @@ let propagate_nodes_divergence
         let mk_incons prop =
           let p_abs = Abs.abstract pname tenv prop in
           let p_zero = Prop.replace_sigma [] (Prop.replace_sub Sil.sub_empty p_abs) in
-          Prop.normalize (Prop.replace_pi [Sil.Aneq (Sil.exp_zero, Sil.exp_zero)] p_zero) in
+          Prop.normalize (Prop.replace_pi [Sil.Aneq (Exp.zero, Exp.zero)] p_zero) in
         Paths.PathSet.map mk_incons diverging_states in
       (L.d_strln_color Orange) "Propagating Divergence -- diverging states:";
       Propgraph.d_proplist Prop.prop_emp (Paths.PathSet.to_proplist prop_incons); L.d_ln ();
@@ -1120,7 +1120,7 @@ let remove_this_not_null prop =
     | hpred -> (var_option, hpred:: hpreds) in
   let collect_atom var atoms = function
     | Sil.Aneq (Exp.Var v, e)
-      when Ident.equal v var && Exp.equal e Sil.exp_null -> atoms
+      when Ident.equal v var && Exp.equal e Exp.null -> atoms
     | a -> a:: atoms in
   match IList.fold_left collect_hpred (None, []) (Prop.get_sigma prop) with
   | None, _ -> prop
diff --git a/infer/src/backend/modelBuiltins.ml b/infer/src/backend/modelBuiltins.ml
index 736665686..e978f1e6e 100644
--- a/infer/src/backend/modelBuiltins.ml
+++ b/infer/src/backend/modelBuiltins.ml
@@ -24,7 +24,7 @@ let execute___builtin_va_arg { Builtin.pdesc; tenv; prop_; path; ret_ids; args;
   : Builtin.ret_typ =
   match args, ret_ids with
   | [_; _; (lexp3, typ3)], _ ->
-      let instr' = Sil.Set (lexp3, typ3, Sil.exp_zero, loc) in
+      let instr' = Sil.Set (lexp3, typ3, Exp.zero, loc) in
       SymExec.instrs ~mask_errors:true tenv pdesc [instr'] [(prop_, path)]
   | _ -> raise (Exceptions.Wrong_argument_number __POS__)
 
@@ -179,7 +179,7 @@ let create_type tenv n_lexp typ prop =
           let prop''= Prop.normalize prop'' in
           prop''
       | None -> prop in
-  let sil_is_null = Exp.BinOp (Binop.Eq, n_lexp, Sil.exp_zero) in
+  let sil_is_null = Exp.BinOp (Binop.Eq, n_lexp, Exp.zero) in
   let sil_is_nonnull = Exp.UnOp (Unop.LNot, sil_is_null, None) in
   let null_case = Propset.to_proplist (prune ~positive:true sil_is_null prop) in
   let non_null_case = Propset.to_proplist (prune ~positive:true sil_is_nonnull prop_type) in
@@ -206,7 +206,7 @@ let execute___get_type_of { Builtin.pdesc; tenv; prop_; path; ret_ids; args; }
             | Sil.Hpointsto(_, _, texp) ->
                 (return_result texp prop ret_ids), path
             | _ -> assert false
-          with Not_found -> (return_result Sil.exp_zero prop ret_ids), path
+          with Not_found -> (return_result Exp.zero prop ret_ids), path
         end in
       (IList.map aux props)
   | _ -> raise (Exceptions.Wrong_argument_number __POS__)
@@ -247,8 +247,8 @@ let execute___instanceof_cast ~instof
         Tabulation.raise_cast_exception
           __POS__ None texp1 texp2 val1 in
       let exe_one_prop prop =
-        if Exp.equal texp2 Sil.exp_zero then
-          [(return_result Sil.exp_zero prop ret_ids, path)]
+        if Exp.equal texp2 Exp.zero then
+          [(return_result Exp.zero prop ret_ids, path)]
         else
           begin
             try
@@ -268,14 +268,14 @@ let execute___instanceof_cast ~instof
                         [(return_result res_e prop' ret_ids, path)] in
                   if instof then (* instanceof *)
                     begin
-                      let pos_res = mk_res pos_type_opt Sil.exp_one in
-                      let neg_res = mk_res neg_type_opt Sil.exp_zero in
+                      let pos_res = mk_res pos_type_opt Exp.one in
+                      let neg_res = mk_res neg_type_opt Exp.zero in
                       pos_res @ neg_res
                     end
                   else (* cast *)
                   if not should_throw_exception then (* C++ case when negative cast returns 0 *)
                     let pos_res = mk_res pos_type_opt val1 in
-                    let neg_res = mk_res neg_type_opt Sil.exp_zero in
+                    let neg_res = mk_res neg_type_opt Exp.zero in
                     pos_res @ neg_res
                   else
                     begin
@@ -799,7 +799,7 @@ let execute_alloc mk can_return_null
     Prop.add_or_replace_attribute prop' (Apred (Aresource ra, [exp_new])) in
   let prop_alloc = Prop.conjoin_eq (Exp.Var ret_id) exp_new prop_plus_ptsto in
   if can_return_null then
-    let prop_null = Prop.conjoin_eq (Exp.Var ret_id) Sil.exp_zero prop in
+    let prop_null = Prop.conjoin_eq (Exp.Var ret_id) Exp.zero prop in
     [(prop_alloc, path); (prop_null, path)]
   else [(prop_alloc, path)]
 
@@ -918,7 +918,7 @@ let execute___infer_assume { Builtin.prop_; path; args; }
   : Builtin.ret_typ =
   match args with
   | [(lexp, _)] ->
-      let prop_assume = Prop.conjoin_eq lexp (Sil.exp_bool true) prop_ in
+      let prop_assume = Prop.conjoin_eq lexp (Exp.bool true) prop_ in
       if Prover.check_inconsistency prop_assume
       then SymExec.diverge prop_assume path
       else [(prop_assume, path)]
diff --git a/infer/src/backend/prop.ml b/infer/src/backend/prop.ml
index e380530de..a56bf8056 100644
--- a/infer/src/backend/prop.ml
+++ b/infer/src/backend/prop.ml
@@ -471,13 +471,13 @@ let sym_eval abs e =
         begin
           match eval e1 with
           | Exp.Const (Const.Cint i) when IntLit.iszero i ->
-              Sil.exp_one
+              Exp.one
           | Exp.Const (Const.Cint _) ->
-              Sil.exp_zero
+              Exp.zero
           | Exp.UnOp(Unop.LNot, e1', _) ->
               e1'
           | e1' ->
-              if abs then Sil.exp_get_undefined false else Exp.UnOp(Unop.LNot, e1', topt)
+              if abs then Exp.get_undefined false else Exp.UnOp(Unop.LNot, e1', topt)
         end
     | Exp.UnOp (Unop.Neg, e1, topt) ->
         begin
@@ -485,13 +485,13 @@ let sym_eval abs e =
           | Exp.UnOp (Unop.Neg, e2', _) ->
               e2'
           | Exp.Const (Const.Cint i) ->
-              Sil.exp_int (IntLit.neg i)
+              Exp.int (IntLit.neg i)
           | Exp.Const (Const.Cfloat v) ->
-              Sil.exp_float (-. v)
+              Exp.float (-. v)
           | Exp.Var id ->
               Exp.UnOp (Unop.Neg, Exp.Var id, topt)
           | e1' ->
-              if abs then Sil.exp_get_undefined false else Exp.UnOp (Unop.Neg, e1', topt)
+              if abs then Exp.get_undefined false else Exp.UnOp (Unop.Neg, e1', topt)
         end
     | Exp.UnOp (Unop.BNot, e1, topt) ->
         begin
@@ -499,62 +499,62 @@ let sym_eval abs e =
           | Exp.UnOp(Unop.BNot, e2', _) ->
               e2'
           | Exp.Const (Const.Cint i) ->
-              Sil.exp_int (IntLit.lognot i)
+              Exp.int (IntLit.lognot i)
           | e1' ->
-              if abs then Sil.exp_get_undefined false else Exp.UnOp (Unop.BNot, e1', topt)
+              if abs then Exp.get_undefined false else Exp.UnOp (Unop.BNot, e1', topt)
         end
     | Exp.BinOp (Binop.Le, e1, e2) ->
         begin
           match eval e1, eval e2 with
           | Exp.Const (Const.Cint n), Exp.Const (Const.Cint m) ->
-              Sil.exp_bool (IntLit.leq n m)
+              Exp.bool (IntLit.leq n m)
           | Exp.Const (Const.Cfloat v), Exp.Const (Const.Cfloat w) ->
-              Sil.exp_bool (v <= w)
+              Exp.bool (v <= w)
           | Exp.BinOp (Binop.PlusA, e3, Exp.Const (Const.Cint n)), Exp.Const (Const.Cint m) ->
-              Exp.BinOp (Binop.Le, e3, Sil.exp_int (m -- n))
+              Exp.BinOp (Binop.Le, e3, Exp.int (m -- n))
           | e1', e2' ->
-              Sil.exp_le e1' e2'
+              Exp.le e1' e2'
         end
     | Exp.BinOp (Binop.Lt, e1, e2) ->
         begin
           match eval e1, eval e2 with
           | Exp.Const (Const.Cint n), Exp.Const (Const.Cint m) ->
-              Sil.exp_bool (IntLit.lt n m)
+              Exp.bool (IntLit.lt n m)
           | Exp.Const (Const.Cfloat v), Exp.Const (Const.Cfloat w) ->
-              Sil.exp_bool (v < w)
+              Exp.bool (v < w)
           | Exp.Const (Const.Cint n), Exp.BinOp (Binop.MinusA, f1, f2) ->
               Exp.BinOp
-                (Binop.Le, Exp.BinOp (Binop.MinusA, f2, f1), Sil.exp_int (IntLit.minus_one -- n))
+                (Binop.Le, Exp.BinOp (Binop.MinusA, f2, f1), Exp.int (IntLit.minus_one -- n))
           | Exp.BinOp(Binop.MinusA, f1 , f2), Exp.Const(Const.Cint n) ->
-              Sil.exp_le (Exp.BinOp(Binop.MinusA, f1 , f2)) (Sil.exp_int (n -- IntLit.one))
+              Exp.le (Exp.BinOp(Binop.MinusA, f1 , f2)) (Exp.int (n -- IntLit.one))
           | Exp.BinOp (Binop.PlusA, e3, Exp.Const (Const.Cint n)), Exp.Const (Const.Cint m) ->
-              Exp.BinOp (Binop.Lt, e3, Sil.exp_int (m -- n))
+              Exp.BinOp (Binop.Lt, e3, Exp.int (m -- n))
           | e1', e2' ->
-              Sil.exp_lt e1' e2'
+              Exp.lt e1' e2'
         end
     | Exp.BinOp (Binop.Ge, e1, e2) ->
-        eval (Sil.exp_le e2 e1)
+        eval (Exp.le e2 e1)
     | Exp.BinOp (Binop.Gt, e1, e2) ->
-        eval (Sil.exp_lt e2 e1)
+        eval (Exp.lt e2 e1)
     | Exp.BinOp (Binop.Eq, e1, e2) ->
         begin
           match eval e1, eval e2 with
           | Exp.Const (Const.Cint n), Exp.Const (Const.Cint m) ->
-              Sil.exp_bool (IntLit.eq n m)
+              Exp.bool (IntLit.eq n m)
           | Exp.Const (Const.Cfloat v), Exp.Const (Const.Cfloat w) ->
-              Sil.exp_bool (v = w)
+              Exp.bool (v = w)
           | e1', e2' ->
-              Sil.exp_eq e1' e2'
+              Exp.eq e1' e2'
         end
     | Exp.BinOp (Binop.Ne, e1, e2) ->
         begin
           match eval e1, eval e2 with
           | Exp.Const (Const.Cint n), Exp.Const (Const.Cint m) ->
-              Sil.exp_bool (IntLit.neq n m)
+              Exp.bool (IntLit.neq n m)
           | Exp.Const (Const.Cfloat v), Exp.Const (Const.Cfloat w) ->
-              Sil.exp_bool (v <> w)
+              Exp.bool (v <> w)
           | e1', e2' ->
-              Sil.exp_ne e1' e2'
+              Exp.ne e1' e2'
         end
     | Exp.BinOp (Binop.LAnd, e1, e2) ->
         let e1' = eval e1 in
@@ -627,9 +627,9 @@ let sym_eval abs e =
           | _, Exp.Const c when iszero_int_float c ->
               e1'
           | Exp.Const (Const.Cint n), Exp.Const (Const.Cint m) ->
-              Sil.exp_int (n ++ m)
+              Exp.int (n ++ m)
           | Exp.Const (Const.Cfloat v), Exp.Const (Const.Cfloat w) ->
-              Sil.exp_float (v +. w)
+              Exp.float (v +. w)
           | Exp.UnOp(Unop.Neg, f1, _), f2
           | f2, Exp.UnOp(Unop.Neg, f1, _) ->
               Exp.BinOp (ominus, f2, f1)
@@ -637,10 +637,10 @@ let sym_eval abs e =
           | Exp.BinOp (Binop.PlusPI, e, Exp.Const (Const.Cint n1)), Exp.Const (Const.Cint n2)
           | Exp.Const (Const.Cint n2), Exp.BinOp (Binop.PlusA, e, Exp.Const (Const.Cint n1))
           | Exp.Const (Const.Cint n2), Exp.BinOp (Binop.PlusPI, e, Exp.Const (Const.Cint n1)) ->
-              e +++ (Sil.exp_int (n1 ++ n2))
+              e +++ (Exp.int (n1 ++ n2))
           | Exp.BinOp (Binop.MinusA, Exp.Const (Const.Cint n1), e), Exp.Const (Const.Cint n2)
           | Exp.Const (Const.Cint n2), Exp.BinOp (Binop.MinusA, Exp.Const (Const.Cint n1), e) ->
-              Sil.exp_int (n1 ++ n2) --- e
+              Exp.int (n1 ++ n2) --- e
           | Exp.BinOp (Binop.MinusA, e1, e2), e3 -> (* (e1-e2)+e3 --> e1 + (e3-e2) *)
               (* progress: brings + to the outside *)
               eval (e1 +++ (e3 --- e2))
@@ -651,8 +651,8 @@ let sym_eval abs e =
           | Exp.Var _, Exp.Var _ ->
               e1' +++ e2'
           | _ ->
-              if abs && isPlusA then Sil.exp_get_undefined false else
-              if abs && not isPlusA then e1' +++ (Sil.exp_get_undefined false)
+              if abs && isPlusA then Exp.get_undefined false else
+              if abs && not isPlusA then e1' +++ (Exp.get_undefined false)
               else e1' +++ e2'
         end
     | Exp.BinOp (Binop.MinusA as ominus, e1, e2)
@@ -663,7 +663,7 @@ let sym_eval abs e =
         let oplus = if isMinusA then Binop.PlusA else Binop.PlusPI in
         let (+++) x y = Exp.BinOp (oplus, x, y) in
         let (---) x y = Exp.BinOp (ominus, x, y) in
-        if Exp.equal e1' e2' then Sil.exp_zero
+        if Exp.equal e1' e2' then Exp.zero
         else begin
           match e1', e2' with
           | Exp.Const c, _ when iszero_int_float c ->
@@ -671,22 +671,22 @@ let sym_eval abs e =
           | _, Exp.Const c when iszero_int_float c ->
               e1'
           | Exp.Const (Const.Cint n), Exp.Const (Const.Cint m) ->
-              Sil.exp_int (n -- m)
+              Exp.int (n -- m)
           | Exp.Const (Const.Cfloat v), Exp.Const (Const.Cfloat w) ->
-              Sil.exp_float (v -. w)
+              Exp.float (v -. w)
           | _, Exp.UnOp (Unop.Neg, f2, _) ->
               eval (e1 +++ f2)
           | _ , Exp.Const(Const.Cint n) ->
-              eval (e1' +++ (Sil.exp_int (IntLit.neg n)))
+              eval (e1' +++ (Exp.int (IntLit.neg n)))
           | Exp.Const _, _ ->
               e1' --- e2'
           | Exp.Var _, Exp.Var _ ->
               e1' --- e2'
           | _, _ ->
-              if abs then Sil.exp_get_undefined false else e1' --- e2'
+              if abs then Exp.get_undefined false else e1' --- e2'
         end
     | Exp.BinOp (Binop.MinusPP, e1, e2) ->
-        if abs then Sil.exp_get_undefined false
+        if abs then Exp.get_undefined false
         else Exp.BinOp (Binop.MinusPP, eval e1, eval e2)
     | Exp.BinOp (Binop.Mult, e1, e2) ->
         let e1' = eval e1 in
@@ -694,28 +694,28 @@ let sym_eval abs e =
         begin
           match e1', e2' with
           | Exp.Const c, _ when iszero_int_float c ->
-              Sil.exp_zero
+              Exp.zero
           | Exp.Const c, _ when isone_int_float c ->
               e2'
           | Exp.Const c, _ when isminusone_int_float c ->
               eval (Exp.UnOp (Unop.Neg, e2', None))
           | _, Exp.Const c when iszero_int_float c ->
-              Sil.exp_zero
+              Exp.zero
           | _, Exp.Const c when isone_int_float c ->
               e1'
           | _, Exp.Const c when isminusone_int_float c ->
               eval (Exp.UnOp (Unop.Neg, e1', None))
           | Exp.Const (Const.Cint n), Exp.Const (Const.Cint m) ->
-              Sil.exp_int (IntLit.mul n m)
+              Exp.int (IntLit.mul n m)
           | Exp.Const (Const.Cfloat v), Exp.Const (Const.Cfloat w) ->
-              Sil.exp_float (v *. w)
+              Exp.float (v *. w)
           | Exp.Var _, Exp.Var _ ->
               Exp.BinOp(Binop.Mult, e1', e2')
           | _, Exp.Sizeof _
           | Exp.Sizeof _, _ ->
               Exp.BinOp(Binop.Mult, e1', e2')
           | _, _ ->
-              if abs then Sil.exp_get_undefined false else Exp.BinOp(Binop.Mult, e1', e2')
+              if abs then Exp.get_undefined false else Exp.BinOp(Binop.Mult, e1', e2')
         end
     | Exp.BinOp (Binop.Div, e1, e2) ->
         let e1' = eval e1 in
@@ -723,15 +723,15 @@ let sym_eval abs e =
         begin
           match e1', e2' with
           | _, Exp.Const c when iszero_int_float c ->
-              Sil.exp_get_undefined false
+              Exp.get_undefined false
           | Exp.Const c, _ when iszero_int_float c ->
               e1'
           | _, Exp.Const c when isone_int_float c ->
               e1'
           | Exp.Const (Const.Cint n), Exp.Const (Const.Cint m) ->
-              Sil.exp_int (IntLit.div n m)
+              Exp.int (IntLit.div n m)
           | Exp.Const (Const.Cfloat v), Exp.Const (Const.Cfloat w) ->
-              Sil.exp_float (v /.w)
+              Exp.float (v /.w)
           | Exp.Sizeof (Typ.Tarray (elt, _), Some len, _), Exp.Sizeof (elt2, None, _)
             (* pattern: sizeof(elt[len]) / sizeof(elt) = len *)
             when Typ.equal elt elt2 ->
@@ -741,7 +741,7 @@ let sym_eval abs e =
             when Typ.equal elt elt2 ->
               Exp.Const (Const.Cint len)
           | _ ->
-              if abs then Sil.exp_get_undefined false else Exp.BinOp (Binop.Div, e1', e2')
+              if abs then Exp.get_undefined false else Exp.BinOp (Binop.Div, e1', e2')
         end
     | Exp.BinOp (Binop.Mod, e1, e2) ->
         let e1' = eval e1 in
@@ -749,20 +749,20 @@ let sym_eval abs e =
         begin
           match e1', e2' with
           | _, Exp.Const (Const.Cint i) when IntLit.iszero i ->
-              Sil.exp_get_undefined false
+              Exp.get_undefined false
           | Exp.Const (Const.Cint i), _ when IntLit.iszero i ->
               e1'
           | _, Exp.Const (Const.Cint i) when IntLit.isone i ->
-              Sil.exp_zero
+              Exp.zero
           | Exp.Const (Const.Cint n), Exp.Const (Const.Cint m) ->
-              Sil.exp_int (IntLit.rem n m)
+              Exp.int (IntLit.rem n m)
           | _ ->
-              if abs then Sil.exp_get_undefined false else Exp.BinOp (Binop.Mod, e1', e2')
+              if abs then Exp.get_undefined false else Exp.BinOp (Binop.Mod, e1', e2')
         end
     | Exp.BinOp (Binop.Shiftlt, e1, e2) ->
-        if abs then Sil.exp_get_undefined false else Exp.BinOp (Binop.Shiftlt, eval e1, eval e2)
+        if abs then Exp.get_undefined false else Exp.BinOp (Binop.Shiftlt, eval e1, eval e2)
     | Exp.BinOp (Binop.Shiftrt, e1, e2) ->
-        if abs then Sil.exp_get_undefined false else Exp.BinOp (Binop.Shiftrt, eval e1, eval e2)
+        if abs then Exp.get_undefined false else Exp.BinOp (Binop.Shiftrt, eval e1, eval e2)
     | Exp.BinOp (Binop.BAnd, e1, e2) ->
         let e1' = eval e1 in
         let e2' = eval e2 in
@@ -772,9 +772,9 @@ let sym_eval abs e =
           | _, Exp.Const (Const.Cint i) when IntLit.iszero i ->
               e2'
           | Exp.Const (Const.Cint i1), Exp.Const(Const.Cint i2) ->
-              Sil.exp_int (IntLit.logand i1 i2)
+              Exp.int (IntLit.logand i1 i2)
           | _ ->
-              if abs then Sil.exp_get_undefined false else Exp.BinOp (Binop.BAnd, e1', e2')
+              if abs then Exp.get_undefined false else Exp.BinOp (Binop.BAnd, e1', e2')
         end
     | Exp.BinOp (Binop.BOr, e1, e2) ->
         let e1' = eval e1 in
@@ -785,9 +785,9 @@ let sym_eval abs e =
           | _, Exp.Const (Const.Cint i) when IntLit.iszero i ->
               e1'
           | Exp.Const (Const.Cint i1), Exp.Const(Const.Cint i2) ->
-              Sil.exp_int (IntLit.logor i1 i2)
+              Exp.int (IntLit.logor i1 i2)
           | _ ->
-              if abs then Sil.exp_get_undefined false else Exp.BinOp (Binop.BOr, e1', e2')
+              if abs then Exp.get_undefined false else Exp.BinOp (Binop.BOr, e1', e2')
         end
     | Exp.BinOp (Binop.BXor, e1, e2) ->
         let e1' = eval e1 in
@@ -798,9 +798,9 @@ let sym_eval abs e =
           | _, Exp.Const (Const.Cint i) when IntLit.iszero i ->
               e1'
           | Exp.Const (Const.Cint i1), Exp.Const(Const.Cint i2) ->
-              Sil.exp_int (IntLit.logxor i1 i2)
+              Exp.int (IntLit.logxor i1 i2)
           | _ ->
-              if abs then Sil.exp_get_undefined false else Exp.BinOp (Binop.BXor, e1', e2')
+              if abs then Exp.get_undefined false else Exp.BinOp (Binop.BXor, e1', e2')
         end
     | Exp.BinOp (Binop.PtrFld, e1, e2) ->
         let e1' = eval e1 in
@@ -810,7 +810,7 @@ let sym_eval abs e =
           | Exp.Const (Const.Cptr_to_fld (fn, typ)) ->
               eval (Exp.Lfield(e1', fn, typ))
           | Exp.Const (Const.Cint i) when IntLit.iszero i ->
-              Sil.exp_zero (* cause a NULL dereference *)
+              Exp.zero (* cause a NULL dereference *)
           | _ -> Exp.BinOp (Binop.PtrFld, e1', e2')
         end
     | Exp.Exn _ ->
@@ -875,54 +875,54 @@ let mk_inequality e =
       let nbase = exp_normalize_noabs Sil.sub_empty base in
       (match nbase with
        | Exp.BinOp(Binop.PlusA, base', Exp.Const (Const.Cint n')) ->
-           let new_offset = Sil.exp_int (n -- n') in
+           let new_offset = Exp.int (n -- n') in
            let new_e = Exp.BinOp (Binop.Le, base', new_offset) in
-           Sil.Aeq (new_e, Sil.exp_one)
+           Sil.Aeq (new_e, Exp.one)
        | Exp.BinOp(Binop.PlusA, Exp.Const (Const.Cint n'), base') ->
-           let new_offset = Sil.exp_int (n -- n') in
+           let new_offset = Exp.int (n -- n') in
            let new_e = Exp.BinOp (Binop.Le, base', new_offset) in
-           Sil.Aeq (new_e, Sil.exp_one)
+           Sil.Aeq (new_e, Exp.one)
        | Exp.BinOp(Binop.MinusA, base', Exp.Const (Const.Cint n')) ->
-           let new_offset = Sil.exp_int (n ++ n') in
+           let new_offset = Exp.int (n ++ n') in
            let new_e = Exp.BinOp (Binop.Le, base', new_offset) in
-           Sil.Aeq (new_e, Sil.exp_one)
+           Sil.Aeq (new_e, Exp.one)
        | Exp.BinOp(Binop.MinusA, Exp.Const (Const.Cint n'), base') ->
-           let new_offset = Sil.exp_int (n' -- n -- IntLit.one) in
+           let new_offset = Exp.int (n' -- n -- IntLit.one) in
            let new_e = Exp.BinOp (Binop.Lt, new_offset, base') in
-           Sil.Aeq (new_e, Sil.exp_one)
+           Sil.Aeq (new_e, Exp.one)
        | Exp.UnOp(Unop.Neg, new_base, _) ->
            (* In this case, base = -new_base. Construct -n-1 < new_base. *)
-           let new_offset = Sil.exp_int (IntLit.zero -- n -- IntLit.one) in
+           let new_offset = Exp.int (IntLit.zero -- n -- IntLit.one) in
            let new_e = Exp.BinOp (Binop.Lt, new_offset, new_base) in
-           Sil.Aeq (new_e, Sil.exp_one)
-       | _ -> Sil.Aeq (e, Sil.exp_one))
+           Sil.Aeq (new_e, Exp.one)
+       | _ -> Sil.Aeq (e, Exp.one))
   | Exp.BinOp (Binop.Lt, Exp.Const (Const.Cint n), base) ->
       (* n < base case *)
       let nbase = exp_normalize_noabs Sil.sub_empty base in
       (match nbase with
        | Exp.BinOp(Binop.PlusA, base', Exp.Const (Const.Cint n')) ->
-           let new_offset = Sil.exp_int (n -- n') in
+           let new_offset = Exp.int (n -- n') in
            let new_e = Exp.BinOp (Binop.Lt, new_offset, base') in
-           Sil.Aeq (new_e, Sil.exp_one)
+           Sil.Aeq (new_e, Exp.one)
        | Exp.BinOp(Binop.PlusA, Exp.Const (Const.Cint n'), base') ->
-           let new_offset = Sil.exp_int (n -- n') in
+           let new_offset = Exp.int (n -- n') in
            let new_e = Exp.BinOp (Binop.Lt, new_offset, base') in
-           Sil.Aeq (new_e, Sil.exp_one)
+           Sil.Aeq (new_e, Exp.one)
        | Exp.BinOp(Binop.MinusA, base', Exp.Const (Const.Cint n')) ->
-           let new_offset = Sil.exp_int (n ++ n') in
+           let new_offset = Exp.int (n ++ n') in
            let new_e = Exp.BinOp (Binop.Lt, new_offset, base') in
-           Sil.Aeq (new_e, Sil.exp_one)
+           Sil.Aeq (new_e, Exp.one)
        | Exp.BinOp(Binop.MinusA, Exp.Const (Const.Cint n'), base') ->
-           let new_offset = Sil.exp_int (n' -- n -- IntLit.one) in
+           let new_offset = Exp.int (n' -- n -- IntLit.one) in
            let new_e = Exp.BinOp (Binop.Le, base', new_offset) in
-           Sil.Aeq (new_e, Sil.exp_one)
+           Sil.Aeq (new_e, Exp.one)
        | Exp.UnOp(Unop.Neg, new_base, _) ->
            (* In this case, base = -new_base. Construct new_base <= -n-1 *)
-           let new_offset = Sil.exp_int (IntLit.zero -- n -- IntLit.one) in
+           let new_offset = Exp.int (IntLit.zero -- n -- IntLit.one) in
            let new_e = Exp.BinOp (Binop.Le, new_base, new_offset) in
-           Sil.Aeq (new_e, Sil.exp_one)
-       | _ -> Sil.Aeq (e, Sil.exp_one))
-  | _ -> Sil.Aeq (e, Sil.exp_one)
+           Sil.Aeq (new_e, Exp.one)
+       | _ -> Sil.Aeq (e, Exp.one))
+  | _ -> Sil.Aeq (e, Exp.one)
 
 (** Normalize an inequality *)
 let inequality_normalize a =
@@ -964,12 +964,12 @@ let inequality_normalize a =
     | e:: el -> Exp.BinOp(Binop.PlusA, e, exp_list_to_sum el) in
   let norm_from_exp e =
     match normalize_posnegoff (exp_to_posnegoff e) with
-    | [],[], n -> Exp.BinOp(Binop.Le, Sil.exp_int n, Sil.exp_zero)
-    | [], neg, n -> Exp.BinOp(Binop.Lt, Sil.exp_int (n -- IntLit.one), exp_list_to_sum neg)
-    | pos, [], n -> Exp.BinOp(Binop.Le, exp_list_to_sum pos, Sil.exp_int (IntLit.zero -- n))
+    | [],[], n -> Exp.BinOp(Binop.Le, Exp.int n, Exp.zero)
+    | [], neg, n -> Exp.BinOp(Binop.Lt, Exp.int (n -- IntLit.one), exp_list_to_sum neg)
+    | pos, [], n -> Exp.BinOp(Binop.Le, exp_list_to_sum pos, Exp.int (IntLit.zero -- n))
     | pos, neg, n ->
         let lhs_e = Exp.BinOp(Binop.MinusA, exp_list_to_sum pos, exp_list_to_sum neg) in
-        Exp.BinOp(Binop.Le, lhs_e, Sil.exp_int (IntLit.zero -- n)) in
+        Exp.BinOp(Binop.Le, lhs_e, Exp.int (IntLit.zero -- n)) in
   let ineq = match a with
     | Sil.Aeq (ineq, Exp.Const (Const.Cint i)) when IntLit.isone i ->
         ineq
@@ -979,7 +979,7 @@ let inequality_normalize a =
       let e = Exp.BinOp(Binop.MinusA, e1, e2) in
       mk_inequality (norm_from_exp e)
   | Exp.BinOp(Binop.Lt, e1, e2) ->
-      let e = Exp.BinOp(Binop.MinusA, Exp.BinOp(Binop.MinusA, e1, e2), Sil.exp_minus_one) in
+      let e = Exp.BinOp(Binop.MinusA, Exp.BinOp(Binop.MinusA, e1, e2), Exp.minus_one) in
       mk_inequality (norm_from_exp e)
   | _ -> a
 
@@ -994,14 +994,14 @@ let atom_normalize sub a0 =
     | Exp.BinOp(Binop.PlusA, e1, Exp.Const (Const.Cint n1)), Exp.Const (Const.Cint n2)
     (* e1+n1==n2 ---> e1==n2-n1 *)
     | Exp.BinOp(Binop.PlusPI, e1, Exp.Const (Const.Cint n1)), Exp.Const (Const.Cint n2) ->
-        (e1, Sil.exp_int (n2 -- n1))
+        (e1, Exp.int (n2 -- n1))
     | Exp.BinOp(Binop.MinusA, e1, Exp.Const (Const.Cint n1)), Exp.Const (Const.Cint n2)
     (* e1-n1==n2 ---> e1==n1+n2 *)
     | Exp.BinOp(Binop.MinusPI, e1, Exp.Const (Const.Cint n1)), Exp.Const (Const.Cint n2) ->
-        (e1, Sil.exp_int (n1 ++ n2))
+        (e1, Exp.int (n1 ++ n2))
     | Exp.BinOp(Binop.MinusA, Exp.Const (Const.Cint n1), e1), Exp.Const (Const.Cint n2) ->
         (* n1-e1 == n2 -> e1==n1-n2 *)
-        (e1, Sil.exp_int (n1 -- n2))
+        (e1, Exp.int (n1 -- n2))
     | Exp.Lfield (e1', fld1, _), Exp.Lfield (e2', fld2, _) ->
         if Ident.fieldname_equal fld1 fld2
         then normalize_eq (e1', e2')
@@ -1015,7 +1015,7 @@ let atom_normalize sub a0 =
     match e1, e2 with
     | Exp.UnOp (Unop.LNot, e1', _), Exp.Const (Const.Cint i)
     | Exp.Const (Const.Cint i), Exp.UnOp (Unop.LNot, e1', _) when IntLit.iszero i ->
-        (e1', Sil.exp_zero, true)
+        (e1', Exp.zero, true)
     | _ -> (e1, e2, false) in
   let handle_boolean_operation from_equality e1 e2 =
     let ne1 = exp_normalize sub e1 in
@@ -1043,9 +1043,9 @@ let atom_normalize sub a0 =
 (** Negate an atom *)
 let atom_negate = function
   | Sil.Aeq (Exp.BinOp (Binop.Le, e1, e2), Exp.Const (Const.Cint i)) when IntLit.isone i ->
-      mk_inequality (Sil.exp_lt e2 e1)
+      mk_inequality (Exp.lt e2 e1)
   | Sil.Aeq (Exp.BinOp (Binop.Lt, e1, e2), Exp.Const (Const.Cint i)) when IntLit.isone i ->
-      mk_inequality (Sil.exp_le e2 e1)
+      mk_inequality (Exp.le e2 e1)
   | Sil.Aeq (e1, e2) -> Sil.Aneq (e1, e2)
   | Sil.Aneq (e1, e2) -> Sil.Aeq (e1, e2)
   | Sil.Apred (a, es) -> Sil.Anpred (a, es)
@@ -1093,7 +1093,7 @@ let rec create_strexp_of_type tenvo struct_init_mode typ len inst =
     then
       match typ with
       | Typ.Tfloat _ -> Exp.Const (Const.Cfloat 0.0)
-      | _ -> Sil.exp_zero
+      | _ -> Exp.zero
     else
       create_fresh_var () in
   match typ, len with
@@ -1108,7 +1108,7 @@ let rec create_strexp_of_type tenvo struct_init_mode typ len inst =
              field, but always return None so that only the last field receives len *)
           let f (fld, t, a) (flds, len) =
             if Typ.is_objc_ref_counter_field (fld, t, a) then
-              ((fld, Sil.Eexp (Sil.exp_one, inst)) :: flds, None)
+              ((fld, Sil.Eexp (Exp.one, inst)) :: flds, None)
             else
               ((fld, create_strexp_of_type tenvo struct_init_mode t len inst) :: flds, None) in
           let flds, _ = IList.fold_right f instance_fields ([], len) in
@@ -1116,7 +1116,7 @@ let rec create_strexp_of_type tenvo struct_init_mode typ len inst =
     )
   | Typ.Tarray (_, len_opt), None ->
       let len = match len_opt with
-        | None -> Sil.exp_get_undefined false
+        | None -> Exp.get_undefined false
         | Some len -> Exp.Const (Const.Cint len) in
       Sil.Earray (len, [], inst)
   | Typ.Tarray _, Some len ->
@@ -1249,11 +1249,11 @@ let pi_tighten_ineq pi =
   let ineq_list' =
     let le_ineq_list =
       IList.map
-        (fun (e, n) -> mk_inequality (Exp.BinOp(Binop.Le, e, Sil.exp_int n)))
+        (fun (e, n) -> mk_inequality (Exp.BinOp(Binop.Le, e, Exp.int n)))
         le_list_tightened in
     let lt_ineq_list =
       IList.map
-        (fun (n, e) -> mk_inequality (Exp.BinOp(Binop.Lt, Sil.exp_int n, e)))
+        (fun (n, e) -> mk_inequality (Exp.BinOp(Binop.Lt, Exp.int n, e)))
         lt_list_tightened in
     le_ineq_list @ lt_ineq_list in
   let nonineq_list' =
@@ -1380,7 +1380,7 @@ let exp_normalize_prop prop exp =
   Config.run_with_abs_val_equal_zero (exp_normalize prop.sub) exp
 
 let lexp_normalize_prop p lexp =
-  let root = Sil.root_of_lexp lexp in
+  let root = Exp.root_of_lexp lexp in
   let offsets = Sil.exp_get_offsets lexp in
   let nroot = exp_normalize_prop p root in
   let noffsets =
@@ -1642,13 +1642,13 @@ let sigma_remove_emptylseg sigma =
     | Sil.Hpointsto _ as hpred :: sigma' ->
         f eqs_zero (hpred :: sigma_passed) sigma'
     | Sil.Hlseg (Sil.Lseg_PE, _, e1, e2, _) :: sigma'
-      when (Exp.equal e1 Sil.exp_zero) || (Exp.Set.mem e1 alloc_set) ->
+      when (Exp.equal e1 Exp.zero) || (Exp.Set.mem e1 alloc_set) ->
         f (Sil.Aeq(e1, e2) :: eqs_zero) sigma_passed sigma'
     | Sil.Hlseg _ as hpred :: sigma' ->
         f eqs_zero (hpred :: sigma_passed) sigma'
     | Sil.Hdllseg (Sil.Lseg_PE, _, iF, oB, oF, iB, _) :: sigma'
-      when (Exp.equal iF Sil.exp_zero) || (Exp.Set.mem iF alloc_set)
-           || (Exp.equal iB Sil.exp_zero) || (Exp.Set.mem iB alloc_set) ->
+      when (Exp.equal iF Exp.zero) || (Exp.Set.mem iF alloc_set)
+           || (Exp.equal iB Exp.zero) || (Exp.Set.mem iB alloc_set) ->
         f (Sil.Aeq(iF, oF):: Sil.Aeq(iB, oB):: eqs_zero) sigma_passed sigma'
     | Sil.Hdllseg _ as hpred :: sigma' ->
         f eqs_zero (hpred :: sigma_passed) sigma'
@@ -1683,14 +1683,14 @@ let normalize_and_strengthen_atom (p : normal t) (a : Sil.atom) : Sil.atom =
   match a' with
   | Sil.Aeq (Exp.BinOp (Binop.Le, Exp.Var id, Exp.Const (Const.Cint n)), Exp.Const (Const.Cint i))
     when IntLit.isone i ->
-      let lower = Sil.exp_int (n -- IntLit.one) in
-      let a_lower = Sil.Aeq (Exp.BinOp (Binop.Lt, lower, Exp.Var id), Sil.exp_one) in
+      let lower = Exp.int (n -- IntLit.one) in
+      let a_lower = Sil.Aeq (Exp.BinOp (Binop.Lt, lower, Exp.Var id), Exp.one) in
       if not (IList.mem Sil.atom_equal a_lower p.pi) then a'
-      else Sil.Aeq (Exp.Var id, Sil.exp_int n)
+      else Sil.Aeq (Exp.Var id, Exp.int n)
   | Sil.Aeq (Exp.BinOp (Binop.Lt, Exp.Const (Const.Cint n), Exp.Var id), Exp.Const (Const.Cint i))
     when IntLit.isone i ->
-      let upper = Sil.exp_int (n ++ IntLit.one) in
-      let a_upper = Sil.Aeq (Exp.BinOp (Binop.Le, Exp.Var id, upper), Sil.exp_one) in
+      let upper = Exp.int (n ++ IntLit.one) in
+      let a_upper = Sil.Aeq (Exp.BinOp (Binop.Le, Exp.Var id, upper), Exp.one) in
       if not (IList.mem Sil.atom_equal a_upper p.pi) then a'
       else Sil.Aeq (Exp.Var id, upper)
   | Sil.Aeq (Exp.BinOp (Binop.Ne, e1, e2), Exp.Const (Const.Cint i)) when IntLit.isone i ->
@@ -1924,7 +1924,7 @@ let replace_objc_null prop lhs_exp rhs_exp =
   match get_objc_null_attribute prop rhs_exp, rhs_exp with
   | Some atom, Exp.Var _ ->
       let prop = remove_attribute_from_exp prop atom in
-      let prop = conjoin_eq rhs_exp Sil.exp_zero prop in
+      let prop = conjoin_eq rhs_exp Exp.zero prop in
       let natom = Sil.atom_replace_exp [(rhs_exp, lhs_exp)] atom in
       add_or_replace_attribute prop natom
   | _ -> prop
@@ -1940,7 +1940,7 @@ let rec nullify_exp_with_objc_null prop exp =
       (match get_objc_null_attribute prop exp with
        | Some atom ->
            let prop' = remove_attribute_from_exp prop atom in
-           conjoin_eq exp Sil.exp_zero prop'
+           conjoin_eq exp Exp.zero prop'
        | _ -> prop)
   | _ -> prop
 
@@ -2194,7 +2194,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 = Exp.Var (Ident.create_fresh Ident.kprimed) in
-    let offset_new = Sil.exp_int (IntLit.neg offset) in
+    let offset_new = Exp.int (IntLit.neg offset) in
     let exp_new = Exp.BinOp(Binop.PlusA, base_new, offset_new) in
     (id, exp_new) in
   let reindexing = IList.map transform list_passed in
@@ -2794,7 +2794,7 @@ let trans_land_lor op ((idl1, stml1), e1) ((idl2, stml2), e2) loc =
           | Binop.LOr -> Exp.UnOp(Unop.LNot, e1, None), e1, IntLit.one
           | _ -> assert false in
         let cond_res1 = Exp.BinOp(Binop.Eq, Exp.Var id, e2) in
-        let cond_res2 = Exp.BinOp(Binop.Eq, Exp.Var id, Sil.exp_int res) in
+        let cond_res2 = Exp.BinOp(Binop.Eq, Exp.Var id, Exp.int res) in
         let mk_prune cond =
           (* don't report always true/false *)
           Sil.Prune (cond, loc, true, Sil.Ik_land_lor) in
diff --git a/infer/src/backend/prover.ml b/infer/src/backend/prover.ml
index f8d9df7e8..be087e1a1 100644
--- a/infer/src/backend/prover.ml
+++ b/infer/src/backend/prover.ml
@@ -72,9 +72,9 @@ end = struct
   let equal entry1 entry2 = compare entry1 entry2 = 0
 
   let to_leq (e1, e2, n) =
-    Exp.BinOp(Binop.MinusA, e1, e2), Sil.exp_int n
+    Exp.BinOp(Binop.MinusA, e1, e2), Exp.int n
   let to_lt (e1, e2, n) =
-    Sil.exp_int (IntLit.zero -- n -- IntLit.one), Exp.BinOp(Binop.MinusA, e2, e1)
+    Exp.int (IntLit.zero -- n -- IntLit.one), Exp.BinOp(Binop.MinusA, e2, e1)
   let to_triple entry = entry
 
   let from_leq acc (e1, e2) =
@@ -253,7 +253,7 @@ end = struct
     mutable neqs: (Exp.t * Exp.t) list; (** ne facts [e1 != e2] *)
   }
 
-  let inconsistent_ineq = { leqs = [(Sil.exp_one, Sil.exp_zero)]; lts = []; neqs = [] }
+  let inconsistent_ineq = { leqs = [(Exp.one, Exp.zero)]; lts = []; neqs = [] }
 
   let leq_compare (e1, e2) (f1, f2) =
     let c1 = Exp.compare e1 f1 in
@@ -336,7 +336,7 @@ end = struct
         let umap = umap_create_from_leqs Exp.Map.empty leqs in
         let umap' = umap_improve_by_difference_constraints umap diff_constraints2 in
         let leqs' = Exp.Map.fold
-            (fun e upper acc_leqs -> (e, Sil.exp_int upper):: acc_leqs)
+            (fun e upper acc_leqs -> (e, Exp.int upper):: acc_leqs)
             umap' [] in
         let leqs'' = (IList.map DiffConstr.to_leq diff_constraints2) @ leqs' in
         leqs_sort_then_remove_redundancy leqs'' in
@@ -344,7 +344,7 @@ end = struct
         let lmap = lmap_create_from_lts Exp.Map.empty lts in
         let lmap' = lmap_improve_by_difference_constraints lmap diff_constraints2 in
         let lts' = Exp.Map.fold
-            (fun e lower acc_lts -> (Sil.exp_int lower, e):: acc_lts)
+            (fun e lower acc_lts -> (Exp.int lower, e):: acc_lts)
             lmap' [] in
         let lts'' = (IList.map DiffConstr.to_lt diff_constraints2) @ lts' in
         lts_sort_then_remove_redundancy lts'' in
@@ -372,7 +372,7 @@ end = struct
     let leqs = ref [] in
     let lts = ref [] in
     let add_lt_minus1_e e =
-      lts := (Sil.exp_minus_one, e)::!lts in
+      lts := (Exp.minus_one, e)::!lts in
     let texp_is_unsigned = function
       | Exp.Sizeof (Typ.Tint ik, _, _) -> Typ.ikind_is_unsigned ik
       | _ -> false in
@@ -545,7 +545,7 @@ let check_equal prop e1 e2 =
 
 (** Check [ |- e=0]. Result [false] means "don't know". *)
 let check_zero e =
-  check_equal Prop.prop_emp e Sil.exp_zero
+  check_equal Prop.prop_emp e Exp.zero
 
 (** [is_root prop base_exp exp] checks whether [base_exp =
     exp.offlist] for some list of offsets [offlist]. If so, it returns
@@ -631,7 +631,7 @@ let check_disequal prop e1 e2 =
                if (k == Sil.Lseg_NE || check_pi_implies_disequal e1 e2) then
                  let sigma_irrelevant' = (IList.rev sigma_irrelevant) @ sigma_rest
                  in Some (true, sigma_irrelevant')
-               else if (Exp.equal e2 Sil.exp_zero) then
+               else if (Exp.equal e2 Exp.zero) then
                  let sigma_irrelevant' = (IList.rev sigma_irrelevant) @ sigma_rest
                  in Some (false, sigma_irrelevant')
                else
@@ -653,14 +653,14 @@ let check_disequal prop e1 e2 =
                if (check_pi_implies_disequal iF oF) then
                  let sigma_irrelevant' = (IList.rev sigma_irrelevant) @ sigma_rest
                  in Some (true, sigma_irrelevant')
-               else if (Exp.equal oF Sil.exp_zero) then
+               else if (Exp.equal oF Exp.zero) then
                  let sigma_irrelevant' = (IList.rev sigma_irrelevant) @ sigma_rest
                  in Some (false, sigma_irrelevant')
                else
                  let sigma_rest' = (IList.rev sigma_irrelevant) @ sigma_rest
                  in f [] oF sigma_rest') in
     let f_null_check sigma_irrelevant e sigma_rest =
-      if not (Exp.equal e Sil.exp_zero) then f sigma_irrelevant e sigma_rest
+      if not (Exp.equal e Exp.zero) then f sigma_irrelevant e sigma_rest
       else
         let sigma_irrelevant' = (IList.rev sigma_irrelevant) @ sigma_rest
         in Some (false, sigma_irrelevant')
@@ -680,7 +680,7 @@ let check_le_normalized prop e1 e2 =
   let eL, eR, off = match e1, e2 with
     | Exp.BinOp(Binop.MinusA, f1, f2), Exp.Const (Const.Cint n) ->
         if Exp.equal f1 f2
-        then Sil.exp_zero, Sil.exp_zero, n
+        then Exp.zero, Exp.zero, n
         else f1, f2, n
     | _ ->
         e1, e2, IntLit.zero in
@@ -827,7 +827,7 @@ let check_inconsistency_base prop =
   let pi = Prop.get_pi prop in
   let sigma = Prop.get_sigma prop in
   let inconsistent_ptsto _ =
-    check_allocatedness prop Sil.exp_zero in
+    check_allocatedness prop Exp.zero in
   let inconsistent_this_self_var () =
     let procdesc =
       Cfg.Node.get_proc_desc (State.get_node ()) in
@@ -845,7 +845,7 @@ let check_inconsistency_base prop =
       procedure_attr.ProcAttributes.is_cpp_instance_method in
     let do_hpred = function
       | Sil.Hpointsto (Exp.Lvar pv, Sil.Eexp (e, _), _) ->
-          Exp.equal e Sil.exp_zero &&
+          Exp.equal e Exp.zero &&
           Pvar.is_seed pv &&
           (is_java_this pv || is_cpp_this pv || is_objc_instance_self pv)
       | _ -> false in
@@ -1174,7 +1174,7 @@ let exp_imply calc_missing subs e1_in e2_in : subst2 =
     | Exp.Const (Const.Cint _), Exp.BinOp (Binop.PlusPI, _, _) ->
         raise (IMPL_EXC ("pointer+index cannot evaluate to a constant", subs, (EXC_FALSE_EXPS (e1, e2))))
     | Exp.Const (Const.Cint n1), Exp.BinOp (Binop.PlusA, f1, Exp.Const (Const.Cint n2)) ->
-        do_imply subs (Sil.exp_int (n1 -- n2)) f1
+        do_imply subs (Exp.int (n1 -- n2)) f1
     | Exp.BinOp(op1, e1, f1), Exp.BinOp(op2, e2, f2) when op1 == op2 ->
         do_imply (do_imply subs e1 e2) f1 f2
     | Exp.BinOp (Binop.PlusA, Exp.Var v1, e1), e2 ->
@@ -1286,10 +1286,10 @@ let rec sexp_imply source calc_index_frame calc_missing subs se1 se2 typ2 : subs
       sexp_imply source calc_index_frame calc_missing subs (Sil.Estruct (fsel', inst')) se2 typ2
   | Sil.Eexp _, Sil.Earray (len, _, inst)
   | Sil.Estruct _, Sil.Earray (len, _, inst) ->
-      let se1' = Sil.Earray (len, [(Sil.exp_zero, se1)], inst) in
+      let se1' = Sil.Earray (len, [(Exp.zero, se1)], inst) in
       sexp_imply source calc_index_frame calc_missing subs se1' se2 typ2
   | Sil.Earray (len, _, _), Sil.Eexp (_, inst) ->
-      let se2' = Sil.Earray (len, [(Sil.exp_zero, se2)], inst) in
+      let se2' = Sil.Earray (len, [(Exp.zero, se2)], inst) in
       let typ2' = Typ.Tarray (typ2, None) in
       (* In the sexp_imply, struct_imply, array_imply, and sexp_imply_nolhs functions, the typ2
          argument is only used by eventually passing its value to Typ.struct_typ_fld, Exp.Lfield,
@@ -1468,7 +1468,7 @@ let expand_hpred_pointer calc_index_frame hpred : bool * bool * Sil.hpred =
           | _ -> raise (Failure "expand_hpred_pointer: Unexpected non-sizeof type in Lindex") in
         let len = match t' with
           | Exp.Sizeof (_, Some len, _) -> len
-          | _ -> Sil.exp_get_undefined false in
+          | _ -> Exp.get_undefined false in
         let hpred' = Sil.Hpointsto (e, Sil.Earray (len, [(ind, se)], Sil.inst_none), t') in
         expand true true hpred'
     | Sil.Hpointsto (Exp.BinOp (Binop.PlusPI, e1, e2), Sil.Earray (len, esel, inst), t) ->
@@ -1713,7 +1713,7 @@ let texp_imply tenv subs texp1 texp2 e1 calc_missing =
     of length given by its type only active in type_size mode *)
 let sexp_imply_preprocess se1 texp1 se2 = match se1, texp1, se2 with
   | Sil.Eexp (_, inst), Exp.Sizeof _, Sil.Earray _ when Config.type_size ->
-      let se1' = Sil.Earray (texp1, [(Sil.exp_zero, se1)], inst) in
+      let se1' = Sil.Earray (texp1, [(Exp.zero, se1)], inst) in
       L.d_strln_color Orange "sexp_imply_preprocess"; L.d_str " se1: "; Sil.d_sexp se1; L.d_ln (); L.d_str " se1': "; Sil.d_sexp se1'; L.d_ln ();
       se1'
   | _ -> se1
@@ -1780,7 +1780,7 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2
                 (match Prop.prop_iter_current iter1' with
                  | Sil.Hpointsto (e1, se1, texp1), _ ->
                      (try
-                        let typ2 = Sil.texp_to_typ (Some Typ.Tvoid) texp2 in
+                        let typ2 = Exp.texp_to_typ (Some Typ.Tvoid) texp2 in
                         let typing_frame, typing_missing = texp_imply tenv subs texp1 texp2 e1 calc_missing in
                         let se1' = sexp_imply_preprocess se1 texp1 se2 in
                         let subs', fld_frame, fld_missing = sexp_imply e1 calc_index_frame calc_missing subs se1' se2 typ2 in
@@ -1970,11 +1970,11 @@ and sigma_imply tenv calc_index_frame calc_missing subs prop1 sigma2 : (subst2 *
     let len = IntLit.of_int (1 + String.length s) in
     let root = Exp.Const (Const.Cstr s) in
     let sexp =
-      let index = Sil.exp_int (IntLit.of_int (String.length s)) in
+      let index = Exp.int (IntLit.of_int (String.length s)) in
       match !Config.curr_language with
       | Config.Clang ->
           Sil.Earray
-            (Sil.exp_int len, [(index, Sil.Eexp (Sil.exp_zero, Sil.inst_none))], Sil.inst_none)
+            (Exp.int len, [(index, Sil.Eexp (Exp.zero, Sil.inst_none))], Sil.inst_none)
       | Config.Java ->
           let mk_fld_sexp s =
             let fld = Ident.create_fieldname (Mangled.from_string s) 0 in
@@ -2040,7 +2040,7 @@ and sigma_imply tenv calc_index_frame calc_missing subs prop1 sigma2 : (subst2 *
                  | None ->
                      let subs' = match hpred2' with
                        | Sil.Hpointsto (e2, se2, te2) ->
-                           let typ2 = Sil.texp_to_typ (Some Typ.Tvoid) te2 in
+                           let typ2 = Exp.texp_to_typ (Some Typ.Tvoid) te2 in
                            sexp_imply_nolhs e2 calc_missing subs se2 typ2
                        | _ -> subs in
                      ProverState.add_missing_sigma [hpred2'];
@@ -2139,7 +2139,7 @@ let check_array_bounds (sub1, sub2) prop =
         (* L.d_strln_color Orange "check_bound ";
            Sil.d_exp len1; L.d_str " "; Sil.d_exp len2; L.d_ln(); *)
         let indices_to_check = match len2 with
-          | _ -> [Exp.BinOp(Binop.PlusA, len2, Sil.exp_minus_one)] (* only check len *) in
+          | _ -> [Exp.BinOp(Binop.PlusA, len2, Exp.minus_one)] (* only check len *) in
         IList.iter (fail_if_le len1) indices_to_check
     | ProverState.BCfrom_pre _atom ->
         let atom_neg = Prop.atom_negate (Sil.atom_sub sub2 _atom) in
diff --git a/infer/src/backend/rearrange.ml b/infer/src/backend/rearrange.ml
index d46222401..60871ae99 100644
--- a/infer/src/backend/rearrange.ml
+++ b/infer/src/backend/rearrange.ml
@@ -38,12 +38,12 @@ let check_bad_index pname p len index loc =
     | _ -> false in
   let index_provably_out_of_bound () =
     let index_too_large = Prop.mk_inequality (Exp.BinOp (Binop.Le, len, index)) in
-    let index_negative = Prop.mk_inequality (Exp.BinOp (Binop.Le, index, Sil.exp_minus_one)) in
+    let index_negative = Prop.mk_inequality (Exp.BinOp (Binop.Le, index, Exp.minus_one)) in
     (Prover.check_atom p index_too_large) || (Prover.check_atom p index_negative) in
   let index_provably_in_bound () =
-    let len_minus_one = Exp.BinOp(Binop.PlusA, len, Sil.exp_minus_one) in
+    let len_minus_one = Exp.BinOp(Binop.PlusA, len, Exp.minus_one) in
     let index_not_too_large = Prop.mk_inequality (Exp.BinOp(Binop.Le, index, len_minus_one)) in
-    let index_nonnegative = Prop.mk_inequality (Exp.BinOp(Binop.Le, Sil.exp_zero, index)) in
+    let index_nonnegative = Prop.mk_inequality (Exp.BinOp(Binop.Le, Exp.zero, index)) in
     Prover.check_zero index || (* index 0 always in bound, even when we know nothing about len *)
     ((Prover.check_atom p index_not_too_large) && (Prover.check_atom p index_nonnegative)) in
   let index_has_bounds () =
@@ -199,11 +199,11 @@ let rec _strexp_extend_values
   | [], Sil.Estruct _, _ ->
       [([], se, typ)]
   | [], Sil.Earray _, _ ->
-      let off_new = Sil.Off_index(Sil.exp_zero):: off in
+      let off_new = Sil.Off_index(Exp.zero):: off in
       _strexp_extend_values
         pname tenv orig_prop footprint_part kind max_stamp se typ off_new inst
   | (Sil.Off_fld _) :: _, Sil.Earray _, Typ.Tarray _ ->
-      let off_new = Sil.Off_index(Sil.exp_zero):: off in
+      let off_new = Sil.Off_index(Exp.zero):: off in
       _strexp_extend_values
         pname tenv orig_prop footprint_part kind max_stamp se typ off_new inst
   | (Sil.Off_fld (f, _)):: off', Sil.Estruct (fsel, inst'),
@@ -253,11 +253,11 @@ let rec _strexp_extend_values
   | (Sil.Off_index _):: _, Sil.Estruct _, Typ.Tstruct _ ->
       (* L.d_strln_color Orange "turn into an array"; *)
       let len = match se with
-        | Sil.Eexp (_, Sil.Ialloc) -> Sil.exp_one (* if allocated explicitly, we know len is 1 *)
+        | Sil.Eexp (_, Sil.Ialloc) -> Exp.one (* if allocated explicitly, we know len is 1 *)
         | _ ->
-            if Config.type_size then Sil.exp_one (* Exp.Sizeof (typ, Subtype.exact) *)
+            if Config.type_size then Exp.one (* Exp.Sizeof (typ, Subtype.exact) *)
             else Exp.Var (new_id ()) in
-      let se_new = Sil.Earray (len, [(Sil.exp_zero, se)], inst) in
+      let se_new = Sil.Earray (len, [(Exp.zero, se)], inst) in
       let typ_new = Typ.Tarray (typ, None) in
       _strexp_extend_values
         pname tenv orig_prop footprint_part kind max_stamp se_new typ_new off inst
@@ -384,7 +384,7 @@ let laundry_offset_for_footprint max_stamp offs_in =
 let strexp_extend_values
     pname tenv orig_prop footprint_part kind max_stamp
     se te (off : Sil.offset list) inst =
-  let typ = Sil.texp_to_typ None te in
+  let typ = Exp.texp_to_typ None te in
   let off', laundry_atoms =
     let off', eqs = laundry_offset_for_footprint max_stamp off in
     (* do laundry_offset whether footprint_part is true or not, so max_stamp is modified anyway *)
@@ -410,7 +410,7 @@ let strexp_extend_values
     atoms_se_typ_list_filtered
 
 let collect_root_offset exp =
-  let root = Sil.root_of_lexp exp in
+  let root = Exp.root_of_lexp exp in
   let offsets = Sil.exp_get_offsets exp in
   (root, offsets)
 
@@ -854,7 +854,7 @@ let rearrange_arith lexp prop =
   end;
   if (Config.array_level >= 2) then raise ARRAY_ACCESS
   else
-    let root = Sil.root_of_lexp lexp in
+    let root = Exp.root_of_lexp lexp in
     if Prover.check_allocatedness prop root then
       raise ARRAY_ACCESS
     else
@@ -1103,7 +1103,7 @@ let rec iter_rearrange
     if !Config.footprint then
       prop_iter_add_hpred_footprint pname tenv prop iter' (lexp, typ) inst
     else
-    if (Config.array_level >= 1 && not !Config.footprint && Sil.exp_pointer_arith lexp)
+    if (Config.array_level >= 1 && not !Config.footprint && Exp.pointer_arith lexp)
     then rearrange_arith lexp prop
     else begin
       pp_rearrangement_error "cannot find predicate with root" prop lexp;
@@ -1225,10 +1225,10 @@ let check_dereference_error pdesc (prop : Prop.normal Prop.t) lexp loc =
          | _ -> true)
       (Prop.get_sigma prop) &&
     !nullable_obj_str <> None in
-  let root = Sil.root_of_lexp lexp in
+  let root = Exp.root_of_lexp lexp in
   let is_deref_of_nullable =
     let is_definitely_non_null exp prop =
-      Prover.check_disequal prop exp Sil.exp_zero in
+      Prover.check_disequal prop exp Exp.zero in
     Config.report_nullable_inconsistency && not (is_definitely_non_null root prop)
     && is_only_pt_by_nullable_fld_or_param root in
   let relevant_attributes_getters = [
@@ -1249,7 +1249,7 @@ let check_dereference_error pdesc (prop : Prop.normal Prop.t) lexp loc =
           | Exp.BinOp((Binop.PlusPI | Binop.PlusA | Binop.MinusPI | Binop.MinusA), base, _) -> base
           | _ -> root in
         get_relevant_attributes root_no_offset in
-  if Prover.check_zero (Sil.root_of_lexp root) || is_deref_of_nullable then
+  if Prover.check_zero (Exp.root_of_lexp root) || is_deref_of_nullable then
     begin
       let deref_str =
         if is_deref_of_nullable then
@@ -1287,7 +1287,7 @@ let check_dereference_error pdesc (prop : Prop.normal Prop.t) lexp loc =
       let err_desc = Errdesc.explain_dereference ~use_buckets: true deref_str prop loc in
       raise (Exceptions.Use_after_free (err_desc, __POS__))
   | _ ->
-      if Prover.check_equal Prop.prop_emp (Sil.root_of_lexp root) Sil.exp_minus_one then
+      if Prover.check_equal Prop.prop_emp (Exp.root_of_lexp root) Exp.minus_one then
         let deref_str = Localise.deref_str_dangling None in
         let err_desc = Errdesc.explain_dereference deref_str prop loc in
         raise (Exceptions.Dangling_pointer_dereference (None, err_desc, __POS__))
@@ -1296,7 +1296,7 @@ let check_dereference_error pdesc (prop : Prop.normal Prop.t) lexp loc =
 (* It's used to check that we don't call possibly null blocks *)
 let check_call_to_objc_block_error pdesc prop fun_exp loc =
   let fun_exp_may_be_null () = (* may be null if we don't know if it is definitely not null *)
-    not (Prover.check_disequal prop (Sil.root_of_lexp fun_exp) Sil.exp_zero) in
+    not (Prover.check_disequal prop (Exp.root_of_lexp fun_exp) Exp.zero) in
   let try_explaining_exp e = (* when e is a temp var, try to find the pvar defining e*)
     match e with
     | Exp.Var id ->
@@ -1366,7 +1366,7 @@ let rearrange ?(report_deref_errors=true) pdesc tenv lexp typ prop loc
         Exp.Lindex(ep, e)
     | e -> e in
   let ptr_tested_for_zero =
-    Prover.check_disequal prop (Sil.root_of_lexp nlexp) Sil.exp_zero in
+    Prover.check_disequal prop (Exp.root_of_lexp nlexp) Exp.zero in
   let inst = Sil.inst_rearrange (not ptr_tested_for_zero) loc (State.get_path_pos ()) in
   L.d_strln ".... Rearrangement Start ....";
   L.d_str "Exp: "; Sil.d_exp nlexp; L.d_ln ();
diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml
index d8abd7e53..788aef6ab 100644
--- a/infer/src/backend/symExec.ml
+++ b/infer/src/backend/symExec.ml
@@ -131,11 +131,11 @@ let rec apply_offlist
           (f None, Prop.create_strexp_of_type (Some tenv) Prop.Fld_init typ None inst, typ, None)
         end
   | [], Sil.Earray _ ->
-      let offlist' = (Sil.Off_index Sil.exp_zero):: offlist in
+      let offlist' = (Sil.Off_index Exp.zero):: offlist in
       apply_offlist
         pdesc tenv p fp_root nullify_struct (root_lexp, strexp, typ) offlist' f inst lookup_inst
   | (Sil.Off_fld _):: _, Sil.Earray _ ->
-      let offlist_new = Sil.Off_index(Sil.exp_zero) :: offlist in
+      let offlist_new = Sil.Off_index(Exp.zero) :: offlist in
       apply_offlist
         pdesc tenv p fp_root nullify_struct (root_lexp, strexp, typ) offlist_new f inst lookup_inst
   | (Sil.Off_fld (fld, fld_typ)):: offlist', Sil.Estruct (fsel, inst') ->
@@ -262,7 +262,7 @@ let update_iter iter pi sigma =
     that could mean nonempty heaps. *)
 let rec execute_nullify_se = function
   | Sil.Eexp _ ->
-      Sil.Eexp (Sil.exp_zero, Sil.inst_nullify)
+      Sil.Eexp (Exp.zero, Sil.inst_nullify)
   | Sil.Estruct (fsel, _) ->
       let fsel' = IList.map (fun (fld, se) -> (fld, execute_nullify_se se)) fsel in
       Sil.Estruct (fsel', Sil.inst_nullify)
@@ -309,13 +309,13 @@ let prune_ineq ~is_strict ~positive prop e1 e2 =
     if is_inconsistent then Propset.empty
     else
       let footprint = !Config.footprint in
-      let prop_with_ineq = Prop.conjoin_eq ~footprint prune_cond Sil.exp_one prop in
+      let prop_with_ineq = Prop.conjoin_eq ~footprint prune_cond Exp.one prop in
       Propset.singleton prop_with_ineq
 
 let rec prune ~positive condition prop =
   match condition with
   | Exp.Var _ | Exp.Lvar _ ->
-      prune_ne ~positive condition Sil.exp_zero prop
+      prune_ne ~positive condition Exp.zero prop
   | Exp.Const (Const.Cint i) when IntLit.iszero i ->
       if positive then Propset.empty else Propset.singleton prop
   | Exp.Const (Const.Cint _ | Const.Cstr _ | Const.Cclass _) | Exp.Sizeof _ ->
@@ -351,7 +351,7 @@ let rec prune ~positive condition prop =
       let pruner = if positive then prune_union else prune_inter in
       pruner ~positive condition1 condition2 prop
   | Exp.BinOp _ | Exp.Lfield _ | Exp.Lindex _ ->
-      prune_ne ~positive condition Sil.exp_zero prop
+      prune_ne ~positive condition Exp.zero prop
   | Exp.Exn _ ->
       assert false
   | Exp.Closure _ ->
@@ -401,7 +401,7 @@ let call_should_be_skipped callee_pname summary =
 let check_constant_string_dereference lexp =
   let string_lookup s n =
     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
+    Exp.int (IntLit.of_int c) in
   match lexp with
   | Exp.BinOp(Binop.PlusPI, Exp.Const (Const.Cstr s), e)
   | Exp.Lindex (Exp.Const (Const.Cstr s), e) ->
@@ -410,7 +410,7 @@ let check_constant_string_dereference lexp =
           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
+        | _ -> Exp.get_undefined false in
       Some value
   | Exp.Const (Const.Cstr s) ->
       Some (string_lookup s IntLit.zero)
@@ -730,7 +730,7 @@ let handle_objc_instance_method_call_or_skip actual_pars path callee_pname pre r
   let is_receiver_null =
     match actual_pars with
     | (e, _) :: _
-      when Exp.equal e Sil.exp_zero ||
+      when Exp.equal e Exp.zero ||
            Option.is_some (Prop.get_objc_null_attribute pre e) -> true
     | _ -> false in
   let add_objc_null_attribute_or_nullify_result prop =
@@ -740,7 +740,7 @@ let handle_objc_instance_method_call_or_skip actual_pars path callee_pname pre r
         | Some vfs ->
             Prop.add_or_replace_attribute prop (Apred (Aobjc_null, [Exp.Var ret_id; vfs]))
         | None ->
-            Prop.conjoin_eq (Exp.Var ret_id) Sil.exp_zero prop
+            Prop.conjoin_eq (Exp.Var ret_id) Exp.zero prop
       )
     | _ -> prop in
   if is_receiver_null then
@@ -760,7 +760,7 @@ let handle_objc_instance_method_call_or_skip actual_pars path callee_pname pre r
     if !Config.footprint && not is_undef then
       let res_null = (* returns: (objc_null(res) /\ receiver=0) or an empty list of results *)
         let pre_with_attr_or_null = add_objc_null_attribute_or_nullify_result pre in
-        let propset = prune_ne ~positive:false receiver Sil.exp_zero pre_with_attr_or_null in
+        let propset = prune_ne ~positive:false receiver Exp.zero pre_with_attr_or_null in
         if Propset.is_empty propset then []
         else
           let prop = IList.hd (Propset.to_proplist propset) in
@@ -840,7 +840,7 @@ let add_constraints_on_retval pdesc prop ret_exp ~has_nullable_annot typ callee_
         prop (* don't assume nonnull if the procedure is annotated with @Nullable *)
       else
         match typ with
-        | Typ.Tptr _ -> Prop.conjoin_neq exp Sil.exp_zero prop
+        | Typ.Tptr _ -> Prop.conjoin_neq exp Exp.zero prop
         | _ -> prop in
     let add_tainted_post ret_exp callee_pname prop =
       Prop.add_or_replace_attribute prop (Apred (Ataint callee_pname, [ret_exp])) in
@@ -953,7 +953,7 @@ let execute_letderef ?(report_deref_errors=true) pname pdesc tenv id rhs_exp typ
   with Rearrange.ARRAY_ACCESS ->
     if (Config.array_level = 0) then assert false
     else
-      let undef = Sil.exp_get_undefined false in
+      let undef = Exp.get_undefined false in
       [Prop.conjoin_eq (Exp.Var id) undef prop_]
 
 let load_ret_annots pname =
diff --git a/infer/src/backend/tabulation.ml b/infer/src/backend/tabulation.ml
index 4e4e6ea70..d4ccca21b 100644
--- a/infer/src/backend/tabulation.ml
+++ b/infer/src/backend/tabulation.ml
@@ -298,7 +298,7 @@ let check_dereferences callee_pname actual_pre sub spec_pre formal_params =
       L.d_strln (" desc: " ^ (pp_to_string Localise.pp_error_desc error_desc));
       error_desc in
     let deref_no_null_check_pos =
-      if Exp.equal e_sub Sil.exp_zero then
+      if Exp.equal e_sub Exp.zero then
         match find_dereference_without_null_check_in_sexp sexp with
         | Some (_, pos) -> Some pos
         | None -> None
@@ -315,7 +315,7 @@ let check_dereferences callee_pname actual_pre sub spec_pre formal_params =
       (* In that case it raise a dangling pointer dereferece *)
     if Prop.has_dangling_uninit_attribute spec_pre e then
       Some (Deref_undef_exp, desc false (Localise.deref_str_dangling (Some Sil.DAuninit)) )
-    else if Exp.equal e_sub Sil.exp_minus_one
+    else if Exp.equal e_sub Exp.minus_one
     then Some (Deref_minusone, desc true (Localise.deref_str_dangling None))
     else match Prop.get_resource_attribute actual_pre e_sub with
       | Some (Apred (Aresource ({ ra_kind = Rrelease } as ra), _)) ->
@@ -327,7 +327,7 @@ let check_dereferences callee_pname actual_pre sub spec_pre formal_params =
            | _ -> None) in
   let check_hpred = function
     | Sil.Hpointsto (lexp, se, _) ->
-        check_dereference (Sil.root_of_lexp lexp) se
+        check_dereference (Exp.root_of_lexp lexp) se
     | _ -> None in
   let deref_err_list = IList.fold_left (fun deref_errs hpred -> match check_hpred hpred with
       | Some reason -> reason :: deref_errs
@@ -449,7 +449,7 @@ and sexp_star_fld se1 se2 : Sil.strexp =
   | Sil.Earray (len1, esel1, _), Sil.Earray (_, esel2, inst2) ->
       Sil.Earray (len1, esel_star_fld esel1 esel2, inst2)
   | Sil.Eexp (_, inst1), Sil.Earray (len2, esel2, _) ->
-      let esel1 = [(Sil.exp_zero, se1)] in
+      let esel1 = [(Exp.zero, se1)] in
       Sil.Earray (len2, esel_star_fld esel1 esel2, inst1)
   | _ ->
       L.d_str "cannot star ";
@@ -678,7 +678,7 @@ let combine
       if !Config.footprint && posts = []
       then (* in case of divergence, produce a prop *)
         (* with updated footprint and inconsistent current *)
-        [(Prop.replace_pi [Sil.Aneq (Sil.exp_zero, Sil.exp_zero)] Prop.prop_emp, path_pre)]
+        [(Prop.replace_pi [Sil.Aneq (Exp.zero, Exp.zero)] Prop.prop_emp, path_pre)]
       else
         IList.map
           (fun (p, path_post) ->
@@ -885,7 +885,7 @@ let mk_posts ret_ids prop callee_pname callee_attrs posts =
           IList.exists
             (function
               | Sil.Apred (Aretval (pname, _), [exp]) when Procname.equal callee_pname pname ->
-                  Prover.check_disequal prop exp Sil.exp_zero
+                  Prover.check_disequal prop exp Exp.zero
               | _ -> false)
             (Prop.get_all_attributes prop) in
         if last_call_ret_non_null then
@@ -893,7 +893,7 @@ let mk_posts ret_ids prop callee_pname callee_attrs posts =
             IList.exists
               (function
                 | Sil.Hpointsto (Exp.Lvar pvar, Sil.Eexp (e, _), _) when Pvar.is_return pvar ->
-                    Prover.check_equal (Prop.normalize prop) e Sil.exp_zero
+                    Prover.check_equal (Prop.normalize prop) e Exp.zero
                 | _ -> false)
               (Prop.get_sigma prop) in
           IList.filter (fun (prop, _) -> not (returns_null prop)) posts
@@ -1321,7 +1321,7 @@ let check_splitting_precondition sub1 sub2 =
 let sigma_has_null_pointer sigma =
   let hpred_null_pointer = function
     | Sil.Hpointsto (e, _, _) ->
-        Exp.equal e Sil.exp_zero
+        Exp.equal e Exp.zero
     | _ -> false in
   IList.exists hpred_null_pointer sigma
 *)
diff --git a/infer/src/checkers/annotationReachability.ml b/infer/src/checkers/annotationReachability.ml
index 8af5b2231..1a8a9b357 100644
--- a/infer/src/checkers/annotationReachability.ml
+++ b/infer/src/checkers/annotationReachability.ml
@@ -294,10 +294,10 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
   let prunes_tracking_var astate = function
     | Exp.BinOp (Binop.Eq, lhs, rhs)
       when is_tracking_exp astate lhs ->
-        Exp.equal rhs Sil.exp_one
+        Exp.equal rhs Exp.one
     | Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.Eq, lhs, rhs), _)
       when is_tracking_exp astate lhs ->
-        Exp.equal rhs Sil.exp_zero
+        Exp.equal rhs Exp.zero
     | _ ->
         false
 
diff --git a/infer/src/checkers/checkers.ml b/infer/src/checkers/checkers.ml
index 7ed432d86..1024f7a1f 100644
--- a/infer/src/checkers/checkers.ml
+++ b/infer/src/checkers/checkers.ml
@@ -199,7 +199,7 @@ let callback_check_write_to_parcel_java
   let is_write_to_parcel this_expr this_type =
     let method_match () =
       Procname.java_get_method pname_java = "writeToParcel" in
-    let expr_match () = Sil.exp_is_this this_expr in
+    let expr_match () = Exp.is_this this_expr in
     let type_match () =
       let class_name =
         Typename.TN_csu (Csu.Class Csu.Java, Mangled.from_string "android.os.Parcelable") in
diff --git a/infer/src/checkers/codeQuery.ml b/infer/src/checkers/codeQuery.ml
index 5c3a45ab6..0b57d0e94 100644
--- a/infer/src/checkers/codeQuery.ml
+++ b/infer/src/checkers/codeQuery.ml
@@ -98,7 +98,7 @@ module Match = struct
     Hashtbl.iter pp_item env
 
   let exp_match env ae value = match ae, value with
-    | CodeQueryAst.Null, Vval e -> Exp.equal e Sil.exp_zero
+    | CodeQueryAst.Null, Vval e -> Exp.equal e Exp.zero
     | CodeQueryAst.Null, _ -> false
     | CodeQueryAst.ConstString s, (Vfun pn) -> string_contains s (Procname.to_string pn)
     | CodeQueryAst.ConstString _, _ -> false
diff --git a/infer/src/checkers/liveness.ml b/infer/src/checkers/liveness.ml
index 43345d9ec..0af3e9883 100644
--- a/infer/src/checkers/liveness.ml
+++ b/infer/src/checkers/liveness.ml
@@ -25,7 +25,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
 
   (* add all of the vars read in [exp] to the live set *)
   let exp_add_live exp astate =
-    let (ids, pvars) = Sil.exp_get_vars exp in
+    let (ids, pvars) = Exp.get_vars exp in
     let astate' =
       IList.fold_left (fun astate_acc id -> Domain.add (Var.of_id id) astate_acc) astate ids in
     IList.fold_left (fun astate_acc pvar -> Domain.add (Var.of_pvar pvar) astate_acc) astate' pvars
diff --git a/infer/src/checkers/patternMatch.ml b/infer/src/checkers/patternMatch.ml
index b9a56b962..5e4aab2eb 100644
--- a/infer/src/checkers/patternMatch.ml
+++ b/infer/src/checkers/patternMatch.ml
@@ -388,9 +388,9 @@ let get_fields_nullified procdesc =
   (* walk through the instructions and look for instance fields that are assigned to null *)
   let collect_nullified_flds (nullified_flds, this_ids) _ = function
     | Sil.Set (Exp.Lfield (Exp.Var lhs, fld, _), _, rhs, _)
-      when Sil.exp_is_null_literal rhs && Ident.IdentSet.mem lhs this_ids ->
+      when Exp.is_null_literal rhs && Ident.IdentSet.mem lhs this_ids ->
         (Ident.FieldSet.add fld nullified_flds, this_ids)
-    | Sil.Letderef (id, rhs, _, _) when Sil.exp_is_this rhs ->
+    | Sil.Letderef (id, rhs, _, _) when Exp.is_this rhs ->
         (nullified_flds, Ident.IdentSet.add id this_ids)
     | _ -> (nullified_flds, this_ids) in
   let (nullified_flds, _) =
diff --git a/infer/src/clang/cArithmetic_trans.ml b/infer/src/clang/cArithmetic_trans.ml
index e75251729..31348515d 100644
--- a/infer/src/clang/cArithmetic_trans.ml
+++ b/infer/src/clang/cArithmetic_trans.ml
@@ -134,7 +134,7 @@ let binary_operation_instruction context boi e1 typ e2 loc rhs_owning_method =
       Printing.log_stats
         "\nWARNING: Missing translation for Binary Operator Kind %s. Construct ignored...\n"
         (Clang_ast_j.string_of_binary_operator_kind bok);
-      (Sil.exp_minus_one, [])
+      (Exp.minus_one, [])
 
 let unary_operation_instruction uoi e typ loc =
   let uok = Clang_ast_j.string_of_unary_operator_kind (uoi.Clang_ast_t.uoi_kind) in
diff --git a/infer/src/clang/cTrans.ml b/infer/src/clang/cTrans.ml
index 01a3cf65f..7e8f41165 100644
--- a/infer/src/clang/cTrans.ml
+++ b/infer/src/clang/cTrans.ml
@@ -347,7 +347,7 @@ struct
 
   let nullPtrExpr_trans trans_state expr_info =
     let typ = CTypes_decl.get_type_from_expr_info expr_info trans_state.context.CContext.tenv in
-    { empty_res_trans with exps = [(Sil.exp_null, typ)]}
+    { empty_res_trans with exps = [(Exp.null, typ)]}
 
   let objCSelectorExpr_trans trans_state expr_info selector =
     stringLiteral_trans trans_state expr_info selector
@@ -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 (IntLit.of_int64 i) in
+        let exp = Exp.int (IntLit.of_int64 i) in
         exp
       with
       | Failure _ ->
@@ -432,7 +432,7 @@ struct
              "\nWARNING: Missing translation of Uniry_Expression_Or_Trait of kind: \
               %s . Expression ignored, returned -1... \n"
              (Clang_ast_j.string_of_unary_expr_or_type_trait_kind k);
-        { empty_res_trans with exps =[(Sil.exp_minus_one, typ)]}
+        { empty_res_trans with exps =[(Exp.minus_one, typ)]}
 
   (* search the label into the hashtbl - create a fake node eventually *)
   (* connect that node with this stmt *)
@@ -1610,7 +1610,7 @@ struct
           (* in initd_exps, then we assume that all the indices were initialized and *)
           (* we don't need any assignments. *)
           if IList.exists
-              ((fun arr index -> Sil.exp_is_array_index_of index arr) var_exp)
+              ((fun arr index -> Exp.is_array_index_of index arr) var_exp)
               initd_exps
           then []
           else IList.map2 assign_instr lh rh_exps in
@@ -2566,7 +2566,7 @@ struct
         implicitValueInitExpr_trans trans_state expr_info
     | GenericSelectionExpr _ (* to be fixed when we dump the right info in the ast *)
     | SizeOfPackExpr _ ->
-        { empty_res_trans with exps = [(Sil.exp_get_undefined false, Typ.Tvoid)] }
+        { empty_res_trans with exps = [(Exp.get_undefined false, Typ.Tvoid)] }
 
     | GCCAsmStmt (stmt_info, stmts) ->
         gccAsmStmt_trans trans_state stmt_info stmts
diff --git a/infer/src/clang/cTrans_utils.ml b/infer/src/clang/cTrans_utils.ml
index f30276833..e22fa17c7 100644
--- a/infer/src/clang/cTrans_utils.ml
+++ b/infer/src/clang/cTrans_utils.ml
@@ -24,7 +24,7 @@ let extract_item_from_singleton l warning_string failure_val =
   | [item] -> item
   | _ -> Printing.log_err "%s" warning_string; failure_val
 
-let dummy_exp = (Sil.exp_minus_one, Typ.Tint Typ.IInt)
+let dummy_exp = (Exp.minus_one, Typ.Tint Typ.IInt)
 
 (* Extract the element of a singleton list. If the list is not a singleton *)
 (* Gives a warning and return -1 as standard value indicating something    *)
@@ -61,9 +61,9 @@ struct
         "\nWARNING: Missing expression for Conditional operator. Need to be fixed" in
     let e_cond'' =
       if branch then
-        Exp.BinOp(Binop.Ne, e_cond', Sil.exp_zero)
+        Exp.BinOp(Binop.Ne, e_cond', Exp.zero)
       else
-        Exp.BinOp(Binop.Eq, e_cond', Sil.exp_zero) in
+        Exp.BinOp(Binop.Eq, e_cond', Exp.zero) in
     let instrs_cond'= instrs_cond @ [Sil.Prune(e_cond'', loc, branch, ik)] in
     create_node (prune_kind branch) instrs_cond' loc context
 
@@ -449,7 +449,7 @@ let trans_assertion_failure sil_loc context =
   { empty_res_trans with root_nodes = [failure_node]; }
 
 let trans_assume_false sil_loc context succ_nodes =
-  let instrs_cond = [Sil.Prune (Sil.exp_zero, sil_loc, true, Sil.Ik_land_lor)] in
+  let instrs_cond = [Sil.Prune (Exp.zero, sil_loc, true, Sil.Ik_land_lor)] in
   let prune_node = Nodes.create_node (Nodes.prune_kind true) instrs_cond sil_loc context in
   Cfg.Node.set_succs_exn context.CContext.cfg prune_node succ_nodes [];
   { empty_res_trans with root_nodes = [prune_node]; leaf_nodes = [prune_node] }
diff --git a/infer/src/eradicate/typeCheck.ml b/infer/src/eradicate/typeCheck.ml
index aa958a13f..56ac3315e 100644
--- a/infer/src/eradicate/typeCheck.ml
+++ b/infer/src/eradicate/typeCheck.ml
@@ -354,7 +354,7 @@ let typecheck_instr
           Pvar.is_global pvar in
 
         let pvar_to_str pvar =
-          if Sil.exp_is_this (Exp.Lvar pvar) then ""
+          if Exp.is_this (Exp.Lvar pvar) then ""
           else Pvar.to_string pvar ^ "_" in
 
         let res = match exp' with
@@ -651,7 +651,7 @@ let typecheck_instr
                 not (TypeAnnotation.origin_is_fun_library ta) in
               if checks.eradicate && should_report then
                 begin
-                  let cond = Exp.BinOp (Binop.Ne, Exp.Lvar pvar, Sil.exp_null) in
+                  let cond = Exp.BinOp (Binop.Ne, Exp.Lvar pvar, Exp.null) in
                   EradicateChecks.report_error
                     find_canonical_duplicate
                     node
diff --git a/infer/src/java/jTrans.ml b/infer/src/java/jTrans.ml
index d8aa690a5..54583670a 100644
--- a/infer/src/java/jTrans.ml
+++ b/infer/src/java/jTrans.ml
@@ -525,7 +525,7 @@ let rec expression context pc expr =
       then
         (* assume that reading from C.$assertionsDisabled always yields "false". this allows *)
         (* Infer to understand the assert keyword in the expected way *)
-        (instrs, Sil.exp_zero, type_of_expr)
+        (instrs, Exp.zero, type_of_expr)
       else
         let sil_expr = Exp.Lfield (sil_expr, field_name, sil_type) in
         let tmp_id = Ident.create_fresh Ident.knormal in
@@ -761,7 +761,7 @@ let is_this expr =
 let assume_not_null loc sil_expr =
   let builtin_infer_assume = Exp.Const (Const.Cfun ModelBuiltins.__infer_assume) in
   let not_null_expr =
-    Exp.BinOp (Binop.Ne, sil_expr, Sil.exp_null) in
+    Exp.BinOp (Binop.Ne, sil_expr, Exp.null) in
   let assume_call_flag = { CallFlags.default with CallFlags.cf_noreturn = true; } in
   let call_args = [(not_null_expr, Typ.Tint Typ.IBool)] in
   Sil.Call ([], builtin_infer_assume, call_args, loc, assume_call_flag)
@@ -1003,12 +1003,12 @@ let rec instruction context pc instr : translation =
     | JBir.Check (JBir.CheckNullPointer expr) when Config.report_runtime_exceptions ->
         let (instrs, sil_expr, _) = expression context pc expr in
         let not_null_node =
-          let sil_not_null = Exp.BinOp (Binop.Ne, sil_expr, Sil.exp_null) in
+          let sil_not_null = Exp.BinOp (Binop.Ne, sil_expr, Exp.null) in
           let sil_prune_not_null = Sil.Prune (sil_not_null, loc, true, Sil.Ik_if)
           and not_null_kind = Cfg.Node.Prune_node (true, Sil.Ik_if, "Not null") in
           create_node not_null_kind (instrs @ [sil_prune_not_null]) in
         let throw_npe_node =
-          let sil_is_null = Exp.BinOp (Binop.Eq, sil_expr, Sil.exp_null) in
+          let sil_is_null = Exp.BinOp (Binop.Eq, sil_expr, Exp.null) in
           let sil_prune_null = Sil.Prune (sil_is_null, loc, true, Sil.Ik_if)
           and npe_kind = Cfg.Node.Stmt_node "Throw NPE"
           and npe_cn = JBasics.make_cn JConfig.npe_cl in
@@ -1095,12 +1095,12 @@ let rec instruction context pc instr : translation =
         let call = Sil.Call([ret_id], check_cast, args, loc, CallFlags.default) in
         let res_ex = Exp.Var ret_id in
         let is_instance_node =
-          let check_is_false = Exp.BinOp (Binop.Ne, res_ex, Sil.exp_zero) in
+          let check_is_false = Exp.BinOp (Binop.Ne, res_ex, Exp.zero) in
           let asssume_instance_of = Sil.Prune (check_is_false, loc, true, Sil.Ik_if)
           and instance_of_kind = Cfg.Node.Prune_node (true, Sil.Ik_if, "Is instance") in
           create_node instance_of_kind (instrs @ [call; asssume_instance_of])
         and throw_cast_exception_node =
-          let check_is_true = Exp.BinOp (Binop.Ne, res_ex, Sil.exp_one) in
+          let check_is_true = Exp.BinOp (Binop.Ne, res_ex, Exp.one) in
           let asssume_not_instance_of = Sil.Prune (check_is_true, loc, true, Sil.Ik_if)
           and throw_cast_exception_kind = Cfg.Node.Stmt_node "Class cast exception"
           and cce_cn = JBasics.make_cn JConfig.cce_cl in
diff --git a/infer/src/llvm/lTrans.ml b/infer/src/llvm/lTrans.ml
index 615c0f8f7..f6cbbd80d 100644
--- a/infer/src/llvm/lTrans.ml
+++ b/infer/src/llvm/lTrans.ml
@@ -25,7 +25,7 @@ let trans_variable (var : LAst.variable) : Exp.t = Exp.Var (ident_of_variable va
 
 let trans_constant : LAst.constant -> Exp.t = function
   | Cint i -> Exp.Const (Const.Cint (IntLit.of_int i))
-  | Cnull -> Sil.exp_null
+  | Cnull -> Exp.null
 
 let trans_operand : LAst.operand -> Exp.t = function
   | Var var -> trans_variable var
diff --git a/infer/src/unit/accessPathTests.ml b/infer/src/unit/accessPathTests.ml
index eee810931..7f5c39a16 100644
--- a/infer/src/unit/accessPathTests.ml
+++ b/infer/src/unit/accessPathTests.ml
@@ -100,7 +100,7 @@ let tests =
       check_make_ap xF_exp xF ~f_resolve_id;
       let xFG_exp = Exp.Lfield (xF_exp, g_fieldname, dummy_typ) in
       check_make_ap xFG_exp xFG ~f_resolve_id;
-      let xArr_exp = Exp.Lindex (x_exp, Sil.exp_zero) in
+      let xArr_exp = Exp.Lindex (x_exp, Exp.zero) in
       check_make_ap xArr_exp xArr ~f_resolve_id;
       (* make sure [f_resolve_id] works *)
       let f_resolve_id_to_xF _ = Some xF in
diff --git a/infer/src/unit/analyzerTester.ml b/infer/src/unit/analyzerTester.ml
index 8ca7bb6d0..448de6b6d 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 (IntLit.of_int rhs) in
+    let rhs_exp = Exp.int (IntLit.of_int rhs) in
     let rhs_typ = Typ.Tint Typ.IInt in
     var_assign_exp ~rhs_typ lhs rhs_exp
 
diff --git a/infer/src/unit/livenessTests.ml b/infer/src/unit/livenessTests.ml
index 5f39be30d..f64a28056 100644
--- a/infer/src/unit/livenessTests.ml
+++ b/infer/src/unit/livenessTests.ml
@@ -28,7 +28,7 @@ let tests =
     Exp.Closure closure in
   let unknown_cond =
     (* don't want to use AnalyzerTest.unknown_exp because we'll treat it as a live var! *)
-    Sil.exp_zero in
+    Exp.zero in
   let test_list = [
     "basic_live",
     [