diff --git a/infer/src/pulse/PulseDummySledge.ml b/infer/src/pulse/PulseDummySledge.ml
index 170924242..2fc206181 100644
--- a/infer/src/pulse/PulseDummySledge.ml
+++ b/infer/src/pulse/PulseDummySledge.ml
@@ -37,14 +37,14 @@ module Term = struct
 end
 
 (* same type as {!PulsePathCondition.t} to be nice to summary serialization *)
-type t = {eqs: Sledge.Equality.t lazy_t; non_eqs: Sledge.Term.t lazy_t}
+type t = {eqs: Ses.Equality.t lazy_t; non_eqs: Ses.Term.t lazy_t}
 
 (* still print to make sure the formula never changes in debug *)
 let pp fmt {eqs= (lazy eqs); non_eqs= (lazy non_eqs)} =
-  F.fprintf fmt "%a∧%a" Sledge.Equality.pp eqs Sledge.Term.pp non_eqs
+  F.fprintf fmt "%a∧%a" Ses.Equality.pp eqs Ses.Term.pp non_eqs
 
 
-let true_ = {eqs= Lazy.from_val Sledge.Equality.true_; non_eqs= Lazy.from_val Sledge.Term.true_}
+let true_ = {eqs= Lazy.from_val Ses.Equality.true_; non_eqs= Lazy.from_val Ses.Term.true_}
 
 let and_eq () () phi = phi
 
diff --git a/infer/src/pulse/PulseSledge.ml b/infer/src/pulse/PulseSledge.ml
index b85fc3767..009713277 100644
--- a/infer/src/pulse/PulseSledge.ml
+++ b/infer/src/pulse/PulseSledge.ml
@@ -13,7 +13,7 @@ module AbstractValue = PulseAbstractValue
 [@@@warning "+9"]
 
 module Var = struct
-  module Var = Sledge.Var
+  module Var = Ses.Var
 
   let of_absval (v : AbstractValue.t) = Var.identified ~name:"v" ~id:(v :> int)
 
@@ -26,7 +26,7 @@ module Var = struct
 end
 
 module Term = struct
-  module Term = Sledge.Term
+  module Term = Ses.Term
 
   let of_intlit i = Term.integer (IntLit.to_big_int i)
 
@@ -75,7 +75,7 @@ module Term = struct
 end
 
 module Equality = struct
-  include Sledge.Equality
+  include Ses.Equality
 
   let assert_no_new_vars api new_vars =
     if not (Var.Set.is_empty new_vars) then
@@ -83,25 +83,25 @@ module Equality = struct
 
 
   let and_eq t1 t2 r =
-    let new_vars, r' = Sledge.Equality.and_eq Var.Set.empty t1 t2 r in
+    let new_vars, r' = Ses.Equality.and_eq Var.Set.empty t1 t2 r in
     assert_no_new_vars "Equality.and_eq" new_vars ;
     r'
 
 
   let and_term t r =
-    let new_vars, r' = Sledge.Equality.and_term Var.Set.empty t r in
+    let new_vars, r' = Ses.Equality.and_term Var.Set.empty t r in
     assert_no_new_vars "Equality.and_term" new_vars ;
     r'
 
 
   let and_ r1 r2 =
-    let new_vars, r' = Sledge.Equality.and_ Var.Set.empty r1 r2 in
+    let new_vars, r' = Ses.Equality.and_ Var.Set.empty r1 r2 in
     assert_no_new_vars "Equality.and_" new_vars ;
     r'
 
 
   let apply_subst subst r =
-    let new_vars, r' = Sledge.Equality.apply_subst Var.Set.empty subst r in
+    let new_vars, r' = Ses.Equality.apply_subst Var.Set.empty subst r in
     assert_no_new_vars "Equality.apply_subst" new_vars ;
     r'
 end
diff --git a/sledge/bin/domain_itv.ml b/sledge/bin/domain_itv.ml
index ecf033500..f1c25a11d 100644
--- a/sledge/bin/domain_itv.ml
+++ b/sledge/bin/domain_itv.ml
@@ -7,6 +7,7 @@
 
 (** Interval abstract domain *)
 
+open Ses
 open Apron
 
 let equal_apron_typ =
diff --git a/sledge/dune b/sledge/dune
index d8dbae304..fb9e835b3 100644
--- a/sledge/dune
+++ b/sledge/dune
@@ -45,12 +45,24 @@
    (pps ppx_sledge ppx_trace))
   (inline_tests)))
 
