diff --git a/sledge/src/domain_sh.ml b/sledge/src/domain_sh.ml
index 3ce029f3f..171dd9e64 100644
--- a/sledge/src/domain_sh.ml
+++ b/sledge/src/domain_sh.ml
@@ -7,6 +7,7 @@
 
 (** Abstract domain *)
 
+module X = Llair_to_Fol
 open Fol
 
 type t = Sh.t [@@deriving equal, sexp]
@@ -21,9 +22,9 @@ let simplify q = if !simplify_states then Sh.simplify q else q
 let init globals =
   IArray.fold globals ~init:Sh.emp ~f:(fun q -> function
     | {Llair.Global.reg; init= Some (seq, siz)} ->
-        let loc = Term.var (Var_of_Llair.reg reg) in
+        let loc = Term.var (X.reg reg) in
         let len = Term.integer (Z.of_int siz) in
-        let seq = Term_of_Llair.exp seq in
+        let seq = X.term seq in
         Sh.star q (Sh.seg {loc; bas= loc; len; siz= len; seq})
     | _ -> q )
 
@@ -36,16 +37,11 @@ let join p q =
 
 let is_false = Sh.is_false
 let dnf = Sh.dnf
-
-let exec_assume q b =
-  Exec.assume q (Formula_of_Llair.exp b) |> Option.map ~f:simplify
-
-let exec_kill q r = Exec.kill q (Var_of_Llair.reg r) |> simplify
+let exec_assume q b = Exec.assume q (X.formula b) |> Option.map ~f:simplify
+let exec_kill q r = Exec.kill q (X.reg r) |> simplify
 
 let exec_move q res =
-  Exec.move q
-    (IArray.map res ~f:(fun (r, e) ->
-         (Var_of_Llair.reg r, Term_of_Llair.exp e) ))
+  Exec.move q (IArray.map res ~f:(fun (r, e) -> (X.reg r, X.term e)))
   |> simplify
 
 let exec_inst pre inst =
@@ -53,37 +49,27 @@ let exec_inst pre inst =
   | Move {reg_exps; _} ->
       Some
         (Exec.move pre
-           (IArray.map reg_exps ~f:(fun (r, e) ->
-                (Var_of_Llair.reg r, Term_of_Llair.exp e) )))
+           (IArray.map reg_exps ~f:(fun (r, e) -> (X.reg r, X.term e))))
   | Load {reg; ptr; len; _} ->
-      Exec.load pre ~reg:(Var_of_Llair.reg reg) ~ptr:(Term_of_Llair.exp ptr)
-        ~len:(Term_of_Llair.exp len)
+      Exec.load pre ~reg:(X.reg reg) ~ptr:(X.term ptr) ~len:(X.term len)
   | Store {ptr; exp; len; _} ->
-      Exec.store pre ~ptr:(Term_of_Llair.exp ptr)
-        ~exp:(Term_of_Llair.exp exp) ~len:(Term_of_Llair.exp len)
+      Exec.store pre ~ptr:(X.term ptr) ~exp:(X.term exp) ~len:(X.term len)
   | Memset {dst; byt; len; _} ->
-      Exec.memset pre ~dst:(Term_of_Llair.exp dst)
-        ~byt:(Term_of_Llair.exp byt) ~len:(Term_of_Llair.exp len)
+      Exec.memset pre ~dst:(X.term dst) ~byt:(X.term byt) ~len:(X.term len)
   | Memcpy {dst; src; len; _} ->
-      Exec.memcpy pre ~dst:(Term_of_Llair.exp dst)
-        ~src:(Term_of_Llair.exp src) ~len:(Term_of_Llair.exp len)
+      Exec.memcpy pre ~dst:(X.term dst) ~src:(X.term src) ~len:(X.term len)
   | Memmov {dst; src; len; _} ->
-      Exec.memmov pre ~dst:(Term_of_Llair.exp dst)
-        ~src:(Term_of_Llair.exp src) ~len:(Term_of_Llair.exp len)
+      Exec.memmov pre ~dst:(X.term dst) ~src:(X.term src) ~len:(X.term len)
   | Alloc {reg; num; len; _} ->
