diff --git a/infer/src/pulse/Pudge_intf.ml b/infer/src/pulse/Pudge_intf.ml
index 60aba4b24..132fa87d4 100644
--- a/infer/src/pulse/Pudge_intf.ml
+++ b/infer/src/pulse/Pudge_intf.ml
@@ -16,39 +16,43 @@ module type S = sig
 
   val true_ : t
 
-  module Term : sig
+  module Var : sig
     type t
 
-    val zero : t
+    val of_absval : AbstractValue.t -> t
 
-    val le : t -> t -> t
+    val to_absval : t -> AbstractValue.t
+    (** use with caution: will crash the program if the given variable wasn't generated from an
+        [AbstractValue.t] using [Var.of_absval] *)
+  end
 
-    val lt : t -> t -> t
+  module Term : sig
+    type t
 
-    val not_ : t -> t
+    val zero : t
 
     val of_intlit : IntLit.t -> t
 
     val of_absval : AbstractValue.t -> t
 
-    val of_unop : Unop.t -> t -> t
+    val of_unop : Unop.t -> t -> t option
 
-    val of_binop : Binop.t -> t -> t -> t
+    val of_binop : Binop.t -> t -> t -> t option
   end
 
-  module Var : sig
+  module Formula : sig
     type t
 
-    val of_absval : AbstractValue.t -> t
+    val eq : Term.t -> Term.t -> t
 
-    val to_absval : t -> AbstractValue.t
-    (** use with caution: will crash the program if the given variable wasn't generated from an
-        [AbstractValue.t] using [Var.of_absval] *)
-  end
+    val lt : Term.t -> Term.t -> t
 
-  val and_eq : Term.t -> Term.t -> t -> t
+    val not_ : t -> t
+
+    val term_binop : Binop.t -> Term.t -> Term.t -> t option
+  end
 
-  val and_term : Term.t -> t -> t
+  val and_formula : Formula.t -> t -> t
 
   val and_ : t -> t -> t
 
diff --git a/infer/src/pulse/PulseDummySledge.ml b/infer/src/pulse/PulseDummySledge.ml
index 2fc206181..a8b2061b4 100644
--- a/infer/src/pulse/PulseDummySledge.ml
+++ b/infer/src/pulse/PulseDummySledge.ml
@@ -21,19 +21,25 @@ module Term = struct
 
   let zero = ()
 
-  let le () () = ()
+  let of_intlit _ = ()
 
-  let lt () () = ()
+  let of_absval _ = ()
 
-  let not_ () = ()
+  let of_unop _ () = None
 
-  let of_intlit _ = ()
+  let of_binop _ () () = None
+end
 
-  let of_absval _ = ()
+module Formula = struct
+  type t = unit
+
+  let eq () () = ()
+
+  let lt () () = ()
 
-  let of_unop _ () = ()
+  let not_ () = ()
 
-  let of_binop _ () () = ()
+  let term_binop _ () () = None
 end
 
 (* same type as {!PulsePathCondition.t} to be nice to summary serialization *)
@@ -46,9 +52,7 @@ let pp fmt {eqs= (lazy eqs); non_eqs= (lazy non_eqs)} =
 
 let true_ = {eqs= Lazy.from_val Ses.Equality.true_; non_eqs= Lazy.from_val Ses.Term.true_}
 
-let and_eq () () phi = phi
-
-let and_term () phi = phi
+let and_formula () phi = phi
 
 let and_ phi1 _ = phi1
 
diff --git a/infer/src/pulse/PulsePathCondition.ml b/infer/src/pulse/PulsePathCondition.ml
index 046ce8fa1..644a1b507 100644
--- a/infer/src/pulse/PulsePathCondition.ml
+++ b/infer/src/pulse/PulsePathCondition.ml
@@ -51,7 +51,7 @@ let and_nonnegative v ({satisfiable; bo_itvs; citvs; pudge} as phi) =
     { satisfiable
     ; bo_itvs= BoItvs.add v Itv.ItvPure.nat bo_itvs
     ; citvs= CItvs.add v CItv.zero_inf citvs
-    ; pudge= Pudge.and_term Pudge.Term.(le zero (of_absval v)) pudge }
+    ; pudge= Pudge.(and_formula (Formula.lt Term.zero (Term.of_absval v)) pudge) }
 
 
 let and_positive v ({satisfiable; bo_itvs; citvs; pudge} as phi) =
@@ -60,7 +60,7 @@ let and_positive v ({satisfiable; bo_itvs; citvs; pudge} as phi) =
     { satisfiable
     ; bo_itvs= BoItvs.add v Itv.ItvPure.pos bo_itvs
     ; citvs= CItvs.add v (CItv.ge_to IntLit.one) citvs
-    ; pudge= Pudge.and_term Pudge.Term.(lt zero (of_absval v)) pudge }
+    ; pudge= Pudge.(and_formula (Formula.lt Term.zero (Term.of_absval v)) pudge) }
 
 
 let and_eq_int v i ({satisfiable; bo_itvs; citvs; pudge} as phi) =
@@ -69,7 +69,7 @@ let and_eq_int v i ({satisfiable; bo_itvs; citvs; pudge} as phi) =
     { satisfiable
     ; bo_itvs= BoItvs.add v (Itv.ItvPure.of_int_lit i) bo_itvs
     ; citvs= CItvs.add v (CItv.equal_to i) citvs
-    ; pudge= Pudge.and_eq (Pudge.Term.of_absval v) (Pudge.Term.of_intlit i) pudge }
+    ; pudge= Pudge.(and_formula (Formula.eq (Term.of_absval v) (Term.of_intlit i)) pudge) }
 
 
 let simplify ~keep {satisfiable; bo_itvs; citvs; pudge} =
@@ -182,8 +182,9 @@ let and_pudge_callee subst pudge_caller pudge_callee =
         let subst', v_caller = subst_find_or_new subst v_callee in
         (subst', Pudge.Var.of_absval v_caller) )
   in
-  (* Don't trigger the computation of [path_condition] by asking for satisfiability here. Instead,
-     pudge (un-)satisfiability is computed lazily when we discover issues. *)
+  (* Don't trigger the computation of the underlying Sledge data structure by asking for
+     satisfiability here. Instead, pudge (un-)satisfiability is computed lazily when we discover
+     issues. *)
   (subst, Pudge.and_ pudge_caller pudge_callee_translated)
 
 
@@ -240,16 +241,19 @@ let eval_bo_itv_binop binop_addr bop op_lhs op_rhs bo_itvs =
   BoItvs.add binop_addr bo_itv bo_itvs
 
 
-let eval_path_condition_binop binop_addr binop op_lhs op_rhs pudge =
+let eval_pudge_binop binop_addr binop op_lhs op_rhs pudge =
+  let open Pudge in
   let term_of_op = function
     | LiteralOperand i ->
-        Pudge.Term.of_intlit i
+        Term.of_intlit i
     | AbstractValueOperand v ->
-        Pudge.Term.of_absval v
+        Term.of_absval v
   in
-  Pudge.and_eq (Pudge.Term.of_absval binop_addr)
-    (Pudge.Term.of_binop binop (term_of_op op_lhs) (term_of_op op_rhs))
-    pudge
+  match Term.of_binop binop (term_of_op op_lhs) (term_of_op op_rhs) with
+  | None ->
+      pudge
+  | Some t_binop ->
+      and_formula (Formula.eq (Term.of_absval binop_addr) t_binop) pudge
 
 
 let eval_binop binop_addr binop op_lhs op_rhs ({satisfiable; bo_itvs; citvs; pudge} as phi) =
@@ -258,7 +262,7 @@ let eval_binop binop_addr binop op_lhs op_rhs ({satisfiable; bo_itvs; citvs; pud
     { satisfiable
     ; bo_itvs= eval_bo_itv_binop binop_addr binop op_lhs op_rhs bo_itvs
     ; citvs= eval_citv_binop binop_addr binop op_lhs op_rhs citvs
-    ; pudge= eval_path_condition_binop binop_addr binop op_lhs op_rhs pudge }
+    ; pudge= eval_pudge_binop binop_addr binop op_lhs op_rhs pudge }
 
 
 let eval_citv_unop unop_addr unop operand_addr citvs =
@@ -278,8 +282,13 @@ let eval_bo_itv_unop unop_addr unop operand_addr bo_itvs =
       BoItvs.add unop_addr itv bo_itvs
 
 
-let eval_path_condition_unop unop_addr unop addr pudge =
-  Pudge.and_eq (Pudge.Term.of_absval unop_addr) Pudge.Term.(of_unop unop (of_absval addr)) pudge
+let eval_pudge_unop unop_addr (unop : Unop.t) addr pudge =
+  let open Pudge in
+  match Term.of_unop unop (Term.of_absval addr) with
+  | None ->
+      pudge
+  | Some t_unop ->
+      and_formula (Formula.eq (Term.of_absval unop_addr) t_unop) pudge
 
 
 let eval_unop unop_addr unop addr ({satisfiable; bo_itvs; citvs; pudge} as phi) =
@@ -288,7 +297,7 @@ let eval_unop unop_addr unop addr ({satisfiable; bo_itvs; citvs; pudge} as phi)
     { satisfiable
     ; bo_itvs= eval_bo_itv_unop unop_addr unop addr bo_itvs
     ; citvs= eval_citv_unop unop_addr unop addr citvs
-    ; pudge= eval_path_condition_unop unop_addr unop addr pudge }
+    ; pudge= eval_pudge_unop unop_addr unop addr pudge }
 
 
 let prune_bo_with_bop ~negated v_opt arith bop arith' phi =
@@ -328,15 +337,18 @@ let bind_satisfiable phi ~f = if phi.satisfiable then f phi else phi
 let prune_binop ~negated bop lhs_op rhs_op ({satisfiable; bo_itvs= _; citvs; pudge} as phi) =
   if not satisfiable then phi
   else
-    let value_lhs_opt, arith_lhs_opt, bo_itv_lhs, path_cond_lhs = eval_operand phi lhs_op in
-    let value_rhs_opt, arith_rhs_opt, bo_itv_rhs, path_cond_rhs = eval_operand phi rhs_op in
+    let value_lhs_opt, arith_lhs_opt, bo_itv_lhs, pudge_lhs = eval_operand phi lhs_op in
+    let value_rhs_opt, arith_rhs_opt, bo_itv_rhs, pudge_rhs = eval_operand phi rhs_op in
     let phi =
-      let pudge =
-        let t_positive = Pudge.Term.of_binop bop path_cond_lhs path_cond_rhs in
-        let t = if negated then Pudge.Term.not_ t_positive else t_positive in
-        Pudge.and_term t pudge
-      in
-      {phi with pudge}
+      match Pudge.Formula.term_binop bop pudge_lhs pudge_rhs with
+      | None ->
+          phi
+      | Some f_positive ->
+          let pudge =
+            let f = if negated then Pudge.Formula.not_ f_positive else f_positive in
+            Pudge.and_formula f pudge
+          in
+          {phi with pudge}
     in
     match CItv.abduce_binop_is_true ~negated bop arith_lhs_opt arith_rhs_opt with
     | Unsatisfiable ->
diff --git a/infer/src/pulse/PulseSledge.ml b/infer/src/pulse/PulseSledge.ml
index 009713277..d9a47c529 100644
--- a/infer/src/pulse/PulseSledge.ml
+++ b/infer/src/pulse/PulseSledge.ml
@@ -6,14 +6,13 @@
  *)
 
 open! IStd
