diff --git a/infer/src/IR/Cfg.re b/infer/src/IR/Cfg.re
index 66ca3b0db..81544e7a5 100644
--- a/infer/src/IR/Cfg.re
+++ b/infer/src/IR/Cfg.re
@@ -279,7 +279,7 @@ let mark_unchanged_pdescs cfg_new cfg_old => {
           IList.equal
             (
               fun i1 i2 => {
-                let (n, exp_map') = Sil.instr_compare_structural i1 i2 !exp_map;
+                let (n, exp_map') = Sil.compare_structural_instr i1 i2 !exp_map;
                 exp_map := exp_map';
                 n
               }
diff --git a/infer/src/IR/Sil.re b/infer/src/IR/Sil.re
index ae1995fb1..e95552811 100644
--- a/infer/src/IR/Sil.re
+++ b/infer/src/IR/Sil.re
@@ -29,7 +29,8 @@ type if_kind =
   | Ik_if
   | Ik_land_lor /* obtained from translation of && or || */
   | Ik_while
-  | Ik_switch;
+  | Ik_switch
+[@@deriving compare];
 
 
 /** An instruction. */
@@ -57,7 +58,8 @@ type instr =
   | Nullify Pvar.t Location.t
   | Abstract Location.t /** apply abstraction */
   | Remove_temps (list Ident.t) Location.t /** remove temporaries */
-  | Declare_locals (list (Pvar.t, Typ.t)) Location.t /** declare local variables */;
+  | Declare_locals (list (Pvar.t, Typ.t)) Location.t /** declare local variables */
+[@@deriving compare];
 
 let skip_instr = Remove_temps [] Location.dummy;
 
@@ -88,21 +90,27 @@ type atom =
   | Aeq Exp.t Exp.t /** equality */
   | Aneq Exp.t Exp.t /** disequality */
   | Apred PredSymb.t (list Exp.t) /** predicate symbol applied to exps */
-  | Anpred PredSymb.t (list Exp.t) /** negated predicate symbol applied to exps */;
+  | Anpred PredSymb.t (list Exp.t) /** negated predicate symbol applied to exps */
+[@@deriving compare];
+
+let equal_atom x y => compare_atom x y == 0;
 
 
 /** kind of lseg or dllseg predicates */
 type lseg_kind =
   | Lseg_NE /** nonempty (possibly circular) listseg */
-  | Lseg_PE /** possibly empty (possibly circular) listseg */;
+  | Lseg_PE /** possibly empty (possibly circular) listseg */
+[@@deriving compare];
+
+let equal_lseg_kind k1 k2 => compare_lseg_kind k1 k2 == 0;
 
 
 /** The boolean is true when the pointer was dereferenced without testing for zero. */
-type zero_flag = option bool;
+type zero_flag = option bool [@@deriving compare];
 
 
 /** True when the value was obtained by doing case analysis on null in a procedure call. */
-type null_case_flag = bool;
+type null_case_flag = bool [@@deriving compare];
 
 
 /** instrumentation of heap values */
@@ -118,13 +126,19 @@ type inst =
   | Irearrange zero_flag null_case_flag int PredSymb.path_pos
   | Itaint
   | Iupdate zero_flag null_case_flag int PredSymb.path_pos
-  | Ireturn_from_call int;
+  | Ireturn_from_call int
+[@@deriving compare];
+
+/* some occurrences of inst are always ignored by compare */
+type _inst = inst;
+
+let compare__inst _ _ => 0;
 
 
 /** structured expressions represent a value of structured type, such as an array or a struct. */
-type strexp =
-  | Eexp Exp.t inst /** Base case: expression with instrumentation */
-  | Estruct (list (Ident.fieldname, strexp)) inst /** C structure */
+type strexp0 'inst =
+  | Eexp Exp.t 'inst /** Base case: expression with instrumentation */
+  | Estruct (list (Ident.fieldname, strexp0 _inst)) 'inst /** C structure */
   /** Array of given length
       There are two conditions imposed / used in the array case.
       First, if some index and value pair appears inside an array
@@ -132,45 +146,102 @@ type strexp =
       For instance, x |->[10 | e1: v1] implies that e1 <= 9.
       Second, if two indices appear in an array, they should be different.
       For instance, x |->[10 | e1: v1, e2: v2] implies that e1 != e2. */
-  | Earray Exp.t (list (Exp.t, strexp)) inst;
+  | Earray Exp.t (list (Exp.t, strexp0 _inst)) 'inst
+[@@deriving compare];
+
+type strexp = strexp0 inst;
+
+let compare_strexp inst::inst=false se1 se2 =>
+  compare_strexp0 (inst ? compare_inst : compare__inst) se1 se2;
+
+let equal_strexp inst::inst=false se1 se2 => compare_strexp inst::inst se1 se2 == 0;
 
 
 /** an atomic heap predicate */
-type hpred =
-  | Hpointsto Exp.t strexp Exp.t
+type hpred0 'inst =
+  | Hpointsto Exp.t (strexp0 'inst) Exp.t
   /** represents [exp|->strexp:typexp] where [typexp]
       is an expression representing a type, e.h. [sizeof(t)]. */
-  | Hlseg lseg_kind hpara Exp.t Exp.t (list Exp.t)
+  | Hlseg lseg_kind (hpara0 'inst) Exp.t Exp.t (list Exp.t)
   /** higher - order predicate for singly - linked lists.
       Should ensure that exp1!= exp2 implies that exp1 is allocated.
       This assumption is used in the rearrangement. The last [exp list] parameter
       is used to denote the shared links by all the nodes in the list. */
-  | Hdllseg lseg_kind hpara_dll Exp.t Exp.t Exp.t Exp.t (list Exp.t)
-/** higher-order predicate for doubly-linked lists. */
-/** parameter for the higher-order singly-linked list predicate.
-    Means "lambda (root,next,svars). Exists evars. body".
-    Assume that root, next, svars, evars are disjoint sets of
-    primed identifiers, and include all the free primed identifiers in body.
-    body should not contain any non - primed identifiers or program
-    variables (i.e. pvars). */
-and hpara = {
+  | Hdllseg lseg_kind (hpara_dll0 'inst) Exp.t Exp.t Exp.t Exp.t (list Exp.t)
+  /** higher-order predicate for doubly-linked lists.
+      Parameter for the higher-order singly-linked list predicate.
+      Means "lambda (root,next,svars). Exists evars. body".
+      Assume that root, next, svars, evars are disjoint sets of
+      primed identifiers, and include all the free primed identifiers in body.
+      body should not contain any non - primed identifiers or program
+      variables (i.e. pvars). */
+[@@deriving compare]
+and hpara0 'inst = {
   root: Ident.t,
   next: Ident.t,
   svars: list Ident.t,
   evars: list Ident.t,
-  body: list hpred
+  body: list (hpred0 'inst)
 }
+[@@deriving compare]
 /** parameter for the higher-order doubly-linked list predicates.
     Assume that all the free identifiers in body_dll should belong to
     cell, blink, flink, svars_dll, evars_dll. */
-and hpara_dll = {
+and hpara_dll0 'inst = {
   cell: Ident.t, /** address cell */
   blink: Ident.t, /** backward link */
   flink: Ident.t, /** forward link */
   svars_dll: list Ident.t,
   evars_dll: list Ident.t,
-  body_dll: list hpred
-};
+  body_dll: list (hpred0 'inst)
+}
+[@@deriving compare];
+
+type hpred = hpred0 inst;
+
+
+/** Comparsion between heap predicates. Reverse natural order, and order first by anchor exp. */
+let compare_hpred inst::inst=false hpred1 hpred2 =>
+  if (hpred1 === hpred2) {
+    0
+  } else {
+    switch (hpred1, hpred2) {
+    | (
+        Hpointsto e1 _ _ | Hlseg _ _ e1 _ _ | Hdllseg _ _ e1 _ _ _ _,
+        Hpointsto e2 _ _ | Hlseg _ _ e2 _ _ | Hdllseg _ _ e2 _ _ _ _
+      )
+        when Exp.compare e2 e1 != 0 =>
+      Exp.compare e2 e1
+    | (Hpointsto _, Hpointsto _)
+    | (Hlseg _, Hlseg _)
+    | (Hdllseg _, Hdllseg _) =>
+      if inst {
+        compare_hpred0 compare_inst hpred2 hpred1
+      } else {
+        compare_hpred0 (fun _ _ => 0) hpred2 hpred1
+      }
+    | _ =>
+      if inst {
+        compare_hpred0 compare_inst hpred1 hpred2
+      } else {
+        compare_hpred0 (fun _ _ => 0) hpred1 hpred2
+      }
+    }
+  };
+
+let equal_hpred inst::inst=false hpred1 hpred2 => compare_hpred inst::inst hpred1 hpred2 == 0;
+
+type hpara = hpara0 inst;
+
+let compare_hpara = compare_hpara0 (fun _ _ => 0);
+
+let equal_hpara hpara1 hpara2 => compare_hpara hpara1 hpara2 == 0;
+
+type hpara_dll = hpara_dll0 inst;
+
+let compare_hpara_dll = compare_hpara_dll0 (fun _ _ => 0);
+
+let equal_hpara_dll hpara1 hpara2 => compare_hpara_dll hpara1 hpara2 == 0;
 
 
 /** Return the lhs expression of a hpred */
@@ -222,343 +293,6 @@ let is_static_local_name pname pvar => {
   }
 };
 
-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;
-
-
-/** Compare atoms. Equalities come before disequalities */
-let atom_compare a b =>
-  if (a === b) {
-    0
-  } else {
-    switch (a, b) {
-    | (Aeq e1 e2, Aeq f1 f2) =>
-      let n = Exp.compare e1 f1;
-      if (n != 0) {
-        n
-      } else {
-        Exp.compare e2 f2
-      }
-    | (Aeq _, _) => (-1)
-    | (_, Aeq _) => 1
-    | (Aneq e1 e2, Aneq f1 f2) =>
-      let n = Exp.compare e1 f1;
-      if (n != 0) {
-        n
-      } else {
-        Exp.compare e2 f2
-      }
-    | (Aneq _, _) => (-1)
-    | (_, Aneq _) => 1
-    | (Apred a1 es1, Apred a2 es2) =>
-      let n = PredSymb.compare a1 a2;
-      if (n != 0) {
-        n
-      } else {
-        IList.compare Exp.compare es1 es2
-      }
-    | (Apred _, _) => (-1)
-    | (_, Apred _) => 1
-    | (Anpred a1 es1, Anpred a2 es2) =>
-      let n = PredSymb.compare a1 a2;
-      if (n != 0) {
-        n
-      } else {
-        IList.compare Exp.compare es1 es2
-      }
-    }
-  };
-
-let atom_equal x y => atom_compare x y == 0;
-
-let lseg_kind_compare k1 k2 =>
-  switch (k1, k2) {
-  | (Lseg_NE, Lseg_NE) => 0
-  | (Lseg_NE, Lseg_PE) => (-1)
-  | (Lseg_PE, Lseg_NE) => 1
-  | (Lseg_PE, Lseg_PE) => 0
-  };
-
-let lseg_kind_equal k1 k2 => lseg_kind_compare k1 k2 == 0;
-
-let zero_flag_compare = opt_compare bool_compare;
-
-let inst_compare_base inst1 inst2 =>
-  switch (inst1, inst2) {
-  | (Iabstraction, Iabstraction) => 0
-  | (Iabstraction, _) => (-1)
-  | (_, Iabstraction) => 1
-  | (Iactual_precondition, Iactual_precondition) => 0
-  | (Iactual_precondition, _) => (-1)
-  | (_, Iactual_precondition) => 1
-  | (Ialloc, Ialloc) => 0
-  | (Ialloc, _) => (-1)
-  | (_, Ialloc) => 1
-  | (Iformal zero_flag1 null_case_flag1, Iformal zero_flag2 null_case_flag2) =>
-    let n = zero_flag_compare zero_flag1 zero_flag2;
-    if (n != 0) {
-      n
-    } else {
-      bool_compare null_case_flag1 null_case_flag2
-    }
-  | (Iformal _, _) => (-1)
-  | (_, Iformal _) => 1
-  | (Iinitial, Iinitial) => 0
-  | (Iinitial, _) => (-1)
-  | (_, Iinitial) => 1
-  | (Ilookup, Ilookup) => 0
-  | (Ilookup, _) => (-1)
-  | (_, Ilookup) => 1
-  | (Inone, Inone) => 0
-  | (Inone, _) => (-1)
-  | (_, Inone) => 1
-  | (Inullify, Inullify) => 0
-  | (Inullify, _) => (-1)
-  | (_, Inullify) => 1
-  | (
-      Irearrange zero_flag1 null_case_flag1 i1 path_pos1,
-      Irearrange zero_flag2 null_case_flag2 i2 path_pos2
-    ) =>
-    let n = zero_flag_compare zero_flag1 zero_flag2;
-    if (n != 0) {
-      n
-    } else {
-      let n = bool_compare null_case_flag1 null_case_flag2;
-      if (n != 0) {
-        n
-      } else {
-        let n = int_compare i1 i2;
-        if (n != 0) {
-          n
-        } else {
-          PredSymb.compare_path_pos path_pos1 path_pos2
-        }
-      }
-    }
-  | (Irearrange _, _) => (-1)
-  | (_, Irearrange _) => 1
-  | (Itaint, Itaint) => 0
-  | (Itaint, _) => (-1)
-  | (_, Itaint) => 1
-  | (
-      Iupdate zero_flag1 null_case_flag1 i1 path_pos1,
-      Iupdate zero_flag2 null_case_flag2 i2 path_pos2
-    ) =>
-    let n = zero_flag_compare zero_flag1 zero_flag2;
-    if (n != 0) {
-      n
-    } else {
-      let n = bool_compare null_case_flag1 null_case_flag2;
-      if (n != 0) {
-        n
-      } else {
-        let n = int_compare i1 i2;
-        if (n != 0) {
-          n
-        } else {
-          PredSymb.compare_path_pos path_pos1 path_pos2
-        }
-      }
-    }
-  | (Iupdate _, _) => (-1)
-  | (_, Iupdate _) => 1
-  | (Ireturn_from_call i1, Ireturn_from_call i2) => int_compare i1 i2
-  };
-
-let inst_compare inst::inst inst1 inst2 => inst ? inst_compare_base inst1 inst2 : 0;
-
-/* Comparison for strexps */
-let rec strexp_compare inst::inst=false se1 se2 =>
-  if (se1 === se2) {
-    0
-  } else {
-    switch (se1, se2) {
-    | (Eexp e1 i1, Eexp e2 i2) =>
-      let n = Exp.compare e1 e2;
-      if (n != 0) {
-        n
-      } else {
-        inst_compare inst::inst i1 i2
-      }
-    | (Eexp _, _) => (-1)
-    | (_, Eexp _) => 1
-    | (Estruct fel1 i1, Estruct fel2 i2) =>
-      let n = fld_strexp_list_compare fel1 fel2;
-      if (n != 0) {
-        n
-      } else {
-        inst_compare inst::inst i1 i2
-      }
-    | (Estruct _, _) => (-1)
-    | (_, Estruct _) => 1
-    | (Earray e1 esel1 i1, Earray e2 esel2 i2) =>
-      let n = Exp.compare e1 e2;
-      if (n != 0) {
-        n
-      } else {
-        let n = exp_strexp_list_compare esel1 esel2;
-        if (n != 0) {
-          n
-        } else {
-          inst_compare inst::inst i1 i2
-        }
-      }
-    }
-  }
-and fld_strexp_compare fse1 fse2 => pair_compare Ident.compare_fieldname 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_list_compare esel1 esel2 => IList.compare exp_strexp_compare esel1 esel2;
-
-
-/** Comparsion between heap predicates. Hpointsto comes before others. */
-let rec hpred_compare inst::inst=false hpred1 hpred2 =>
-  if (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 se1 te1, Hpointsto e2 se2 te2) =>
-      let n = Exp.compare e2 e1;
-      if (n != 0) {
-        n
-      } else {
-        let n = strexp_compare inst::inst se2 se1;
-        if (n != 0) {
-          n
-        } else {
-          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;
-      if (n != 0) {
-        n
-      } else {
-        let n = lseg_kind_compare k2 k1;
-        if (n != 0) {
-          n
-        } else {
-          let n = hpara_compare hpar2 hpar1;
-          if (n != 0) {
-            n
-          } else {
-            let n = Exp.compare f2 f1;
-            if (n != 0) {
-              n
-            } else {
-              exp_list_compare el2 el1
-            }
-          }
-        }
-      }
-    | (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;
-      if (n != 0) {
-        n
-      } else {
-        let n = lseg_kind_compare k2 k1;
-        if (n != 0) {
-          n
-        } else {
-          let n = hpara_dll_compare hpar2 hpar1;
-          if (n != 0) {
-            n
-          } else {
-            let n = Exp.compare f2 f1;
-            if (n != 0) {
-              n
-            } else {
-              let n = Exp.compare g2 g1;
-              if (n != 0) {
-                n
-              } else {
-                let n = Exp.compare h2 h1;
-                if (n != 0) {
-                  n
-                } else {
-                  exp_list_compare el2 el1
-                }
-              }
-            }
-          }
-        }
-      }
-    }
-  }
-and hpred_list_compare l1 l2 => IList.compare hpred_compare l1 l2
-and hpara_compare hp1 hp2 => {
-  let n = Ident.compare hp1.root hp2.root;
-  if (n != 0) {
-    n
-  } else {
-    let n = Ident.compare hp1.next hp2.next;
-    if (n != 0) {
-      n
-    } else {
-      let n = IList.compare Ident.compare hp1.svars hp2.svars;
-      if (n != 0) {
-        n
-      } else {
-        let n = IList.compare Ident.compare hp1.evars hp2.evars;
-        if (n != 0) {
-          n
-        } else {
-          hpred_list_compare hp1.body hp2.body
-        }
-      }
-    }
-  }
-}
-and hpara_dll_compare hp1 hp2 => {
-  let n = Ident.compare hp1.cell hp2.cell;
-  if (n != 0) {
-    n
-  } else {
-    let n = Ident.compare hp1.blink hp2.blink;
-    if (n != 0) {
-      n
-    } else {
-      let n = Ident.compare hp1.flink hp2.flink;
-      if (n != 0) {
-        n
-      } else {
-        let n = IList.compare Ident.compare hp1.svars_dll hp2.svars_dll;
-        if (n != 0) {
-          n
-        } else {
-          let n = IList.compare Ident.compare hp1.evars_dll hp2.evars_dll;
-          if (n != 0) {
-            n
-          } else {
-            hpred_list_compare hp1.body_dll hp2.body_dll
-          }
-        }
-      }
-    }
-  }
-};
-
-let strexp_equal inst::inst=false se1 se2 => strexp_compare inst::inst se1 se2 == 0;
-
-let hpred_equal inst::inst=false hpred1 hpred2 => hpred_compare inst::inst hpred1 hpred2 == 0;
-
-let hpara_equal hpara1 hpara2 => hpara_compare hpara1 hpara2 == 0;
-
-let hpara_dll_equal hpara1 hpara2 => hpara_dll_compare hpara1 hpara2 == 0;
-
 
 /** {2 Sets of expressions} */
 let elist_to_eset es => IList.fold_left (fun set e => Exp.Set.add e set) Exp.Set.empty es;
@@ -567,7 +301,7 @@ let elist_to_eset es => IList.fold_left (fun set e => Exp.Set.add e set) Exp.Set
 /** {2 Sets of heap predicates} */
 let module HpredSet = Set.Make {
   type t = hpred;
-  let compare = hpred_compare inst::false;
+  let compare = compare_hpred inst::false;
 };
 
 
@@ -891,14 +625,14 @@ let module Predicates: {
   /** hash tables for hpara */
   let module HparaHash = Hashtbl.Make {
     type t = hpara;
-    let equal = hpara_equal;
+    let equal = equal_hpara;
     let hash = Hashtbl.hash;
   };
 
   /** hash tables for hpara_dll */
   let module HparaDllHash = Hashtbl.Make {
     type t = hpara_dll;
-    let equal = hpara_dll_equal;
+    let equal = equal_hpara_dll;
     let hash = Hashtbl.hash;
   };
 
@@ -1915,36 +1649,15 @@ let rec sorted_list_check_consecutives f =>
 
 
 /** substitution */
-type subst = list (Ident.t, Exp.t);
+type ident_exp = (Ident.t, Exp.t) [@@deriving compare];
 
+let equal_ident_exp ide1 ide2 => compare_ident_exp ide1 ide2 == 0;
 
-/** Comparison between substitutions. */
-let rec sub_compare (sub1: subst) (sub2: subst) =>
-  if (sub1 === sub2) {
-    0
-  } else {
-    switch (sub1, sub2) {
-    | ([], []) => 0
-    | ([], [_, ..._]) => (-1)
-    | ([(i1, e1), ...sub1'], [(i2, e2), ...sub2']) =>
-      let n = Ident.compare i1 i2;
-      if (n != 0) {
-        n
-      } else {
-        let n = Exp.compare e1 e2;
-        if (n != 0) {
-          n
-        } else {
-          sub_compare sub1' sub2'
-        }
-      }
-    | ([_, ..._], []) => 1
-    }
-  };
+type subst = list ident_exp [@@deriving compare];
 
 
 /** Equality for substitutions. */
-let sub_equal sub1 sub2 => sub_compare sub1 sub2 == 0;
+let equal_subst sub1 sub2 => compare_subst sub1 sub2 == 0;
 
 let sub_check_duplicated_ids sub => {
   let f (id1, _) (id2, _) => Ident.equal id1 id2;
@@ -1956,8 +1669,8 @@ let sub_check_duplicated_ids sub => {
     For all (id1, e1), (id2, e2) in the input list,
     if id1 = id2, then e1 = e2. */
 let sub_of_list sub => {
-  let sub' = IList.sort ident_exp_compare sub;
-  let sub'' = remove_duplicates_from_sorted ident_exp_equal sub';
+  let sub' = IList.sort compare_ident_exp sub;
+  let sub'' = remove_duplicates_from_sorted equal_ident_exp sub';
   if (sub_check_duplicated_ids sub'') {
     assert false
   };
@@ -1967,7 +1680,7 @@ let sub_of_list sub => {
 
 /** like sub_of_list, but allow duplicate ids and only keep the first occurrence */
 let sub_of_list_duplicates sub => {
-  let sub' = IList.sort ident_exp_compare sub;
+  let sub' = IList.sort compare_ident_exp sub;
   let rec remove_duplicate_ids =
     fun
     | [(id1, e1), (id2, e2), ...l] =>
@@ -1992,8 +1705,8 @@ let sub_empty = sub_of_list [];
 /** Join two substitutions into one.
     For all id in dom(sub1) cap dom(sub2), sub1(id) = sub2(id). */
 let sub_join sub1 sub2 => {
-  let sub = sorted_list_merge ident_exp_compare sub1 sub2;
-  let sub' = remove_duplicates_from_sorted ident_exp_equal sub;
+  let sub = sorted_list_merge compare_ident_exp sub1 sub2;
+  let sub' = remove_duplicates_from_sorted equal_ident_exp sub;
   if (sub_check_duplicated_ids sub') {
     assert false
   };
@@ -2015,7 +1728,7 @@ let sub_symmetric_difference sub1_in sub2_in => {
       let sub_common = reverse_with_base [] sub_common;
       (sub_common, sub1_only', sub2_only')
     | ([id_e1, ...sub1'], [id_e2, ...sub2']) =>
-      let n = ident_exp_compare id_e1 id_e2;
+      let n = compare_ident_exp id_e1 id_e2;
       if (n == 0) {
         diff [id_e1, ...sub_common] sub1_only sub2_only sub1' sub2'
       } else if (n < 0) {
@@ -2280,145 +1993,6 @@ let instr_sub_ids sub_id_binders::sub_id_binders (f: Ident.t => Exp.t) instr =>
 /** apply [subst] to all id's in [instr], including binder id's */
 let instr_sub (subst: subst) instr => instr_sub_ids sub_id_binders::true (apply_sub subst) instr;
 
-let id_typ_compare (id1, typ1) (id2, typ2) => {
-  let n = Ident.compare id1 id2;
-  if (n != 0) {
-    n
-  } else {
-    Typ.compare typ1 typ2
-  }
-};
-
-let exp_typ_compare (exp1, typ1) (exp2, typ2) => {
-  let n = Exp.compare exp1 exp2;
-  if (n != 0) {
-    n
-  } else {
-    Typ.compare typ1 typ2
-  }
-};
-
-let instr_compare instr1 instr2 =>
-  switch (instr1, instr2) {
-  | (Load id1 e1 t1 loc1, Load id2 e2 t2 loc2) =>
-    let n = Ident.compare id1 id2;
-    if (n != 0) {
-      n
-    } else {
-      let n = Exp.compare e1 e2;
-      if (n != 0) {
-        n
-      } else {
-        let n = Typ.compare t1 t2;
-        if (n != 0) {
-          n
-        } else {
-          Location.compare loc1 loc2
-        }
-      }
-    }
-  | (Load _, _) => (-1)
-  | (_, Load _) => 1
-  | (Store e11 t1 e21 loc1, Store e12 t2 e22 loc2) =>
-    let n = Exp.compare e11 e12;
-    if (n != 0) {
-      n
-    } else {
-      let n = Typ.compare t1 t2;
-      if (n != 0) {
-        n
-      } else {
-        let n = Exp.compare e21 e22;
-        if (n != 0) {
-          n
-        } else {
-          Location.compare loc1 loc2
-        }
-      }
-    }
-  | (Store _, _) => (-1)
-  | (_, Store _) => 1
-  | (Prune cond1 loc1 true_branch1 ik1, Prune cond2 loc2 true_branch2 ik2) =>
-    let n = Exp.compare cond1 cond2;
-    if (n != 0) {
-      n
-    } else {
-      let n = Location.compare loc1 loc2;
-      if (n != 0) {
-        n
-      } else {
-        let n = bool_compare true_branch1 true_branch2;
-        if (n != 0) {
-          n
-        } else {
-          Pervasives.compare ik1 ik2
-        }
-      }
-    }
-  | (Prune _, _) => (-1)
-  | (_, Prune _) => 1
-  | (Call ret_id1 e1 arg_ts1 loc1 cf1, Call ret_id2 e2 arg_ts2 loc2 cf2) =>
-    let n = opt_compare id_typ_compare ret_id1 ret_id2;
-    if (n != 0) {
-      n
-    } else {
-      let n = Exp.compare e1 e2;
-      if (n != 0) {
-        n
-      } else {
-        let n = IList.compare exp_typ_compare arg_ts1 arg_ts2;
-        if (n != 0) {
-          n
-        } else {
-          let n = Location.compare loc1 loc2;
-          if (n != 0) {
-            n
-          } else {
-            CallFlags.compare cf1 cf2
-          }
-        }
-      }
-    }
-  | (Call _, _) => (-1)
-  | (_, Call _) => 1
-  | (Nullify pvar1 loc1, Nullify pvar2 loc2) =>
-    let n = Pvar.compare pvar1 pvar2;
-    if (n != 0) {
-      n
-    } else {
-      Location.compare loc1 loc2
-    }
-  | (Nullify _, _) => (-1)
-  | (_, Nullify _) => 1
-  | (Abstract loc1, Abstract loc2) => Location.compare loc1 loc2
-  | (Abstract _, _) => (-1)
-  | (_, Abstract _) => 1
-  | (Remove_temps temps1 loc1, Remove_temps temps2 loc2) =>
-    let n = IList.compare Ident.compare temps1 temps2;
-    if (n != 0) {
-      n
-    } else {
-      Location.compare loc1 loc2
-    }
-  | (Remove_temps _, _) => (-1)
-  | (_, Remove_temps _) => 1
-  | (Declare_locals ptl1 loc1, Declare_locals ptl2 loc2) =>
-    let pt_compare (pv1, t1) (pv2, t2) => {
-      let n = Pvar.compare pv1 pv2;
-      if (n != 0) {
-        n
-      } else {
-        Typ.compare t1 t2
-      }
-    };
-    let n = IList.compare pt_compare ptl1 ptl2;
-    if (n != 0) {
-      n
-    } else {
-      Location.compare loc1 loc2
-    }
-  };
-
 
 /** compare expressions from different procedures without considering loc's, ident's, and pvar's.
     the [exp_map] param gives a mapping of names used in the procedure of [e1] to names used in the
@@ -2515,7 +2089,7 @@ let exp_typ_compare_structural (e1, t1) (e2, t2) exp_map => {
 /** compare instructions from different procedures without considering loc's, ident's, and pvar's.
     the [exp_map] param gives a mapping of names used in the procedure of [instr1] to identifiers
     used in the procedure of [instr2] */
-let instr_compare_structural instr1 instr2 exp_map => {
+let compare_structural_instr instr1 instr2 exp_map => {
   let id_typ_opt_compare_structural id_typ1 id_typ2 exp_map => {
     let id_typ_compare_structural (id1, typ1) (id2, typ2) => {
       let (n, exp_map) = exp_compare_structural (Var id1) (Var id2) exp_map;
@@ -2660,7 +2234,7 @@ let instr_compare_structural instr1 instr2 exp_map => {
         ptl1
         ptl2
     }
-  | _ => (instr_compare instr1 instr2, exp_map)
+  | _ => (compare_instr instr1 instr2, exp_map)
   }
 };
 
@@ -2726,7 +2300,7 @@ let hpred_replace_exp epairs =>
 /** {2 Compaction} */
 let module HpredInstHash = Hashtbl.Make {
   type t = hpred;
-  let equal = hpred_equal inst::true;
+  let equal = equal_hpred inst::true;
   let hash = Hashtbl.hash;
 };
 
diff --git a/infer/src/IR/Sil.rei b/infer/src/IR/Sil.rei
index afba88c53..853cdcc83 100644
--- a/infer/src/IR/Sil.rei
+++ b/infer/src/IR/Sil.rei
@@ -31,7 +31,8 @@ type if_kind =
   | Ik_if
   | Ik_land_lor /* obtained from translation of && or || */
   | Ik_while
-  | Ik_switch;
+  | Ik_switch
+[@@deriving compare];
 
 
 /** An instruction. */
@@ -59,7 +60,14 @@ type instr =
   | Nullify Pvar.t Location.t
   | Abstract Location.t /** apply abstraction */
   | Remove_temps (list Ident.t) Location.t /** remove temporaries */
-  | Declare_locals (list (Pvar.t, Typ.t)) Location.t /** declare local variables */;
+  | Declare_locals (list (Pvar.t, Typ.t)) Location.t /** declare local variables */
+[@@deriving compare];
+
+
+/** compare instructions from different procedures without considering loc's, ident's, and pvar's.
+    the [exp_map] param gives a mapping of names used in the procedure of [instr1] to identifiers
+    used in the procedure of [instr2] */
+let compare_structural_instr: instr => instr => Exp.Map.t Exp.t => (int, Exp.Map.t Exp.t);
 
 let skip_instr: instr;
 
@@ -81,13 +89,19 @@ type atom =
   | Aeq Exp.t Exp.t /** equality */
   | Aneq Exp.t Exp.t /** disequality */
   | Apred PredSymb.t (list Exp.t) /** predicate symbol applied to exps */
-  | Anpred PredSymb.t (list Exp.t) /** negated predicate symbol applied to exps */;
+  | Anpred PredSymb.t (list Exp.t) /** negated predicate symbol applied to exps */
+[@@deriving compare];
+
+let equal_atom: atom => atom => bool;
 
 
 /** kind of lseg or dllseg predicates */
 type lseg_kind =
   | Lseg_NE /** nonempty (possibly circular) listseg */
-  | Lseg_PE /** possibly empty (possibly circular) listseg */;
+  | Lseg_PE /** possibly empty (possibly circular) listseg */
+[@@deriving compare];
+
+let equal_lseg_kind: lseg_kind => lseg_kind => bool;
 
 
 /** The boolean is true when the pointer was dereferenced without testing for zero. */
@@ -111,7 +125,8 @@ type inst =
   | Irearrange zero_flag null_case_flag int PredSymb.path_pos
   | Itaint
   | Iupdate zero_flag null_case_flag int PredSymb.path_pos
-  | Ireturn_from_call int;
+  | Ireturn_from_call int
+[@@deriving compare];
 
 let inst_abstraction: inst;
 
@@ -161,11 +176,13 @@ let inst_partial_join: inst => inst => inst;
 /** meet of instrumentations */
 let inst_partial_meet: inst => inst => inst;
 
+type _inst = inst;
+
 
 /** structured expressions represent a value of structured type, such as an array or a struct. */
-type strexp =
-  | Eexp Exp.t inst /** Base case: expression with instrumentation */
-  | Estruct (list (Ident.fieldname, strexp)) inst /** C structure */
+type strexp0 'inst =
+  | Eexp Exp.t 'inst /** Base case: expression with instrumentation */
+  | Estruct (list (Ident.fieldname, strexp0 _inst)) 'inst /** C structure */
   /** Array of given length
       There are two conditions imposed / used in the array case.
       First, if some index and value pair appears inside an array
@@ -173,45 +190,81 @@ type strexp =
       For instance, x |->[10 | e1: v1] implies that e1 <= 9.
       Second, if two indices appear in an array, they should be different.
       For instance, x |->[10 | e1: v1, e2: v2] implies that e1 != e2. */
-  | Earray Exp.t (list (Exp.t, strexp)) inst;
+  | Earray Exp.t (list (Exp.t, strexp0 _inst)) 'inst
+[@@deriving compare];
+
+type strexp = strexp0 inst;
+
+
+/** Comparison function for strexp.
+    The inst:: parameter specifies whether instumentations should also
+    be considered (false by default).  */
+let compare_strexp: inst::bool? => strexp => strexp => int;
+
+
+/** Equality function for strexp.
+    The inst:: parameter specifies whether instumentations should also
+    be considered (false by default).  */
+let equal_strexp: inst::bool? => strexp => strexp => bool;
 
 
 /** an atomic heap predicate */
-type hpred =
-  | Hpointsto Exp.t strexp Exp.t
+type hpred0 'inst =
+  | Hpointsto Exp.t (strexp0 'inst) Exp.t
   /** represents [exp|->strexp:typexp] where [typexp]
-      is an expression representing a type, e.g. [sizeof(t)]. */
-  | Hlseg lseg_kind hpara Exp.t Exp.t (list Exp.t)
+      is an expression representing a type, e.h. [sizeof(t)]. */
+  | Hlseg lseg_kind (hpara0 'inst) Exp.t Exp.t (list Exp.t)
   /** higher - order predicate for singly - linked lists.
       Should ensure that exp1!= exp2 implies that exp1 is allocated.
       This assumption is used in the rearrangement. The last [exp list] parameter
-      is used to denote the shared links by all the nodes in the list.*/
-  | Hdllseg lseg_kind hpara_dll Exp.t Exp.t Exp.t Exp.t (list Exp.t)
-/** higher-order predicate for doubly-linked lists. */
-/** parameter for the higher-order singly-linked list predicate.
-    Means "lambda (root,next,svars). Exists evars. body".
-    Assume that root, next, svars, evars are disjoint sets of
-    primed identifiers, and include all the free primed identifiers in body.
-    body should not contain any non - primed identifiers or program
-    variables (i.e. pvars). */
-and hpara = {
+      is used to denote the shared links by all the nodes in the list. */
+  | Hdllseg lseg_kind (hpara_dll0 'inst) Exp.t Exp.t Exp.t Exp.t (list Exp.t)
+  /** higher-order predicate for doubly-linked lists.
+      Parameter for the higher-order singly-linked list predicate.
+      Means "lambda (root,next,svars). Exists evars. body".
+      Assume that root, next, svars, evars are disjoint sets of
+      primed identifiers, and include all the free primed identifiers in body.
+      body should not contain any non - primed identifiers or program
+      variables (i.e. pvars). */
+[@@deriving compare]
+and hpara0 'inst = {
   root: Ident.t,
   next: Ident.t,
   svars: list Ident.t,
   evars: list Ident.t,
-  body: list hpred
+  body: list (hpred0 'inst)
 }
+[@@deriving compare]
 /** parameter for the higher-order doubly-linked list predicates.
     Assume that all the free identifiers in body_dll should belong to
     cell, blink, flink, svars_dll, evars_dll. */
-and hpara_dll = {
+and hpara_dll0 'inst = {
   cell: Ident.t, /** address cell */
   blink: Ident.t, /** backward link */
   flink: Ident.t, /** forward link */
   svars_dll: list Ident.t,
   evars_dll: list Ident.t,
-  body_dll: list hpred
-};
+  body_dll: list (hpred0 'inst)
+}
+[@@deriving compare];
+
+type hpred = hpred0 inst;
+
+type hpara = hpara0 inst;
+
+type hpara_dll = hpara_dll0 inst;
+
+
+/** Comparison function for hpred.
+    The inst:: parameter specifies whether instumentations should also
+    be considered (false by default).  */
+let compare_hpred: inst::bool? => hpred => hpred => int;
+
+
+/** Equality function for hpred.
+    The inst:: parameter specifies whether instumentations should also
+    be considered (false by default).  */
+let equal_hpred: inst::bool? => hpred => hpred => bool;
 
 
 /** Sets of heap predicates */
@@ -260,63 +313,6 @@ let block_pvar: Pvar.t;
 /** Check if a pvar is a local pointing to a block in objc */
 let is_block_pvar: Pvar.t => bool;
 
-let exp_typ_compare: (Exp.t, Typ.t) => (Exp.t, Typ.t) => int;
-
-let instr_compare: instr => instr => int;
-
-
-/** compare instructions from different procedures without considering loc's, ident's, and pvar's.
-    the [exp_map] param gives a mapping of names used in the procedure of [instr1] to identifiers
-    used in the procedure of [instr2] */
-let instr_compare_structural: instr => instr => Exp.Map.t Exp.t => (int, Exp.Map.t Exp.t);
-
-let atom_compare: atom => atom => int;
-
-let atom_equal: atom => atom => bool;
-
-
-/** Comparison function for strexp.
-    The inst:: parameter specifies whether instumentations should also
-    be considered (false by default).  */
-let strexp_compare: inst::bool? => strexp => strexp => int;
-
-
-/** Equality function for strexp.
-    The inst:: parameter specifies whether instumentations should also
-    be considered (false by default).  */
-let strexp_equal: inst::bool? => strexp => strexp => bool;
-
-let hpara_compare: hpara => hpara => int;
-
-let hpara_equal: hpara => hpara => bool;
-
-let hpara_dll_compare: hpara_dll => hpara_dll => int;
-
-let hpara_dll_equal: hpara_dll => hpara_dll => bool;
-
-let lseg_kind_compare: lseg_kind => lseg_kind => int;
-
-let lseg_kind_equal: lseg_kind => lseg_kind => bool;
-
-
-/** Comparison function for hpred.
-    The inst:: parameter specifies whether instumentations should also
-    be considered (false by default).  */
-let hpred_compare: inst::bool? => hpred => hpred => int;
-
-
-/** Equality function for hpred.
-    The inst:: parameter specifies whether instumentations should also
-    be considered (false by default).  */
-let hpred_equal: inst::bool? => hpred => hpred => bool;
-
-let fld_strexp_compare: (Ident.fieldname, strexp) => (Ident.fieldname, strexp) => int;
-
-let fld_strexp_list_compare:
-  list (Ident.fieldname, strexp) => list (Ident.fieldname, strexp) => int;
-
-let exp_strexp_compare: (Exp.t, strexp) => (Exp.t, strexp) => int;
-
 
 /** Return the lhs expression of a hpred */
 let hpred_get_lhs: hpred => Exp.t;
@@ -669,7 +665,11 @@ let hpara_av_add: fav => hpara => unit;
 
 
 /** {2 Substitution} */
-type subst;
+type subst [@@deriving compare];
+
+
+/** Equality for substitutions. */
+let equal_subst: subst => subst => bool;
 
 
 /** Create a substitution from a list of pairs.
@@ -690,14 +690,6 @@ let sub_to_list: subst => list (Ident.t, Exp.t);
 let sub_empty: subst;
 
 
-/** Comparison for substitutions. */
-let sub_compare: subst => subst => int;
-
-
-/** Equality for substitutions. */
-let sub_equal: subst => subst => bool;
-
-
 /** Compute the common id-exp part of two inputs [subst1] and [subst2].
     The first component of the output is this common part.
     The second and third components are the remainder of [subst1]
diff --git a/infer/src/backend/Attribute.ml b/infer/src/backend/Attribute.ml
index c68fab377..a4701a8ac 100644
--- a/infer/src/backend/Attribute.ml
+++ b/infer/src/backend/Attribute.ml
@@ -135,7 +135,7 @@ let filter_atoms tenv ~f prop =
 let remove tenv prop atom =
   if is_pred atom then
     let natom = Prop.atom_normalize_prop tenv prop atom in
-    let f a = not (Sil.atom_equal natom a) in
+    let f a = not (Sil.equal_atom natom a) in
     filter_atoms tenv ~f prop
   else
     prop
@@ -295,7 +295,7 @@ let find_equal_formal_path tenv e prop =
   let rec find_in_sigma e seen_hpreds =
     IList.fold_right (
       fun hpred res ->
-        if IList.mem Sil.hpred_equal hpred seen_hpreds then None
+        if IList.mem Sil.equal_hpred hpred seen_hpreds then None
         else
           let seen_hpreds = hpred :: seen_hpreds in
           match res with
diff --git a/infer/src/backend/abs.ml b/infer/src/backend/abs.ml
index 982e8f7bf..547e8efe5 100644
--- a/infer/src/backend/abs.ml
+++ b/infer/src/backend/abs.ml
@@ -189,7 +189,7 @@ let mk_rule_lsls_ls tenv k1 k2 impl_ok1 impl_ok2 para =
   (find id_base, find id_next, find id_end)
   with Not_found -> assert false in
   let spooky_case _ =
-  (lseg_kind_equal Sil.Lseg_PE k_res)
+  (equal_lseg_kind Sil.Lseg_PE k_res)
   && (check_allocatedness p_leftover inst_end)
   && ((check_disequal p_start inst_base inst_next)
   || (check_disequal p_start inst_next inst_end)) in
@@ -836,7 +836,7 @@ module IdMap = Map.Make (Ident) (** maps from identifiers *)
 module HpredSet =
   Set.Make(struct
     type t = Sil.hpred
-    let compare = Sil.hpred_compare ~inst:false
+    let compare = Sil.compare_hpred ~inst:false
   end)
 
 let hpred_entries hpred = match hpred with
@@ -904,9 +904,9 @@ let get_cycle root prop =
     match el with
     | [] -> path, false
     | (f, e):: el' ->
-        if Sil.strexp_equal e e_root then
+        if Sil.equal_strexp e e_root then
           (et_src, f, e):: path, true
-        else if IList.mem Sil.strexp_equal e visited then
+        else if IList.mem Sil.equal_strexp e visited then
           path, false
         else (
           let visited' = (fst et_src):: visited in
@@ -954,7 +954,7 @@ let get_var_retain_cycle prop_ =
   let sigma = prop_.Prop.sigma in
   let is_pvar v h =
     match h with
-    | Sil.Hpointsto (Exp.Lvar _, v', _) when Sil.strexp_equal v v' -> true
+    | Sil.Hpointsto (Exp.Lvar _, v', _) when Sil.equal_strexp v v' -> true
     | _ -> false in
   let is_hpred_block v h =
     match h, v with
diff --git a/infer/src/backend/absarray.ml b/infer/src/backend/absarray.ml
index a22afd4c8..8727b6264 100644
--- a/infer/src/backend/absarray.ml
+++ b/infer/src/backend/absarray.ml
@@ -271,7 +271,7 @@ end = struct
   let replace_strexp_sigma footprint_part ((_, hpred, syn_offs) : t) se_in sigma_in =
     let new_sigma = hpred :: sigma_in in
     let sigma' = replace_strexp tenv footprint_part (new_sigma, hpred, syn_offs) se_in in
-    IList.sort Sil.hpred_compare sigma'
+    IList.sort Sil.compare_hpred sigma'
 *)
 end
 
diff --git a/infer/src/backend/dom.ml b/infer/src/backend/dom.ml
index 8a9158821..7d7c39b18 100644
--- a/infer/src/backend/dom.ml
+++ b/infer/src/backend/dom.ml
@@ -32,10 +32,10 @@ let sigma_equal sigma1 sigma2 =
     | [], _:: _ | _:: _, [] ->
         (L.d_strln "failure reason 1"; raise IList.Fail)
     | hpred1:: sigma1_rest', hpred2:: sigma2_rest' ->
-        if Sil.hpred_equal hpred1 hpred2 then f sigma1_rest' sigma2_rest'
+        if Sil.equal_hpred hpred1 hpred2 then f sigma1_rest' sigma2_rest'
         else (L.d_strln "failure reason 2"; raise IList.Fail) in
-  let sigma1_sorted = IList.sort Sil.hpred_compare sigma1 in
-  let sigma2_sorted = IList.sort Sil.hpred_compare sigma2 in
+  let sigma1_sorted = IList.sort Sil.compare_hpred sigma1 in
+  let sigma2_sorted = IList.sort Sil.compare_hpred sigma2 in
   f sigma1_sorted sigma2_sorted
 
 let sigma_get_start_lexps_sort sigma =
@@ -1436,7 +1436,7 @@ let rec sigma_partial_join' tenv mode (sigma_acc: Prop.sigma)
 
     | Some (Sil.Hlseg (k, _, _, _, _) as lseg), None
     | Some (Sil.Hdllseg (k, _, _, _, _, _, _) as lseg), None ->
-        if (not Config.nelseg) || (Sil.lseg_kind_equal k Sil.Lseg_PE) then
+        if (not Config.nelseg) || (Sil.equal_lseg_kind k Sil.Lseg_PE) then
           let sigma_acc' = join_list_and_non Lhs e lseg e1 e2 :: sigma_acc in
           sigma_partial_join' tenv mode sigma_acc' sigma1 sigma2
         else
@@ -1444,7 +1444,7 @@ let rec sigma_partial_join' tenv mode (sigma_acc: Prop.sigma)
 
     | None, Some (Sil.Hlseg (k, _, _, _, _) as lseg)
     | None, Some (Sil.Hdllseg (k, _, _, _, _, _, _) as lseg) ->
-        if (not Config.nelseg) || (Sil.lseg_kind_equal k Sil.Lseg_PE) then
+        if (not Config.nelseg) || (Sil.equal_lseg_kind k Sil.Lseg_PE) then
           let sigma_acc' = join_list_and_non Rhs e lseg e2 e1 :: sigma_acc in
           sigma_partial_join' tenv mode sigma_acc' sigma1 sigma2
         else
@@ -1675,7 +1675,7 @@ let pi_partial_join tenv mode
       IList.fold_left (handle_atom_with_widening Rhs p1 pi1) [] pi2 in
     if Config.trace_join then
       (L.d_str "atom_list2: "; Prop.d_pi atom_list2; L.d_ln ());
-    let atom_list_combined = IList.inter Sil.atom_compare atom_list1 atom_list2 in
+    let atom_list_combined = IList.inter Sil.compare_atom atom_list1 atom_list2 in
     if Config.trace_join then
       (L.d_str "atom_list_combined: "; Prop.d_pi atom_list_combined; L.d_ln ());
     atom_list_combined
@@ -1722,7 +1722,7 @@ let eprop_partial_meet tenv (ep1: 'a Prop.t) (ep2: 'b Prop.t) : 'c Prop.t =
     let sub2 = ep2.Prop.sub in
     let range1 = Sil.sub_range sub1 in
     let f e = Sil.fav_for_all (Sil.exp_fav e) Ident.is_normal in
-    Sil.sub_equal sub1 sub2 && IList.for_all f range1 in
+    Sil.equal_subst sub1 sub2 && IList.for_all f range1 in
 
   if not (sub_check ()) then
     (L.d_strln "sub_check() failed"; raise IList.Fail)
diff --git a/infer/src/backend/dotty.ml b/infer/src/backend/dotty.ml
index 32bd6d1bf..31bd1fe58 100644
--- a/infer/src/backend/dotty.ml
+++ b/infer/src/backend/dotty.ml
@@ -384,7 +384,7 @@ let in_cycle cycle edge =
   match cycle with
   | Some cycle' ->
       IList.mem (fun (fn, se) (_,fn',se') ->
-          Ident.equal_fieldname fn fn' && Sil.strexp_equal se se') edge cycle'
+          Ident.equal_fieldname fn fn' && Sil.equal_strexp se se') edge cycle'
   | _ -> false
 
 let node_in_cycle cycle node =
diff --git a/infer/src/backend/match.ml b/infer/src/backend/match.ml
index f0bca1a23..cc34f174d 100644
--- a/infer/src/backend/match.ml
+++ b/infer/src/backend/match.ml
@@ -335,7 +335,7 @@ let rec iter_match_with_impl tenv iter condition sub vars hpat hpats =
         | (None, _) when not hpat.flag ->
             (* L.out "@[.... iter_match_with_impl (lseg not-matched) ....@\n@."; *)
             None
-        | (None, _) when Sil.lseg_kind_equal k2 Sil.Lseg_NE ->
+        | (None, _) when Sil.equal_lseg_kind k2 Sil.Lseg_NE ->
             (* L.out "@[.... iter_match_with_impl (lseg not-matched) ....@\n@."; *)
             do_para_lseg ()
         | (None, _) ->
@@ -390,7 +390,7 @@ let rec iter_match_with_impl tenv iter condition sub vars hpat hpats =
               | Some _ -> None
       in begin match ((Prop.prop_iter_find iter filter), hpats) with
         | (None, _) when not hpat.flag -> None
-        | (None, _) when Sil.lseg_kind_equal k2 Sil.Lseg_NE -> do_para_dllseg ()
+        | (None, _) when Sil.equal_lseg_kind k2 Sil.Lseg_NE -> do_para_dllseg ()
         | (None, _) -> execute_with_backtracking [do_emp_dllseg; do_para_dllseg]
         | (Some iter_cur, []) -> do_empty_hpats iter_cur ()
         | (Some iter_cur, _) -> execute_with_backtracking [do_nonempty_hpats iter_cur; do_next iter_cur]
diff --git a/infer/src/backend/preanal.ml b/infer/src/backend/preanal.ml
index f2f304917..045ccb0a8 100644
--- a/infer/src/backend/preanal.ml
+++ b/infer/src/backend/preanal.ml
@@ -127,7 +127,7 @@ module NullifyTransferFunctions = struct
   let is_last_instr_in_node instr node =
     let rec is_last_instr instr = function
       | [] -> true
-      | last_instr :: [] -> Sil.instr_compare instr last_instr = 0
+      | last_instr :: [] -> Sil.compare_instr instr last_instr = 0
       | _ :: instrs -> is_last_instr instr instrs in
     is_last_instr instr (CFG.instrs node)
 
diff --git a/infer/src/backend/prop.ml b/infer/src/backend/prop.ml
index da214226b..660ee8cc2 100644
--- a/infer/src/backend/prop.ml
+++ b/infer/src/backend/prop.ml
@@ -112,7 +112,7 @@ let rec pi_compare pi1 pi2 =
     | ([], _:: _) -> - 1
     | (_:: _,[]) -> 1
     | (a1:: pi1', a2:: pi2') ->
-        let n = Sil.atom_compare a1 a2 in
+        let n = Sil.compare_atom a1 a2 in
         if n <> 0 then n
         else pi_compare pi1' pi2'
 
@@ -127,7 +127,7 @@ let rec sigma_compare sigma1 sigma2 =
     | ([], _:: _) -> - 1
     | (_:: _,[]) -> 1
     | (h1:: sigma1', h2:: sigma2') ->
-        let n = Sil.hpred_compare h1 h2 in
+        let n = Sil.compare_hpred h1 h2 in
         if n <> 0 then n
         else sigma_compare sigma1' sigma2'
 
@@ -137,7 +137,7 @@ let sigma_equal sigma1 sigma2 =
 (** Comparison between propositions. Lexicographical order. *)
 let prop_compare p1 p2 =
   sigma_compare p1.sigma p2.sigma
-  |> next Sil.sub_compare p1.sub p2.sub
+  |> next Sil.compare_subst p1.sub p2.sub
   |> next pi_compare p1.pi p2.pi
   |> next sigma_compare p1.sigma_fp p2.sigma_fp
   |> next pi_compare p1.pi_fp p2.pi_fp
@@ -230,7 +230,7 @@ let sigma_get_stack_nonstack only_local_vars sigma =
 let pp_sigma_simple pe env fmt sigma =
   let sigma_stack, sigma_nonstack = sigma_get_stack_nonstack false sigma in
   let pp_stack fmt _sg =
-    let sg = IList.sort Sil.hpred_compare _sg in
+    let sg = IList.sort Sil.compare_hpred _sg in
     if sg != [] then Format.fprintf fmt "%a" (pp_semicolon_seq pe (pp_hpred_stackvar pe)) sg in
   let pp_nl fmt doit = if doit then
       (match pe.pe_kind with
@@ -549,7 +549,7 @@ let rec pi_sorted_remove_redundant (pi : pi) = match pi with
       (* first inequality redundant *)
       pi_sorted_remove_redundant (a2 :: rest)
   | a1:: a2:: rest ->
-      if Sil.atom_equal a1 a2 then pi_sorted_remove_redundant (a2 :: rest)
+      if Sil.equal_atom a1 a2 then pi_sorted_remove_redundant (a2 :: rest)
       else a1 :: pi_sorted_remove_redundant (a2 :: rest)
   | [a] -> [a]
   | [] -> []
@@ -1314,13 +1314,13 @@ module Normalize = struct
       when IntLit.isone i ->
         let lower = Exp.int (n -- IntLit.one) in
         let a_lower : Sil.atom = Aeq (BinOp (Lt, lower, Var id), Exp.one) in
-        if not (IList.mem Sil.atom_equal a_lower p.pi) then a'
+        if not (IList.mem Sil.equal_atom a_lower p.pi) then a'
         else Aeq (Var id, Exp.int n)
     | Aeq (BinOp (Lt, Const (Cint n), Var id), Const (Cint i))
       when IntLit.isone i ->
         let upper = Exp.int (n ++ IntLit.one) in
         let a_upper : Sil.atom = Aeq (BinOp (Le, Var id, upper), Exp.one) in
-        if not (IList.mem Sil.atom_equal a_upper p.pi) then a'
+        if not (IList.mem Sil.equal_atom a_upper p.pi) then a'
         else Aeq (Var id, upper)
     | Aeq (BinOp (Ne, e1, e2), Const (Cint i)) when IntLit.isone i ->
         Aneq (e1, e2)
@@ -1338,7 +1338,7 @@ module Normalize = struct
               let fld_cnts' =
                 IList.map (fun (fld, cnt) ->
                     fld, strexp_normalize tenv sub cnt) fld_cnts in
-              let fld_cnts'' = IList.sort Sil.fld_strexp_compare fld_cnts' in
+              let fld_cnts'' = IList.sort [%compare: Ident.fieldname * Sil.strexp] fld_cnts' in
               Estruct (fld_cnts'', inst)
         end
     | Earray (len, idx_cnts, inst) ->
@@ -1353,7 +1353,7 @@ module Normalize = struct
                     let idx' = exp_normalize tenv sub idx in
                     idx', strexp_normalize tenv sub cnt) idx_cnts in
               let idx_cnts'' =
-                IList.sort Sil.exp_strexp_compare idx_cnts' in
+                IList.sort [%compare: Exp.t * Sil.strexp] idx_cnts' in
               Earray (len', idx_cnts'', inst)
         end
 
@@ -1433,18 +1433,18 @@ module Normalize = struct
 
   and hpara_normalize tenv (para : Sil.hpara) =
     let normalized_body = IList.map (hpred_normalize tenv Sil.sub_empty) (para.body) in
-    let sorted_body = IList.sort Sil.hpred_compare normalized_body in
+    let sorted_body = IList.sort Sil.compare_hpred normalized_body in
     { para with body = sorted_body }
 
   and hpara_dll_normalize tenv (para : Sil.hpara_dll) =
     let normalized_body = IList.map (hpred_normalize tenv Sil.sub_empty) (para.body_dll) in
-    let sorted_body = IList.sort Sil.hpred_compare normalized_body in
+    let sorted_body = IList.sort Sil.compare_hpred normalized_body in
     { para with body_dll = sorted_body }
 
 
   let sigma_normalize tenv sub sigma =
     let sigma' =
-      IList.stable_sort Sil.hpred_compare (IList.map (hpred_normalize tenv sub) sigma) in
+      IList.stable_sort Sil.compare_hpred (IList.map (hpred_normalize tenv sub) sigma) in
     if sigma_equal sigma sigma' then sigma else sigma'
 
   let pi_tighten_ineq tenv pi =
@@ -1540,7 +1540,7 @@ module Normalize = struct
       | _ -> true in
     let pi' =
       IList.stable_sort
-        Sil.atom_compare
+        Sil.compare_atom
         ((IList.filter filter_useful_atom nonineq_list) @ ineq_list) in
     let pi'' = pi_sorted_remove_redundant pi' in
     if pi_equal pi0 pi'' then pi0 else pi''
@@ -1580,12 +1580,12 @@ module Normalize = struct
   let sub_normalize sub =
     let f (id, e) = (not (Ident.is_primed id)) && (not (Sil.ident_in_exp id e)) in
     let sub' = Sil.sub_filter_pair f sub in
-    if Sil.sub_equal sub sub' then sub else sub'
+    if Sil.equal_subst sub sub' then sub else sub'
 
   (** Conjoin a pure atomic predicate by normal conjunction. *)
   let rec prop_atom_and tenv ?(footprint=false) (p : normal t) a : normal t =
     let a' = normalize_and_strengthen_atom tenv p a in
-    if IList.mem Sil.atom_equal a' p.pi then p
+    if IList.mem Sil.equal_atom a' p.pi then p
     else begin
       let p' =
         match a' with
@@ -2152,7 +2152,7 @@ let exist_quantify tenv fav (prop : normal t) : normal t =
       (* throw away x=E if x becomes _x *)
       let mem_idlist i = IList.exists (fun id -> Ident.equal i id) in
       let sub = Sil.sub_filter (fun i -> not (mem_idlist i ids)) prop.sub in
-      if Sil.sub_equal sub prop.sub then prop
+      if Sil.equal_subst sub prop.sub then prop
       else unsafe_cast_to_normal (set prop ~sub) in
     (*
     L.out "@[<2>.... Existential Quantification ....\n";
@@ -2457,7 +2457,7 @@ let rec strexp_gc_fields (fav: Sil.fav) (se : Sil.strexp) =
       let fsel' =
         let fselo' = IList.filter (function | (_, Some _) -> true | _ -> false) fselo in
         IList.map (function (f, seo) -> (f, unSome seo)) fselo' in
-      if Sil.fld_strexp_list_compare fsel fsel' = 0 then Some se
+      if [%compare.equal: (Ident.fieldname * Sil.strexp) list] fsel fsel' then Some se
       else Some (Sil.Estruct (fsel', inst))
   | Earray _ ->
       Some se
@@ -2469,7 +2469,7 @@ let hpred_gc_fields (fav: Sil.fav) (hpred : Sil.hpred) : Sil.hpred = match hpred
       (match strexp_gc_fields fav se with
        | None -> hpred
        | Some se' ->
-           if Sil.strexp_compare se se' = 0 then hpred
+           if Sil.compare_strexp se se' = 0 then hpred
            else Hpointsto (e, se', te))
   | Hlseg _ | Hdllseg _ ->
       hpred
diff --git a/infer/src/backend/propgraph.ml b/infer/src/backend/propgraph.ml
index 7e83a6e7e..8a2e4bc4c 100644
--- a/infer/src/backend/propgraph.ml
+++ b/infer/src/backend/propgraph.ml
@@ -98,8 +98,8 @@ let get_edges footprint_part g =
   IList.map (fun hpred -> Ehpred hpred) hpreds @ IList.map (fun a -> Eatom a) atoms @ IList.map (fun entry -> Esub_entry entry) subst_entries
 
 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
+  | Ehpred hp1, Ehpred hp2 -> Sil.equal_hpred hp1 hp2
+  | Eatom a1, Eatom a2 -> Sil.equal_atom a1 a2
   | Esub_entry (x1, e1), Esub_entry (x2, e2) -> Ident.equal x1 x2 && Exp.equal e1 e2
   | _ -> false
 
diff --git a/infer/src/backend/prover.ml b/infer/src/backend/prover.ml
index 1a5809005..c10d2550c 100644
--- a/infer/src/backend/prover.ml
+++ b/infer/src/backend/prover.ml
@@ -565,7 +565,7 @@ let check_equal tenv prop e1 e2 =
     let eq = Sil.Aeq(n_e1, n_e2) in
     let n_eq = Prop.atom_normalize_prop tenv prop eq in
     let pi = prop.Prop.pi in
-    IList.exists (Sil.atom_equal n_eq) pi in
+    IList.exists (Sil.equal_atom n_eq) pi in
   check_equal () || check_equal_const () || check_equal_pi ()
 
 (** Check [ |- e=0]. Result [false] means "don't know". *)
@@ -769,7 +769,7 @@ let check_atom tenv prop a0 =
     when IntLit.isone i -> check_lt_normalized tenv prop e1 e2
   | Sil.Aeq (e1, e2) -> check_equal tenv prop e1 e2
   | Sil.Aneq (e1, e2) -> check_disequal tenv prop e1 e2
-  | Sil.Apred _ | Anpred _ -> IList.exists (Sil.atom_equal a) prop.Prop.pi
+  | Sil.Apred _ | Anpred _ -> IList.exists (Sil.equal_atom a) prop.Prop.pi
 
 (** Check [prop |- e1<=e2]. Result [false] means "don't know". *)
 let check_le tenv prop e1 e2 =
@@ -1432,12 +1432,12 @@ let filter_ne_lhs sub e0 = function
 
 let filter_hpred sub hpred2 hpred1 = match (Sil.hpred_sub sub hpred1), hpred2 with
   | Sil.Hlseg(Sil.Lseg_NE, hpara1, e1, f1, el1), Sil.Hlseg(Sil.Lseg_PE, _, _, _, _) ->
-      if Sil.hpred_equal (Sil.Hlseg(Sil.Lseg_PE, hpara1, e1, f1, el1)) hpred2 then Some false else None
+      if Sil.equal_hpred (Sil.Hlseg(Sil.Lseg_PE, hpara1, e1, f1, el1)) hpred2 then Some false else None
   | 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 *)
+      if Sil.equal_hpred (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 Exp.equal e1 e2 then Some false else None
-  | hpred1, hpred2 -> if Sil.hpred_equal hpred1 hpred2 then Some false else None
+  | hpred1, hpred2 -> if Sil.equal_hpred hpred1 hpred2 then Some false else None
 
 let hpred_has_primed_lhs sub hpred =
   let rec find_primed e = match e with
diff --git a/infer/src/backend/rearrange.ml b/infer/src/backend/rearrange.ml
index 8d411911b..d1a2df363 100644
--- a/infer/src/backend/rearrange.ml
+++ b/infer/src/backend/rearrange.ml
@@ -217,7 +217,7 @@ let rec _strexp_extend_values
                   let replace acc (res_atoms', res_se', res_typ') =
                     let replace_fse = replace_fv res_se' in
                     let res_fsel' =
-                      IList.sort Sil.fld_strexp_compare (IList.map replace_fse fsel) in
+                      IList.sort [%compare: Ident.fieldname * Sil.strexp] (IList.map replace_fse fsel) in
                     let replace_fta (f, t, a) =
                       let f', t' = replace_fv res_typ' (f, t) in
                       (f', t', a) in
@@ -230,7 +230,7 @@ let rec _strexp_extend_values
                   let atoms', se', res_typ' =
                     create_struct_values
                       pname tenv orig_prop footprint_part kind max_stamp typ' off' inst in
-                  let res_fsel' = IList.sort Sil.fld_strexp_compare ((f, se'):: fsel) in
+                  let res_fsel' = IList.sort [%compare: Ident.fieldname * Sil.strexp] ((f, se'):: fsel) in
                   let replace_fta (f', t', a') =
                     if Ident.equal_fieldname f' f then (f, res_typ', a') else (f', t', a') in
                   let fields' =
@@ -312,7 +312,7 @@ and array_case_analysis_index pname tenv orig_prop
       create_struct_values
         pname tenv orig_prop footprint_part kind max_stamp typ_cont off inst in
     check_sound elem_typ;
-    let cont_new = IList.sort Sil.exp_strexp_compare ((index, elem_se):: array_cont) in
+    let cont_new = IList.sort [%compare: Exp.t * Sil.strexp] ((index, elem_se):: array_cont) in
     let array_new = Sil.Earray (array_len, cont_new, inst_arr) in
     let typ_new = Typ.Tarray (elem_typ, typ_array_len) in
     [(atoms, array_new, typ_new)]
@@ -325,7 +325,7 @@ and array_case_analysis_index pname tenv orig_prop
           create_struct_values
             pname tenv orig_prop footprint_part kind max_stamp typ_cont off inst in
         check_sound elem_typ;
-        let cont_new = IList.sort Sil.exp_strexp_compare ((index, elem_se):: array_cont) in
+        let cont_new = IList.sort [%compare: Exp.t * Sil.strexp] ((index, elem_se):: array_cont) in
         let array_new = Sil.Earray (array_len, cont_new, inst_arr) in
         let typ_new = Typ.Tarray (elem_typ, typ_array_len) in
         [(atoms, array_new, typ_new)]
@@ -554,7 +554,7 @@ let prop_iter_extend_ptsto pname tenv orig_prop iter lexp inst =
             | _ ->
                 L.d_warning "Cannot extend "; Sil.d_exp lexp; L.d_strln " in"; Prop.d_prop (Prop.prop_iter_to_prop tenv iter); L.d_ln();
                 [([], footprint_sigma)] in
-          IList.map (fun (atoms, sigma') -> (atoms, IList.stable_sort Sil.hpred_compare sigma')) atoms_sigma_list in
+          IList.map (fun (atoms, sigma') -> (atoms, IList.stable_sort Sil.compare_hpred sigma')) atoms_sigma_list in
         let iter_atoms_fp_sigma_list =
           list_product iter_list atoms_fp_sigma_list in
         IList.map (fun (iter, (atoms, fp_sigma)) ->
diff --git a/infer/src/backend/state.ml b/infer/src/backend/state.ml
index d15efed6e..1eab0a550 100644
--- a/infer/src/backend/state.ml
+++ b/infer/src/backend/state.ml
@@ -217,7 +217,7 @@ let mk_find_duplicate_nodes proc_desc : (Procdesc.Node.t -> Procdesc.NodeSet.t)
         | _ -> raise Not_found in
       let duplicates =
         let equal_normalized_instrs (_, normalized_instrs') =
-          IList.compare Sil.instr_compare node_normalized_instrs normalized_instrs' = 0 in
+          IList.compare Sil.compare_instr node_normalized_instrs normalized_instrs' = 0 in
         IList.filter equal_normalized_instrs elements in
       IList.fold_left
         (fun nset (node', _) -> Procdesc.NodeSet.add node' nset)
diff --git a/infer/src/backend/tabulation.ml b/infer/src/backend/tabulation.ml
index 881987fb5..9804c5be1 100644
--- a/infer/src/backend/tabulation.ml
+++ b/infer/src/backend/tabulation.ml
@@ -403,7 +403,7 @@ let hpred_lhs_compare hpred1 hpred2 = match hpred1, hpred2 with
   | Sil.Hpointsto(e1, _, _), Sil.Hpointsto(e2, _, _) -> Exp.compare e1 e2
   | Sil.Hpointsto _, _ -> - 1
   | _, Sil.Hpointsto _ -> 1
-  | hpred1, hpred2 -> Sil.hpred_compare hpred1 hpred2
+  | hpred1, hpred2 -> Sil.compare_hpred hpred1 hpred2
 
 (** set the inst everywhere in a sexp *)
 let rec sexp_set_inst inst = function
@@ -974,7 +974,7 @@ let do_taint_check tenv caller_pname callee_pname calling_prop missing_pi sub ac
       (Exp.Map.exists
          (fun _ (_, untaint_atoms) ->
             IList.exists
-              (fun a -> Sil.atom_equal atom a)
+              (fun a -> Sil.equal_atom atom a)
               untaint_atoms)
          taint_untaint_exp_map) in
   check_taint_on_variadic_function tenv callee_pname caller_pname actual_params calling_prop;
diff --git a/infer/src/checkers/repeatedCallsChecker.ml b/infer/src/checkers/repeatedCallsChecker.ml
index 4c95f3c90..2efe30490 100644
--- a/infer/src/checkers/repeatedCallsChecker.ml
+++ b/infer/src/checkers/repeatedCallsChecker.ml
@@ -25,9 +25,9 @@ struct
         | Sil.Call (_, e1, etl1, _, cf1), Sil.Call (_, e2, etl2, _, cf2) ->
             (* ignore return ids and call flags *)
             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 let n = IList.compare [%compare: Exp.t * Typ.t] etl1 etl2 in
               if n <> 0 then n else CallFlags.compare cf1 cf2
-        | _ -> Sil.instr_compare i1 i2
+        | _ -> Sil.compare_instr i1 i2
     end)
 
   type extension = InstrSet.t