diff --git a/sledge/src/domain_sh.ml b/sledge/src/domain_sh.ml
index 7ec996f3b..1b2e75b76 100644
--- a/sledge/src/domain_sh.ml
+++ b/sledge/src/domain_sh.ml
@@ -79,7 +79,7 @@ let term_eq_class_has_only_vars_in fvs ctx term =
       Context.pp ctx Term.pp term]
   ;
   let term_has_only_vars_in fvs term =
-    Var.Set.subset (Term.fv term) ~of_:fvs
+    Var.Set.subset (Trm.fv term) ~of_:fvs
   in
   let term_eq_class = Context.class_of ctx term in
   List.exists ~f:(term_has_only_vars_in fvs) term_eq_class
@@ -98,7 +98,7 @@ let garbage_collect (q : t) ~wrt =
         List.fold q.heap current ~f:(fun seg current ->
             if term_eq_class_has_only_vars_in current q.ctx seg.loc then
               List.fold (Context.class_of q.ctx seg.seq) current
-                ~f:(fun e c -> Var.Set.union c (Term.fv e))
+                ~f:(fun e c -> Var.Set.union c (Trm.fv e))
             else current )
       in
       all_reachable_vars current new_set q
diff --git a/sledge/src/fol.ml b/sledge/src/fol.ml
index d245170e8..fad60ed5c 100644
--- a/sledge/src/fol.ml
+++ b/sledge/src/fol.ml
@@ -60,17 +60,6 @@ let _Ite cnd thn els =
   | _ when Fml.is_negative cnd -> `Ite (Fml.not_ cnd, els, thn)
   | _ -> `Ite (cnd, thn, els)
 
-(** 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
@@ -101,23 +90,16 @@ let ite : fml -> exp -> exp -> exp =
       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 :> exp) )
 