-      Exec.alloc pre ~reg:(Var_of_Llair.reg reg)
-        ~num:(Term_of_Llair.exp num) ~len
-  | Free {ptr; _} -> Exec.free pre ~ptr:(Term_of_Llair.exp ptr)
-  | Nondet {reg; _} ->
-      Some (Exec.nondet pre (Option.map ~f:Var_of_Llair.reg reg))
+      Exec.alloc pre ~reg:(X.reg reg) ~num:(X.term num) ~len
+  | Free {ptr; _} -> Exec.free pre ~ptr:(X.term ptr)
+  | Nondet {reg; _} -> Some (Exec.nondet pre (Option.map ~f:X.reg reg))
   | Abort _ -> Exec.abort pre )
   |> Option.map ~f:simplify
 
 let exec_intrinsic ~skip_throw q r i es =
-  Exec.intrinsic ~skip_throw q
-    (Option.map ~f:Var_of_Llair.reg r)
-    (Var_of_Llair.reg i)
-    (List.map ~f:Term_of_Llair.exp es)
+  Exec.intrinsic ~skip_throw q (Option.map ~f:X.reg r) (X.reg i)
+    (List.map ~f:X.term es)
   |> Option.map ~f:(Option.map ~f:simplify)
 
 let term_eq_class_has_only_vars_in fvs ctx term =
@@ -132,12 +118,9 @@ let and_eqs sub formals actuals q =
 let localize_entry globals actuals formals freturn locals shadow pre entry =
   (* Add the formals here to do garbage collection and then get rid of them *)
   let formals_set = Var.Set.of_list formals in
-  let freturn_locals =
-    Var_of_Llair.regs (Llair.Reg.Set.add_option freturn locals)
-  in
+  let freturn_locals = X.regs (Llair.Reg.Set.add_option freturn locals) in
   let function_summary_pre =
-    garbage_collect entry
-      ~wrt:(Var.Set.union formals_set (Var_of_Llair.regs globals))
+    garbage_collect entry ~wrt:(Var.Set.union formals_set (X.regs globals))
   in
   [%Trace.info "function summary pre %a" pp function_summary_pre] ;
   let foot = Sh.exists formals_set function_summary_pre in
@@ -169,12 +152,10 @@ let call ~summaries ~globals ~actuals ~areturn ~formals ~freturn ~locals q =
       (List.rev formals) Llair.Reg.Set.pp locals Llair.Reg.Set.pp globals pp
       q]
   ;
-  let actuals = List.map ~f:Term_of_Llair.exp actuals in
-  let areturn = Option.map ~f:Var_of_Llair.reg areturn in
-  let formals = List.map ~f:Var_of_Llair.reg formals in
-  let freturn_locals =
-    Var_of_Llair.regs (Llair.Reg.Set.add_option freturn locals)
-  in
+  let actuals = List.map ~f:X.term actuals in
+  let areturn = Option.map ~f:X.reg areturn in
+  let formals = List.map ~f:X.reg formals in
+  let freturn_locals = X.regs (Llair.Reg.Set.add_option freturn locals) in
   let modifs = Var.Set.of_option areturn in
   (* quantify modifs, their current value will be overwritten and so does
      not need to be saved in the freshening renaming *)
@@ -210,7 +191,7 @@ let post locals _ q =
   [%Trace.call fun {pf} ->
     pf "@[<hv>locals: {@[%a@]}@ q: %a@]" Llair.Reg.Set.pp locals Sh.pp q]
   ;
-  Sh.exists (Var_of_Llair.regs locals) q |> simplify
+  Sh.exists (X.regs locals) q |> simplify
   |>
   [%Trace.retn fun {pf} -> pf "%a" Sh.pp]
 
@@ -227,8 +208,8 @@ let retn formals freturn {areturn; unshadow; frame} q =
       (Option.pp "@ areturn: %a" Var.pp)
       areturn Var.Subst.pp unshadow pp q pp frame]
   ;
-  let formals = List.map ~f:Var_of_Llair.reg formals in
-  let freturn = Option.map ~f:Var_of_Llair.reg freturn in
+  let formals = List.map ~f:X.reg formals in
+  let freturn = Option.map ~f:X.reg freturn in
   let q, shadows =
     match areturn with
     | Some areturn -> (
@@ -272,8 +253,8 @@ let create_summary ~locals ~formals ~entry ~current:(post : Sh.t) =
     pf "formals %a@ entry: %a@ current: %a" Llair.Reg.Set.pp formals pp
       entry pp post]
   ;
