diff --git a/infer/src/IR/Exp.re b/infer/src/IR/Exp.re
index 3435a25cc..4c1498556 100644
--- a/infer/src/IR/Exp.re
+++ b/infer/src/IR/Exp.re
@@ -50,3 +50,120 @@ and t =
       obtained from the type definition, e.g. when an array is over-allocated.  For struct types,
       the [dynamic_length] is that of the final extensible array, if any. */
   | Sizeof of Typ.t dynamic_length Subtype.t;
+
+
+/** Compare expressions. Variables come before other expressions. */
+let rec compare e1 e2 =>
+  switch (e1, e2) {
+  | (Var id1, Var id2) => Ident.compare id2 id1
+  | (Var _, _) => (-1)
+  | (_, Var _) => 1
+  | (UnOp o1 e1 to1, UnOp o2 e2 to2) =>
+    let n = Unop.compare o1 o2;
+    if (n != 0) {
+      n
+    } else {
+      let n = compare e1 e2;
+      if (n != 0) {
+        n
+      } else {
+        opt_compare Typ.compare to1 to2
+      }
+    }
+  | (UnOp _, _) => (-1)
+  | (_, UnOp _) => 1
+  | (BinOp o1 e1 f1, BinOp o2 e2 f2) =>
+    let n = Binop.compare o1 o2;
+    if (n != 0) {
+      n
+    } else {
+      let n = compare e1 e2;
+      if (n != 0) {
+        n
+      } else {
+        compare f1 f2
+      }
+    }
+  | (BinOp _, _) => (-1)
+  | (_, BinOp _) => 1
+  | (Exn e1, Exn e2) => compare e1 e2
+  | (Exn _, _) => (-1)
+  | (_, Exn _) => 1
+  | (Closure {name: n1, captured_vars: c1}, Closure {name: n2, captured_vars: c2}) =>
+    let captured_var_compare acc (e1, pvar1, typ1) (e2, pvar2, typ2) =>
+      if (acc != 0) {
+        acc
+      } else {
+        let n = compare e1 e2;
+        if (n != 0) {
+          n
+        } else {
+          let n = Pvar.compare pvar1 pvar2;
+          if (n != 0) {
+            n
+          } else {
+            Typ.compare typ1 typ2
+          }
+        }
+      };
+    let n = Procname.compare n1 n2;
+    if (n != 0) {
+      n
+    } else {
+      IList.fold_left2 captured_var_compare 0 c1 c2
+    }
+  | (Closure _, _) => (-1)
+  | (_, Closure _) => 1
+  | (Const c1, Const c2) => Const.compare c1 c2
+  | (Const _, _) => (-1)
+  | (_, Const _) => 1
+  | (Cast t1 e1, Cast t2 e2) =>
+    let n = compare e1 e2;
+    if (n != 0) {
+      n
+    } else {
+      Typ.compare t1 t2
+    }
+  | (Cast _, _) => (-1)
+  | (_, Cast _) => 1
+  | (Lvar i1, Lvar i2) => Pvar.compare i1 i2
+  | (Lvar _, _) => (-1)
+  | (_, Lvar _) => 1
+  | (Lfield e1 f1 t1, Lfield e2 f2 t2) =>
+    let n = compare e1 e2;
+    if (n != 0) {
+      n
+    } else {
+      let n = Ident.fieldname_compare f1 f2;
+      if (n != 0) {
+        n
+      } else {
+        Typ.compare t1 t2
+      }
+    }
+  | (Lfield _, _) => (-1)
+  | (_, Lfield _) => 1
+  | (Lindex e1 f1, Lindex e2 f2) =>
+    let n = compare e1 e2;
+    if (n != 0) {
+      n
+    } else {
+      compare f1 f2
+    }
+  | (Lindex _, _) => (-1)
+  | (_, Lindex _) => 1
+  | (Sizeof t1 l1 s1, Sizeof t2 l2 s2) =>
+    let n = Typ.compare t1 t2;
+    if (n != 0) {
+      n
+    } else {
+      let n = opt_compare compare l1 l2;
+      if (n != 0) {
+        n
+      } else {
+        Subtype.compare s1 s2
+      }
+    }
+  };
+
+let equal e1 e2 => compare e1 e2 == 0;
diff --git a/infer/src/IR/Exp.rei b/infer/src/IR/Exp.rei
index 3435a25cc..a6cbaac5d 100644
--- a/infer/src/IR/Exp.rei
+++ b/infer/src/IR/Exp.rei
@@ -50,3 +50,11 @@ and t =
       obtained from the type definition, e.g. when an array is over-allocated.  For struct types,
       the [dynamic_length] is that of the final extensible array, if any. */
   | Sizeof of Typ.t dynamic_length Subtype.t;
+
+
+/** Comparison for expressions. */
+let compare: t => t => int;
+
+
+/** Equality for expressions. */
+let equal: t => t => bool;
diff --git a/infer/src/IR/Sil.re b/infer/src/IR/Sil.re
index 447e889cb..5b46e0f3d 100644
--- a/infer/src/IR/Sil.re
+++ b/infer/src/IR/Sil.re
@@ -516,134 +516,17 @@ let attribute_compare (att1: attribute) (att2: attribute) :int =>
   | (_, Aunsubscribed_observer) => 1
   };
 
-
-/** Compare epressions. Variables come before other expressions. */
-let rec exp_compare (e1: Exp.t) (e2: Exp.t) :int =>
-  switch (e1, e2) {
-  | (Var id1, Var id2) => Ident.compare id2 id1
-  | (Var _, _) => (-1)
-  | (_, Var _) => 1
-  | (UnOp o1 e1 to1, UnOp o2 e2 to2) =>
-    let n = Unop.compare o1 o2;
-    if (n != 0) {
-      n
-    } else {
-      let n = exp_compare e1 e2;
-      if (n != 0) {
-        n
-      } else {
-        opt_compare Typ.compare to1 to2
-      }
-    }
-  | (UnOp _, _) => (-1)
-  | (_, UnOp _) => 1
-  | (BinOp o1 e1 f1, BinOp o2 e2 f2) =>
-    let n = Binop.compare o1 o2;
-    if (n != 0) {
-      n
-    } else {
-      let n = exp_compare e1 e2;
-      if (n != 0) {
-        n
-      } else {
-        exp_compare f1 f2
-      }
-    }
-  | (BinOp _, _) => (-1)
-  | (_, BinOp _) => 1
-  | (Exn e1, Exn e2) => exp_compare e1 e2
-  | (Exn _, _) => (-1)
-  | (_, Exn _) => 1
-  | (Closure {name: n1, captured_vars: c1}, Closure {name: n2, captured_vars: c2}) =>
-    let captured_var_compare acc (e1, pvar1, typ1) (e2, pvar2, typ2) =>
-      if (acc != 0) {
-        acc
-      } else {
-        let n = exp_compare e1 e2;
-        if (n != 0) {
-          n
-        } else {
-          let n = Pvar.compare pvar1 pvar2;
-          if (n != 0) {
-            n
-          } else {
-            Typ.compare typ1 typ2
-          }
-        }
-      };
-    let n = Procname.compare n1 n2;
-    if (n != 0) {
-      n
-    } else {
-      IList.fold_left2 captured_var_compare 0 c1 c2
-    }
-  | (Closure _, _) => (-1)
-  | (_, Closure _) => 1
-  | (Const c1, Const c2) => Const.compare c1 c2
-  | (Const _, _) => (-1)
-  | (_, Const _) => 1
-  | (Cast t1 e1, Cast t2 e2) =>
-    let n = exp_compare e1 e2;
-    if (n != 0) {
-      n
-    } else {
-      Typ.compare t1 t2
-    }
-  | (Cast _, _) => (-1)
-  | (_, Cast _) => 1
-  | (Lvar i1, Lvar i2) => Pvar.compare i1 i2
-  | (Lvar _, _) => (-1)
-  | (_, Lvar _) => 1
-  | (Lfield e1 f1 t1, Lfield e2 f2 t2) =>
-    let n = exp_compare e1 e2;
-    if (n != 0) {
-      n
-    } else {
-      let n = Ident.fieldname_compare f1 f2;
-      if (n != 0) {
-        n
-      } else {
-        Typ.compare t1 t2
-      }
-    }
-  | (Lfield _, _) => (-1)
-  | (_, Lfield _) => 1
-  | (Lindex e1 f1, Lindex e2 f2) =>
-    let n = exp_compare e1 e2;
-    if (n != 0) {
-      n
-    } else {
-      exp_compare f1 f2
-    }
-  | (Lindex _, _) => (-1)
-  | (_, Lindex _) => 1
-  | (Sizeof t1 l1 s1, Sizeof t2 l2 s2) =>
-    let n = Typ.compare t1 t2;
-    if (n != 0) {
-      n
-    } else {
-      let n = opt_compare exp_compare l1 l2;
-      if (n != 0) {
-        n
-      } else {
-        Subtype.compare s1 s2
-      }
-    }
-  };
-
-let exp_equal e1 e2 => exp_compare e1 e2 == 0;
-
 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
+  | _ => Exp.equal exp1 exp2
   };
 
-let ident_exp_compare = pair_compare Ident.compare exp_compare;
+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_compare = IList.compare Exp.compare;
 
 let exp_list_equal el1 el2 => exp_list_compare el1 el2 == 0;
 
@@ -657,20 +540,20 @@ let atom_compare a b =>
   } else {
     switch (a, b) {
     | (Aeq e1 e2, Aeq f1 f2) =>
-      let n = exp_compare e1 f1;
+      let n = Exp.compare e1 f1;
       if (n != 0) {
         n
       } else {
-        exp_compare e2 f2
+        Exp.compare e2 f2
       }
     | (Aeq _, _) => (-1)
     | (_, Aeq _) => 1
     | (Aneq e1 e2, Aneq f1 f2) =>
-      let n = exp_compare e1 f1;
+      let n = Exp.compare e1 f1;
       if (n != 0) {
         n
       } else {
-        exp_compare e2 f2
+        Exp.compare e2 f2
       }
     | (Aneq _, _) => (-1)
     | (_, Aneq _) => 1
@@ -679,7 +562,7 @@ let atom_compare a b =>
       if (n != 0) {
         n
       } else {
-        IList.compare exp_compare es1 es2
+        IList.compare Exp.compare es1 es2
       }
     | (Apred _, _) => (-1)
     | (_, Apred _) => 1
@@ -688,7 +571,7 @@ let atom_compare a b =>
       if (n != 0) {
         n
       } else {
-        IList.compare exp_compare es1 es2
+        IList.compare Exp.compare es1 es2
       }
     }
   };
