diff --git a/sledge/src/domain_sh.ml b/sledge/src/domain_sh.ml
index 0cf0574c4..9199a2457 100644
--- a/sledge/src/domain_sh.ml
+++ b/sledge/src/domain_sh.ml
@@ -7,7 +7,7 @@
 
 (** Abstract domain *)
 
-open Ses
+open Fol
 
 type t = Sh.t [@@deriving equal, sexp]
 
diff --git a/sledge/src/exec.ml b/sledge/src/exec.ml
index 3c87e65ce..f98a95bd0 100644
--- a/sledge/src/exec.ml
+++ b/sledge/src/exec.ml
@@ -7,7 +7,7 @@
 
 (** Symbolic Execution *)
 
-open Ses
+open Fol
 
 [@@@warning "+9"]
 
diff --git a/sledge/src/exec.mli b/sledge/src/exec.mli
index 5f70d5514..4fef881c4 100644
--- a/sledge/src/exec.mli
+++ b/sledge/src/exec.mli
@@ -7,7 +7,7 @@
 
 (** Symbolic Execution *)
 
-open Ses
+open Fol
 
 val assume : Sh.t -> Term.t -> Sh.t option
 val kill : Sh.t -> Var.t -> Sh.t
diff --git a/sledge/src/fol.ml b/sledge/src/fol.ml
new file mode 100644
index 000000000..815af7adf
--- /dev/null
+++ b/sledge/src/fol.ml
@@ -0,0 +1,10 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+module Var = Ses.Var
+module Term = Ses.Term
+module Equality = Ses.Equality
diff --git a/sledge/src/fol.mli b/sledge/src/fol.mli
new file mode 100644
index 000000000..815af7adf
--- /dev/null
+++ b/sledge/src/fol.mli
@@ -0,0 +1,10 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+module Var = Ses.Var
+module Term = Ses.Term
+module Equality = Ses.Equality
diff --git a/sledge/src/sh.ml b/sledge/src/sh.ml
index 376dd244f..9db819adf 100644
--- a/sledge/src/sh.ml
+++ b/sledge/src/sh.ml
@@ -7,7 +7,7 @@
 
 (** Symbolic Heap Formulas *)
 
-open Ses
+open Fol
 
 [@@@warning "+9"]
 
diff --git a/sledge/src/sh.mli b/sledge/src/sh.mli
index 50d8fd946..8595ec8d0 100644
--- a/sledge/src/sh.mli
+++ b/sledge/src/sh.mli
@@ -7,7 +7,7 @@
 
 (** Symbolic Heap Formulas *)
 
-open Ses
+open Fol
 
 (** Segment of memory starting at [loc] containing [seq] (a byte-array) of
     size [siz], contained in an enclosing allocation-block starting at [bas]
diff --git a/sledge/src/sh_test.ml b/sledge/src/sh_test.ml
index a13068de9..8e4185e17 100644
--- a/sledge/src/sh_test.ml
+++ b/sledge/src/sh_test.ml
@@ -5,7 +5,7 @@
  * LICENSE file in the root directory of this source tree.
  *)
 
-open Ses
+open Fol
 
 let%test_module _ =
   ( module struct
diff --git a/sledge/src/solver.ml b/sledge/src/solver.ml
index f12a70735..fd7fb2ba9 100644
--- a/sledge/src/solver.ml
+++ b/sledge/src/solver.ml
@@ -7,7 +7,7 @@
 
 (** Frame Inference Solver over Symbolic Heaps *)
 
-open Ses
+open Fol
 
 module Goal : sig
   (** Excision judgment
diff --git a/sledge/src/solver.mli b/sledge/src/solver.mli
index c4e1600de..ae6ae86ca 100644
--- a/sledge/src/solver.mli
+++ b/sledge/src/solver.mli
@@ -7,7 +7,7 @@
 
 (** Frame Inference Solver over Symbolic Heaps *)
 
-open Ses
+open Fol
 
 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
diff --git a/sledge/src/solver_test.ml b/sledge/src/solver_test.ml
index 85306c4fd..db520f393 100644
--- a/sledge/src/solver_test.ml
+++ b/sledge/src/solver_test.ml
@@ -5,7 +5,7 @@
  * LICENSE file in the root directory of this source tree.
  *)
 
-open Ses
+open Fol
 
 let%test_module _ =
   ( module struct