-  let locals = Var_of_Llair.regs locals in
-  let formals = Var_of_Llair.regs formals in
+  let locals = X.regs locals in
+  let formals = X.regs formals in
   let foot = Sh.exists locals entry in
   let foot, subst = Sh.freshen ~wrt:(Var.Set.union foot.us post.us) foot in
   let restore_formals q =
diff --git a/sledge/src/fol.ml b/sledge/src/fol.ml
index 6f96285d5..861079662 100644
--- a/sledge/src/fol.ml
+++ b/sledge/src/fol.ml
@@ -401,7 +401,6 @@ module Var : sig
   include Ses.Var_intf.VAR with type t = private trm
 
   val of_ : trm -> t
-  val of_exp : exp -> t option
 end = struct
   module T = struct
     type t = trm [@@deriving compare, equal, sexp]
@@ -422,10 +421,6 @@ end = struct
   end)
 
   let of_ v = v |> check invariant
-
-  let of_exp = function
-    | `Trm (Var _ as v) -> Some (v |> check invariant)
-    | _ -> None
 end
 
 type var = Var.t
@@ -1147,11 +1142,8 @@ let vs_of_ses : Ses.Var.Set.t -> Var.Set.t =
   Ses.Var.Set.fold vs ~init:Var.Set.empty ~f:(fun vs v ->
       Var.Set.add vs (v_of_ses v) )
 
-let uap0 f = `Trm (Apply (f, [||]))
 let uap1 f = ap1t (fun x -> Apply (f, [|x|]))
 let uap2 f = ap2t (fun x y -> Apply (f, [|x; y|]))
-let upos2 p = ap2f (fun x y -> _UPosLit p [|x; y|])
-let uneg2 p = ap2f (fun x y -> _UNegLit p [|x; y|])
 let uposN p = apNf (_UPosLit p)
 let unegN p = apNf (_UNegLit p)
 
@@ -1517,133 +1509,3 @@ module Context = struct
   let elim ks r =
     wrap elim_tmr (fun () -> elim ks r) (fun () -> Elim (ks, r))
 end
