diff --git a/infer/src/IR/Pvar.re b/infer/src/IR/Pvar.re
index b3bad8fb9..c87b55639 100644
--- a/infer/src/IR/Pvar.re
+++ b/infer/src/IR/Pvar.re
@@ -36,9 +36,6 @@ type pvar_kind =
 /** Names for program variables. */
 and t = {pv_hash: int, pv_name: Mangled.t, pv_kind: pvar_kind} [@@deriving compare];
 
-let compare_alpha pv1 pv2 =>
-  [%compare : (Mangled.t, pvar_kind)] (pv1.pv_name, pv1.pv_kind) (pv2.pv_name, pv2.pv_kind);
-
 let equal = [%compare.equal : t];
 
 let pp_translation_unit fmt =>
@@ -384,11 +381,3 @@ let get_initializer_pname {pv_name, pv_kind} =>
     )
   | _ => None
   };
-
-module Set =
-  PrettyPrintable.MakePPCompareSet {
-    type nonrec t = t;
-    let compare = compare;
-    let compare_pp = compare_alpha;
-    let pp = pp Pp.text;
-  };
diff --git a/infer/src/IR/Pvar.rei b/infer/src/IR/Pvar.rei
index a3de879be..0a05e75e3 100644
--- a/infer/src/IR/Pvar.rei
+++ b/infer/src/IR/Pvar.rei
@@ -32,10 +32,6 @@ type t [@@deriving compare];
 let equal: t => t => bool;
 
 
-/** Compare two pvar's in alphabetical order */
-let compare_alpha: t => t => int;
-
-
 /** Dump a program variable. */
 let d: t => unit;
 
@@ -174,5 +170,3 @@ let is_pod: t => bool;
 
 /** Get the procname of the initializer function for the given global variable */
 let get_initializer_pname: t => option Typ.Procname.t;