@@ -711,14 +594,14 @@ let rec strexp_compare se1 se2 =>
     0
   } else {
     switch (se1, se2) {
-    | (Eexp e1 _, Eexp e2 _) => exp_compare e1 e2
+    | (Eexp e1 _, Eexp e2 _) => Exp.compare e1 e2
     | (Eexp _, _) => (-1)
     | (_, Eexp _) => 1
     | (Estruct fel1 _, Estruct fel2 _) => fld_strexp_list_compare fel1 fel2
     | (Estruct _, _) => (-1)
     | (_, Estruct _) => 1
     | (Earray e1 esel1 _, Earray e2 esel2 _) =>
-      let n = exp_compare e1 e2;
+      let n = Exp.compare e1 e2;
       if (n != 0) {
         n
       } else {
@@ -728,7 +611,7 @@ let rec strexp_compare se1 se2 =>
   }
 and fld_strexp_compare fse1 fse2 => pair_compare Ident.fieldname_compare strexp_compare fse1 fse2
 and fld_strexp_list_compare fsel1 fsel2 => IList.compare fld_strexp_compare fsel1 fsel2
-and exp_strexp_compare ese1 ese2 => pair_compare exp_compare strexp_compare ese1 ese2
+and exp_strexp_compare ese1 ese2 => pair_compare Exp.compare strexp_compare ese1 ese2
 and exp_strexp_list_compare esel1 esel2 => IList.compare exp_strexp_compare esel1 esel2;
 
 
@@ -738,14 +621,14 @@ let rec hpred_compare hpred1 hpred2 =>
     0
   } else {
     switch (hpred1, hpred2) {
-    | (Hpointsto e1 _ _, Hlseg _ _ e2 _ _) when exp_compare e2 e1 != 0 => exp_compare e2 e1
-    | (Hpointsto e1 _ _, Hdllseg _ _ e2 _ _ _ _) when exp_compare e2 e1 != 0 => exp_compare e2 e1
-    | (Hlseg _ _ e1 _ _, Hpointsto e2 _ _) when exp_compare e2 e1 != 0 => exp_compare e2 e1
-    | (Hlseg _ _ e1 _ _, Hdllseg _ _ e2 _ _ _ _) when exp_compare e2 e1 != 0 => exp_compare e2 e1
-    | (Hdllseg _ _ e1 _ _ _ _, Hpointsto e2 _ _) when exp_compare e2 e1 != 0 => exp_compare e2 e1
-    | (Hdllseg _ _ e1 _ _ _ _, Hlseg _ _ e2 _ _) when exp_compare e2 e1 != 0 => exp_compare e2 e1
+    | (Hpointsto e1 _ _, Hlseg _ _ e2 _ _) when Exp.compare e2 e1 != 0 => Exp.compare e2 e1
+    | (Hpointsto e1 _ _, Hdllseg _ _ e2 _ _ _ _) when Exp.compare e2 e1 != 0 => Exp.compare e2 e1
+    | (Hlseg _ _ e1 _ _, Hpointsto e2 _ _) when Exp.compare e2 e1 != 0 => Exp.compare e2 e1
+    | (Hlseg _ _ e1 _ _, Hdllseg _ _ e2 _ _ _ _) when Exp.compare e2 e1 != 0 => Exp.compare e2 e1
+    | (Hdllseg _ _ e1 _ _ _ _, Hpointsto e2 _ _) when Exp.compare e2 e1 != 0 => Exp.compare e2 e1
+    | (Hdllseg _ _ e1 _ _ _ _, Hlseg _ _ e2 _ _) when Exp.compare e2 e1 != 0 => Exp.compare e2 e1
     | (Hpointsto e1 se1 te1, Hpointsto e2 se2 te2) =>
-      let n = exp_compare e2 e1;
+      let n = Exp.compare e2 e1;
       if (n != 0) {
         n
       } else {
@@ -753,13 +636,13 @@ let rec hpred_compare hpred1 hpred2 =>
         if (n != 0) {
           n
         } else {
-          exp_compare te2 te1
+          Exp.compare te2 te1
         }
       }
     | (Hpointsto _, _) => (-1)
     | (_, Hpointsto _) => 1
     | (Hlseg k1 hpar1 e1 f1 el1, Hlseg k2 hpar2 e2 f2 el2) =>
-      let n = exp_compare e2 e1;
+      let n = Exp.compare e2 e1;
       if (n != 0) {
         n
       } else {
@@ -771,7 +654,7 @@ let rec hpred_compare hpred1 hpred2 =>
           if (n != 0) {
             n
           } else {
-            let n = exp_compare f2 f1;
+            let n = Exp.compare f2 f1;
             if (n != 0) {
               n
             } else {
@@ -783,7 +666,7 @@ let rec hpred_compare hpred1 hpred2 =>
     | (Hlseg _, Hdllseg _) => (-1)
     | (Hdllseg _, Hlseg _) => 1
     | (Hdllseg k1 hpar1 e1 f1 g1 h1 el1, Hdllseg k2 hpar2 e2 f2 g2 h2 el2) =>
-      let n = exp_compare e2 e1;
+      let n = Exp.compare e2 e1;
       if (n != 0) {
         n
       } else {
@@ -795,15 +678,15 @@ let rec hpred_compare hpred1 hpred2 =>
           if (n != 0) {
             n
           } else {
-            let n = exp_compare f2 f1;
+            let n = Exp.compare f2 f1;
             if (n != 0) {
               n
             } else {
-              let n = exp_compare g2 g1;
+              let n = Exp.compare g2 g1;
               if (n != 0) {
                 n
               } else {
-                let n = exp_compare h2 h1;
+                let n = Exp.compare h2 h1;
                 if (n != 0) {
                   n
                 } else {
@@ -881,12 +764,12 @@ let hpara_dll_equal hpara1 hpara2 => hpara_dll_compare hpara1 hpara2 == 0;
 /** {2 Sets of expressions} */
 let module ExpSet = Set.Make {
   type t = Exp.t;
-  let compare = exp_compare;
+  let compare = Exp.compare;
 };
 
 let module ExpMap = Map.Make {
   type t = Exp.t;
-  let compare = exp_compare;
+  let compare = Exp.compare;
 };
 
 let elist_to_eset es => IList.fold_left (fun set e => ExpSet.add e set) ExpSet.empty es;
@@ -1032,7 +915,7 @@ let rec _pp_exp pe0 pp_t f e0 => {
     | Some sub => Obj.obj (sub (Obj.repr e0)) /* apply object substitution to expression */
     | None => e0
     };
-  if (not (exp_equal e0 e)) {
+  if (not (Exp.equal e0 e)) {
     switch e {
     | Exp.Lvar pvar => Pvar.pp_value pe f pvar
     | _ => assert false
@@ -2449,7 +2332,7 @@ let rec sub_compare (sub1: subst) (sub2: subst) =>
       if (n != 0) {
         n
       } else {
-        let n = exp_compare e1 e2;
+        let n = Exp.compare e1 e2;
         if (n != 0) {
           n
         } else {
@@ -2795,7 +2678,7 @@ let instr_sub_ids sub_id_binders::sub_id_binders (f: Ident.t => Exp.t) instr =>
 let instr_sub (subst: subst) instr => instr_sub_ids sub_id_binders::true (apply_sub subst) instr;
 
 let exp_typ_compare (exp1, typ1) (exp2, typ2) => {
-  let n = exp_compare exp1 exp2;
+  let n = Exp.compare exp1 exp2;
   if (n != 0) {
     n
   } else {
@@ -2810,7 +2693,7 @@ let instr_compare instr1 instr2 =>
     if (n != 0) {
       n
     } else {
-      let n = exp_compare e1 e2;
+      let n = Exp.compare e1 e2;
       if (n != 0) {
         n
       } else {
@@ -2825,7 +2708,7 @@ let instr_compare instr1 instr2 =>
   | (Letderef _, _) => (-1)
   | (_, Letderef _) => 1
   | (Set e11 t1 e21 loc1, Set e12 t2 e22 loc2) =>
-    let n = exp_compare e11 e12;
+    let n = Exp.compare e11 e12;
     if (n != 0) {
       n
     } else {
@@ -2833,7 +2716,7 @@ let instr_compare instr1 instr2 =>
       if (n != 0) {
         n
       } else {
-        let n = exp_compare e21 e22;
+        let n = Exp.compare e21 e22;
         if (n != 0) {
           n
         } else {
@@ -2844,7 +2727,7 @@ let instr_compare instr1 instr2 =>
   | (Set _, _) => (-1)
   | (_, Set _) => 1
   | (Prune cond1 loc1 true_branch1 ik1, Prune cond2 loc2 true_branch2 ik2) =>
-    let n = exp_compare cond1 cond2;
+    let n = Exp.compare cond1 cond2;
     if (n != 0) {
       n
     } else {
@@ -2867,7 +2750,7 @@ let instr_compare instr1 instr2 =>
     if (n != 0) {
       n
     } else {
-      let n = exp_compare e1 e2;
+      let n = Exp.compare e1 e2;
       if (n != 0) {
         n
       } else {
@@ -2941,7 +2824,7 @@ let rec exp_compare_structural e1 e2 exp_map => {
   let compare_exps_with_map e1 e2 exp_map =>
     try {
       let e1_mapping = ExpMap.find e1 exp_map;
-      (exp_compare e1_mapping e2, exp_map)
+      (Exp.compare e1_mapping e2, exp_map)
     } {
     | Not_found =>
       /* assume e1 and e2 equal, enforce by adding to [exp_map] */
@@ -3009,7 +2892,7 @@ let rec exp_compare_structural e1 e2 exp_map => {
     } else {
       exp_compare_structural f1 f2 exp_map
     }
-  | _ => (exp_compare e1 e2, exp_map)
+  | _ => (Exp.compare e1 e2, exp_map)
   }
 };
 
@@ -3174,7 +3057,7 @@ let hpred_sub subst => {
 /** {2 Functions for replacing occurrences of expressions.} */
 let exp_replace_exp epairs e =>
   try {
-    let (_, e') = IList.find (fun (e1, _) => exp_equal e e1) epairs;
+    let (_, e') = IList.find (fun (e1, _) => Exp.equal e e1) epairs;
     e'
   } {
   | Not_found => e
@@ -3225,7 +3108,7 @@ let hpred_replace_exp epairs =>
 /** {2 Compaction} */
 let module ExpHash = Hashtbl.Make {
   type t = Exp.t;
-  let equal = exp_equal;
+  let equal = Exp.equal;
   let hash = Hashtbl.hash;
 };
 
diff --git a/infer/src/IR/Sil.rei b/infer/src/IR/Sil.rei
index dbef6bc2f..e166a234c 100644
--- a/infer/src/IR/Sil.rei
+++ b/infer/src/IR/Sil.rei
@@ -403,10 +403,6 @@ let attribute_to_category: attribute => attribute_category;
 
 let attr_is_undef: attribute => bool;
 
-let exp_compare: Exp.t => Exp.t => int;
-
-let exp_equal: Exp.t => Exp.t => 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;
diff --git a/infer/src/backend/abs.ml b/infer/src/backend/abs.ml
index e618bdce9..19165f308 100644
--- a/infer/src/backend/abs.ml
+++ b/infer/src/backend/abs.ml
@@ -434,8 +434,8 @@ let typ_get_recursive_flds tenv typ_exp =
       assert false
 
 let discover_para_roots p root1 next1 root2 next2 : Sil.hpara option =
-  let eq_arg1 = Sil.exp_equal root1 next1 in
-  let eq_arg2 = Sil.exp_equal root2 next2 in
+  let eq_arg1 = Exp.equal root1 next1 in
+  let eq_arg2 = Exp.equal root2 next2 in
   let precondition_check = (not eq_arg1 && not eq_arg2) in
   if not precondition_check then None
   else
@@ -449,10 +449,10 @@ let discover_para_roots p root1 next1 root2 next2 : Sil.hpara option =
         Some hpara
 
 let discover_para_dll_roots p root1 blink1 flink1 root2 blink2 flink2 : Sil.hpara_dll option =
-  let eq_arg1 = Sil.exp_equal root1 blink1 in
-  let eq_arg1' = Sil.exp_equal root1 flink1 in
-  let eq_arg2 = Sil.exp_equal root2 blink2 in
-  let eq_arg2' = Sil.exp_equal root2 flink2 in
+  let eq_arg1 = Exp.equal root1 blink1 in
+  let eq_arg1' = Exp.equal root1 flink1 in
+  let eq_arg2 = Exp.equal root2 blink2 in
+  let eq_arg2' = Exp.equal root2 flink2 in
   let precondition_check = not (eq_arg1 || eq_arg1' || eq_arg2 || eq_arg2') in
   if not precondition_check then None
   else
@@ -491,7 +491,7 @@ let discover_para_candidates tenv p =
     | [] -> IList.rev found
     | (e1, e2) :: edges_notseen ->
         let edges_others = (IList.rev edges_seen) @ edges_notseen in
-        let edges_matched = IList.filter (fun (e1', _) -> Sil.exp_equal e2 e1') edges_others in
+        let edges_matched = IList.filter (fun (e1', _) -> Exp.equal e2 e1') edges_others in
         let new_found =
           let f found_acc (_, e3) = (e1, e2, e3) :: found_acc in
           IList.fold_left f found edges_matched in
@@ -531,7 +531,7 @@ let discover_para_dll_candidates tenv p =
     | [] -> IList.rev found
     | (iF, blink, flink) :: edges_notseen ->
         let edges_others = (IList.rev edges_seen) @ edges_notseen in
-        let edges_matched = IList.filter (fun (e1', _, _) -> Sil.exp_equal flink e1') edges_others in
+        let edges_matched = IList.filter (fun (e1', _, _) -> Exp.equal flink e1') edges_others in
         let new_found =
           let f found_acc (_, _, flink2) = (iF, blink, flink, flink2) :: found_acc in
           IList.fold_left f found edges_matched in
@@ -608,7 +608,7 @@ let eqs_solve ids_in eqs_in =
         solve sub' eqs_rest' in
     match eqs with
     | [] -> Some sub
-    | (e1, e2) :: eqs_rest when Sil.exp_equal e1 e2 ->
+    | (e1, e2) :: eqs_rest when Exp.equal e1 e2 ->
         solve sub eqs_rest
     | (Exp.Var id1, (Exp.Const _ as e2)) :: eqs_rest ->
         do_default id1 e2 eqs_rest
@@ -884,7 +884,7 @@ let get_cycle root prop =
     | Sil.Eexp(e', _) ->
         (try
            Some(IList.find (fun hpred -> match hpred with
-               | Sil.Hpointsto(e'', _, _) -> Sil.exp_equal e'' e'
+               | Sil.Hpointsto(e'', _, _) -> Exp.equal e'' e'
                | _ -> false) sigma)
          with _ -> None)
     | _ -> None in
@@ -959,7 +959,7 @@ let get_var_retain_cycle _prop =
   let is_hpred_block v h =
     match h, v with
     | Sil.Hpointsto (e, _, Exp.Sizeof (typ, _, _)), Sil.Eexp (e', _)
-      when Sil.exp_equal e e' && Typ.is_block_type typ -> true
+      when Exp.equal e e' && Typ.is_block_type typ -> true
     | _, _ -> false in
   let find v =
     try
diff --git a/infer/src/backend/absarray.ml b/infer/src/backend/absarray.ml
index 3c7d7b382..0496832b5 100644
--- a/infer/src/backend/absarray.ml
+++ b/infer/src/backend/absarray.ml
@@ -74,7 +74,7 @@ end = struct
                  Ident.fieldname_equal f' fld) instance_fields) in
         get_strexp_at_syn_offsets se' t' syn_offs'
     | Sil.Earray (_, esel, _), Typ.Tarray (t', _), Index ind :: syn_offs' ->
-        let se' = snd (IList.find (fun (i', _) -> Sil.exp_equal i' ind) esel) in
+        let se' = snd (IList.find (fun (i', _) -> Exp.equal i' ind) esel) in
         get_strexp_at_syn_offsets se' t' syn_offs'
     | _ ->
         L.d_strln "Failure of get_strexp_at_syn_offsets";
@@ -99,9 +99,10 @@ end = struct
             ) fsel in
         Sil.Estruct (fsel', inst)
     | Sil.Earray (len, esel, inst), Typ.Tarray (t', _), Index idx :: syn_offs' ->
-        let se' = snd (IList.find (fun (i', _) -> Sil.exp_equal i' idx) esel) in
+        let se' = snd (IList.find (fun (i', _) -> Exp.equal i' idx) esel) in
         let se_mod = replace_strexp_at_syn_offsets se' t' syn_offs' update in
-        let esel' = IList.map (fun ese -> if Sil.exp_equal (fst ese) idx then (idx, se_mod) else ese) esel in
+        let esel' =
+          IList.map (fun ese -> if Exp.equal (fst ese) idx then (idx, se_mod) else ese) esel in
         Sil.Earray (len, esel', inst)
     | _ -> assert false
 
@@ -136,7 +137,7 @@ end = struct
   (** Find an array at the given path. Can raise [Not_found] *)
   let find_path sigma (root, syn_offs) : t =
     let filter = function
-      | Sil.Hpointsto (e, _, _) -> Sil.exp_equal root e
+      | Sil.Hpointsto (e, _, _) -> Exp.equal root e
       | _ -> false in
     let hpred = IList.find filter sigma in
     (sigma, hpred, syn_offs)
@@ -210,7 +211,7 @@ end = struct
       match se', se_in with
       | Sil.Earray (len, esel, _), Sil.Earray (_, esel_in, inst2) ->
           let orig_indices = IList.map fst esel in
-          let index_is_not_new idx = IList.exists (Sil.exp_equal idx) orig_indices in
+          let index_is_not_new idx = IList.exists (Exp.equal idx) orig_indices in
           let process_index idx =
             if index_is_not_new idx then idx else (Sil.array_clean_new_index footprint_part idx) in
           let esel_in' = IList.map (fun (idx, se) -> process_index idx, se) esel_in in
@@ -236,7 +237,10 @@ end = struct
     let update se' =
       match se' with
       | Sil.Earray (len, esel, inst) ->
-          let esel' = IList.map (fun (e', se') -> if Sil.exp_equal e' index then (index', se') else (e', se')) esel in
+          let esel' =
+            IList.map (fun (e', se') ->
+                if Exp.equal e' index then (index', se') else (e', se')
+              ) esel in
           Sil.Earray (len, esel', inst)
       | _ -> assert false in
     let hpred' = hpred_replace_strexp footprint_part hpred syn_offs update in
@@ -273,7 +277,7 @@ let prop_replace_path_index
       ) [] elist_path in
   let expmap_fun e' =
     try
-      let _, fresh_e = IList.find (fun (e, _) -> Sil.exp_equal e e') expmap_list in
+      let _, fresh_e = IList.find (fun (e, _) -> Exp.equal e e') expmap_list in
       fresh_e
     with Not_found -> e' in
   Prop.prop_expmap expmap_fun p
@@ -358,7 +362,7 @@ let index_is_pointed_to (p: Prop.normal Prop.t) (path: StrexpMatch.path) (index:
     fun i -> IList.map (add_index i) elist_path in
   let pointers = IList.flatten (IList.map add_index_to_paths indices) in
   let filter = function
-    | Sil.Hpointsto (_, Sil.Eexp (e, _), _) -> IList.exists (Sil.exp_equal e) pointers
+    | Sil.Hpointsto (_, Sil.Eexp (e, _), _) -> IList.exists (Exp.equal e) pointers
     | _ -> false in
   IList.exists filter (Prop.get_sigma p)
 
@@ -419,7 +423,8 @@ let keep_only_indices
       let (_, se, _) = StrexpMatch.get_data matched in
       match se with
       | Sil.Earray (len, esel, inst) ->
-          let esel', esel_leftover' = IList.partition (fun (e, _) -> IList.exists (Sil.exp_equal e) indices) esel in
+          let esel', esel_leftover' =
+            IList.partition (fun (e, _) -> IList.exists (Exp.equal e) indices) esel in
           if esel_leftover' == [] then (sigma, false)
           else begin
             let se' = Sil.Earray (len, esel', inst) in
diff --git a/infer/src/backend/dom.ml b/infer/src/backend/dom.ml
index f69b178c5..fc30d7989 100644
--- a/infer/src/backend/dom.ml
+++ b/infer/src/backend/dom.ml
@@ -39,7 +39,7 @@ let sigma_equal sigma1 sigma2 =
   f sigma1_sorted sigma2_sorted
 
 let sigma_get_start_lexps_sort sigma =
-  let exp_compare_neg e1 e2 = - (Sil.exp_compare e1 e2) in
+  let exp_compare_neg e1 e2 = - (Exp.compare e1 e2) in
   let filter e = Sil.fav_for_all (Sil.exp_fav e) Ident.is_normal in
   let lexps = Sil.hpred_list_get_lexps filter sigma in
   IList.sort exp_compare_neg lexps
@@ -69,9 +69,9 @@ module EPset = Set.Make
     (struct
       type t = Exp.t * Exp.t
       let compare (e1, e1') (e2, e2') =
-        match (Sil.exp_compare e1 e2) with
+        match (Exp.compare e1 e2) with
         | i when i <> 0 -> i
-        | _ -> Sil.exp_compare e1' e2'
+        | _ -> Exp.compare e1' e2'
     end)
 
 (** {2 Module for maintaining information about noninjectivity during join} *)
@@ -120,7 +120,7 @@ end = struct
     let e' = lookup_equiv' tbl e in
     match e' with
     | Exp.Var _ ->
-        if Sil.exp_equal e e' then e
+        if Exp.equal e e' then e
         else
           begin
             let root = find' tbl e' in
@@ -133,7 +133,7 @@ end = struct
     let r1 = find' tbl e1 in
     let r2 = find' tbl e2 in
     let new_r, old_r =
-      match (Sil.exp_compare r1 r2) with
+      match (Exp.compare r1 r2) with
       | i when i <= 0 -> r1, r2
       | _ -> r2, r1 in
     let new_c = lookup_const' const_tbl new_r in
@@ -171,7 +171,7 @@ end = struct
         if (can_rename id') then replace_const' tbl const_tbl e' e
         else (L.d_strln "failure reason 7"; raise IList.Fail)
     | _ ->
-        if not (Sil.exp_equal e e') then (L.d_strln "failure reason 8"; raise IList.Fail) else ()
+        if not (Exp.equal e e') then (L.d_strln "failure reason 8"; raise IList.Fail) else ()
 
   let check side es =
     let f = function Exp.Var id -> can_rename id | _ -> false in
@@ -188,7 +188,7 @@ end = struct
       | v:: vars', _ ->
           let r = find' tbl v in
           let set = lookup_const' const_tbl r in
-          (IList.for_all (fun v' -> Sil.exp_equal (find' tbl v') r) vars') &&
+          (IList.for_all (fun v' -> Exp.equal (find' tbl v') r) vars') &&
           (IList.for_all (fun c -> Sil.ExpSet.mem c set) nonvars)
 
 end
@@ -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 (Sil.exp_equal Sil.exp_zero) es
+          IList.exists (Exp.equal Sil.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
@@ -449,12 +449,12 @@ end = struct
   let final () = t := []
 
   let entry_compare (e1, e2, _) (_, e2', _) =
-    let n1 = Sil.exp_compare e1 e2 in
-    if n1 <> 0 then n1 else Sil.exp_compare e2 e2'
+    let n1 = Exp.compare e1 e2 in
+    if n1 <> 0 then n1 else Exp.compare e2 e2'
 
   let get_fresh_exp e1 e2 =
     try
-      let (_, _, e) = IList.find (fun (e1', e2', _) -> Sil.exp_equal e1 e1' && Sil.exp_equal e2 e2') !t in
+      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
@@ -512,7 +512,7 @@ end = struct
   let lookup side e =
     try
       let (e1, e2, e) =
-        IList.find (fun (e1', e2', _) -> Sil.exp_equal e (select side e1' e2')) !t in
+        IList.find (fun (e1', e2', _) -> Exp.equal e (select side e1' e2')) !t in
       Some (e, select (opposite side) e1 e2)
     with Not_found ->
       None
@@ -573,7 +573,7 @@ end = struct
         | Exp.Const _ -> []
         | Exp.Lvar _ | Exp.Var _
         | Exp.BinOp (Binop.PlusA, Exp.Var _, _) ->
-            let is_same_e (e1, e2, _) = Sil.exp_equal e (select side e1 e2) in
+            let is_same_e (e1, e2, _) = Exp.equal e (select side e1 e2) in
             let assoc = IList.filter is_same_e !tbl in
             IList.map (fun (e1, e2, _) -> select side_op e1 e2) assoc
         | _ ->
@@ -585,19 +585,19 @@ end = struct
     (IList.for_all (f Rhs) rhs_es) && (IList.for_all (f Lhs) lhs_es)
 
   let lookup_side' side e =
-    let f (e1, e2, _) = Sil.exp_equal e (select side e1 e2) in
+    let f (e1, e2, _) = Exp.equal e (select side e1 e2) in
     IList.filter f !tbl
 
   let lookup_side_induced' side e =
     let res = ref [] in
     let f v = match v, side with
       | (Exp.BinOp (Binop.PlusA, e1', Exp.Const (Const.Cint i)), e2, e'), Lhs
-        when Sil.exp_equal e e1' ->
+        when Exp.equal e e1' ->
           let c' = Sil.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 Sil.exp_equal e e2' ->
+        when Exp.equal e e2' ->
           let c' = Sil.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
@@ -633,10 +633,10 @@ end = struct
         (function (e1, e2, Exp.Var i) -> (i, select side e1 e2) | _ -> assert false)
         renaming_restricted in
     let sub_list_side_sorted =
-      IList.sort (fun (_, e) (_, e') -> Sil.exp_compare e e') sub_list_side in
+      IList.sort (fun (_, e) (_, e') -> Exp.compare e e') sub_list_side in
     let rec find_duplicates =
       function
-      | (_, e):: ((_, e'):: _ as t) -> Sil.exp_equal e e' || find_duplicates t
+      | (_, e):: ((_, e'):: _ as t) -> Exp.equal e e' || find_duplicates t
       | _ -> false in
     if find_duplicates sub_list_side_sorted then (L.d_strln "failure reason 11"; raise IList.Fail)
     else Sil.sub_of_list sub_list_side
@@ -751,7 +751,7 @@ end = struct
    * should be a primed or footprint variable *)
   let extend e1 e2 default_op =
     try
-      let eq_to_e (f1, f2, _) = Sil.exp_equal e1 f1 && Sil.exp_equal e2 f2 in
+      let eq_to_e (f1, f2, _) = Exp.equal e1 f1 && Exp.equal e2 f2 in
       let _, _, res = IList.find eq_to_e !tbl in
       res
     with Not_found ->
@@ -762,7 +762,7 @@ end = struct
       let some_primed () = Sil.fav_exists fav1 Ident.is_primed || Sil.fav_exists fav2 Ident.is_primed in
       let e =
         if (no_ren1 && no_ren2) then
-          if (Sil.exp_equal e1 e2) then e1 else (L.d_strln "failure reason 13"; raise IList.Fail)
+          if (Exp.equal e1 e2) then e1 else (L.d_strln "failure reason 13"; raise IList.Fail)
         else
           match default_op with
           | ExtDefault e -> e
@@ -775,7 +775,7 @@ end = struct
       e
 (*
   let get e1 e2 =
-    let f (e1', e2', _) = Sil.exp_equal e1 e1' && Sil.exp_equal e2 e2' in
+    let f (e1', e2', _) = Exp.equal e1 e1' && Exp.equal e2 e2' in
     match (IList.filter f !tbl) with
     | [] -> None
     | (_, _, e):: _ -> Some e
@@ -1170,7 +1170,7 @@ let rec strexp_partial_meet (strexp1: Sil.strexp) (strexp2: Sil.strexp) : Sil.st
       let inst = Sil.inst_partial_meet inst1 inst2 in
       f_fld_se_list inst [] fld_se_list1 fld_se_list2
   | Sil.Earray (len1, idx_se_list1, inst1), Sil.Earray (len2, idx_se_list2, inst2)
-    when Sil.exp_equal len1 len2 ->
+    when Exp.equal len1 len2 ->
       let inst = Sil.inst_partial_meet inst1 inst2 in
       f_idx_se_list inst len1 [] idx_se_list1 idx_se_list2
   | _ -> (L.d_strln "failure reason 52"; raise IList.Fail)
@@ -1235,8 +1235,8 @@ let hpred_partial_join mode (todo: Exp.t * Exp.t * Exp.t) (hpred1: Sil.hpred) (h
       Prop.mk_lseg (kind_join k1 k2) hpara' e next' shared'
   | Sil.Hdllseg (k1, para1, iF1, oB1, oF1, iB1, shared1),
     Sil.Hdllseg (k2, para2, iF2, oB2, oF2, iB2, shared2) ->
-      let fwd1 = Sil.exp_equal e1 iF1 in
-      let fwd2 = Sil.exp_equal e2 iF2 in
+      let fwd1 = Exp.equal e1 iF1 in
+      let fwd2 = Exp.equal e2 iF2 in
       let hpara' = hpara_dll_partial_join para1 para2 in
       let iF', iB' =
         if (fwd1 && fwd2) then (e, exp_partial_join iB1 iB2)
@@ -1253,7 +1253,7 @@ let hpred_partial_meet (todo: Exp.t * Exp.t * Exp.t) (hpred1: Sil.hpred) (hpred2
   : Sil.hpred =
   let e1, e2, e = todo in
   match hpred1, hpred2 with
-  | Sil.Hpointsto (_, se1, te1), Sil.Hpointsto (_, se2, te2) when Sil.exp_equal te1 te2 ->
+  | Sil.Hpointsto (_, se1, te1), Sil.Hpointsto (_, se2, te2) when Exp.equal te1 te2 ->
       Prop.mk_ptsto e (strexp_partial_meet se1 se2) te1
   | Sil.Hpointsto _, _ | _, Sil.Hpointsto _ ->
       (L.d_strln "failure reason 58"; raise IList.Fail)
@@ -1264,8 +1264,8 @@ let hpred_partial_meet (todo: Exp.t * Exp.t * Exp.t) (hpred1: Sil.hpred) (hpred2
       Prop.mk_lseg (kind_meet k1 k2) hpara' e next' shared'
   | Sil.Hdllseg (k1, para1, iF1, oB1, oF1, iB1, shared1),
     Sil.Hdllseg (k2, para2, iF2, oB2, oF2, iB2, shared2) ->
-      let fwd1 = Sil.exp_equal e1 iF1 in
-      let fwd2 = Sil.exp_equal e2 iF2 in
+      let fwd1 = Exp.equal e1 iF1 in
+      let fwd2 = Exp.equal e2 iF2 in
       let hpara' = hpara_dll_partial_meet para1 para2 in
       let iF', iB' =
         if (fwd1 && fwd2) then (e, exp_partial_meet iB1 iB2)
@@ -1337,7 +1337,7 @@ let rec sigma_partial_join' mode (sigma_acc: Prop.sigma)
         Sil.Hlseg (Sil.Lseg_PE, hpara, root', next', shared')
 
     | Sil.Hdllseg (_, hpara, iF, oB, oF, iB, shared)
-      when Sil.exp_equal iF e ->
+      when Exp.equal iF e ->
         let oF' = do_side side exp_partial_join oF opposite in
         let shared' = Rename.lookup_list side shared in
         let oB', iB' = lookup_and_expand side oB iB in
@@ -1350,7 +1350,7 @@ let rec sigma_partial_join' mode (sigma_acc: Prop.sigma)
         Sil.Hdllseg (Sil.Lseg_PE, hpara, root', oB', oF', iB', shared')
 
     | Sil.Hdllseg (_, hpara, iF, oB, oF, iB, shared)
-      when Sil.exp_equal iB e ->
+      when Exp.equal iB e ->
         let oB' = do_side side exp_partial_join oB opposite in
         let shared' = Rename.lookup_list side shared in
         let oF', iF' = lookup_and_expand side oF iF in
@@ -1467,7 +1467,7 @@ let rec sigma_partial_join' mode (sigma_acc: Prop.sigma)
         sigma_partial_join' mode sigma_acc' sigma1' sigma2
 
     | Some (Sil.Hdllseg (_, _, iF1, _, _, iB1, _) as dllseg), Some (hpred2)
-      when Sil.exp_equal e1 iF1 ->
+      when Exp.equal e1 iF1 ->
         let iB_res = exp_partial_join iB1 e2 in
         let sigma2' = cut_dllseg Lhs todo_curr iF1 dllseg (hpred2:: sigma2) in
         let sigma_acc' = update_dllseg Lhs dllseg e iB_res :: sigma_acc in
@@ -1475,7 +1475,7 @@ let rec sigma_partial_join' mode (sigma_acc: Prop.sigma)
         sigma_partial_join' mode sigma_acc' sigma1 sigma2'
 
     | Some (Sil.Hdllseg (_, _, iF1, _, _, iB1, _) as dllseg), Some (hpred2)
-    (* when Sil.exp_equal e1 iB1 *) ->
+      (* when Exp.equal e1 iB1 *) ->
         let iF_res = exp_partial_join iF1 e2 in
         let sigma2' = cut_dllseg Lhs todo_curr iB1 dllseg (hpred2:: sigma2) in
         let sigma_acc' = update_dllseg Lhs dllseg iF_res e :: sigma_acc in
@@ -1483,7 +1483,7 @@ let rec sigma_partial_join' mode (sigma_acc: Prop.sigma)
         sigma_partial_join' mode sigma_acc' sigma1 sigma2'
 
     | Some (hpred1), Some (Sil.Hdllseg (_, _, iF2, _, _, iB2, _) as dllseg)
-      when Sil.exp_equal e2 iF2 ->
+      when Exp.equal e2 iF2 ->
         let iB_res = exp_partial_join e1 iB2 in
         let sigma1' = cut_dllseg Rhs todo_curr iF2 dllseg (hpred1:: sigma1) in
         let sigma_acc' = update_dllseg Rhs dllseg e iB_res :: sigma_acc in
@@ -1622,11 +1622,11 @@ let pi_partial_join mode
   let is_stronger_le e n a =
     match Prop.atom_exp_le_const a with
     | None -> false
-    | Some (e', n') -> Sil.exp_equal e e' && IntLit.lt n' n in
+    | Some (e', n') -> Exp.equal e e' && IntLit.lt n' n in
   let is_stronger_lt n e a =
     match Prop.atom_const_lt_exp a with
     | None -> false
-    | Some (n', e') -> Sil.exp_equal e e' && IntLit.lt n n' in
+    | Some (n', e') -> Exp.equal e e' && IntLit.lt n n' in
   let join_atom_check_pre p a =
     (* check for atoms in pre mode: fail if the negation is implied by the other side *)
     let not_a = Prop.atom_negate a in
@@ -1735,7 +1735,7 @@ let eprop_partial_meet (ep1: 'a Prop.t) (ep2: 'b Prop.t) : 'c Prop.t =
 
   let es1 = sigma_get_start_lexps_sort sigma1 in
   let es2 = sigma_get_start_lexps_sort sigma2 in
-  let es = IList.merge_sorted_nodup Sil.exp_compare [] es1 es2 in
+  let es = IList.merge_sorted_nodup Exp.compare [] es1 es2 in
 
   let sub_check _ =
     let sub1 = Prop.get_sub ep1 in
@@ -1785,7 +1785,7 @@ let eprop_partial_join' mode (ep1: Prop.exposed Prop.t) (ep2: Prop.exposed Prop.
     | [], [] -> true
     | [], _:: _ | _:: _, [] -> false
     | e1:: es1'', e2:: es2'' ->
-        Sil.exp_equal e1 e2 && expensive_check es1'' es2'' in
+        Exp.equal e1 e2 && expensive_check es1'' es2'' in
   let sub_common, eqs_from_sub1, eqs_from_sub2 =
     let sub1 = Prop.get_sub ep1 in
     let sub2 = Prop.get_sub ep2 in
diff --git a/infer/src/backend/dotty.ml b/infer/src/backend/dotty.ml
index df9419d16..73c5a7fdb 100644
--- a/infer/src/backend/dotty.ml
+++ b/infer/src/backend/dotty.ml
@@ -173,7 +173,7 @@ and get_contents pe coo f = function
 (* true if node is the sorce node of the expression e*)
 let is_source_node_of_exp e node =
   match node with
-  | Dotpointsto (_, e', _) -> Sil.exp_compare e e' = 0
+  | Dotpointsto (_, e', _) -> Exp.compare e e' = 0
   | _ -> false
 
 (* given a node returns its coordinates and the expression. Return -1 in case the expressio doesn.t*)
@@ -203,7 +203,7 @@ let rec look_up_for_back_pointer e dotnodes lambda =
   match dotnodes with
   | [] -> []
   | Dotdllseg(coo, _, _, _, e4, _, _, _):: dotnodes' ->
-      if Sil.exp_compare e e4 = 0 && lambda = coo.lambda then [coo.id + 1]
+      if Exp.compare e e4 = 0 && lambda = coo.lambda then [coo.id + 1]
       else look_up_for_back_pointer e dotnodes' lambda
   | _:: dotnodes' -> look_up_for_back_pointer e dotnodes' lambda
 
@@ -213,7 +213,8 @@ let rec select_nodes_exp_lambda dotnodes e lambda =
   | [] -> []
   | node:: l' ->
       let (coo, e') = get_coordinate_and_exp node in
-      if (Sil.exp_compare e e' = 0) && lambda = coo.lambda then node:: select_nodes_exp_lambda l' e lambda
+      if (Exp.compare e e' = 0) && lambda = coo.lambda
+      then node:: select_nodes_exp_lambda l' e lambda
       else select_nodes_exp_lambda l' e lambda
 
 (* look-up the coordinate id in the list of dotnodes those nodes which correspond to expression e*)
@@ -245,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 (Sil.exp_equal e Sil.exp_zero)  && !print_full_prop ->
+       when not (Exp.equal e Sil.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 (Sil.exp_equal e2 Sil.exp_zero) ->
+     | Sil.Hlseg (_, _, _, e2, _) when not (Exp.equal e2 Sil.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 (Sil.exp_equal e2 Sil.exp_zero) then
+         let ll = if not (Exp.equal e2 Sil.exp_zero) then
              [Dotdangling(coo, e2, e2_color_str)]
            else [] in
-         if not (Sil.exp_equal e3 Sil.exp_zero) then Dotdangling(coo, e3, e3_color_str):: ll
+         if not (Exp.equal e3 Sil.exp_zero) then Dotdangling(coo, e3, e3_color_str):: ll
          else ll
      | Sil.Hpointsto (_, _, _)
      | _ -> [] (* arrays and struct do not give danglings*)
@@ -269,7 +270,7 @@ let make_dangling_boxes pe allocated_nodes (sigma_lambda: (Sil.hpred * int) list
             | Dotpointsto(_, e', _)
             | Dotarray(_, _, e', _, _, _)
             | Dotlseg(_, e', _, _, _, _)
-            | Dotdllseg(_, e', _, _, _, _, _, _) -> Sil.exp_equal e e'
+            | Dotdllseg(_, e', _, _, _, _, _, _) -> Exp.equal e e'
             | _ -> false
           ) allocated_nodes
     | _ -> false (*this should never happen since d must be a dangling node *) in
@@ -277,7 +278,7 @@ let make_dangling_boxes pe allocated_nodes (sigma_lambda: (Sil.hpred * int) list
     match l with
     | [] -> []
     | Dotdangling(coo, e, color):: l' ->
-        if (IList.exists (Sil.exp_equal e) seen_exp) then filter_duplicate l' seen_exp
+        if (IList.exists (Exp.equal e) seen_exp) then filter_duplicate l' seen_exp
         else Dotdangling(coo, e, color):: filter_duplicate l' (e:: seen_exp)
     | box:: l' -> box:: filter_duplicate l' seen_exp (* this case cannot happen*) in
   let rec subtract_allocated candidate_dangling =
@@ -308,7 +309,7 @@ let rec dotty_mk_node pe sigma =
          Dotstruct((mk_coordinate (n + 1) lambda), e, l, e_color_str, te);]
     | (Sil.Hpointsto (e, _, _), lambda) ->
         let e_color_str = color_to_str (exp_color e) in
-        if IList.mem Sil.exp_equal e !struct_exp_nodes then [] else
+        if IList.mem Exp.equal e !struct_exp_nodes then [] else
           [Dotpointsto((mk_coordinate n lambda), e, e_color_str)]
     | (Sil.Hlseg (k, hpara, e1, e2, _), lambda) ->
         incr dotty_state_count; (* increment once more n+1 is the box for last element of the list *)
@@ -336,7 +337,7 @@ let set_exps_neq_zero pi =
 
 let box_dangling e =
   let entry_e = IList.filter (fun b -> match b with
-      | Dotdangling(_, e', _) -> Sil.exp_equal e e' | _ -> false ) !dangling_dotboxes in
+      | Dotdangling(_, e', _) -> Exp.equal e e' | _ -> false ) !dangling_dotboxes in
   match entry_e with
   |[] -> None
   | Dotdangling(coo, _, _):: _ -> Some coo.id
@@ -376,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 =
-  (Sil.exp_equal e Sil.exp_zero) || (Prover.check_equal prop e Sil.exp_zero)
+  (Exp.equal e Sil.exp_zero) || (Prover.check_equal prop e Sil.exp_zero)
 
 (* an edge is in cycle *)
 let in_cycle cycle edge =
@@ -413,7 +414,7 @@ let rec compute_target_struct_fields dotnodes list_fld p f lambda cycle =
                )
            | [node] | [Dotpointsto _ ; node] | [node; Dotpointsto _] ->
                let n = get_coordinate_id node in
-               if IList.mem Sil.exp_equal e !struct_exp_nodes then begin
+               if IList.mem Exp.equal e !struct_exp_nodes then begin
                  let e_no_special_char = strip_special_chars (Sil.exp_to_string e) in
                  let link_kind = if (in_cycle cycle (fn, se)) && (not !print_full_prop) then
                      LinkRetainCycle
@@ -449,7 +450,7 @@ let rec compute_target_array_elements dotnodes list_elements p f lambda =
                )
            | [node] | [Dotpointsto _ ; node] | [node; Dotpointsto _] ->
                let n = get_coordinate_id node in
-               if IList.mem Sil.exp_equal e !struct_exp_nodes then begin
+               if IList.mem Exp.equal e !struct_exp_nodes then begin
                  let e_no_special_char = strip_special_chars (Sil.exp_to_string e) in
                  [(LinkArrayToStruct, Sil.exp_to_string idx, n, e_no_special_char)]
                end else
@@ -1112,7 +1113,7 @@ let atom_to_xml_string a =
 (* return the dangling node corresponding to an expression it exists or None *)
 let exp_dangling_node e =
   let entry_e = IList.filter (fun b -> match b with
-      | VH_dangling(_, e') -> Sil.exp_equal e e' | _ -> false ) !set_dangling_nodes in
+      | VH_dangling(_, e') -> Exp.equal e e' | _ -> false ) !set_dangling_nodes in
   match entry_e with
   |[] -> None
   | VH_dangling(n, e') :: _ -> Some (VH_dangling(n, e'))
@@ -1156,7 +1157,7 @@ let rec select_node_at_address nodes e =
   | [] -> None
   | n:: l' ->
       let e' = get_node_addr n in
-      if (Sil.exp_compare e e' = 0) then Some n
+      if (Exp.compare e e' = 0) then Some n
       else select_node_at_address l' e
 
 (* look-up the ids in the list of nodes corresponding to expression e*)
@@ -1171,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 (Sil.exp_equal e Sil.exp_zero) -> [e]
-     | Sil.Hlseg (_, _, _, e2, _) when not (Sil.exp_equal e2 Sil.exp_zero) -> [e2]
+     | 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.Hdllseg (_, _, _, e2, e3, _, _) ->
-         if (Sil.exp_equal e2 Sil.exp_zero) then
-           if (Sil.exp_equal e3 Sil.exp_zero) then []
+         if (Exp.equal e2 Sil.exp_zero) then
+           if (Exp.equal e3 Sil.exp_zero) then []
            else [e3]
          else [e2; e3]
      | Sil.Hpointsto (_, _, _)
@@ -1185,14 +1186,14 @@ let make_set_dangling_nodes allocated_nodes (sigma: Sil.hpred list) =
     let allocated = IList.exists (fun a -> match a with
         | VH_pointsto(_, e', _, _)
         | VH_lseg(_, e', _ , _)
-        | VH_dllseg(_, e', _, _, _, _) -> Sil.exp_equal e e'
+        | VH_dllseg(_, e', _, _, _, _) -> Exp.equal e e'
         | _ -> false ) allocated_nodes in
     not allocated in
   let rec filter_duplicate l seen_exp =
     match l with
     | [] -> []
     | e:: l' ->
-        if (IList.exists (Sil.exp_equal e) seen_exp) then filter_duplicate l' seen_exp
+        if (IList.exists (Exp.equal e) seen_exp) then filter_duplicate l' seen_exp
         else e:: filter_duplicate l' (e:: seen_exp) in
   let rhs_exp_list = IList.flatten (IList.map get_rhs_predicate sigma) in
   let candidate_dangling_exps = filter_duplicate rhs_exp_list [] in
@@ -1408,7 +1409,7 @@ let print_specs_xml signature specs loc fmt =
 
 (*
 let exp_is_neq_zero e =
-  IList.exists (fun e' -> Sil.exp_equal e e') !exps_neq_zero
+  IList.exists (fun e' -> Exp.equal e e') !exps_neq_zero
 
 let rec get_contents_range_single pe coo f range_se =
   let (e1, e2), se = range_se in
@@ -1454,5 +1455,5 @@ let rec get_color_exp dot_nodes e =
   | Dotlseg(_, e', _, _, _, c):: l'
   | Dotstruct(_, e', _, c, _):: l'
   | Dotdllseg(_, e', _, _, _, _, _, c):: l' ->
-      if (Sil.exp_equal e e') then c else get_color_exp l' e
+      if (Exp.equal e e') then c else get_color_exp l' e
 *)
diff --git a/infer/src/backend/errdesc.ml b/infer/src/backend/errdesc.ml
index 54e1ea12e..bbe7d6b83 100644
--- a/infer/src/backend/errdesc.ml
+++ b/infer/src/backend/errdesc.ml
@@ -97,7 +97,7 @@ let find_in_node_or_preds start_node f_node_instr =
 (** Find the Set instruction used to assign [id] to a program variable, if any *)
 let find_variable_assigment node id : Sil.instr option =
   let find_set _ instr = match instr with
-    | Sil.Set (Exp.Lvar _, _, e, _) when Sil.exp_equal (Exp.Var id) e -> Some instr
+    | Sil.Set (Exp.Lvar _, _, e, _) when Exp.equal (Exp.Var id) e -> Some instr
     | _ -> None in
   find_in_node_or_preds node find_set
 
@@ -453,7 +453,7 @@ let leak_from_list_abstraction hpred prop =
     | _ -> None in
   let found = ref false in
   let check_hpred texp hp = match hpred_type hp with
-    | Some texp' when Sil.exp_equal texp texp' -> found := true
+    | Some texp' when Exp.equal texp texp' -> found := true
     | _ -> () in
   let check_hpara texp _ hpara =
     IList.iter (check_hpred texp) hpara.Sil.body in
@@ -479,7 +479,7 @@ let find_hpred_typ hpred = match hpred with
 let find_typ_without_ptr prop pvar =
   let res = ref None in
   let do_hpred = function
-    | Sil.Hpointsto (e, _, te) when Sil.exp_equal e (Exp.Lvar pvar) ->
+    | Sil.Hpointsto (e, _, te) when Exp.equal e (Exp.Lvar pvar) ->
         res := Some te
     | _ -> () in
   IList.iter do_hpred (Prop.get_sigma prop);
@@ -586,7 +586,7 @@ let vpath_find prop _exp : DExp.t option * Typ.t option =
   if verbose then (L.d_str "in vpath_find exp:"; Sil.d_exp _exp; L.d_ln ());
   let rec find sigma_acc sigma_todo exp =
     let do_fse res sigma_acc' sigma_todo' lexp texp (f, se) = match se with
-      | Sil.Eexp (e, _) when Sil.exp_equal exp e ->
+      | Sil.Eexp (e, _) when Exp.equal exp e ->
           let sigma' = (IList.rev_append sigma_acc' sigma_todo') in
           (match lexp with
            | Exp.Lvar pv ->
@@ -612,7 +612,7 @@ let vpath_find prop _exp : DExp.t option * Typ.t option =
                   Sil.d_exp lexp; L.d_ln ()))
       | _ -> () in
     let do_sexp sigma_acc' sigma_todo' lexp sexp texp = match sexp with
-      | Sil.Eexp (e, _) when Sil.exp_equal exp e ->
+      | Sil.Eexp (e, _) when Exp.equal exp e ->
           let sigma' = (IList.rev_append sigma_acc' sigma_todo') in
           (match lexp with
            | Exp.Lvar pv when not (Pvar.is_frontend_tmp pv) ->
@@ -682,7 +682,7 @@ let explain_dexp_access prop dexp is_nullable =
   let find_ptsto (e : Exp.t) : Sil.strexp option =
     let res = ref None in
     let do_hpred = function
-      | Sil.Hpointsto (e', se, _) when Sil.exp_equal e e' ->
+      | Sil.Hpointsto (e', se, _) when Exp.equal e e' ->
           res := Some se
       | _ -> () in
     IList.iter do_hpred sigma;
@@ -701,7 +701,7 @@ let explain_dexp_access prop dexp is_nullable =
         if verbose then (L.d_str "lookup_esel: can't find index "; Sil.d_exp e; L.d_ln ());
         None
     | (e1, se):: esel' ->
-        if Sil.exp_equal e1 e then Some se
+        if Exp.equal e1 e then Some se
         else lookup_esel esel' e in
   let rec lookup : DExp.t -> Sil.strexp option = function
     | DExp.Dconst c ->
@@ -1006,17 +1006,17 @@ let find_with_exp prop exp =
     if !res = None then res := Some (pv, Fstruct (IList.rev fld_lst)) in
   let rec search_struct pv fld_lst = function
     | Sil.Eexp (e, _) ->
-        if Sil.exp_equal e exp then found_in_struct pv fld_lst
+        if Exp.equal e exp then found_in_struct pv fld_lst
     | Sil.Estruct (fsel, _) ->
         IList.iter (fun (f, se) -> search_struct pv (f:: fld_lst) se) fsel
     | _ -> () in
   let do_hpred_pointed_by_pvar pv e = function
     | Sil.Hpointsto(e1, se, _) ->
-        if Sil.exp_equal e e1 then search_struct pv [] se
+        if Exp.equal e e1 then search_struct pv [] se
     | _ -> () in
   let do_hpred = function
     | Sil.Hpointsto(Exp.Lvar pv, Sil.Eexp (e, _), _) ->
-        if Sil.exp_equal e exp then found_in_pvar pv
+        if Exp.equal e exp then found_in_pvar pv
         else IList.iter (do_hpred_pointed_by_pvar pv e) (Prop.get_sigma prop)
     | _ -> () in
   IList.iter do_hpred (Prop.get_sigma prop);
diff --git a/infer/src/backend/interproc.ml b/infer/src/backend/interproc.ml
index 05ac35bbc..3d3470e0d 100644
--- a/infer/src/backend/interproc.ml
+++ b/infer/src/backend/interproc.ml
@@ -409,7 +409,7 @@ let check_assignement_guard node =
           [e']
       | _ -> [] in
     let prune_vars = IList.flatten(IList.map (fun n -> prune_var n) succs) in
-    IList.for_all (fun e' -> Sil.exp_equal e' e) prune_vars in
+    IList.for_all (fun e' -> Exp.equal e' e) prune_vars in
   let succs_loc = IList.map (fun n -> Cfg.Node.get_loc n) succs in
   let succs_are_all_prune_nodes () =
     IList.for_all (fun n -> match Cfg.Node.get_kind n with
@@ -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 && Sil.exp_equal e Sil.exp_null -> atoms
+      when Ident.equal v var && Exp.equal e Sil.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/match.ml b/infer/src/backend/match.ml
index 71058ccd8..4ca7a77db 100644
--- a/infer/src/backend/match.ml
+++ b/infer/src/backend/match.ml
@@ -38,7 +38,7 @@ let rec pp_hpat_list pe f = function
 let rec exp_match e1 sub vars e2 : (Sil.subst * Ident.t list) option =
   let check_equal sub vars e1 e2 =
     let e2_inst = Sil.exp_sub sub e2
-    in if (Sil.exp_equal e1 e2_inst) then Some(sub, vars) else None in
+    in if (Exp.equal e1 e2_inst) then Some(sub, vars) else None in
   match e1, e2 with
   | _, Exp.Var id2 when (Ident.is_primed id2 && mem_idlist id2 vars) ->
       let vars_new = IList.filter (fun id -> not (Ident.equal id id2)) vars in
@@ -148,7 +148,7 @@ and isel_match isel1 sub vars isel2 =
         L.out "@[<4>    IDX2: %a, STREXP2: %a@\n@." (Sil.pp_exp pe) idx2 (Sil.pp_sexp pe) se2';
         assert false
       end
-      else if Sil.exp_equal idx1 idx2 then begin
+      else if Exp.equal idx1 idx2 then begin
         match strexp_match se1' sub vars se2' with
         | None -> None
         | Some (sub', vars') -> isel_match isel1' sub' vars' isel2'
@@ -246,7 +246,7 @@ let rec iter_match_with_impl iter condition sub vars hpat hpats =
     in prop_match_with_impl_sub p_rest condition sub_new vars_leftover hpat_next hpats_rest
   in
   let gen_filter_pointsto lexp2 strexp2 te2 = function
-    | Sil.Hpointsto (lexp1, strexp1, te1) when Sil.exp_equal te1 te2 ->
+    | Sil.Hpointsto (lexp1, strexp1, te1) when Exp.equal te1 te2 ->
         (match (exp_match lexp1 sub vars lexp2) with
          | None -> None
          | Some (sub', vars_leftover) -> strexp_match strexp1 sub' vars_leftover strexp2)
@@ -502,7 +502,7 @@ let rec generate_todos_from_strexp mode todos sexp1 sexp2 =
   | Sil.Estruct _, _ ->
       None
   | Sil.Earray (len1, iel1, _), Sil.Earray (len2, iel2, _) ->
-      if (not (Sil.exp_equal len1 len2) || IList.length iel1 <> IList.length iel2)
+      if (not (Exp.equal len1 len2) || IList.length iel1 <> IList.length iel2)
       then None
       else generate_todos_from_iel mode todos iel1 iel2
   | Sil.Earray _, _ ->
@@ -548,22 +548,22 @@ and generate_todos_from_iel mode todos iel1 iel2 =
 
 (** add (e1,e2) at the front of corres, if necessary. *)
 let corres_extend_front e1 e2 corres =
-  let filter (e1', e2') = (Sil.exp_equal e1 e1') || (Sil.exp_equal e2 e2') in
-  let checker e1' e2' = (Sil.exp_equal e1 e1') && (Sil.exp_equal e2 e2')
+  let filter (e1', e2') = (Exp.equal e1 e1') || (Exp.equal e2 e2') in
+  let checker e1' e2' = (Exp.equal e1 e1') && (Exp.equal e2 e2')
   in match (IList.filter filter corres) with
   | [] -> Some ((e1, e2) :: corres)
   | [(e1', e2')] when checker e1' e2' -> Some corres
   | _ -> None
 
 let corres_extensible corres e1 e2 =
-  let predicate (e1', e2') = (Sil.exp_equal e1 e1') || (Sil.exp_equal e2 e2')
-  in not (IList.exists predicate corres) && not (Sil.exp_equal e1 e2)
+  let predicate (e1', e2') = (Exp.equal e1 e1') || (Exp.equal e2 e2')
+  in not (IList.exists predicate corres) && not (Exp.equal e1 e2)
 
 let corres_related corres e1 e2 =
-  let filter (e1', e2') = (Sil.exp_equal e1 e1') || (Sil.exp_equal e2 e2') in
-  let checker e1' e2' = (Sil.exp_equal e1 e1') && (Sil.exp_equal e2 e2') in
+  let filter (e1', e2') = (Exp.equal e1 e1') || (Exp.equal e2 e2') in
+  let checker e1' e2' = (Exp.equal e1 e1') && (Exp.equal e2 e2') in
   match (IList.filter filter corres) with
-  | [] -> Sil.exp_equal e1 e2
+  | [] -> Exp.equal e1 e2
   | [(e1', e2')] when checker e1' e2' -> true
   | _ -> false
 
@@ -604,7 +604,7 @@ let rec generic_find_partial_iso mode update corres sigma_corres todos sigma_tod
         | None, _ | _, None ->
             None
         | Some (Sil.Hpointsto (_, _, te1)), Some (Sil.Hpointsto (_, _, te2))
-          when not (Sil.exp_equal te1 te2) ->
+          when not (Exp.equal te1 te2) ->
             None
         | Some (Sil.Hpointsto (_, se1, _) as hpred1),
           Some (Sil.Hpointsto (_, se2, _) as hpred2) ->
@@ -723,9 +723,9 @@ let generic_para_create corres sigma1 elist1 =
     let add_fresh_id pair = (pair, Ident.create_fresh Ident.kprimed) in
     IList.map add_fresh_id new_corres' in
   let (es_shared, ids_shared, ids_exists) =
-    let not_in_elist1 ((e1, _), _) = not (IList.exists (Sil.exp_equal e1) elist1) in
+    let not_in_elist1 ((e1, _), _) = not (IList.exists (Exp.equal e1) elist1) in
     let corres_ids_no_elist1 = IList.filter not_in_elist1 corres_ids in
-    let should_be_shared ((e1, e2), _) = Sil.exp_equal e1 e2 in
+    let should_be_shared ((e1, e2), _) = Exp.equal e1 e2 in
     let shared, exists = IList.partition should_be_shared corres_ids_no_elist1 in
     let es_shared = IList.map (fun ((e1, _), _) -> e1) shared in
     (es_shared, IList.map snd shared, IList.map snd exists) in
@@ -745,7 +745,7 @@ let hpara_create corres sigma1 root1 next1 =
     generic_para_create corres sigma1 [root1; next1] in
   let get_id1 e1 =
     try
-      let is_equal_to_e1 (e1', _) = Sil.exp_equal e1 e1' in
+      let is_equal_to_e1 (e1', _) = Exp.equal e1 e1' in
       let _, id = IList.find is_equal_to_e1 renaming in
       id
     with Not_found -> assert false in
@@ -768,7 +768,7 @@ let hpara_dll_create corres sigma1 root1 blink1 flink1 =
     generic_para_create corres sigma1 [root1; blink1; flink1] in
   let get_id1 e1 =
     try
-      let is_equal_to_e1 (e1', _) = Sil.exp_equal e1 e1' in
+      let is_equal_to_e1 (e1', _) = Exp.equal e1 e1' in
       let _, id = IList.find is_equal_to_e1 renaming in
       id
     with Not_found -> assert false in
diff --git a/infer/src/backend/modelBuiltins.ml b/infer/src/backend/modelBuiltins.ml
index 903dd51ff..736665686 100644
--- a/infer/src/backend/modelBuiltins.ml
+++ b/infer/src/backend/modelBuiltins.ml
@@ -63,7 +63,7 @@ let add_array_to_prop pdesc prop_ lexp typ =
   begin
     try
       let hpred = IList.find (function
-          | Sil.Hpointsto(e, _, _) -> Sil.exp_equal e n_lexp
+          | Sil.Hpointsto(e, _, _) -> Exp.equal e n_lexp
           | _ -> false) (Prop.get_sigma prop) in
       match hpred with
       | Sil.Hpointsto(_, Sil.Earray (len, _, _), _) ->
@@ -114,7 +114,7 @@ let execute___set_array_length { Builtin.pdesc; prop_; path; ret_ids; args; }
            let n_lexp, prop__ = check_arith_norm_exp pname lexp prop_a in
            let n_len, prop = check_arith_norm_exp pname len prop__ in
            let hpred, sigma' = IList.partition (function
-               | Sil.Hpointsto(e, _, _) -> Sil.exp_equal e n_lexp
+               | Sil.Hpointsto(e, _, _) -> Exp.equal e n_lexp
                | _ -> false) (Prop.get_sigma prop) in
            (match hpred with
             | [Sil.Hpointsto(e, Sil.Earray(_, esel, inst), t)] ->
@@ -146,7 +146,7 @@ let create_type tenv n_lexp typ prop =
   let prop_type =
     try
       let _ = IList.find (function
-          | Sil.Hpointsto(e, _, _) -> Sil.exp_equal e n_lexp
+          | Sil.Hpointsto(e, _, _) -> Exp.equal e n_lexp
           | _ -> false) (Prop.get_sigma prop) in
       prop
     with Not_found ->
@@ -200,7 +200,7 @@ let execute___get_type_of { Builtin.pdesc; tenv; prop_; path; ret_ids; args; }
         begin
           try
             let hpred = IList.find (function
-                | Sil.Hpointsto(e, _, _) -> Sil.exp_equal e n_lexp
+                | Sil.Hpointsto(e, _, _) -> Exp.equal e n_lexp
                 | _ -> false) (Prop.get_sigma prop) in
             match hpred with
             | Sil.Hpointsto(_, _, texp) ->
@@ -216,7 +216,7 @@ let replace_ptsto_texp prop root_e texp =
   let process_sigma sigma =
     let sigma1, sigma2 =
       IList.partition (function
-          | Sil.Hpointsto(e, _, _) -> Sil.exp_equal e root_e
+          | Sil.Hpointsto(e, _, _) -> Exp.equal e root_e
           | _ -> false) sigma in
     match sigma1 with
     | [Sil.Hpointsto(e, se, _)] -> (Sil.Hpointsto (e, se, texp)) :: sigma2
@@ -247,13 +247,13 @@ let execute___instanceof_cast ~instof
         Tabulation.raise_cast_exception
           __POS__ None texp1 texp2 val1 in
       let exe_one_prop prop =
-        if Sil.exp_equal texp2 Sil.exp_zero then
+        if Exp.equal texp2 Sil.exp_zero then
           [(return_result Sil.exp_zero prop ret_ids, path)]
         else
           begin
             try
               let hpred = IList.find (function
-                  | Sil.Hpointsto (e1, _, _) -> Sil.exp_equal e1 val1
+                  | Sil.Hpointsto (e1, _, _) -> Exp.equal e1 val1
                   | _ -> false) (Prop.get_sigma prop) in
               match hpred with
               | Sil.Hpointsto (_, _, texp1) ->
@@ -263,7 +263,7 @@ let execute___instanceof_cast ~instof
                     | None -> []
                     | Some texp1' ->
                         let prop' =
-                          if Sil.exp_equal texp1 texp1' then prop
+                          if Exp.equal texp1 texp1' then prop
                           else replace_ptsto_texp prop val1 texp1' in
                         [(return_result res_e prop' ret_ids, path)] in
                   if instof then (* instanceof *)
@@ -395,14 +395,14 @@ let execute___get_hidden_field { Builtin.pdesc; prop_; path; ret_ids; args; }
       let has_fld_hidden fsel = IList.exists filter_fld_hidden fsel in
       let do_hpred in_foot hpred = match hpred with
         | Sil.Hpointsto(e, Sil.Estruct (fsel, inst), texp)
-          when Sil.exp_equal e n_lexp && (not (has_fld_hidden fsel)) ->
+          when Exp.equal e n_lexp && (not (has_fld_hidden fsel)) ->
             let foot_e = Lazy.force foot_var in
             ret_val := Some foot_e;
             let se = Sil.Eexp(foot_e, Sil.inst_none) in
             let fsel' = (Ident.fieldname_hidden, se) :: fsel in
             Sil.Hpointsto(e, Sil.Estruct (fsel', inst), texp)
         | Sil.Hpointsto(e, Sil.Estruct (fsel, _), _)
-          when Sil.exp_equal e n_lexp && not in_foot && has_fld_hidden fsel ->
+          when Exp.equal e n_lexp && not in_foot && has_fld_hidden fsel ->
             let set_ret_val () =
               match IList.find filter_fld_hidden fsel with
               | _, Sil.Eexp(e, _) -> ret_val := Some e
@@ -431,14 +431,14 @@ let execute___set_hidden_field { Builtin.pdesc; prop_; path; args; }
       let has_fld_hidden fsel = IList.exists filter_fld_hidden fsel in
       let do_hpred in_foot hpred = match hpred with
         | Sil.Hpointsto(e, Sil.Estruct (fsel, inst), texp)
-          when Sil.exp_equal e n_lexp1 && not in_foot ->
+          when Exp.equal e n_lexp1 && not in_foot ->
             let se = Sil.Eexp(n_lexp2, Sil.inst_none) in
             let fsel' =
               (Ident.fieldname_hidden, se) ::
               (IList.filter (fun x -> not (filter_fld_hidden x)) fsel) in
             Sil.Hpointsto(e, Sil.Estruct (fsel', inst), texp)
         | Sil.Hpointsto(e, Sil.Estruct (fsel, inst), texp)
-          when Sil.exp_equal e n_lexp1 && in_foot && not (has_fld_hidden fsel) ->
+          when Exp.equal e n_lexp1 && in_foot && not (has_fld_hidden fsel) ->
             let foot_e = Lazy.force foot_var in
             let se = Sil.Eexp(foot_e, Sil.inst_none) in
             let fsel' = (Ident.fieldname_hidden, se) :: fsel in
@@ -562,7 +562,7 @@ let execute___release_autorelease_pool
       | ((prop', path') :: _, Sil.Apred (_, exp :: _)) ->
           (try
              let hpred = IList.find (function
-                 | Sil.Hpointsto(e1, _, _) -> Sil.exp_equal e1 exp
+                 | Sil.Hpointsto(e1, _, _) -> Exp.equal e1 exp
                  | _ -> false) (Prop.get_sigma prop_) in
              match hpred with
              | Sil.Hpointsto (_, _, Exp.Sizeof (typ, _, _)) ->
@@ -661,7 +661,7 @@ let execute___objc_cast { Builtin.pdesc; prop_; path; ret_ids; args; }
       let texp2, prop = check_arith_norm_exp pname texp2_ prop__ in
       (try
          let hpred = IList.find (function
-             | Sil.Hpointsto(e1, _, _) -> Sil.exp_equal e1 val1
+             | Sil.Hpointsto(e1, _, _) -> Exp.equal e1 val1
              | _ -> false) (Prop.get_sigma prop) in
          match hpred, texp2 with
          | Sil.Hpointsto (val1, _, _), Exp.Sizeof _ ->
@@ -815,7 +815,7 @@ let execute___cxx_typeid ({ Builtin.pdesc; tenv; prop_; args; loc} as r)
            let typ =
              try
                let hpred = IList.find (function
-                   | Sil.Hpointsto (e, _, _) -> Sil.exp_equal e n_lexp
+                   | Sil.Hpointsto (e, _, _) -> Exp.equal e n_lexp
                    | _ -> false) (Prop.get_sigma prop) in
                match hpred with
                | Sil.Hpointsto (_, _, Exp.Sizeof (dynamic_type, _, _)) -> dynamic_type
diff --git a/infer/src/backend/prop.ml b/infer/src/backend/prop.ml
index a8fc57ec0..3d7ef9785 100644
--- a/infer/src/backend/prop.ml
+++ b/infer/src/backend/prop.ml
@@ -259,7 +259,7 @@ let create_pvar_env (sigma: sigma) : (Exp.t -> Exp.t) =
   IList.iter filter sigma;
   let find e =
     try
-      snd (IList.find (fun (e1, _) -> Sil.exp_equal e1 e) !env)
+      snd (IList.find (fun (e1, _) -> Exp.equal e1 e) !env)
     with Not_found -> e in
   find
 
@@ -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 Sil.exp_equal e1' e2' then Sil.exp_zero
+        if Exp.equal e1' e2' then Sil.exp_zero
         else begin
           match e1', e2' with
           | Exp.Const c, _ when iszero_int_float c ->
@@ -946,11 +946,11 @@ let inequality_normalize a =
     | _ -> [e],[], IntLit.zero in
   (* sort and filter out expressions appearing in both the positive and negative part *)
   let normalize_posnegoff (pos, neg, off) =
-    let pos' = IList.sort Sil.exp_compare pos in
-    let neg' = IList.sort Sil.exp_compare neg in
+    let pos' = IList.sort Exp.compare pos in
+    let neg' = IList.sort Exp.compare neg in
     let rec combine pacc nacc = function
       | x:: ps, y:: ng ->
-          (match Sil.exp_compare x y with
+          (match Exp.compare x y with
            | n when n < 0 -> combine (x:: pacc) nacc (ps, y :: ng)
            | 0 -> combine pacc nacc (ps, ng)
            | _ -> combine pacc (y:: nacc) (x :: ps, ng))
@@ -983,7 +983,7 @@ let inequality_normalize a =
       mk_inequality (norm_from_exp e)
   | _ -> a
 
-let exp_reorder e1 e2 = if Sil.exp_compare e1 e2 <= 0 then (e1, e2) else (e2, e1)
+let exp_reorder e1 e2 = if Exp.compare e1 e2 <= 0 then (e1, e2) else (e2, e1)
 
 (** Normalize an atom.
     We keep the convention that inequalities with constants
@@ -1007,8 +1007,8 @@ let atom_normalize sub a0 =
         then normalize_eq (e1', e2')
         else eq
     | Exp.Lindex (e1', idx1), Exp.Lindex (e2', idx2) ->
-        if Sil.exp_equal idx1 idx2 then normalize_eq (e1', e2')
-        else if Sil.exp_equal e1' e2' then normalize_eq (idx1, idx2)
+        if Exp.equal idx1 idx2 then normalize_eq (e1', e2')
+        else if Exp.equal e1' e2' then normalize_eq (idx1, idx2)
         else eq
     | _ -> eq in
   let handle_unary_negation e1 e2 =
@@ -1071,7 +1071,7 @@ let rec strexp_normalize sub se =
         let len' = exp_normalize_noabs sub len in
         match idx_cnts with
         | [] ->
-            if Sil.exp_equal len len' then se else Sil.Earray (len', idx_cnts, inst)
+            if Exp.equal len len' then se else Sil.Earray (len', idx_cnts, inst)
         | _ ->
             let idx_cnts' =
               IList.map (fun (idx, cnt) ->
@@ -1220,7 +1220,7 @@ let pi_tighten_ineq pi =
       | _ -> acc in
     IList.fold_left get_disequality_info [] nonineq_list in
   let is_neq e n =
-    IList.exists (fun (e', n') -> Sil.exp_equal e e' && IntLit.eq n n') diseq_list in
+    IList.exists (fun (e', n') -> Exp.equal e e' && IntLit.eq n n') diseq_list in
   let le_list_tightened =
     let get_le_inequality_info acc a =
       match atom_exp_le_const a with
@@ -1262,10 +1262,10 @@ let pi_tighten_ineq pi =
         | Sil.Aneq(Exp.Const (Const.Cint n), e)
         | Sil.Aneq(e, Exp.Const (Const.Cint n)) ->
             (not (IList.exists
-                    (fun (e', n') -> Sil.exp_equal e e' && IntLit.lt n' n)
+                    (fun (e', n') -> Exp.equal e e' && IntLit.lt n' n)
                     le_list_tightened)) &&
             (not (IList.exists
-                    (fun (n', e') -> Sil.exp_equal e e' && IntLit.leq n n')
+                    (fun (n', e') -> Exp.equal e e' && IntLit.leq n n')
                     lt_list_tightened))
         | _ -> true)
       nonineq_list in
@@ -1277,13 +1277,13 @@ let rec pi_sorted_remove_redundant = function
               Exp.Const (Const.Cint i1)) as a1) ::
     Sil.Aeq (Exp.BinOp (Binop.Le, e2, Exp.Const (Const.Cint n2)),
              Exp.Const (Const.Cint i2)) :: rest
-    when IntLit.isone i1 && IntLit.isone i2 && Sil.exp_equal e1 e2 && IntLit.lt n1 n2 ->
+    when IntLit.isone i1 && IntLit.isone i2 && Exp.equal e1 e2 && IntLit.lt n1 n2 ->
       (* second inequality redundant *)
       pi_sorted_remove_redundant (a1 :: rest)
   | Sil.Aeq (Exp.BinOp (Binop.Lt, Exp.Const (Const.Cint n1), e1), Exp.Const (Const.Cint i1)) ::
     (Sil.Aeq (Exp.BinOp (Binop.Lt, Exp.Const (Const.Cint n2), e2), Exp.Const (Const.Cint i2)) as a2)
     :: rest
-    when IntLit.isone i1 && IntLit.isone i2 && Sil.exp_equal e1 e2 && IntLit.lt n1 n2 ->
+    when IntLit.isone i1 && IntLit.isone i2 && Exp.equal e1 e2 && IntLit.lt n1 n2 ->
       (* first inequality redundant *)
       pi_sorted_remove_redundant (a2 :: rest)
   | a1:: a2:: rest ->
@@ -1310,15 +1310,15 @@ let pi_normalize sub sigma pi0 =
   let ineq_list, nonineq_list = pi_tighten_ineq pi in
   let syntactically_different = function
     | Exp.BinOp(op1, e1, Exp.Const(c1)), Exp.BinOp(op2, e2, Exp.Const(c2))
-      when Sil.exp_equal e1 e2 ->
+      when Exp.equal e1 e2 ->
         Binop.equal op1 op2 && Binop.injective op1 && not (Const.equal c1 c2)
     | e1, Exp.BinOp(op2, e2, Exp.Const(c2))
-      when Sil.exp_equal e1 e2 ->
+      when Exp.equal e1 e2 ->
         Binop.injective op2 &&
         Binop.is_zero_runit op2 &&
         not (Const.equal (Const.Cint IntLit.zero) c2)
     | Exp.BinOp(op1, e1, Exp.Const(c1)), e2
-      when Sil.exp_equal e1 e2 ->
+      when Exp.equal e1 e2 ->
         Binop.injective op1 &&
         Binop.is_zero_runit op1 &&
         not (Const.equal (Const.Cint IntLit.zero) c1)
@@ -1327,7 +1327,7 @@ let pi_normalize sub sigma pi0 =
     let unsigned_exps = lazy (sigma_get_unsigned_exps sigma) in
     function
     | Sil.Aneq ((Exp.Var _) as e, Exp.Const (Const.Cint n)) when IntLit.isnegative n ->
-        not (IList.exists (Sil.exp_equal e) (Lazy.force unsigned_exps))
+        not (IList.exists (Exp.equal e) (Lazy.force unsigned_exps))
     | Sil.Aneq(e1, e2) ->
         not (syntactically_different (e1, e2))
     | Sil.Aeq(Exp.Const c1, Exp.Const c2) ->
@@ -1574,7 +1574,7 @@ let compute_reachable_hpreds sigma exps =
     [reachable_hpreds]. *)
 let get_fld_typ_path_opt src_exps snk_exp_ reachable_hpreds_ =
   let strexp_matches target_exp = function
-    | (_, Sil.Eexp (e, _)) -> Sil.exp_equal target_exp e
+    | (_, Sil.Eexp (e, _)) -> Exp.equal target_exp e
     | _ -> false in
   let extend_path hpred (snk_exp, path, reachable_hpreds) = match hpred with
     | Sil.Hpointsto (lhs, Sil.Estruct (flds, _), Exp.Sizeof (typ, _, _)) ->
@@ -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 (Sil.exp_equal e1 Sil.exp_zero) || (Sil.ExpSet.mem e1 alloc_set) ->
+      when (Exp.equal e1 Sil.exp_zero) || (Sil.ExpSet.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 (Sil.exp_equal iF Sil.exp_zero) || (Sil.ExpSet.mem iF alloc_set)
-           || (Sil.exp_equal iB Sil.exp_zero) || (Sil.ExpSet.mem iB alloc_set) ->
+      when (Exp.equal iF Sil.exp_zero) || (Sil.ExpSet.mem iF alloc_set)
+           || (Exp.equal iB Sil.exp_zero) || (Sil.ExpSet.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'
@@ -1662,16 +1662,16 @@ let sigma_intro_nonemptylseg e1 e2 sigma =
     | Sil.Hpointsto _ as hpred :: sigma' ->
         f (hpred :: sigma_passed) sigma'
     | Sil.Hlseg (Sil.Lseg_PE, para, f1, f2, shared) :: sigma'
-      when (Sil.exp_equal e1 f1 && Sil.exp_equal e2 f2)
-        || (Sil.exp_equal e2 f1 && Sil.exp_equal e1 f2) ->
+      when (Exp.equal e1 f1 && Exp.equal e2 f2)
+        || (Exp.equal e2 f1 && Exp.equal e1 f2) ->
         f (Sil.Hlseg (Sil.Lseg_NE, para, f1, f2, shared) :: sigma_passed) sigma'
     | Sil.Hlseg _ as hpred :: sigma' ->
         f (hpred :: sigma_passed) sigma'
     | Sil.Hdllseg (Sil.Lseg_PE, para, iF, oB, oF, iB, shared) :: sigma'
-      when (Sil.exp_equal e1 iF && Sil.exp_equal e2 oF)
-        || (Sil.exp_equal e2 iF && Sil.exp_equal e1 oF)
-        || (Sil.exp_equal e1 iB && Sil.exp_equal e2 oB)
-        || (Sil.exp_equal e2 iB && Sil.exp_equal e1 oB) ->
+      when (Exp.equal e1 iF && Exp.equal e2 oF)
+        || (Exp.equal e2 iF && Exp.equal e1 oF)
+        || (Exp.equal e1 iB && Exp.equal e2 oB)
+        || (Exp.equal e2 iB && Exp.equal e1 oB) ->
         f (Sil.Hdllseg (Sil.Lseg_NE, para, iF, oB, oF, iB, shared) :: sigma_passed) sigma'
     | Sil.Hdllseg _ as hpred :: sigma' ->
         f (hpred :: sigma_passed) sigma'
@@ -1716,7 +1716,7 @@ let rec prop_atom_and ?(footprint=false) (p : normal t) a : normal t =
           let (eqs_zero, nsigma'') = sigma_remove_emptylseg nsigma' in
           let p' = { p with sub = nsub'; pi = npi'; sigma = nsigma''} in
           IList.fold_left (prop_atom_and ~footprint) p' eqs_zero
-      | Sil.Aeq (e1, e2) when (Sil.exp_compare e1 e2 = 0) ->
+      | Sil.Aeq (e1, e2) when (Exp.compare e1 e2 = 0) ->
           p
       | Sil.Aneq (e1, e2) ->
           let sigma' = sigma_intro_nonemptylseg e1 e2 p.sigma in
@@ -1790,7 +1790,7 @@ let get_attributes prop exp =
   let nexp = exp_normalize_prop prop exp in
   let atom_get_attr attributes atom =
     match atom with
-    | Sil.Apred (_, es) | Anpred (_, es) when IList.mem Sil.exp_equal nexp es -> atom :: attributes
+    | Sil.Apred (_, es) | Anpred (_, es) when IList.mem Exp.equal nexp es -> atom :: attributes
     | _ -> attributes in
   IList.fold_left atom_get_attr [] prop.pi
 
@@ -1864,7 +1864,7 @@ let add_or_replace_attribute_check_changed check_attribute_change prop atom0 =
       let natom = Sil.atom_replace_exp (IList.combine exps0 nexps) atom0 in
       let atom_map = function
         | Sil.Apred (att, exp :: _) | Anpred (att, exp :: _)
-          when Sil.exp_equal nexp exp && attributes_in_same_category att att0 ->
+          when Exp.equal nexp exp && attributes_in_same_category att att0 ->
             check_attribute_change att att0;
             natom
         | atom ->
@@ -2089,7 +2089,7 @@ end = struct
 end
 
 let sigma_get_start_lexps_sort sigma =
-  let exp_compare_neg e1 e2 = - (Sil.exp_compare e1 e2) in
+  let exp_compare_neg e1 e2 = - (Exp.compare e1 e2) in
   let filter e = Sil.fav_for_all (Sil.exp_fav e) Ident.is_normal in
   let lexps = Sil.hpred_list_get_lexps filter sigma in
   IList.sort exp_compare_neg lexps
@@ -2114,14 +2114,14 @@ let sigma_dfs_sort sigma =
     | hpred :: cur ->
         begin
           match hpred with
-          | Sil.Hpointsto (e', se, _) when Sil.exp_equal e e' ->
+          | Sil.Hpointsto (e', se, _) when Exp.equal e e' ->
               handle_strexp se;
               (hpred:: visited, IList.rev_append cur seen)
-          | Sil.Hlseg (_, _, root, next, shared) when Sil.exp_equal e root ->
+          | Sil.Hlseg (_, _, root, next, shared) when Exp.equal e root ->
               IList.iter ExpStack.push (next:: shared);
               (hpred:: visited, IList.rev_append cur seen)
           | Sil.Hdllseg (_, _, iF, oB, oF, iB, shared)
-            when Sil.exp_equal e iF || Sil.exp_equal e iB ->
+            when Exp.equal e iF || Exp.equal e iB ->
               IList.iter ExpStack.push (oB:: oF:: shared);
               (hpred:: visited, IList.rev_append cur seen)
           | _ ->
@@ -2231,7 +2231,7 @@ let prop_rename_array_indices prop =
       match e1, e2 with
       | Exp.BinOp(Binop.PlusA, e1', Exp.Const (Const.Cint n1')),
         Exp.BinOp(Binop.PlusA, e2', Exp.Const (Const.Cint n2')) ->
-          not (Sil.exp_equal e1' e2' && IntLit.lt n1' n2')
+          not (Exp.equal e1' e2' && IntLit.lt n1' n2')
       | _ -> true in
     let rec select_minimal_indices indices_seen = function
       | [] -> IList.rev indices_seen
@@ -2819,7 +2819,7 @@ let find_equal_formal_path e prop =
           | None ->
               match hpred with
               | Sil.Hpointsto (Exp.Lvar pvar1, Sil.Eexp (exp2, Sil.Iformal(_, _) ), _)
-                when Sil.exp_equal exp2 e &&
+                when Exp.equal exp2 e &&
                      (Pvar.is_local pvar1 || Pvar.is_seed pvar1) ->
                   Some (Exp.Lvar pvar1)
               | Sil.Hpointsto (exp1, Sil.Estruct (fields, _), _) ->
@@ -2828,7 +2828,7 @@ let find_equal_formal_path e prop =
                       | Some _ -> res
                       | None ->
                           match strexp with
-                          | Sil.Eexp (exp2, _) when Sil.exp_equal exp2 e ->
+                          | Sil.Eexp (exp2, _) when Exp.equal exp2 e ->
                               (match find_in_sigma exp1 seen_hpreds with
                                | Some vfs -> Some (Exp.Lfield (vfs, field, Typ.Tvoid))
                                | None -> None)
@@ -3027,7 +3027,7 @@ let rec pp_ren pe f = function
   | (i, x):: ren -> F.fprintf f "%a->%a, %a" (Ident.pp pe) i (Ident.pp pe) x (pp_ren pe) ren
 
 let id_exp_compare (id1, e1) (id2, e2) =
-  let n = Sil.exp_compare e1 e2 in
+  let n = Exp.compare e1 e2 in
   if n <> 0 then n
   else Ident.compare id1 id2
 
diff --git a/infer/src/backend/propgraph.ml b/infer/src/backend/propgraph.ml
index 609de577e..ffd697f99 100644
--- a/infer/src/backend/propgraph.ml
+++ b/infer/src/backend/propgraph.ml
@@ -34,7 +34,7 @@ let rec is_root = function
 
 (** Return [true] if the nodes are connected. Used to compute reachability. *)
 let nodes_connected n1 n2 =
-  Sil.exp_equal n1 n2 (* Implemented as equality for now, later it might contain offset by a constant *)
+  Exp.equal n1 n2 (* Implemented as equality for now, later it might contain offset by a constant *)
 
 (** Return [true] if the edge is an hpred, and [false] if it is an atom *)
 let edge_is_hpred = function
@@ -77,7 +77,7 @@ let edge_from_source g n footprint_part is_hpred =
     else IList.map (fun a -> Eatom a) (get_pi footprint_part g) @ IList.map (fun entry -> Esub_entry entry) (get_subl footprint_part g) in
   let starts_from hpred =
     match edge_get_source hpred with
-    | Some e -> Sil.exp_equal n e
+    | Some e -> Exp.equal n e
     | None -> false in
   match IList.filter starts_from edges with
   | [] -> None
@@ -100,7 +100,7 @@ let get_edges footprint_part g =
 let edge_equal e1 e2 = match e1, e2 with
   | Ehpred hp1, Ehpred hp2 -> Sil.hpred_equal hp1 hp2
   | Eatom a1, Eatom a2 -> Sil.atom_equal a1 a2
-  | Esub_entry (x1, e1), Esub_entry (x2, e2) -> Ident.equal x1 x2 && Sil.exp_equal e1 e2
+  | Esub_entry (x1, e1), Esub_entry (x2, e2) -> Ident.equal x1 x2 && Exp.equal e1 e2
   | _ -> false
 
 (** [contains_edge footprint_part g e] returns true if the graph [g] contains edge [e],
@@ -124,12 +124,12 @@ type diff =
 
 (** Compute the subobjects in [e2] which are different from those in [e1] *)
 let compute_exp_diff (e1: Exp.t) (e2: Exp.t) : Obj.t list =
-  if Sil.exp_equal e1 e2 then [] else [Obj.repr e2]
+  if Exp.equal e1 e2 then [] else [Obj.repr e2]
 
 
 (** Compute the subobjects in [se2] which are different from those in [se1] *)
 let rec compute_sexp_diff (se1: Sil.strexp) (se2: Sil.strexp) : Obj.t list = match se1, se2 with
-  | Sil.Eexp (e1, _), Sil.Eexp (e2, _) -> if Sil.exp_equal e1 e2 then [] else [Obj.repr se2]
+  | Sil.Eexp (e1, _), Sil.Eexp (e2, _) -> if Exp.equal e1 e2 then [] else [Obj.repr se2]
   | Sil.Estruct (fsel1, _), Sil.Estruct (fsel2, _) ->
       compute_fsel_diff fsel1 fsel2
   | Sil.Earray (e1, esel1, _), Sil.Earray (e2, esel2, _) ->
@@ -148,7 +148,7 @@ and compute_fsel_diff fsel1 fsel2 : Obj.t list = match fsel1, fsel2 with
 
 and compute_esel_diff esel1 esel2 : Obj.t list = match esel1, esel2 with
   | ((e1, se1):: esel1'), (((e2, se2) as x):: esel2') ->
-      (match Sil.exp_compare e1 e2 with
+      (match Exp.compare e1 e2 with
        | n when n < 0 -> compute_esel_diff esel1' esel2
        | 0 -> compute_sexp_diff se1 se2 @ compute_esel_diff esel1' esel2'
        | _ -> (Obj.repr x) :: compute_esel_diff esel1 esel2')
diff --git a/infer/src/backend/prover.ml b/infer/src/backend/prover.ml
index 74f2fd627..cbe530aba 100644
--- a/infer/src/backend/prover.ml
+++ b/infer/src/backend/prover.ml
@@ -26,8 +26,8 @@ let compute_min_from_nonempty_int_list l =
   IList.hd (IList.sort IntLit.compare_value l)
 
 let exp_pair_compare (e1, e2) (f1, f2) =
-  let c1 = Sil.exp_compare e1 f1 in
-  if c1 <> 0 then c1 else Sil.exp_compare e2 f2
+  let c1 = Exp.compare e1 f1 in
+  if c1 <> 0 then c1 else Exp.compare e2 f2
 
 let rec list_rev_acc acc = function
   | [] -> acc
@@ -102,8 +102,8 @@ end = struct
   let rec generate ((e1, e2, n) as constr) acc = function
     | [] -> false, acc
     | (f1, f2, m):: rest ->
-        let equal_e2_f1 = Sil.exp_equal e2 f1 in
-        let equal_e1_f2 = Sil.exp_equal e1 f2 in
+        let equal_e2_f1 = Exp.equal e2 f1 in
+        let equal_e1_f2 = Exp.equal e1 f2 in
         if equal_e2_f1 && equal_e1_f2 && IntLit.lt (n ++ m) IntLit.zero then
           true, [] (* constraints are inconsistent *)
         else if equal_e2_f1 && equal_e1_f2 then
@@ -256,18 +256,18 @@ end = struct
   let inconsistent_ineq = { leqs = [(Sil.exp_one, Sil.exp_zero)]; lts = []; neqs = [] }
 
   let leq_compare (e1, e2) (f1, f2) =
-    let c1 = Sil.exp_compare e1 f1 in
-    if c1 <> 0 then c1 else Sil.exp_compare e2 f2
+    let c1 = Exp.compare e1 f1 in
+    if c1 <> 0 then c1 else Exp.compare e2 f2
   let lt_compare (e1, e2) (f1, f2) =
-    let c2 = Sil.exp_compare e2 f2 in
-    if c2 <> 0 then c2 else - (Sil.exp_compare e1 f1)
+    let c2 = Exp.compare e2 f2 in
+    if c2 <> 0 then c2 else - (Exp.compare e1 f1)
 
   let leqs_sort_then_remove_redundancy leqs =
     let leqs_sorted = IList.sort leq_compare leqs in
     let have_same_key leq1 leq2 =
       match leq1, leq2 with
       | (e1, Exp.Const (Const.Cint n1)), (e2, Exp.Const (Const.Cint n2)) ->
-          Sil.exp_equal e1 e2 && IntLit.leq n1 n2
+          Exp.equal e1 e2 && IntLit.leq n1 n2
       | _, _ -> false in
     remove_redundancy have_same_key [] leqs_sorted
   let lts_sort_then_remove_redundancy lts =
@@ -275,7 +275,7 @@ end = struct
     let have_same_key lt1 lt2 =
       match lt1, lt2 with
       | (Exp.Const (Const.Cint n1), e1), (Exp.Const (Const.Cint n2), e2) ->
-          Sil.exp_equal e1 e2 && IntLit.geq n1 n2
+          Exp.equal e1 e2 && IntLit.geq n1 n2
       | _, _ -> false in
     remove_redundancy have_same_key [] lts_sorted
 
@@ -411,7 +411,7 @@ end = struct
 
   (** Return true if the two pairs of expressions are equal *)
   let exp_pair_eq (e1, e2) (f1, f2) =
-    Sil.exp_equal e1 f1 && Sil.exp_equal e2 f2
+    Exp.equal e1 f1 && Exp.equal e2 f2
 
   (** Check [t |- e1<=e2]. Result [false] means "don't know". *)
   let check_le { leqs = leqs; lts = lts; neqs = _ } e1 e2 =
@@ -425,13 +425,13 @@ end = struct
         check_type_size_lt t1 t2
     | e, Exp.Const (Const.Cint n) -> (* [e <= n' <= n |- e <= n] *)
         IList.exists (function
-            | e', Exp.Const (Const.Cint n') -> Sil.exp_equal e e' && IntLit.leq n' n
+            | e', Exp.Const (Const.Cint n') -> Exp.equal e e' && IntLit.leq n' n
             | _, _ -> false) leqs
     | Exp.Const (Const.Cint n), e -> (* [ n-1 <= n' < e |- n <= e] *)
         IList.exists (function
-            | Exp.Const (Const.Cint n'), e' -> Sil.exp_equal e e' && IntLit.leq (n -- IntLit.one) n'
+            | Exp.Const (Const.Cint n'), e' -> Exp.equal e e' && IntLit.leq (n -- IntLit.one) n'
             | _, _ -> false) lts
-    | _ -> Sil.exp_equal e1 e2
+    | _ -> Exp.equal e1 e2
 
   (** Check [prop |- e1<e2]. Result [false] means "don't know". *)
   let check_lt { leqs = leqs; lts = lts; neqs = _ } e1 e2 =
@@ -440,17 +440,17 @@ end = struct
     | Exp.Const (Const.Cint n1), Exp.Const (Const.Cint n2) -> IntLit.lt n1 n2
     | Exp.Const (Const.Cint n), e -> (* [n <= n' < e  |- n < e] *)
         IList.exists (function
-            | Exp.Const (Const.Cint n'), e' -> Sil.exp_equal e e' && IntLit.leq n n'
+            | Exp.Const (Const.Cint n'), e' -> Exp.equal e e' && IntLit.leq n n'
             | _, _ -> false) lts
     | e, Exp.Const (Const.Cint n) -> (* [e <= n' <= n-1 |- e < n] *)
         IList.exists (function
-            | e', Exp.Const (Const.Cint n') -> Sil.exp_equal e e' && IntLit.leq n' (n -- IntLit.one)
+            | e', Exp.Const (Const.Cint n') -> Exp.equal e e' && IntLit.leq n' (n -- IntLit.one)
             | _, _ -> false) leqs
     | _ -> false
 
   (** Check [prop |- e1!=e2]. Result [false] means "don't know". *)
   let check_ne ineq _e1 _e2 =
-    let e1, e2 = if Sil.exp_compare _e1 _e2 <= 0 then _e1, _e2 else _e2, _e1 in
+    let e1, e2 = if Exp.compare _e1 _e2 <= 0 then _e1, _e2 else _e2, _e1 in
     IList.exists (exp_pair_eq (e1, e2)) ineq.neqs || check_lt ineq e1 e2 || check_lt ineq e2 e1
 
   (** Find a IntLit.t n such that [t |- e<=n] if possible. *)
@@ -460,7 +460,7 @@ end = struct
     | _ ->
         let e_upper_list =
           IList.filter (function
-              | e', Exp.Const (Const.Cint _) -> Sil.exp_equal e1 e'
+              | e', Exp.Const (Const.Cint _) -> Exp.equal e1 e'
               | _, _ -> false) leqs in
         let upper_list =
           IList.map (function
@@ -477,7 +477,7 @@ end = struct
     | _ ->
         let e_lower_list =
           IList.filter (function
-              | Exp.Const (Const.Cint _), e' -> Sil.exp_equal e1 e'
+              | Exp.Const (Const.Cint _), e' -> Exp.equal e1 e'
               | _, _ -> false) lts in
         let lower_list =
           IList.map (function
@@ -524,12 +524,12 @@ let check_equal prop e1 e2 =
   let n_e1 = Prop.exp_normalize_prop prop e1 in
   let n_e2 = Prop.exp_normalize_prop prop e2 in
   let check_equal () =
-    Sil.exp_equal n_e1 n_e2 in
+    Exp.equal n_e1 n_e2 in
   let check_equal_const () =
     match n_e1, n_e2 with
     | Exp.BinOp (Binop.PlusA, e1, Exp.Const (Const.Cint d)), e2
     | e2, Exp.BinOp (Binop.PlusA, e1, Exp.Const (Const.Cint d)) ->
-        if Sil.exp_equal e1 e2 then IntLit.iszero d
+        if Exp.equal e1 e2 then IntLit.iszero d
         else false
     | Exp.Const c1, Exp.Lindex(Exp.Const c2, Exp.Const (Const.Cint i)) when IntLit.iszero i ->
         Const.equal c1 c2
@@ -597,11 +597,11 @@ let check_disequal prop e1 e2 =
         else Const.equal c1 c2 (* same base, different offsets *)
     | Exp.BinOp (Binop.PlusA, e1, Exp.Const (Const.Cint d1)),
       Exp.BinOp (Binop.PlusA, e2, Exp.Const (Const.Cint d2)) ->
-        if Sil.exp_equal e1 e2 then IntLit.neq d1 d2
+        if Exp.equal e1 e2 then IntLit.neq d1 d2
         else false
     | Exp.BinOp (Binop.PlusA, e1, Exp.Const (Const.Cint d)), e2
     | e2, Exp.BinOp (Binop.PlusA, e1, Exp.Const (Const.Cint d)) ->
-        if Sil.exp_equal e1 e2 then not (IntLit.iszero d)
+        if Exp.equal e1 e2 then not (IntLit.iszero d)
         else false
     | Exp.Lindex(Exp.Const c1, Exp.Const (Const.Cint d)), Exp.Const c2 ->
         if IntLit.iszero d then not (Const.equal c1 c2) else Const.equal c1 c2
@@ -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 (Sil.exp_equal e2 Sil.exp_zero) then
+               else if (Exp.equal e2 Sil.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 (Sil.exp_equal oF Sil.exp_zero) then
+               else if (Exp.equal oF Sil.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 (Sil.exp_equal e Sil.exp_zero) then f sigma_irrelevant e sigma_rest
+      if not (Exp.equal e Sil.exp_zero) then f sigma_irrelevant e sigma_rest
       else
         let sigma_irrelevant' = (IList.rev sigma_irrelevant) @ sigma_rest
         in Some (false, sigma_irrelevant')
@@ -679,7 +679,7 @@ let check_le_normalized prop e1 e2 =
   (* L.d_str "check_le_normalized "; Sil.d_exp e1; L.d_str " "; Sil.d_exp e2; L.d_ln (); *)
   let eL, eR, off = match e1, e2 with
     | Exp.BinOp(Binop.MinusA, f1, f2), Exp.Const (Const.Cint n) ->
-        if Sil.exp_equal f1 f2
+        if Exp.equal f1 f2
         then Sil.exp_zero, Sil.exp_zero, n
         else f1, f2, n
     | _ ->
@@ -777,17 +777,17 @@ let check_inconsistency_two_hpreds prop =
     | [] -> false
     | (Sil.Hpointsto (e1, _, _) as hpred) :: sigma_rest
     | (Sil.Hlseg (Sil.Lseg_NE, _, e1, _, _) as hpred) :: sigma_rest ->
-        if Sil.exp_equal e1 e then true
+        if Exp.equal e1 e then true
         else f e (hpred:: sigma_seen) sigma_rest
     | (Sil.Hdllseg (Sil.Lseg_NE, _, iF, _, _, iB, _) as hpred) :: sigma_rest ->
-        if Sil.exp_equal iF e || Sil.exp_equal iB e then true
+        if Exp.equal iF e || Exp.equal iB e then true
         else f e (hpred:: sigma_seen) sigma_rest
     | Sil.Hlseg (Sil.Lseg_PE, _, e1, Exp.Const (Const.Cint i), _) as hpred :: sigma_rest
       when IntLit.iszero i ->
-        if Sil.exp_equal e1 e then true
+        if Exp.equal e1 e then true
         else f e (hpred:: sigma_seen) sigma_rest
     | Sil.Hlseg (Sil.Lseg_PE, _, e1, e2, _) as hpred :: sigma_rest ->
-        if Sil.exp_equal e1 e
+        if Exp.equal e1 e
         then
           let prop' = Prop.normalize (Prop.from_sigma (sigma_seen@sigma_rest)) in
           let prop_new = Prop.conjoin_eq e1 e2 prop' in
@@ -797,10 +797,10 @@ let check_inconsistency_two_hpreds prop =
         else f e (hpred:: sigma_seen) sigma_rest
     | Sil.Hdllseg (Sil.Lseg_PE, _, e1, _, Exp.Const (Const.Cint i), _, _) as hpred :: sigma_rest
       when IntLit.iszero i ->
-        if Sil.exp_equal e1 e then true
+        if Exp.equal e1 e then true
         else f e (hpred:: sigma_seen) sigma_rest
     | Sil.Hdllseg (Sil.Lseg_PE, _, e1, _, e3, _, _) as hpred :: sigma_rest ->
-        if Sil.exp_equal e1 e
+        if Exp.equal e1 e
         then
           let prop' = Prop.normalize (Prop.from_sigma (sigma_seen@sigma_rest)) in
           let prop_new = Prop.conjoin_eq e1 e3 prop' 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, _), _) ->
-          Sil.exp_equal e Sil.exp_zero &&
+          Exp.equal e Sil.exp_zero &&
           Pvar.is_seed pv &&
           (is_java_this pv || is_cpp_this pv || is_objc_instance_self pv)
       | _ -> false in
@@ -858,7 +858,7 @@ let check_inconsistency_base prop =
     | Sil.Aneq (e1, e2) ->
         (match e1, e2 with
          | Exp.Const c1, Exp.Const c2 -> Const.equal c1 c2
-         | _ -> (Sil.exp_compare e1 e2 = 0))
+         | _ -> (Exp.compare e1 e2 = 0))
     | Sil.Apred _ | Anpred _ -> false in
   let inconsistent_inequalities () =
     let ineq = Inequalities.from_prop prop in
@@ -1344,7 +1344,7 @@ and array_imply source calc_index_frame calc_missing subs esel1 esel2 typ2
   | (e1, se1) :: esel1', (e2, se2) :: esel2' ->
       let e1n = Prop.exp_normalize_noabs (fst subs) e1 in
       let e2n = Prop.exp_normalize_noabs (snd subs) e2 in
-      let n = Sil.exp_compare e1n e2n in
+      let n = Exp.compare e1n e2n in
       if n < 0 then array_imply source calc_index_frame calc_missing subs esel1' esel2 typ2
       else if n > 0 then array_imply source calc_index_frame calc_missing subs esel1 esel2' typ2
       else (* n=0 *)
@@ -1391,10 +1391,11 @@ let rec exp_list_imply calc_missing subs l1 l2 = match l1, l2 with
   | _ -> assert false
 
 let filter_ne_lhs sub e0 = function
-  | Sil.Hpointsto (e, _, _) -> if Sil.exp_equal e0 (Sil.exp_sub sub e) then Some () else None
-  | Sil.Hlseg (Sil.Lseg_NE, _, e, _, _) -> if Sil.exp_equal e0 (Sil.exp_sub sub e) then Some () else None
+  | Sil.Hpointsto (e, _, _) -> if Exp.equal e0 (Sil.exp_sub sub e) then Some () else None
+  | Sil.Hlseg (Sil.Lseg_NE, _, e, _, _) ->
+      if Exp.equal e0 (Sil.exp_sub sub e) then Some () else None
   | Sil.Hdllseg (Sil.Lseg_NE, _, e, _, _, e', _) ->
-      if Sil.exp_equal e0 (Sil.exp_sub sub e) || Sil.exp_equal e0 (Sil.exp_sub sub e')
+      if Exp.equal e0 (Sil.exp_sub sub e) || Exp.equal e0 (Sil.exp_sub sub e')
       then Some ()
       else None
   | _ -> None
@@ -1405,7 +1406,7 @@ let filter_hpred sub hpred2 hpred1 = match (Sil.hpred_sub sub hpred1), hpred2 wi
   | Sil.Hlseg(Sil.Lseg_PE, hpara1, e1, f1, el1), Sil.Hlseg(Sil.Lseg_NE, _, _, _, _) ->
       if Sil.hpred_equal (Sil.Hlseg(Sil.Lseg_NE, hpara1, e1, f1, el1)) hpred2 then Some true else None (* return missing disequality *)
   | Sil.Hpointsto(e1, _, _), Sil.Hlseg(_, _, e2, _, _) ->
-      if Sil.exp_equal e1 e2 then Some false else None
+      if Exp.equal e1 e2 then Some false else None
   | hpred1, hpred2 -> if Sil.hpred_equal hpred1 hpred2 then Some false else None
 
 let hpred_has_primed_lhs sub hpred =
@@ -1661,9 +1662,9 @@ let get_overrides_of tenv supertype pname =
 let texp_equal_modulo_subtype_flag texp1 texp2 = match texp1, texp2 with
   | Exp.Sizeof (t1, len1, st1), Exp.Sizeof (t2, len2, st2) ->
       Typ.equal t1 t2
-      && (opt_equal Sil.exp_equal len1 len2)
+      && (opt_equal Exp.equal len1 len2)
       && Subtype.equal_modulo_flag st1 st2
-  | _ -> Sil.exp_equal texp1 texp2
+  | _ -> Exp.equal texp1 texp2
 
 (** check implication between type expressions *)
 let texp_imply tenv subs texp1 texp2 e1 calc_missing =
@@ -1725,13 +1726,13 @@ let handle_parameter_subtype tenv prop1 sigma2 subs (e1, se1, texp1) (se2, texp2
     | _ -> false in
   let is_allocated_lhs e =
     let filter = function
-      | Sil.Hpointsto(e', _, _) -> Sil.exp_equal e' e
+      | Sil.Hpointsto(e', _, _) -> Exp.equal e' e
       | _ -> false in
     IList.exists filter (Prop.get_sigma prop1) in
   let type_rhs e =
     let sub_opt = ref None in
     let filter = function
-      | Sil.Hpointsto(e', _, Exp.Sizeof(t, len, sub)) when Sil.exp_equal e' e ->
+      | Sil.Hpointsto(e', _, Exp.Sizeof(t, len, sub)) when Exp.equal e' e ->
           sub_opt := Some (t, len, sub);
           true
       | _ -> false in
@@ -1820,7 +1821,7 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2
                      L.d_decrease_indent 1;
                      res
                  | Sil.Hdllseg (Sil.Lseg_NE, para1, iF1, oB1, oF1, iB1, elist1), _
-                   when Sil.exp_equal (Sil.exp_sub (fst subs) iF1) e2 -> (* Unroll dllseg forward *)
+                   when Exp.equal (Sil.exp_sub (fst subs) iF1) e2 -> (* Unroll dllseg forward *)
                      let n' = Exp.Var (Ident.create_fresh Ident.kprimed) in
                      let (_, para_inst1) = Sil.hpara_dll_instantiate para1 iF1 oB1 n' elist1 in
                      let hpred_list1 = para_inst1@[Prop.mk_dllseg Sil.Lseg_PE para1 n' iF1 oF1 iB1 elist1] in
@@ -1832,8 +1833,7 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2
                      L.d_decrease_indent 1;
                      res
                  | Sil.Hdllseg (Sil.Lseg_NE, para1, iF1, oB1, oF1, iB1, elist1), _
-                   when Sil.exp_equal (Sil.exp_sub (fst subs) iB1) e2 ->
-                     (* Unroll dllseg backward *)
+                   when Exp.equal (Sil.exp_sub (fst subs) iB1) e2 -> (* Unroll dllseg backward *)
                      let n' = Exp.Var (Ident.create_fresh Ident.kprimed) in
                      let (_, para_inst1) = Sil.hpara_dll_instantiate para1 iB1 n' oF1 elist1 in
                      let hpred_list1 = para_inst1@[Prop.mk_dllseg Sil.Lseg_PE para1 iF1 oB1 iB1 n' elist1] in
@@ -1857,7 +1857,7 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2
                raise (Exceptions.Abduction_case_not_implemented __POS__))
         | _ -> ()
       in
-      if Sil.exp_equal e2 f2 && k == Sil.Lseg_PE then (subs, prop1)
+      if Exp.equal e2 f2 && k == Sil.Lseg_PE then (subs, prop1)
       else
         (match Prop.prop_iter_create prop1 with
          | None -> raise (IMPL_EXC ("lhs is empty", subs, EXC_FALSE))
@@ -1932,7 +1932,7 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2
             | None ->
                 let elist2 = IList.map (fun e -> Sil.exp_sub (snd subs) e) elist2 in
                 let _, para_inst2 =
-                  if Sil.exp_equal iF2 iB2 then
+                  if Exp.equal iF2 iB2 then
                     Sil.hpara_dll_instantiate para2 iF2 oB2 oF2 elist2
                   else assert false (* Only base case of rhs list considered for now *) in
                 L.d_increase_indent 1;
@@ -2094,7 +2094,7 @@ let rec pre_check_pure_implication calc_missing subs pi1 pi2 =
   | [] -> subs
   | (Sil.Aeq (e2_in, f2_in) as a) :: pi2' when not (Prop.atom_is_inequality a) ->
       let e2, f2 = Sil.exp_sub (snd subs) e2_in, Sil.exp_sub (snd subs) f2_in in
-      if Sil.exp_equal e2 f2 then pre_check_pure_implication calc_missing subs pi1 pi2'
+      if Exp.equal e2 f2 then pre_check_pure_implication calc_missing subs pi1 pi2'
       else
         (match e2, f2 with
          | Exp.Var v2, f2
@@ -2275,6 +2275,6 @@ let check_lt prop e1 e2 =
   check_atom prop (Prop.mk_inequality e1_lt_e2)
 
 let filter_ptsto_lhs sub e0 = function
-  | Sil.Hpointsto (e, _, _) -> if Sil.exp_equal e0 (Sil.exp_sub sub e) then Some () else None
+  | Sil.Hpointsto (e, _, _) -> if Exp.equal e0 (Sil.exp_sub sub e) then Some () else None
   | _ -> None
 *)
diff --git a/infer/src/backend/rearrange.ml b/infer/src/backend/rearrange.ml
index e37208152..d46222401 100644
--- a/infer/src/backend/rearrange.ml
+++ b/infer/src/backend/rearrange.ml
@@ -265,12 +265,12 @@ let rec _strexp_extend_values
       bounds_check pname orig_prop len e (State.get_loc ());
       begin
         try
-          let _, se' = IList.find (fun (e', _) -> Sil.exp_equal e e') esel in
+          let _, se' = IList.find (fun (e', _) -> Exp.equal e e') esel in
           let atoms_se_typ_list' =
             _strexp_extend_values
               pname tenv orig_prop footprint_part kind max_stamp se' typ' off' inst in
           let replace acc (res_atoms', res_se', res_typ') =
-            let replace_ise ise = if Sil.exp_equal e (fst ise) then (e, res_se') else ise in
+            let replace_ise ise = if Exp.equal e (fst ise) then (e, res_se') else ise in
             let res_esel' = IList.map replace_ise esel in
             if (Typ.equal res_typ' typ') || (IList.length res_esel' = 1) then
               ( res_atoms'
@@ -544,10 +544,10 @@ let prop_iter_extend_ptsto pname tenv orig_prop iter lexp inst =
           let footprint_sigma = Prop.prop_iter_get_footprint_sigma iter in
           let sigma_pto, sigma_rest =
             IList.partition (function
-                | Sil.Hpointsto(e', _, _) -> Sil.exp_equal e e'
-                | Sil.Hlseg (_, _, e1, _, _) -> Sil.exp_equal e e1
+                | Sil.Hpointsto(e', _, _) -> Exp.equal e e'
+                | Sil.Hlseg (_, _, e1, _, _) -> Exp.equal e e1
                 | Sil.Hdllseg (_, _, e_iF, _, _, e_iB, _) ->
-                    Sil.exp_equal e e_iF || Sil.exp_equal e e_iB
+                    Exp.equal e e_iF || Exp.equal e e_iB
               ) footprint_sigma in
           let atoms_sigma_list =
             match sigma_pto with
@@ -756,12 +756,12 @@ let add_guarded_by_constraints prop lexp pdesc =
         IList.exists
           (function
             | Sil.Hpointsto (Lvar _, Eexp (rhs_exp, _), _) ->
-                Sil.exp_equal exp rhs_exp
+                Exp.equal exp rhs_exp
             | Sil.Hpointsto (_, Estruct (flds, _), _) ->
                 IList.exists
                   (fun (fld, strexp) -> match strexp with
                      | Sil.Eexp (rhs_exp, _) ->
-                         Sil.exp_equal exp rhs_exp && not (Ident.fieldname_equal fld accessed_fld)
+                         Exp.equal exp rhs_exp && not (Ident.fieldname_equal fld accessed_fld)
                      | _ ->
                          false)
                   flds
@@ -811,7 +811,7 @@ let add_guarded_by_constraints prop lexp pdesc =
     | Some guarded_by_fld_str -> enforce_guarded_access_ fld guarded_by_fld_str prop
     | None -> prop in
   let check_fld_locks typ prop_acc (fld, strexp) = match strexp with
-    | Sil.Eexp (exp, _) when Sil.exp_equal exp lexp -> enforce_guarded_access fld typ prop_acc
+    | Sil.Eexp (exp, _) when Exp.equal exp lexp -> enforce_guarded_access fld typ prop_acc
     | _ -> prop_acc in
   let hpred_check_flds prop_acc = function
     | Sil.Hpointsto (_, Estruct (flds, _), Sizeof (typ, _, _)) ->
@@ -1188,7 +1188,7 @@ let check_dereference_error pdesc (prop : Prop.normal Prop.t) lexp loc =
       (fun hpred ->
          match hpred with
          | Sil.Hpointsto (Exp.Lvar pvar, Sil.Eexp (Exp.Var _ as exp, _), _)
-           when Sil.exp_equal exp deref_exp ->
+           when Exp.equal exp deref_exp ->
              let is_weak_captured_var = is_weak_captured_var pdesc pvar in
              let is_nullable =
                if Annotations.param_is_nullable pvar ann_sig || is_weak_captured_var
@@ -1215,7 +1215,7 @@ let check_dereference_error pdesc (prop : Prop.normal Prop.t) lexp loc =
                | _ -> false in
              let is_strexp_pt_by_nullable_fld (fld, strexp) =
                match strexp with
-               | Sil.Eexp (Exp.Var _ as exp, _) when Sil.exp_equal exp deref_exp ->
+               | Sil.Eexp (Exp.Var _ as exp, _) when Exp.equal exp deref_exp ->
                    let is_nullable = fld_is_nullable fld in
                    if is_nullable then
                      nullable_obj_str := Some (Ident.fieldname_to_simplified_string fld);
diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml
index 0a6e7b271..d8abd7e53 100644
--- a/infer/src/backend/symExec.ml
+++ b/infer/src/backend/symExec.ml
@@ -184,7 +184,7 @@ let rec apply_offlist
               pdesc tenv p fp_root nullify_struct
               (root_lexp, se', t') offlist' f inst lookup_inst in
           let replace_ese ese =
-            if Sil.exp_equal idx_ese' (fst ese)
+            if Exp.equal idx_ese' (fst ese)
             then (idx_ese', res_se')
             else ese in
           let res_se = Sil.Earray (len, IList.map replace_ese esel, inst1) in
@@ -288,7 +288,7 @@ let prune_ne ~positive e1 e2 prop =
     is "<" if [is_strict] is true and "<=" if [is_strict] is false.
 *)
 let prune_ineq ~is_strict ~positive prop e1 e2 =
-  if Sil.exp_equal e1 e2 then
+  if Exp.equal e1 e2 then
     if (positive && not is_strict) || (not positive && is_strict) then
       Propset.singleton prop
     else Propset.empty
@@ -439,7 +439,7 @@ let check_arith_norm_exp pname exp prop =
 let check_already_dereferenced pname cond prop =
   let find_hpred lhs =
     try Some (IList.find (function
-        | Sil.Hpointsto (e, _, _) -> Sil.exp_equal e lhs
+        | Sil.Hpointsto (e, _, _) -> Exp.equal e lhs
         | _ -> false) (Prop.get_sigma prop))
     with Not_found -> None in
   let rec is_check_zero = function
@@ -530,7 +530,7 @@ let resolve_typename prop receiver_exp =
   let typexp_opt =
     let rec loop = function
       | [] -> None
-      | Sil.Hpointsto(e, _, typexp) :: _ when Sil.exp_equal e receiver_exp -> Some typexp
+      | Sil.Hpointsto(e, _, typexp) :: _ when Exp.equal e receiver_exp -> Some typexp
       | _ :: hpreds -> loop hpreds in
     loop (Prop.get_sigma prop) in
   match typexp_opt with
@@ -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 Sil.exp_equal e Sil.exp_zero ||
+      when Exp.equal e Sil.exp_zero ||
            Option.is_some (Prop.get_objc_null_attribute pre e) -> true
     | _ -> false in
   let add_objc_null_attribute_or_nullify_result prop =
@@ -1285,7 +1285,7 @@ and add_constraints_on_actuals_by_ref tenv prop actuals_by_ref callee_pname call
     let sigma' =
       IList.map
         (function
-          | Sil.Hpointsto (lhs, _, _) when Sil.exp_equal lhs actual_var -> new_hpred
+          | Sil.Hpointsto (lhs, _, _) when Exp.equal lhs actual_var -> new_hpred
           | hpred -> hpred)
         (Prop.get_sigma prop) in
     Prop.normalize (Prop.replace_sigma sigma' prop) in
@@ -1324,7 +1324,7 @@ and add_constraints_on_actuals_by_ref tenv prop actuals_by_ref callee_pname call
             let filtered_sigma =
               IList.map
                 (function
-                  | Sil.Hpointsto (lhs, _, typ_exp) when Sil.exp_equal lhs actual ->
+                  | Sil.Hpointsto (lhs, _, typ_exp) when Exp.equal lhs actual ->
                       Sil.Hpointsto (lhs, abduced_strexp, typ_exp)
                   | hpred -> hpred)
                 (Prop.get_sigma prop') in
@@ -1335,7 +1335,7 @@ and add_constraints_on_actuals_by_ref tenv prop actuals_by_ref callee_pname call
               let filtered_sigma =
                 IList.filter
                   (function
-                    | Sil.Hpointsto (lhs, _, _) when Sil.exp_equal lhs actual ->
+                    | Sil.Hpointsto (lhs, _, _) when Exp.equal lhs actual ->
                         false
                     | _ -> true)
                   (Prop.get_sigma prop) in
diff --git a/infer/src/backend/tabulation.ml b/infer/src/backend/tabulation.ml
index 83b3c1bd4..6542d7851 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 Sil.exp_equal e_sub Sil.exp_zero then
+      if Exp.equal e_sub Sil.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 Sil.exp_equal e_sub Sil.exp_minus_one
+    else if Exp.equal e_sub Sil.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), _)) ->
@@ -401,7 +401,7 @@ let post_process_post
   post', post_path
 
 let hpred_lhs_compare hpred1 hpred2 = match hpred1, hpred2 with
-  | Sil.Hpointsto(e1, _, _), Sil.Hpointsto(e2, _, _) -> Sil.exp_compare e1 e2
+  | Sil.Hpointsto(e1, _, _), Sil.Hpointsto(e2, _, _) -> Exp.compare e1 e2
   | Sil.Hpointsto _, _ -> - 1
   | _, Sil.Hpointsto _ -> 1
   | hpred1, hpred2 -> Sil.hpred_compare hpred1 hpred2
@@ -433,7 +433,7 @@ and esel_star_fld esel1 esel2 = match esel1, esel2 with
       IList.map (fun (e, se) -> (e, sexp_set_inst Sil.Inone se)) esel2
   | esel1,[] -> esel1
   | (e1, se1):: esel1', (e2, se2):: esel2' ->
-      (match Sil.exp_compare e1 e2 with
+      (match Exp.compare e1 e2 with
        | 0 -> (e1, array_content_star se1 se2) :: esel_star_fld esel1' esel2'
        | n when n < 0 -> (e1, se1) :: esel_star_fld esel1' esel2
        | _ ->
@@ -510,7 +510,7 @@ let sigma_star_fld (sigma1 : Sil.hpred list) (sigma2 : Sil.hpred list) : Sil.hpr
     raise (Prop.Cannot_star __POS__)
 
 let hpred_typing_lhs_compare hpred1 (e2, _) = match hpred1 with
-  | Sil.Hpointsto(e1, _, _) -> Sil.exp_compare e1 e2
+  | Sil.Hpointsto(e1, _, _) -> Exp.compare e1 e2
   | _ -> - 1
 
 let hpred_star_typing (hpred1 : Sil.hpred) (_, te2) : Sil.hpred =
@@ -521,7 +521,7 @@ let hpred_star_typing (hpred1 : Sil.hpred) (_, te2) : Sil.hpred =
 (** Implementation of [*] between predicates and typings *)
 let sigma_star_typ
     (sigma1 : Sil.hpred list) (typings2 : (Exp.t * Exp.t) list) : Sil.hpred list =
-  let typing_lhs_compare (e1, _) (e2, _) = Sil.exp_compare e1 e2 in
+  let typing_lhs_compare (e1, _) (e2, _) = Exp.compare e1 e2 in
   let sigma1 = IList.stable_sort hpred_lhs_compare sigma1 in
   let typings2 = IList.stable_sort typing_lhs_compare typings2 in
   let rec star sg1 typ2 : Sil.hpred list =
@@ -618,7 +618,7 @@ let exp_is_exn = function
 let prop_is_exn pname prop =
   let ret_pvar = Exp.Lvar (Pvar.get_ret_pvar pname) in
   let is_exn = function
-    | Sil.Hpointsto (e1, Sil.Eexp(e2, _), _) when Sil.exp_equal e1 ret_pvar ->
+    | Sil.Hpointsto (e1, Sil.Eexp(e2, _), _) when Exp.equal e1 ret_pvar ->
         exp_is_exn e2
     | _ -> false in
   IList.exists is_exn (Prop.get_sigma prop)
@@ -629,13 +629,13 @@ let prop_get_exn_name pname prop =
   let rec search_exn e = function
     | [] -> None
     | Sil.Hpointsto (e1, _, Exp.Sizeof (Typ.Tstruct  { Typ.struct_name = Some name }, _, _)) :: _
-      when Sil.exp_equal e1 e ->
+      when Exp.equal e1 e ->
         Some (Typename.TN_csu (Csu.Class Csu.Java, name))
     | _ :: tl -> search_exn e tl in
   let rec find_exn_name hpreds = function
     | [] -> None
     | Sil.Hpointsto (e1, Sil.Eexp (Exp.Exn e2, _), _) :: _
-      when Sil.exp_equal e1 ret_pvar ->
+      when Exp.equal e1 ret_pvar ->
         search_exn e2 hpreds
     | _ :: tl -> find_exn_name hpreds tl in
   let hpreds = Prop.get_sigma prop in
@@ -655,7 +655,7 @@ let lookup_custom_errors prop =
 let prop_set_exn pname prop se_exn =
   let ret_pvar = Exp.Lvar (Pvar.get_ret_pvar pname) in
   let map_hpred = function
-    | Sil.Hpointsto (e, _, t) when Sil.exp_equal e ret_pvar ->
+    | Sil.Hpointsto (e, _, t) when Exp.equal e ret_pvar ->
         Sil.Hpointsto(e, se_exn, t)
     | hpred -> hpred in
   let sigma' = IList.map map_hpred (Prop.get_sigma prop) in
@@ -744,7 +744,7 @@ let combine
       | None -> post_p2
       | Some iter ->
           let filter = function
-            | Sil.Hpointsto (e, _, _) when Sil.exp_equal e callee_ret_pvar -> Some ()
+            | Sil.Hpointsto (e, _, _) when Exp.equal e callee_ret_pvar -> Some ()
             | _ -> None in
           match Prop.prop_iter_find iter filter with
           | None -> post_p2
@@ -1321,7 +1321,7 @@ let check_splitting_precondition sub1 sub2 =
 let sigma_has_null_pointer sigma =
   let hpred_null_pointer = function
     | Sil.Hpointsto (e, _, _) ->
-        Sil.exp_equal e Sil.exp_zero
+        Exp.equal e Sil.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 16f368824..8af5b2231 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 ->
-        Sil.exp_equal rhs Sil.exp_one
+        Exp.equal rhs Sil.exp_one
     | Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.Eq, lhs, rhs), _)
       when is_tracking_exp astate lhs ->
-        Sil.exp_equal rhs Sil.exp_zero
+        Exp.equal rhs Sil.exp_zero
     | _ ->
         false
 
diff --git a/infer/src/checkers/checkers.ml b/infer/src/checkers/checkers.ml
index 3fe5ea04c..239aa0c82 100644
--- a/infer/src/checkers/checkers.ml
+++ b/infer/src/checkers/checkers.ml
@@ -448,7 +448,7 @@ let callback_find_deserialization { Callbacks.proc_desc; get_proc_desc; idenv; p
                      when Ident.equal i1 i2 -> true
                    | _ -> false in
                  let is_set_instr = function
-                   | Sil.Set (e1, _, _, _) when Sil.exp_equal expanded e1 -> true
+                   | Sil.Set (e1, _, _, _) when Exp.equal expanded e1 -> true
                    | _ -> false in
                  match reverse_find_instr is_set_instr node with
                  (* Look for ivar := tmp *)
diff --git a/infer/src/checkers/codeQuery.ml b/infer/src/checkers/codeQuery.ml
index 505b98b67..5c3a45ab6 100644
--- a/infer/src/checkers/codeQuery.ml
+++ b/infer/src/checkers/codeQuery.ml
@@ -76,7 +76,7 @@ module Match = struct
     | Vfun pn -> F.fprintf fmt "%s" (Procname.to_string pn)
 
   let value_equal v1 v2 = match v1, v2 with
-    | Vval e1, Vval e2 -> Sil.exp_equal e1 e2
+    | Vval e1, Vval e2 -> Exp.equal e1 e2
     | Vval _, _ -> false
     | _, Vval _ -> false
     | Vfun pn1, Vfun pn2 -> Procname.equal pn1 pn2
@@ -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 -> Sil.exp_equal e Sil.exp_zero
+    | CodeQueryAst.Null, Vval e -> Exp.equal e Sil.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/patternMatch.ml b/infer/src/checkers/patternMatch.ml
index 784bc2d86..b9a56b962 100644
--- a/infer/src/checkers/patternMatch.ml
+++ b/infer/src/checkers/patternMatch.ml
@@ -318,7 +318,7 @@ let java_get_vararg_values node pvar idenv =
   let values = ref [] in
   let do_instr = function
     | Sil.Set (Exp.Lindex (array_exp, _), _, content_exp, _)
-      when Sil.exp_equal (Exp.Lvar pvar) (Idenv.expand_expr idenv array_exp) ->
+      when Exp.equal (Exp.Lvar pvar) (Idenv.expand_expr idenv array_exp) ->
         (* Each vararg argument is an assigment to a pvar denoting an array of objects. *)
         values := content_exp :: !values
     | _ -> () in
diff --git a/infer/src/checkers/repeatedCallsChecker.ml b/infer/src/checkers/repeatedCallsChecker.ml
index 18645f64b..d14cfe3ce 100644
--- a/infer/src/checkers/repeatedCallsChecker.ml
+++ b/infer/src/checkers/repeatedCallsChecker.ml
@@ -27,7 +27,7 @@ struct
       let compare i1 i2 = match i1, i2 with
         | Sil.Call (_, e1, etl1, _, cf1), Sil.Call (_, e2, etl2, _, cf2) ->
             (* ignore return ids and call flags *)
-            let n = Sil.exp_compare e1 e2 in
+            let n = Exp.compare e1 e2 in
             if n <> 0 then n else let n = IList.compare Sil.exp_typ_compare etl1 etl2 in
               if n <> 0 then n else CallFlags.compare cf1 cf2
         | _ -> Sil.instr_compare i1 i2
diff --git a/infer/src/clang/cFrontend_utils.ml b/infer/src/clang/cFrontend_utils.ml
index 2ea73576f..1947710a7 100644
--- a/infer/src/clang/cFrontend_utils.ml
+++ b/infer/src/clang/cFrontend_utils.ml
@@ -533,7 +533,7 @@ struct
     append_no_duplicates eq list1 list2
 
   let append_no_duplicateds list1 list2 =
-    let eq (e1, t1) (e2, t2) = (Sil.exp_equal e1 e2) && (Typ.equal t1 t2) in
+    let eq (e1, t1) (e2, t2) = (Exp.equal e1 e2) && (Typ.equal t1 t2) in
     append_no_duplicates eq list1 list2
 
 
diff --git a/infer/src/clang/cTrans.ml b/infer/src/clang/cTrans.ml
index 2ca00efb9..01a3cf65f 100644
--- a/infer/src/clang/cTrans.ml
+++ b/infer/src/clang/cTrans.ml
@@ -766,7 +766,7 @@ struct
         let (sil_e2, _) = extract_exp_from_list res_trans_e2.exps
             "\nWARNING: Missing RHS operand in BinOp. Returning -1. Fix needed...\n" in
         let binop_res_trans, exp_to_parent =
-          if IList.exists (Sil.exp_equal var_exp) res_trans_e2.initd_exps then [], []
+          if IList.exists (Exp.equal var_exp) res_trans_e2.initd_exps then [], []
           else
             let exp_op, instr_bin =
               CArithmetic_trans.binary_operation_instruction
@@ -1653,7 +1653,7 @@ struct
         let rhs_owning_method = CTrans_utils.is_owning_method ie in
         let _, instrs_assign =
           (* variable might be initialized already - do nothing in that case*)
-          if IList.exists (Sil.exp_equal var_exp) res_trans_ie.initd_exps then ([], [])
+          if IList.exists (Exp.equal var_exp) res_trans_ie.initd_exps then ([], [])
           else if !Config.arc_mode &&
                   (CTrans_utils.is_method_call ie ||
                    ObjcInterface_decl.is_pointer_to_objc_class context.CContext.tenv ie_typ)
@@ -1873,7 +1873,7 @@ struct
             let (sil_expr, _) = extract_exp_from_list res_trans_stmt.exps
                 "WARNING: There should be only one return expression.\n" in
 
-            let ret_instrs = if IList.exists (Sil.exp_equal ret_exp) res_trans_stmt.initd_exps
+            let ret_instrs = if IList.exists (Exp.equal ret_exp) res_trans_stmt.initd_exps
               then []
               else [Sil.Set (ret_exp, ret_type, sil_expr, sil_loc)] in
             let autorelease_instrs =
diff --git a/infer/src/eradicate/typeCheck.ml b/infer/src/eradicate/typeCheck.ml
index 99a9b47f0..aa958a13f 100644
--- a/infer/src/eradicate/typeCheck.ml
+++ b/infer/src/eradicate/typeCheck.ml
@@ -1037,7 +1037,7 @@ let typecheck_instr
             let found = ref None in
             let do_instr i = match i with
               | Sil.Set (e, _, e', _)
-                when Sil.exp_equal (Exp.Lvar pvar) (Idenv.expand_expr idenv e') ->
+                when Exp.equal (Exp.Lvar pvar) (Idenv.expand_expr idenv e') ->
                   found := Some e
               | _ -> () in
             IList.iter do_instr (Cfg.Node.get_instrs prev_node);
@@ -1055,7 +1055,7 @@ let typecheck_instr
             node'', Exp.BinOp (bop, c1', c2')
         | Exp.Var _ ->
             let c' = Idenv.expand_expr idenv _cond in
-            if not (Sil.exp_equal c' _cond) then normalize_cond _node c'
+            if not (Exp.equal c' _cond) then normalize_cond _node c'
             else _node, c'
         | Exp.Lvar pvar when Pvar.is_frontend_tmp pvar ->
             (match handle_assignment_in_condition pvar with
diff --git a/infer/src/eradicate/typeState.ml b/infer/src/eradicate/typeState.ml
index a745c65e7..dfebec6da 100644
--- a/infer/src/eradicate/typeState.ml
+++ b/infer/src/eradicate/typeState.ml
@@ -35,7 +35,7 @@ type 'a ext =
 
 module M = Map.Make (struct
     type t = Exp.t
-    let compare = Sil.exp_compare end)
+    let compare = Exp.compare end)
 
 type range = Typ.t * TypeAnnotation.t * (Location.t list)