-
-(*
- * Convert from Llair
- *)
-
-module Term_of_Llair = struct
-  let rec uap_te f a = uap1 f (exp a)
-  and uap_tte f a b = uap2 f (exp a) (exp b)
-
-  and usap_ttt : 'a. (exp -> exp -> 'a) -> _ -> _ -> _ -> 'a =
-   fun f typ a b ->
-    let bits = Llair.Typ.bit_size_of typ in
-    f (uap1 (Unsigned bits) (exp a)) (uap1 (Unsigned bits) (exp b))
-
-  and usap_ttf (f : exp -> exp -> fml) typ a b = `Fml (usap_ttt f typ a b)
-  and ap_ttt : 'a. (exp -> exp -> 'a) -> _ -> _ -> 'a =
-   fun f a b -> f (exp a) (exp b)
-  and ap_ttf (f : exp -> exp -> fml) a b = `Fml (ap_ttt f a b)
-
-  and ap_fff (f : fml -> fml -> fml) a b =
-    `Fml (f (embed_into_fml (exp a)) (embed_into_fml (exp b)))
-
-  and ap_ffff (f : fml -> fml -> fml -> fml) a b c =
-    `Fml
-      (f
-         (embed_into_fml (exp a))
-         (embed_into_fml (exp b))
-         (embed_into_fml (exp c)))
-
-  and exp : Llair.Exp.t -> exp =
-   fun e ->
-    let open Term in
-    let open Formula in
-    match e with
-    | Reg {name; global; typ= _} -> var (Var.program ~name ~global)
-    | Label {parent; name} ->
-        uap0 (Uninterp ("label_" ^ parent ^ "_" ^ name))
-    | Integer {typ= _; data} -> integer data
-    | Float {data; typ= _} -> (
-      match Q.of_float (Float.of_string data) with
-      | q when Q.is_real q -> rational q
-      | _ | (exception Invalid_argument _) ->
-          uap0 (Uninterp ("float_" ^ data)) )
-    | Ap1 (Signed {bits}, _, e) ->
-        let a = exp e in
-        if bits = 1 then
-          match Formula.project a with
-          | Some fml -> Formula.inject fml
-          | _ -> uap1 (Signed bits) a
-        else uap1 (Signed bits) a
-    | Ap1 (Unsigned {bits}, _, e) ->
-        let a = exp e in
-        if bits = 1 then
-          match Formula.project a with
-          | Some fml -> Formula.inject fml
-          | _ -> uap1 (Unsigned bits) a
-        else uap1 (Unsigned bits) a
-    | Ap1 (Convert {src}, dst, e) ->
-        let s =
-          Format.asprintf "convert_%a_%a" Llair.Typ.pp src Llair.Typ.pp dst
-        in
-        uap_te (Uninterp s) e
-    | Ap2 (Eq, Integer {bits= 1; _}, p, q) -> ap_fff iff p q
-    | Ap2 (Dq, Integer {bits= 1; _}, p, q) -> ap_fff xor p q
-    | Ap2 ((Gt | Ugt), Integer {bits= 1; _}, p, q)
-     |Ap2 ((Lt | Ult), Integer {bits= 1; _}, q, p) ->
-        ap_fff (fun p q -> and_ p (not_ q)) p q
-    | Ap2 ((Ge | Uge), Integer {bits= 1; _}, p, q)
-     |Ap2 ((Le | Ule), Integer {bits= 1; _}, q, p) ->
-        ap_fff (fun p q -> or_ p (not_ q)) p q
-    | Ap2 (Eq, _, d, e) -> ap_ttf eq d e
-    | Ap2 (Dq, _, d, e) -> ap_ttf dq d e
-    | Ap2 (Gt, _, d, e) -> ap_ttf gt d e
-    | Ap2 (Lt, _, d, e) -> ap_ttf lt d e
-    | Ap2 (Ge, _, d, e) -> ap_ttf ge d e
-    | Ap2 (Le, _, d, e) -> ap_ttf le d e
-    | Ap2 (Ugt, typ, d, e) -> usap_ttf gt typ d e
-    | Ap2 (Ult, typ, d, e) -> usap_ttf lt typ d e
-    | Ap2 (Uge, typ, d, e) -> usap_ttf ge typ d e
-    | Ap2 (Ule, typ, d, e) -> usap_ttf le typ d e
-    | Ap2 (Ord, _, d, e) -> ap_ttf (upos2 (Predsym.uninterp "ord")) d e
-    | Ap2 (Uno, _, d, e) -> ap_ttf (uneg2 (Predsym.uninterp "ord")) d e
-    | Ap2 (Add, Integer {bits= 1; _}, p, q) -> ap_fff xor p q
-    | Ap2 (Sub, Integer {bits= 1; _}, p, q) -> ap_fff xor p q
-    | Ap2 (Mul, Integer {bits= 1; _}, p, q) -> ap_fff and_ p q
-    | Ap2 (Add, _, d, e) -> ap_ttt add d e
-    | Ap2 (Sub, _, d, e) -> ap_ttt sub d e
-    | Ap2 (Mul, _, d, e) -> ap_ttt mul d e
-    | Ap2 (Div, _, d, e) -> uap_tte Div d e
-    | Ap2 (Rem, _, d, e) -> uap_tte Rem d e
-    | Ap2 (Udiv, typ, d, e) -> usap_ttt (uap2 Div) typ d e
-    | Ap2 (Urem, typ, d, e) -> usap_ttt (uap2 Rem) typ d e
-    | Ap2 (And, Integer {bits= 1; _}, p, q) -> ap_fff and_ p q
-    | Ap2 (Or, Integer {bits= 1; _}, p, q) -> ap_fff or_ p q
-    | Ap2 (Xor, Integer {bits= 1; _}, p, q) -> ap_fff xor p q
-    | Ap2 (And, _, d, e) -> ap_ttt (uap2 BitAnd) d e
-    | Ap2 (Or, _, d, e) -> ap_ttt (uap2 BitOr) d e
-    | Ap2 (Xor, _, d, e) -> ap_ttt (uap2 BitXor) d e
-    | Ap2 (Shl, _, d, e) -> ap_ttt (uap2 BitShl) d e
-    | Ap2 (Lshr, _, d, e) -> ap_ttt (uap2 BitLshr) d e
-    | Ap2 (Ashr, _, d, e) -> ap_ttt (uap2 BitAshr) d e
-    | Ap3 (Conditional, Integer {bits= 1; _}, cnd, pos, neg) ->
-        ap_ffff _Cond cnd pos neg
-    | Ap3 (Conditional, _, cnd, thn, els) ->
-        ite ~cnd:(embed_into_fml (exp cnd)) ~thn:(exp thn) ~els:(exp els)
-    | Ap1 (Select idx, _, rcd) -> select ~rcd:(exp rcd) ~idx
-    | Ap2 (Update idx, _, rcd, elt) ->
-        update ~rcd:(exp rcd) ~idx ~elt:(exp elt)
-    | ApN (Record, _, elts) ->
-        record (Array.map ~f:exp (IArray.to_array elts))
-    | RecRecord (i, _) -> ancestor i
-    | Ap1 (Splat, _, byt) -> splat (exp byt)
-end
-
-module Formula_of_Llair = struct
-  let exp e = embed_into_fml (Term_of_Llair.exp e)
-end
-
-module Var_of_Llair = struct
-  let reg r =
-    match
-      Var.of_exp (Term_of_Llair.exp (r : Llair.Reg.t :> Llair.Exp.t))
-    with
-    | Some v -> v
-    | _ -> violates Llair.Reg.invariant r
-
-  let regs =
-    Llair.Reg.Set.fold ~init:Var.Set.empty ~f:(fun s r ->
-        Var.Set.add s (reg r) )
-end
diff --git a/sledge/src/fol.mli b/sledge/src/fol.mli
index 9dc918240..cdaff4888 100644
--- a/sledge/src/fol.mli
+++ b/sledge/src/fol.mli
@@ -64,6 +64,7 @@ module rec Term : sig
   val select : rcd:t -> idx:int -> t
   val update : rcd:t -> idx:int -> elt:t -> t
   val record : t array -> t
