diff --git a/sledge/bin/dune b/sledge/bin/dune
index a4c8ed933..993508f6d 100644
--- a/sledge/bin/dune
+++ b/sledge/bin/dune
@@ -6,8 +6,8 @@
 (executable
  (public_name sledge)
  (package sledge)
- (libraries apron apron.boxMPQ core ctypes ctypes.foreign dune-build-info
-   llvm llvm.irreader llvm.analysis llvm.scalar_opts llvm.target llvm.ipo
+ (libraries apron apron.boxMPQ ctypes ctypes.foreign dune-build-info llvm
+   llvm.irreader llvm.analysis llvm.scalar_opts llvm.target llvm.ipo
    llvm.linker shexp.process yojson trace import sledgelib model)
  (flags
   (:standard -open Import -open Sledgelib -open Model))
diff --git a/sledge/lib/exp.ml b/sledge/lib/exp.ml
index 87aebff8d..f6777df92 100644
--- a/sledge/lib/exp.ml
+++ b/sledge/lib/exp.ml
@@ -79,13 +79,7 @@ module T = struct
 end
 
 include T
-
-module Set = struct
-  include Set.Make (T)
-
-  let t_of_sexp = t_of_sexp T.t_of_sexp
-end
-
+module Set = struct include Set.Make (T) include Provide_of_sexp (T) end
 module Map = Map.Make (T)
 
 let term e = e.term
diff --git a/sledge/lib/import/dune b/sledge/lib/import/dune
index a57711243..00ec926ad 100644
--- a/sledge/lib/import/dune
+++ b/sledge/lib/import/dune
@@ -6,7 +6,7 @@
 (library
  (name import)
  (public_name sledge.import)
- (libraries core_kernel.fheap zarith trace)
+ (libraries core core_kernel.fheap zarith trace)
  (flags (:standard))
  (preprocess
   (pps ppx_sledge))
diff --git a/sledge/lib/import/set.ml b/sledge/lib/import/set.ml
index 32f168a0e..1f95fa93e 100644
--- a/sledge/lib/import/set.ml
+++ b/sledge/lib/import/set.ml
@@ -5,48 +5,40 @@
  * LICENSE file in the root directory of this source tree.
  *)
 
-open Import0
 include Set_intf
 
-module Make (Elt : OrderedType) : S with type elt = Elt.t = struct
-  module S = Caml.Set.Make (Elt)
+module Make (Elt : sig
+  type t [@@deriving compare, sexp_of]
+end) : S with type elt = Elt.t = struct
+  module EltSet = Core.Set.Make_plain (Elt)
+  module Elt = EltSet.Elt
 
   type elt = Elt.t
-  type t = S.t
 
-  let compare = S.compare
-  let equal = S.equal
-  let sexp_of_t s = List.sexp_of_t Elt.sexp_of_t (S.elements s)
+  include EltSet.Tree
 
-  let t_of_sexp elt_of_sexp sexp =
-    S.of_list (List.t_of_sexp elt_of_sexp sexp)
-
-  let pp pp_elt fs x = List.pp ",@ " pp_elt fs (S.elements x)
+  let pp pp_elt fs x = List.pp ",@ " pp_elt fs (elements x)
 
   let pp_diff pp_elt fs (xs, ys) =
-    let lose = S.diff xs ys and gain = S.diff ys xs in
-    if not (S.is_empty lose) then Format.fprintf fs "-- %a" (pp pp_elt) lose ;
-    if not (S.is_empty gain) then Format.fprintf fs "++ %a" (pp pp_elt) gain
-
-  let empty = S.empty
-  let of_ x = S.add x empty
-  let of_option = Option.fold ~f:(fun x y -> S.add y x) ~init:empty
-  let of_list = S.of_list
-  let of_vector x = S.of_list (IArray.to_list x)
-  let add s e = S.add e s
-  let add_option yo x = Option.fold ~f:(fun x y -> S.add y x) ~init:x yo
-  let add_list ys x = List.fold ~f:(fun x y -> S.add y x) ~init:x ys
-  let remove s e = S.remove e s
-  let filter s ~f = S.filter f s
-  let union = S.union
-  let union_list ss = List.fold ss ~init:empty ~f:union
-  let diff = S.diff
-  let inter = S.inter
-  let diff_inter x y = (S.diff x y, S.inter x y)
-  let is_empty = S.is_empty
-  let mem s e = S.mem e s
-  let is_subset x ~of_ = S.subset x of_
-  let disjoint = S.disjoint
-  let max_elt = S.max_elt_opt
-  let fold s ~init:z ~f = S.fold (fun z x -> f x z) s z
+    let lose = diff xs ys and gain = diff ys xs in
+    if not (is_empty lose) then Format.fprintf fs "-- %a" (pp pp_elt) lose ;
+    if not (is_empty gain) then Format.fprintf fs "++ %a" (pp pp_elt) gain
+
+  let of_ x = add empty x
+  let of_option = Option.fold ~f:add ~init:empty
+  let of_iarray a = of_array (IArray.to_array a)
+  let add_option xo s = Option.fold ~f:add ~init:s xo
+  let add_list xs s = List.fold ~f:add ~init:s xs
+  let diff_inter s t = (diff s t, inter s t)
+
+  let rec disjoint s1 s2 =
+    match choose s1 with
+    | None -> true
+    | _ when is_empty s2 -> true
+    | _ when s1 == s2 -> false
+    | Some x -> (
+        let l1, _, r1 = split s1 x in
+        match split s2 x with
+        | _, Some _, _ -> false
+        | l2, None, r2 -> disjoint l1 l2 && disjoint r1 r2 )
 end
diff --git a/sledge/lib/import/set.mli b/sledge/lib/import/set.mli
index 4ef862c8d..20fed6478 100644
--- a/sledge/lib/import/set.mli
+++ b/sledge/lib/import/set.mli
@@ -5,6 +5,8 @@
  * LICENSE file in the root directory of this source tree.
  *)
 
-open Import0
 include module type of Set_intf
-module Make (Elt : OrderedType) : S with type elt = Elt.t
+
+module Make (Elt : sig
+  type t [@@deriving compare, sexp_of]
+end) : S with type elt = Elt.t
diff --git a/sledge/lib/import/set_intf.ml b/sledge/lib/import/set_intf.ml
index 29b98cb6a..8db56475b 100644
--- a/sledge/lib/import/set_intf.ml
+++ b/sledge/lib/import/set_intf.ml
@@ -9,41 +9,22 @@ open Import0
 
 module type S = sig
   type elt
-  type t
 
-  val compare : t -> t -> int
-  val equal : t -> t -> bool
-  val sexp_of_t : t -> Sexp.t
-  val t_of_sexp : (Sexp.t -> elt) -> Sexp.t -> t
+  module Elt : sig
+    type t = elt
+
+    include Core.Comparator.S with type t := t
+  end
+
+  include Core_kernel.Set_intf.Make_S_plain_tree(Elt).S
+
   val pp : elt pp -> t pp
   val pp_diff : elt pp -> (t * t) pp
-
-  (* initial constructors *)
-  val empty : t
   val of_ : elt -> t
   val of_option : elt option -> t
-  val of_list : elt list -> t
-  val of_vector : elt IArray.t -> t
-
-  (* constructors *)
-  val add : t -> elt -> t
+  val of_iarray : elt IArray.t -> t
   val add_option : elt option -> t -> t
   val add_list : elt list -> t -> t
-  val remove : t -> elt -> t
-  val filter : t -> f:(elt -> bool) -> t
-  val union : t -> t -> t
-  val union_list : t list -> t
-  val diff : t -> t -> t
-  val inter : t -> t -> t
   val diff_inter : t -> t -> t * t
-
-  (* queries *)
-  val is_empty : t -> bool
-  val mem : t -> elt -> bool
-  val is_subset : t -> of_:t -> bool
   val disjoint : t -> t -> bool
-  val max_elt : t -> elt option
-
-  (* traversals *)
-  val fold : t -> init:'s -> f:('s -> elt -> 's) -> 's
 end
diff --git a/sledge/lib/term.ml b/sledge/lib/term.ml
index db243c756..77b639ba6 100644
--- a/sledge/lib/term.ml
+++ b/sledge/lib/term.ml
@@ -101,12 +101,7 @@ end
 
 include T
 module Map = Map.Make (T)
-
-module Set = struct
-  include Set.Make (T)
-
-  let t_of_sexp = t_of_sexp T.t_of_sexp
-end
+module Set = struct include Set.Make (T) include Provide_of_sexp (T) end
 
 let fix (f : (t -> 'a as 'f) -> 'f) (bot : 'f) (e : t) : 'a =
   let rec fix_f seen e =