-module F = Format
 module L = Logging
 module AbstractValue = PulseAbstractValue
 
 [@@@warning "+9"]
 
 module Var = struct
-  module Var = Ses.Var
+  module Var = Sledge.Fol.Var
 
   let of_absval (v : AbstractValue.t) = Var.identified ~name:"v" ~id:(v :> int)
 
@@ -26,153 +25,133 @@ module Var = struct
 end
 
 module Term = struct
-  module Term = Ses.Term
+  module Term = Sledge.Fol.Term
 
   let of_intlit i = Term.integer (IntLit.to_big_int i)
 
   let of_absval v = Term.var (Var.of_absval v)
 
-  let of_unop (unop : Unop.t) t = match unop with Neg -> Term.neg t | BNot | LNot -> Term.not_ t
+  let of_unop (unop : Unop.t) t = match unop with Neg -> Some (Term.neg t) | BNot | LNot -> None
 
   let of_binop (binop : Binop.t) t1 t2 =
     let open Term in
     match binop with
     | PlusA _ | PlusPI ->
-        add t1 t2
+        Some (add t1 t2)
     | MinusA _ | MinusPI | MinusPP ->
-        sub t1 t2
+        Some (sub t1 t2)
     | Mult _ ->
-        mul t1 t2
-    | Div ->
-        div t1 t2
-    | Mod ->
-        rem t1 t2
-    | Shiftlt ->
-        shl t1 t2
+        Some (mul t1 t2)
+    | Div | Mod | Shiftlt | Shiftrt | Lt | Gt | Le | Ge | Eq | Ne | BAnd | LAnd | BOr | LOr | BXor
+      ->
+        None
+
+
+  include Term
+end
+
+module Formula = struct
+  module Formula = Sledge.Fol.Formula
+
+  let term_binop (binop : Binop.t) t1 t2 =
+    match binop with
+    | BAnd
+    | BOr
+    | BXor
+    | PlusA _
+    | PlusPI
+    | MinusA _
+    | MinusPI
+    | MinusPP
+    | Mult _
+    | Div
+    | Mod
+    | Shiftlt
     | Shiftrt ->
-        lshr t1 t2
+        Term.of_binop binop t1 t2 |> Option.map ~f:(fun t -> Formula.dq t Term.zero)
     | Lt ->
-        lt t1 t2
+        Some (Formula.lt t1 t2)
     | Gt ->
-        lt t2 t1
+        Some (Formula.lt t2 t1)
     | Le ->
-        le t1 t2
+        Some (Formula.le t1 t2)
     | Ge ->
-        le t2 t1
+        Some (Formula.le t2 t1)
     | Eq ->
-        eq t1 t2
+        Some (Formula.eq t1 t2)
     | Ne ->
-        dq t1 t2
-    | BAnd | LAnd ->
-        and_ t1 t2
-    | BOr | LOr ->
-        or_ t1 t2
-    | BXor ->
-        xor t1 t2
+        Some (Formula.dq t1 t2)
+    | LAnd ->
+        Option.both (Formula.project t1) (Formula.project t2)
+        |> Option.map ~f:(fun (f1, f2) -> Formula.and_ f1 f2)
+    | LOr ->
+        Option.both (Formula.project t1) (Formula.project t2)
+        |> Option.map ~f:(fun (f1, f2) -> Formula.or_ f1 f2)
 
 
-  include Term
+  include Formula
 end
 
-module Equality = struct
-  include Ses.Equality
+module Context = struct
+  include Sledge.Fol.Context
 
   let assert_no_new_vars api new_vars =
     if not (Var.Set.is_empty new_vars) then
       L.die InternalError "Huho, %s generated fresh new variables %a" api Var.Set.pp new_vars
 
 
-  let and_eq t1 t2 r =
-    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' = Ses.Equality.and_term Var.Set.empty t r in
-    assert_no_new_vars "Equality.and_term" new_vars ;
+  let and_formula phi r =
+    let new_vars, r' = Sledge.Fol.Context.and_formula Var.Set.empty phi r in
+    assert_no_new_vars "Context.and_formula" new_vars ;
     r'
 
 
   let and_ r1 r2 =
-    let new_vars, r' = Ses.Equality.and_ Var.Set.empty r1 r2 in
-    assert_no_new_vars "Equality.and_" new_vars ;
+    let new_vars, r' = Sledge.Fol.Context.and_ Var.Set.empty r1 r2 in
+    assert_no_new_vars "Context.and_" new_vars ;
     r'
 
 
   let apply_subst subst r =
-    let new_vars, r' = Ses.Equality.apply_subst Var.Set.empty subst r in
-    assert_no_new_vars "Equality.apply_subst" new_vars ;
+    let new_vars, r' = Sledge.Fol.Context.apply_subst Var.Set.empty subst r in
+    assert_no_new_vars "Context.apply_subst" new_vars ;
     r'
 end
 
-(** We distinguish between what the equality relation of sledge can express and the "non-equalities"
-    terms that this relation ignores. We keep the latter around for completeness: we can still
-    substitute known equalities into these and sometimes get contradictions back. *)
-type t = {eqs: Equality.t lazy_t; non_eqs: Term.t lazy_t}
-
-let pp fmt {eqs= (lazy eqs); non_eqs= (lazy non_eqs)} =
-  F.fprintf fmt "%a∧%a" Equality.pp eqs Term.pp non_eqs
-
-
-let true_ = {eqs= Lazy.from_val Equality.true_; non_eqs= Lazy.from_val Term.true_}
+type t = Context.t lazy_t
 
-let and_eq t1 t2 phi = {phi with eqs= lazy (Equality.and_eq t1 t2 (Lazy.force phi.eqs))}
+let pp fmt (lazy phi) = Context.pp fmt phi
 
-let and_term (t : Term.t) phi =
-  (* add the term to the relation *)
-  let eqs = lazy (Equality.and_term t (Lazy.force phi.eqs)) in
-  (* [t] normalizes to [true_] so [non_eqs] never changes, do this regardless for now *)
-  let non_eqs = lazy (Term.and_ (Lazy.force phi.non_eqs) (Equality.normalize (Lazy.force eqs) t)) in
-  {eqs; non_eqs}
+let true_ = Lazy.from_val Context.true_
 
+let and_formula f phi = lazy (Context.and_formula f (Lazy.force phi))
 
-let and_ phi1 phi2 =
-  { eqs= lazy (Equality.and_ (Lazy.force phi1.eqs) (Lazy.force phi2.eqs))
-  ; non_eqs= lazy (Term.and_ (Lazy.force phi1.non_eqs) (Lazy.force phi2.non_eqs)) }
+let and_ phi1 phi2 = lazy (Context.and_ (Lazy.force phi1) (Lazy.force phi2))
 
+let is_known_zero t phi = Context.entails_eq (Lazy.force phi) t Term.zero
 
-let is_known_zero t phi = Equality.entails_eq (Lazy.force phi.eqs) t Term.zero
-
-(* NOTE: not normalizing non_eqs here gives imprecise results but is cheaper *)
-let is_unsat {eqs; non_eqs} =
-  (* [Term.is_false] is cheap, forcing [eqs] is expensive, then calling [Equality.normalize] is
-     expensive on top of that *)
-  Term.is_false (Lazy.force non_eqs)
-  || Equality.is_false (Lazy.force eqs)
-  || Term.is_false (Equality.normalize (Lazy.force eqs) (Lazy.force non_eqs))
-
-
-let fv {eqs= (lazy eqs); non_eqs= (lazy non_eqs)} =
-  Term.Var.Set.union (Equality.fv eqs) (Term.fv non_eqs)
+let is_unsat phi = Context.is_false (Lazy.force phi)
 
+let fv (lazy phi) = Context.fv phi
 
 let fold_map_variables phi ~init ~f =