+  val ancestor : int -> t
 
   (* uninterpreted *)
   val apply : Ses.Funsym.t -> t array -> t
@@ -138,6 +139,8 @@ and Formula : sig
   val andN : t list -> t
   val or_ : t -> t -> t
   val orN : t list -> t
+  val iff : t -> t -> t
+  val xor : t -> t -> t
   val cond : cnd:t -> pos:t -> neg:t -> t
 
   (** Query *)
@@ -265,18 +268,3 @@ module Context : sig
   val replay : string -> unit
   (** Replay debugging *)
 end
-
-(** Convert from Llair *)
-
-module Var_of_Llair : sig
-  val reg : Llair.Reg.t -> Var.t
-  val regs : Llair.Reg.Set.t -> Var.Set.t
-end
-
-module Term_of_Llair : sig
-  val exp : Llair.Exp.t -> Term.t
-end
-
-module Formula_of_Llair : sig
-  val exp : Llair.Exp.t -> Formula.t
-end
diff --git a/sledge/src/llair_to_Fol.ml b/sledge/src/llair_to_Fol.ml
new file mode 100644
index 000000000..1501c4d34
--- /dev/null
+++ b/sledge/src/llair_to_Fol.ml
@@ -0,0 +1,127 @@
+(*
+ * 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.
+ *)
+
+open Fol
+module Funsym = Ses.Funsym
+module Predsym = Ses.Predsym
+module T = Term
+module F = Formula
+
+let reg r =
+  let name = Llair.Reg.name r in
+  let global = Llair.Reg.is_global r in
+  Var.program ~name ~global
+
+let regs =
+  Llair.Reg.Set.fold ~init:Var.Set.empty ~f:(fun s r ->
+      Var.Set.add s (reg r) )
+
+let uap0 f = T.apply f [||]
+let uap1 f a = T.apply f [|a|]
+let uap2 f a b = T.apply f [|a; b|]
+let uposlit2 p a b = F.uposlit p [|a; b|]
+let uneglit2 p a b = F.uneglit p [|a; b|]
+
+let rec ap_ttt : 'a. (T.t -> T.t -> 'a) -> _ -> _ -> 'a =
+ fun f a b -> f (term a) (term b)
+and ap_ttf (f : T.t -> T.t -> F.t) a b = F.inject (ap_ttt f a b)
+
+and ap_fff (f : F.t -> F.t -> F.t) a b =
+  F.inject (f (formula a) (formula b))
+
+and ap_uut : 'a. (T.t -> T.t -> 'a) -> _ -> _ -> _ -> 'a =
+ fun f typ a b ->
+  let bits = Llair.Typ.bit_size_of typ in
+  let unsigned x = uap1 (Unsigned bits) x in
+  f (unsigned (term a)) (unsigned (term b))
+
+and ap_uuf (f : T.t -> T.t -> F.t) typ a b = F.inject (ap_uut f typ a b)
+
+and term : Llair.Exp.t -> T.t =
+ fun e ->
+  match e with
+  | Reg {name; global; typ= _} -> T.var (Var.program ~name ~global)
+  | Label {parent; name} ->
+      uap0 (Funsym.uninterp ("label_" ^ parent ^ "_" ^ name))
+  | Integer {typ= _; data} -> T.integer data
+  | Float {data; typ= _} -> (
+    match Q.of_float (Float.of_string data) with
+    | q when Q.is_real q -> T.rational q
+    | _ | (exception Invalid_argument _) ->
+        uap0 (Funsym.uninterp ("float_" ^ data)) )
+  | Ap1 (Signed {bits}, _, e) ->
+      let a = term e in
+      if bits = 1 then
+        match F.project a with
+        | Some fml -> F.inject fml
+        | _ -> uap1 (Signed bits) a
+      else uap1 (Signed bits) a
+  | Ap1 (Unsigned {bits}, _, e) ->
+      let a = term e in
+      if bits = 1 then
+        match F.project a with
+        | Some fml -> F.inject fml
+        | _ -> uap1 (Unsigned bits) a
+      else uap1 (Unsigned bits) a
+  | Ap1 (Convert {src}, dst, e) ->
+      let s =
+        Format.asprintf "convert_%a_%a" Llair.Typ.pp src Llair.Typ.pp dst
+      in
+      uap1 (Funsym.uninterp s) (term e)
+  | Ap2 (Eq, Integer {bits= 1; _}, p, q) -> ap_fff F.iff p q
+  | Ap2 (Dq, Integer {bits= 1; _}, p, q) -> ap_fff F.xor p q
+  | Ap2 ((Gt | Ugt), Integer {bits= 1; _}, p, q)
+   |Ap2 ((Lt | Ult), Integer {bits= 1; _}, q, p) ->
+      ap_fff (fun p q -> F.and_ p (F.not_ q)) p q
+  | Ap2 ((Ge | Uge), Integer {bits= 1; _}, p, q)
+   |Ap2 ((Le | Ule), Integer {bits= 1; _}, q, p) ->
+      ap_fff (fun p q -> F.or_ p (F.not_ q)) p q
+  | Ap2 (Eq, _, d, e) -> ap_ttf F.eq d e
+  | Ap2 (Dq, _, d, e) -> ap_ttf F.dq d e
+  | Ap2 (Gt, _, d, e) -> ap_ttf F.gt d e
+  | Ap2 (Lt, _, d, e) -> ap_ttf F.lt d e
+  | Ap2 (Ge, _, d, e) -> ap_ttf F.ge d e
+  | Ap2 (Le, _, d, e) -> ap_ttf F.le d e
+  | Ap2 (Ugt, typ, d, e) -> ap_uuf F.gt typ d e
+  | Ap2 (Ult, typ, d, e) -> ap_uuf F.lt typ d e
+  | Ap2 (Uge, typ, d, e) -> ap_uuf F.ge typ d e
+  | Ap2 (Ule, typ, d, e) -> ap_uuf F.le typ d e
+  | Ap2 (Ord, _, d, e) -> ap_ttf (uposlit2 (Predsym.uninterp "ord")) d e
+  | Ap2 (Uno, _, d, e) -> ap_ttf (uneglit2 (Predsym.uninterp "ord")) d e
+  | Ap2 (Add, Integer {bits= 1; _}, p, q) -> ap_fff F.xor p q
+  | Ap2 (Sub, Integer {bits= 1; _}, p, q) -> ap_fff F.xor p q
+  | Ap2 (Mul, Integer {bits= 1; _}, p, q) -> ap_fff F.and_ p q
+  | Ap2 (Add, _, d, e) -> ap_ttt T.add d e
+  | Ap2 (Sub, _, d, e) -> ap_ttt T.sub d e
+  | Ap2 (Mul, _, d, e) -> ap_ttt T.mul d e
+  | Ap2 (Div, _, d, e) -> ap_ttt (uap2 Div) d e
+  | Ap2 (Rem, _, d, e) -> ap_ttt (uap2 Rem) d e
+  | Ap2 (Udiv, typ, d, e) -> ap_uut (uap2 Div) typ d e
+  | Ap2 (Urem, typ, d, e) -> ap_uut (uap2 Rem) typ d e
+  | Ap2 (And, Integer {bits= 1; _}, p, q) -> ap_fff F.and_ p q
+  | Ap2 (Or, Integer {bits= 1; _}, p, q) -> ap_fff F.or_ p q
+  | Ap2 (Xor, Integer {bits= 1; _}, p, q) -> ap_fff F.xor p q
+  | Ap2 (And, _, d, e) -> ap_ttt (uap2 BitAnd) d e
+  | Ap2 (Or, _, d, e) -> ap_ttt (uap2 BitOr) d e
+  | Ap2 (Xor, _, d, e) -> ap_ttt (uap2 BitXor) d e
+  | Ap2 (Shl, _, d, e) -> ap_ttt (uap2 BitShl) d e
+  | Ap2 (Lshr, _, d, e) -> ap_ttt (uap2 BitLshr) d e
+  | Ap2 (Ashr, _, d, e) -> ap_ttt (uap2 BitAshr) d e
+  | Ap3 (Conditional, Integer {bits= 1; _}, cnd, pos, neg) ->
+      F.inject
+        (F.cond ~cnd:(formula cnd) ~pos:(formula pos) ~neg:(formula neg))
+  | Ap3 (Conditional, _, cnd, thn, els) ->
+      T.ite ~cnd:(formula cnd) ~thn:(term thn) ~els:(term els)
+  | Ap1 (Select idx, _, rcd) -> T.select ~rcd:(term rcd) ~idx
+  | Ap2 (Update idx, _, rcd, elt) ->
+      T.update ~rcd:(term rcd) ~idx ~elt:(term elt)
+  | ApN (Record, _, elts) ->
+      T.record (Array.map ~f:term (IArray.to_array elts))
+  | RecRecord (i, _) -> T.ancestor i
+  | Ap1 (Splat, _, byt) -> T.splat (term byt)
+
+and formula e = F.dq0 (term e)
diff --git a/sledge/src/llair_to_Fol.mli b/sledge/src/llair_to_Fol.mli
new file mode 100644
index 000000000..cc501922d
--- /dev/null
+++ b/sledge/src/llair_to_Fol.mli
@@ -0,0 +1,13 @@
+(*
+ * 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.
+ *)
+
+open Fol
+
+val reg : Llair.Reg.t -> Var.t
+val regs : Llair.Reg.Set.t -> Var.Set.t
+val term : Llair.Exp.t -> Term.t
+val formula : Llair.Exp.t -> Formula.t
diff --git a/sledge/src/ses/funsym.ml b/sledge/src/ses/funsym.ml
index c11c07ee4..f00a5086e 100644
--- a/sledge/src/ses/funsym.ml
+++ b/sledge/src/ses/funsym.ml
@@ -37,3 +37,5 @@ let pp ppf f =
   | Signed n -> pf "(s%i)" n
   | Unsigned n -> pf "(u%i)" n
   | Uninterp sym -> pf "%s" sym