-(** 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 -> map_cnd cond (fun e -> Fml.not_ (Fml.eq0 e)) c
+(** 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'
 
 (** Map a unary function on terms over an expression. *)
 let ap1 : (trm -> exp) -> exp -> exp =
@@ -448,461 +430,3 @@ module Formula = struct
 
   let rename s e = map_vars ~f:(Var.Subst.apply s) e
 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 -> Ses.Var.Set.of_iter (Iter.map ~f:v_to_ses (Var.Set.to_iter vs))
-
-let rec arith_to_ses poly =
-  Trm.Arith.fold_monomials poly Ses.Term.zero ~f:(fun mono coeff e ->
-      Ses.Term.add e
-        (Ses.Term.mulq coeff
-           (Trm.Arith.fold_factors mono Ses.Term.one ~f:(fun trm pow f ->
-                let rec exp b i =
-                  assert (i > 0) ;
-                  if i = 1 then b else Ses.Term.mul b (exp f (i - 1))
-                in
-                Ses.Term.mul f (exp (t_to_ses trm) pow) ))) )
-
-and 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
-  | Arith a -> arith_to_ses a
-  | 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 (Array.map ~f:t_to_ses es)
-  | Select {idx; rcd} -> Ses.Term.select ~rcd:(t_to_ses rcd) ~idx
-  | Update {idx; rcd; elt} ->
-      Ses.Term.update ~rcd:(t_to_ses rcd) ~idx ~elt:(t_to_ses elt)
-  | Record es ->
-      Ses.Term.record (IArray.of_array (Array.map ~f:t_to_ses es))
-  | Ancestor i -> Ses.Term.rec_record i
-  | Apply (Rem, [|x; y|]) -> Ses.Term.rem (t_to_ses x) (t_to_ses y)
-  | Apply (BitAnd, [|x; y|]) -> Ses.Term.and_ (t_to_ses x) (t_to_ses y)
-  | Apply (BitOr, [|x; y|]) -> Ses.Term.or_ (t_to_ses x) (t_to_ses y)
-  | Apply (BitXor, [|x; y|]) -> Ses.Term.dq (t_to_ses x) (t_to_ses y)
-  | Apply (BitShl, [|x; y|]) -> Ses.Term.shl (t_to_ses x) (t_to_ses y)
-  | Apply (BitLshr, [|x; y|]) -> Ses.Term.lshr (t_to_ses x) (t_to_ses y)
-  | Apply (BitAshr, [|x; y|]) -> Ses.Term.ashr (t_to_ses x) (t_to_ses y)
-  | Apply (Signed n, [|x|]) -> Ses.Term.signed n (t_to_ses x)
-  | Apply (Unsigned n, [|x|]) -> Ses.Term.unsigned n (t_to_ses x)
-  | Apply (sym, xs) ->
-      Ses.Term.apply sym (IArray.of_array (Array.map ~f:t_to_ses xs))
-
-let rec f_to_ses : fml -> Ses.Term.t = function
-  | Tt -> Ses.Term.true_
-  | Not Tt -> Ses.Term.false_
-  | Eq (x, y) -> Ses.Term.eq (t_to_ses x) (t_to_ses y)
-  | Eq0 x -> Ses.Term.eq Ses.Term.zero (t_to_ses x)
-  | Pos x -> Ses.Term.lt Ses.Term.zero (t_to_ses x)
-  | Not p -> Ses.Term.not_ (f_to_ses p)
-  | And {pos; neg} ->
-      Formula.fold_pos_neg
-        ~f:(fun f p -> Ses.Term.and_ p (f_to_ses f))
-        ~pos ~neg Ses.Term.true_
-  | Or {pos; neg} ->
-      Formula.fold_pos_neg
-        ~f:(fun f p -> Ses.Term.or_ p (f_to_ses f))
-        ~pos ~neg Ses.Term.false_
-  | Iff (p, q) -> Ses.Term.eq (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)
-  | Lit (sym, args) ->
-      Ses.Term.poslit sym (IArray.of_array (Array.map ~f:t_to_ses args))
-
-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 -> Var.Set.of_iter (Iter.map ~f:v_of_ses (Ses.Var.Set.to_iter vs))
-
-let uap1 f = ap1t (fun x -> Trm.apply f [|x|])
-let uap2 f = ap2t (fun x y -> Trm.apply f [|x; y|])
-let litN p = apNf (Fml.lit p)
-
-let rec uap_tt f a = uap1 f (of_ses a)
-and uap_ttt f a b = uap2 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 es (None, None) ~f:(fun e (fs, ts) ->
-        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
-  | Ap1 (Signed {bits}, e) -> uap_tt (Signed bits) e
-  | Ap1 (Unsigned {bits}, e) -> uap_tt (Unsigned bits) 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 (fun p q -> and_ (not_ p) q) lt d e
-  | Ap2 (Le, d, e) -> ap2_f (fun p q -> or_ (not_ p) q) le d e
-  | PosLit (p, es) ->
-      `Fml (litN p (IArray.to_array (IArray.map ~f:of_ses es)))
-  | NegLit (p, es) ->
-      `Fml (not_ (litN p (IArray.to_array (IArray.map ~f:of_ses es))))
-  | Add sum -> (
-    match Ses.Term.Qset.pop_min_elt sum with
-    | None -> zero
-    | Some (e, q, sum) ->
-        let mul e q =
-          if Q.equal Q.one q then of_ses e
-          else
-            match of_ses e with
-            | `Trm (Z z) -> rational (Q.mul q (Q.of_z z))
-            | `Trm (Q r) -> rational (Q.mul q r)
-            | t -> mulq q t
-        in
-        Ses.Term.Qset.fold ~f:(fun e q -> add (mul e q)) sum (mul e q) )
-  | Mul prod -> (
-    match Ses.Term.Qset.pop_min_elt prod with
-    | None -> one
-    | Some (e, q, prod) ->
-        let rec expn e n =
-          let p = Z.pred n in
-          if Z.sign p = 0 then e else mul e (expn e p)
-        in
-        let exp e q =
-          let n = Q.num q in
-          let sn = Z.sign n in
-          if sn = 0 then of_ses e
-          else if sn > 0 then expn (of_ses e) n
-          else div one (expn (of_ses e) (Z.neg n))
-        in
-        Ses.Term.Qset.fold ~f:(fun e q -> mul (exp e q)) prod (exp e q) )
-  | Ap2 (Div, d, e) -> div (of_ses d) (of_ses e)
-  | Ap2 (Rem, d, e) -> uap_ttt Rem d e
-  | And es -> apN and_ (uap2 BitAnd) tt es
-  | Or es -> apN or_ (uap2 BitOr) ff es
-  | Ap2 (Xor, d, e) -> ap2 xor (uap2 BitXor) d e
-  | Ap2 (Shl, d, e) -> uap_ttt BitShl d e
-  | Ap2 (Lshr, d, e) -> uap_ttt BitLshr d e
-  | Ap2 (Ashr, d, e) -> uap_ttt BitAshr 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 (Array.map ~f:of_ses (IArray.to_array 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 (Array.map ~f:of_ses (IArray.to_array elts))
-  | RecRecord i -> ancestor i
-  | Apply (sym, args) ->
-      apply sym (Array.map ~f:of_ses (IArray.to_array args))
-
-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 -> of_ses (f (to_ses x))
-
-let f_ses_map : (Ses.Term.t -> Ses.Term.t) -> fml -> fml =
- fun f x -> f_of_ses (f (f_to_ses x))
-
-(*
- * Contexts
- *)
-
-module Context = struct
-  type t = Ses.Equality.t [@@deriving sexp]
-
-  let invariant = Ses.Equality.invariant
-
-  (* Query *)
-
-  let vars x =
-    Iter.from_iter (fun f ->
-        Ses.Equality.fold_vars ~f:(fun v () -> f (v_of_ses v)) x () )
-
-  let fv x = Var.Set.of_iter (vars x)
-  let is_empty x = Ses.Equality.is_true x
-  let is_unsat x = Ses.Equality.is_false x
-  let implies x b = Ses.Equality.implies x (f_to_ses b)
-
-  let refutes x b =
-    Ses.Term.is_false (Ses.Equality.normalize x (f_to_ses b))
-
-  let normalize x e = ses_map (Ses.Equality.normalize x) e
-
-  (* Classes *)
-
-  let class_of x e = List.map ~f:of_ses (Ses.Equality.class_of x (to_ses e))
-
-  let classes x =
-    Ses.Term.Map.fold (Ses.Equality.classes x) 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.add ~key:rep' ~data:cls' clss )
-
-  let diff_classes r s =
-    Term.Map.filter_mapi (classes r) ~f:(fun ~key:rep ~data:cls ->
-        match
-          List.filter cls ~f:(fun exp ->
-              not (implies s (Formula.eq rep exp)) )
-        with
-        | [] -> None
-        | cls -> Some cls )
-
-  (* Pretty printing *)
-
-  let pp_raw = Ses.Equality.pp
-  let ppx_cls x = List.pp "@ = " (Term.ppx x)
-
-  let ppx_classes x fs clss =
-    List.pp "@ @<2>∧ "
-      (fun fs (rep, cls) ->
-        Format.fprintf fs "@[%a@ = %a@]" (Term.ppx x) rep (ppx_cls x)
-          (List.sort ~cmp:Term.compare cls) )
-      fs
-      (Iter.to_list (Term.Map.to_iter clss))
-
-  let pp fs r = ppx_classes (fun _ -> None) fs (classes r)
-
-  let ppx var_strength fs clss noneqs =
-    let first = Term.Map.is_empty clss in
-    if not first then Format.fprintf fs "  " ;
-    ppx_classes var_strength fs clss ;
-    List.pp
-      ~pre:(if first then "@[  " else "@ @[@<2>∧ ")
-      "@ @<2>∧ "
-      (Formula.ppx var_strength)
-      fs noneqs ~suf:"@]" ;
-    first && List.is_empty noneqs
-
-  let ppx_diff var_strength fs parent_ctx fml ctx =
-    let fml' = f_ses_map (Ses.Equality.normalize ctx) fml in
-    ppx var_strength fs
-      (diff_classes ctx parent_ctx)
-      (if Formula.(equal tt fml') then [] else [fml'])
-
-  (* Construct *)
-
-  let empty = Ses.Equality.true_
-
-  let add 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 union vs x y =
-    let vs', z = Ses.Equality.and_ (vs_to_ses vs) x y in
-    (vs_of_ses vs', z)
-
-  let inter vs x y =
-    let vs', z = Ses.Equality.or_ (vs_to_ses vs) x y in
-    (vs_of_ses vs', z)
-
-  let interN vs xs =
-    let vs', z = Ses.Equality.orN (vs_to_ses vs) xs in
-    (vs_of_ses vs', z)
-
-  let dnf f =
-    let meet1 a (vs, p, x) =
-      let vs, x = add vs a x in
-      (vs, Formula.and_ p a, x)
-    in
-    let join1 = Iter.cons in
-    let top = (Var.Set.empty, Formula.tt, empty) in
-    let bot = Iter.empty in
-    Formula.fold_dnf ~meet1 ~join1 ~top ~bot f
-
-  let rename x sub = Ses.Equality.rename x (v_map_ses (Var.Subst.apply sub))
-
-  (* Substs *)
-
-  module Subst = struct
-    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 z ~f =
-      Ses.Equality.Subst.fold s z ~f:(fun ~key ~data ->
-          f ~key:(of_ses key) ~data:(of_ses data) )
-
-    let subst s = 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 =
-    | Add of Var.Set.t * fml * t
-    | Union of Var.Set.t * t * t
-    | Inter of Var.Set.t * t * t
-    | InterN of Var.Set.t * t list
-    | Rename of t * Var.Subst.t
-    | Is_unsat of t
-    | Implies of t * fml
-    | Refutes of t * fml
-    | Normalize of t * exp
-    | Apply_subst of Var.Set.t * Subst.t * t
-    | Solve_for_vars of Var.Set.t list * t
-    | Elim of Var.Set.t * t
-  [@@deriving sexp]
-
-  let replay c =
-    match call_of_sexp (Sexp.of_string c) with
-    | Add (us, e, r) -> add us e r |> ignore
-    | Union (us, r, s) -> union us r s |> ignore
-    | Inter (us, r, s) -> inter us r s |> ignore
-    | InterN (us, rs) -> interN us rs |> ignore
-    | Rename (r, s) -> rename r s |> ignore
-    | Is_unsat r -> is_unsat r |> ignore
-    | Implies (r, f) -> implies r f |> ignore
-    | Refutes (r, f) -> refutes r f |> ignore
-    | Normalize (r, e) -> normalize r e |> ignore
-    | Apply_subst (us, s, r) -> apply_subst us s r |> ignore
-    | Solve_for_vars (vss, r) -> solve_for_vars vss r |> ignore
-    | Elim (ks, r) -> elim ks r |> ignore
-
-  (* Debug wrappers *)
-
-  let report ~name ~elapsed ~aggregate ~count =
-    Format.eprintf "%15s time: %12.3f ms  %12.3f ms  %12d calls@." name
-      elapsed aggregate count
-
-  let dump_threshold = ref 1000.
-
-  let wrap tmr f call =
-    let f () =
-      Timer.start tmr ;
-      let r = f () in
-      Timer.stop_report tmr (fun ~name ~elapsed ~aggregate ~count ->
-          report ~name ~elapsed ~aggregate ~count ;
-          if Float.(elapsed > !dump_threshold) then (
-            dump_threshold := 2. *. !dump_threshold ;
-            Format.eprintf "@\n%a@\n@." Sexp.pp_hum (sexp_of_call (call ()))
-            ) ) ;
-      r
-    in
-    if not [%debug] then f ()
-    else
-      try f ()
-      with exn ->
-        let bt = Printexc.get_raw_backtrace () in
-        let sexp = sexp_of_call (call ()) in
-        raise (Replay (exn, bt, sexp))
-
-  let add_tmr = Timer.create "add" ~at_exit:report
-  let union_tmr = Timer.create "union" ~at_exit:report
-  let inter_tmr = Timer.create "inter" ~at_exit:report
-  let interN_tmr = Timer.create "interN" ~at_exit:report
-  let rename_tmr = Timer.create "rename" ~at_exit:report
-  let is_unsat_tmr = Timer.create "is_unsat" ~at_exit:report
-  let implies_tmr = Timer.create "implies" ~at_exit:report
-  let refutes_tmr = Timer.create "refutes" ~at_exit:report
-  let normalize_tmr = Timer.create "normalize" ~at_exit:report
-  let apply_subst_tmr = Timer.create "apply_subst" ~at_exit:report
-  let solve_for_vars_tmr = Timer.create "solve_for_vars" ~at_exit:report
-  let elim_tmr = Timer.create "elim" ~at_exit:report
-
-  let add us e r =
-    wrap add_tmr (fun () -> add us e r) (fun () -> Add (us, e, r))
-
-  let union us r s =
-    wrap union_tmr (fun () -> union us r s) (fun () -> Union (us, r, s))
-
-  let inter us r s =
-    wrap inter_tmr (fun () -> inter us r s) (fun () -> Inter (us, r, s))
-
-  let interN us rs =
-    wrap interN_tmr (fun () -> interN us rs) (fun () -> InterN (us, rs))
-
-  let rename r s =
-    wrap rename_tmr (fun () -> rename r s) (fun () -> Rename (r, s))
-
-  let is_unsat r =
-    wrap is_unsat_tmr (fun () -> is_unsat r) (fun () -> Is_unsat r)
-
-  let implies r f =
-    wrap implies_tmr (fun () -> implies r f) (fun () -> Implies (r, f))
-
-  let refutes r f =
-    wrap refutes_tmr (fun () -> refutes r f) (fun () -> Refutes (r, f))
-
-  let normalize r e =
-    wrap normalize_tmr (fun () -> normalize r e) (fun () -> Normalize (r, e))
-
-  let apply_subst us s r =
-    wrap apply_subst_tmr
-      (fun () -> apply_subst us s r)
-      (fun () -> Apply_subst (us, s, r))
-
-  let solve_for_vars vss r =
-    wrap solve_for_vars_tmr
-      (fun () -> solve_for_vars vss r)
-      (fun () -> Solve_for_vars (vss, r))
-
-  let elim ks r =
-    wrap elim_tmr (fun () -> elim ks r) (fun () -> Elim (ks, r))
-end
diff --git a/sledge/src/fol.mli b/sledge/src/fol.mli
index e868955c7..120a11e98 100644
--- a/sledge/src/fol.mli
+++ b/sledge/src/fol.mli
@@ -141,108 +141,3 @@ and Formula : sig
   val fold_map_vars : t -> 's -> f:(Var.t -> 's -> Var.t * 's) -> t * 's
   val rename : Var.Subst.t -> t -> t
 end
-
-(** Sets of assumptions, interpreted as conjunction, plus reasoning about
-    their logical consequences. *)
-module Context : sig
-  type t [@@deriving sexp]
-
-  val pp : t pp
-
-  val ppx_diff :
-    Var.strength -> Format.formatter -> t -> Formula.t -> t -> bool
-
-  include Invariant.S with type t := t
-
-  val empty : t
-  (** The empty context of assumptions. *)
-
-  val add : Var.Set.t -> Formula.t -> t -> Var.Set.t * t
-  (** Add (that is, conjoin) an assumption to a context. *)
-
-  val union : Var.Set.t -> t -> t -> Var.Set.t * t
-  (** Union (that is, conjoin) two contexts of assumptions. *)
-
-  val inter : Var.Set.t -> t -> t -> Var.Set.t * t
-  (** Intersect (that is, disjoin) contexts of assumptions. *)
-
-  val interN : Var.Set.t -> t list -> Var.Set.t * t
-  (** Intersect contexts of assumptions. Possibly weaker than logical
-      disjunction. *)
-
-  val dnf : Formula.t -> (Var.Set.t * Formula.t * t) iter
-  (** Disjunctive-normal form expansion. *)
-
-  val rename : t -> Var.Subst.t -> t
-  (** Apply a renaming substitution to the context. *)
-
-  val is_empty : t -> bool
-  (** Test if the context of assumptions is empty. *)
-
-  val is_unsat : t -> bool
-  (** Test if the context of assumptions is inconsistent. *)
-
-  val implies : t -> Formula.t -> bool
-  (** Holds only if a formula is a logical consequence of a context of
-      assumptions. This only checks if the formula is valid in the current
-      state of the context, without doing any further logical reasoning or
-      propagation. *)
-
-  val refutes : t -> Formula.t -> bool
-  (** Holds only if a formula is inconsistent with a context of assumptions,
-      that is, conjoining the formula to the assumptions is unsatisfiable. *)
-
-  val normalize : t -> Term.t -> Term.t
-  (** Normalize a term [e] to [e'] such that [e = e'] is implied by the
-      assumptions, where [e'] and its subterms are expressed in terms of the
-      canonical representatives of each equivalence class. *)
-
-  val class_of : t -> Term.t -> Term.t list
-  (** Equivalence class of [e]: all the terms [f] in the context such that
-      [e = f] is implied by the assumptions. *)
-
-  val vars : t -> Var.t iter
-  (** Enumerate the variables occurring in the terms of the context. *)
-
-  val fv : t -> Var.Set.t
-  (** The variables occurring in the terms of the context. *)
-
-  (** Solution Substitutions *)
-  module Subst : sig
-    type t
-
-    val pp : t pp
-    val is_empty : t -> bool
-    val fold : t -> 's -> f:(key:Term.t -> data:Term.t -> 's -> 's) -> 's
-
-    val subst : t -> Term.t -> Term.t
-    (** Apply a substitution recursively to subterms. *)
-
-    val partition_valid : Var.Set.t -> t -> t * Var.Set.t * t
-    (** Partition ∃xs. σ into equivalent ∃xs. τ ∧ ∃ks. ν where ks
-        and ν are maximal where ∃ks. ν is universally valid, xs ⊇ ks
-        and ks ∩ fv(τ) = ∅. *)
-  end
-
-  val apply_subst : Var.Set.t -> Subst.t -> t -> Var.Set.t * t
-  (** Context induced by applying a solution substitution to a set of
-      equations generating the argument context. *)
-
-  val solve_for_vars : Var.Set.t list -> t -> Subst.t
-  (** [solve_for_vars vss x] is a solution substitution that is implied by
-      [x] and consists of oriented equalities [v ↦ e] that map terms [v]
-      with free variables contained in (the union of) a prefix [uss] of
-      [vss] to terms [e] with free variables contained in as short a prefix
-      of [uss] as possible. *)
-
-  val elim : Var.Set.t -> t -> t
-  (** [elim ks x] is [x] weakened by removing oriented equations [k ↦ _]
-      for [k] in [ks]. *)
-
-  (**/**)
-
-  val pp_raw : t pp
-
-  val replay : string -> unit
-  (** Replay debugging *)
-end
diff --git a/sledge/src/propositional_intf.ml b/sledge/src/propositional_intf.ml
index c7ccacb40..361f8b73d 100644
--- a/sledge/src/propositional_intf.ml
+++ b/sledge/src/propositional_intf.ml
@@ -7,8 +7,6 @@
 
 (** Propositional formulas *)
 
-open Ses
-
 module type TERM = sig
   type t [@@deriving compare, equal, sexp]
 end
@@ -35,7 +33,7 @@ module type FORMULA = sig
     | Iff of t * t
     | Cond of {cnd: t; pos: t; neg: t}
     (* uninterpreted literals *)
-    | Lit of Predsym.t * trm array
+    | Lit of Ses.Predsym.t * trm array
   [@@deriving compare, equal, sexp]
 
   val mk_Tt : unit -> t
@@ -47,7 +45,7 @@ module type FORMULA = sig
   val _Or : pos:set -> neg:set -> t
   val _Iff : t -> t -> t
   val _Cond : t -> t -> t -> t
-  val _Lit : Predsym.t -> trm array -> t
+  val _Lit : Ses.Predsym.t -> trm array -> t
   val and_ : t -> t -> t
   val or_ : t -> t -> t
   val is_negative : t -> bool
diff --git a/sledge/src/ses/equality.ml b/sledge/src/ses/equality.ml
deleted file mode 100644
index 48da4aa0a..000000000
--- a/sledge/src/ses/equality.ml
+++ /dev/null
@@ -1,1036 +0,0 @@
-(*
- * 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.
- *)
-
-(** Equality over uninterpreted functions and linear rational arithmetic *)
-
-(** Classification of Terms by Theory *)
-
-type kind = Interpreted | Atomic | Uninterpreted
-[@@deriving compare, equal]
-
-let classify e =
-  match (e : Term.t) with
-  | Add _ | Ap2 (Sized, _, _) | Ap3 (Extract, _, _, _) | ApN (Concat, _) ->
-      Interpreted
-  | Mul _ | Ap1 _ | Ap2 _ | Ap3 _ | ApN _ | Apply _ | PosLit _ | NegLit _
-   |And _ | Or _ ->
-      Uninterpreted
-  | Var _ | Integer _ | Rational _ | RecRecord _ -> Atomic
-
-let interpreted e = equal_kind (classify e) Interpreted
-let non_interpreted e = not (interpreted e)
-let uninterpreted e = equal_kind (classify e) Uninterpreted
-
-let rec fold_max_solvables e s ~f =
-  if non_interpreted e then f e s
-  else Term.fold ~f:(fold_max_solvables ~f) e s
-
-(** Solution Substitutions *)
-module Subst : sig
-  type t [@@deriving compare, equal, sexp]
-
-  val pp : t pp
-  val pp_diff : (t * t) pp
-  val empty : t
-  val is_empty : t -> bool
-  val length : t -> int
-  val mem : Term.t -> t -> bool
-  val find : Term.t -> t -> Term.t option
-  val fold : t -> 's -> f:(key:Term.t -> data:Term.t -> 's -> 's) -> 's
-  val iteri : t -> f:(key:Term.t -> data:Term.t -> unit) -> unit
-  val for_alli : t -> f:(key:Term.t -> data:Term.t -> bool) -> bool
-  val apply : t -> Term.t -> Term.t
-  val subst : t -> Term.t -> Term.t
-  val norm : t -> Term.t -> Term.t
-  val compose : t -> t -> t
-  val compose1 : key:Term.t -> data:Term.t -> t -> t
-  val extend : Term.t -> t -> t option
-  val remove : Var.Set.t -> t -> t
-  val map_entries : f:(Term.t -> Term.t) -> t -> t
-  val to_iter : t -> (Term.t * Term.t) iter
-  val partition_valid : Var.Set.t -> t -> t * Var.Set.t * t
-end = struct
-  type t = Term.t Term.Map.t [@@deriving compare, equal, sexp_of]
-
-  let t_of_sexp = Term.Map.t_of_sexp Term.t_of_sexp
-  let pp = Term.Map.pp Term.pp Term.pp
-  let pp_diff = Term.Map.pp_diff ~eq:Term.equal Term.pp Term.pp Term.pp_diff
-  let empty = Term.Map.empty
-  let is_empty = Term.Map.is_empty
-  let length = Term.Map.length
-  let mem = Term.Map.mem
-  let find = Term.Map.find
-  let fold = Term.Map.fold
-  let iteri = Term.Map.iteri
-  let for_alli = Term.Map.for_alli
-  let to_iter = Term.Map.to_iter
-
-  (** look up a term in a substitution *)
-  let apply s a = Term.Map.find a s |> Option.value ~default:a
-
-  let rec subst s a = apply s (Term.map ~f:(subst s) a)
-
-  (** apply a substitution to maximal non-interpreted subterms *)
-  let rec norm s a =
-    if interpreted a then Term.map ~f:(norm s) a else apply s a
-
-  (** compose two substitutions *)
-  let compose r s =
-    [%Trace.call fun {pf} -> pf "%a@ %a" pp r pp s]
-    ;
-    let r' = Term.Map.map_endo ~f:(norm s) r in
-    Term.Map.merge_endo r' s ~f:(fun key -> function
-      | `Both (data_r, data_s) ->
-          assert (
-            Term.equal data_s data_r
-            || fail "domains intersect: %a" Term.pp key () ) ;
-          Some data_r
-      | `Left data | `Right data -> Some data )
-    |>
-    [%Trace.retn fun {pf} r' ->
-      pf "%a" pp_diff (r, r') ;
-      assert (r' == r || not (equal r' r))]
-
-  (** compose a substitution with a mapping *)
-  let compose1 ~key ~data s =
-    match (key : Term.t) with
-    | Integer _ | Rational _ -> s
-    | _ ->
-        if Term.equal key data then s
-        else compose s (Term.Map.singleton key data)
-
-  (** add an identity entry if the term is not already present *)
-  let extend e s =
-    let exception Found in
-    match
-      Term.Map.update e s ~f:(function
-        | Some _ -> raise_notrace Found
-        | None -> e )
-    with
-    | exception Found -> None
-    | s -> Some s
-
-  (** remove entries for vars *)
-  let remove xs s =
-    Var.Set.fold ~f:(fun x -> Term.Map.remove (Term.var x)) xs s
-
-  (** map over a subst, applying [f] to both domain and range, requires that
-      [f] is injective and for any set of terms [E], [f\[E\]] is disjoint
-      from [E] *)
-  let map_entries ~f s =
-    Term.Map.fold s s ~f:(fun ~key ~data s ->
-        let key' = f key in
-        let data' = f data in
-        if Term.equal key' key then
-          if Term.equal data' data then s
-          else Term.Map.add ~key ~data:data' s
-        else
-          let s = Term.Map.remove key s in
-          match (key : Term.t) with
-          | Integer _ | Rational _ -> s
-          | _ -> Term.Map.add_exn ~key:key' ~data:data' s )
-
-  (** Holds only if [true ⊢ ∃xs. e=f]. Clients assume
-      [not (is_valid_eq xs e f)] implies [not (is_valid_eq ys e f)] for
-      [ys ⊆ xs]. *)
-  let is_valid_eq xs e f =
-    let is_var_in xs e =
-      Option.exists ~f:(fun x -> Var.Set.mem x xs) (Var.of_term e)
-    in
-    ( is_var_in xs e
-    || is_var_in xs f
-    || (uninterpreted e && Term.exists ~f:(is_var_in xs) e)
-    || (uninterpreted f && Term.exists ~f:(is_var_in xs) f) )
-    $> fun b ->
-    [%Trace.info
-      "is_valid_eq %a%a=%a = %b" Var.Set.pp_xs xs Term.pp e Term.pp f b]
-
-  (** Partition ∃xs. σ into equivalent ∃xs. τ ∧ ∃ks. ν where ks
-      and ν are maximal where ∃ks. ν is universally valid, xs ⊇ ks and
-      ks ∩ fv(τ) = ∅. *)
-  let partition_valid xs s =
-    (* Move equations e=f from s to t when ∃ks.e=f fails to be provably
-       valid. When moving an equation, reduce ks by fv(e=f) to maintain ks ∩
-       fv(t) = ∅. This reduction may cause equations in s to no longer be
-       valid, so loop until no change. *)
-    let rec partition_valid_ t ks s =
-      let t', ks', s' =
-        Term.Map.fold s (t, ks, s) ~f:(fun ~key ~data (t, ks, s) ->
-            if is_valid_eq ks key data then (t, ks, s)
-            else
-              let t = Term.Map.add ~key ~data t
-              and ks =
-                Var.Set.diff ks (Var.Set.union (Term.fv key) (Term.fv data))
-              and s = Term.Map.remove key s in
-              (t, ks, s) )
-      in
-      if s' != s then partition_valid_ t' ks' s' else (t', ks', s')
-    in
-    partition_valid_ empty xs s
-end
-
-(** Theory Solver *)
-
-(** prefer representative terms that are minimal in the order s.t. Var <
-    Sized < Extract < Concat < others, then using height of sequence
-    nesting, and then using Term.compare *)
-let prefer e f =
-  let rank e =
-    match (e : Term.t) with
-    | Var _ -> 0
-    | Ap2 (Sized, _, _) -> 1
-    | Ap3 (Extract, _, _, _) -> 2
-    | ApN (Concat, _) -> 3
-    | _ -> 4
-  in
-  let o = compare (rank e) (rank f) in
-  if o <> 0 then o
-  else
-    let o = compare (Term.height e) (Term.height f) in
-    if o <> 0 then o else Term.compare e f
-
-(** orient equations based on representative preference *)
-let orient e f =
-  match Sign.of_int (prefer e f) with
-  | Neg -> Some (e, f)
-  | Zero -> None
-  | Pos -> Some (f, e)
-
-let norm (_, _, s) e = Subst.norm s e
-
-let compose1 ?f ~var ~rep (us, xs, s) =
-  let s =
-    match f with
-    | Some f when not (f var rep) -> s
-    | _ -> Subst.compose1 ~key:var ~data:rep s
-  in
-  Some (us, xs, s)
-
-let fresh name (us, xs, s) =
-  let x, us = Var.fresh name ~wrt:us in
-  let xs = Var.Set.add x xs in
-  (Term.var x, (us, xs, s))
-
-let solve_poly ?f p q s =
-  match Term.sub p q with
-  | Integer {data} -> if Z.equal Z.zero data then Some s else None
-  | Var _ as var -> compose1 ?f ~var ~rep:Term.zero s
-  | p_q -> (
-    match Term.solve_zero_eq p_q with
-    | Some (var, rep) -> compose1 ?f ~var ~rep s
-    | None -> compose1 ?f ~var:p_q ~rep:Term.zero s )
-
-(* α[o,l) = β ==> l = |β| ∧ α = (⟨n,c⟩[0,o) ^ β ^ ⟨n,c⟩[o+l,n-o-l)) where n
-   = |α| and c fresh *)
-let rec solve_extract ?f a o l b s =
-  let n = Term.seq_size_exn a in
-  let c, s = fresh "c" s in
-  let n_c = Term.sized ~siz:n ~seq:c in
-  let o_l = Term.add o l in
-  let n_o_l = Term.sub n o_l in
-  let c0 = Term.extract ~seq:n_c ~off:Term.zero ~len:o in
-  let c1 = Term.extract ~seq:n_c ~off:o_l ~len:n_o_l in
-  let b, s =
-    match Term.seq_size b with
-    | None -> (Term.sized ~siz:l ~seq:b, Some s)
-    | Some m -> (b, solve_ ?f l m s)
-  in
-  s >>= solve_ ?f a (Term.concat [|c0; b; c1|])
-
-(* α₀^…^αᵢ^αⱼ^…^αᵥ = β ==> |α₀^…^αᵥ| = |β| ∧ … ∧ αⱼ = β[n₀+…+nᵢ,nⱼ) ∧ …
-   where nₓ ≡ |αₓ| and m = |β| *)
-and solve_concat ?f a0V b m s =
-  Iter.fold_until (IArray.to_iter a0V) (s, Term.zero)
-    ~f:(fun aJ (s, oI) ->
-      let nJ = Term.seq_size_exn aJ in
-      let oJ = Term.add oI nJ in
-      match solve_ ?f aJ (Term.extract ~seq:b ~off:oI ~len:nJ) s with
-      | Some s -> `Continue (s, oJ)
-      | None -> `Stop None )
-    ~finish:(fun (s, n0V) -> solve_ ?f n0V m s)
-
-and solve_ ?f d e s =
-  [%Trace.call fun {pf} ->
-    pf "%a@[%a@ %a@ %a@]" Var.Set.pp_xs (snd3 s) Term.pp d Term.pp e
-      Subst.pp (trd3 s)]
-  ;
-  ( match orient (norm s d) (norm s e) with
-  (* e' = f' ==> true when e' ≡ f' *)
-  | None -> Some s
-  (* i = j ==> false when i ≠ j *)
-  | Some (Integer _, Integer _) | Some (Rational _, Rational _) -> None
-  (* ⟨0,a⟩ = β ==> a = β = ⟨⟩ *)
-  | Some (Ap2 (Sized, n, a), b) when Term.equal n Term.zero ->
-      s |> solve_ ?f a (Term.concat [||]) >>= solve_ ?f b (Term.concat [||])
-  | Some (b, Ap2 (Sized, n, a)) when Term.equal n Term.zero ->
-      s |> solve_ ?f a (Term.concat [||]) >>= solve_ ?f b (Term.concat [||])
-  (* v = ⟨n,a⟩ ==> v = a *)
-  | Some ((Var _ as v), Ap2 (Sized, _, a)) -> s |> solve_ ?f v a
-  (* ⟨n,a⟩ = ⟨m,b⟩ ==> n = m ∧ a = β *)
-  | Some (Ap2 (Sized, n, a), Ap2 (Sized, m, b)) ->
-      s |> solve_ ?f n m >>= solve_ ?f a b
-  (* ⟨n,a⟩ = β ==> n = |β| ∧ a = β *)
-  | Some (Ap2 (Sized, n, a), b) ->
-      ( match Term.seq_size b with
-      | None -> Some s
-      | Some m -> solve_ ?f n m s )
-      >>= solve_ ?f a b
-  | Some ((Var _ as v), (Ap3 (Extract, _, _, l) as e)) ->
-      if not (Var.Set.mem (Var.of_ v) (Term.fv e)) then
-        (* v = α[o,l) ==> v ↦ α[o,l) when v ∉ fv(α[o,l)) *)
-        compose1 ?f ~var:v ~rep:e s
-      else
-        (* v = α[o,l) ==> α[o,l) ↦ ⟨l,v⟩ when v ∈ fv(α[o,l)) *)
-        compose1 ?f ~var:e ~rep:(Term.sized ~siz:l ~seq:v) s
-  | Some ((Var _ as v), (ApN (Concat, a0V) as c)) ->
-      if not (Var.Set.mem (Var.of_ v) (Term.fv c)) then
-        (* v = α₀^…^αᵥ ==> v ↦ α₀^…^αᵥ when v ∉ fv(α₀^…^αᵥ) *)
-        compose1 ?f ~var:v ~rep:c s
-      else
-        (* v = α₀^…^αᵥ ==> ⟨|α₀^…^αᵥ|,v⟩ = α₀^…^αᵥ when v ∈ fv(α₀^…^αᵥ) *)
-        let m = Term.seq_size_exn c in
-        solve_concat ?f a0V (Term.sized ~siz:m ~seq:v) m s
-  | Some ((Ap3 (Extract, _, _, l) as e), ApN (Concat, a0V)) ->
-      solve_concat ?f a0V e l s
-  | Some (ApN (Concat, a0V), (ApN (Concat, _) as c)) ->
-      solve_concat ?f a0V c (Term.seq_size_exn c) s
-  | Some (Ap3 (Extract, a, o, l), e) -> solve_extract ?f a o l e s
-  (* p = q ==> p-q = 0 *)
-  | Some
-      ( ((Add _ | Mul _ | Integer _ | Rational _) as p), q
-      | q, ((Add _ | Mul _ | Integer _ | Rational _) as p) ) ->
-      solve_poly ?f p q s
-  | Some (rep, var) ->
-      assert (non_interpreted var) ;
-      assert (non_interpreted rep) ;
-      compose1 ?f ~var ~rep s )
-  |>
-  [%Trace.retn fun {pf} ->
-    function
-    | Some (_, xs, s) -> pf "%a%a" Var.Set.pp_xs xs Subst.pp s
-    | None -> pf "false"]
-
-let solve ?f ~us ~xs d e =
-  [%Trace.call fun {pf} -> pf "%a@ %a" Term.pp d Term.pp e]
-  ;
-  (solve_ ?f d e (us, xs, Subst.empty) |>= fun (_, xs, s) -> (xs, s))
-  |>
-  [%Trace.retn fun {pf} ->
-    function
-    | Some (xs, s) -> pf "%a%a" Var.Set.pp_xs xs Subst.pp s
-    | None -> pf "false"]
-
-(** Equality Relations *)
-
-(** see also [invariant] *)
-type t =
-  { xs: Var.Set.t
-        (** existential variables that did not appear in input equations *)
-  ; sat: bool  (** [false] only if constraints are inconsistent *)
-  ; rep: Subst.t
-        (** functional set of oriented equations: map [a] to [a'],
-            indicating that [a = a'] holds, and that [a'] is the
-            'rep(resentative)' of [a] *) }
-[@@deriving compare, equal, sexp]
-
-type classes = Term.t list Term.Map.t
-
-let classes r =
-  let add key data cls =
-    if Term.equal key data then cls
-    else Term.Map.add_multi ~key:data ~data:key cls
-  in
-  Subst.fold r.rep Term.Map.empty ~f:(fun ~key ~data cls ->
-      match classify key with
-      | Interpreted | Atomic -> add key data cls
-      | Uninterpreted -> add (Term.map ~f:(Subst.apply r.rep) key) data cls )
-
-let cls_of r e =
-  let e' = Subst.apply r.rep e in
-  Term.Map.find e' (classes r) |> Option.value ~default:[e']
-
-(** Pretty-printing *)
-
-let pp fs {sat; rep} =
-  let pp_alist pp_k pp_v fs alist =
-    let pp_assoc fs (k, v) =
-      Format.fprintf fs "[@[%a@ @<2>↦ %a@]]" pp_k k pp_v (k, v)
-    in
-    Format.fprintf fs "[@[<hv>%a@]]" (List.pp ";@ " pp_assoc) alist
-  in
-  let pp_term_v fs (k, v) = if not (Term.equal k v) then Term.pp fs v in
-  Format.fprintf fs "@[{@[<hv>sat= %b;@ rep= %a@]}@]" sat
-    (pp_alist Term.pp pp_term_v)
-    (Iter.to_list (Subst.to_iter rep))
-
-let pp_diff fs (r, s) =
-  let pp_sat fs =
-    if not (Bool.equal r.sat s.sat) then
-      Format.fprintf fs "sat= @[-- %b@ ++ %b@];@ " r.sat s.sat
-  in
-  let pp_rep fs =
-    if not (Subst.is_empty r.rep) then
-      Format.fprintf fs "rep= %a" Subst.pp_diff (r.rep, s.rep)
-  in
-  Format.fprintf fs "@[{@[<hv>%t%t@]}@]" pp_sat pp_rep
-
-let ppx_cls x = List.pp "@ = " (Term.ppx x)
-let pp_cls = ppx_cls (fun _ -> None)
-let pp_diff_cls = List.pp_diff ~cmp:Term.compare "@ = " Term.pp
-
-let ppx_classes x fs clss =
-  List.pp "@ @<2>∧ "
-    (fun fs (rep, cls) ->
-      Format.fprintf fs "@[%a@ = %a@]" (Term.ppx x) rep (ppx_cls x)
-        (List.sort ~cmp:Term.compare cls) )
-    fs
-    (Iter.to_list (Term.Map.to_iter clss))
-
-let pp_classes fs r = ppx_classes (fun _ -> None) fs (classes r)
-
-let pp_diff_clss =
-  Term.Map.pp_diff ~eq:(List.equal Term.equal) Term.pp pp_cls pp_diff_cls
-
-(** Basic queries *)
-
-(** test membership in carrier *)
-let in_car r e = Subst.mem e r.rep
-
-(** congruent specialized to assume subterms of [a'] are [Subst.norm]alized
-    wrt [r] (or canonized) *)
-let semi_congruent r a' b = Term.equal a' (Term.map ~f:(Subst.norm r.rep) b)
-
-(** terms are congruent if equal after normalizing subterms *)
-let congruent r a b = semi_congruent r (Term.map ~f:(Subst.norm r.rep) a) b
-
-(** Invariant *)
-
-let pre_invariant r =
-  let@ () = Invariant.invariant [%here] r [%sexp_of: t] in
-  Subst.iteri r.rep ~f:(fun ~key:trm ~data:_ ->
-      (* no interpreted terms in carrier *)
-      assert (non_interpreted trm || fail "non-interp %a" Term.pp trm ()) ;
-      (* carrier is closed under subterms *)
-      Term.iter trm ~f:(fun subtrm ->
-          assert (
-            (not (non_interpreted subtrm))
-            || Term.is_constant subtrm
-            || in_car r subtrm
-            || fail "@[subterm %a@ of %a@ not in carrier of@ %a@]" Term.pp
-                 subtrm Term.pp trm pp r () ) ) )
-
-let invariant r =
-  let@ () = Invariant.invariant [%here] r [%sexp_of: t] in
-  pre_invariant r ;
-  assert (
-    (not r.sat)
-    || Subst.for_alli r.rep ~f:(fun ~key:a ~data:a' ->
-           Subst.for_alli r.rep ~f:(fun ~key:b ~data:b' ->
-               Term.compare a b >= 0
-               || (not (congruent r a b))
-               || Term.equal a' b'
-               || fail "not congruent %a@ %a@ in@ %a" Term.pp a Term.pp b pp
-                    r () ) ) )
-
-(** Core operations *)
-
-let true_ =
-  let rep = Subst.empty in
-  let rep = Option.get_exn (Subst.extend Term.true_ rep) in
-  let rep = Option.get_exn (Subst.extend Term.false_ rep) in
-  {xs= Var.Set.empty; sat= true; rep} |> check invariant
-
-let false_ = {true_ with sat= false}
-
-(** [lookup r a] is [b'] if [a ~ b = b'] for some equation [b = b'] in rep *)
-let lookup r a =
-  ([%Trace.call fun {pf} -> pf "%a" Term.pp a]
-  ;
-  Iter.find_map (Subst.to_iter r.rep) ~f:(fun (b, b') ->
-      Option.return_if (semi_congruent r a b) b' )
-  |> Option.value ~default:a)
-  |>
-  [%Trace.retn fun {pf} -> pf "%a" Term.pp]
-
-(** rewrite a term into canonical form using rep and, for non-interpreted
-    terms, congruence composed with rep *)
-let rec canon r a =
-  [%Trace.call fun {pf} -> pf "%a" Term.pp a]
-  ;
-  ( match classify a with
-  | Atomic -> Subst.apply r.rep a
-  | Interpreted -> Term.map ~f:(canon r) a
-  | Uninterpreted -> (
-      let a' = Term.map ~f:(canon r) a in
-      match classify a' with
-      | Atomic -> Subst.apply r.rep a'
-      | Interpreted -> a'
-      | Uninterpreted -> lookup r a' ) )
-  |>
-  [%Trace.retn fun {pf} -> pf "%a" Term.pp]
-
-let rec extend_ a r =
-  match (a : Term.t) with
-  | Integer _ | Rational _ -> r
-  | _ -> (
-      if interpreted a then Term.fold ~f:extend_ a r
-      else
-        (* add uninterpreted terms *)
-        match Subst.extend a r with
-        (* and their subterms if newly added *)
-        | Some r -> Term.fold ~f:extend_ a r
-        | None -> r )
-
-(** add a term to the carrier *)
-let extend a r =
-  let rep = extend_ a r.rep in
-  if rep == r.rep then r else {r with rep} |> check pre_invariant
-
-let merge us a b r =
-  [%Trace.call fun {pf} -> pf "%a@ %a@ %a" Term.pp a Term.pp b pp r]
-  ;
-  ( match solve ~us ~xs:r.xs a b with
-  | Some (xs, s) ->
-      {r with xs= Var.Set.union r.xs xs; rep= Subst.compose r.rep s}
-  | None -> {r with sat= false} )
-  |>
-  [%Trace.retn fun {pf} r' ->
-    pf "%a" pp_diff (r, r') ;
-    pre_invariant r']
-
-(** find an unproved equation between congruent terms *)
-let find_missing r =
-  Iter.find_map (Subst.to_iter r.rep) ~f:(fun (a, a') ->
-      let a_subnorm = Term.map ~f:(Subst.norm r.rep) a in
-      Iter.find_map (Subst.to_iter r.rep) ~f:(fun (b, b') ->
-          (* need to equate a' and b'? *)
-          let need_a'_eq_b' =
-            (* optimize: do not consider both a = b and b = a *)
-            Term.compare a b < 0
-            (* a and b are not already equal *)
-            && (not (Term.equal a' b'))
-            (* a and b are congruent *)
-            && semi_congruent r a_subnorm b
-          in
-          Option.return_if need_a'_eq_b' (a', b') ) )
-
-let rec close us r =
-  if not r.sat then r
-  else
-    match find_missing r with
-    | Some (a', b') -> close us (merge us a' b' r)
-    | None -> r
-
-let close us r =
-  [%Trace.call fun {pf} -> pf "%a" pp r]
-  ;
-  close us r
-  |>
-  [%Trace.retn fun {pf} r' ->
-    pf "%a" pp_diff (r, r') ;
-    invariant r']
-
-let and_eq_ us a b r =
-  if not r.sat then r
-  else
-    let r0 = r in
-    let a' = canon r a in
-    let b' = canon r b in
-    let r = extend a' r in
-    let r = extend b' r in
-    if Term.equal a' b' then r
-    else
-      let r = merge us a' b' r in
-      match (a, b) with
-      | (Var _ as v), _ when not (in_car r0 v) -> r
-      | _, (Var _ as v) when not (in_car r0 v) -> r
-      | _ -> close us r
-
-let extract_xs r = (r.xs, {r with xs= Var.Set.empty})
-
-(** Exposed interface *)
-
-let is_true {sat; rep} =
-  sat && Subst.for_alli rep ~f:(fun ~key:a ~data:a' -> Term.equal a a')
-
-let is_false {sat} = not sat
-
-let implies r b =
-  [%Trace.call fun {pf} -> pf "%a@ %a" Term.pp b pp r]
-  ;
-  Term.is_true (canon r b)
-  |>
-  [%Trace.retn fun {pf} -> pf "%b"]
-
-let normalize = canon
-
-let class_of r e =
-  let e' = normalize r e in
-  e' :: Term.Map.find_multi e' (classes r)
-
-let fold_uses_of r t s ~f =
-  let rec fold_ e s ~f =
-    let s =
-      Term.fold e s ~f:(fun sub s -> if Term.equal t sub then f s e else s)
-    in
-    if interpreted e then Term.fold ~f:(fold_ ~f) e s else s
-  in
-  Subst.fold r.rep s ~f:(fun ~key:trm ~data:rep s ->
-      fold_ ~f trm (fold_ ~f rep s) )
-
-let apply_subst us s r =
-  [%Trace.call fun {pf} -> pf "%a@ %a" Subst.pp s pp r]
-  ;
-  Term.Map.fold (classes r) true_ ~f:(fun ~key:rep ~data:cls r ->
-      let rep' = Subst.subst s rep in
-      List.fold cls r ~f:(fun trm r ->
-          let trm' = Subst.subst s trm in
-          and_eq_ us trm' rep' r ) )
-  |> extract_xs
-  |>
-  [%Trace.retn fun {pf} (xs, r') ->
-    pf "%a%a" Var.Set.pp_xs xs pp_diff (r, r') ;
-    invariant r']
-
-let and_ us r s =
-  [%Trace.call fun {pf} -> pf "@[<hv 1>   %a@ @<2>∧ %a@]" pp r pp s]
-  ;
-  ( if not r.sat then r
-  else if not s.sat then s
-  else
-    let s, r =
-      if Subst.length s.rep <= Subst.length r.rep then (s, r) else (r, s)
-    in
-    Subst.fold s.rep r ~f:(fun ~key:e ~data:e' r -> and_eq_ us e e' r) )
-  |> extract_xs
-  |>
-  [%Trace.retn fun {pf} (_, r') ->
-    pf "%a" pp_diff (r, r') ;
-    invariant r']
-
-let or_ us r s =
-  [%Trace.call fun {pf} -> pf "@[<hv 1>   %a@ @<2>∨ %a@]" pp r pp s]
-  ;
-  ( if not s.sat then r
-  else if not r.sat then s
-  else
-    let merge_mems rs r s =
-      Term.Map.fold (classes s) rs ~f:(fun ~key:rep ~data:cls rs ->
-          List.fold cls
-            ([rep], rs)
-            ~f:(fun exp (reps, rs) ->
-              match
-                List.find ~f:(fun rep -> implies r (Term.eq exp rep)) reps
-              with
-              | Some rep -> (reps, and_eq_ us exp rep rs)
-              | None -> (exp :: reps, rs) )
-          |> snd )
-    in
-    let rs = true_ in
-    let rs = merge_mems rs r s in
-    let rs = merge_mems rs s r in
-    rs )
-  |> extract_xs
-  |>
-  [%Trace.retn fun {pf} (_, r') ->
-    pf "%a" pp_diff (r, r') ;
-    invariant r']
-
-let orN us rs =
-  match rs with
-  | [] -> (us, false_)
-  | r :: rs -> List.fold ~f:(fun r (us, s) -> or_ us s r) rs (us, r)
-
-let rec and_term_ us e r =
-  let eq_false b r = and_eq_ us b Term.false_ r in
-  match (e : Term.t) with
-  | Integer {data} -> if Z.is_false data then false_ else r
-  | And cs -> Term.Set.fold ~f:(and_term_ us) cs r
-  | Ap2 (Eq, a, b) -> and_eq_ us a b r
-  | Ap2 (Xor, Integer {data}, a) when Z.is_true data -> eq_false a r
-  | Ap2 (Xor, a, Integer {data}) when Z.is_true data -> eq_false a r
-  | _ -> r
-
-let and_term us e r =
-  [%Trace.call fun {pf} -> pf "%a@ %a" Term.pp e pp r]
-  ;
-  and_term_ us e r |> extract_xs
-  |>
-  [%Trace.retn fun {pf} (_, r') ->
-    pf "%a" pp_diff (r, r') ;
-    invariant r']
-
-let and_eq us a b r =
-  [%Trace.call fun {pf} -> pf "%a = %a@ %a" Term.pp a Term.pp b pp r]
-  ;
-  and_eq_ us a b r |> extract_xs
-  |>
-  [%Trace.retn fun {pf} (_, r') ->
-    pf "%a" pp_diff (r, r') ;
-    invariant r']
-
-let rename r sub =
-  [%Trace.call fun {pf} -> pf "%a" pp r]
-  ;
-  let rep = Subst.map_entries ~f:(Term.rename sub) r.rep in
-  (if rep == r.rep then r else {r with rep})
-  |>
-  [%Trace.retn fun {pf} r' ->
-    pf "%a" pp_diff (r, r') ;
-    invariant r']
-
-let fold_terms r z ~f =
-  Subst.fold ~f:(fun ~key ~data z -> f key (f data z)) r.rep z
-
-let fold_vars r z ~f = fold_terms ~f:(Term.fold_vars ~f) r z
-
-(** Existential Witnessing and Elimination *)
-
-let subst_invariant us s0 s =
-  assert (s0 == s || not (Subst.equal s0 s)) ;
-  assert (
-    Subst.iteri s ~f:(fun ~key ~data ->
-        (* dom of new entries not ito us *)
-        assert (
-          Option.for_all ~f:(Term.equal data) (Subst.find key s0)
-          || not (Var.Set.subset (Term.fv key) ~of_:us) ) ;
-        (* rep not ito us implies trm not ito us *)
-        assert (
-          Var.Set.subset (Term.fv data) ~of_:us
-          || not (Var.Set.subset (Term.fv key) ~of_:us) ) ) ;
-    true )
-
-type 'a zom = Zero | One of 'a | Many
-
-(** try to solve [p = q] such that [fv (p - q) ⊆ us ∪ xs] and [p - q]
-    has at most one maximal solvable subterm, [kill], where
-    [fv kill ⊈ us]; solve [p = q] for [kill]; extend subst mapping [kill]
-    to the solution *)
-let solve_poly_eq us p' q' subst =
-  [%Trace.call fun {pf} -> pf "%a = %a" Term.pp p' Term.pp q']
-  ;
-  let diff = Term.sub p' q' in
-  let max_solvables_not_ito_us =
-    fold_max_solvables diff Zero ~f:(fun solvable_subterm -> function
-      | Many -> Many
-      | zom when Var.Set.subset (Term.fv solvable_subterm) ~of_:us -> zom
-      | One _ -> Many
-      | Zero -> One solvable_subterm )
-  in
-  ( match max_solvables_not_ito_us with
-  | One kill ->
-      let+ kill, keep = Term.solve_zero_eq diff ~for_:kill in
-      Subst.compose1 ~key:kill ~data:keep subst
-  | Many | Zero -> None )
-  |>
-  [%Trace.retn fun {pf} subst' ->
-    pf "@[%a@]" Subst.pp_diff (subst, Option.value subst' ~default:subst)]
-
-let solve_seq_eq us e' f' subst =
-  [%Trace.call fun {pf} -> pf "%a = %a" Term.pp e' Term.pp f']
-  ;
-  let f x u =
-    (not (Var.Set.subset (Term.fv x) ~of_:us))
-    && Var.Set.subset (Term.fv u) ~of_:us
-  in
-  let solve_concat ms n a =
-    let a, n =
-      match Term.seq_size a with
-      | Some n -> (a, n)
-      | None -> (Term.sized ~siz:n ~seq:a, n)
-    in
-    let+ _, xs, s = solve_concat ~f ms a n (us, Var.Set.empty, subst) in
-    assert (Var.Set.is_empty xs) ;
-    s
-  in
-  ( match ((e' : Term.t), (f' : Term.t)) with
-  | (ApN (Concat, ms) as c), a when f c a ->
-      solve_concat ms (Term.seq_size_exn c) a
-  | a, (ApN (Concat, ms) as c) when f c a ->
-      solve_concat ms (Term.seq_size_exn c) a
-  | (Ap2 (Sized, _, (Var _ as v)) as m), u when f m u ->
-      Some (Subst.compose1 ~key:v ~data:u subst)
-  | u, (Ap2 (Sized, _, (Var _ as v)) as m) when f m u ->
-      Some (Subst.compose1 ~key:v ~data:u subst)
-  | _ -> None )
-  |>
-  [%Trace.retn fun {pf} subst' ->
-    pf "@[%a@]" Subst.pp_diff (subst, Option.value subst' ~default:subst)]
-
-let solve_interp_eq us e' (cls, subst) =
-  [%Trace.call fun {pf} ->
-    pf "trm: @[%a@]@ cls: @[%a@]@ subst: @[%a@]" Term.pp e' pp_cls cls
-      Subst.pp subst]
-  ;
-  List.find_map cls ~f:(fun f ->
-      let f' = Subst.norm subst f in
-      match solve_seq_eq us e' f' subst with
-      | Some subst -> Some subst
-      | None -> solve_poly_eq us e' f' subst )
-  |>
-  [%Trace.retn fun {pf} subst' ->
-    pf "@[%a@]" Subst.pp_diff (subst, Option.value subst' ~default:subst) ;
-    Option.iter ~f:(subst_invariant us subst) subst']
-
-(** move equations from [cls] to [subst] which are between interpreted terms
-    and can be expressed, after normalizing with [subst], as [x ↦ u] where
-    [us ∪ xs ⊇ fv x ⊈ us] and [fv u ⊆ us] or else
-    [fv u ⊆ us ∪ xs] *)
-let rec solve_interp_eqs us (cls, subst) =
-  [%Trace.call fun {pf} ->
-    pf "cls: @[%a@]@ subst: @[%a@]" pp_cls cls Subst.pp subst]
-  ;
-  let rec solve_interp_eqs_ cls' (cls, subst) =
-    match cls with
-    | [] -> (cls', subst)
-    | trm :: cls ->
-        let trm' = Subst.norm subst trm in
-        if interpreted trm' then
-          match solve_interp_eq us trm' (cls, subst) with
-          | Some subst -> solve_interp_eqs_ cls' (cls, subst)
-          | None -> solve_interp_eqs_ (trm' :: cls') (cls, subst)
-        else solve_interp_eqs_ (trm' :: cls') (cls, subst)
-  in
-  let cls', subst' = solve_interp_eqs_ [] (cls, subst) in
-  ( if subst' != subst then solve_interp_eqs us (cls', subst')
-  else (cls', subst') )
-  |>
-  [%Trace.retn fun {pf} (cls', subst') ->
-    pf "cls: @[%a@]@ subst: @[%a@]" pp_diff_cls (cls, cls') Subst.pp_diff
-      (subst, subst')]
-
-type cls_solve_state =
-  { rep_us: Term.t option  (** rep, that is ito us, for class *)
-  ; cls_us: Term.t list  (** cls that is ito us, or interpreted *)
-  ; rep_xs: Term.t option  (** rep, that is *not* ito us, for class *)
-  ; cls_xs: Term.t list  (** cls that is *not* ito us *) }
-
-let dom_trm e =
-  match (e : Term.t) with
-  | Ap2 (Sized, _, (Var _ as v)) -> Some v
-  | _ when non_interpreted e -> Some e
-  | _ -> None
-
-(** move equations from [cls] (which is assumed to be normalized by [subst])
-    to [subst] which can be expressed as [x ↦ u] where [x] is
-    non-interpreted [us ∪ xs ⊇ fv x ⊈ us] and [fv u ⊆ us] or else
-    [fv u ⊆ us ∪ xs] *)
-let solve_uninterp_eqs us (cls, subst) =
-  [%Trace.call fun {pf} ->
-    pf "cls: @[%a@]@ subst: @[%a@]" pp_cls cls Subst.pp subst]
-  ;
-  let compare e f =
-    [%compare: kind * Term.t] (classify e, e) (classify f, f)
-  in
-  let {rep_us; cls_us; rep_xs; cls_xs} =
-    List.fold cls {rep_us= None; cls_us= []; rep_xs= None; cls_xs= []}
-      ~f:(fun trm ({rep_us; cls_us; rep_xs; cls_xs} as s) ->
-        if Var.Set.subset (Term.fv trm) ~of_:us then
-          match rep_us with
-          | Some rep when compare rep trm <= 0 ->
-              {s with cls_us= trm :: cls_us}
-          | Some rep -> {s with rep_us= Some trm; cls_us= rep :: cls_us}
-          | None -> {s with rep_us= Some trm}
-        else
-          match rep_xs with
-          | Some rep -> (
-              if compare rep trm <= 0 then
-                match dom_trm trm with
-                | Some trm -> {s with cls_xs= trm :: cls_xs}
-                | None -> {s with cls_us= trm :: cls_us}
-              else
-                match dom_trm rep with
-                | Some rep ->
-                    {s with rep_xs= Some trm; cls_xs= rep :: cls_xs}
-                | None -> {s with rep_xs= Some trm; cls_us= rep :: cls_us} )
-          | None -> {s with rep_xs= Some trm} )
-  in
-  ( match rep_us with
-  | Some rep_us ->
-      let cls = rep_us :: cls_us in
-      let cls, cls_xs =
-        match rep_xs with
-        | Some rep -> (
-          match dom_trm rep with
-          | Some rep -> (cls, rep :: cls_xs)
-          | None -> (rep :: cls, cls_xs) )
-        | None -> (cls, cls_xs)
-      in
-      let subst =
-        List.fold cls_xs subst ~f:(fun trm_xs subst ->
-            Subst.compose1 ~key:trm_xs ~data:rep_us subst )
-      in
-      (cls, subst)
-  | None -> (
-    match rep_xs with
-    | Some rep_xs ->
-        let cls = rep_xs :: cls_us in
-        let subst =
-          List.fold cls_xs subst ~f:(fun trm_xs subst ->
-              Subst.compose1 ~key:trm_xs ~data:rep_xs subst )
-        in
-        (cls, subst)
-    | None -> (cls, subst) ) )
-  |>
-  [%Trace.retn fun {pf} (cls', subst') ->
-    pf "cls: @[%a@]@ subst: @[%a@]" pp_diff_cls (cls, cls') Subst.pp_diff
-      (subst, subst') ;
-    subst_invariant us subst subst']
-
-(** move equations between terms in [rep]'s class [cls] from [classes] to
-    [subst] which can be expressed, after normalizing with [subst], as
-    [x ↦ u] where [us ∪ xs ⊇ fv x ⊈ us] and [fv u ⊆ us] or else
-    [fv u ⊆ us ∪ xs] *)
-let solve_class us us_xs ~key:rep ~data:cls (classes, subst) =
-  let classes0 = classes in
-  [%Trace.call fun {pf} ->
-    pf "rep: @[%a@]@ cls: @[%a@]@ subst: @[%a@]" Term.pp rep pp_cls cls
-      Subst.pp subst]
-  ;
-  let cls, cls_not_ito_us_xs =
-    List.partition
-      ~f:(fun e -> Var.Set.subset (Term.fv e) ~of_:us_xs)
-      (rep :: cls)
-  in
-  let cls, subst = solve_interp_eqs us (cls, subst) in
-  let cls, subst = solve_uninterp_eqs us (cls, subst) in
-  let cls = List.rev_append cls_not_ito_us_xs cls in
-  let cls = List.remove ~eq:Term.equal (Subst.norm subst rep) cls in
-  let classes =
-    if List.is_empty cls then Term.Map.remove rep classes
-    else Term.Map.add ~key:rep ~data:cls classes
-  in
-  (classes, subst)
-  |>
-  [%Trace.retn fun {pf} (classes', subst') ->
-    pf "subst: @[%a@]@ classes: @[%a@]" Subst.pp_diff (subst, subst')
-      pp_diff_clss (classes0, classes')]
-
-let solve_concat_extracts_eq r x =
-  [%Trace.call fun {pf} -> pf "%a@ %a" Term.pp x pp r]
-  ;
-  let uses =
-    fold_uses_of r x [] ~f:(fun uses -> function
-      | Ap2 (Sized, _, _) as m ->
-          fold_uses_of r m uses ~f:(fun uses -> function
-            | Ap3 (Extract, _, _, _) as e -> e :: uses | _ -> uses )
-      | _ -> uses )
-  in
-  let find_extracts_at_off off =
-    List.filter uses ~f:(fun use ->
-        match (use : Term.t) with
-        | Ap3 (Extract, _, o, _) -> implies r (Term.eq o off)
-        | _ -> false )
-  in
-  let rec find_extracts full_rev_extracts rev_prefix off =
-    List.fold (find_extracts_at_off off) full_rev_extracts
-      ~f:(fun e full_rev_extracts ->
-        match e with
-        | Ap3 (Extract, Ap2 (Sized, n, _), o, l) ->
-            let o_l = Term.add o l in
-            if implies r (Term.eq n o_l) then
-              (e :: rev_prefix) :: full_rev_extracts
-            else find_extracts full_rev_extracts (e :: rev_prefix) o_l
-        | _ -> full_rev_extracts )
-  in
-  find_extracts [] [] Term.zero
-  |>
-  [%Trace.retn fun {pf} ->
-    pf "@[[%a]@]" (List.pp ";@ " (List.pp ",@ " Term.pp))]
-
-let solve_concat_extracts r us x (classes, subst, us_xs) =
-  match
-    List.filter_map (solve_concat_extracts_eq r x) ~f:(fun rev_extracts ->
-        Iter.fold_opt (Iter.of_list rev_extracts) [] ~f:(fun e suffix ->
-            let+ rep_ito_us =
-              List.fold (cls_of r e) None ~f:(fun trm rep_ito_us ->
-                  match rep_ito_us with
-                  | Some rep when Term.compare rep trm <= 0 -> rep_ito_us
-                  | _ when Var.Set.subset (Term.fv trm) ~of_:us -> Some trm
-                  | _ -> rep_ito_us )
-            in
-            Term.sized ~siz:(Term.seq_size_exn e) ~seq:rep_ito_us :: suffix ) )
-    |> Iter.of_list
-    |> Iter.min ~lt:(fun xs ys -> [%compare: Term.t list] xs ys < 0)
-  with
-  | Some extracts ->
-      let concat = Term.concat (Array.of_list extracts) in
-      let subst = Subst.compose1 ~key:x ~data:concat subst in
-      (classes, subst, us_xs)
-  | None -> (classes, subst, us_xs)
-
-let solve_for_xs r us xs =
-  Var.Set.fold xs ~f:(fun x (classes, subst, us_xs) ->
-      let x = Term.var x in
-      if Subst.mem x subst then (classes, subst, us_xs)
-      else solve_concat_extracts r us x (classes, subst, us_xs) )
-
-(** move equations from [classes] to [subst] which can be expressed, after
-    normalizing with [subst], as [x ↦ u] where [us ∪ xs ⊇ fv x ⊈ us]
-    and [fv u ⊆ us] or else [fv u ⊆ us ∪ xs]. *)
-let solve_classes r xs (classes, subst, us) =
-  [%Trace.call fun {pf} ->
-    pf "us: {@[%a@]}@ xs: {@[%a@]}" Var.Set.pp us Var.Set.pp xs]
-  ;
-  let rec solve_classes_ (classes0, subst0, us_xs) =
-    let classes, subst =
-      Term.Map.fold ~f:(solve_class us us_xs) classes0 (classes0, subst0)
-    in
-    if subst != subst0 then solve_classes_ (classes, subst, us_xs)
-    else (classes, subst, us_xs)
-  in
-  (classes, subst, Var.Set.union us xs)
-  |> solve_classes_
-  |> solve_for_xs r us xs
-  |>
-  [%Trace.retn fun {pf} (classes', subst', _) ->
-    pf "subst: @[%a@]@ classes: @[%a@]" Subst.pp_diff (subst, subst')
-      pp_diff_clss (classes, classes')]
-
-let pp_vss fs vss =
-  Format.fprintf fs "[@[%a@]]"
-    (List.pp ";@ " (fun fs vs -> Format.fprintf fs "{@[%a@]}" Var.Set.pp vs))
-    vss
-
-(** enumerate variable contexts vᵢ in [v₁;…] and accumulate a solution
-    subst with entries [x ↦ u] where [r] entails [x = u] and
-    [⋃ⱼ₌₁ⁱ vⱼ ⊇ fv x ⊈ ⋃ⱼ₌₁ⁱ⁻¹ vⱼ] and
-    [fv u ⊆ ⋃ⱼ₌₁ⁱ⁻¹ vⱼ] if possible and otherwise
-    [fv u ⊆ ⋃ⱼ₌₁ⁱ vⱼ] *)
-let solve_for_vars vss r =
-  [%Trace.call fun {pf} ->
-    pf "%a@ @[%a@]@ @[%a@]" pp_vss vss pp_classes r pp r ;
-    invariant r]
-  ;
-  let us, vss =
-    match vss with us :: vss -> (us, vss) | [] -> (Var.Set.empty, vss)
-  in
-  List.fold ~f:(solve_classes r) vss (classes r, Subst.empty, us) |> snd3
-  |>
-  [%Trace.retn fun {pf} subst ->
-    pf "%a" Subst.pp subst ;
-    Subst.iteri subst ~f:(fun ~key ~data ->
-        assert (
-          implies r (Term.eq key data)
-          || fail "@[%a@ = %a@ not entailed by@ @[%a@]@]" Term.pp key
-               Term.pp data pp_classes r () ) ;
-        assert (
-          Iter.fold_until (Iter.of_list vss) us
-            ~f:(fun xs us ->
-              let us_xs = Var.Set.union us xs in
-              let ks = Term.fv key in
-              let ds = Term.fv data in
-              if
-                Var.Set.subset ks ~of_:us_xs
-                && Var.Set.subset ds ~of_:us_xs
-                && ( Var.Set.subset ds ~of_:us
-                   || not (Var.Set.subset ks ~of_:us) )
-              then `Stop true
-              else `Continue us_xs )
-            ~finish:(fun _ -> false) ) )]
-
-let elim xs r = {r with rep= Subst.remove xs r.rep}
diff --git a/sledge/src/ses/equality.mli b/sledge/src/ses/equality.mli
deleted file mode 100644
index 68f2f100c..000000000
--- a/sledge/src/ses/equality.mli
+++ /dev/null
@@ -1,100 +0,0 @@
-(*
- * 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.
- *)
-
-(** Constraints representing equivalence relations over uninterpreted
-    functions and linear rational arithmetic.
-
-    Functions that return relations that might be stronger than their
-    argument relations accept and return a set of variables. The input set
-    is the variables with which any generated variables must be chosen
-    fresh, and the output set is the variables that have been generated. *)
-
-type t [@@deriving compare, equal, sexp]
-type classes = Term.t list Term.Map.t
-
-val classes : t -> classes
-(** [classes r] maps each equivalence class representative to the other
-    terms [r] proves equal to it. *)
-
-val pp : t pp
-val pp_classes : t pp
-val ppx_classes : Var.strength -> classes pp
-
-include Invariant.S with type t := t
-
-val true_ : t
-(** The diagonal relation, which only equates each term with itself. *)
-
-val and_eq : Var.Set.t -> Term.t -> Term.t -> t -> Var.Set.t * t
-(** Conjoin an equation to a relation. *)
-
-val and_term : Var.Set.t -> Term.t -> t -> Var.Set.t * t
-(** Conjoin a (Boolean) term to a relation. *)
-
-val and_ : Var.Set.t -> t -> t -> Var.Set.t * t
-(** Conjunction. *)
-
-val or_ : Var.Set.t -> t -> t -> Var.Set.t * t
-(** Disjunction. *)
-
-val orN : Var.Set.t -> t list -> Var.Set.t * t
-(** Nary disjunction. *)
-
-val rename : t -> (Var.t -> Var.t) -> t
-(** Apply a renaming substitution to the relation. *)
-
-val is_true : t -> bool
-(** Test if the relation is diagonal. *)
-
-val is_false : t -> bool
-(** Test if the relation is empty / inconsistent. *)
-
-val implies : t -> Term.t -> bool
-(** Test if a term is implied by a relation. *)
-
-val class_of : t -> Term.t -> Term.t list
-(** Equivalence class of [e]: all the terms [f] in the relation such that
-    [e = f] is implied by the relation. *)
-
-val normalize : t -> Term.t -> Term.t
-(** Normalize a term [e] to [e'] such that [e = e'] is implied by the
-    relation, where [e'] and its subterms are expressed in terms of the
-    relation's canonical representatives of each equivalence class. *)
-
-val fold_vars : t -> 's -> f:(Var.t -> 's -> 's) -> 's
-
-(** Solution Substitutions *)
-module Subst : sig
-  type t [@@deriving compare, equal, sexp]
-
-  val pp : t pp
-  val is_empty : t -> bool
-  val fold : t -> 's -> f:(key:Term.t -> data:Term.t -> 's -> 's) -> 's
-
-  val subst : t -> Term.t -> Term.t
-  (** Apply a substitution recursively to subterms. *)
-
-  val partition_valid : Var.Set.t -> t -> t * Var.Set.t * t
-  (** Partition ∃xs. σ into equivalent ∃xs. τ ∧ ∃ks. ν where ks
-      and ν are maximal where ∃ks. ν is universally valid, xs ⊇ ks and
-      ks ∩ fv(τ) = ∅. *)
-end
-
-val apply_subst : Var.Set.t -> Subst.t -> t -> Var.Set.t * t
-(** Relation induced by applying a substitution to a set of equations
-    generating the argument relation. *)
-
-val solve_for_vars : Var.Set.t list -> t -> Subst.t
-(** [solve_for_vars vss r] is a solution substitution that is entailed by
-    [r] and consists of oriented equalities [x ↦ e] that map terms [x]
-    with free variables contained in (the union of) a prefix [uss] of [vss]
-    to terms [e] with free variables contained in as short a prefix of [uss]
-    as possible. *)
-
-val elim : Var.Set.t -> t -> t
-(** Weaken relation by removing oriented equations [k ↦ _] for [k] in
-    [ks]. *)
diff --git a/sledge/src/ses/term.ml b/sledge/src/ses/term.ml
deleted file mode 100644
index 625cae597..000000000
--- a/sledge/src/ses/term.ml
+++ /dev/null
@@ -1,1217 +0,0 @@
-(*
- * 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.
- *)
-
-(** Terms *)
-
-[@@@warning "+9"]
-
-type op1 =
-  | Signed of {bits: int}
-  | Unsigned of {bits: int}
-  | Splat
-  | Select of int
-[@@deriving compare, equal, hash, sexp]
-
-type op2 =
-  | Eq
-  | Dq
-  | Lt
-  | Le
-  | Div
-  | Rem
-  | Xor
-  | Shl
-  | Lshr
-  | Ashr
-  | Sized
-  | Update of int
-[@@deriving compare, equal, hash, sexp]
-
-type op3 = Conditional | Extract [@@deriving compare, equal, hash, sexp]
-type opN = Concat | Record [@@deriving compare, equal, hash, sexp]
-
-module rec Set : sig
-  include NS.Set.S with type elt := T.t
-
-  val t_of_sexp : Sexp.t -> t
-end = struct
-  include NS.Set.Make (T)
-  include Provide_of_sexp (T)
-end
-
-and Qset : sig
-  include NS.Multiset.S with type mul := Q.t with type elt := T.t
-
-  val t_of_sexp : Sexp.t -> t
-end = struct
-  include NS.Multiset.Make (Q) (T)
-
-  let t_of_sexp = t_of_sexp T.t_of_sexp
-end
-
-and T : sig
-  type set = Set.t [@@deriving compare, equal, sexp]
-  type qset = Qset.t [@@deriving compare, equal, sexp]
-
-  type t =
-    | Var of {id: int; name: string}
-    | Ap1 of op1 * t
-    | Ap2 of op2 * t * t
-    | Ap3 of op3 * t * t * t
-    | ApN of opN * t iarray
-    | And of set
-    | Or of set
-    | Add of qset
-    | Mul of qset
-    | Integer of {data: Z.t}
-    | Rational of {data: Q.t}
-    | RecRecord of int
-    | Apply of Funsym.t * t iarray
-    | PosLit of Predsym.t * t iarray
-    | NegLit of Predsym.t * t iarray
-  [@@deriving compare, equal, sexp]
-end = struct
-  type set = Set.t [@@deriving compare, equal, sexp]
-  type qset = Qset.t [@@deriving compare, equal, sexp]
-
-  type t =
-    | Var of {id: int; name: string}
-    | Ap1 of op1 * t
-    | Ap2 of op2 * t * t
-    | Ap3 of op3 * t * t * t
-    | ApN of opN * t iarray
-    | And of set
-    | Or of set
-    | Add of qset
-    | Mul of qset
-    | Integer of {data: Z.t}
-    | Rational of {data: Q.t}
-    | RecRecord of int
-    | Apply of Funsym.t * t iarray
-    | PosLit of Predsym.t * t iarray
-    | NegLit of Predsym.t * t iarray
-  [@@deriving compare, equal, sexp]
-
-  (* Note: solve (and invariant) requires Qset.min_elt to return a
-     non-coefficient, so Integer and Rational terms must compare higher than
-     any valid monomial *)
-  let compare 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 x y
-
-  let equal 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 x y
-end
-
-include T
-
-module Map = struct
-  include Map.Make (T)
-  include Provide_of_sexp (T)
-end
-
-(** Invariant *)
-
-let assert_conjunction = function
-  | And cs ->
-      Set.iter cs ~f:(fun c ->
-          assert (match c with And _ -> false | _ -> true) )
-  | _ -> assert false
-
-let assert_disjunction = function
-  | Or cs ->
-      Set.iter cs ~f:(fun c ->
-          assert (match c with Or _ -> false | _ -> true) )
-  | _ -> assert false
-
-(* an indeterminate (factor of a monomial) is any
-   non-Add/Mul/Integer/Rational term *)
-let assert_indeterminate = function
-  | Integer _ | Rational _ | Add _ | Mul _ -> assert false
-  | _ -> assert true
-
-(* a monomial is a power product of factors, e.g.
- *     ∏ᵢ xᵢ^nᵢ
- * for (non-constant) indeterminants xᵢ and positive integer exponents nᵢ
- *)
-let assert_monomial mono =
-  match mono with
-  | Mul args ->
-      Qset.iter args ~f:(fun factor exponent ->
-          assert (Z.equal (Q.den exponent) Z.one) ;
-          assert (Q.sign exponent > 0) ;
-          assert_indeterminate factor |> Fun.id )
-  | _ -> assert_indeterminate mono |> Fun.id
-
-(* a polynomial term is a monomial multiplied by a non-zero coefficient
- *     c × ∏ᵢ xᵢ
- *)
-let assert_poly_term mono coeff =
-  assert (Q.is_real coeff) ;
-  assert (Q.sign coeff <> 0) ;
-  match mono with
-  | Integer {data} -> assert (Z.equal Z.one data)
-  | Mul args ->
-      ( match Qset.min_elt args with
-      | None | Some ((Integer _ | Rational _), _) -> assert false
-      | Some (_, n) -> assert (Qset.length args > 1 || not (Q.equal Q.one n))
-      ) ;
-      assert_monomial mono |> Fun.id
-  | _ -> assert_monomial mono |> Fun.id
-
-(* a polynomial is a linear combination of monomials, e.g.
- *     ∑ᵢ cᵢ × ∏ⱼ xᵢⱼ
- * for non-zero constant coefficients cᵢ
- * and monomials ∏ⱼ xᵢⱼ, one of which may be the empty product 1
- *)
-let assert_polynomial poly =
-  match poly with
-  | Add args ->
-      ( match Qset.min_elt args with
-      | None | Some ((Integer _ | Rational _), _) -> assert false
-      | Some (_, k) -> assert (Qset.length args > 1 || not (Q.equal Q.one k))
-      ) ;
-      Qset.iter args ~f:(fun m c -> assert_poly_term m c |> Fun.id)
-  | _ -> assert false
-
-(* sequence args of Extract and Concat must be sequence terms, in
-   particular, not variables *)
-let rec assert_sequence = function
-  | Ap2 (Sized, _, _) -> ()
-  | Ap3 (Extract, a, _, _) -> assert_sequence a
-  | ApN (Concat, a0N) ->
-      assert (IArray.length a0N <> 1) ;
-      IArray.iter ~f:assert_sequence a0N
-  | _ -> assert false
-
-let invariant e =
-  let@ () = Invariant.invariant [%here] e [%sexp_of: t] in
-  match e with
-  | And _ -> assert_conjunction e |> Fun.id
-  | Or _ -> assert_disjunction e |> Fun.id
-  | Add _ -> assert_polynomial e |> Fun.id
-  | Mul _ -> assert_monomial e |> Fun.id
-  | Ap2 (Sized, _, _) | Ap3 (Extract, _, _, _) | ApN (Concat, _) ->
-      assert_sequence e
-  | ApN (Record, elts) -> assert (not (IArray.is_empty elts))
-  | Rational {data} ->
-      assert (Q.is_real data) ;
-      assert (not (Z.equal Z.one (Q.den data)))
-  | _ -> ()
-  [@@warning "-9"]
-
-(** Variables are the terms constructed by [Var] *)
-module Var : sig
-  include Var_intf.VAR with type t = private T.t
-
-  val of_ : T.t -> t
-  val of_term : T.t -> t option
-end = struct
-  let invariant x =
-    let@ () = Invariant.invariant [%here] x [%sexp_of: t] in
-    match x with Var _ -> invariant x | _ -> assert false
-
-  include Var0.Make (struct
-    include T
-
-    let make ~id ~name = Var {id; name} |> check invariant
-    let id = function Var v -> v.id | x -> violates invariant x
-    let name = function Var v -> v.name | x -> violates invariant x
-  end)
-
-  let of_ v = v |> check invariant
-  let of_term = function Var _ as v -> Some v | _ -> None
-end
-
-(** Pretty-print *)
-
-let rec ppx strength fs term =
-  let rec pp fs term =
-    let pf fmt =
-      Format.pp_open_box fs 2 ;
-      Format.kfprintf (fun fs -> Format.pp_close_box fs ()) fs fmt
-    in
-    match term with
-    | Var _ as v -> Var.ppx strength fs (Var.of_ v)
-    | Integer {data} -> Trace.pp_styled `Magenta "%a" fs Z.pp data
-    | Rational {data} -> Trace.pp_styled `Magenta "%a" fs Q.pp data
-    | Ap1 (Signed {bits}, arg) -> pf "((s%i)@ %a)" bits pp arg
-    | Ap1 (Unsigned {bits}, arg) -> pf "((u%i)@ %a)" bits pp arg
-    | Ap2 (Eq, x, y) -> pf "(%a@ = %a)" pp x pp y
-    | Ap2 (Dq, x, y) -> pf "(%a@ @<2>≠ %a)" pp x pp y
-    | Ap2 (Lt, x, y) -> pf "(%a@ < %a)" pp x pp y
-    | Ap2 (Le, x, y) -> pf "(%a@ @<2>≤ %a)" pp x pp y
-    | Add args ->
-        let pp_poly_term fs (monomial, coefficient) =
-          match monomial with
-          | Integer {data} when Z.equal Z.one data -> Q.pp fs coefficient
-          | _ when Q.equal Q.one coefficient -> pp fs monomial
-          | _ ->
-              Format.fprintf fs "%a @<1>× %a" Q.pp coefficient pp monomial
-        in
-        pf "(%a)" (Qset.pp "@ + " pp_poly_term) args
-    | Mul args ->
-        let pp_mono_term fs (factor, exponent) =
-          if Q.equal Q.one exponent then pp fs factor
-          else Format.fprintf fs "%a^%a" pp factor Q.pp exponent
-        in
-        pf "(%a)" (Qset.pp "@ @<2>× " pp_mono_term) args
-    | Ap2 (Div, x, y) -> pf "(%a@ / %a)" pp x pp y
-    | Ap2 (Rem, x, y) -> pf "(%a@ rem %a)" pp x pp y
-    | And xs -> pf "(@[%a@])" (Set.pp ~sep:" &&@ " pp) xs
-    | Or xs -> pf "(@[%a@])" (Set.pp ~sep:" ||@ " pp) xs
-    | Ap2 (Xor, x, Integer {data}) when Z.is_true data -> pf "¬%a" pp x
-    | Ap2 (Xor, Integer {data}, x) when Z.is_true data -> pf "¬%a" pp x
-    | Ap2 (Xor, x, y) -> pf "(%a@ xor %a)" pp x pp y
-    | Ap2 (Shl, x, y) -> pf "(%a@ shl %a)" pp x pp y
-    | Ap2 (Lshr, x, y) -> pf "(%a@ lshr %a)" pp x pp y
-    | Ap2 (Ashr, x, y) -> pf "(%a@ ashr %a)" pp x pp y
-    | Ap3 (Conditional, cnd, thn, els) ->
-        pf "(%a@ ? %a@ : %a)" pp cnd pp thn pp els
-    | Ap3 (Extract, seq, off, len) -> pf "%a[%a,%a)" pp seq pp off pp len
-    | Ap1 (Splat, byt) -> pf "%a^" pp byt
-    | Ap2 (Sized, siz, arr) -> pf "@<1>⟨%a,%a@<1>⟩" pp siz pp arr
-    | ApN (Concat, args) when IArray.is_empty args -> pf "@<2>⟨⟩"
-    | ApN (Concat, args) -> pf "(%a)" (IArray.pp "@,^" pp) args
-    | ApN (Record, elts) -> pf "{%a}" (pp_record strength) elts
-    | Ap1 (Select idx, rcd) -> pf "%a[%i]" pp rcd idx
-    | Ap2 (Update idx, rcd, elt) ->
-        pf "[%a@ @[| %i → %a@]]" pp rcd idx pp elt
-    | RecRecord i -> pf "(rec_record %i)" i
-    | Apply (sym, args) ->
-        pf "(%a@ %a)" Funsym.pp sym (IArray.pp "@ " pp) args
-    | PosLit (sym, args) ->
-        pf "(%a@ %a)" Predsym.pp sym (IArray.pp "@ " pp) args
-    | NegLit (sym, args) ->
-        pf "¬(%a@ %a)" Predsym.pp sym (IArray.pp "@ " pp) args
-  in
-  pp fs term
-  [@@warning "-9"]
-
-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
-              | Integer {data} -> Char.of_int_exn (Z.to_int data)
-              | _ -> 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 strength))
-              elts )
-      elts]
-
-let pp = ppx (fun _ -> None)
-let pp_diff fs (x, y) = Format.fprintf fs "-- %a ++ %a" pp x pp y
-
-(** Construct *)
-
-(* variables *)
-
-let var v = (v : Var.t :> t)
-
-(* constants *)
-
-let integer data = Integer {data} |> check invariant
-
-let rational data =
-  ( if Z.equal Z.one (Q.den data) then Integer {data= Q.num data}
-  else Rational {data} )
-  |> check invariant
-
-let zero = integer Z.zero
-let one = integer Z.one
-let minus_one = integer Z.minus_one
-let bool b = integer (Z.of_bool b)
-let true_ = bool true
-let false_ = bool false
-
-(* type conversions *)
-
-let simp_signed bits arg =
-  match arg with
-  | Integer {data} -> integer (Z.signed_extract data 0 bits)
-  | _ -> Ap1 (Signed {bits}, arg)
-
-let simp_unsigned bits arg =
-  match arg with
-  | Integer {data} -> integer (Z.extract data 0 bits)
-  | _ -> Ap1 (Unsigned {bits}, arg)
-
-(* arithmetic *)
-
-(* Sums of polynomial terms represented by multisets. A sum ∑ᵢ cᵢ × Xᵢ of
-   monomials Xᵢ with coefficients cᵢ is represented by a multiset where the
-   elements are Xᵢ with multiplicities cᵢ. A constant is treated as the
-   coefficient of the empty monomial, which is the unit of multiplication 1. *)
-module Sum = struct
-  let empty = Qset.empty
-
-  let add coeff term sum =
-    assert (not (Q.equal Q.zero coeff)) ;
-    match term with
-    | Integer {data} when Z.equal Z.zero data -> sum
-    | Integer {data} -> Qset.add one Q.(coeff * of_z data) sum
-    | Rational {data} -> Qset.add one Q.(coeff * data) sum
-    | _ -> Qset.add term coeff sum
-
-  let of_ ?(coeff = Q.one) term = add coeff term empty
-  let map sum ~f = Qset.fold ~f:(fun e c sum -> add c (f e) sum) sum empty
-
-  let mul_const const sum =
-    assert (not (Q.equal Q.zero const)) ;
-    if Q.equal Q.one const then sum
-    else Qset.map_counts ~f:(Q.mul const) sum
-
-  let to_term sum =
-    match Qset.classify sum with
-    | `Zero -> zero
-    | `One (arg, q) -> (
-      match arg with
-      | Integer {data} ->
-          assert (Z.equal Z.one data) ;
-          rational q
-      | _ when Q.equal Q.one q -> arg
-      | _ -> Add sum )
-    | `Many -> Add sum
-end
-
-(* Products of indeterminants represented by multisets. A product ∏ᵢ xᵢ^nᵢ
-   of indeterminates xᵢ is represented by a multiset where the elements are
-   xᵢ and the multiplicities are the exponents nᵢ. *)
-module Prod = struct
-  let empty = Qset.empty
-
-  let add term prod =
-    assert (match term with Integer _ | Rational _ -> false | _ -> true) ;
-    Qset.add term Q.one prod
-
-  let of_ term = add term empty
-  let union = Qset.union
-
-  let to_term prod =
-    match Qset.pop prod with
-    | None -> one
-    | Some (factor, power, prod')
-      when Qset.is_empty prod' && Q.equal Q.one power ->
-        factor
-    | _ -> Mul prod
-end
-
-let rec simp_add_ es poly =
-  (* (coeff × term) + poly *)
-  let f term coeff poly =
-    match (term, poly) with
-    (* (0 × e) + s ==> s (optim) *)
-    | _ when Q.equal Q.zero coeff -> poly
-    (* (c × 0) + s ==> s (optim) *)
-    | Integer {data}, _ when Z.equal Z.zero data -> poly
-    (* (c × cᵢ) + cⱼ ==> c×cᵢ+cⱼ *)
-    | Integer {data= i}, Integer {data= j} ->
-        rational Q.((coeff * of_z i) + of_z j)
-    | Rational {data= i}, Rational {data= j} -> rational Q.((coeff * i) + j)
-    (* (c × ∑ᵢ cᵢ × Xᵢ) + s ==> (∑ᵢ (c × cᵢ) × Xᵢ) + s *)
-    | Add args, _ -> simp_add_ (Sum.mul_const coeff args) poly
-    (* (c₀ × X₀) + (∑ᵢ₌₁ⁿ cᵢ × Xᵢ) ==> ∑ᵢ₌₀ⁿ cᵢ × Xᵢ *)
-    | _, Add args -> Sum.to_term (Sum.add coeff term args)
-    (* (c₁ × X₁) + X₂ ==> ∑ᵢ₌₁² cᵢ × Xᵢ for c₂ = 1 *)
-    | _ -> Sum.to_term (Sum.add coeff term (Sum.of_ poly))
-  in
-  Qset.fold ~f es poly
-
-and simp_mul2 e f =
-  match (e, f) with
-  (* c₁ × c₂ ==> c₁×c₂ *)
-  | Integer {data= i}, Integer {data= j} -> integer (Z.mul i j)
-  | Rational {data= i}, Rational {data= j} -> rational (Q.mul i j)
-  (* 0 × f ==> 0 *)
-  | Integer {data}, _ when Z.equal Z.zero data -> e
-  (* e × 0 ==> 0 *)
-  | _, Integer {data} when Z.equal Z.zero data -> f
-  (* c × (∑ᵤ cᵤ × ∏ⱼ yᵤⱼ) ==> ∑ᵤ c × cᵤ × ∏ⱼ yᵤⱼ *)
-  | Integer {data}, Add args | Add args, Integer {data} ->
-      Sum.to_term (Sum.mul_const (Q.of_z data) args)
-  | Rational {data}, Add args | Add args, Rational {data} ->
-      Sum.to_term (Sum.mul_const data args)
-  (* c₁ × x₁ ==> ∑ᵢ₌₁ cᵢ × xᵢ *)
-  | Integer {data= c}, x | x, Integer {data= c} ->
-      Sum.to_term (Sum.of_ ~coeff:(Q.of_z c) x)
-  | Rational {data= c}, x | x, Rational {data= c} ->
-      Sum.to_term (Sum.of_ ~coeff:c x)
-  (* (∏ᵤ₌₀ⁱ xᵤ) × (∏ᵥ₌ᵢ₊₁ⁿ xᵥ) ==> ∏ⱼ₌₀ⁿ xⱼ *)
-  | Mul xs1, Mul xs2 -> Prod.to_term (Prod.union xs1 xs2)
-  (* (∏ᵢ xᵢ) × (∑ᵤ cᵤ × ∏ⱼ yᵤⱼ) ==> ∑ᵤ cᵤ × ∏ᵢ xᵢ × ∏ⱼ yᵤⱼ *)
-  | (Mul prod as m), Add sum | Add sum, (Mul prod as m) ->
-      Sum.to_term
-        (Sum.map sum ~f:(function
-          | Mul args -> Prod.to_term (Prod.union prod args)
-          | (Integer _ | Rational _) as c -> simp_mul2 c m
-          | mono -> Prod.to_term (Prod.add mono prod) ))
-  (* x₀ × (∏ᵢ₌₁ⁿ xᵢ) ==> ∏ᵢ₌₀ⁿ xᵢ *)
-  | Mul xs1, x | x, Mul xs1 -> Prod.to_term (Prod.add x xs1)
-  (* e × (∑ᵤ cᵤ × ∏ⱼ yᵤⱼ) ==> ∑ᵤ e × cᵤ × ∏ⱼ yᵤⱼ *)
-  | Add args, e | e, Add args ->
-      simp_add_ (Sum.map ~f:(fun m -> simp_mul2 e m) args) zero
-  (* x₁ × x₂ ==> ∏ᵢ₌₁² xᵢ *)
-  | _ -> Prod.to_term (Prod.add e (Prod.of_ f))
-
-let simp_div x y =
-  match (x, y) with
-  (* e / 0 ==> e / 0 *)
-  | _, Integer {data} when Z.equal Z.zero data -> Ap2 (Div, x, y)
-  (* e / 1 ==> e *)
-  | e, Integer {data} when Z.equal Z.one data -> e
-  (* e / -1 ==> -1×e *)
-  | e, (Integer {data} as c) when Z.equal Z.minus_one data -> simp_mul2 e c
-  (* i / j ==> i/j *)
-  | Integer {data= i}, Integer {data= j} -> integer (Z.div i j)
-  | Rational {data= i}, Rational {data= j} -> rational (Q.div i j)
-  (* (∑ᵢ cᵢ × Xᵢ) / z ==> ∑ᵢ cᵢ/z × Xᵢ *)
-  | Add args, Integer {data} ->
-      Sum.to_term (Sum.mul_const Q.(inv (of_z data)) args)
-  | Add args, Rational {data} ->
-      Sum.to_term (Sum.mul_const Q.(inv data) args)
-  (* x / n ==> 1/n × x *)
-  | _, Integer {data} -> Sum.to_term (Sum.of_ ~coeff:Q.(inv (of_z data)) x)
-  | _, Rational {data} -> Sum.to_term (Sum.of_ ~coeff:Q.(inv data) x)
-  (* x / y *)
-  | _ -> Ap2 (Div, x, y)
-
-let simp_rem x y =
-  match (x, y) with
-  (* i % j *)
-  | Integer {data= i}, Integer {data= j} when not (Z.equal Z.zero j) ->
-      integer (Z.rem i j)
-  (* (n/d) % i ==> (n / d) % i *)
-  | Rational {data= q}, Integer {data= i} when not (Z.equal Z.zero i) ->
-      integer (Z.rem (Z.div q.num q.den) i)
-  (* e % 1 ==> 0 *)
-  | _, Integer {data} when Z.equal Z.one data -> zero
-  | _ -> Ap2 (Rem, x, y)
-
-let simp_add es = simp_add_ es zero
-let simp_add2 e f = simp_add_ (Sum.of_ e) f
-let simp_negate x = simp_mul2 minus_one x
-
-let simp_sub x y =
-  match (x, y) with
-  (* i - j *)
-  | Integer {data= i}, Integer {data= j} -> integer (Z.sub i j)
-  | Rational {data= i}, Rational {data= j} -> rational (Q.sub i j)
-  (* x - y ==> x + (-1 * y) *)
-  | _ -> simp_add2 x (simp_negate y)
-
-let simp_mul es =
-  (* (bas ^ pwr) × term *)
-  let rec mul_pwr bas pwr term =
-    if Q.equal Q.zero pwr then term
-    else mul_pwr bas Q.(pwr - one) (simp_mul2 bas term)
-  in
-  Qset.fold es one ~f:(fun bas pwr term ->
-      if Q.sign pwr >= 0 then mul_pwr bas pwr term
-      else simp_div term (mul_pwr bas (Q.neg pwr) one) )
-
-(* if-then-else *)
-
-let simp_cond cnd thn els =
-  match cnd with
-  (* (true ? t : e) ==> t *)
-  | Integer {data} when Z.is_true data -> thn
-  (* (false ? t : e) ==> e *)
-  | Integer {data} when Z.is_false data -> els
-  | _ -> Ap3 (Conditional, cnd, thn, els)
-
-(* boolean / bitwise *)
-
-let rec is_boolean = function
-  | Ap1 (Unsigned {bits= 1}, _) | Ap2 ((Eq | Dq | Lt | Le), _, _) -> true
-  | Ap2 ((Div | Rem | Xor | Shl | Lshr | Ashr), x, y)
-   |Ap3 (Conditional, _, x, y) ->
-      is_boolean x || is_boolean y
-  | And xs | Or xs -> Set.for_all ~f:is_boolean xs
-  | _ -> false
-
-let rec simp_and2 x y =
-  match (x, y) with
-  (* i && j *)
-  | Integer {data= i}, Integer {data= j} -> integer (Z.logand i j)
-  (* e && true ==> e *)
-  | (Integer {data}, e | e, Integer {data}) when Z.is_true data -> e
-  (* e && false ==> false *)
-  | ((Integer {data} as f), _ | _, (Integer {data} as f))
-    when Z.is_false data ->
-      f
-  (* e && (c ? t : f) ==> (c ? e && t : e && f) *)
-  | e, Ap3 (Conditional, c, t, f) | Ap3 (Conditional, c, t, f), e ->
-      simp_cond c (simp_and2 e t) (simp_and2 e f)
-  (* e && e ==> e *)
-  | _ when equal x y -> x
-  | _ ->
-      let add s = function And cs -> Set.union s cs | c -> Set.add c s in
-      And (add (add Set.empty x) y)
-
-let simp_and xs = Set.fold ~f:simp_and2 xs true_
-
-let rec simp_or2 x y =
-  match (x, y) with
-  (* i || j *)
-  | Integer {data= i}, Integer {data= j} -> integer (Z.logor i j)
-  (* e || true ==> true *)
-  | ((Integer {data} as t), _ | _, (Integer {data} as t))
-    when Z.is_true data ->
-      t
-  (* e || false ==> e *)
-  | (Integer {data}, e | e, Integer {data}) when Z.is_false data -> e
-  (* e || (c ? t : f) ==> (c ? e || t : e || f) *)
-  | e, Ap3 (Conditional, c, t, f) | Ap3 (Conditional, c, t, f), e ->
-      simp_cond c (simp_or2 e t) (simp_or2 e f)
-  (* e || e ==> e *)
-  | _ when equal x y -> x
-  | _ ->
-      let add s = function Or cs -> Set.union s cs | c -> Set.add c s in
-      Or (add (add Set.empty x) y)
-
-let simp_or xs = Set.fold ~f:simp_or2 xs false_
-
-(* sequence sizes *)
-
-let rec seq_size_exn = function
-  | Ap2 (Sized, n, _) | Ap3 (Extract, _, _, n) -> n
-  | ApN (Concat, a0U) ->
-      IArray.fold
-        ~f:(fun aJ a0I -> simp_add2 a0I (seq_size_exn aJ))
-        a0U zero
-  | _ -> invalid_arg "seq_size_exn"
-
-let seq_size e = try Some (seq_size_exn e) with Invalid_argument _ -> None
-
-(* sequences *)
-
-let empty_seq = ApN (Concat, IArray.of_array [||])
-let simp_splat byt = Ap1 (Splat, byt)
-
-let simp_sized siz arr =
-  (* ⟨n,α⟩ ==> α when n ≡ |α| *)
-  match seq_size arr with
-  | Some n when equal siz n -> arr
-  | _ -> Ap2 (Sized, siz, arr)
-
-type pcmp = Lt | Eq | Gt | Unknown
-
-let partial_compare x y : pcmp =
-  match simp_sub x y with
-  | Integer {data} -> (
-    match Int.sign (Z.sign data) with Neg -> Lt | Zero -> Eq | Pos -> Gt )
-  | Rational {data} -> (
-    match Int.sign (Q.sign data) with Neg -> Lt | Zero -> Eq | Pos -> Gt )
-  | _ -> Unknown
-
-let partial_ge x y =
-  match partial_compare x y with Gt | Eq -> true | Lt | Unknown -> false
-
-let rec simp_extract seq off len =
-  [%Trace.call fun {pf} -> pf "%a" pp (Ap3 (Extract, seq, off, len))]
-  ;
-  (* _[_,0) ==> ⟨⟩ *)
-  ( if equal len zero then empty_seq
-  else
-    let o_l = simp_add2 off len in
-    match seq with
-    (* α[m,k)[o,l) ==> α[m+o,l) when k ≥ o+l *)
-    | Ap3 (Extract, a, m, k) when partial_ge k o_l ->
-        simp_extract a (simp_add2 m off) len
-    (* ⟨n,E^⟩[o,l) ==> ⟨l,E^⟩ when n ≥ o+l *)
-    | Ap2 (Sized, n, (Ap1 (Splat, _) as e)) when partial_ge n o_l ->
-        simp_sized len e
-    (* ⟨n,a⟩[0,n) ==> ⟨n,a⟩ *)
-    | Ap2 (Sized, n, _) when equal off zero && equal n len -> seq
-    (* For (α₀^α₁)[o,l) there are 3 cases:
-     *
-     * ⟨...⟩^⟨...⟩
-     *  [,)
-     * o < o+l ≤ |α₀| : (α₀^α₁)[o,l) ==> α₀[o,l) ^ α₁[0,0)
-     *
-     * ⟨...⟩^⟨...⟩
-     *   [  ,  )
-     * o ≤ |α₀| < o+l : (α₀^α₁)[o,l) ==> α₀[o,|α₀|-o) ^ α₁[0,l-(|α₀|-o))
-     *
-     * ⟨...⟩^⟨...⟩
-     *        [,)
-     * |α₀| ≤ o : (α₀^α₁)[o,l) ==> α₀[o,0) ^ α₁[o-|α₀|,l)
-     *
-     * So in general:
-     *
-     * (α₀^α₁)[o,l) ==> α₀[o,l₀) ^ α₁[o₁,l-l₀)
-     * where l₀ = max 0 (min l |α₀|-o)
-     *       o₁ = max 0 o-|α₀|
-     *)
-    | ApN (Concat, na1N) -> (
-      match len with
-      | Integer {data= l} ->
-          IArray.fold_map_until na1N (l, off)
-            ~f:(fun naI (l, oI) ->
-              let nI = seq_size_exn naI in
-              if Z.equal Z.zero l then
-                `Continue (simp_extract naI oI zero, (l, oI))
-              else
-                let oI_nI = simp_sub oI nI in
-                match oI_nI with
-                | Integer {data} ->
-                    let oJ = if Z.sign data <= 0 then zero else oI_nI in
-                    let lI = Z.(max zero (min l (neg data))) in
-                    let l = Z.(l - lI) in
-                    `Continue (simp_extract naI oI (integer lI), (l, oJ))
-                | _ -> `Stop (Ap3 (Extract, seq, off, len)) )
-            ~finish:(fun (e1N, _) -> simp_concat e1N)
-      | _ -> Ap3 (Extract, seq, off, len) )
-    (* α[o,l) *)
-    | _ -> Ap3 (Extract, seq, off, len) )
-  |>
-  [%Trace.retn fun {pf} -> pf "%a" pp]
-
-and simp_concat xs =
-  [%Trace.call fun {pf} -> pf "%a" pp (ApN (Concat, xs))]
-  ;
-  (* (α^(β^γ)^δ) ==> (α^β^γ^δ) *)
-  let flatten xs =
-    let exists_sub_Concat =
-      IArray.exists ~f:(function ApN (Concat, _) -> true | _ -> false)
-    in
-    let concat_sub_Concat xs =
-      IArray.concat
-        (IArray.fold_right xs [] ~f:(fun x s ->
-             match x with
-             | ApN (Concat, ys) -> ys :: s
-             | x -> IArray.of_array [|x|] :: s ))
-    in
-    if exists_sub_Concat xs then concat_sub_Concat xs else xs
-  in
-  let simp_adjacent e f =
-    match (e, f) with
-    (* ⟨n,a⟩[o,k)^⟨n,a⟩[o+k,l) ==> ⟨n,a⟩[o,k+l) when n ≥ o+k+l *)
-    | ( Ap3 (Extract, (Ap2 (Sized, n, _) as na), o, k)
-      , Ap3 (Extract, na', o_k, l) )
-      when equal na na'
-           && equal o_k (simp_add2 o k)
-           && partial_ge n (simp_add2 o_k l) ->
-        Some (simp_extract na o (simp_add2 k l))
-    (* ⟨m,E^⟩^⟨n,E^⟩ ==> ⟨m+n,E^⟩ *)
-    | Ap2 (Sized, m, (Ap1 (Splat, _) as a)), Ap2 (Sized, n, a')
-      when equal a a' ->
-        Some (simp_sized (simp_add2 m n) a)
-    | _ -> None
-  in
-  let xs = flatten xs in
-  let xs = IArray.reduce_adjacent ~f:simp_adjacent xs in
-  (if IArray.length xs = 1 then IArray.get xs 0 else ApN (Concat, xs))
-  |>
-  [%Trace.retn fun {pf} -> pf "%a" pp]
-
-let simp_poslit sym args = PosLit (sym, args)
-let simp_neglit sym args = NegLit (sym, args)
-
-(* comparison *)
-
-let simp_lt x y =
-  match (x, y) with
-  | Integer {data= i}, Integer {data= j} -> bool (Z.lt i j)
-  | Rational {data= i}, Rational {data= j} -> bool (Q.lt i j)
-  | _ -> Ap2 (Lt, x, y)
-
-let simp_le x y =
-  match (x, y) with
-  | Integer {data= i}, Integer {data= j} -> bool (Z.leq i j)
-  | Rational {data= i}, Rational {data= j} -> bool (Q.leq i j)
-  | _ -> Ap2 (Le, x, y)
-
-let rec simp_eq x y =
-  match
-    match Sign.of_int (compare x y) with
-    | Neg -> Some (x, y)
-    | Zero -> None
-    | Pos -> Some (y, x)
-  with
-  (* e = e ==> true *)
-  | None -> bool true
-  | Some (x, y) -> (
-    match (x, y) with
-    (* i = j ==> false when i ≠ j *)
-    | Integer _, Integer _ | Rational _, Rational _ -> bool false
-    (* b = false ==> ¬b *)
-    | b, Integer {data} when Z.is_false data && is_boolean b -> simp_not b
-    (* b = true ==> b *)
-    | b, Integer {data} when Z.is_true data && is_boolean b -> b
-    (* e = (c ? t : f) ==> (c ? e = t : e = f) *)
-    | e, Ap3 (Conditional, c, t, f) | Ap3 (Conditional, c, t, f), e ->
-        simp_cond c (simp_eq e t) (simp_eq e f)
-    (* α^β^δ = α^γ^δ ==> β = γ *)
-    | ApN (Concat, a), ApN (Concat, b) ->
-        let m = IArray.length a in
-        let n = IArray.length b in
-        let length_common_prefix =
-          let rec find_lcp i =
-            if equal (IArray.get a i) (IArray.get b i) then find_lcp (i + 1)
-            else i
-          in
-          find_lcp 0
-        in
-        let length_common_suffix =
-          let rec find_lcs i =
-            if equal (IArray.get a (m - 1 - i)) (IArray.get b (n - 1 - i))
-            then find_lcs (i + 1)
-            else i
-          in
-          find_lcs 0
-        in
-        let length_common = length_common_prefix + length_common_suffix in
-        if length_common = 0 then Ap2 (Eq, x, y)
-        else
-          let pos = length_common_prefix in
-          let a = IArray.sub ~pos ~len:(m - length_common) a in
-          let b = IArray.sub ~pos ~len:(n - length_common) b in
-          simp_eq (simp_concat a) (simp_concat b)
-    | ( (Ap2 (Sized, _, _) | Ap3 (Extract, _, _, _) | ApN (Concat, _))
-      , (Ap2 (Sized, _, _) | Ap3 (Extract, _, _, _) | ApN (Concat, _)) ) ->
-        Ap2 (Eq, x, y)
-    (* x = α ==> ⟨x,|α|⟩ = α *)
-    | ( x
-      , ((Ap2 (Sized, _, _) | Ap3 (Extract, _, _, _) | ApN (Concat, _)) as a)
-      )
-     |( ((Ap2 (Sized, _, _) | Ap3 (Extract, _, _, _) | ApN (Concat, _)) as a)
-      , x ) ->
-        simp_eq (Ap2 (Sized, seq_size_exn a, x)) a
-    | x, y -> Ap2 (Eq, x, y) )
-
-and simp_dq x y =
-  match (x, y) with
-  (* e ≠ (c ? t : f) ==> (c ? e ≠ t : e ≠ f) *)
-  | e, Ap3 (Conditional, c, t, f) | Ap3 (Conditional, c, t, f), e ->
-      simp_cond c (simp_dq e t) (simp_dq e f)
-  | _ -> (
-    match simp_eq x y with
-    | Ap2 (Eq, x, y) -> Ap2 (Dq, x, y)
-    | b -> simp_not b )
-
-(* negation-normal form *)
-and simp_not term =
-  match term with
-  (* ¬(x = y) ==> x ≠ y *)
-  | Ap2 (Eq, x, y) -> simp_dq x y
-  (* ¬(x ≠ y) ==> x = y *)
-  | Ap2 (Dq, x, y) -> simp_eq x y
-  (* ¬(x < y) ==> y <= x *)
-  | Ap2 (Lt, x, y) -> simp_le y x
-  (* ¬(x <= y) ==> y < x *)
-  | Ap2 (Le, x, y) -> simp_lt y x
-  (* ¬p(xs) ==> (¬p)(xs) *)
-  | PosLit (p, xs) -> simp_neglit p xs
-  (* ¬(¬p)(xs) ==> p(xs) *)
-  | NegLit (p, xs) -> simp_poslit p xs
-  (* ¬(a ∧ b) ==> ¬a ∨ ¬b *)
-  | And xs -> simp_or (Set.map ~f:simp_not xs)
-  (* ¬(a ∨ b) ==> ¬a ∧ ¬b *)
-  | Or xs -> simp_and (Set.map ~f:simp_not xs)
-  (* ¬¬e ==> e *)
-  | Ap2 (Xor, Integer {data}, e) when Z.is_true data -> e
-  | Ap2 (Xor, e, Integer {data}) when Z.is_true data -> e
-  (* ¬(c ? t : e) ==> c ? ¬t : ¬e *)
-  | Ap3 (Conditional, cnd, thn, els) ->
-      simp_cond cnd (simp_not thn) (simp_not els)
-  (* ¬i ==> -i-1 *)
-  | Integer {data} -> integer (Z.lognot data)
-  (* ¬e ==> true xor e *)
-  | e -> Ap2 (Xor, true_, e)
-
-(* bitwise *)
-
-let simp_xor x y =
-  match (x, y) with
-  (* i xor j *)
-  | Integer {data= i}, Integer {data= j} -> integer (Z.logxor i j)
-  (* true xor b ==> ¬b *)
-  | Integer {data}, b when Z.is_true data && is_boolean b -> simp_not b
-  | b, Integer {data} when Z.is_true data && is_boolean b -> simp_not b
-  (* e xor e ==> 0 *)
-  | _ when equal x y -> zero
-  | _ -> Ap2 (Xor, x, y)
-
-let simp_shl x y =
-  match (x, y) with
-  (* i shl j *)
-  | Integer {data= i}, Integer {data= j} when Z.sign j >= 0 ->
-      integer (Z.shift_left i (Z.to_int j))
-  (* e shl 0 ==> e *)
-  | e, Integer {data} when Z.equal Z.zero data -> e
-  | _ -> Ap2 (Shl, x, y)
-
-let simp_lshr x y =
-  match (x, y) with
-  (* i lshr j *)
-  | Integer {data= i}, Integer {data= j} when Z.sign j >= 0 ->
-      integer (Z.shift_right_trunc i (Z.to_int j))
-  (* e lshr 0 ==> e *)
-  | e, Integer {data} when Z.equal Z.zero data -> e
-  | _ -> Ap2 (Lshr, x, y)
-
-let simp_ashr x y =
-  match (x, y) with
-  (* i ashr j *)
-  | Integer {data= i}, Integer {data= j} when Z.sign j >= 0 ->
-      integer (Z.shift_right i (Z.to_int j))
-  (* e ashr 0 ==> e *)
-  | e, Integer {data} when Z.equal Z.zero data -> e
-  | _ -> Ap2 (Ashr, x, y)
-
-(* records *)
-
-let simp_record elts = ApN (Record, elts)
-let simp_select idx rcd = Ap1 (Select idx, rcd)
-let simp_update idx rcd elt = Ap2 (Update idx, rcd, elt)
-let simp_rec_record i = RecRecord i
-
-(* uninterpreted *)
-
-let simp_apply sym args = Apply (sym, args)
-
-(* dispatching for normalization and invariant checking *)
-
-let norm1 op x =
-  ( match op with
-  | Signed {bits} -> simp_signed bits x
-  | Unsigned {bits} -> simp_unsigned bits x
-  | Splat -> simp_splat x
-  | Select idx -> simp_select idx x )
-  |> check invariant
-
-let norm2 op x y =
-  ( match op with
-  | Sized -> simp_sized x y
-  | Eq -> simp_eq x y
-  | Dq -> simp_dq x y
-  | Lt -> simp_lt x y
-  | Le -> simp_le x y
-  | Div -> simp_div x y
-  | Rem -> simp_rem x y
-  | Xor -> simp_xor x y
-  | Shl -> simp_shl x y
-  | Lshr -> simp_lshr x y
-  | Ashr -> simp_ashr x y
-  | Update idx -> simp_update idx x y )
-  |> check invariant
-
-let norm3 op x y z =
-  ( match op with
-  | Conditional -> simp_cond x y z
-  | Extract -> simp_extract x y z )
-  |> check invariant
-
-let normN op xs =
-  (match op with Concat -> simp_concat xs | Record -> simp_record xs)
-  |> check invariant
-
-(* exposed interface *)
-
-let signed bits term = norm1 (Signed {bits}) term
-let unsigned bits term = norm1 (Unsigned {bits}) term
-let eq = norm2 Eq
-let dq = norm2 Dq
-let lt = norm2 Lt
-let le = norm2 Le
-let neg e = simp_negate e |> check invariant
-let add e f = simp_add2 e f |> check invariant
-let addN args = simp_add args |> check invariant
-let sub e f = simp_sub e f |> check invariant
-let mul e f = simp_mul2 e f |> check invariant
-let mulq q e = mul (rational q) e
-let mulN args = simp_mul args |> check invariant
-let div = norm2 Div
-let rem = norm2 Rem
-let and_ e f = simp_and2 e f |> check invariant
-let or_ e f = simp_or2 e f |> check invariant
-let andN es = simp_and es |> check invariant
-let orN es = simp_or es |> check invariant
-let not_ e = simp_not e |> check invariant
-let xor = norm2 Xor
-let shl = norm2 Shl
-let lshr = norm2 Lshr
-let ashr = norm2 Ashr
-let conditional ~cnd ~thn ~els = norm3 Conditional cnd thn els
-let splat byt = norm1 Splat byt
-let sized ~seq ~siz = norm2 Sized siz seq
-let extract ~seq ~off ~len = norm3 Extract seq off len
-let concat xs = normN Concat (IArray.of_array xs)
-let record elts = normN Record elts
-let select ~rcd ~idx = norm1 (Select idx) rcd
-let update ~rcd ~idx ~elt = norm2 (Update idx) rcd elt
-let rec_record i = simp_rec_record i |> check invariant
-let apply sym args = simp_apply sym args |> check invariant
-let poslit sym args = simp_poslit sym args |> check invariant
-let neglit sym args = simp_neglit sym args |> check invariant
-
-(** Destruct *)
-
-let d_int = function Integer {data} -> Some data | _ -> None
-
-(** Access *)
-
-let const_of = function Add poly -> Some (Qset.count one poly) | _ -> None
-
-(** Transform *)
-
-let map e ~f =
-  let map1 op ~f x =
-    let x' = f x in
-    if x' == x then e else norm1 op x'
-  in
-  let map2 op ~f x y =
-    let x' = f x in
-    let y' = f y in
-    if x' == x && y' == y then e else norm2 op x' y'
-  in
-  let map3 op ~f 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 norm3 op x' y' z'
-  in
-  let mapN mk ~f xs =
-    let xs' = IArray.map_endo ~f xs in
-    if xs' == xs then e else mk xs'
-  in
-  let map_set mk ~f args =
-    let args' = Set.map ~f args in
-    if args' == args then e else mk args'
-  in
-  let map_qset mk ~f args =
-    let args' = Qset.map ~f:(fun arg q -> (f arg, q)) args in
-    if args' == args then e else mk args'
-  in
-  match e with
-  | And args -> map_set andN ~f args
-  | Or args -> map_set orN ~f args
-  | Add args -> map_qset addN ~f args
-  | Mul args -> map_qset mulN ~f args
-  | Ap1 (op, x) -> map1 op ~f x
-  | Ap2 (op, x, y) -> map2 op ~f x y
-  | Ap3 (op, x, y, z) -> map3 op ~f x y z
-  | ApN (op, xs) -> mapN (normN op) ~f xs
-  | Apply (sym, xs) -> mapN (simp_apply sym) ~f xs
-  | PosLit (sym, xs) -> mapN (simp_poslit sym) ~f xs
-  | NegLit (sym, xs) -> mapN (simp_neglit sym) ~f xs
-  | Var _ | Integer _ | Rational _ | RecRecord _ -> e
-
-let fold_map e s0 ~f =
-  let s = ref s0 in
-  let f x =
-    let x', s' = f x !s in
-    s := s' ;
-    x'
-  in
-  let e' = map e ~f in
-  (e', !s)
-
-let rec map_rec_pre e ~f =
-  match f e with Some e' -> e' | None -> map ~f:(map_rec_pre ~f) e
-
-let rec fold_map_rec_pre e s ~f =
-  match f e s with
-  | Some (e', s) -> (e', s)
-  | None -> fold_map ~f:(fold_map_rec_pre ~f) e s
-
-let disjuncts e =
-  let rec disjuncts_ e =
-    match e with
-    | Or es ->
-        let e0, e1N = Set.pop_exn es in
-        Set.fold ~f:(fun e -> Set.union (disjuncts_ e)) e1N (disjuncts_ e0)
-    | Ap3 (Conditional, cnd, thn, els) ->
-        Set.add
-          (and_ (orN (disjuncts_ (not_ cnd))) (orN (disjuncts_ els)))
-          (Set.of_ (and_ (orN (disjuncts_ cnd)) (orN (disjuncts_ thn))))
-    | _ -> Set.of_ e
-  in
-  Iter.to_list (Set.to_iter (disjuncts_ e))
-
-let rename f e =
-  let f = (f : Var.t -> Var.t :> Var.t -> t) in
-  map_rec_pre ~f:(fun e -> Option.map ~f (Var.of_term e)) e
-
-(** Traverse *)
-
-let iter e ~f =
-  match e with
-  | Ap1 (_, x) -> f x
-  | Ap2 (_, x, y) ->
-      f x ;
-      f y
-  | Ap3 (_, x, y, z) ->
-      f x ;
-      f y ;
-      f z
-  | ApN (_, xs) | Apply (_, xs) | PosLit (_, xs) | NegLit (_, xs) ->
-      IArray.iter ~f xs
-  | And args | Or args -> Set.iter ~f args
-  | Add args | Mul args -> Qset.iter ~f:(fun arg _ -> f arg) args
-  | Var _ | Integer _ | Rational _ | RecRecord _ -> ()
-
-let exists e ~f =
-  match e with
-  | Ap1 (_, x) -> f x
-  | Ap2 (_, x, y) -> f x || f y
-  | Ap3 (_, x, y, z) -> f x || f y || f z
-  | ApN (_, xs) | Apply (_, xs) | PosLit (_, xs) | NegLit (_, xs) ->
-      IArray.exists ~f xs
-  | And args | Or args -> Set.exists ~f args
-  | Add args | Mul args -> Qset.exists ~f:(fun arg _ -> f arg) args
-  | Var _ | Integer _ | Rational _ | RecRecord _ -> false
-
-let for_all e ~f =
-  match e with
-  | Ap1 (_, x) -> f x
-  | Ap2 (_, x, y) -> f x && f y
-  | Ap3 (_, x, y, z) -> f x && f y && f z
-  | ApN (_, xs) | Apply (_, xs) | PosLit (_, xs) | NegLit (_, xs) ->
-      IArray.for_all ~f xs
-  | And args | Or args -> Set.for_all ~f args
-  | Add args | Mul args -> Qset.for_all ~f:(fun arg _ -> f arg) args
-  | Var _ | Integer _ | Rational _ | RecRecord _ -> true
-
-let fold e s ~f =
-  match e with
-  | Ap1 (_, x) -> f x s
-  | Ap2 (_, x, y) -> f y (f x s)
-  | Ap3 (_, x, y, z) -> f z (f y (f x s))
-  | ApN (_, xs) | Apply (_, xs) | PosLit (_, xs) | NegLit (_, xs) ->
-      IArray.fold ~f xs s
-  | And args | Or args -> Set.fold ~f args s
-  | Add args | Mul args -> Qset.fold ~f:(fun e _ s -> f e s) args s
-  | Var _ | Integer _ | Rational _ | RecRecord _ -> s
-
-let rec iter_terms e ~f =
-  ( match e with
-  | Ap1 (_, x) -> iter_terms ~f x
-  | Ap2 (_, x, y) ->
-      iter_terms ~f x ;
-      iter_terms ~f y
-  | Ap3 (_, x, y, z) ->
-      iter_terms ~f x ;
-      iter_terms ~f y ;
-      iter_terms ~f z
-  | ApN (_, xs) | Apply (_, xs) | PosLit (_, xs) | NegLit (_, xs) ->
-      IArray.iter ~f:(iter_terms ~f) xs
-  | And args | Or args -> Set.iter args ~f:(iter_terms ~f)
-  | Add args | Mul args ->
-      Qset.iter args ~f:(fun arg _ -> iter_terms ~f arg)
-  | Var _ | Integer _ | Rational _ | RecRecord _ -> () ) ;
-  f e
-
-let rec fold_terms e s ~f =
-  f e
-    ( match e with
-    | Ap1 (_, x) -> fold_terms ~f x s
-    | Ap2 (_, x, y) -> fold_terms ~f y (fold_terms ~f x s)
-    | Ap3 (_, x, y, z) ->
-        fold_terms ~f z (fold_terms ~f y (fold_terms ~f x s))
-    | ApN (_, xs) | Apply (_, xs) | PosLit (_, xs) | NegLit (_, xs) ->
-        IArray.fold ~f:(fold_terms ~f) xs s
-    | And args | Or args -> Set.fold ~f:(fold_terms ~f) args s
-    | Add args | Mul args ->
-        Qset.fold ~f:(fun arg _ -> fold_terms ~f arg) args s
-    | Var _ | Integer _ | Rational _ | RecRecord _ -> s )
-
-let iter_vars e ~f =
-  iter_terms ~f:(fun e -> Option.iter ~f (Var.of_term e)) e
-
-let exists_vars e ~f =
-  Iter.exists ~f (Iter.from_labelled_iter (iter_vars e))
-
-let fold_vars e s ~f =
-  fold_terms ~f:(fun e -> Option.fold ~f (Var.of_term e)) e s
-
-(** Query *)
-
-let fv e = fold_vars ~f:Var.Set.add e Var.Set.empty
-let is_true = function Integer {data} -> Z.is_true data | _ -> false
-let is_false = function Integer {data} -> Z.is_false data | _ -> false
-
-let rec is_constant = function
-  | Var _ -> false
-  | Integer _ | Rational _ -> true
-  | a -> for_all ~f:is_constant a
-
-let rec height = function
-  | Var _ -> 0
-  | Ap1 (_, a) -> 1 + height a
-  | Ap2 (_, a, b) -> 1 + max (height a) (height b)
-  | Ap3 (_, a, b, c) -> 1 + max (height a) (max (height b) (height c))
-  | ApN (_, v) | Apply (_, v) | PosLit (_, v) | NegLit (_, v) ->
-      1 + IArray.fold ~f:(fun a m -> max m (height a)) v 0
-  | And bs | Or bs -> 1 + Set.fold ~f:(fun a m -> max m (height a)) bs 0
-  | Add qs | Mul qs -> 1 + Qset.fold ~f:(fun a _ m -> max m (height a)) qs 0
-  | Integer _ | Rational _ | RecRecord _ -> 0
-
-(** Solve *)
-
-let exists_fv_in vs qset =
-  Qset.exists qset ~f:(fun e _ ->
-      exists_vars e ~f:(fun v -> Var.Set.mem v vs) )
-
-(* solve [0 = rejected_sum + (coeff × mono) + sum] *)
-let solve_for_mono rejected_sum coeff mono sum =
-  match mono with
-  | Integer _ -> None
-  | _ ->
-      if exists_fv_in (fv mono) sum then None
-      else
-        Some
-          ( mono
-          , Sum.to_term
-              (Sum.mul_const
-                 (Q.inv (Q.neg coeff))
-                 (Qset.union rejected_sum sum)) )
-
-(* solve [0 = rejected + sum] *)
-let rec solve_sum rejected_sum sum =
-  let* mono, coeff, sum = Qset.pop_min_elt sum in
-  match solve_for_mono rejected_sum coeff mono sum with
-  | Some _ as soln -> soln
-  | None -> solve_sum (Qset.add mono coeff rejected_sum) sum
-
-(* solve [0 = e] *)
-let solve_zero_eq ?for_ e =
-  [%Trace.call fun {pf} -> pf "0 = %a%a" pp e (Option.pp " for %a" pp) for_]
-  ;
-  ( match e with
-  | Add sum -> (
-    match for_ with
-    | None -> solve_sum Qset.empty sum
-    | Some mono ->
-        let* coeff, sum = Qset.find_and_remove mono sum in
-        solve_for_mono Qset.empty coeff mono sum )
-  | _ -> None )
-  |>
-  [%Trace.retn fun {pf} s ->
-    pf "%a"
-      (Option.pp "%a" (fun fs (c, r) ->
-           Format.fprintf fs "%a ↦ %a" pp c pp r ))
-      s ;
-    match (for_, s) with
-    | Some f, Some (c, _) -> assert (equal f c)
-    | _ -> ()]
diff --git a/sledge/src/ses/term.mli b/sledge/src/ses/term.mli
deleted file mode 100644
index 2c0a06e12..000000000
--- a/sledge/src/ses/term.mli
+++ /dev/null
@@ -1,231 +0,0 @@
-(*
- * 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.
- *)
-
-(** Terms
-
-    Pure (heap-independent) terms are arithmetic, bitwise-logical, etc.
-    operations over literal values and variables. *)
-
-type op1 =
-  | Signed of {bits: int}
-      (** [Ap1 (Signed {bits= n}, arg)] is [arg] interpreted as an [n]-bit
-          signed integer. That is, it two's-complement--decodes the low [n]
-          bits of the infinite two's-complement encoding of [arg]. *)
-  | Unsigned of {bits: int}
-      (** [Ap1 (Unsigned {bits= n}, arg)] is [arg] interpreted as an [n]-bit
-          unsigned integer. That is, it unsigned-binary--decodes the low [n]
-          bits of the infinite two's-complement encoding of [arg]. *)
-  | Splat  (** Iterated concatenation of a single byte *)
-  | Select of int  (** Select an index from a record *)
-[@@deriving compare, equal, sexp]
-
-type op2 =
-  | Eq  (** Equal test *)
-  | Dq  (** Disequal test *)
-  | Lt  (** Less-than test *)
-  | Le  (** Less-than-or-equal test *)
-  | Div  (** Division, for integers result is truncated toward zero *)
-  | Rem
-      (** Remainder of division, satisfies [a = b * div a b + rem a b] and
-          for integers [rem a b] has same sign as [a], and [|rem a b| < |b|] *)
-  | Xor  (** Exclusive-or, bitwise *)
-  | Shl  (** Shift left, bitwise *)
-  | Lshr  (** Logical shift right, bitwise *)
-  | Ashr  (** Arithmetic shift right, bitwise *)
-  | Sized  (** Size-tagged sequence *)
-  | Update of int  (** Constant record with updated index *)
-[@@deriving compare, equal, sexp]
-
-type op3 =
-  | Conditional  (** If-then-else *)
-  | Extract  (** Extract a slice of an sequence value *)
-[@@deriving compare, equal, sexp]
-
-type opN =
-  | Concat  (** Byte-array concatenation *)
-  | Record  (** Record (array / struct) constant *)
-[@@deriving compare, equal, sexp]
-
-module rec Set : sig
-  include NS.Set.S with type elt := T.t
-
-  val t_of_sexp : Sexp.t -> t
-end
-
-and Qset : sig
-  include NS.Multiset.S with type mul := Q.t with type elt := T.t
-
-  val t_of_sexp : Sexp.t -> t
-end
-
-and T : sig
-  type set = Set.t [@@deriving compare, equal, sexp]
-
-  type qset = Qset.t [@@deriving compare, equal, sexp]
-
-  and t = private
-    | Var of {id: int; name: string}
-        (** Local variable / virtual register *)
-    | Ap1 of op1 * t  (** Unary application *)
-    | Ap2 of op2 * t * t  (** Binary application *)
-    | Ap3 of op3 * t * t * t  (** Ternary application *)
-    | ApN of opN * t iarray  (** N-ary application *)
-    | And of set  (** Conjunction, boolean or bitwise *)
-    | Or of set  (** Disjunction, boolean or bitwise *)
-    | Add of qset  (** Sum of terms with rational coefficients *)
-    | Mul of qset  (** Product of terms with rational exponents *)
-    | Integer of {data: Z.t}  (** Integer constant *)
-    | Rational of {data: Q.t}  (** Rational constant *)
-    | RecRecord of int  (** Reference to ancestor recursive record *)
-    | Apply of Funsym.t * t iarray
-        (** Uninterpreted function application *)
-    | PosLit of Predsym.t * t iarray
-    | NegLit of Predsym.t * t iarray
-  [@@deriving compare, equal, sexp]
-end
-
-include module type of T with type t = T.t
-
-(** Term.Var is re-exported as Var *)
-module Var : sig
-  include Var_intf.VAR with type t = private T.t
-
-  val of_ : T.t -> t
-  (** [var (of_ e)] = [e] if [e] matches [Var _], otherwise undefined *)
-
-  val of_term : T.t -> t option
-end
-
-module Map : sig
-  include Map.S with type key := t
-
-  val t_of_sexp : (Sexp.t -> 'a) -> Sexp.t -> 'a t
-end
-
-val ppx : Var.strength -> t pp
-val pp : t pp
-val pp_diff : (t * t) pp
-val invariant : t -> unit
-
-(** Construct *)
-
-(* variables *)
-val var : Var.t -> t
-
-(* constants *)
-val bool : bool -> t
-val true_ : t
-val false_ : t
-val integer : Z.t -> t
-val zero : t
-val one : t
-val minus_one : t
-val rational : Q.t -> t
-
-(* type conversions *)
-val signed : int -> t -> t
-val unsigned : int -> t -> t
-
-(* comparisons *)
-val eq : t -> t -> t
-val dq : t -> t -> t
-val lt : t -> t -> t
-val le : t -> t -> t
-
-(* arithmetic *)
-val neg : t -> t
-val add : t -> t -> t
-val sub : t -> t -> t
-val mulq : Q.t -> t -> t
-val mul : t -> t -> t
-val div : t -> t -> t
-val rem : t -> t -> t
-
-(* boolean / bitwise *)
-val and_ : t -> t -> t
-val or_ : t -> t -> t
-val not_ : t -> t
-
-(* bitwise *)
-val xor : t -> t -> t
-val shl : t -> t -> t
-val lshr : t -> t -> t
-val ashr : t -> t -> t
-
-(* if-then-else *)
-val conditional : cnd:t -> thn:t -> els:t -> t
-
-(* sequence sizes *)
-val seq_size_exn : t -> t
-val seq_size : t -> t option
-
-(* sequences *)
-val splat : t -> t
-val sized : seq:t -> siz:t -> t
-val extract : seq:t -> off:t -> len:t -> t
-val concat : t array -> t
-
-(* records (struct / array values) *)
-val record : t iarray -> t
-val select : rcd:t -> idx:int -> t
-val update : rcd:t -> idx:int -> elt:t -> t
-val rec_record : int -> t
-
-(* uninterpreted *)
-val apply : Funsym.t -> t iarray -> t
-val poslit : Predsym.t -> t iarray -> t
-val neglit : Predsym.t -> t iarray -> t
-
-(** Destruct *)
-
-val d_int : t -> Z.t option
-
-(** Access *)
-
-val const_of : t -> Q.t option
-
-(** Transform *)
-
-val map : t -> f:(t -> t) -> t
-
-val map_rec_pre : t -> f:(t -> t option) -> t
-(** Pre-order transformation. Each subterm [x] from root to leaves is
-    presented to [f]. If [f x = Some x'] then the subterms of [x] are not
-    traversed and [x] is transformed to [x']. Otherwise traversal proceeds
-    to the subterms of [x], followed by rebuilding the term structure on the
-    transformed subterms. *)
-
-val fold_map : t -> 's -> f:(t -> 's -> t * 's) -> t * 's
-val fold_map_rec_pre : t -> 's -> f:(t -> 's -> (t * 's) option) -> t * 's
-val disjuncts : t -> t list
-val rename : (Var.t -> Var.t) -> t -> t
-
-(** Traverse *)
-
-val iter : t -> f:(t -> unit) -> unit
-val exists : t -> f:(t -> bool) -> bool
-val fold : t -> 'a -> f:(t -> 'a -> 'a) -> 'a
-val fold_vars : t -> 'a -> f:(Var.t -> 'a -> 'a) -> 'a
-val fold_terms : t -> 'a -> f:(t -> 'a -> 'a) -> 'a
-
-(** Query *)
-
-val fv : t -> Var.Set.t
-val is_true : t -> bool
-val is_false : t -> bool
-
-val is_constant : t -> bool
-(** Test if a term's semantics is independent of the values of variables. *)
-
-val height : t -> int
-
-(** Solve *)
-
-val solve_zero_eq : ?for_:t -> t -> (t * t) option
-(** [solve_zero_eq d] is [Some (e, f)] if [d = 0] can be equivalently
-    expressed as [e = f] for some monomial subterm [e] of [d]. If [for_] is
-    passed, then the subterm [e] must be [for_]. *)
diff --git a/sledge/src/ses/var.ml b/sledge/src/ses/var.ml
deleted file mode 100644
index 0b93a52e0..000000000
--- a/sledge/src/ses/var.ml
+++ /dev/null
@@ -1,10 +0,0 @@
-(*
- * 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.
- *)
-
-(** Variables *)
-
-include Term.Var
diff --git a/sledge/src/ses/var.mli b/sledge/src/ses/var.mli
deleted file mode 100644
index d4d909555..000000000
--- a/sledge/src/ses/var.mli
+++ /dev/null
@@ -1,10 +0,0 @@
-(*
- * 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.
- *)
-
-(** Variables *)
-
-include module type of Term.Var
diff --git a/sledge/src/sh.ml b/sledge/src/sh.ml
index ac30ede56..965431535 100644
--- a/sledge/src/sh.ml
+++ b/sledge/src/sh.ml
@@ -531,9 +531,7 @@ let and_ e q = star (pure e) q
 let and_subst subst q =
   [%Trace.call fun {pf} -> pf "%a@ %a" Context.Subst.pp subst pp q]
   ;
-  Context.Subst.fold
-    ~f:(fun ~key ~data -> and_ (Formula.eq key data))
-    subst q
+  Context.Subst.fold_eqs ~f:and_ subst q
   |>
   [%Trace.retn fun {pf} q ->
     pf "%a" pp q ;
diff --git a/sledge/src/test/equality_test.ml b/sledge/src/test/context_test.ml
similarity index 66%
rename from sledge/src/test/equality_test.ml
rename to sledge/src/test/context_test.ml
index 54cdd260d..5afd36141 100644
--- a/sledge/src/test/equality_test.ml
+++ b/sledge/src/test/context_test.ml
@@ -5,11 +5,12 @@
  * LICENSE file in the root directory of this source tree.
  *)
 
-open Ses
+open Sledge
+open Fol
 
 let%test_module _ =
   ( module struct
-    open Equality
+    open Context
 
     let () = Trace.init ~margin:68 ()
 
@@ -21,10 +22,10 @@ let%test_module _ =
      * [@@@warning "-32"] *)
 
     let printf pp = Format.printf "@\n%a@." pp
-    let pp = printf pp
-    let pp_classes = Format.printf "@\n@[<hv>  %a@]@." pp_classes
+    let pp = printf Context.pp_raw
+    let pp_classes = Format.printf "@\n@[<hv>  %a@]@." Context.pp
     let ( ! ) i = Term.integer (Z.of_int i)
-    let g = Term.rem
+    let g x y = Term.apply (Uninterp "g") [|x; y|]
     let wrt = Var.Set.empty
     let t_, wrt = Var.fresh "t" ~wrt
     let u_, wrt = Var.fresh "u" ~wrt
@@ -42,10 +43,12 @@ let%test_module _ =
     let z = Term.var z_
 
     let of_eqs l =
-      List.fold ~f:(fun (a, b) (us, r) -> and_eq us a b r) l (wrt, true_)
+      List.fold
+        ~f:(fun (a, b) (us, r) -> add us (Formula.eq a b) r)
+        l (wrt, empty)
       |> snd
 
-    let implies_eq r a b = implies r (Term.eq a b)
+    let implies_eq r a b = implies r (Formula.eq a b)
 
     (* tests *)
 
@@ -56,8 +59,8 @@ let%test_module _ =
       pp r3 ;
       [%expect
         {|
-        %t_1 = %u_2 = %v_3 = %w_4 = %x_5 = %z_7 = (%y_6 rem %t_1)
-        = (%y_6 rem %t_1)
+        %t_1 = %u_2 = %v_3 = %w_4 = %x_5 = %z_7 = g(%y_6, %t_1)
+        = g(%y_6, %t_1)
 
       {sat= true;
        rep= [[%t_1 ↦ ];
@@ -67,22 +70,19 @@ let%test_module _ =
              [%x_5 ↦ %t_1];
              [%y_6 ↦ ];
              [%z_7 ↦ %t_1];
-             [(%y_6 rem %v_3) ↦ %t_1];
-             [(%y_6 rem %z_7) ↦ %t_1];
-             [-1 ↦ ];
-             [0 ↦ ]]} |}]
+             [g(%y_6, %v_3) ↦ %t_1];
+             [g(%y_6, %z_7) ↦ %t_1]]} |}]
 
     let%test _ = implies_eq r3 t z
 
-    let b = Term.dq x !0
+    let b = Formula.inject (Formula.dq x !0)
     let r15 = of_eqs [(b, b); (x, !1)]
 
     let%expect_test _ =
       pp r15 ;
-      [%expect
-        {|
-          {sat= true; rep= [[%x_5 ↦ 1]; [(%x_5 ≠ 0) ↦ -1]; [-1 ↦ ]; [0 ↦ ]]} |}]
+      [%expect {|
+          {sat= true; rep= [[%x_5 ↦ 1]]} |}]
 
-    let%test _ = implies_eq r15 b (Term.signed 1 !1)
-    let%test _ = implies_eq r15 (Term.unsigned 1 b) !1
+    let%test _ = implies_eq r15 (Term.neg b) (Term.apply (Signed 1) [|!1|])
+    let%test _ = implies_eq r15 (Term.apply (Unsigned 1) [|b|]) !1
   end )
diff --git a/sledge/src/test/equality_test.mli b/sledge/src/test/context_test.mli
similarity index 100%
rename from sledge/src/test/equality_test.mli
rename to sledge/src/test/context_test.mli
diff --git a/sledge/src/test/fol_test.ml b/sledge/src/test/fol_test.ml
index 531c56f2d..2822ea9de 100644
--- a/sledge/src/test/fol_test.ml
+++ b/sledge/src/test/fol_test.ml
@@ -16,7 +16,7 @@ let%test_module _ =
 
     (* let () =
      *   Trace.init ~margin:160
-     *     ~config:(Result.get_ok (Trace.parse "+Fol"))
+     *     ~config:(Result.get_ok (Trace.parse "+Fol+Context+Arithmetic"))
      *     () *)
 
     [@@@warning "-32"]
@@ -43,8 +43,8 @@ let%test_module _ =
     let x = Term.var x_
     let y = Term.var y_
     let z = Term.var z_
-    let f = Term.splat
-    let g = Term.mul
+    let f x = Term.apply (Uninterp "f") [|x|]
+    let g x y = Term.apply (Uninterp "g") [|x; y|]
 
     let of_eqs l =
       List.fold
@@ -66,7 +66,7 @@ let%test_module _ =
 
     let%expect_test _ =
       pp_raw f1 ;
-      [%expect {| {sat= false; rep= [[-1 ↦ ]; [0 ↦ ]]} |}]
+      [%expect {| {sat= false; rep= []} |}]
 
     let%test _ = is_unsat (add_eq !1 !1 f1)
 
@@ -76,7 +76,7 @@ let%test_module _ =
 
     let%expect_test _ =
       pp_raw f2 ;
-      [%expect {| {sat= false; rep= [[-1 ↦ ]; [0 ↦ ]]} |}]
+      [%expect {| {sat= false; rep= []} |}]
 
     let f3 = of_eqs [(x + !0, x + !1)]
 
@@ -84,7 +84,7 @@ let%test_module _ =
 
     let%expect_test _ =
       pp_raw f3 ;
-      [%expect {| {sat= false; rep= [[-1 ↦ ]; [0 ↦ ]]} |}]
+      [%expect {| {sat= false; rep= []} |}]
 
     let f4 = of_eqs [(x, y); (x + !0, y + !1)]
 
@@ -92,8 +92,7 @@ let%test_module _ =
 
     let%expect_test _ =
       pp_raw f4 ;
-      [%expect
-        {| {sat= false; rep= [[%x_5 ↦ ]; [%y_6 ↦ %x_5]; [-1 ↦ ]; [0 ↦ ]]} |}]
+      [%expect {| {sat= false; rep= [[%x_5 ↦ ]; [%y_6 ↦ %x_5]]} |}]
 
     let t1 = of_eqs [(!1, !1)]
 
@@ -109,7 +108,7 @@ let%test_module _ =
 
     let%expect_test _ =
       pp_raw r0 ;
-      [%expect {| {sat= true; rep= [[-1 ↦ ]; [0 ↦ ]]} |}]
+      [%expect {| {sat= true; rep= []} |}]
 
     let%expect_test _ =
       pp r0 ;
@@ -128,7 +127,7 @@ let%test_module _ =
 
         %x_5 = %y_6
 
-      {sat= true; rep= [[%x_5 ↦ ]; [%y_6 ↦ %x_5]; [-1 ↦ ]; [0 ↦ ]]} |}]
+      {sat= true; rep= [[%x_5 ↦ ]; [%y_6 ↦ %x_5]]} |}]
 
     let%test _ = implies_eq r1 x y
 
@@ -139,15 +138,10 @@ let%test_module _ =
       pp_raw r2 ;
       [%expect
         {|
-        %x_5 = %y_6 = %z_7 = %x_5^
+        %x_5 = %y_6 = %z_7 = f(%x_5)
 
       {sat= true;
-       rep= [[%x_5 ↦ ];
-             [%y_6 ↦ %x_5];
-             [%z_7 ↦ %x_5];
-             [%x_5^ ↦ %x_5];
-             [-1 ↦ ];
-             [0 ↦ ]]} |}]
+       rep= [[%x_5 ↦ ]; [%y_6 ↦ %x_5]; [%z_7 ↦ %x_5]; [f(%x_5) ↦ %x_5]]} |}]
 
     let%test _ = implies_eq r2 x z
     let%test _ = implies_eq (inter r1 r2) x y
@@ -168,13 +162,11 @@ let%test_module _ =
       pp_raw rs ;
       [%expect
         {|
-        {sat= true;
-         rep= [[%w_4 ↦ ]; [%y_6 ↦ %w_4]; [%z_7 ↦ %w_4]; [-1 ↦ ]; [0 ↦ ]]}
+        {sat= true; rep= [[%w_4 ↦ ]; [%y_6 ↦ %w_4]; [%z_7 ↦ %w_4]]}
 
-        {sat= true;
-         rep= [[%x_5 ↦ ]; [%y_6 ↦ %x_5]; [%z_7 ↦ %x_5]; [-1 ↦ ]; [0 ↦ ]]}
+        {sat= true; rep= [[%x_5 ↦ ]; [%y_6 ↦ %x_5]; [%z_7 ↦ %x_5]]}
 
-        {sat= true; rep= [[%y_6 ↦ ]; [%z_7 ↦ %y_6]; [-1 ↦ ]; [0 ↦ ]]} |}]
+        {sat= true; rep= [[%y_6 ↦ ]; [%z_7 ↦ %y_6]]} |}]
 
     let%test _ =
       let r = of_eqs [(w, y); (y, z)] in
@@ -189,23 +181,21 @@ let%test_module _ =
       pp_raw r3 ;
       [%expect
         {|
-        %z_7 = %u_2 = %v_3 = %w_4 = %x_5 = (%y_6 × %z_7)
-      ∧ (%y_6^2 × %z_7) = %t_1
+        %t_1 = %u_2 = %v_3 = %w_4 = %x_5 = %z_7 = g(%y_6, %t_1)
+        = g(%y_6, %t_1)
 
       {sat= true;
-       rep= [[%t_1 ↦ (%y_6^2 × %z_7)];
-             [%u_2 ↦ %z_7];
-             [%v_3 ↦ %z_7];
-             [%w_4 ↦ %z_7];
-             [%x_5 ↦ %z_7];
+       rep= [[%t_1 ↦ ];
+             [%u_2 ↦ %t_1];
+             [%v_3 ↦ %t_1];
+             [%w_4 ↦ %t_1];
+             [%x_5 ↦ %t_1];
              [%y_6 ↦ ];
-             [%z_7 ↦ ];
-             [(%y_6 × %z_7) ↦ %z_7];
-             [(%y_6^2 × %z_7) ↦ ];
-             [-1 ↦ ];
-             [0 ↦ ]]} |}]
+             [%z_7 ↦ %t_1];
+             [g(%y_6, %v_3) ↦ %t_1];
+             [g(%y_6, %z_7) ↦ %t_1]]} |}]
 
-    let%test _ = not (implies_eq r3 t z) (* incomplete *)
+    let%test _ = implies_eq r3 t z
     let%test _ = implies_eq r3 x z
     let%test _ = implies_eq (union r2 r3) x z
 
@@ -219,12 +209,10 @@ let%test_module _ =
         (-4 + %z_7) = %y_6 ∧ (3 + %z_7) = %w_4 ∧ (8 + %z_7) = %x_5
 
       {sat= true;
-       rep= [[%w_4 ↦ (%z_7 + 3)];
-             [%x_5 ↦ (%z_7 + 8)];
-             [%y_6 ↦ (%z_7 + -4)];
-             [%z_7 ↦ ];
-             [-1 ↦ ];
-             [0 ↦ ]]} |}]
+       rep= [[%w_4 ↦ (3 + %z_7)];
+             [%x_5 ↦ (8 + %z_7)];
+             [%y_6 ↦ (-4 + %z_7)];
+             [%z_7 ↦ ]]} |}]
 
     let%test _ = implies_eq r4 x (w + !5)
     let%test _ = difference r4 x w |> Poly.equal (Some (Z.of_int 5))
@@ -242,7 +230,7 @@ let%test_module _ =
         {|
         1 = %x_5 = %y_6
 
-      {sat= true; rep= [[%x_5 ↦ 1]; [%y_6 ↦ 1]; [-1 ↦ ]; [0 ↦ ]]} |}]
+      {sat= true; rep= [[%x_5 ↦ 1]; [%y_6 ↦ 1]]} |}]
 
     let%test _ = implies_eq r6 x y
 
@@ -251,8 +239,6 @@ let%test_module _ =
     let%expect_test _ =
       pp r7 ;
       pp_raw r7 ;
-      pp_raw (add_eq x z r7) ;
-      pp (add_eq x z r7) ;
       [%expect
         {|
           %v_3 = %x_5 ∧ %w_4 = %y_6 = %z_7
@@ -262,32 +248,7 @@ let%test_module _ =
                [%w_4 ↦ ];
                [%x_5 ↦ %v_3];
                [%y_6 ↦ %w_4];
-               [%z_7 ↦ %w_4];
-               [-1 ↦ ];
-               [0 ↦ ]]}
-
-        {sat= true;
-         rep= [[%v_3 ↦ ];
-               [%w_4 ↦ %v_3];
-               [%x_5 ↦ %v_3];
-               [%y_6 ↦ %v_3];
-               [%z_7 ↦ %v_3];
-               [-1 ↦ ];
-               [0 ↦ ]]}
-
-          %v_3 = %w_4 = %x_5 = %y_6 = %z_7 |}]
-
-    let%expect_test _ =
-      printf (List.pp " , " Term.pp) (class_of r7 t) ;
-      printf (List.pp " , " Term.pp) (class_of r7 x) ;
-      printf (List.pp " , " Term.pp) (class_of r7 z) ;
-      [%expect
-        {|
-        %t_1
-
-        %v_3 , %x_5
-
-        %w_4 , %z_7 , %y_6 |}]
+               [%z_7 ↦ %w_4]]} |}]
 
     let r7' = add_eq x z r7
 
@@ -303,9 +264,7 @@ let%test_module _ =
              [%w_4 ↦ %v_3];
              [%x_5 ↦ %v_3];
              [%y_6 ↦ %v_3];
-             [%z_7 ↦ %v_3];
-             [-1 ↦ ];
-             [0 ↦ ]]} |}]
+             [%z_7 ↦ %v_3]]} |}]
 
     let%test _ = normalize r7' w |> Term.equal v
 
@@ -324,8 +283,7 @@ let%test_module _ =
         {|
         14 = %y_6 ∧ 13×%z_7 = %x_5
     
-      {sat= true;
-       rep= [[%x_5 ↦ (13 × %z_7)]; [%y_6 ↦ 14]; [%z_7 ↦ ]; [-1 ↦ ]; [0 ↦ ]]} |}]
+      {sat= true; rep= [[%x_5 ↦ 13×%z_7]; [%y_6 ↦ 14]; [%z_7 ↦ ]]} |}]
 
     let%test _ = implies_eq r8 y !14
 
@@ -336,11 +294,9 @@ let%test_module _ =
       pp_raw r9 ;
       [%expect
         {|
-      {sat= true;
-       rep= [[%x_5 ↦ (%z_7 + -16)]; [%z_7 ↦ ]; [-1 ↦ ]; [0 ↦ ]]}
+      {sat= true; rep= [[%x_5 ↦ (-16 + %z_7)]; [%z_7 ↦ ]]}
 
-      {sat= true;
-       rep= [[%x_5 ↦ (%z_7 + -16)]; [%z_7 ↦ ]; [-1 ↦ ]; [0 ↦ ]]} |}]
+      {sat= true; rep= [[%x_5 ↦ (-16 + %z_7)]; [%z_7 ↦ ]]} |}]
 
     let%test _ = difference r9 z (x + !8) |> Poly.equal (Some (Z.of_int 8))
 
@@ -355,11 +311,9 @@ let%test_module _ =
       Format.printf "@.%a@." Term.pp (normalize r10 (x + !8 - z)) ;
       [%expect
         {|
-        {sat= true;
-         rep= [[%x_5 ↦ (%z_7 + -16)]; [%z_7 ↦ ]; [-1 ↦ ]; [0 ↦ ]]}
+        {sat= true; rep= [[%x_5 ↦ (-16 + %z_7)]; [%z_7 ↦ ]]}
 
-        {sat= true;
-         rep= [[%x_5 ↦ (%z_7 + -16)]; [%z_7 ↦ ]; [-1 ↦ ]; [0 ↦ ]]}
+        {sat= true; rep= [[%x_5 ↦ (-16 + %z_7)]; [%z_7 ↦ ]]}
 
         (-8 + -1×%x_5 + %z_7)
 
@@ -394,8 +348,7 @@ let%test_module _ =
 
     let%expect_test _ =
       pp_raw r13 ;
-      [%expect
-        {| {sat= true; rep= [[%y_6 ↦ ]; [%z_7 ↦ %y_6]; [-1 ↦ ]; [0 ↦ ]]} |}]
+      [%expect {| {sat= true; rep= [[%y_6 ↦ ]; [%z_7 ↦ %y_6]]} |}]
 
     let%test _ = not (is_unsat r13) (* incomplete *)
 
@@ -404,9 +357,8 @@ let%test_module _ =
 
     let%expect_test _ =
       pp_raw r14 ;
-      [%expect
-        {|
-          {sat= true; rep= [[%x_5 ↦ 1]; [-1 ↦ ]; [0 ↦ ]]} |}]
+      [%expect {|
+          {sat= true; rep= [[%x_5 ↦ 1]]} |}]
 
     let%test _ = implies_eq r14 a (Formula.inject Formula.tt)
 
@@ -415,15 +367,8 @@ let%test_module _ =
 
     let%expect_test _ =
       pp_raw r14 ;
-      [%expect
-        {|
-          {sat= true;
-           rep= [[%x_5 ↦ 1];
-                 [%y_6 ↦ ];
-                 [(%x_5 = 0) ↦ 0];
-                 [(%y_6 = 0) ↦ 0];
-                 [-1 ↦ ];
-                 [0 ↦ ]]} |}]
+      [%expect {|
+          {sat= true; rep= [[%x_5 ↦ 1]]} |}]
 
     let%test _ = implies_eq r14 a (Formula.inject Formula.tt)
     (* incomplete *)
@@ -434,9 +379,8 @@ let%test_module _ =
 
     let%expect_test _ =
       pp_raw r15 ;
-      [%expect
-        {|
-          {sat= true; rep= [[%x_5 ↦ 1]; [-1 ↦ ]; [0 ↦ ]]} |}]
+      [%expect {|
+          {sat= true; rep= [[%x_5 ↦ 1]]} |}]
 
     (* f(x−1)−1=x+1, f(y)+1=y−1, y+1=x ⊢ false *)
     let r16 =
@@ -447,12 +391,10 @@ let%test_module _ =
       [%expect
         {|
       {sat= false;
-       rep= [[%x_5 ↦ (%y_6 + 1)];
+       rep= [[%x_5 ↦ (1 + %y_6)];
              [%y_6 ↦ ];
-             [%y_6^ ↦ (%y_6 + -2)];
-             [(%x_5 + -1)^ ↦ (%y_6 + 3)];
-             [-1 ↦ ];
-             [0 ↦ ]]} |}]
+             [f(%y_6) ↦ (-2 + %y_6)];
+             [f((-1 + %x_5)) ↦ (3 + %y_6)]]} |}]
 
     let%test _ = is_unsat r16
 
@@ -466,10 +408,8 @@ let%test_module _ =
       {sat= false;
        rep= [[%x_5 ↦ ];
              [%y_6 ↦ %x_5];
-             [%x_5^ ↦ %x_5];
-             [%y_6^ ↦ (%x_5 + -1)];
-             [-1 ↦ ];
-             [0 ↦ ]]} |}]
+             [f(%x_5) ↦ %x_5];
+             [f(%y_6) ↦ (-1 + %x_5)]]} |}]
 
     let%test _ = is_unsat r17
 
@@ -482,12 +422,10 @@ let%test_module _ =
         {sat= true;
          rep= [[%x_5 ↦ ];
                [%y_6 ↦ ];
-               [%x_5^ ↦ %x_5];
-               [%y_6^ ↦ (%y_6 + -1)];
-               [-1 ↦ ];
-               [0 ↦ ]]}
+               [f(%x_5) ↦ %x_5];
+               [f(%y_6) ↦ (-1 + %y_6)]]}
 
-          %x_5 = %x_5^ ∧ (-1 + %y_6) = %y_6^ |}]
+          %x_5 = f(%x_5) ∧ (-1 + %y_6) = f(%y_6) |}]
 
     let r19 = of_eqs [(x, y + z); (x, !0); (y, !0)]
 
@@ -495,9 +433,10 @@ let%test_module _ =
       pp_raw r19 ;
       [%expect
         {|
-          {sat= true;
-           rep= [[%x_5 ↦ 0]; [%y_6 ↦ 0]; [%z_7 ↦ 0]; [-1 ↦ ]; [0 ↦ ]]} |}]
+          {sat= true; rep= [[%x_5 ↦ 0]; [%y_6 ↦ 0]; [%z_7 ↦ 0]]} |}]
 
+    let%test _ = implies_eq r19 x !0
+    let%test _ = implies_eq r19 y !0
     let%test _ = implies_eq r19 z !0
 
     let%expect_test _ =
diff --git a/sledge/src/test/sh_test.ml b/sledge/src/test/sh_test.ml
index 58583f13c..e9c344192 100644
--- a/sledge/src/test/sh_test.ml
+++ b/sledge/src/test/sh_test.ml
@@ -15,9 +15,11 @@ let%test_module _ =
     let () = Trace.init ~margin:68 ()
 
     (* let () =
-     *   Trace.init ~margin:160 ~config:(Result.get_ok (Trace.parse "+Sh")) ()
-     *
-     * [@@@warning "-32"] *)
+     *   Trace.init ~margin:160
+     *     ~config:(Result.get_ok (Trace.parse "+Sh+Context+Arithmetic"))
+     *     () *)
+
+    [@@@warning "-32"]
 
     let pp = Format.printf "@\n%a@." pp
     let pp_raw = Format.printf "@\n%a@." pp_raw
diff --git a/sledge/src/test/solver_test.ml b/sledge/src/test/solver_test.ml
index acdbe2ea9..e71762c1a 100644
--- a/sledge/src/test/solver_test.ml
+++ b/sledge/src/test/solver_test.ml
@@ -19,9 +19,9 @@ let%test_module _ =
      *   Trace.init ~margin:160
      *     ~config:
      *       (Result.get_ok (Trace.parse "+Solver.infer_frame+Solver.excise"))
-     *     ()
-     * 
-     * [@@@warning "-32"] *)
+     *     () *)
+
+    [@@@warning "-32"]
 
     let infer_frame p xs q =
       Solver.infer_frame p (Var.Set.of_list xs) q
diff --git a/sledge/src/test/term_test.ml b/sledge/src/test/term_test.ml
index 532a1e588..ea76d9cdb 100644
--- a/sledge/src/test/term_test.ml
+++ b/sledge/src/test/term_test.ml
@@ -5,7 +5,10 @@
  * LICENSE file in the root directory of this source tree.
  *)
 
-open Ses
+open Sledge
+open Fol
+module T = Term
+module F = Formula
 
 (* [@@@warning "-32"] *)
 
@@ -15,46 +18,48 @@ let%test_module _ =
 
     (* let () = Trace.init ~margin:68 ~config:Trace.all () *)
 
-    open Term
-
-    let pp = Format.printf "@\n%a@." pp
-    let ( ! ) i = integer (Z.of_int i)
-    let ( + ) = add
-    let ( - ) = sub
-    let ( * ) = mul
-    let ( = ) = eq
-    let ( != ) = dq
-    let ( < ) = lt
-    let ( <= ) = le
-    let ( && ) = and_
-    let ( || ) = or_
-    let ( ~~ ) = not_
+    let pp = Format.printf "@\n%a@." T.pp
+    let ppf = Format.printf "@\n%a@." F.pp
+    let ( ! ) i = T.integer (Z.of_int i)
+    let ( + ) = T.add
+    let ( - ) = T.sub
+    let ( * ) = T.mul
+    let ( = ) = F.eq
+    let ( != ) = F.dq
+    let ( < ) = F.lt
+    let ( <= ) = F.le
+    let ( && ) = F.and_
+    let ( || ) = F.or_
+    let ( ~~ ) = F.not_
     let wrt = Var.Set.empty
     let y_, wrt = Var.fresh "y" ~wrt
     let z_, _ = Var.fresh "z" ~wrt
-    let y = var y_
-    let z = var z_
+    let y = T.var y_
+    let z = T.var z_
 
-    let%test "booleans distinct" = is_false (true_ = false_)
-    let%test "u1 values distinct" = is_false (one = zero)
-    let%test "boolean overflow" = is_true (minus_one = signed 1 one)
-    let%test _ = is_true (one = unsigned 1 minus_one)
+    let%test "booleans distinct" = F.equal F.ff (F.iff F.tt F.ff)
+    let%test "u1 values distinct" = F.equal F.ff (T.one = T.zero)
+
+    let%test "boolean overflow" =
+      F.equal F.tt (!(-1) = T.apply (Signed 1) [|!1|])
+
+    let%test _ = F.equal F.tt (T.one = T.apply (Unsigned 1) [|!(-1)|])
 
     let%expect_test _ =
       pp (!42 + !13) ;
       [%expect {| 55 |}]
 
     let%expect_test _ =
-      pp (!(-128) && !127) ;
+      pp (T.apply BitAnd [|!(-128); !127|]) ;
       [%expect {| 0 |}]
 
     let%expect_test _ =
-      pp (!(-128) || !127) ;
+      pp (T.apply BitOr [|!(-128); !127|]) ;
       [%expect {| -1 |}]
 
     let%expect_test _ =
       pp (z + !42 + !13) ;
-      [%expect {| (%z_2 + 55) |}]
+      [%expect {| (55 + %z_2) |}]
 
     let%expect_test _ =
       pp (z + !42 + !(-42)) ;
@@ -70,7 +75,7 @@ let%test_module _ =
 
     let%expect_test _ =
       pp ((!2 * z * z) + (!3 * z) + !4) ;
-      [%expect {| (3 × %z_2 + 2 × (%z_2^2) + 4) |}]
+      [%expect {| (4 + 3×%z_2 + 2×%z_2^2) |}]
 
     let%expect_test _ =
       pp
@@ -85,9 +90,8 @@ let%test_module _ =
         + (!9 * z * z * z) ) ;
       [%expect
         {|
-         (3 × %y_1 + 2 × %z_2 + 6 × (%y_1 × %z_2) + 8 × (%y_1 × %z_2^2)
-           + 5 × (%y_1^2) + 7 × (%y_1^2 × %z_2) + 4 × (%z_2^2) + 9 × (%z_2^3)
-           + 1) |}]
+         (1 + 3×%y_1 + 6×(%y_1 × %z_2) + 8×(%y_1 × %z_2^2) + 5×%y_1^2
+           + 7×(%y_1^2 × %z_2) + 2×%z_2 + 4×%z_2^2 + 9×%z_2^3) |}]
 
     let%expect_test _ =
       pp (!0 * z * y) ;
@@ -99,15 +103,15 @@ let%test_module _ =
 
     let%expect_test _ =
       pp (!7 * z * (!2 * y)) ;
-      [%expect {| (14 × (%y_1 × %z_2)) |}]
+      [%expect {| 14×(%y_1 × %z_2) |}]
 
     let%expect_test _ =
       pp (!13 + (!42 * z)) ;
-      [%expect {| (42 × %z_2 + 13) |}]
+      [%expect {| (13 + 42×%z_2) |}]
 
     let%expect_test _ =
       pp ((!13 * z) + !42) ;
-      [%expect {| (13 × %z_2 + 42) |}]
+      [%expect {| (42 + 13×%z_2) |}]
 
     let%expect_test _ =
       pp ((!2 * z) - !3 + ((!(-2) * z) + !3)) ;
@@ -115,31 +119,31 @@ let%test_module _ =
 
     let%expect_test _ =
       pp ((!3 * y) + (!13 * z) + !42) ;
-      [%expect {| (3 × %y_1 + 13 × %z_2 + 42) |}]
+      [%expect {| (42 + 3×%y_1 + 13×%z_2) |}]
 
     let%expect_test _ =
       pp ((!13 * z) + !42 + (!3 * y)) ;
-      [%expect {| (3 × %y_1 + 13 × %z_2 + 42) |}]
+      [%expect {| (42 + 3×%y_1 + 13×%z_2) |}]
 
     let%expect_test _ =
       pp ((!13 * z) + !42 + (!3 * y) + (!2 * z)) ;
-      [%expect {| (3 × %y_1 + 15 × %z_2 + 42) |}]
+      [%expect {| (42 + 3×%y_1 + 15×%z_2) |}]
 
     let%expect_test _ =
       pp ((!13 * z) + !42 + (!3 * y) + (!(-13) * z)) ;
-      [%expect {| (3 × %y_1 + 42) |}]
+      [%expect {| (42 + 3×%y_1) |}]
 
     let%expect_test _ =
       pp (z + !42 + ((!3 * y) + (!(-1) * z))) ;
-      [%expect {| (3 × %y_1 + 42) |}]
+      [%expect {| (42 + 3×%y_1) |}]
 
     let%expect_test _ =
       pp (!(-1) * (z + (!(-1) * y))) ;
-      [%expect {| (%y_1 + -1 × %z_2) |}]
+      [%expect {| (%y_1 + -1×%z_2) |}]
 
     let%expect_test _ =
       pp (((!3 * y) + !2) * (!4 + (!5 * z))) ;
-      [%expect {| (12 × %y_1 + 10 × %z_2 + 15 × (%y_1 × %z_2) + 8) |}]
+      [%expect {| ((2 + 3×%y_1) × (4 + 5×%z_2)) |}]
 
     let%expect_test _ =
       pp (((!2 * z) - !3 + ((!(-2) * z) + !3)) * (!4 + (!5 * z))) ;
@@ -147,112 +151,111 @@ let%test_module _ =
 
     let%expect_test _ =
       pp ((!13 * z) + !42 - ((!3 * y) + (!13 * z))) ;
-      [%expect {| (-3 × %y_1 + 42) |}]
+      [%expect {| (42 + -3×%y_1) |}]
 
     let%expect_test _ =
-      pp (z = y) ;
+      ppf (z = y) ;
       [%expect {| (%y_1 = %z_2) |}]
 
     let%expect_test _ =
-      pp (z = z) ;
-      [%expect {| -1 |}]
+      ppf (z = z) ;
+      [%expect {| tt |}]
 
     let%expect_test _ =
-      pp (z != z) ;
-      [%expect {| 0 |}]
+      ppf (z != z) ;
+      [%expect {| ff |}]
 
     let%expect_test _ =
-      pp (!1 = !0) ;
-      [%expect {| 0 |}]
+      ppf (!1 = !0) ;
+      [%expect {| ff |}]
 
     let%expect_test _ =
-      pp (!3 * y = z = true_) ;
-      [%expect {| (%z_2 = (3 × %y_1)) |}]
+      ppf (F.iff (!3 * y = z) F.tt) ;
+      [%expect {| (3×%y_1 = %z_2) |}]
 
     let%expect_test _ =
-      pp (true_ = (!3 * y = z)) ;
-      [%expect {| (%z_2 = (3 × %y_1)) |}]
+      ppf (F.iff F.tt (!3 * y = z)) ;
+      [%expect {| (3×%y_1 = %z_2) |}]
 
     let%expect_test _ =
-      pp (!3 * y = z = false_) ;
-      [%expect {| (%z_2 ≠ (3 × %y_1)) |}]
+      ppf (F.iff (!3 * y = z) F.ff) ;
+      [%expect {| (3×%y_1 ≠ %z_2) |}]
 
     let%expect_test _ =
-      pp (false_ = (!3 * y = z)) ;
-      [%expect {| (%z_2 ≠ (3 × %y_1)) |}]
+      ppf (F.iff F.ff (!3 * y = z)) ;
+      [%expect {| (3×%y_1 ≠ %z_2) |}]
 
     let%expect_test _ =
       pp (y - (!(-3) * y) + !4) ;
-      [%expect {| (4 × %y_1 + 4) |}]
+      [%expect {| (4 + 4×%y_1) |}]
 
     let%expect_test _ =
       pp ((!(-3) * y) + !4 - y) ;
-      [%expect {| (-4 × %y_1 + 4) |}]
+      [%expect {| (4 + -4×%y_1) |}]
 
     let%expect_test _ =
-      pp (y = (!(-3) * y) + !4) ;
-      [%expect {| (%y_1 = (-3 × %y_1 + 4)) |}]
+      ppf (y = (!(-3) * y) + !4) ;
+      [%expect {| (4 = 4×%y_1) |}]
 
     let%expect_test _ =
-      pp ((!(-3) * y) + !4 = y) ;
-      [%expect {| (%y_1 = (-3 × %y_1 + 4)) |}]
+      ppf ((!(-3) * y) + !4 = y) ;
+      [%expect {| (4 = 4×%y_1) |}]
 
     let%expect_test _ =
-      pp (sub true_ (z = !4)) ;
-      [%expect {| (-1 × (%z_2 = 4) + -1) |}]
+      pp (T.sub (F.inject F.tt) (F.inject (z = !4))) ;
+      [%expect {| ((4 = %z_2) ? 0 : 1) |}]
 
     let%expect_test _ =
-      pp (add true_ (z = !4) = (z = !4)) ;
-      [%expect {| ((%z_2 = 4) = ((%z_2 = 4) + -1)) |}]
+      pp (T.add (F.inject F.tt) (F.inject (F.iff (z = !4) (z = !4)))) ;
+      [%expect {| 2 |}]
 
     let%expect_test _ =
-      pp ((!13 * z) + !42 = (!3 * y) + (!13 * z)) ;
-      [%expect {| ((3 × %y_1 + 13 × %z_2) = (13 × %z_2 + 42)) |}]
+      ppf ((!13 * z) + !42 = (!3 * y) + (!13 * z)) ;
+      [%expect {| (42 = 3×%y_1) |}]
 
     let%expect_test _ =
-      pp ((!13 * z) + !(-42) = (!3 * y) + (!13 * z)) ;
-      [%expect {| ((3 × %y_1 + 13 × %z_2) = (13 × %z_2 + -42)) |}]
+      ppf ((!13 * z) + !(-42) = (!3 * y) + (!13 * z)) ;
+      [%expect {| (-42 = 3×%y_1) |}]
 
     let%expect_test _ =
-      pp ((!13 * z) + !42 = (!(-3) * y) + (!13 * z)) ;
-      [%expect {| ((-3 × %y_1 + 13 × %z_2) = (13 × %z_2 + 42)) |}]
+      ppf ((!13 * z) + !42 = (!(-3) * y) + (!13 * z)) ;
+      [%expect {| (-42 = 3×%y_1) |}]
 
     let%expect_test _ =
-      pp ((!10 * z) + !42 = (!(-3) * y) + (!13 * z)) ;
-      [%expect {| ((-3 × %y_1 + 13 × %z_2) = (10 × %z_2 + 42)) |}]
+      ppf ((!10 * z) + !42 = (!(-3) * y) + (!13 * z)) ;
+      [%expect {| ((42 + 3×%y_1) = 3×%z_2) |}]
 
     let%expect_test _ =
-      pp ~~((!13 * z) + !(-42) != (!3 * y) + (!13 * z)) ;
-      [%expect {| ((3 × %y_1 + 13 × %z_2) = (13 × %z_2 + -42)) |}]
+      ppf ~~((!13 * z) + !(-42) != (!3 * y) + (!13 * z)) ;
+      [%expect {| (-42 = 3×%y_1) |}]
 
     let%expect_test _ =
-      pp ~~(!2 < y && z <= !3) ;
-      [%expect {| ((3 < %z_2) || (%y_1 ≤ 2)) |}]
+      ppf ~~(!2 < y && z <= !3) ;
+      [%expect {| ((3 < %z_2) ∨ (2 ≥ %y_1)) |}]
 
     let%expect_test _ =
-      pp ~~(!2 <= y || z < !3) ;
-      [%expect {| ((%y_1 < 2) && (3 ≤ %z_2)) |}]
+      ppf ~~(!2 <= y || z < !3) ;
+      [%expect {| ((2 > %y_1) ∧ (3 ≤ %z_2)) |}]
 
     let%expect_test _ =
-      pp (eq z zero) ;
-      pp (eq zero z) ;
-      pp (dq (eq zero z) false_) ;
+      ppf (F.eq z T.zero) ;
+      ppf (F.eq T.zero z) ;
+      ppf (F.xor (F.eq T.zero z) F.ff) ;
       [%expect
         {|
-        (%z_2 = 0)
+        (0 = %z_2)
 
-        (%z_2 = 0)
+        (0 = %z_2)
 
-        (%z_2 = 0) |}]
+        (0 = %z_2) |}]
 
     let%expect_test _ =
       let z1 = z + !1 in
       let z1_2 = z1 * z1 in
       pp z1_2 ;
       pp (z1_2 * z1_2) ;
-      [%expect
-        {|
-        (2 × %z_2 + (%z_2^2) + 1)
+      [%expect {|
+        (1 + %z_2)^2
 
-        (4 × %z_2 + 6 × (%z_2^2) + 4 × (%z_2^3) + (%z_2^4) + 1) |}]
+        (1 + %z_2)^4 |}]
   end )