+(subdir
+ src/ses
+ (library
+  (name ses)
+  (public_name sledge.ses)
+  (libraries nonstdlib llair)
+  (flags
+   (:standard -open NS))
+  (preprocess
+   (pps ppx_sledge ppx_trace))
+  (inline_tests)))
+
 (subdir
  src
  (library
   (name sledge)
   (public_name sledge)
-  (libraries nonstdlib llair)
+  (libraries nonstdlib llair ses)
   (flags
    (:standard -open NS))
   (preprocess
diff --git a/sledge/src/domain_sh.ml b/sledge/src/domain_sh.ml
index 0f1182c1e..0cf0574c4 100644
--- a/sledge/src/domain_sh.ml
+++ b/sledge/src/domain_sh.ml
@@ -7,6 +7,8 @@
 
 (** Abstract domain *)
 
+open Ses
+
 type t = Sh.t [@@deriving equal, sexp]
 
 let pp fs q = Format.fprintf fs "@[{ %a@ }@]" Sh.pp q
diff --git a/sledge/src/exec.ml b/sledge/src/exec.ml
index 70b44d323..3c87e65ce 100644
--- a/sledge/src/exec.ml
+++ b/sledge/src/exec.ml
@@ -7,6 +7,8 @@
 
 (** Symbolic Execution *)
 
+open Ses
+
 [@@@warning "+9"]
 
 module Fresh : sig
diff --git a/sledge/src/exec.mli b/sledge/src/exec.mli
index 68d2e3af0..5f70d5514 100644
--- a/sledge/src/exec.mli
+++ b/sledge/src/exec.mli
@@ -7,6 +7,8 @@
 
 (** Symbolic Execution *)
 
+open Ses
+
 val assume : Sh.t -> Term.t -> Sh.t option
 val kill : Sh.t -> Var.t -> Sh.t
 val move : Sh.t -> (Var.t * Term.t) iarray -> Sh.t
diff --git a/sledge/src/equality.ml b/sledge/src/ses/equality.ml
similarity index 100%
rename from sledge/src/equality.ml
rename to sledge/src/ses/equality.ml
diff --git a/sledge/src/equality.mli b/sledge/src/ses/equality.mli
similarity index 100%
rename from sledge/src/equality.mli
rename to sledge/src/ses/equality.mli
diff --git a/sledge/src/equality_test.ml b/sledge/src/ses/equality_test.ml
similarity index 100%
rename from sledge/src/equality_test.ml
rename to sledge/src/ses/equality_test.ml
diff --git a/sledge/src/equality_test.mli b/sledge/src/ses/equality_test.mli
similarity index 100%
rename from sledge/src/equality_test.mli
rename to sledge/src/ses/equality_test.mli
diff --git a/sledge/src/term.ml b/sledge/src/ses/term.ml
similarity index 100%
rename from sledge/src/term.ml
rename to sledge/src/ses/term.ml
diff --git a/sledge/src/term.mli b/sledge/src/ses/term.mli
similarity index 100%
rename from sledge/src/term.mli
rename to sledge/src/ses/term.mli
diff --git a/sledge/src/term_test.ml b/sledge/src/ses/term_test.ml
similarity index 100%
rename from sledge/src/term_test.ml
rename to sledge/src/ses/term_test.ml
diff --git a/sledge/src/term_test.mli b/sledge/src/ses/term_test.mli
similarity index 100%
rename from sledge/src/term_test.mli
rename to sledge/src/ses/term_test.mli
diff --git a/sledge/src/var.ml b/sledge/src/ses/var.ml
similarity index 100%
rename from sledge/src/var.ml
rename to sledge/src/ses/var.ml
diff --git a/sledge/src/var.mli b/sledge/src/ses/var.mli
similarity index 100%
rename from sledge/src/var.mli
rename to sledge/src/ses/var.mli
diff --git a/sledge/src/sh.ml b/sledge/src/sh.ml
index 5cd920669..376dd244f 100644
--- a/sledge/src/sh.ml
+++ b/sledge/src/sh.ml
@@ -7,6 +7,8 @@
 
 (** Symbolic Heap Formulas *)
 
+open Ses
+
 [@@@warning "+9"]
 
 type seg = {loc: Term.t; bas: Term.t; len: Term.t; siz: Term.t; seq: Term.t}
diff --git a/sledge/src/sh.mli b/sledge/src/sh.mli
index 376f7b1da..50d8fd946 100644
--- a/sledge/src/sh.mli
+++ b/sledge/src/sh.mli
@@ -7,6 +7,8 @@
 
 (** Symbolic Heap Formulas *)
 
+open Ses
+
 (** Segment of memory starting at [loc] containing [seq] (a byte-array) of
     size [siz], contained in an enclosing allocation-block starting at [bas]
     of length [len]. *)
diff --git a/sledge/src/sh_test.ml b/sledge/src/sh_test.ml
index 06908aaf2..a13068de9 100644
--- a/sledge/src/sh_test.ml
+++ b/sledge/src/sh_test.ml
@@ -5,6 +5,8 @@
  * LICENSE file in the root directory of this source tree.
  *)
 
+open Ses
+
 let%test_module _ =
   ( module struct
     open Sh
diff --git a/sledge/src/solver.ml b/sledge/src/solver.ml
index b39b1af14..f12a70735 100644
--- a/sledge/src/solver.ml
+++ b/sledge/src/solver.ml
@@ -7,6 +7,8 @@
 
 (** Frame Inference Solver over Symbolic Heaps *)
 
+open Ses
+
 module Goal : sig
   (** Excision judgment
 
diff --git a/sledge/src/solver.mli b/sledge/src/solver.mli
index 3a84142aa..c4e1600de 100644
--- a/sledge/src/solver.mli
+++ b/sledge/src/solver.mli
@@ -7,6 +7,8 @@
 
 (** Frame Inference Solver over Symbolic Heaps *)
 
+open Ses
+
 val infer_frame : Sh.t -> Var.Set.t -> Sh.t -> Sh.t option
 (** If [infer_frame p xs q] is [Some r], then [p ⊢ ∃xs. q * r]. The
     vocabulary of [r] is the vocabulary of [q] union [xs]. A goal is for [r]
diff --git a/sledge/src/solver_test.ml b/sledge/src/solver_test.ml
index 014b71cd9..85306c4fd 100644
--- a/sledge/src/solver_test.ml
+++ b/sledge/src/solver_test.ml
@@ -5,6 +5,8 @@
  * LICENSE file in the root directory of this source tree.
  *)
 
+open Ses
+
 let%test_module _ =
   ( module struct
     let () =