-
-module Set: PrettyPrintable.PPSet with type elt = t;
diff --git a/infer/src/backend/preanal.ml b/infer/src/backend/preanal.ml
index 96c7c9a7c..a8c86d96d 100644
--- a/infer/src/backend/preanal.ml
+++ b/infer/src/backend/preanal.ml
@@ -95,7 +95,7 @@ module BackwardCfg = ProcCfg.OneInstrPerNode(ProcCfg.Backward(ProcCfg.Exceptiona
 
 module LivenessAnalysis = AbstractInterpreter.Make (BackwardCfg) (Liveness.TransferFunctions)
 
-module VarDomain = AbstractDomain.FiniteSet(Var.Set)
+module VarDomain = Liveness.Domain
 
 (** computes the non-nullified reaching definitions at the end of each node by building on the
     results of a liveness analysis to be precise, what we want to compute is:
@@ -208,7 +208,7 @@ let add_nullify_instrs pdesc tenv liveness_inv_map =
         match NullifyAnalysis.extract_post (ProcCfg.Exceptional.id node) nullify_inv_map with
         | Some (_, to_nullify) ->
             let pvars_to_nullify, ids_to_remove =
-              Var.Set.fold
+              VarDomain.fold
                 (fun var (pvars_acc, ids_acc) -> match Var.to_exp var with
                    (* we nullify all address taken variables at the end of the procedure *)
                    | Exp.Lvar pvar when not (AddressTaken.Domain.mem pvar address_taken_vars) ->
diff --git a/infer/src/base/PrettyPrintable.ml b/infer/src/base/PrettyPrintable.ml
index d45dfcf77..92eafb42c 100644
--- a/infer/src/base/PrettyPrintable.ml
+++ b/infer/src/base/PrettyPrintable.ml
@@ -48,17 +48,6 @@ module MakePPSet (Ord : PrintableOrderedType) = struct
     pp_collection ~pp_item:pp_element fmt (elements s)
 end
 
-module MakePPCompareSet
-    (Ord : sig include PrintableOrderedType val compare_pp : t -> t -> int end) = struct
-  include Caml.Set.Make(Ord)
-
-  let pp_element = Ord.pp
-
-  let pp fmt s =
-    let elements_alpha = List.sort ~cmp:Ord.compare_pp (elements s) in
-    pp_collection ~pp_item:pp_element fmt elements_alpha
-end
-
 module MakePPMap (Ord : PrintableOrderedType) = struct
   include Caml.Map.Make(Ord)
 
diff --git a/infer/src/base/PrettyPrintable.mli b/infer/src/base/PrettyPrintable.mli
index 2e3bae4a1..7c6e84b5d 100644
--- a/infer/src/base/PrettyPrintable.mli
+++ b/infer/src/base/PrettyPrintable.mli
@@ -35,12 +35,4 @@ end
 
 module MakePPSet (Ord : PrintableOrderedType) : (PPSet with type elt = Ord.t)
 
-(** Use a comparison function to determine the order of the elements printed *)
-module MakePPCompareSet
-    (Ord : sig
-       include PrintableOrderedType
-       val compare_pp : t -> t -> int
-     end)
-  : (PPSet with type elt = Ord.t)
-
 module MakePPMap (Ord : PrintableOrderedType) : (PPMap with type key = Ord.t)
diff --git a/infer/src/bufferoverrun/absLoc.ml b/infer/src/bufferoverrun/absLoc.ml
index b4f0f8113..801a0a280 100644
--- a/infer/src/bufferoverrun/absLoc.ml
+++ b/infer/src/bufferoverrun/absLoc.ml
@@ -26,16 +26,16 @@ struct
     | Allocsite of Allocsite.t
     | Field of t * Fieldname.t
     | Unknown
-      [@@deriving compare]
+  [@@deriving compare]
 
   let unknown = Unknown
   let rec pp fmt = function
     | Var v ->
-      Var.pp F.str_formatter v;
-      let s = F.flush_str_formatter () in
-      if s.[0] = '&' then
-        F.fprintf fmt "%s" (String.sub s 1 (String.length s - 1))
-      else F.fprintf fmt "%s" s
+        Var.pp F.str_formatter v;
+        let s = F.flush_str_formatter () in
+        if s.[0] = '&' then
+          F.fprintf fmt "%s" (String.sub s 1 (String.length s - 1))
+        else F.fprintf fmt "%s" s
     | Allocsite a -> Allocsite.pp fmt a
     | Field (l, f) -> F.fprintf fmt "%a.%a" pp l Fieldname.pp f
     | Unknown -> F.fprintf fmt "Unknown"
@@ -51,13 +51,13 @@ struct
 
   let is_return = function
     | Var (Var.ProgramVar x) ->
-      Mangled.equal (Pvar.get_name x) Ident.name_return
+        Mangled.equal (Pvar.get_name x) Ident.name_return
     | _ -> false
 end
 
 module PowLoc =
 struct
-  include AbstractDomain.FiniteSet(PrettyPrintable.MakePPSet(Loc))
+  include AbstractDomain.FiniteSet(Loc)
 
   let bot = empty
   let is_bot = is_empty
diff --git a/infer/src/bufferoverrun/arrayBlk.ml b/infer/src/bufferoverrun/arrayBlk.ml
index 2c7b625e2..dfb39e7e7 100644
--- a/infer/src/bufferoverrun/arrayBlk.ml
+++ b/infer/src/bufferoverrun/arrayBlk.ml
@@ -116,16 +116,7 @@ struct
     = fun arr1 arr2 -> { arr1 with offset = Itv.prune_ne arr1.offset arr2.offset }
 end
 
-module PPMap =
-struct
-  include PrettyPrintable.MakePPMap (Allocsite)
-
-  let pp ~pp_value fmt m =
-    let pp_item fmt (k, v) = F.fprintf fmt "(%a, %a)" pp_key k pp_value v in
-    PrettyPrintable.pp_collection ~pp_item fmt (bindings m)
-end
-
-include AbstractDomain.Map (PPMap) (ArrInfo)
+include AbstractDomain.Map (Allocsite) (ArrInfo)
 
 let bot : astate
   = empty
diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml
index a279b9de1..a82095be3 100644
--- a/infer/src/bufferoverrun/bufferOverrunDomain.ml
+++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml
@@ -28,141 +28,140 @@ struct
       loc : Location.t;
       trace : trace;
       id : string }
-      [@@deriving compare]
-  and trace = Intra of Typ.Procname.t
-            | Inter of Typ.Procname.t * Typ.Procname.t * Location.t
-                    [@@deriving compare]
-
-  and astate = t
-
-  let set_size_pos : t -> t
-    = fun c ->
-      if Itv.Bound.lt (Itv.lb c.size) Itv.Bound.zero
-      then { c with size = Itv.make Itv.Bound.zero (Itv.ub c.size) }
-      else c
-
-  let string_of_location : Location.t -> string
-    = fun loc ->
-      let fname = SourceFile.to_string loc.Location.file in
-      let pos = Location.to_string loc in
-      F.fprintf F.str_formatter "%s:%s" fname pos;
-      F.flush_str_formatter ()
-
-  let pp_location : F.formatter -> t -> unit
-    = fun fmt c ->
-      F.fprintf fmt "%s" (string_of_location c.loc)
+  [@@deriving compare]
+and trace = Intra of Typ.Procname.t
+          | Inter of Typ.Procname.t * Typ.Procname.t * Location.t
+[@@deriving compare]
+
+and astate = t
+
+let set_size_pos : t -> t
+  = fun c ->
+    if Itv.Bound.lt (Itv.lb c.size) Itv.Bound.zero
+    then { c with size = Itv.make Itv.Bound.zero (Itv.ub c.size) }
+    else c
+
+let string_of_location : Location.t -> string
+  = fun loc ->
+    let fname = SourceFile.to_string loc.Location.file in
+    let pos = Location.to_string loc in
+    F.fprintf F.str_formatter "%s:%s" fname pos;
+    F.flush_str_formatter ()
+
+let pp_location : F.formatter -> t -> unit
+  = fun fmt c ->
+    F.fprintf fmt "%s" (string_of_location c.loc)
 
-  let pp : F.formatter -> t -> unit
-    = fun fmt c ->
-      let c = set_size_pos c in
-      if Config.bo_debug <= 1 then
-        F.fprintf fmt "%a < %a at %a" Itv.pp c.idx Itv.pp c.size pp_location c
-      else
-        match c.trace with
-          Inter (_, pname, loc) ->
+let pp : F.formatter -> t -> unit
+  = fun fmt c ->
+    let c = set_size_pos c in
+    if Config.bo_debug <= 1 then
+      F.fprintf fmt "%a < %a at %a" Itv.pp c.idx Itv.pp c.size pp_location c
+    else
+      match c.trace with
+        Inter (_, pname, loc) ->
           let pname = Typ.Procname.to_string pname in
           F.fprintf fmt "%a < %a at %a by call %s() at %s"
             Itv.pp c.idx Itv.pp c.size pp_location c pname (string_of_location loc)
-        | Intra _ -> F.fprintf fmt "%a < %a at %a" Itv.pp c.idx Itv.pp c.size pp_location c
-
-  let get_location : t -> Location.t
-    = fun c -> c.loc
-
-  let get_trace : t -> trace
-    = fun c -> c.trace
-
-  let get_proc_name : t -> Typ.Procname.t
-    = fun c -> c.proc_name
-
-  let make : Typ.Procname.t -> Location.t -> string -> idx:Itv.t -> size:Itv.t -> t
-    = fun proc_name loc id ~idx ~size ->
-      { proc_name; idx; size; loc; id ; trace = Intra proc_name }
-
-  let filter1 : t -> bool
-    = fun c ->
-      Itv.eq c.idx Itv.top || Itv.eq c.size Itv.top
-      || Itv.Bound.eq (Itv.lb c.idx) Itv.Bound.MInf
-      || Itv.Bound.eq (Itv.lb c.size) Itv.Bound.MInf
-      || (Itv.eq c.idx Itv.nat && Itv.eq c.size Itv.nat)
-
-  let filter2 : t -> bool
-    = fun c ->
-      (* basically, alarms involving infinity are filtered *)
-      (not (Itv.is_finite c.idx) || not (Itv.is_finite c.size))
-      &&                                                        (* except the following cases *)
-      not ((Itv.Bound.is_not_infty (Itv.lb c.idx) &&            (* idx non-infty lb < 0 *)
-            Itv.Bound.lt (Itv.lb c.idx) Itv.Bound.zero)
-           ||
-           (Itv.Bound.is_not_infty (Itv.lb c.idx) &&            (* idx non-infty lb > size lb *)
-            (Itv.Bound.gt (Itv.lb c.idx) (Itv.lb c.size)))
-           ||
-           (Itv.Bound.is_not_infty (Itv.lb c.idx) &&            (* idx non-infty lb > size ub *)
-            (Itv.Bound.gt (Itv.lb c.idx) (Itv.ub c.size)))
-           ||
-           (Itv.Bound.is_not_infty (Itv.ub c.idx) &&            (* idx non-infty ub > size lb *)
-            (Itv.Bound.gt (Itv.ub c.idx) (Itv.lb c.size)))
-           ||
-           (Itv.Bound.is_not_infty (Itv.ub c.idx) &&            (* idx non-infty ub > size ub *)
-            (Itv.Bound.gt (Itv.ub c.idx) (Itv.ub c.size))))
-
-  (* check buffer overrun and return its confidence *)
-  let check : t -> string option
-    = fun c ->
-      (* idx = [il, iu], size = [sl, su], we want to check that 0 <= idx < size *)
-      let c' = set_size_pos c in (* if sl < 0, use sl' = 0 *)
-      let not_overrun = Itv.lt_sem c'.idx c'.size in
-      let not_underrun = Itv.le_sem Itv.zero c'.idx in
-      (* il >= 0 and iu < sl, definitely not an error *)
-      if Itv.eq not_overrun Itv.one && Itv.eq not_underrun Itv.one then
-        None
+      | Intra _ -> F.fprintf fmt "%a < %a at %a" Itv.pp c.idx Itv.pp c.size pp_location c
+
+let get_location : t -> Location.t
+  = fun c -> c.loc
+
+let get_trace : t -> trace
+  = fun c -> c.trace
+
+let get_proc_name : t -> Typ.Procname.t
+  = fun c -> c.proc_name
+
+let make : Typ.Procname.t -> Location.t -> string -> idx:Itv.t -> size:Itv.t -> t
+  = fun proc_name loc id ~idx ~size ->
+    { proc_name; idx; size; loc; id ; trace = Intra proc_name }
+
+let filter1 : t -> bool
+  = fun c ->
+    Itv.eq c.idx Itv.top || Itv.eq c.size Itv.top
+    || Itv.Bound.eq (Itv.lb c.idx) Itv.Bound.MInf
+    || Itv.Bound.eq (Itv.lb c.size) Itv.Bound.MInf
+    || (Itv.eq c.idx Itv.nat && Itv.eq c.size Itv.nat)
+
+let filter2 : t -> bool
+  = fun c ->
+    (* basically, alarms involving infinity are filtered *)
+    (not (Itv.is_finite c.idx) || not (Itv.is_finite c.size))
+    &&                                                        (* except the following cases *)
+    not ((Itv.Bound.is_not_infty (Itv.lb c.idx) &&            (* idx non-infty lb < 0 *)
+          Itv.Bound.lt (Itv.lb c.idx) Itv.Bound.zero)
+         ||
+         (Itv.Bound.is_not_infty (Itv.lb c.idx) &&            (* idx non-infty lb > size lb *)
+          (Itv.Bound.gt (Itv.lb c.idx) (Itv.lb c.size)))
+         ||
+         (Itv.Bound.is_not_infty (Itv.lb c.idx) &&            (* idx non-infty lb > size ub *)
+          (Itv.Bound.gt (Itv.lb c.idx) (Itv.ub c.size)))
+         ||
+         (Itv.Bound.is_not_infty (Itv.ub c.idx) &&            (* idx non-infty ub > size lb *)
+          (Itv.Bound.gt (Itv.ub c.idx) (Itv.lb c.size)))
+         ||
+         (Itv.Bound.is_not_infty (Itv.ub c.idx) &&            (* idx non-infty ub > size ub *)
+          (Itv.Bound.gt (Itv.ub c.idx) (Itv.ub c.size))))
+
+(* check buffer overrun and return its confidence *)
+let check : t -> string option
+  = fun c ->
+    (* idx = [il, iu], size = [sl, su], we want to check that 0 <= idx < size *)
+    let c' = set_size_pos c in (* if sl < 0, use sl' = 0 *)
+    let not_overrun = Itv.lt_sem c'.idx c'.size in
+    let not_underrun = Itv.le_sem Itv.zero c'.idx in
+    (* il >= 0 and iu < sl, definitely not an error *)
+    if Itv.eq not_overrun Itv.one && Itv.eq not_underrun Itv.one then
+      None
       (* iu < 0 or il >= su, definitely an error *)
-      else if Itv.eq not_overrun Itv.zero || Itv.eq not_underrun Itv.zero then
-        Some Localise.BucketLevel.b1
+    else if Itv.eq not_overrun Itv.zero || Itv.eq not_underrun Itv.zero then
+      Some Localise.BucketLevel.b1
       (* su <= iu < +oo, most probably an error *)
-      else if Itv.Bound.is_not_infty (Itv.ub c.idx)
-              && Itv.Bound.le (Itv.ub c.size) (Itv.ub c.idx) then
-        Some Localise.BucketLevel.b2
+    else if Itv.Bound.is_not_infty (Itv.ub c.idx)
+         && Itv.Bound.le (Itv.ub c.size) (Itv.ub c.idx) then
+      Some Localise.BucketLevel.b2
       (* symbolic il >= sl, probably an error *)
-      else if Itv.Bound.is_symbolic (Itv.lb c.idx)
-              && Itv.Bound.le (Itv.lb c'.size) (Itv.lb c.idx) then
-        Some Localise.BucketLevel.b3
+    else if Itv.Bound.is_symbolic (Itv.lb c.idx)
+         && Itv.Bound.le (Itv.lb c'.size) (Itv.lb c.idx) then
+      Some Localise.BucketLevel.b3
       (* other symbolic bounds are probably too noisy *)
-      else if Config.bo_debug <= 1 && (Itv.is_symbolic c.idx || Itv.is_symbolic c.size) then
-        None
-      else if filter1 c then
-        Some Localise.BucketLevel.b5
-      else if filter2 c then
-        Some Localise.BucketLevel.b3
-      else
-        Some Localise.BucketLevel.b2
-
-  let invalid : t -> bool
-    = fun x -> Itv.invalid x.idx || Itv.invalid x.size
-
-  let to_string : t -> string
-    = fun c ->
-      let c = set_size_pos c in
-      "Offset: " ^ Itv.to_string c.idx ^ " Size: " ^ Itv.to_string c.size
-      ^ " @ " ^ string_of_location c.loc
-      ^ (match c.trace with
-        Inter (_, pname, _) ->
-        " by call "
-        ^ MF.monospaced_to_string (Typ.Procname.to_string pname ^ "()") ^ " "
-      | Intra _ -> "")
-
-  let subst : t -> Itv.Bound.t Itv.SubstMap.t -> Typ.Procname.t -> Typ.Procname.t -> Location.t -> t
-    = fun c subst_map caller_pname callee_pname loc ->
-      if Itv.is_symbolic c.idx || Itv.is_symbolic c.size then
-        { c with idx = Itv.subst c.idx subst_map;
-                       size = Itv.subst c.size subst_map;
-                       trace = Inter (caller_pname, callee_pname, loc) }
-      else c
+    else if Config.bo_debug <= 1 && (Itv.is_symbolic c.idx || Itv.is_symbolic c.size) then
+      None
+    else if filter1 c then
+      Some Localise.BucketLevel.b5
+    else if filter2 c then
+      Some Localise.BucketLevel.b3
+    else
+      Some Localise.BucketLevel.b2
+
+let invalid : t -> bool
+  = fun x -> Itv.invalid x.idx || Itv.invalid x.size
+
+let to_string : t -> string
+  = fun c ->
+    let c = set_size_pos c in
+    "Offset: " ^ Itv.to_string c.idx ^ " Size: " ^ Itv.to_string c.size
+    ^ " @ " ^ string_of_location c.loc
+    ^ (match c.trace with
+          Inter (_, pname, _) ->
+            " by call "
+            ^ MF.monospaced_to_string (Typ.Procname.to_string pname ^ "()") ^ " "
+        | Intra _ -> "")
+
+let subst : t -> Itv.Bound.t Itv.SubstMap.t -> Typ.Procname.t -> Typ.Procname.t -> Location.t -> t
+  = fun c subst_map caller_pname callee_pname loc ->
+    if Itv.is_symbolic c.idx || Itv.is_symbolic c.size then
+      { c with idx = Itv.subst c.idx subst_map;
+               size = Itv.subst c.size subst_map;
+               trace = Inter (caller_pname, callee_pname, loc) }
+    else c
 end
 
 module ConditionSet =
 struct
-  module PPSet = PrettyPrintable.MakePPSet (Condition)
-  include AbstractDomain.FiniteSet (PPSet)
+  include AbstractDomain.FiniteSet (Condition)
 
   module Map = Caml.Map.Make (struct
       type t = Location.t [@@deriving compare]
@@ -180,8 +179,8 @@ struct
   let group : t -> t Map.t
     = fun x ->
       fold (fun cond map ->
-        let old_set = try Map.find cond.loc map with _ -> empty in
-        Map.add cond.loc (add cond old_set) map) x Map.empty
+          let old_set = try Map.find cond.loc map with _ -> empty in
+          Map.add cond.loc (add cond old_set) map) x Map.empty
 
   let pp_summary : F.formatter -> t -> unit
     = fun fmt x ->
@@ -247,9 +246,9 @@ struct
 
   let rec joins : t list -> t
     = function
-    | [] -> bot
-    | [a] -> a
-    | a :: b -> join a (joins b)
+      | [] -> bot
+      | [a] -> a
+      | a :: b -> join a (joins b)
 
   let get_itv : t -> Itv.t
     = fun x -> x.itv
@@ -403,7 +402,7 @@ struct
   let subst : t -> Itv.Bound.t Itv.SubstMap.t -> t
     = fun x subst_map ->
       { x with itv = Itv.subst x.itv subst_map;
-                   arrayblk = ArrayBlk.subst x.arrayblk subst_map }
+               arrayblk = ArrayBlk.subst x.arrayblk subst_map }
 
   let get_symbols : t -> Itv.Symbol.t list
     = fun x ->
@@ -419,28 +418,7 @@ end
 
 module Stack =
 struct
-  module PPMap =
-  struct
-    include PrettyPrintable.MakePPMap (Loc)
-
-    let pp_collection
-      : pp_item:(F.formatter -> 'a -> unit) -> F.formatter -> 'a list -> unit
-      = fun ~pp_item fmt c ->
-        let pp_sep fmt () = F.fprintf fmt ",@," in
-        F.pp_print_list ~pp_sep pp_item fmt c
-
-    let pp
-      : pp_value:(F.formatter -> 'a -> unit) -> F.formatter -> 'a t -> unit
-      = fun ~pp_value fmt m ->
-        let pp_item fmt (k, v) =
-          F.fprintf fmt "%a -> %a" Loc.pp k pp_value v
-        in
-        F.fprintf fmt "@[<v 2>{ ";
-        pp_collection ~pp_item fmt (bindings m);
-        F.fprintf fmt " }@]"
-  end
-
-  include AbstractDomain.Map (PPMap) (Val)
+  include AbstractDomain.Map (Loc) (Val)
 
   let bot = empty
 
@@ -493,7 +471,7 @@ struct
         F.fprintf fmt " }@]"
   end
 
-  include AbstractDomain.Map (PPMap) (Val)
+  include AbstractDomain.Map (Loc) (Val)
 
   let bot = empty
 
@@ -549,49 +527,49 @@ struct
         match M.find k rhs with
         | v' -> Pvar.equal v v'
         | exception Not_found -> false
-in
-M.for_all is_in_rhs lhs
-
-let join : t -> t -> t
-  = fun x y ->
-    let join_v _ v1_opt v2_opt =
-      match v1_opt, v2_opt with
-      | None, None -> None
-      | Some v, None
-      | None, Some v -> Some v
-      | Some v1, Some v2 -> if Pvar.equal v1 v2 then Some v1 else assert false
-    in
-    M.merge join_v x y
-
-let widen : prev:t -> next:t -> num_iters:int -> t
-  = fun ~prev ~next ~num_iters:_ -> join prev next
+      in
+      M.for_all is_in_rhs lhs
 
-let pp : F.formatter -> t -> unit
-  = fun fmt x ->
-    let pp_sep fmt () = F.fprintf fmt ", @," in
-    let pp1 fmt (k, v) =
-      F.fprintf fmt "%a=%a" (Ident.pp Pp.text) k (Pvar.pp Pp.text) v
-    in
-    (* F.fprintf fmt "@[<v 0>Logical Variables :@,"; *)
-    F.fprintf fmt "@[<hov 2>{ @,";
-    F.pp_print_list ~pp_sep pp1 fmt (M.bindings x);
-    F.fprintf fmt " }@]";
-    F.fprintf fmt "@]"
-
-let load : Ident.t -> Exp.t -> t -> t
-  = fun id exp m ->
-    match exp with
-    | Exp.Lvar x -> M.add id x m
-    | _ -> m
-
-let store : Exp.t -> Exp.t -> t -> t
-  = fun e _ m ->
-    match e with
-    | Exp.Lvar x -> M.filter (fun _ y -> not (Pvar.equal x y)) m
-    | _ -> m
-
-let find : Ident.t -> t -> Pvar.t option
-  = fun k m -> try Some (M.find k m) with Not_found -> None
+  let join : t -> t -> t
+    = fun x y ->
+      let join_v _ v1_opt v2_opt =
+        match v1_opt, v2_opt with
+        | None, None -> None
+        | Some v, None
+        | None, Some v -> Some v
+        | Some v1, Some v2 -> if Pvar.equal v1 v2 then Some v1 else assert false
+      in
+      M.merge join_v x y
+
+  let widen : prev:t -> next:t -> num_iters:int -> t
+    = fun ~prev ~next ~num_iters:_ -> join prev next
+
+  let pp : F.formatter -> t -> unit
+    = fun fmt x ->
+      let pp_sep fmt () = F.fprintf fmt ", @," in
+      let pp1 fmt (k, v) =
+        F.fprintf fmt "%a=%a" (Ident.pp Pp.text) k (Pvar.pp Pp.text) v
+      in
+      (* F.fprintf fmt "@[<v 0>Logical Variables :@,"; *)
+      F.fprintf fmt "@[<hov 2>{ @,";
+      F.pp_print_list ~pp_sep pp1 fmt (M.bindings x);
+      F.fprintf fmt " }@]";
+      F.fprintf fmt "@]"
+
+  let load : Ident.t -> Exp.t -> t -> t
+    = fun id exp m ->
+      match exp with
+      | Exp.Lvar x -> M.add id x m
+      | _ -> m
+
+  let store : Exp.t -> Exp.t -> t -> t
+    = fun e _ m ->
+      match e with
+      | Exp.Lvar x -> M.filter (fun _ y -> not (Pvar.equal x y)) m
+      | _ -> m
+
+  let find : Ident.t -> t -> Pvar.t option
+    = fun k m -> try Some (M.find k m) with Not_found -> None
 end
 
 module MemReach =
diff --git a/infer/src/checkers/AbstractDomain.ml b/infer/src/checkers/AbstractDomain.ml
index 044203bb4..60298719a 100644
--- a/infer/src/checkers/AbstractDomain.ml
+++ b/infer/src/checkers/AbstractDomain.ml
@@ -136,8 +136,8 @@ module Pair (Domain1 : S) (Domain2 : S) = struct
     F.fprintf fmt "(%a, %a)" Domain1.pp astate1 Domain2.pp astate2
 end
 
-module FiniteSet (S : PrettyPrintable.PPSet) = struct
-  include S
+module FiniteSet (Element : PrettyPrintable.PrintableOrderedType) = struct
+  include PrettyPrintable.MakePPSet(Element)
   type astate = t
 
   let (<=) ~lhs ~rhs =
@@ -172,7 +172,8 @@ module InvertedSet (S : PrettyPrintable.PPSet) = struct
     join prev next
 end
 
-module Map (M : PrettyPrintable.PPMap) (ValueDomain : S) = struct
+module Map (Key : PrettyPrintable.PrintableOrderedType) (ValueDomain : S) = struct
+  module M = PrettyPrintable.MakePPMap(Key)
   include M
   type astate = ValueDomain.astate M.t
 
diff --git a/infer/src/checkers/AbstractDomain.mli b/infer/src/checkers/AbstractDomain.mli
index 041b9755d..4d796f7a8 100644
--- a/infer/src/checkers/AbstractDomain.mli
+++ b/infer/src/checkers/AbstractDomain.mli
@@ -67,8 +67,8 @@ module Pair (Domain1 : S) (Domain2 : S) : S with type astate = Domain1.astate *
 
 (** Lift a set to a powerset domain ordered by subset. The elements of the set should be drawn from
     a *finite* collection of possible values, since the widening operator here is just union. *)
-module FiniteSet (Set : PrettyPrintable.PPSet) : sig
-  include PrettyPrintable.PPSet with type t = Set.t and type elt = Set.elt
+module FiniteSet (Element : PrettyPrintable.PrintableOrderedType) : sig
+  include (module type of PrettyPrintable.MakePPSet(Element))
   include WithBottom with type astate = t
 end
 
@@ -80,9 +80,9 @@ end
 
 (** Map domain ordered by union over the set of bindings, so the bottom element is the empty map.
     Every element implicitly maps to bottom unless it is explicitly bound to something else *)
-module Map (Map : PrettyPrintable.PPMap) (ValueDomain : S) : sig
-  include PrettyPrintable.PPMap with type 'a t = 'a Map.t and type key = Map.key
-  include WithBottom with type astate = ValueDomain.astate Map.t
+module Map (Key : PrettyPrintable.PrintableOrderedType) (ValueDomain : S) : sig
+  include (module type of PrettyPrintable.MakePPMap(Key))
+  include WithBottom with type astate = ValueDomain.astate t
 end
 
 (** Map domain ordered by intersection over the set of bindings, so the top element is the empty
diff --git a/infer/src/checkers/AnnotReachabilityDomain.ml b/infer/src/checkers/AnnotReachabilityDomain.ml
index 1520ee4f3..46de520df 100644
--- a/infer/src/checkers/AnnotReachabilityDomain.ml
+++ b/infer/src/checkers/AnnotReachabilityDomain.ml
@@ -7,8 +7,8 @@
  * of patent rights can be found in the PATENTS file in the same directory.
  *)
 
-module CallSites = AbstractDomain.FiniteSet (CallSite.Set)
+module CallSites = AbstractDomain.FiniteSet (CallSite)
 
-module SinkMap = AbstractDomain.Map (Typ.Procname.Map) (CallSites)
+module SinkMap = AbstractDomain.Map (Typ.Procname) (CallSites)
 
-include AbstractDomain.Map (Annot.Map) (SinkMap)
+include AbstractDomain.Map (Annot) (SinkMap)
diff --git a/infer/src/checkers/BoundedCallTree.ml b/infer/src/checkers/BoundedCallTree.ml
index 603b77be2..0875607fd 100644
--- a/infer/src/checkers/BoundedCallTree.ml
+++ b/infer/src/checkers/BoundedCallTree.ml
@@ -14,7 +14,7 @@ module L = Logging
 
 (** find transitive procedure calls for each procedure *)
 
-module Domain = AbstractDomain.FiniteSet(Typ.Procname.Set)
+module Domain = AbstractDomain.FiniteSet(Typ.Procname)
 
 (* Store a single stacktree frame per method. That is, callees is
    always []. Instead, the expanded per-method summaries are directly stored
diff --git a/infer/src/checkers/NullabilityPreanalysis.ml b/infer/src/checkers/NullabilityPreanalysis.ml
index d691cdec1..bf1cf03a9 100644
--- a/infer/src/checkers/NullabilityPreanalysis.ml
+++ b/infer/src/checkers/NullabilityPreanalysis.ml
@@ -14,20 +14,14 @@ open! IStd
 module F = Format
 module L = Logging
 
-type t = Fieldname.t * Typ.t [@@deriving compare]
+module FieldsAssignedInConstructors =
+  AbstractDomain.FiniteSet(struct
+    type t = Fieldname.t * Typ.t [@@deriving compare]
 
-let pp fmt (fieldname, typ) =
-  F.fprintf fmt "(%a, %a)" Fieldname.pp fieldname (Typ.pp_full Pp.text) typ
-
-module DomainSet =
-  PrettyPrintable.MakePPSet(struct
-    type nonrec t = t
-    let compare = compare
-    let pp = pp
+    let pp fmt (fieldname, typ) =
+      F.fprintf fmt "(%a, %a)" Fieldname.pp fieldname (Typ.pp_full Pp.text) typ
   end)
 
-module FieldsAssignedInConstructors = AbstractDomain.FiniteSet(DomainSet)
-
 module TransferFunctions (CFG : ProcCfg.S) = struct
   module CFG = CFG
   module Domain = FieldsAssignedInConstructors
@@ -94,7 +88,7 @@ let add_nonnull_to_fields fields tenv =
                  ~fields: fields_with_annot ~statics ~supers ~methods ~annots typ_name)
          | None -> ())
     | None -> () in
-  DomainSet.iter add_nonnull_to_field fields
+  FieldsAssignedInConstructors.iter add_nonnull_to_field fields
 
 let analysis cfg tenv =
   let initial = FieldsAssignedInConstructors.empty in
diff --git a/infer/src/checkers/SimpleChecker.ml b/infer/src/checkers/SimpleChecker.ml
index 6f4bd00d5..d92ef6dbd 100644
--- a/infer/src/checkers/SimpleChecker.ml
+++ b/infer/src/checkers/SimpleChecker.ml
@@ -46,13 +46,12 @@ module Make (Spec : Spec) : S = struct
   module Domain = struct
     include
       AbstractDomain.FiniteSet
-        (PrettyPrintable.MakePPSet(
-          struct
-            type t = Spec.astate
-            let compare = Spec.compare
-            let pp _ _ = ()
-          end)
-        )
+        (struct
+          type t = Spec.astate
+          let compare = Spec.compare
+          let pp _ _ = ()
+        end)
+
 
     let widen ~prev ~next ~num_iters =
       let iters_befor_timeout = 1000 in
diff --git a/infer/src/checkers/SiofDomain.ml b/infer/src/checkers/SiofDomain.ml
index 2d510492f..915a85a2b 100644
--- a/infer/src/checkers/SiofDomain.ml
+++ b/infer/src/checkers/SiofDomain.ml
@@ -9,13 +9,13 @@
 
 open! IStd
 
-module VarNames = PrettyPrintable.MakePPSet(String)
+module VarNames = AbstractDomain.FiniteSet(String)
 
 module BottomSiofTrace = AbstractDomain.BottomLifted(SiofTrace)
 
 include AbstractDomain.Pair
     (BottomSiofTrace)
-    (AbstractDomain.FiniteSet(VarNames))
+    (VarNames)
 
 (** group together procedure-local accesses *)
 let normalize ((trace, initialized) as astate) = match trace with
diff --git a/infer/src/checkers/SiofDomain.mli b/infer/src/checkers/SiofDomain.mli
index bb7f01510..734e5c3ae 100644
--- a/infer/src/checkers/SiofDomain.mli
+++ b/infer/src/checkers/SiofDomain.mli
@@ -7,7 +7,9 @@
  * of patent rights can be found in the PATENTS file in the same directory.
  *)
 
-module VarNames : PrettyPrintable.PPSet with type elt = string
+open! IStd
+
+module VarNames : module type of AbstractDomain.FiniteSet(String)
 
 module BottomSiofTrace : module type of AbstractDomain.BottomLifted(SiofTrace)
 
@@ -28,7 +30,7 @@ module BottomSiofTrace : module type of AbstractDomain.BottomLifted(SiofTrace)
    std::ios_base::Init::Init(). *)
 include module type of AbstractDomain.Pair
     (AbstractDomain.BottomLifted(SiofTrace))
-    (AbstractDomain.FiniteSet(VarNames))
+    (VarNames)
 
 (** group together procedure-local accesses *)
 val normalize : astate -> astate
diff --git a/infer/src/checkers/ThreadSafetyDomain.ml b/infer/src/checkers/ThreadSafetyDomain.ml
index 02c4b66d8..b11d13dcd 100644
--- a/infer/src/checkers/ThreadSafetyDomain.ml
+++ b/infer/src/checkers/ThreadSafetyDomain.ml
@@ -173,16 +173,10 @@ module AccessPrecondition = struct
     | Protected -> F.fprintf fmt "Protected"
     | Unprotected (Some index) -> F.fprintf fmt "Unprotected(%d)" index
     | Unprotected None -> F.fprintf fmt "Unprotected"
-
-  module Map = PrettyPrintable.MakePPMap(struct
-      type nonrec t = t
-      let compare = compare
-      let pp = pp
-    end)
 end
 
 module AccessDomain = struct
-  include AbstractDomain.Map (AccessPrecondition.Map) (PathDomain)
+  include AbstractDomain.Map (AccessPrecondition) (PathDomain)
 
   let add_access precondition access_path t =
     let precondition_accesses =
diff --git a/infer/src/checkers/ThreadSafetyDomain.mli b/infer/src/checkers/ThreadSafetyDomain.mli
index 6b8c90bdb..cc7a86294 100644
--- a/infer/src/checkers/ThreadSafetyDomain.mli
+++ b/infer/src/checkers/ThreadSafetyDomain.mli
@@ -101,14 +101,12 @@ module AccessPrecondition : sig
   val unprotected : t
 
   val pp : F.formatter -> t -> unit
-
-  module Map : PrettyPrintable.PPMap with type key = t
 end
 
 (** map of access precondition |-> set of accesses. the map should hold all accesses to a
     possibly-unowned access path *)
 module AccessDomain : sig
-  include module type of AbstractDomain.Map (AccessPrecondition.Map) (PathDomain)
+  include module type of AbstractDomain.Map (AccessPrecondition) (PathDomain)
 
   (* add the given (access, precondition) pair to the map *)
   val add_access : AccessPrecondition.t -> TraceElem.t -> astate -> astate
diff --git a/infer/src/checkers/addressTaken.ml b/infer/src/checkers/addressTaken.ml
index 751d71735..820da9240 100644
--- a/infer/src/checkers/addressTaken.ml
+++ b/infer/src/checkers/addressTaken.ml
@@ -9,7 +9,10 @@
 
 open! IStd
 
-module Domain = AbstractDomain.FiniteSet(Pvar.Set)
+module Domain = AbstractDomain.FiniteSet(struct
+    include Pvar
+    let pp = pp Pp.text
+  end)
 
 module TransferFunctions (CFG : ProcCfg.S) = struct
   module CFG = CFG
diff --git a/infer/src/checkers/annotationReachability.ml b/infer/src/checkers/annotationReachability.ml
index f2d3502f2..70a65e32d 100644
--- a/infer/src/checkers/annotationReachability.ml
+++ b/infer/src/checkers/annotationReachability.ml
@@ -42,7 +42,7 @@ let src_snk_pairs =
     specs
 
 module Domain = struct
-  module TrackingVar = AbstractDomain.FiniteSet (Var.Set)
+  module TrackingVar = AbstractDomain.FiniteSet (Var)
   module TrackingDomain = AbstractDomain.BottomLifted (TrackingVar)
   include AbstractDomain.Pair (AnnotReachabilityDomain) (TrackingDomain)
 
@@ -159,7 +159,7 @@ let lookup_annotation_calls caller_pdesc annot pname =
   | Some { Specs.payload = { Specs.annot_map = Some annot_map; }; } ->
       begin
         try
-          Annot.Map.find annot annot_map
+          AnnotReachabilityDomain.find annot annot_map
         with Not_found ->
           AnnotReachabilityDomain.SinkMap.empty
       end
@@ -309,7 +309,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
           if AnnotReachabilityDomain.CallSites.is_empty calls
           then astate
           else Domain.add_call_site annot sink call_site astate in
-        Annot.Map.fold
+        AnnotReachabilityDomain.fold
           (fun annot sink_map astate ->
              AnnotReachabilityDomain.SinkMap.fold
                (add_call_site annot)
@@ -389,7 +389,7 @@ module Interprocedural = struct
             (CallSite.make proc_name loc)
             sink_map in
       try
-        let sink_map = Annot.Map.find snk_annot annot_map in
+        let sink_map = AnnotReachabilityDomain.find snk_annot annot_map in
         List.iter ~f:(report_src_snk_path sink_map) src_annot_list
       with Not_found -> () in
 
diff --git a/infer/src/checkers/liveness.ml b/infer/src/checkers/liveness.ml
index fff657eac..c287aca80 100644
--- a/infer/src/checkers/liveness.ml
+++ b/infer/src/checkers/liveness.ml
@@ -14,7 +14,7 @@ module L = Logging
 
 (** backward analysis for computing set of maybe-live variables at each program point *)
 
-module Domain = AbstractDomain.FiniteSet(Var.Set)
+module Domain = AbstractDomain.FiniteSet(Var)
 
 (* compilers 101-style backward transfer functions for liveness analysis. gen a variable when it is
    read, kill the variable when it is assigned *)
diff --git a/infer/src/checkers/var.ml b/infer/src/checkers/var.ml
index 8e1685db1..452350da2 100644
--- a/infer/src/checkers/var.ml
+++ b/infer/src/checkers/var.ml
@@ -28,10 +28,6 @@ let to_exp = function
   | ProgramVar pvar -> Exp.Lvar pvar
   | LogicalVar id -> Exp.Var id
 
-let compare_alpha v1 v2 = match v1, v2 with
-  | ProgramVar pv1, ProgramVar pv2 -> Pvar.compare_alpha pv1 pv2
-  | _ -> compare v1 v2
-
 let pp fmt = function
   | ProgramVar pv -> (Pvar.pp Pp.text) fmt pv
   | LogicalVar id -> (Ident.pp Pp.text) fmt id
@@ -41,10 +37,3 @@ module Map = PrettyPrintable.MakePPMap(struct
     let compare = compare
     let pp = pp
   end)
-
-module Set = PrettyPrintable.MakePPCompareSet(struct
-    type nonrec t = t
-    let compare = compare
-    let compare_pp = compare_alpha
-    let pp = pp
-  end)
diff --git a/infer/src/checkers/var.mli b/infer/src/checkers/var.mli
index b31ab6865..b341e71fc 100644
--- a/infer/src/checkers/var.mli
+++ b/infer/src/checkers/var.mli
@@ -27,5 +27,3 @@ val to_exp : t -> Exp.t
 val pp : Format.formatter -> t -> unit
 
 module Map : PrettyPrintable.PPMap with type key = t
-
-module Set : PrettyPrintable.PPSet with type elt = t
diff --git a/infer/src/unit/accessTreeTests.ml b/infer/src/unit/accessTreeTests.ml
index 2d3430e5c..3bc3ec945 100644
--- a/infer/src/unit/accessTreeTests.ml
+++ b/infer/src/unit/accessTreeTests.ml
@@ -13,7 +13,7 @@ module F = Format
 
 (* string set domain we use to ensure we're getting the expected traces *)
 module MockTraceDomain = struct
-  include AbstractDomain.FiniteSet (PrettyPrintable.MakePPSet (String))
+  include AbstractDomain.FiniteSet (String)
 
   let top_str = "T"
 
diff --git a/infer/src/unit/addressTakenTests.ml b/infer/src/unit/addressTakenTests.ml
index 7dd4119c8..2b25efce7 100644
--- a/infer/src/unit/addressTakenTests.ml
+++ b/infer/src/unit/addressTakenTests.ml
@@ -93,7 +93,7 @@ let tests =
             );
       invariant "{ &b, &d }";
       var_assign_addrof_var ~rhs_typ:int_ptr_typ "e" "f";
-      invariant "{ &b, &d, &f }"
+      invariant "{ &b, &f, &d }"
     ];
   ] |> TestInterpreter.create_tests ProcData.empty_extras ~initial:AddressTaken.Domain.empty in
   "address_taken_suite">:::test_list
diff --git a/infer/src/unit/livenessTests.ml b/infer/src/unit/livenessTests.ml
index 959f4f98d..7512c294a 100644
--- a/infer/src/unit/livenessTests.ml
+++ b/infer/src/unit/livenessTests.ml
@@ -42,7 +42,7 @@ let tests =
     ];
     "iterative_live",
     [
-      invariant "{ &b, &d, &f }";
+      invariant "{ &b, &f, &d }";
       id_assign_var "e" "f";
       invariant "{ &b, &d }";
       id_assign_var "c" "d";
@@ -91,7 +91,7 @@ let tests =
     ];
     "call_params_live",
     [
-      invariant "{ &a, &b, &c }";
+      invariant "{ &b, &a, &c }";
       call_unknown_no_ret ["a"; "b"; "c";]
     ];
     "dead_after_call_with_retval",