-  let term_fold_map t ~init ~f =
-    Term.fold_map_rec_pre t ~init ~f:(fun acc t ->
-        Var.of_term t
-        |> Option.map ~f:(fun v ->
-               let acc', v' = f acc v in
-               (acc', Term.var v') ) )
-  in
-  let acc, eqs' =
-    Equality.classes (Lazy.force phi.eqs)
-    |> Term.Map.fold ~init:(init, Equality.true_) ~f:(fun ~key:t ~data:equal_ts (acc, eqs') ->
-           let acc, t' = term_fold_map ~init:acc ~f t in
-           List.fold equal_ts ~init:(acc, eqs') ~f:(fun (acc, eqs') equal_t ->
-               let acc, t_mapped = term_fold_map ~init:acc ~f equal_t in
-               (acc, Equality.and_eq t' t_mapped eqs') ) )
+  let acc, phi' =
+    Context.classes (Lazy.force phi)
+    |> Term.Map.fold ~init:(init, Context.true_) ~f:(fun ~key:t ~data:equal_ts (acc, phi') ->
+           let acc, t' = Term.fold_map_vars ~init:acc ~f t in
+           List.fold equal_ts ~init:(acc, phi') ~f:(fun (acc, phi') equal_t ->
+               let acc, t_mapped = Term.fold_map_vars ~init:acc ~f equal_t in
+               (acc, Context.and_formula (Formula.eq t' t_mapped) phi') ) )
   in
-  let acc, non_eqs' = term_fold_map ~init:acc ~f (Lazy.force phi.non_eqs) in
-  (acc, {eqs= Lazy.from_val eqs'; non_eqs= Lazy.from_val non_eqs'})
+  (acc, Lazy.from_val phi')
 
 
 let simplify ~keep phi =
   let all_vs = fv phi in
   let keep_vs =
     AbstractValue.Set.fold
-      (fun v keep_vs -> Term.Var.Set.add keep_vs (Var.of_absval v))
-      keep Term.Var.Set.empty
+      (fun v keep_vs -> Var.Set.add keep_vs (Var.of_absval v))
+      keep Var.Set.empty
   in
-  let simpl_subst = Equality.solve_for_vars [keep_vs; all_vs] (Lazy.force phi.eqs) in
-  {phi with eqs= Lazy.from_val (Equality.apply_subst simpl_subst (Lazy.force phi.eqs))}
+  let simpl_subst = Context.solve_for_vars [keep_vs; all_vs] (Lazy.force phi) in
+  Lazy.from_val (Context.apply_subst simpl_subst (Lazy.force phi))
diff --git a/sledge/src/fol.ml b/sledge/src/fol.ml
index 578596fd1..69e990db6 100644
--- a/sledge/src/fol.ml
+++ b/sledge/src/fol.ml
@@ -5,15 +5,280 @@
  * LICENSE file in the root directory of this source tree.
  *)
 
-module Var = struct
-  include Ses.Term.Var
+let pp_boxed fs fmt =
+  Format.pp_open_box fs 2 ;
+  Format.kfprintf (fun fs -> Format.pp_close_box fs ()) fs fmt
+
+(*
+ * Terms
+ *)
+
+(** Terms, denoting functions from structures to values, built from
+    variables and applications of function symbols from various theories. *)
+type trm =
+  | Var of {id: int; name: string}
+  | Z of Z.t
+  | Q of Q.t
+  | Neg of trm
+  | Add of trm * trm
+  | Sub of trm * trm
+  | Mulq of Q.t * trm
+  | Mul of trm * trm
+  | Div of trm * trm
+  | Rem of trm * trm
+  | Splat of trm
+  | Sized of {seq: trm; siz: trm}
+  | Extract of {seq: trm; off: trm; len: trm}
+  | Concat of trm iarray
+  | Select of trm * int
+  | Update of trm * int * trm
+  | Record of trm iarray
+  | RecRecord of int
+  | Label of {parent: string; name: string}
+  | Float of string
+  | BAnd of trm * trm
+  | BOr of trm * trm
+  | BXor of trm * trm
+  | BShl of trm * trm
+  | BLshr of trm * trm
+  | BAshr of trm * trm
+  | Signed of int * trm
+  | Unsigned of int * trm
+  | Convert of {src: Llair.Typ.t; dst: Llair.Typ.t; arg: trm}
+[@@deriving compare, equal, sexp]
+
+let compare_trm x y =
+  if x == y then 0
+  else
+    match (x, y) with
+    | Var {id= i; name= _}, Var {id= j; name= _} when i > 0 && j > 0 ->
+        Int.compare i j
+    | _ -> compare_trm x y
+
+let equal_trm x y =
+  x == y
+  ||
+  match (x, y) with
+  | Var {id= i; name= _}, Var {id= j; name= _} when i > 0 && j > 0 ->
+      Int.equal i j
+  | _ -> equal_trm x y
+
+let _Neg x = Neg x
+let _Add x y = Add (x, y)
+let _Sub x y = Sub (x, y)
+let _Mulq q x = Mulq (q, x)
+let _Mul x y = Mul (x, y)
+let _Div x y = Div (x, y)
+let _Rem x y = Rem (x, y)
+let _Splat x = Splat x
+let _Sized seq siz = Sized {seq; siz}
+let _Extract seq off len = Extract {seq; off; len}
+let _Concat es = Concat es
+let _Select r i = Select (r, i)
+let _Update r i x = Update (r, i, x)
+let _Record es = Record es
+let _RecRecord n = RecRecord n
+let _BAnd x y = BAnd (x, y)
+let _BOr x y = BOr (x, y)
+let _BXor x y = BXor (x, y)
+let _BShl x y = BShl (x, y)
+let _BLshr x y = BLshr (x, y)
+let _BAshr x y = BAshr (x, y)
+let _Signed n x = Signed (n, x)
+let _Unsigned n x = Unsigned (n, x)
+let _Convert src dst arg = Convert {src; dst; arg}
+
+(*
+ * Formulas
+ *)
+
+(** Formulas, denoting sets of structures, built from propositional
+    variables, applications of predicate symbols from various theories, and
+    first-order logic connectives. *)
+type fml =
+  | Tt
+  | Ff
+  | Eq of trm * trm
+  | Dq of trm * trm
+  | Lt of trm * trm
+  | Le of trm * trm
+  | Ord of trm * trm
+  | Uno of trm * trm
+  | Not of fml
+  | And of fml * fml
+  | Or of fml * fml
+  | Iff of fml * fml
+  | Xor of fml * fml
+  | Imp of fml * fml
+  | Cond of {cnd: fml; pos: fml; neg: fml}
+[@@deriving compare, equal, sexp]
+
+let _Eq x y = Eq (x, y)
+let _Dq x y = Dq (x, y)
+let _Lt x y = Lt (x, y)
+let _Le x y = Le (x, y)
+let _Ord x y = Ord (x, y)
+let _Uno x y = Uno (x, y)
+let _Not p = Not p
+let _And p q = And (p, q)
+let _Or p q = Or (p, q)
+let _Iff p q = Iff (p, q)
+let _Xor p q = Xor (p, q)
+let _Imp p q = Imp (p, q)
+let _Cond cnd pos neg = Cond {cnd; pos; neg}
+
+(*
+ * Conditional terms
+ *)
+
+(** Conditional terms, denoting functions from structures to values, taking
+    the form of trees with internal nodes labeled with formulas and leaves
+    labeled with terms. *)
+type cnd = [`Ite of fml * cnd * cnd | `Trm of trm]
+[@@deriving compare, equal, sexp]
+
+(*
+ * Expressions
+ *)
+
+(** Expressions, which are partitioned into terms, conditional terms, and
+    formulas. *)
+type exp = [cnd | `Fml of fml] [@@deriving compare, equal, sexp]
+
+(*
+ * Variables
+ *)
+
+(** Variable terms *)
+module Var : sig
+  type t = private trm [@@deriving compare, equal, sexp]
+  type strength = t -> [`Universal | `Existential | `Anonymous] option
+
+  val ppx : strength -> t pp
+  val pp : t pp
+
+  module Map : Map.S with type key := t
+
+  module Set : sig
+    include NS.Set.S with type elt := t
+
+    val sexp_of_t : t -> Sexp.t
+    val t_of_sexp : Sexp.t -> t
+    val ppx : strength -> t pp
+    val pp : t pp
+    val pp_xs : t pp
+  end
+
+  val of_ : trm -> t
+  val of_exp : exp -> t option
+  val program : name:string -> global:bool -> t
+  val fresh : string -> wrt:Set.t -> t * Set.t
+
+  val identified : name:string -> id:int -> t
+  (** Variable with the given [id]. Variables are compared by [id] alone,
+      [name] is used only for printing. The only way to ensure [identified]
+      variables do not clash with [fresh] variables is to pass the
+      [identified] variables to [fresh] in [wrt]:
+      [Var.fresh name ~wrt:(Var.Set.of_ (Var.identified ~name ~id))]. *)
+
+  val id : t -> int
+  val name : t -> string
+
+  module Subst : sig
+    type var := t
+    type t [@@deriving compare, equal, sexp]
+    type x = {sub: t; dom: Set.t; rng: Set.t}
+
+    val pp : t pp
+    val empty : t
+    val freshen : Set.t -> wrt:Set.t -> x * Set.t
+    val invert : t -> t
+    val restrict : t -> Set.t -> x
+    val is_empty : t -> bool
+    val domain : t -> Set.t
+    val range : t -> Set.t
+    val fold : t -> init:'a -> f:(var -> var -> 'a -> 'a) -> 'a
+    val apply : t -> var -> var
+  end
+end = struct
+  module T = struct
+    type t = trm [@@deriving compare, equal, sexp]
+    type strength = t -> [`Universal | `Existential | `Anonymous] option
+
+    let invariant (x : t) =
+      let@ () = Invariant.invariant [%here] x [%sexp_of: t] in
+      match x with
+      | Var _ -> ()
+      | _ -> fail "non-var: %a" Sexp.pp_hum (sexp_of_trm x) ()
+
+    let ppx strength fs v =
+      let pf fmt = pp_boxed fs fmt in
+      match (v : trm) with
+      | Var {name; id= -1} -> Trace.pp_styled `Bold "%@%s" fs name
+      | Var {name; id= 0} -> Trace.pp_styled `Bold "%%%s" fs name
+      | Var {name; id} -> (
+        match strength v with
+        | None -> pf "%%%s_%d" name id
+        | Some `Universal -> Trace.pp_styled `Bold "%%%s_%d" fs name id
+        | Some `Existential -> Trace.pp_styled `Cyan "%%%s_%d" fs name id
+        | Some `Anonymous -> Trace.pp_styled `Cyan "_" fs )
+      | x -> violates invariant x
+
+    let pp = ppx (fun _ -> None)
+  end
+
+  include T
+
+  module Map = struct
+    include Map.Make (T)
+    include Provide_of_sexp (T)
+  end
+
+  module Set = struct
+    include Set.Make (T)
+    include Provide_of_sexp (T)
+
+    let ppx strength vs = pp (T.ppx strength) vs
+    let pp vs = pp T.pp vs
+
+    let pp_xs fs xs =
+      if not (is_empty xs) then
+        Format.fprintf fs "@<2>∃ @[%a@] .@;<1 2>" pp xs
+  end
+
+  (* access *)
+
+  let id = function Var v -> v.id | x -> violates invariant x
+  let name = function Var v -> v.name | x -> violates invariant x
+
+  (* construct *)
+
+  let of_ = function Var _ as v -> v | _ -> invalid_arg "Var.of_"
+
+  let of_exp = function
+    | `Trm (Var _ as v) -> Some (v |> check invariant)
+    | _ -> None
+
+  let program ~name ~global = Var {name; id= (if global then -1 else 0)}
+
+  let fresh name ~wrt =
+    let max = match Set.max_elt wrt with None -> 0 | Some max -> id max in
+    let x' = Var {name; id= max + 1} in
+    (x', Set.add wrt x')
+
+  let identified ~name ~id = Var {name; id}
+
+  (*
+   * Renamings
+   *)
 
   (** Variable renaming substitutions *)
   module Subst = struct
-    type nonrec t = t Map.t [@@deriving compare, equal, sexp_of]
+    type t = trm Map.t [@@deriving compare, equal, sexp_of]
     type x = {sub: t; dom: Set.t; rng: Set.t}
 
     let t_of_sexp = Map.t_of_sexp t_of_sexp
+    let pp = Map.pp pp pp
 
     let invariant s =
       let@ () = Invariant.invariant [%here] s [%sexp_of: t] in
@@ -26,7 +291,6 @@ module Var = struct
       in
       assert (Set.disjoint domain range)
 
-    let pp = Map.pp pp pp
     let empty = Map.empty
     let is_empty = Map.is_empty
 
@@ -83,42 +347,920 @@ module Var = struct
   end
 end
 
-module Term = struct
-  include (
-    Ses.Term : module type of Ses.Term with module Var := Ses.Term.Var )
+type var = Var.t
 
-  let ite = conditional
-  let rename s e = rename (Var.Subst.apply s) e
-end
+(*
+ * Representation operations
+ *)
+
+(** pp *)
+
+let rec ppx_t strength fs trm =
+  let rec pp fs trm =
+    let pf fmt = pp_boxed fs fmt in
+    match (trm : trm) with
+    | Var _ as v -> Var.ppx strength fs (Var.of_ v)
+    | Z z -> Trace.pp_styled `Magenta "%a" fs Z.pp z
+    | Q q -> Trace.pp_styled `Magenta "%a" fs Q.pp q
+    | Neg x -> pf "(- %a)" pp x
+    | Add (x, y) -> pf "(%a@ + %a)" pp x pp y
+    | Sub (x, y) -> pf "(%a@ - %a)" pp x pp y
+    | Mulq (q, x) -> pf "(%a@ @<2>× %a)" Q.pp q pp x
+    | Mul (x, y) -> pf "(%a@ @<2>× %a)" pp x pp y
+    | Div (x, y) -> pf "(%a@ / %a)" pp x pp y
+    | Rem (x, y) -> pf "(%a@ %% %a)" pp x pp y
+    | Splat x -> pf "%a^" pp x
+    | Sized {seq; siz} -> pf "@<1>⟨%a,%a@<1>⟩" pp siz pp seq
+    | Extract {seq; off; len} -> pf "%a[%a,%a)" pp seq pp off pp len
+    | Concat xs when IArray.is_empty xs -> pf "@<2>⟨⟩"
+    | Concat xs -> pf "(%a)" (IArray.pp "@,^" pp) xs
+    | Select (rcd, idx) -> pf "%a[%i]" pp rcd idx
+    | Update (rcd, idx, elt) -> pf "[%a@ @[| %i → %a@]]" pp rcd idx pp elt
+    | Record xs -> pf "{%a}" (pp_record strength) xs
+    | RecRecord i -> pf "(rec_record %i)" i
+    | Label {name} -> pf "%s" name
+    | Float s -> pf "%s" s
+    | BAnd (x, y) -> pf "(%a@ && %a)" pp x pp y
+    | BOr (x, y) -> pf "(%a@ || %a)" pp x pp y
+    | BXor (x, y) -> pf "(%a@ xor %a)" pp x pp y
+    | BShl (x, y) -> pf "(%a@ shl %a)" pp x pp y
+    | BLshr (x, y) -> pf "(%a@ lshr %a)" pp x pp y
+    | BAshr (x, y) -> pf "(%a@ ashr %a)" pp x pp y
+    | Signed (n, x) -> pf "((s%i)@ %a)" n pp x
+    | Unsigned (n, x) -> pf "((u%i)@ %a)" n pp x
+    | Convert {src; dst; arg} ->
+        pf "((%a)(%a)@ %a)" Llair.Typ.pp dst Llair.Typ.pp src pp arg
+  in
+  pp fs trm
+
+and pp_record strength fs elts =
+  [%Trace.fprintf
+    fs "%a"
+      (fun fs elts ->
+        match
+          String.init (IArray.length elts) ~f:(fun i ->
+              match IArray.get elts i with
+              | Z z -> Char.of_int_exn (Z.to_int z)
+              | _ -> raise (Invalid_argument "not a string") )
+        with
+        | s -> Format.fprintf fs "@[<h>%s@]" (String.escaped s)
+        | exception _ ->
+            Format.fprintf fs "@[<h>%a@]"
+              (IArray.pp ",@ " (ppx_t strength))
+              elts )
+      elts]
+
+let ppx_f strength fs fml =
+  let pp_t = ppx_t strength in
+  let rec pp fs fml =
+    let pf fmt = pp_boxed fs fmt in
+    match (fml : fml) with
+    | Tt -> pf "tt"
+    | Ff -> pf "ff"
+    | Eq (x, y) -> pf "(%a@ = %a)" pp_t x pp_t y
+    | Dq (x, y) -> pf "(%a@ @<2>≠ %a)" pp_t x pp_t y
+    | Lt (x, y) -> pf "(%a@ < %a)" pp_t x pp_t y
+    | Le (x, y) -> pf "(%a@ @<2>≤ %a)" pp_t x pp_t y
+    | Ord (x, y) -> pf "(%a@ ord %a)" pp_t x pp_t y
+    | Uno (x, y) -> pf "(%a@ uno %a)" pp_t x pp_t y
+    | Not x -> pf "¬%a" pp x
+    | And (x, y) -> pf "(%a@ @<2>∧ %a)" pp x pp y
+    | Or (x, y) -> pf "(%a@ @<2>∨ %a)" pp x pp y
+    | Iff (x, y) -> pf "(%a@ <=> %a)" pp x pp y
+    | Xor (x, y) -> pf "(%a@ xor %a)" pp x pp y
+    | Imp (x, y) -> pf "(%a@ => %a)" pp x pp y
+    | Cond {cnd; pos; neg} -> pf "(%a@ ? %a@ : %a)" pp cnd pp pos pp neg
+  in
+  pp fs fml
+
+let pp_f = ppx_f (fun _ -> None)
+
+let ppx_c strength fs ct =
+  let pp_t = ppx_t strength in
+  let pp_f = ppx_f strength in
+  let rec pp fs ct =
+    let pf fmt = pp_boxed fs fmt in
+    match ct with
+    | `Ite (cnd, thn, els) -> pf "(%a@ ? %a@ : %a)" pp_f cnd pp thn pp els
+    | `Trm t -> pp_t fs t
+  in
+  pp fs ct
+
+let ppx strength fs = function
+  | #cnd as c -> ppx_c strength fs c
+  | `Fml f -> ppx_f strength fs f
+
+let pp = ppx (fun _ -> None)
+
+(** fold_vars *)
+
+let rec fold_vars_t e ~init ~f =
+  match (e : trm) with
+  | Var _ as v -> f init (Var.of_ v)
+  | Z _ | Q _ | RecRecord _ | Label _ | Float _ -> init
+  | Neg x
+   |Mulq (_, x)
+   |Splat x
+   |Select (x, _)
+   |Signed (_, x)
+   |Unsigned (_, x)
+   |Convert {src= _; dst= _; arg= x} ->
+      fold_vars_t ~f x ~init
+  | Add (x, y)
+   |Sub (x, y)
+   |Mul (x, y)
+   |Div (x, y)
+   |Rem (x, y)
+   |Sized {seq= x; siz= y}
+   |Update (x, _, y)
+   |BAnd (x, y)
+   |BOr (x, y)
+   |BXor (x, y)
+   |BShl (x, y)
+   |BLshr (x, y)
+   |BAshr (x, y) ->
+      fold_vars_t ~f x ~init:(fold_vars_t ~f y ~init)
+  | Extract {seq= x; off= y; len= z} ->
+      fold_vars_t ~f x
+        ~init:(fold_vars_t ~f y ~init:(fold_vars_t ~f z ~init))
+  | Concat xs | Record xs ->
+      IArray.fold ~f:(fun init -> fold_vars_t ~f ~init) xs ~init
+
+let rec fold_vars_f ~init p ~f =
+  match (p : fml) with
+  | Tt | Ff -> init
+  | Eq (x, y) | Dq (x, y) | Lt (x, y) | Le (x, y) | Ord (x, y) | Uno (x, y)
+    ->
+      fold_vars_t ~f x ~init:(fold_vars_t ~f y ~init)
+  | Not x -> fold_vars_f ~f x ~init
+  | And (x, y) | Or (x, y) | Iff (x, y) | Xor (x, y) | Imp (x, y) ->
+      fold_vars_f ~f x ~init:(fold_vars_f ~f y ~init)
+  | Cond {cnd; pos; neg} ->
+      fold_vars_f ~f cnd
+        ~init:(fold_vars_f ~f pos ~init:(fold_vars_f ~f neg ~init))
+
+let rec fold_vars_c ~init ~f = function
+  | `Ite (cnd, thn, els) ->
+      fold_vars_f ~f cnd
+        ~init:(fold_vars_c ~f thn ~init:(fold_vars_c ~f els ~init))
+  | `Trm t -> fold_vars_t ~f t ~init
+
+let fold_vars ~init e ~f =
+  match e with
+  | `Fml p -> fold_vars_f ~f ~init p
+  | #cnd as c -> fold_vars_c ~f ~init c
+
+(** map_vars *)
+
+let map1 f e cons x =
+  let x' = f x in
+  if x == x' then e else cons x'
+
+let map2 f e cons x y =
+  let x' = f x in
+  let y' = f y in
+  if x == x' && y == y' then e else cons x' y'
+
+let map3 f e cons x y z =
+  let x' = f x in
+  let y' = f y in
+  let z' = f z in
+  if x == x' && y == y' && z == z' then e else cons x' y' z'
+
+let mapN f e cons xs =
+  let xs' = IArray.map_endo ~f xs in
+  if xs' == xs then e else cons xs'
+
+let rec map_vars_t ~f e =
+  match e with
+  | Var _ as v -> (f (Var.of_ v) : var :> trm)
+  | Z _ | Q _ -> e
+  | Neg x -> map1 (map_vars_t ~f) e _Neg x
+  | Add (x, y) -> map2 (map_vars_t ~f) e _Add x y
+  | Sub (x, y) -> map2 (map_vars_t ~f) e _Sub x y
+  | Mulq (q, x) -> map1 (map_vars_t ~f) e (_Mulq q) x
+  | Mul (x, y) -> map2 (map_vars_t ~f) e _Mul x y
+  | Div (x, y) -> map2 (map_vars_t ~f) e _Div x y
+  | Rem (x, y) -> map2 (map_vars_t ~f) e _Rem x y
+  | Splat x -> map1 (map_vars_t ~f) e _Splat x
+  | Sized {seq; siz} -> map2 (map_vars_t ~f) e _Sized seq siz
+  | Extract {seq; off; len} -> map3 (map_vars_t ~f) e _Extract seq off len
+  | Concat xs -> mapN (map_vars_t ~f) e _Concat xs
+  | Select (r, i) -> map1 (map_vars_t ~f) e (fun r -> _Select r i) r
+  | Update (r, i, e) ->
+      map2 (map_vars_t ~f) e (fun r e -> _Update r i e) r e
+  | Record xs -> mapN (map_vars_t ~f) e _Record xs
+  | RecRecord _ | Label _ | Float _ -> e
+  | BAnd (x, y) -> map2 (map_vars_t ~f) e _BAnd x y
+  | BOr (x, y) -> map2 (map_vars_t ~f) e _BOr x y
+  | BXor (x, y) -> map2 (map_vars_t ~f) e _BXor x y
+  | BShl (x, y) -> map2 (map_vars_t ~f) e _BShl x y
+  | BLshr (x, y) -> map2 (map_vars_t ~f) e _BLshr x y
+  | BAshr (x, y) -> map2 (map_vars_t ~f) e _BAshr x y
+  | Signed (n, x) -> map1 (map_vars_t ~f) e (_Signed n) x
+  | Unsigned (n, x) -> map1 (map_vars_t ~f) e (_Unsigned n) x
+  | Convert {src; dst; arg} -> map1 (map_vars_t ~f) e (_Convert src dst) arg
+
+let rec map_vars_f ~f e =
+  match e with
+  | Tt | Ff -> e
+  | Eq (x, y) -> map2 (map_vars_t ~f) e _Eq x y
+  | Dq (x, y) -> map2 (map_vars_t ~f) e _Dq x y
+  | Lt (x, y) -> map2 (map_vars_t ~f) e _Lt x y
+  | Le (x, y) -> map2 (map_vars_t ~f) e _Le x y
+  | Ord (x, y) -> map2 (map_vars_t ~f) e _Ord x y
+  | Uno (x, y) -> map2 (map_vars_t ~f) e _Uno x y
+  | Not x -> map1 (map_vars_f ~f) e _Not x
+  | And (x, y) -> map2 (map_vars_f ~f) e _And x y
+  | Or (x, y) -> map2 (map_vars_f ~f) e _Or x y
+  | Iff (x, y) -> map2 (map_vars_f ~f) e _Iff x y
+  | Xor (x, y) -> map2 (map_vars_f ~f) e _Xor x y
+  | Imp (x, y) -> map2 (map_vars_f ~f) e _Imp x y
+  | Cond {cnd; pos; neg} -> map3 (map_vars_f ~f) e _Cond cnd pos neg
+
+let rec map_vars_c ~f c =
+  match c with
+  | `Ite (cnd, thn, els) ->
+      let cnd' = map_vars_f ~f cnd in
+      let thn' = map_vars_c ~f thn in
+      let els' = map_vars_c ~f els in
+      if cnd' == cnd && thn' == thn && els' == els then c
+      else `Ite (cnd', thn', els')
+  | `Trm t ->
+      let t' = map_vars_t ~f t in
+      if t' == t then c else `Trm t'
+
+let map_vars ~f = function
+  | `Fml p -> `Fml (map_vars_f ~f p)
+  | #cnd as c -> (map_vars_c ~f c :> exp)
+
+(*
+ * Core construction functions
+ *
+ * Support functions for constructing expressions as if terms and formulas
+ * could be freely mixed, instead of being strictly partitioned into terms
+ * and formulas stratified below conditional terms and then expressions.
+ *)
+
+let zero = Z Z.zero
+let one = Z Z.one
+
+(** Map a unary function on terms over the leaves of a conditional term,
+    rebuilding the tree of conditionals with the supplied ite construction
+    function. *)
+let rec map_cnd : (fml -> 'a -> 'a -> 'a) -> (trm -> 'a) -> cnd -> 'a =
+ fun f_ite f_trm -> function
+  | `Trm trm -> f_trm trm
+  | `Ite (cnd, thn, els) ->
+      let thn' = map_cnd f_ite f_trm thn in
+      let els' = map_cnd f_ite f_trm els in
+      f_ite cnd thn' els'
+
+(** Embed a formula into a conditional term (associating true with 1 and
+    false with 0), identity on conditional terms. *)
+let embed_into_cnd : exp -> cnd = function
+  | #cnd as c -> c
+  (* p ==> (p ? 1 : 0) *)
+  | `Fml fml -> `Ite (fml, `Trm one, `Trm zero)
+
+(** Project out a formula that is embedded into a conditional term.
+
+    - [project_out_fml] is left inverse to [embed_into_cnd] in the sense
+      that [project_out_fml (embed_into_cnd (`Fml f)) = Some f]. *)
+let project_out_fml : cnd -> fml option = function
+  (* (p ? 1 : 0) ==> p *)
+  | `Ite (cnd, `Trm one', `Trm zero') when one == one' && zero == zero' ->
+      Some cnd
+  | _ -> None
+
+(** Embed a conditional term into a formula (associating 0 with false and
+    non-0 with true, lifted over the tree mapping conditional terms to
+    conditional formulas), identity on formulas.
+
+    - [embed_into_fml] is left inverse to [embed_into_cnd] in the sense that
+      [embed_into_fml ((embed_into_cnd (`Fml f)) :> exp) = f].
+    - [embed_into_fml] is not right inverse to [embed_into_cnd] since
+      [embed_into_fml] can only preserve one bit of information from its
+      argument. So in general
+      [(embed_into_cnd (`Fml (embed_into_fml x)) :> exp)] is not equivalent
+      to [x].
+    - The weaker condition that
+      [0 ≠ (embed_into_cnd (`Fml (embed_into_fml x)) :> exp)] iff
+      [0 ≠ x] holds. *)
+let embed_into_fml : exp -> fml = function
+  | `Fml fml -> fml
+  | #cnd as c ->
+      (* Some normalization is necessary for [embed_into_fml] to be left
+         inverse to [embed_into_cnd]. Essentially [0 ≠ (p ? 1 : 0)] needs to
+         normalize to [p], by way of [0 ≠ (p ? 1 : 0)] ==> [(p ? 0 ≠ 1 : 0 ≠
+         0)] ==> [(p ? tt : ff)] ==> [p]. *)
+      let dq0 : trm -> fml = function
+        (* 0 ≠ 0 ==> ff *)
+        | Z _ as z when z == zero -> Ff
+        (* 0 ≠ N ==> tt for N≠0 *)
+        | Z _ -> Tt
+        | t -> Dq (zero, t)
+      in
+      let cond : fml -> fml -> fml -> fml =
+       fun cnd pos neg ->
+        match (pos, neg) with
+        (* (p ? tt : ff) ==> p *)
+        | Tt, Ff -> cnd
+        | _ -> Cond {cnd; pos; neg}
+      in
+      map_cnd cond dq0 c
+
+(** Construct a conditional term, or formula if possible precisely. *)
+let ite : fml -> exp -> exp -> exp =
+ fun cnd thn els ->
+  match (thn, els) with
+  | `Fml pos, `Fml neg -> `Fml (Cond {cnd; pos; neg})
+  | _ -> (
+      let c = `Ite (cnd, embed_into_cnd thn, embed_into_cnd els) in
+      match project_out_fml c with Some f -> `Fml f | None -> c )
+
+(** Map a unary function on terms over an expression. *)
+let ap1 : (trm -> exp) -> exp -> exp =
+ fun f x -> map_cnd ite f (embed_into_cnd x)
+
+let ap1t : (trm -> trm) -> exp -> exp = fun f -> ap1 (fun x -> `Trm (f x))
+
+(** Map a binary function on terms over conditional terms. This yields a
+    conditional tree with the structure from the first argument where each
+    leaf has been replaced by a conditional tree with the structure from the
+    second argument where each leaf has been replaced by the application of
+    the argument binary function to the corresponding leaves from the first
+    and second argument. *)
+let map2_cnd :
+    (fml -> 'a -> 'a -> 'a) -> (trm -> trm -> 'a) -> cnd -> cnd -> 'a =
+ fun f_ite f_trm x y ->
+  map_cnd f_ite (fun x' -> map_cnd f_ite (fun y' -> f_trm x' y') y) x
+
+(** Map a binary function on terms over expressions. *)
+let ap2 : (trm -> trm -> exp) -> exp -> exp -> exp =
+ fun f x y -> map2_cnd ite f (embed_into_cnd x) (embed_into_cnd y)
+
+let ap2t : (trm -> trm -> trm) -> exp -> exp -> exp =
+ fun f -> ap2 (fun x y -> `Trm (f x y))
+
+let ap2f : (trm -> trm -> fml) -> exp -> exp -> fml =
+ fun f x y -> map2_cnd _Cond f (embed_into_cnd x) (embed_into_cnd y)
+
+(** Map a ternary function on terms over conditional terms. *)
+let map3_cnd :
+       (fml -> 'a -> 'a -> 'a)
+    -> (trm -> trm -> trm -> 'a)
+    -> cnd
+    -> cnd
+    -> cnd
+    -> 'a =
+ fun f_ite f_trm x y z ->
+  map_cnd f_ite
+    (fun x' ->
+      map_cnd f_ite (fun y' -> map_cnd f_ite (fun z' -> f_trm x' y' z') z) y
+      )
+    x
+
+(** Map a ternary function on terms over expressions. *)
+let ap3 : (trm -> trm -> trm -> exp) -> exp -> exp -> exp -> exp =
+ fun f x y z ->
+  map3_cnd ite f (embed_into_cnd x) (embed_into_cnd y) (embed_into_cnd z)
+
+let ap3t : (trm -> trm -> trm -> trm) -> exp -> exp -> exp -> exp =
+ fun f -> ap3 (fun x y z -> `Trm (f x y z))
+
+(** Reverse-map an nary function on terms over conditional terms. *)
+let rev_mapN_cnd :
+    (fml -> 'a -> 'a -> 'a) -> (trm list -> 'a) -> cnd list -> 'a =
+ fun f_ite f_trms rev_xs ->
+  let rec loop xs' = function
+    | x :: xs -> map_cnd f_ite (fun x' -> loop (x' :: xs') xs) x
+    | [] -> f_trms xs'
+  in
+  loop [] rev_xs
+
+(** Map an nary function on terms over expressions. *)
+let apNt : (trm list -> trm) -> exp array -> exp =
+ fun f xs ->
+  rev_mapN_cnd ite
+    (fun xs -> `Trm (f xs))
+    (Array.fold ~f:(fun xs x -> embed_into_cnd x :: xs) ~init:[] xs)
+
+(*
+ * Formulas: exposed interface
+ *)
 
 module Formula = struct
-  include Term
+  type t = fml [@@deriving compare, equal, sexp]
 
-  let inject b = b
-  let project e = Some e
-  let tt = true_
-  let ff = false_
-  let cond ~cnd ~pos ~neg = conditional ~cnd ~thn:pos ~els:neg
+  let inject f = `Fml f
+  let project = function `Fml f -> Some f | #cnd as c -> project_out_fml c
+  let ppx = ppx_f
+  let pp = pp_f
+
+  (* constants *)
+
+  let tt = Tt
+  let ff = Ff
+
+  (* comparisons *)
+
+  let eq = ap2f _Eq
+  let dq = ap2f _Dq
+  let lt = ap2f _Lt
+  let le = ap2f _Le
+  let ord = ap2f _Ord
+  let uno = ap2f _Uno
+
+  (* connectives *)
+
+  let not_ = _Not
+  let and_ = _And
+  let or_ = _Or
+  let iff = _Iff
+  let xor = _Xor
+  let imp = _Imp
+  let nimp x y = not_ (imp x y)
+  let cond ~cnd ~pos ~neg = _Cond cnd pos neg
+
+  (** Query *)
+
+  let fv e = fold_vars_f e ~f:Var.Set.add ~init:Var.Set.empty
+  let is_true = function Tt -> true | _ -> false
+  let is_false = function Ff -> true | _ -> false
+
+  (** Traverse *)
+
+  let fold_vars = fold_vars_f
+
+  (** Transform *)
+
+  let map_vars = map_vars_f
+
+  let fold_map_vars ~init e ~f =
+    let s = ref init in
+    let f x =
+      let s', x' = f !s x in
+      s := s' ;
+      x'
+    in
+    let e' = map_vars ~f e in
+    (!s, e')
+
+  let rename s e = map_vars ~f:(Var.Subst.apply s) e
+
+  let disjuncts p =
+    let rec disjuncts_ p ds =
+      match p with
+      | Or (a, b) -> disjuncts_ a (disjuncts_ b ds)
+      | Cond {cnd; pos; neg} ->
+          disjuncts_ (And (cnd, pos)) (disjuncts_ (And (Not cnd, neg)) ds)
+      | d -> d :: ds
+    in
+    disjuncts_ p []
+end
+
+(*
+ * Terms: exposed interface
+ *)
+
+module Term = struct
+  (* Exposed terms are represented as expressions, which allow formulas to
+     appear at toplevel, although semantically these are redundant with
+     their [inject]ion into [trm] proper. This redundancy of representation
+     is allowed in order to avoid churning formulas back and forth between
+     [fml] and [cnd] via [inject] and [project] in cases where formulas only
+     transiently pass through term contexts. The construction functions will
+     convert such a formula [p] into [(p ? 1 : 0)] as soon as it is used as
+     a subterm, so this redundancy is only lazily delaying normalization by
+     one step. *)
+  module T = struct
+    type t = exp [@@deriving compare, equal, sexp]
+  end
+
+  include T
+  module Map = Map.Make (T)
+
+  let ppx = ppx
+  let pp = pp
+
+  (* variables *)
+
+  let var v = `Trm (v : var :> trm)
+
+  (* constants *)
+
+  let zero = `Trm zero
+  let one = `Trm one
+
+  let integer z =
+    if Z.equal Z.zero z then zero
+    else if Z.equal Z.one z then one
+    else `Trm (Z z)
+
+  let rational q = `Trm (Q q)
+
+  let float s =
+    match Q.of_float (Float.of_string s) with
+    | q when Q.is_real q -> rational q
+    | _ | (exception Invalid_argument _) -> `Trm (Float s)
+
+  let label ~parent ~name = `Trm (Label {parent; name})
+
+  (* arithmetic *)
+
+  let neg = ap1t _Neg
+  let add = ap2t _Add
+  let sub = ap2t _Sub
+  let mulq q = ap1t (_Mulq q)
+
+  let mul =
+    ap2 (fun x y ->
+        match x with
+        | Z z -> mulq (Q.of_z z) (`Trm y)
+        | Q q -> mulq q (`Trm y)
+        | _ -> (
+          match y with
+          | Z z -> mulq (Q.of_z z) (`Trm x)
+          | Q q -> mulq q (`Trm x)
+          | _ -> ap2t _Mul (`Trm x) (`Trm y) ) )
+
+  let div = ap2t _Div
+  let rem = ap2t _Rem
+
+  (* sequences *)
+
+  let splat = ap1t _Splat
+  let sized ~seq ~siz = ap2t _Sized seq siz
+  let extract ~seq ~off ~len = ap3t _Extract seq off len
+  let concat elts = apNt (fun es -> _Concat (IArray.of_list es)) elts
+
+  (* records *)
+
+  let select ~rcd ~idx = ap1t (fun r -> _Select r idx) rcd
+  let update ~rcd ~idx ~elt = ap2t (fun r e -> _Update r idx e) rcd elt
+  let record elts = apNt (fun es -> _Record (IArray.of_list es)) elts
+  let rec_record i = `Trm (_RecRecord i)
+
+  (* bitwise *)
+
+  let band = ap2t _BAnd
+  let bor = ap2t _BOr
+  let bxor = ap2t _BXor
+  let bshl = ap2t _BShl
+  let blshr = ap2t _BLshr
+  let bashr = ap2t _BAshr
+
+  (* type conversions *)
+
+  let signed bits = function
+    | `Fml _ as fml when bits = 1 -> fml
+    | arg -> ap1t (_Signed bits) arg
+
+  let unsigned bits = function
+    | `Fml _ as fml when bits = 1 -> fml
+    | arg -> ap1t (_Unsigned bits) arg
+
+  let convert src ~to_:dst arg = ap1t (_Convert src dst) arg
+
+  (* if-then-else *)
+
+  let ite ~cnd ~thn ~els = ite cnd thn els
+
+  (** Destruct *)
+
+  let d_int = function `Trm (Z z) -> Some z | _ -> None
+
+  (** Access *)
+
+  let const_of x =
+    let rec const_of t =
+      let add = Option.map2 ~f:Q.add in
+      let neg = Option.map ~f:Q.neg in
+      match t with
+      | Z z -> Some (Q.of_z z)
+      | Q q -> Some q
+      | Add (x, y) -> add (const_of x) (const_of y)
+      | Sub (x, y) -> add (const_of x) (neg (const_of y))
+      | _ -> None
+    in
+    match x with `Trm t -> const_of t | _ -> None
+
+  (** Traverse *)
+
+  let fold_vars = fold_vars
+
+  (** Transform *)
+
+  let map_vars = map_vars
+
+  let fold_map_vars e ~init ~f =
+    let s = ref init in
+    let f x =
+      let s', x' = f !s x in
+      s := s' ;
+      x'
+    in
+    let e' = map_vars ~f e in
+    (!s, e')
+
+  let rename s e = map_vars ~f:(Var.Subst.apply s) e
+
+  (** Query *)
+
+  let fv e = fold_vars e ~f:Var.Set.add ~init:Var.Set.empty
 end
 
+(*
+ * Convert to Ses
+ *)
+
+let v_to_ses : var -> Ses.Var.t =
+ fun v -> Ses.Var.identified ~id:(Var.id v) ~name:(Var.name v)
+
+let vs_to_ses : Var.Set.t -> Ses.Var.Set.t =
+ fun vs ->
+  Var.Set.fold vs ~init:Ses.Var.Set.empty ~f:(fun vs v ->
+      Ses.Var.Set.add vs (v_to_ses v) )
+
+let rec t_to_ses : trm -> Ses.Term.t = function
+  | Var {name; id} -> Ses.Term.var (Ses.Var.identified ~name ~id)
+  | Z z -> Ses.Term.integer z
+  | Q q -> Ses.Term.rational q
+  | Neg x -> Ses.Term.neg (t_to_ses x)
+  | Add (x, y) -> Ses.Term.add (t_to_ses x) (t_to_ses y)
+  | Sub (x, y) -> Ses.Term.sub (t_to_ses x) (t_to_ses y)
+  | Mulq (q, x) -> Ses.Term.mulq q (t_to_ses x)
+  | Mul (x, y) -> Ses.Term.mul (t_to_ses x) (t_to_ses y)
+  | Div (x, y) -> Ses.Term.div (t_to_ses x) (t_to_ses y)
+  | Rem (x, y) -> Ses.Term.rem (t_to_ses x) (t_to_ses y)
+  | Select (r, i) -> Ses.Term.select ~rcd:(t_to_ses r) ~idx:i
+  | Update (r, i, e) ->
+      Ses.Term.update ~rcd:(t_to_ses r) ~idx:i ~elt:(t_to_ses e)
+  | Record es -> Ses.Term.record (IArray.map ~f:t_to_ses es)
+  | RecRecord i -> Ses.Term.rec_record i
+  | Splat x -> Ses.Term.splat (t_to_ses x)
+  | Sized {seq; siz} ->
+      Ses.Term.sized ~seq:(t_to_ses seq) ~siz:(t_to_ses siz)
+  | Extract {seq; off; len} ->
+      Ses.Term.extract ~seq:(t_to_ses seq) ~off:(t_to_ses off)
+        ~len:(t_to_ses len)
+  | Concat es ->
+      Ses.Term.concat (IArray.to_array (IArray.map ~f:t_to_ses es))
+  | BAnd (x, y) -> Ses.Term.and_ (t_to_ses x) (t_to_ses y)
+  | BOr (x, y) -> Ses.Term.or_ (t_to_ses x) (t_to_ses y)
+  | BXor (x, y) -> Ses.Term.dq (t_to_ses x) (t_to_ses y)
+  | BShl (x, y) -> Ses.Term.shl (t_to_ses x) (t_to_ses y)
+  | BLshr (x, y) -> Ses.Term.lshr (t_to_ses x) (t_to_ses y)
+  | BAshr (x, y) -> Ses.Term.ashr (t_to_ses x) (t_to_ses y)
+  | Label {parent; name} -> Ses.Term.label ~parent ~name
+  | Float s -> Ses.Term.float s
+  | Signed (n, x) -> Ses.Term.signed n (t_to_ses x)
+  | Unsigned (n, x) -> Ses.Term.unsigned n (t_to_ses x)
+  | Convert {src; dst; arg} -> Ses.Term.convert src ~to_:dst (t_to_ses arg)
+
+let rec f_to_ses : fml -> Ses.Term.t = function
+  | Tt -> Ses.Term.true_
+  | Ff -> Ses.Term.false_
+  | Eq (x, y) -> Ses.Term.eq (t_to_ses x) (t_to_ses y)
+  | Dq (x, y) -> Ses.Term.dq (t_to_ses x) (t_to_ses y)
+  | Lt (x, y) -> Ses.Term.lt (t_to_ses x) (t_to_ses y)
+  | Le (x, y) -> Ses.Term.le (t_to_ses x) (t_to_ses y)
+  | Ord (x, y) -> Ses.Term.ord (t_to_ses x) (t_to_ses y)
+  | Uno (x, y) -> Ses.Term.uno (t_to_ses x) (t_to_ses y)
+  | Not p -> Ses.Term.not_ (f_to_ses p)
+  | And (p, q) -> Ses.Term.and_ (f_to_ses p) (f_to_ses q)
+  | Or (p, q) -> Ses.Term.or_ (f_to_ses p) (f_to_ses q)
+  | Iff (p, q) -> Ses.Term.eq (f_to_ses p) (f_to_ses q)
+  | Xor (p, q) -> Ses.Term.dq (f_to_ses p) (f_to_ses q)
+  | Imp (p, q) -> Ses.Term.le (f_to_ses p) (f_to_ses q)
+  | Cond {cnd; pos; neg} ->
+      Ses.Term.conditional ~cnd:(f_to_ses cnd) ~thn:(f_to_ses pos)
+        ~els:(f_to_ses neg)
+
+let rec to_ses : exp -> Ses.Term.t = function
+  | `Ite (cnd, thn, els) ->
+      Ses.Term.conditional ~cnd:(f_to_ses cnd)
+        ~thn:(to_ses (thn :> exp))
+        ~els:(to_ses (els :> exp))
+  | `Trm t -> t_to_ses t
+  | `Fml f -> f_to_ses f
+
+(*
+ * Convert from Ses
+ *)
+
+let v_of_ses : Ses.Var.t -> var =
+ fun v -> Var.identified ~id:(Ses.Var.id v) ~name:(Ses.Var.name v)
+
+let vs_of_ses : Ses.Var.Set.t -> Var.Set.t =
+ fun vs ->
+  Ses.Var.Set.fold vs ~init:Var.Set.empty ~f:(fun vs v ->
+      Var.Set.add vs (v_of_ses v) )
+
+let rec ap_tt f a = f (of_ses a)
+and ap_ttt f a b = f (of_ses a) (of_ses b)
+and ap_ttf f a b = `Fml (f (of_ses a) (of_ses b))
+
+and ap2 mk_f mk_t a b =
+  match (of_ses a, of_ses b) with
+  | `Fml p, `Fml q -> `Fml (mk_f p q)
+  | x, y -> mk_t x y
+
+and ap2_f mk_f mk_t a b = ap2 mk_f (fun x y -> `Fml (mk_t x y)) a b
+
+and apN mk_f mk_t mk_unit es =
+  match
+    Ses.Term.Set.fold ~init:(None, None) es ~f:(fun (fs, ts) e ->
+        match of_ses e with
+        | `Fml f ->
+            (Some (match fs with None -> f | Some g -> mk_f f g), ts)
+        | t -> (fs, Some (match ts with None -> t | Some u -> mk_t t u)) )
+  with
+  | Some f, Some t -> mk_t t (Formula.inject f)
+  | Some f, None -> `Fml f
+  | None, Some t -> t
+  | None, None -> `Fml mk_unit
+
+and of_ses : Ses.Term.t -> exp =
+ fun t ->
+  let open Term in
+  let open Formula in
+  match t with
+  | Var {id; name} -> var (Var.identified ~id ~name)
+  | Integer {data} -> integer data
+  | Rational {data} -> rational data
+  | Float {data} -> float data
+  | Label {parent; name} -> label ~parent ~name
+  | Ap1 (Signed {bits}, e) -> ap_tt (signed bits) e
+  | Ap1 (Unsigned {bits}, e) -> ap_tt (unsigned bits) e
+  | Ap1 (Convert {src; dst}, e) -> ap_tt (convert src ~to_:dst) e
+  | Ap2 (Eq, d, e) -> ap2_f iff eq d e
+  | Ap2 (Dq, d, e) -> ap2_f xor dq d e
+  | Ap2 (Lt, d, e) -> ap2_f (Fn.flip nimp) lt d e
+  | Ap2 (Le, d, e) -> ap2_f imp le d e
+  | Ap2 (Ord, d, e) -> ap_ttf ord d e
+  | Ap2 (Uno, d, e) -> ap_ttf uno d e
+  | Add sum -> (
+    match Ses.Term.Qset.pop_min_elt sum with
+    | None -> zero
+    | Some (e, q, sum) ->
+        let mul e q = mulq q (of_ses e) in
+        Ses.Term.Qset.fold sum ~init:(mul e q) ~f:(fun e q s ->
+            add (mul e q) s ) )
+  | Mul prod -> (
+    match Ses.Term.Qset.pop_min_elt prod with
+    | None -> one
+    | Some (e, q, prod) ->
+        let rec expn e n =
+          if Z.sign n = 0 then one else mul e (expn e (Z.pred n))
+        in
+        let exp e q =
+          let n = Q.num q in
+          if Z.sign n >= 0 then expn (of_ses e) n
+          else div one (expn (of_ses e) (Z.neg n))
+        in
+        Ses.Term.Qset.fold prod ~init:(exp e q) ~f:(fun e q s ->
+            mul (exp e q) s ) )
+  | Ap2 (Div, d, e) -> ap_ttt div d e
+  | Ap2 (Rem, d, e) -> ap_ttt rem d e
+  | And es -> apN and_ band tt es
+  | Or es -> apN or_ bor ff es
+  | Ap2 (Xor, d, e) -> ap2 xor bxor d e
+  | Ap2 (Shl, d, e) -> ap_ttt bshl d e
+  | Ap2 (Lshr, d, e) -> ap_ttt blshr d e
+  | Ap2 (Ashr, d, e) -> ap_ttt bashr d e
+  | Ap3 (Conditional, cnd, thn, els) -> (
+      let cnd = embed_into_fml (of_ses cnd) in
+      match (of_ses thn, of_ses els) with
+      | `Fml pos, `Fml neg -> `Fml (cond ~cnd ~pos ~neg)
+      | thn, els -> ite ~cnd ~thn ~els )
+  | Ap1 (Splat, byt) -> splat (of_ses byt)
+  | Ap3 (Extract, seq, off, len) ->
+      extract ~seq:(of_ses seq) ~off:(of_ses off) ~len:(of_ses len)
+  | Ap2 (Sized, siz, seq) -> sized ~seq:(of_ses seq) ~siz:(of_ses siz)
+  | ApN (Concat, args) ->
+      concat (IArray.to_array (IArray.map ~f:of_ses args))
+  | Ap1 (Select idx, rcd) -> select ~rcd:(of_ses rcd) ~idx
+  | Ap2 (Update idx, rcd, elt) ->
+      update ~rcd:(of_ses rcd) ~idx ~elt:(of_ses elt)
+  | ApN (Record, elts) ->
+      record (IArray.to_array (IArray.map ~f:of_ses elts))
+  | RecRecord i -> rec_record i
+
+let f_of_ses e = embed_into_fml (of_ses e)
+
+let v_map_ses : (var -> var) -> Ses.Var.t -> Ses.Var.t =
+ fun f x ->
+  let v = v_of_ses x in
+  let v' = f v in
+  if v' == v then x else v_to_ses v'
+
+let ses_map : (Ses.Term.t -> Ses.Term.t) -> exp -> exp =
+ fun f x ->
+  let e = to_ses x in
+  let e' = f e in
+  if e' == e then x else of_ses e'
+
+let f_ses_map : (Ses.Term.t -> Ses.Term.t) -> fml -> fml =
+ fun f x ->
+  let e = f_to_ses x in
+  let e' = f e in
+  if e' == e then x else f_of_ses e'
+
+(*
+ * Contexts
+ *)
+
 module Context = struct
-  include Ses.Equality
+  type t = Ses.Equality.t [@@deriving compare, equal, sexp]
+  type classes = exp list Term.Map.t
+
+  let classes_of_ses clss =
+    Ses.Term.Map.fold clss ~init:Term.Map.empty
+      ~f:(fun ~key:rep ~data:cls clss ->
+        let rep' = of_ses rep in
+        let cls' = List.map ~f:of_ses cls in
+        Term.Map.set ~key:rep' ~data:cls' clss )
+
+  let classes_to_ses clss =
+    Term.Map.fold clss ~init:Ses.Term.Map.empty
+      ~f:(fun ~key:rep ~data:cls clss ->
+        let rep' = to_ses rep in
+        let cls' = List.map ~f:to_ses cls in
+        Ses.Term.Map.set ~key:rep' ~data:cls' clss )
+
+  let classes x = classes_of_ses (Ses.Equality.classes x)
+  let diff_classes x y = classes_of_ses (Ses.Equality.diff_classes x y)
+  let pp = Ses.Equality.pp
+  let pp_classes = Ses.Equality.pp_classes
+
+  let ppx_classes x fs clss =
+    Ses.Equality.ppx_classes
+      (fun v -> x (v_of_ses v))
+      fs (classes_to_ses clss)
+
+  let invariant = Ses.Equality.invariant
+  let true_ = Ses.Equality.true_
+
+  let and_formula vs f x =
+    let vs', x' = Ses.Equality.and_term (vs_to_ses vs) (f_to_ses f) x in
+    (vs_of_ses vs', x')
+
+  let and_ vs x y =
+    let vs', z = Ses.Equality.and_ (vs_to_ses vs) x y in
+    (vs_of_ses vs', z)
 
-  let and_formula = and_term
-  let normalizef = normalize
-  let rename x sub = rename x (Var.Subst.apply sub)
+  let orN vs xs =
+    let vs', z = Ses.Equality.orN (vs_to_ses vs) xs in
+    (vs_of_ses vs', z)
+
+  let rename x sub = Ses.Equality.rename x (v_map_ses (Var.Subst.apply sub))
+  let fv x = vs_of_ses (Ses.Equality.fv x)
+  let is_true x = Ses.Equality.is_true x
+  let is_false x = Ses.Equality.is_false x
+  let entails_eq x e f = Ses.Equality.entails_eq x (to_ses e) (to_ses f)
+  let class_of x e = List.map ~f:of_ses (Ses.Equality.class_of x (to_ses e))
+  let normalize x e = ses_map (Ses.Equality.normalize x) e
+  let normalizef x e = f_ses_map (Ses.Equality.normalize x) e
+  let difference x e f = Ses.Equality.difference x (to_ses e) (to_ses f)
+
+  let fold_terms ~init x ~f =
+    Ses.Equality.fold_terms x ~init ~f:(fun s e -> f s (of_ses e))
 
   module Subst = struct
-    include Subst
+    type t = Ses.Equality.Subst.t [@@deriving sexp]
+
+    let pp = Ses.Equality.Subst.pp
+    let is_empty = Ses.Equality.Subst.is_empty
+
+    let fold s ~init ~f =
+      Ses.Equality.Subst.fold s ~init ~f:(fun ~key ~data ->
+          f ~key:(of_ses key) ~data:(of_ses data) )
 
-    let substf = subst
+    let subst s = ses_map (Ses.Equality.Subst.subst s)
+    let substf s = f_ses_map (Ses.Equality.Subst.subst s)
+
+    let partition_valid vs s =
+      let t, ks, u = Ses.Equality.Subst.partition_valid (vs_to_ses vs) s in
+      (t, vs_of_ses ks, u)
   end
 
+  let apply_subst vs s x =
+    let vs', x' = Ses.Equality.apply_subst (vs_to_ses vs) s x in
+    (vs_of_ses vs', x')
+
+  let solve_for_vars vss x =
+    Ses.Equality.solve_for_vars (List.map ~f:vs_to_ses vss) x
+
+  let elim vs x = Ses.Equality.elim (vs_to_ses vs) x
+
   (* Replay debugging *)
 
   type call =
-    | Normalize of t * Term.t
-    | And_formula of Var.Set.t * Formula.t * t
+    | Normalize of t * exp
+    | Normalizef of t * fml
+    | And_formula of Var.Set.t * fml * t
     | And_ of Var.Set.t * t * t
     | OrN of Var.Set.t * t list
     | Rename of t * Var.Subst.t
@@ -129,6 +1271,7 @@ module Context = struct
   let replay c =
     match call_of_sexp (Sexp.of_string c) with
     | Normalize (r, e) -> normalize r e |> ignore
+    | Normalizef (r, e) -> normalizef r e |> ignore
     | And_formula (us, e, r) -> and_formula us e r |> ignore
     | And_ (us, r, s) -> and_ us r s |> ignore
     | OrN (us, rs) -> orN us rs |> ignore
@@ -171,6 +1314,11 @@ module Context = struct
   let normalize r e =
     wrap normalize_tmr (fun () -> normalize r e) (fun () -> Normalize (r, e))
 
+  let normalizef r e =
+    wrap normalize_tmr
+      (fun () -> normalizef r e)
+      (fun () -> Normalizef (r, e))
+
   let and_formula us e r =
     wrap and_formula_tmr
       (fun () -> and_formula us e r)
@@ -200,14 +1348,102 @@ end
  *)
 
 module Term_of_Llair = struct
-  let exp = Ses.Term.of_exp
+  let rec uap_ttt : 'a. (exp -> exp -> 'a) -> _ -> _ -> _ -> 'a =
+   fun f typ a b ->
+    let bits = Llair.Typ.bit_size_of typ in
+    f (Term.unsigned bits (exp a)) (Term.unsigned bits (exp b))
+
+  and uap_ttf (f : exp -> exp -> fml) typ a b = `Fml (uap_ttt f typ a b)
+  and ap_tt : 'a. (exp -> 'a) -> _ -> 'a = fun f a -> f (exp a)
+  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} -> label ~parent ~name
+    | Integer {typ= _; data} -> integer data
+    | Float {data; typ= _} -> float data
+    | Ap1 (Signed {bits}, _, e) -> ap_tt (signed bits) e
+    | Ap1 (Unsigned {bits}, _, e) -> ap_tt (unsigned bits) e
+    | Ap1 (Convert {src}, dst, e) -> ap_tt (convert src ~to_:dst) e
+    | Ap2 (Eq, Integer {bits= 1; _}, d, e) -> ap_fff iff d e
+    | Ap2 (Dq, Integer {bits= 1; _}, d, e) -> ap_fff xor d e
+    | Ap2 ((Gt | Ugt), Integer {bits= 1; _}, d, e) -> ap_fff nimp d e
+    | Ap2 ((Lt | Ult), Integer {bits= 1; _}, d, e) -> ap_fff nimp e d
+    | Ap2 ((Ge | Uge), Integer {bits= 1; _}, d, e) -> ap_fff imp e d
+    | Ap2 ((Le | Ule), Integer {bits= 1; _}, d, e) -> ap_fff imp d e
+    | Ap2 (Eq, _, d, e) -> ap_ttf eq d e
+    | Ap2 (Dq, _, d, e) -> ap_ttf dq d e
+    | Ap2 (Gt, _, d, e) -> ap_ttf lt e d
+    | Ap2 (Lt, _, d, e) -> ap_ttf lt d e
+    | Ap2 (Ge, _, d, e) -> ap_ttf le e d
+    | Ap2 (Le, _, d, e) -> ap_ttf le d e
+    | Ap2 (Ugt, typ, d, e) -> uap_ttf lt typ e d
+    | Ap2 (Ult, typ, d, e) -> uap_ttf lt typ d e
+    | Ap2 (Uge, typ, d, e) -> uap_ttf le typ e d
+    | Ap2 (Ule, typ, d, e) -> uap_ttf le typ d e
+    | Ap2 (Ord, _, d, e) -> ap_ttf ord d e
+    | Ap2 (Uno, _, d, e) -> ap_ttf uno d e
+    | Ap2 (Add, Integer {bits= 1; _}, d, e) -> ap_fff xor d e
+    | Ap2 (Sub, Integer {bits= 1; _}, d, e) -> ap_fff xor d e
+    | Ap2 (Mul, Integer {bits= 1; _}, d, e) -> ap_fff and_ d e
+    | 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) -> ap_ttt div d e
+    | Ap2 (Rem, _, d, e) -> ap_ttt rem d e
+    | Ap2 (Udiv, typ, d, e) -> uap_ttt div typ d e
+    | Ap2 (Urem, typ, d, e) -> uap_ttt rem typ d e
+    | Ap2 (And, Integer {bits= 1; _}, d, e) -> ap_fff and_ d e
+    | Ap2 (Or, Integer {bits= 1; _}, d, e) -> ap_fff or_ d e
+    | Ap2 (Xor, Integer {bits= 1; _}, d, e) -> ap_fff xor d e
+    | Ap2 (And, _, d, e) -> ap_ttt band d e
+    | Ap2 (Or, _, d, e) -> ap_ttt bor d e
+    | Ap2 (Xor, _, d, e) -> ap_ttt bxor d e
+    | Ap2 (Shl, _, d, e) -> ap_ttt bshl d e
+    | Ap2 (Lshr, _, d, e) -> ap_ttt blshr d e
+    | Ap2 (Ashr, _, d, e) -> ap_ttt bashr 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 (IArray.to_array (IArray.map ~f:exp elts))
+    | RecRecord (i, _) -> rec_record i
+    | Ap1 (Splat, _, byt) -> splat (exp byt)
 end
 
 module Formula_of_Llair = struct
-  let exp = Term_of_Llair.exp
+  let exp e = embed_into_fml (Term_of_Llair.exp e)
 end
 
 module Var_of_Llair = struct
-  let reg = Ses.Var.of_reg
-  let regs = Ses.Var.Set.of_regs
+  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 4faa286e2..ba03fa3e5 100644
--- a/sledge/src/fol.mli
+++ b/sledge/src/fol.mli
@@ -10,6 +10,7 @@ module Var : sig
   type t [@@deriving compare, equal, sexp]
   type strength = t -> [`Universal | `Existential | `Anonymous] option
 
+  val ppx : strength -> t pp
   val pp : t pp
 
   module Map : Map.S with type key := t
@@ -98,17 +99,22 @@ module rec Term : sig
 
   val const_of : t -> Q.t option
 
-  (** Transform *)
+  (** Query *)
 
-  val rename : Var.Subst.t -> t -> t
+  val fv : t -> Var.Set.t
 
   (** Traverse *)
 
-  val fold_vars : t -> init:'a -> f:('a -> Var.t -> 'a) -> 'a
+  val fold_vars : init:'a -> t -> f:('a -> Var.t -> 'a) -> 'a
 
-  (** Query *)
+  (** Transform *)
 
-  val fv : t -> Var.Set.t
+  val map_vars : f:(Var.t -> Var.t) -> t -> t
+
+  val fold_map_vars :
+    t -> init:'a -> f:('a -> Var.t -> 'a * Var.t) -> 'a * t
+
+  val rename : Var.Subst.t -> t -> t
 end
 
 (** Formulas *)
@@ -140,16 +146,25 @@ and Formula : sig
   val or_ : t -> t -> t
   val cond : cnd:t -> pos:t -> neg:t -> t
 
-  (** Transform *)
-
-  val rename : Var.Subst.t -> t -> t
-  val disjuncts : t -> t list
-
   (** Query *)
 
+  val fv : t -> Var.Set.t
   val is_true : t -> bool
   val is_false : t -> bool
-  val fv : t -> Var.Set.t
+
+  (** Traverse *)
+
+  val fold_vars : init:'a -> t -> f:('a -> Var.t -> 'a) -> 'a
+
+  (** Transform *)
+
+  val map_vars : f:(Var.t -> Var.t) -> t -> t
+
+  val fold_map_vars :
+    init:'a -> t -> f:('a -> Var.t -> 'a * Var.t) -> 'a * t
+
+  val rename : Var.Subst.t -> t -> t
+  val disjuncts : t -> t list
 end
 
 (** Inference System *)
@@ -214,7 +229,7 @@ module Context : sig
       implies [a = b+k], or [None] if [a] and [b] are not equal up to an
       integer offset. *)
 
-  val fold_terms : t -> init:'a -> f:('a -> Term.t -> 'a) -> 'a
+  val fold_terms : init:'a -> t -> f:('a -> Term.t -> 'a) -> 'a
 
   (** Solution Substitutions *)
   module Subst : sig
diff --git a/sledge/src/ses/term.ml b/sledge/src/ses/term.ml
index f1a013b1b..aacccb999 100644
--- a/sledge/src/ses/term.ml
+++ b/sledge/src/ses/term.ml
@@ -1040,6 +1040,8 @@ module Var = struct
     | Some v -> v
     | _ -> violates Llair.Reg.invariant r
 
+  let program ~name ~global = Var {name; id= (if global then -1 else 0)}
+
   let fresh name ~wrt =
     let max = match Set.max_elt wrt with None -> 0 | Some max -> id max in
     let x' = Var {name; id= max + 1} in
diff --git a/sledge/src/ses/term.mli b/sledge/src/ses/term.mli
index 54f6652c3..64cdc7b3d 100644
--- a/sledge/src/ses/term.mli
+++ b/sledge/src/ses/term.mli
@@ -128,6 +128,7 @@ module Var : sig
   val of_ : term -> t
   val of_term : term -> t option
   val of_reg : Llair.Reg.t -> t
+  val program : name:string -> global:bool -> t
   val fresh : string -> wrt:Set.t -> t * Set.t
 
   val identified : name:string -> id:int -> t
diff --git a/sledge/src/sh_test.ml b/sledge/src/sh_test.ml
index 1c8a66eda..c6d71dea3 100644
--- a/sledge/src/sh_test.ml
+++ b/sledge/src/sh_test.ml
@@ -83,9 +83,9 @@ let%test_module _ =
           ( (  0 = %x_6 ∧ emp)
           ∨ (  ( (  1 = _ = %y_7 ∧ emp) ∨ (  2 = _ ∧ emp) ))
           )
-
+    
         ( (∃ %x_6, %x_7 .   2 = %x_7 ∧ (%x_7 = 2) ∧ emp)
-        ∨ (∃ %x_6 .   1 = %x_6 = %y_7 ∧ ((%x_6 = 1) && (%y_7 = 1)) ∧ emp)
+        ∨ (∃ %x_6 .   1 = %x_6 = %y_7 ∧ ((%x_6 = 1) ∧ (%y_7 = 1)) ∧ emp)
         ∨ (  0 = %x_6 ∧ (%x_6 = 0) ∧ emp)
         ) |}]
 
@@ -108,11 +108,11 @@ let%test_module _ =
           ( (  0 = _ ∧ emp)
           ∨ (  ( (  1 = _ = %y_7 ∧ emp) ∨ (  2 = _ ∧ emp) ))
           )
-
+    
         ( (∃ %x_6, %x_8, %x_9 .   2 = %x_9 ∧ (%x_9 = 2) ∧ emp)
         ∨ (∃ %x_6, %x_8 .
              1 = %y_7 = %x_8
-           ∧ ((%y_7 = 1) && (%x_8 = 1))
+           ∧ ((%x_8 = 1) ∧ (%y_7 = 1))
            ∧ emp)
         ∨ (∃ %x_6 .   0 = %x_6 ∧ (%x_6 = 0) ∧ emp)
         ) |}]
@@ -136,7 +136,7 @@ let%test_module _ =
         ( (  0 = _ ∧ emp)
         ∨ (  ( (  1 = _ = %y_7 ∧ emp) ∨ (  2 = _ ∧ emp) ))
         )
-
+    
         ( (  1 = %y_7 ∧ emp) ∨ (  emp) ∨ (  emp) ) |}]
 
     let%expect_test _ =
@@ -148,9 +148,9 @@ let%test_module _ =
       [%expect
         {|
         ∃ %x_6 .   %x_6 = %x_6^ ∧ (%y_7 + -1) = %y_7^ ∧ emp
-
-          (%y_7 + -1) = %y_7^ ∧ (%y_7^ = (%y_7 + -1)) ∧ emp
-
+    
+          (%y_7 + -1) = %y_7^ ∧ (%y_7^ = ((-1 × 1) + (1 × %y_7))) ∧ emp
+    
           (%y_7 + -1) = %y_7^ ∧ emp |}]
 
     let%expect_test _ =
@@ -173,7 +173,7 @@ let%test_module _ =
         {|
         ∃ %a_1, %c_3, %d_4, %e_5 .
           (⟨8,%a_1⟩^⟨8,%d_4⟩) = %e_5
-        ∧ (⟨16,%e_5⟩ = (⟨8,%a_1⟩^⟨8,%d_4⟩))
+        ∧ ((⟨16,%e_5⟩ = (⟨8,%a_1⟩^⟨8,%d_4⟩)) ∧ tt)
         ∧ emp
         * ( (  (%x_6 ≠ 0) ∧ emp)
           ∨ (∃ %b_2 .
@@ -182,7 +182,7 @@ let%test_module _ =
              ∧ emp)
           )
 
-          -1 ∧ emp * ( (  -1 ∧ emp) ∨ (  (%x_6 ≠ 0) ∧ emp) )
+          tt ∧ emp * ( (  tt ∧ emp) ∨ (  (%x_6 ≠ 0) ∧ emp) )
 
           ( (  emp) ∨ (  (%x_6 ≠ 0) ∧ emp) ) |}]
   end )
diff --git a/sledge/src/solver_test.ml b/sledge/src/solver_test.ml
index 01b8eb039..5c5d63748 100644
--- a/sledge/src/solver_test.ml
+++ b/sledge/src/solver_test.ml
@@ -196,7 +196,7 @@ let%test_module _ =
             %a_2 = %a0_10
           ∧ (⟨16,%a_2⟩^⟨16,%a1_11⟩) = %a_1
           ∧ 16 = %m_8 = %n_9
-          ∧ (%k_5 + 16) -[ %k_5, 16 )-> ⟨16,%a1_11⟩ |}]
+          ∧ ((16 × 1) + (1 × %k_5)) -[ %k_5, 16 )-> ⟨16,%a1_11⟩ |}]
 
     let%expect_test _ =
       infer_frame
@@ -218,7 +218,7 @@ let%test_module _ =
             %a_2 = %a0_10
           ∧ (⟨16,%a_2⟩^⟨16,%a1_11⟩) = %a_1
           ∧ 16 = %m_8 = %n_9
-          ∧ (%k_5 + 16) -[ %k_5, 16 )-> ⟨16,%a1_11⟩ |}]
+          ∧ ((16 × 1) + (1 × %k_5)) -[ %k_5, 16 )-> ⟨16,%a1_11⟩ |}]
 
     let seg_split_symbolically =
       Sh.star
@@ -236,7 +236,7 @@ let%test_module _ =
       [%expect
         {|
         ( infer_frame:
-            %l_6 -[ %l_6, 16 )-> ⟨(8 × %n_9),%a_2⟩^⟨(-8 × %n_9 + 16),%a_3⟩
+            %l_6 -[ %l_6, 16 )-> ⟨(8 × %n_9),%a_2⟩^⟨(16 - (8 × %n_9)),%a_3⟩
           * ( (  2 = %n_9 ∧ emp)
             ∨ (  0 = %n_9 ∧ emp)
             ∨ (  1 = %n_9 ∧ emp)
@@ -247,7 +247,7 @@ let%test_module _ =
             ( (  %a_1 = %a_2
                ∧ 2 = %n_9
                ∧ 16 = %m_8
-               ∧ (%l_6 + 16) -[ %l_6, 16 )-> ⟨0,%a_3⟩)
+               ∧ ((16 × 1) + (1 × %l_6)) -[ %l_6, 16 )-> ⟨0,%a_3⟩)
             ∨ (  %a_3 = _
                ∧ (⟨8,%a_2⟩^⟨8,%a_3⟩) = %a_1
                ∧ 1 = %n_9
@@ -269,8 +269,8 @@ let%test_module _ =
       [%expect
         {|
         ( infer_frame:
-            (%n_9 ≤ 2)
-          ∧ %l_6 -[ %l_6, 16 )-> ⟨(8 × %n_9),%a_2⟩^⟨(-8 × %n_9 + 16),%a_3⟩
+            ((%n_9 ≤ 2) ∧ (tt ∧ tt))
+          ∧ %l_6 -[ %l_6, 16 )-> ⟨(8 × %n_9),%a_2⟩^⟨(16 - (8 × %n_9)),%a_3⟩
           \- ∃ %a_1, %m_8 .
               %l_6 -[ %l_6, %m_8 )-> ⟨%m_8,%a_1⟩
         ) infer_frame: |}]