+
+let uninterp s = Uninterp s
diff --git a/sledge/src/ses/funsym.mli b/sledge/src/ses/funsym.mli
index 01d090076..5913296dc 100644
--- a/sledge/src/ses/funsym.mli
+++ b/sledge/src/ses/funsym.mli
@@ -35,3 +35,4 @@ type t =
 [@@deriving compare, equal, sexp]
 
 val pp : t pp
+val uninterp : string -> t
diff --git a/sledge/src/test/fol_test.ml b/sledge/src/test/fol_test.ml
index a4a19764a..314f4159b 100644
--- a/sledge/src/test/fol_test.ml
+++ b/sledge/src/test/fol_test.ml
@@ -523,7 +523,7 @@ let%test_module _ =
 
     let%test "unsigned boolean overflow" =
       Formula.equal Formula.tt
-        (Formula_of_Llair.exp
+        (Llair_to_Fol.formula
            Llair.(
              Exp.uge
                (Exp.integer Typ.bool Z.minus_one)
@@ -531,7 +531,7 @@ let%test_module _ =
 
     let pp_exp e =
       Format.printf "@\nexp= %a; term= %a@." Llair.Exp.pp e Term.pp
-        (Term_of_Llair.exp e)
+        (Llair_to_Fol.term e)
 
     let ( !! ) i = Llair.(Exp.integer Typ.siz (Z.of_int i))