diff --git a/sledge/nonstdlib/NS.ml b/sledge/nonstdlib/NS.ml
index 5c8f0be9c..9da6f75ed 100644
--- a/sledge/nonstdlib/NS.ml
+++ b/sledge/nonstdlib/NS.ml
@@ -183,6 +183,14 @@ module Q = struct
 
   let of_z = Q.of_bigint
 
+  let pow q = function
+    | 1 -> q
+    | 0 -> Q.one
+    | -1 -> Q.inv q
+    | n ->
+        let q, n = if n < 0 then (Q.inv q, -n) else (q, n) in
+        Q.make (Z.pow (Q.num q) n) (Z.pow (Q.den q) n)
+
   include Q
 end
 
diff --git a/sledge/nonstdlib/NS.mli b/sledge/nonstdlib/NS.mli
index 93c60e13a..e6f238325 100644
--- a/sledge/nonstdlib/NS.mli
+++ b/sledge/nonstdlib/NS.mli
@@ -147,6 +147,7 @@ module Q : sig
   val t_of_sexp : Sexp.t -> t
   val sexp_of_t : t -> Sexp.t
   val pp : t pp
+  val pow : t -> int -> t
 end
 
 module Z : sig
diff --git a/sledge/nonstdlib/map.ml b/sledge/nonstdlib/map.ml
index 9acfab4b4..1e0b0b817 100644
--- a/sledge/nonstdlib/map.ml
+++ b/sledge/nonstdlib/map.ml
@@ -62,6 +62,7 @@ end) : S with type key = Key.t = struct
     M.union (fun key v1 v2 -> Some (combine ~key v1 v2)) x y
 
   let union x y ~f = M.union f x y
+  let partition m ~f = M.partition f m
   let is_empty = M.is_empty
 
   let root_key m =
@@ -110,6 +111,22 @@ end) : S with type key = Key.t = struct
   let find_exn m k = M.find k m
   let find m k = M.find_opt k m
 
+  let only_binding m =
+    match root_key m with
+    | Some k -> (
+      match M.split k m with
+      | l, Some v, r when is_empty l && is_empty r -> Some (k, v)
+      | _ -> None )
+    | None -> None
+
+  let classify m =
+    match root_key m with
+    | None -> `Zero
+    | Some k -> (
+      match M.split k m with
+      | l, Some v, r when is_empty l && is_empty r -> `One (k, v)
+      | _ -> `Many )
+
   let find_multi m k =
     match M.find_opt k m with None -> [] | Some vs -> vs
 
diff --git a/sledge/nonstdlib/map_intf.ml b/sledge/nonstdlib/map_intf.ml
index 89026a1f4..0afbeb641 100644
--- a/sledge/nonstdlib/map_intf.ml
+++ b/sledge/nonstdlib/map_intf.ml
@@ -53,12 +53,15 @@ module type S = sig
     'a t -> 'a t -> combine:(key:key -> 'a -> 'a -> 'a) -> 'a t
 
   val union : 'a t -> 'a t -> f:(key -> 'a -> 'a -> 'a option) -> 'a t
+  val partition : 'a t -> f:(key -> 'a -> bool) -> 'a t * 'a t
 
   (** {1 Query} *)
 
   val is_empty : 'a t -> bool
   val is_singleton : 'a t -> bool
   val length : 'a t -> int
+  val only_binding : 'a t -> (key * 'a) option
+  val classify : 'a t -> [`Zero | `One of key * 'a | `Many]
 
   val choose_key : 'a t -> key option
   (** Find an unspecified key. Different keys may be chosen for equivalent
diff --git a/sledge/nonstdlib/multiset.ml b/sledge/nonstdlib/multiset.ml
index f3fa8ddf8..e2429689c 100644
--- a/sledge/nonstdlib/multiset.ml
+++ b/sledge/nonstdlib/multiset.ml
@@ -46,8 +46,8 @@ struct
 
   let pp sep pp_elt fs s = List.pp sep pp_elt fs (M.to_alist s)
   let empty = M.empty
-  let of_ = M.singleton
-  let if_nz q = if Mul.equal Mul.zero q then None else Some q
+  let of_ x i = if Mul.equal Mul.zero i then empty else M.singleton x i
+  let if_nz i = if Mul.equal Mul.zero i then None else Some i
 
   let add m x i =
     M.change m x ~f:(function
@@ -58,6 +58,14 @@ struct
   let find_and_remove = M.find_and_remove
   let union m n = M.union m n ~f:(fun _ i j -> if_nz (Mul.add i j))
 
+  let diff m n =
+    M.merge m n ~f:(fun ~key:_ -> function
+      | `Both (i, j) -> if_nz (Mul.sub i j)
+      | `Left i -> Some i
+      | `Right j -> Some (Mul.neg j) )
+
+  let partition = M.partition
+
   let map m ~f =
     let m' = empty in
     let m, m' =
@@ -67,28 +75,40 @@ struct
             if Mul.equal i' i then (m, m') else (M.set m ~key:x ~data:i', m')
           else (M.remove m x, add m' x' i') )
     in
-    M.fold m' ~init:m ~f:(fun ~key:x ~data:i m -> add m x i)
+    union m m'
+
+  let map_counts m ~f = M.map ~f m
+  let mapi_counts m ~f = M.mapi ~f:(fun ~key ~data -> f key data) m
+
+  let flat_map m ~f =
+    let m' = empty in
+    let m, m' =
+      M.fold m ~init:(m, m') ~f:(fun ~key:x ~data:i (m, m') ->
+          let d = f x i in
+          match M.only_binding d with
+          | Some (x', i') ->
+              if x' == x then
+                if Mul.equal i' i then (m, m')
+                else (M.set m ~key:x ~data:i', m')
+              else (M.remove m x, union m' d)
+          | None -> (M.remove m x, union m' d) )
+    in
+    union m m'
 
-  let map_counts m ~f = M.mapi ~f:(fun ~key ~data -> f key data) m
   let is_empty = M.is_empty
   let is_singleton = M.is_singleton
   let length m = M.length m
   let count m x = match M.find m x with Some q -> q | None -> Mul.zero
+  let only_elt = M.only_binding
+  let classify = M.classify
   let choose = M.choose
   let choose_exn = M.choose_exn
   let pop = M.pop
   let min_elt = M.min_binding
   let pop_min_elt = M.pop_min_binding
-
-  let classify s =
-    match pop s with
-    | None -> `Zero
-    | Some (elt, q, s') when is_empty s' -> `One (elt, q)
-    | _ -> `Many
-
   let to_list m = M.to_alist m
   let iter m ~f = M.iteri ~f:(fun ~key ~data -> f key data) m
   let exists m ~f = M.existsi ~f:(fun ~key ~data -> f key data) m
   let for_all m ~f = M.for_alli ~f:(fun ~key ~data -> f key data) m
-  let fold m ~f ~init = M.fold ~f:(fun ~key ~data -> f key data) m ~init
+  let fold m ~init ~f = M.fold ~f:(fun ~key ~data -> f key data) m ~init
 end
diff --git a/sledge/nonstdlib/multiset_intf.ml b/sledge/nonstdlib/multiset_intf.ml
index ee138a8c3..b31b58909 100644
--- a/sledge/nonstdlib/multiset_intf.ml
+++ b/sledge/nonstdlib/multiset_intf.ml
@@ -44,15 +44,28 @@ module type S = sig
   (** Set the multiplicity of an element to zero. [O(log n)] *)
 
   val union : t -> t -> t
-  (** Sum multiplicities pointwise. [O(n + m)] *)
+  (** Add multiplicities pointwise. [O(n + m)] *)
+
+  val diff : t -> t -> t
+  (** Subtract multiplicities pointwise. [O(n + m)] *)
 
   val map : t -> f:(elt -> mul -> elt * mul) -> t
   (** Map over the elements in ascending order. Preserves physical equality
       if [f] does. *)
 
-  val map_counts : t -> f:(elt -> mul -> mul) -> t
+  val map_counts : t -> f:(mul -> mul) -> t
+  (** Map over the multiplicities of the elements in ascending order. *)
+
+  val mapi_counts : t -> f:(elt -> mul -> mul) -> t
   (** Map over the multiplicities of the elements in ascending order. *)
 
+  val flat_map : t -> f:(elt -> mul -> t) -> t
+  (** Flat map over the elements in ascending order. Preserves physical
+      equality if [f e m] is a singleton [(e', m')] with [e == e'] and
+      [Mul.equal m m'] for all elements. *)
+
+  val partition : t -> f:(elt -> mul -> bool) -> t * t
+
   (* queries *)
 
   val is_empty : t -> bool
@@ -64,6 +77,9 @@ module type S = sig
   val count : t -> elt -> mul
   (** Multiplicity of an element. [O(log n)]. *)
 
+  val only_elt : t -> (elt * mul) option
+  (** The only element of a singleton multiset. [O(1)]. *)
+
   val choose_exn : t -> elt * mul
   (** Find an unspecified element. [O(1)]. *)
 
@@ -99,6 +115,6 @@ module type S = sig
   val for_all : t -> f:(elt -> mul -> bool) -> bool
   (** Test whether all elements satisfy a predicate. *)
 
-  val fold : t -> f:(elt -> mul -> 's -> 's) -> init:'s -> 's
+  val fold : t -> init:'s -> f:(elt -> mul -> 's -> 's) -> 's
   (** Fold over the elements in ascending order. *)
 end
diff --git a/sledge/src/arithmetic.ml b/sledge/src/arithmetic.ml
new file mode 100644
index 000000000..a0e21e6e8
--- /dev/null
+++ b/sledge/src/arithmetic.ml
@@ -0,0 +1,268 @@
+(*
+ * 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.
+ *)
+
+(** Arithmetic terms *)
+
+include Arithmetic_intf
+
+module Representation (Trm : INDETERMINATE) = struct
+  module Prod = struct
+    include Multiset.Make
+              (Int)
+              (struct
+                type t = Trm.trm [@@deriving compare, equal, sexp]
+              end)
+
+    let t_of_sexp = t_of_sexp Trm.trm_of_sexp
+  end
+
+  module Mono = struct
+    type t = Prod.t [@@deriving compare, equal, sexp]
+
+    let num_den m = Prod.partition m ~f:(fun _ i -> i >= 0)
+
+    let ppx strength ppf power_product =
+      let pp_factor ppf (indet, exponent) =
+        if exponent = 1 then (Trm.ppx strength) ppf indet
+        else Format.fprintf ppf "%a^%i" (Trm.ppx strength) indet exponent
+      in
+      let pp_num ppf num =
+        if Prod.is_empty num then Trace.pp_styled `Magenta "1" ppf
+        else Prod.pp "@ @<2>× " pp_factor ppf num
+      in
+      let pp_den ppf den =
+        if not (Prod.is_empty den) then
+          Format.fprintf ppf "@ / %a"
+            (Prod.pp "@ / " pp_factor)
+            (Prod.map_counts ~f:Int.neg den)
+      in
+      let num, den = num_den power_product in
+      Format.fprintf ppf "@[<2>(%a%a)@]" pp_num num pp_den den
+
+    (** [one] is the empty product Πᵢ₌₁⁰ xᵢ^pᵢ *)
+    let one = Prod.empty
+
+    let equal_one = Prod.is_empty
+
+    (** [of_ x₁ p₁] is the singleton product Πᵢ₌₁¹ x₁^p₁ *)
+    let of_ x p = Prod.of_ x p
+
+    (** [pow (Πᵢ₌₁ⁿ xᵢ^pᵢ) p] is Πᵢ₌₁ⁿ xᵢ^(pᵢ×p) *)
+    let pow mono = function
+      | 0 -> Prod.empty
+      | 1 -> mono
+      | power -> Prod.map_counts ~f:(Int.mul power) mono
+
+    let mul x y = Prod.union x y
+
+    (** [get_trm m] is [Some x] iff [equal m (of_ x 1)] *)
+    let get_trm mono =
+      match Prod.only_elt mono with Some (trm, 1) -> Some trm | _ -> None
+  end
+
+  module Sum = struct
+    include Multiset.Make (Q) (Mono)
+
+    let t_of_sexp = t_of_sexp Mono.t_of_sexp
+  end
+
+  module Poly = struct
+    type t = Sum.t [@@deriving compare, equal, sexp]
+    type trm = Trm.trm
+  end
+
+  include Poly
+
+  module Make (Embed : EMBEDDING with type trm := Trm.trm and type t := t) =
+  struct
+    include Poly
+
+    let ppx strength ppf poly =
+      if Sum.is_empty poly then Trace.pp_styled `Magenta "0" ppf
+      else
+        let pp_coeff_mono ppf (m, c) =
+          if Mono.equal_one m then Trace.pp_styled `Magenta "%a" ppf Q.pp c
+          else
+            Format.fprintf ppf "%a @<2>× %a" Q.pp c (Mono.ppx strength) m
+        in
+        Format.fprintf ppf "@[<2>(%a)@]" (Sum.pp "@ + " pp_coeff_mono) poly
+
+    let mono_invariant mono =
+      let@ () = Invariant.invariant [%here] mono [%sexp_of: Mono.t] in
+      Prod.iter mono ~f:(fun base power ->
+          (* powers are non-zero *)
+          assert (not (Int.equal Int.zero power)) ;
+          match Embed.get_arith base with
+          | None -> ()
+          | Some poly -> (
+            match Sum.classify poly with
+            | `Many -> ()
+            | `Zero | `One _ ->
+                (* polynomial factors are not constant or singleton, which
+                   should have been flattened into the parent monomial *)
+                assert false ) ) ;
+      match Mono.get_trm mono with
+      | None -> ()
+      | Some trm -> (
+        match Embed.get_arith trm with
+        | None -> ()
+        | Some _ ->
+            (* singleton monomials are not polynomials, which should have
+               been flattened into the parent polynomial *)
+            assert false )
+
+    let invariant poly =
+      let@ () = Invariant.invariant [%here] poly [%sexp_of: t] in
+      Sum.iter poly ~f:(fun mono coeff ->
+          (* coefficients are non-zero *)
+          assert (not (Q.equal Q.zero coeff)) ;
+          mono_invariant mono )
+
+    (* constants *)
+
+    let const q = Sum.of_ Mono.one q |> check invariant
+    let zero = const Q.zero |> check (fun p -> assert (Sum.is_empty p))
+
+    (* core constructors *)
+
+    let neg poly = Sum.map_counts ~f:Q.neg poly |> check invariant
+    let add p q = Sum.union p q |> check invariant
+    let sub p q = add p (neg q)
+
+    let mulc coeff poly =
+      ( if Q.equal Q.one coeff then poly
+      else if Q.equal Q.zero coeff then zero
+      else Sum.map_counts ~f:(Q.mul coeff) poly )
+      |> check invariant
+
+    (* projections and embeddings *)
+
+    type view = Trm of trm | Const of Q.t | Compound
+
+    let classify poly =
+      match Sum.classify poly with
+      | `Zero -> Const Q.zero
+      | `One (mono, coeff) -> (
+        match Prod.classify mono with
+        | `Zero -> Const coeff
+        | `One (trm, 1) when Q.equal Q.one coeff -> Trm trm
+        | _ -> Compound )
+      | `Many -> Compound
+
+    let get_const poly =
+      match Sum.classify poly with
+      | `Zero -> Some Q.zero
+      | `One (mono, coeff) when Mono.equal_one mono -> Some coeff
+      | _ -> None
+
+    let get_mono poly =
+      match Sum.only_elt poly with
+      | Some (mono, coeff) when Q.equal Q.one coeff -> Some mono
+      | _ -> None
+
+    (** Terms of a polynomial: product of a coefficient and a monomial *)
+    module CM = struct
+      type t = Q.t * Prod.t
+
+      let one = (Q.one, Mono.one)
+      let equal_one (c, m) = Mono.equal_one m && Q.equal Q.one c
+      let mul (c1, m1) (c2, m2) = (Q.mul c1 c2, Mono.mul m1 m2)
+
+      (** Monomials [Mono.t] have [trm] indeterminates, which include, via
+          [get_arith], polynomials [t] over monomials themselves. To avoid
+          redundant representations, singleton polynomials are flattened. *)
+      let of_trm : ?power:int -> trm -> t =
+       fun ?(power = 1) base ->
+        match Embed.get_arith base with
+        | Some poly -> (
+          match Sum.classify poly with
+          (* 0 ^ p₁ ==> 0 × 1 *)
+          | `Zero -> (Q.zero, Mono.one)
+          (* (Σᵢ₌₁¹ cᵢ × Xᵢ) ^ p₁ ==> cᵢ^p₁ × Πⱼ₌₁¹ Xⱼ^pⱼ *)
+          | `One (mono, coeff) -> (Q.pow coeff power, Mono.pow mono power)
+          (* (Σᵢ₌₁ⁿ cᵢ × Xᵢ) ^ p₁ ==> 1 × Πⱼ₌₁¹ (Σᵢ₌₁ⁿ cᵢ × Xᵢ)^pⱼ *)
+          | `Many -> (Q.one, Mono.of_ base power) )
+        (* X₁ ^ p₁ ==> 1 × Πⱼ₌₁¹ Xⱼ^pⱼ *)
+        | None -> (Q.one, Mono.of_ base power)
+
+      (** Polynomials [t] have [trm] indeterminates, which, via [get_arith],
+          include polynomials themselves. To avoid redundant
+          representations, singleton monomials are flattened. Also, constant
+          multiplication is not interpreted in [Prod], so constant
+          polynomials are multiplied by their coefficients directly. *)
+      let to_poly : t -> Poly.t =
+       fun (coeff, mono) ->
+        ( match Mono.get_trm mono with
+        | Some trm -> (
+          match Embed.get_arith trm with
+          (* c × (Σᵢ₌₁ⁿ cᵢ × Xᵢ) ==> Σᵢ₌₁ⁿ c×cᵢ × Xᵢ *)
+          | Some poly -> mulc coeff poly
+          (* c₁ × X₁ ==> Σᵢ₌₁¹ cᵢ × Xᵢ *)
+          | None -> Sum.of_ mono coeff )
+        (* c₁ × (Πⱼ₌₁ᵐ X₁ⱼ^p₁ⱼ) ==> Σᵢ₌₁¹ cᵢ × (Πⱼ₌₁ᵐ Xᵢⱼ^pᵢⱼ) *)
+        | None -> Sum.of_ mono coeff )
+        |> check invariant
+    end
+
+    (** Embed a term into a polynomial, by projecting a polynomial out of
+        the term if possible *)
+    let trm trm =
+      ( match Embed.get_arith trm with
+      | Some poly -> poly
+      | None -> Sum.of_ (Mono.of_ trm 1) Q.one )
+      |> check (fun poly ->
+             assert (equal poly (CM.to_poly (CM.of_trm trm))) )
+
+    (** Project out the term embedded into a polynomial, if possible *)
+    let get_trm poly =
+      match get_mono poly with
+      | Some mono -> Mono.get_trm mono
+      | None -> None
+
+    (* constructors over indeterminates *)
+
+    let mul e1 e2 = CM.to_poly (CM.mul (CM.of_trm e1) (CM.of_trm e2))
+
+    let div n d =
+      CM.to_poly (CM.mul (CM.of_trm n) (CM.of_trm d ~power:(-1)))
+
+    let pow base power = CM.to_poly (CM.of_trm base ~power)
+
+    (* transform *)
+
+    let map poly ~f =
+      let p, p' = (poly, Sum.empty) in
+      let p, p' =
+        Sum.fold poly ~init:(p, p') ~f:(fun mono coeff (p, p') ->
+            let m, cm' = (mono, CM.one) in
+            let m, cm' =
+              Prod.fold mono ~init:(m, cm') ~f:(fun trm power (m, cm') ->
+                  let trm' = f trm in
+                  if trm == trm' then (m, cm')
+                  else
+                    (Prod.remove m trm, CM.mul cm' (CM.of_trm trm' ~power)) )
+            in
+            if CM.equal_one cm' then (p, p')
+            else
+              ( Sum.remove p mono
+              , Sum.union p' (CM.to_poly (CM.mul (coeff, m) cm')) ) )
+      in
+      if Sum.is_empty p' then poly else Sum.union p p' |> check invariant
+
+    (* traverse *)
+
+    let iter poly =
+      Iter.from_iter (fun f ->
+          Sum.iter poly ~f:(fun mono _ ->
+              Prod.iter mono ~f:(fun trm _ -> f trm) ) )
+
+    type product = Prod.t
+
+    let fold_factors = Prod.fold
+    let fold_monomials = Sum.fold
+  end
+end
diff --git a/sledge/src/arithmetic.mli b/sledge/src/arithmetic.mli
new file mode 100644
index 000000000..96bf41b65
--- /dev/null
+++ b/sledge/src/arithmetic.mli
@@ -0,0 +1,15 @@
+(*
+ * 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.
+ *)
+
+(** Arithmetic terms *)
+
+include module type of Arithmetic_intf
+
+module Representation (Indeterminate : INDETERMINATE) :
+  REPRESENTATION
+    with type var := Indeterminate.var
+    with type trm := Indeterminate.trm
diff --git a/sledge/src/arithmetic_intf.ml b/sledge/src/arithmetic_intf.ml
new file mode 100644
index 000000000..36b2a9138
--- /dev/null
+++ b/sledge/src/arithmetic_intf.ml
@@ -0,0 +1,104 @@
+(*
+ * 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.
+ *)
+
+(** Arithmetic terms *)
+
+open Ses
+
+module type S = sig
+  type var
+  type trm
+  type t [@@deriving compare, equal, sexp]
+
+  val ppx : var Var.strength -> t pp
+
+  (** Construct and Destruct atomic terms *)
+
+  val const : Q.t -> t
+  (** [const q] represents the constant [q] *)
+
+  val get_const : t -> Q.t option
+  (** [get_const a] is [Some q] iff [equal a (const q)] *)
+
+  val trm : trm -> t
+  (** [trm x] represents the indeterminate term [x] *)
+
+  val get_trm : t -> trm option
+  (** [get_trm a] is [Some x] iff [equal a (trm x)] *)
+
+  type view = Trm of trm | Const of Q.t | Compound
+
+  val classify : t -> view
+  (** [classify a] is [Trm x] iff [get_trm a] is [Some x], [Const q] iff
+      [get_const a] is [Some q], and [Compound] otherwise *)
+
+  (** Construct compound terms *)
+
+  val neg : t -> t
+  val add : t -> t -> t
+  val sub : t -> t -> t
+  val mulc : Q.t -> t -> t
+  val mul : trm -> trm -> t
+  val div : trm -> trm -> t
+  val pow : trm -> int -> t
+
+  (** Transform *)
+
+  val map : t -> f:(trm -> trm) -> t
+  (** [map ~f a] is [a] with each indeterminate transformed by [f]. Viewing
+      [a] as a polynomial,
+      [map ~f (Σᵢ₌₁ⁿ cᵢ × Πⱼ₌₁ᵐᵢ xᵢⱼ^pᵢⱼ)] is
+      [Σᵢ₌₁ⁿ cᵢ × Πⱼ₌₁ᵐᵢ (f xᵢⱼ)^pᵢⱼ]. *)
+
+  (** Traverse *)
+
+  val iter : t -> trm iter
+  (** [iter a] enumerates the indeterminate terms appearing in [a] *)
+
+  (**/**)
+
+  type product
+
+  val fold_factors : product -> init:'s -> f:(trm -> int -> 's -> 's) -> 's
+  val fold_monomials : t -> init:'s -> f:(product -> Q.t -> 's -> 's) -> 's
+end
+
+(** Indeterminate terms, treated as atomic / variables except when they can
+    be flattened using [EMBEDDING.get_arith]. *)
+module type INDETERMINATE = sig
+  type trm [@@deriving compare, equal, sexp]
+  type var
+
+  val ppx : var Var.strength -> trm pp
+end
+
+(** An embedding of arithmetic terms [t] into indeterminates [trm],
+    expressed as a partial projection from [trm] to [t]. The inverse
+    embedding function is generally internal to the client. *)
+module type EMBEDDING = sig
+  type trm
+  type t
+
+  val get_arith : trm -> t option
+  (** [get_arith x] should be [Some a] if indeterminate [x] is equivalent to
+      [a] embedded into an indeterminate term. This is used to flatten
+      indeterminates that are actually arithmetic for the client, thereby
+      enabling arithmetic operations to be interpreted more often. *)
+end
+
+(** A type [t] representing arithmetic terms over indeterminates [trm]
+    together with a functor [Make] that takes an [EMBEDDING] of arithmetic
+    terms [t] into indeterminates [trm] and produces an implementation of
+    the primary interface [S]. *)
+module type REPRESENTATION = sig
+  type t [@@deriving compare, equal, sexp]
+  type var
+  type trm
+
+  module Make (_ : EMBEDDING with type trm := trm and type t := t) :
+    S with type var := var with type trm := trm with type t := t
+end
diff --git a/sledge/src/fol.ml b/sledge/src/fol.ml
index 913862dac..4f669d511 100644
--- a/sledge/src/fol.ml
+++ b/sledge/src/fol.ml
@@ -5,110 +5,239 @@
  * LICENSE file in the root directory of this source tree.
  *)
 
+open Ses
+
 let pp_boxed fs fmt =
   Format.pp_open_box fs 2 ;
   Format.kfprintf (fun fs -> Format.pp_close_box fs ()) fs fmt
 
-module Funsym = Ses.Funsym
-module Predsym = Ses.Predsym
-
 (*
  * Terms
  *)
 
-(** Terms, denoting functions from structures to values, built from
-    variables and applications of function symbols from various theories. *)
-type trm =
-  (* variables *)
-  | Var of {id: int; name: string}
-  (* arithmetic *)
-  | Z of Z.t
-  | Q of Q.t
-  | Neg of trm
-  | Add of trm * trm
-  | Sub of trm * trm
-  | Mulq of Q.t * trm
-  (* sequences (of non-fixed size) *)
-  | Splat of trm
-  | Sized of {seq: trm; siz: trm}
-  | Extract of {seq: trm; off: trm; len: trm}
-  | Concat of trm array
-  (* records (with fixed indices) *)
-  | Select of {idx: int; rcd: trm}
-  | Update of {idx: int; rcd: trm; elt: trm}
-  | Record of trm array
-  | Ancestor of int
-  (* uninterpreted *)
-  | Apply of Funsym.t * trm array
-[@@deriving compare, equal, sexp]
-
-let compare_trm x y =
-  if x == y then 0
-  else
-    match (x, y) with
-    | Var {id= i; name= _}, Var {id= j; name= _} when i > 0 && j > 0 ->
-        Int.compare i j
-    | _ -> compare_trm x y
+(** Variable terms, represented as a subtype of general terms *)
+module rec Var : sig
+  include Var_intf.VAR with type t = private Trm.trm
 
-let equal_trm x y =
-  x == y
-  ||
-  match (x, y) with
-  | Var {id= i; name= _}, Var {id= j; name= _} when i > 0 && j > 0 ->
-      Int.equal i j
-  | _ -> equal_trm x y
+  val of_ : Trm.trm -> t
+end = struct
+  module T = struct
+    type t = Trm.trm [@@deriving compare, equal, sexp]
 
-(* destructors *)
+    let invariant x =
+      let@ () = Invariant.invariant [%here] x [%sexp_of: t] in
+      match x with
+      | Var _ -> ()
+      | _ -> fail "non-var: %a" Sexp.pp_hum (sexp_of_t x) ()
 
-let get_z = function Z z -> Some z | _ -> None
-let get_q = function Q q -> Some q | Z z -> Some (Q.of_z z) | _ -> None
+    let make ~id ~name = Trm._Var id name |> check invariant
+    let id = function Trm.Var v -> v.id | x -> violates invariant x
+    let name = function Trm.Var v -> v.name | x -> violates invariant x
+  end
 
-(* constructors *)
+  include Var0.Make (T)
 
-(* statically allocated since they are tested with == *)
-let zero = Z Z.zero
-let one = Z Z.one
+  let of_ v = v |> check T.invariant
+end
 
-let _Z z =
-  if Z.equal Z.zero z then zero else if Z.equal Z.one z then one else Z z
+and Arith0 :
+  (Arithmetic.REPRESENTATION
+    with type var := Var.t
+    with type trm := Trm.trm) =
+  Arithmetic.Representation (Trm)
+
+and Arith :
+  (Arithmetic.S
+    with type var := Var.t
+    with type trm := Trm.trm
+    with type t = Arith0.t) = struct
+  include Arith0
+
+  include Make (struct
+    let get_arith (e : Trm.trm) =
+      match e with
+      | Z z -> Some (Arith.const (Q.of_z z))
+      | Q q -> Some (Arith.const q)
+      | Arith a -> Some a
+      | _ -> None
+  end)
+end
 
-let _Q q = if Z.equal Z.one (Q.den q) then _Z (Q.num q) else Q q
-let _Neg x = Neg x
+(** Terms, built from variables and applications of function symbols from
+    various theories. Denote functions from structures to values. *)
+and Trm : sig
+  type var = Var.t
 
-let _Add x y =
-  match (x, y) with
-  | _, Q q when Q.sign q = 0 -> x
-  | Q q, _ when Q.sign q = 0 -> y
-  | _ -> Add (x, y)
+  type trm = private
+    (* variables *)
+    | Var of {id: int; name: string}
+    (* arithmetic *)
+    | Z of Z.t
+    | Q of Q.t
+    | Arith of Arith.t
+    (* sequences (of flexible size) *)
+    | Splat of trm
+    | Sized of {seq: trm; siz: trm}
+    | Extract of {seq: trm; off: trm; len: trm}
+    | Concat of trm array
+    (* records (with fixed indices) *)
+    | Select of {idx: int; rcd: trm}
+    | Update of {idx: int; rcd: trm; elt: trm}
+    | Record of trm array
+    | Ancestor of int
+    (* uninterpreted *)
+    | Apply of Funsym.t * trm array
+  [@@deriving compare, equal, sexp]
 
-let _Sub x y = Sub (x, y)
+  val ppx : Var.t Var.strength -> trm pp
+  val _Var : int -> string -> trm
+  val _Z : Z.t -> trm
+  val _Q : Q.t -> trm
+  val _Arith : Arith.t -> trm
+  val _Splat : trm -> trm
+  val _Sized : trm -> trm -> trm
+  val _Extract : trm -> trm -> trm -> trm
+  val _Concat : trm array -> trm
+  val _Select : int -> trm -> trm
+  val _Update : int -> trm -> trm -> trm
+  val _Record : trm array -> trm
+  val _Ancestor : int -> trm
+  val _Apply : Funsym.t -> trm array -> trm
+end = struct
+  type var = Var.t
+
+  type trm =
+    | Var of {id: int; name: string}
+    | Z of Z.t
+    | Q of Q.t
+    | Arith of Arith.t
+    | Splat of trm
+    | Sized of {seq: trm; siz: trm}
+    | Extract of {seq: trm; off: trm; len: trm}
+    | Concat of trm array
+    | Select of {idx: int; rcd: trm}
+    | Update of {idx: int; rcd: trm; elt: trm}
+    | Record of trm array
+    | Ancestor of int
+    | Apply of Funsym.t * trm array
+  [@@deriving compare, equal, sexp]
 
-let _Mulq q x =
-  if Q.equal Q.one q then x else if Q.sign q = 0 then zero else Mulq (q, x)
+  let compare_trm x y =
+    if x == y then 0
+    else
+      match (x, y) with
+      | Var {id= i; name= _}, Var {id= j; name= _} when i > 0 && j > 0 ->
+          Int.compare i j
+      | _ -> compare_trm x y
+
+  let equal_trm x y =
+    x == y
+    ||
+    match (x, y) with
+    | Var {id= i; name= _}, Var {id= j; name= _} when i > 0 && j > 0 ->
+        Int.equal i j
+    | _ -> equal_trm x y
+
+  let rec ppx strength fs trm =
+    let rec pp fs trm =
+      let pf fmt = pp_boxed fs fmt in
+      match trm with
+      | Var _ as v -> Var.ppx strength fs (Var.of_ v)
+      | Z z -> Trace.pp_styled `Magenta "%a" fs Z.pp z
+      | Q q -> Trace.pp_styled `Magenta "%a" fs Q.pp q
+      | Arith a -> Arith.ppx strength fs a
+      | Splat x -> pf "%a^" pp x
+      | Sized {seq; siz} -> pf "@<1>⟨%a,%a@<1>⟩" pp siz pp seq
+      | Extract {seq; off; len} -> pf "%a[%a,%a)" pp seq pp off pp len
+      | Concat [||] -> pf "@<2>⟨⟩"
+      | Concat xs -> pf "(%a)" (Array.pp "@,^" pp) xs
+      | Select {idx; rcd} -> pf "%a[%i]" pp rcd idx
+      | Update {idx; rcd; elt} ->
+          pf "[%a@ @[| %i → %a@]]" pp rcd idx pp elt
+      | Record xs -> pf "{%a}" (ppx_record strength) xs
+      | Ancestor i -> pf "(ancestor %i)" i
+      | Apply (f, [||]) -> pf "%a" Funsym.pp f
+      | Apply
+          ( ( (Rem | BitAnd | BitOr | BitXor | BitShl | BitLshr | BitAshr)
+            as f )
+          , [|x; y|] ) ->
+          pf "(%a@ %a@ %a)" pp x Funsym.pp f pp y
+      | Apply (f, es) ->
+          pf "%a(%a)" Funsym.pp f (Array.pp ",@ " (ppx strength)) es
+    in
+    pp fs trm
+
+  and ppx_record strength fs elts =
+    [%Trace.fprintf
+      fs "%a"
+        (fun fs elts ->
+          let exception Not_a_string in
+          match
+            String.init (Array.length elts) ~f:(fun i ->
+                match elts.(i) with
+                | Z c -> Char.of_int_exn (Z.to_int c)
+                | _ -> raise Not_a_string )
+          with
+          | s -> Format.fprintf fs "%S" s
+          | exception (Not_a_string | Z.Overflow | Failure _) ->
+              Format.fprintf fs "@[<h>%a@]"
+                (Array.pp ",@ " (ppx strength))
+                elts )
+        elts]
+
+  (* destructors *)
+
+  let get_z = function Z z -> Some z | _ -> None
+  let get_q = function Q q -> Some q | Z z -> Some (Q.of_z z) | _ -> None
+
+  (* constructors *)
+
+  let _Var id name = Var {id; name}
+
+  (* statically allocated since they are tested with == *)
+  let zero = Z Z.zero
+  let one = Z Z.one
+
+  let _Z z =
+    if Z.equal Z.zero z then zero else if Z.equal Z.one z then one else Z z
+
+  let _Q q = if Z.equal Z.one (Q.den q) then _Z (Q.num q) else Q q
+
+  let _Arith a =
+    match Arith.classify a with
+    | Trm e -> e
+    | Const q -> _Q q
+    | Compound -> Arith a
+
+  let _Splat x = Splat x
+  let _Sized seq siz = Sized {seq; siz}
+  let _Extract seq off len = Extract {seq; off; len}
+  let _Concat es = Concat es
+  let _Select idx rcd = Select {idx; rcd}
+  let _Update idx rcd elt = Update {idx; rcd; elt}
+  let _Record es = Record es
+  let _Ancestor i = Ancestor i
+
+  let _Apply f es =
+    match
+      Funsym.eval ~equal:equal_trm ~get_z ~ret_z:_Z ~get_q ~ret_q:_Q f es
+    with
+    | Some c -> c
+    | None -> Apply (f, es)
+end
 
-let _Splat x = Splat x
-let _Sized seq siz = Sized {seq; siz}
-let _Extract seq off len = Extract {seq; off; len}
-let _Concat es = Concat es
-let _Select idx rcd = Select {idx; rcd}
-let _Update idx rcd elt = Update {idx; rcd; elt}
-let _Record es = Record es
-let _Ancestor i = Ancestor i
+open Trm
 
-let _Apply f es =
-  match
-    Funsym.eval ~equal:equal_trm ~get_z ~ret_z:_Z ~get_q ~ret_q:_Q f es
-  with
-  | Some c -> c
-  | None -> Apply (f, es)
+let zero = _Z Z.zero
+let one = _Z Z.one
 
 (*
  * Formulas
  *)
 
-(** Formulas, denoting sets of structures, built from propositional
-    variables, applications of predicate symbols from various theories, and
-    first-order logic connectives. *)
+(** Formulas, built from literals with predicate symbols from various
+    theories, and propositional constants and connectives. Denote sets of
+    structures. *)
 module Fml : sig
   type fml = private
     (* propositional constants *)
@@ -421,96 +550,14 @@ type cnd = [`Ite of fml * cnd * cnd | `Trm of trm]
     formulas. *)
 type exp = [cnd | `Fml of fml] [@@deriving compare, equal, sexp]
 
-(*
- * Variables
- *)
-
-(** Variable terms *)
-module Var : sig
-  include Ses.Var_intf.VAR with type t = private trm
-
-  val of_ : trm -> t
-end = struct
-  module T = struct
-    type t = trm [@@deriving compare, equal, sexp]
-  end
-
-  let invariant (x : trm) =
-    let@ () = Invariant.invariant [%here] x [%sexp_of: trm] in
-    match x with
-    | Var _ -> ()
-    | _ -> fail "non-var: %a" Sexp.pp_hum (sexp_of_trm x) ()
-
-  include Ses.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
-end
-
-type var = Var.t
-
 (*
  * Representation operations
  *)
 
 (** pp *)
 
-let rec ppx_t strength fs trm =
-  let rec pp fs trm =
-    let pf fmt = pp_boxed fs fmt in
-    match trm with
-    | Var _ as v -> Var.ppx strength fs (Var.of_ v)
-    | Z z -> Trace.pp_styled `Magenta "%a" fs Z.pp z
-    | Q q -> Trace.pp_styled `Magenta "%a" fs Q.pp q
-    | Neg x -> pf "(- %a)" pp x
-    | Add (x, y) -> pf "(%a@ + %a)" pp x pp y
-    | Sub (x, y) -> pf "(%a@ - %a)" pp x pp y
-    | Mulq (q, x) -> pf "(%a@ @<2>× %a)" Q.pp q pp x
-    | Splat x -> pf "%a^" pp x
-    | Sized {seq; siz} -> pf "@<1>⟨%a,%a@<1>⟩" pp siz pp seq
-    | Extract {seq; off; len} -> pf "%a[%a,%a)" pp seq pp off pp len
-    | Concat [||] -> pf "@<2>⟨⟩"
-    | Concat xs -> pf "(%a)" (Array.pp "@,^" pp) xs
-    | Select {idx; rcd} -> pf "%a[%i]" pp rcd idx
-    | Update {idx; rcd; elt} -> pf "[%a@ @[| %i → %a@]]" pp rcd idx pp elt
-    | Record xs -> pf "{%a}" (ppx_record strength) xs
-    | Ancestor i -> pf "(ancestor %i)" i
-    | Apply (f, [||]) -> pf "%a" Funsym.pp f
-    | Apply
-        ( ( ( Mul | Div | Rem | BitAnd | BitOr | BitXor | BitShl | BitLshr
-            | BitAshr ) as f )
-        , [|x; y|] ) ->
-        pf "(%a@ %a@ %a)" pp x Funsym.pp f pp y
-    | Apply (f, es) ->
-        pf "%a(%a)" Funsym.pp f (Array.pp ",@ " (ppx_t strength)) es
-  in
-  pp fs trm
-
-and ppx_record strength fs elts =
-  [%Trace.fprintf
-    fs "%a"
-      (fun fs elts ->
-        let exception Not_a_string in
-        match
-          String.init (Array.length elts) ~f:(fun i ->
-              match elts.(i) with
-              | Z c -> Char.of_int_exn (Z.to_int c)
-              | _ -> raise Not_a_string )
-        with
-        | s -> Format.fprintf fs "%S" s
-        | exception (Not_a_string | Z.Overflow | Failure _) ->
-            Format.fprintf fs "@[<h>%a@]"
-              (Array.pp ",@ " (ppx_t strength))
-              elts )
-      elts]
-
 let ppx_f strength fs fml =
-  let pp_t = ppx_t strength in
+  let pp_t = Trm.ppx strength in
   let rec pp fs fml =
     let pf fmt = pp_boxed fs fmt in
     match (fml : fml) with
@@ -539,7 +586,7 @@ let ppx_f strength fs fml =
 let pp_f = ppx_f (fun _ -> None)
 
 let ppx_c strength fs ct =
-  let pp_t = ppx_t strength in
+  let pp_t = Trm.ppx strength in
   let pp_f = ppx_f strength in
   let rec pp fs ct =
     let pf fmt = pp_boxed fs fmt in
@@ -559,20 +606,20 @@ let pp = ppx (fun _ -> None)
 
 let rec fold_vars_t e ~init ~f =
   match e with
-  | Var _ as v -> f init (Var.of_ v)
   | Z _ | Q _ | Ancestor _ -> init
-  | Neg x | Mulq (_, x) | Splat x | Select {rcd= x} ->
-      fold_vars_t ~f x ~init
-  | Add (x, y)
-   |Sub (x, y)
-   |Sized {seq= x; siz= y}
-   |Update {rcd= x; elt= y} ->
+  | Var _ as v -> f init (Var.of_ v)
+  | Splat x | Select {rcd= x} -> fold_vars_t ~f x ~init
+  | Sized {seq= x; siz= y} | Update {rcd= x; elt= y} ->
       fold_vars_t ~f x ~init:(fold_vars_t ~f y ~init)
   | Extract {seq= x; off= y; len= z} ->
       fold_vars_t ~f x
         ~init:(fold_vars_t ~f y ~init:(fold_vars_t ~f z ~init))
   | Concat xs | Record xs | Apply (_, xs) ->
       Array.fold ~f:(fun init -> fold_vars_t ~f ~init) xs ~init
+  | Arith a ->
+      Iter.fold
+        ~f:(fun s x -> fold_vars_t ~f x ~init:s)
+        ~init (Arith.iter a)
 
 let rec fold_vars_f ~init p ~f =
   match (p : fml) with
@@ -645,11 +692,10 @@ let rec map_trms_f ~f b =
 let rec map_vars_t ~f e =
   match e with
   | Var _ as v -> (f (Var.of_ v) : var :> trm)
-  | Z _ | Q _ | Ancestor _ -> e
-  | Neg x -> map1 (map_vars_t ~f) e _Neg x
-  | Add (x, y) -> map2 (map_vars_t ~f) e _Add x y
-  | Sub (x, y) -> map2 (map_vars_t ~f) e _Sub x y
-  | Mulq (q, x) -> map1 (map_vars_t ~f) e (_Mulq q) x
+  | Z _ | Q _ -> e
+  | Arith a ->
+      let a' = Arith.map ~f:(map_vars_t ~f) a in
+      if a == a' then e else _Arith a'
   | Splat x -> map1 (map_vars_t ~f) e _Splat x
   | Sized {seq; siz} -> map2 (map_vars_t ~f) e _Sized seq siz
   | Extract {seq; off; len} -> map3 (map_vars_t ~f) e _Extract seq off len
@@ -657,6 +703,7 @@ let rec map_vars_t ~f e =
   | Select {idx; rcd} -> map1 (map_vars_t ~f) e (_Select idx) rcd
   | Update {idx; rcd; elt} -> map2 (map_vars_t ~f) e (_Update idx) rcd elt
   | Record xs -> mapN (map_vars_t ~f) e _Record xs
+  | Ancestor _ -> e
   | Apply (g, xs) -> mapN (map_vars_t ~f) e (_Apply g) xs
 
 let map_vars_f ~f = map_trms_f ~f:(map_vars_t ~f)
@@ -844,35 +891,19 @@ module Term = struct
 
   let var v = `Trm (v : var :> trm)
 
-  (* constants *)
+  (* arithmetic *)
 
   let zero = `Trm zero
   let one = `Trm one
-
-  let integer z =
-    if Z.equal Z.zero z then zero
-    else if Z.equal Z.one z then one
-    else `Trm (Z z)
-
-  let rational q = `Trm (Q q)
-
-  (* arithmetic *)
-
-  let neg = ap1t _Neg
-  let add = ap2t _Add
-  let sub = ap2t _Sub
-  let mulq q = ap1t (_Mulq q)
-
-  let mul =
-    ap2 (fun x y ->
-        match x with
-        | Z z -> mulq (Q.of_z z) (`Trm y)
-        | Q q -> mulq q (`Trm y)
-        | _ -> (
-          match y with
-          | Z z -> mulq (Q.of_z z) (`Trm x)
-          | Q q -> mulq q (`Trm x)
-          | _ -> ap2t (fun x y -> Apply (Mul, [|x; y|])) (`Trm x) (`Trm y) ) )
+  let integer z = `Trm (_Z z)
+  let rational q = `Trm (_Q q)
+  let neg = ap1t @@ fun x -> _Arith Arith.(neg (trm x))
+  let add = ap2t @@ fun x y -> _Arith Arith.(add (trm x) (trm y))
+  let sub = ap2t @@ fun x y -> _Arith Arith.(sub (trm x) (trm y))
+  let mulq q = ap1t @@ fun x -> _Arith Arith.(mulc q (trm x))
+  let mul = ap2t @@ fun x y -> _Arith (Arith.mul x y)
+  let div = ap2t @@ fun x y -> _Arith (Arith.div x y)
+  let pow x i = (ap1t @@ fun x -> _Arith (Arith.pow x i)) x
 
   (* sequences *)
 
@@ -888,33 +919,25 @@ module Term = struct
   let record elts = apNt _Record elts
   let ancestor i = `Trm (_Ancestor i)
 
-  (* if-then-else *)
-
-  let ite ~cnd ~thn ~els = ite cnd thn els
-
   (* uninterpreted *)
 
   let apply sym args = apNt (_Apply sym) args
 
+  (* if-then-else *)
+
+  let ite ~cnd ~thn ~els = ite cnd thn els
+
   (** Destruct *)
 
   let d_int = function `Trm (Z z) -> Some z | _ -> None
 
   (** Access *)
 
-  let const_of x =
-    let rec const_of t =
-      let neg = Option.map ~f:Q.neg in
-      let add = Option.map2 ~f:Q.add in
-      match t with
-      | Z z -> Some (Q.of_z z)
-      | Q q -> Some q
-      | Neg x -> neg (const_of x)
-      | Add (x, y) -> add (const_of x) (const_of y)
-      | Sub (x, y) -> add (const_of x) (neg (const_of y))
-      | _ -> None
-    in
-    match x with `Trm t -> const_of t | _ -> None
+  let const_of = function
+    | `Trm (Z z) -> Some (Q.of_z z)
+    | `Trm (Q q) -> Some q
+    | `Trm (Arith a) -> Arith.get_const a
+    | _ -> None
 
   (** Traverse *)
 
@@ -1093,14 +1116,22 @@ let vs_to_ses : Var.Set.t -> Ses.Var.Set.t =
   Var.Set.fold vs ~init:Ses.Var.Set.empty ~f:(fun vs v ->
       Ses.Var.Set.add vs (v_to_ses v) )
 
-let rec t_to_ses : trm -> Ses.Term.t = function
+let rec arith_to_ses poly =
+  Arith.fold_monomials poly ~init:Ses.Term.zero ~f:(fun mono coeff e ->
+      Ses.Term.add e
+        (Ses.Term.mulq coeff
+           (Arith.fold_factors mono ~init: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
-  | Neg x -> Ses.Term.neg (t_to_ses x)
-  | Add (x, y) -> Ses.Term.add (t_to_ses x) (t_to_ses y)
-  | Sub (x, y) -> Ses.Term.sub (t_to_ses x) (t_to_ses y)
-  | Mulq (q, x) -> Ses.Term.mulq q (t_to_ses x)
+  | 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)
@@ -1114,8 +1145,6 @@ let rec t_to_ses : trm -> Ses.Term.t = function
   | Record es ->
       Ses.Term.record (IArray.of_array (Array.map ~f:t_to_ses es))
   | Ancestor i -> Ses.Term.rec_record i
-  | Apply (Mul, [|x; y|]) -> Ses.Term.mul (t_to_ses x) (t_to_ses y)
-  | Apply (Div, [|x; y|]) -> Ses.Term.div (t_to_ses x) (t_to_ses y)
   | 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)
@@ -1171,8 +1200,8 @@ let vs_of_ses : Ses.Var.Set.t -> Var.Set.t =
   Ses.Var.Set.fold vs ~init:Var.Set.empty ~f:(fun vs v ->
       Var.Set.add vs (v_of_ses v) )
 
-let uap1 f = ap1t (fun x -> Apply (f, [|x|]))
-let uap2 f = ap2t (fun x y -> Apply (f, [|x; y|]))
+let uap1 f = ap1t (fun x -> _Apply f [|x|])
+let uap2 f = ap2t (fun x y -> _Apply f [|x; y|])
 let uposN p = apNf (_UPosLit p)
 let unegN p = apNf (_UNegLit p)
 
@@ -1237,18 +1266,18 @@ and of_ses : Ses.Term.t -> exp =
     | Some (e, q, prod) ->
         let rec expn e n =
           let p = Z.pred n in
-          if Z.sign p = 0 then e else uap2 Mul e (expn e p)
+          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 uap2 Div one (expn (of_ses e) (Z.neg n))
+          else div one (expn (of_ses e) (Z.neg n))
         in
         Ses.Term.Qset.fold prod ~init:(exp e q) ~f:(fun e q s ->
-            uap2 Mul (exp e q) s ) )
-  | Ap2 (Div, d, e) -> uap_ttt Div d e
+            mul (exp e q) s ) )
+  | 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
diff --git a/sledge/src/fol.mli b/sledge/src/fol.mli
index fa7e67cdf..160bbd425 100644
--- a/sledge/src/fol.mli
+++ b/sledge/src/fol.mli
@@ -5,26 +5,10 @@
  * LICENSE file in the root directory of this source tree.
  *)
 
-(** Variables *)
-module Var : sig
-  include Ses.Var_intf.VAR
-
-  module Subst : sig
-    type var := t
-    type t [@@deriving compare, equal, sexp]
-    type x = {sub: t; dom: Set.t; rng: Set.t}
+open Ses
 
-    val pp : t pp
-    val empty : t
-    val freshen : Set.t -> wrt:Set.t -> x * Set.t
-    val invert : t -> t
-    val restrict : t -> Set.t -> x
-    val is_empty : t -> bool
-    val domain : t -> Set.t
-    val range : t -> Set.t
-    val fold : t -> init:'a -> f:(var -> var -> 'a -> 'a) -> 'a
-  end
-end
+(** Variables *)
+module Var : Var_intf.VAR
 
 (** Terms *)
 module rec Term : sig
@@ -51,8 +35,10 @@ module rec Term : sig
   val sub : t -> t -> t
   val mulq : Q.t -> t -> t
   val mul : t -> t -> t
+  val div : t -> t -> t
+  val pow : t -> int -> t
 
-  (* sequences (of non-fixed size) *)
+  (* sequences (of flexible size) *)
   val splat : t -> t
   val sized : seq:t -> siz:t -> t
   val extract : seq:t -> off:t -> len:t -> t
@@ -65,7 +51,7 @@ module rec Term : sig
   val ancestor : int -> t
 
   (* uninterpreted *)
-  val apply : Ses.Funsym.t -> t array -> t
+  val apply : Funsym.t -> t array -> t
 
   (* if-then-else *)
   val ite : cnd:Formula.t -> thn:t -> els:t -> t
@@ -130,8 +116,8 @@ and Formula : sig
   val le : Term.t -> Term.t -> t
 
   (* uninterpreted *)
-  val uposlit : Ses.Predsym.t -> Term.t array -> t
-  val uneglit : Ses.Predsym.t -> Term.t array -> t
+  val uposlit : Predsym.t -> Term.t array -> t
+  val uneglit : Predsym.t -> Term.t array -> t
 
   (* connectives *)
   val not_ : t -> t
diff --git a/sledge/src/llair_to_Fol.ml b/sledge/src/llair_to_Fol.ml
index 92488c099..b70f8a933 100644
--- a/sledge/src/llair_to_Fol.ml
+++ b/sledge/src/llair_to_Fol.ml
@@ -111,9 +111,9 @@ and term : Llair.Exp.t -> T.t =
   | Ap2 (Add, _, d, e) -> ap_ttt T.add d e
   | Ap2 (Sub, _, d, e) -> ap_ttt T.sub d e
   | Ap2 (Mul, _, d, e) -> ap_ttt T.mul d e
-  | Ap2 (Div, _, d, e) -> ap_ttt (uap2 Div) d e
+  | Ap2 (Div, _, d, e) -> ap_ttt T.div d e
   | Ap2 (Rem, _, d, e) -> ap_ttt (uap2 Rem) d e
-  | Ap2 (Udiv, typ, d, e) -> ap_uut (uap2 Div) typ d e
+  | Ap2 (Udiv, typ, d, e) -> ap_uut T.div typ d e
   | Ap2 (Urem, typ, d, e) -> ap_uut (uap2 Rem) typ d e
   | Ap2 (And, _, d, e) -> ap_ttt (uap2 BitAnd) d e
   | Ap2 (Or, _, d, e) -> ap_ttt (uap2 BitOr) d e
diff --git a/sledge/src/ses/funsym.ml b/sledge/src/ses/funsym.ml
index 295f82a3c..2d4401b7f 100644
--- a/sledge/src/ses/funsym.ml
+++ b/sledge/src/ses/funsym.ml
@@ -8,8 +8,6 @@
 (** Function Symbols *)
 
 type t =
-  | Mul
-  | Div
   | Rem
   | BitAnd
   | BitOr
@@ -25,8 +23,6 @@ type t =
 let pp ppf f =
   let pf fmt = Format.fprintf ppf fmt in
   match f with
-  | Mul -> pf "@<1>×"
-  | Div -> pf "/"
   | Rem -> pf "%%"
   | BitAnd -> pf "&&"
   | BitOr -> pf "||"
diff --git a/sledge/src/ses/funsym.mli b/sledge/src/ses/funsym.mli
index c65e06187..d5ffc9b88 100644
--- a/sledge/src/ses/funsym.mli
+++ b/sledge/src/ses/funsym.mli
@@ -12,8 +12,6 @@
     applied to literal values of the expected sorts are reduced to literal
     values. *)
 type t =
-  | Mul  (** Multiplication *)
-  | 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|] *)
diff --git a/sledge/src/ses/term.ml b/sledge/src/ses/term.ml
index 289a32562..903ca9756 100644
--- a/sledge/src/ses/term.ml
+++ b/sledge/src/ses/term.ml
@@ -380,7 +380,7 @@ module Sum = struct
   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:(fun _ -> Q.mul const) sum
+    else Qset.map_counts ~f:(Q.mul const) sum
 
   let to_term sum =
     match Qset.classify sum with
diff --git a/sledge/src/test/fol_test.ml b/sledge/src/test/fol_test.ml
index c359a3f93..b2ebeaf3e 100644
--- a/sledge/src/test/fol_test.ml
+++ b/sledge/src/test/fol_test.ml
@@ -189,8 +189,8 @@ let%test_module _ =
       pp_raw r3 ;
       [%expect
         {|
-        (%z_7 × (%y_6 × %y_6)) = %t_1
-      ∧ %z_7 = %u_2 = %v_3 = %w_4 = %x_5 = (%z_7 × %y_6)
+        (1 × (%z_7 × %y_6^2)) = %t_1
+      ∧ %z_7 = %u_2 = %v_3 = %w_4 = %x_5 = (1 × (%z_7 × %y_6))
 
       {sat= true;
        rep= [[0 ↦ ];
@@ -216,7 +216,9 @@ let%test_module _ =
       pp_raw r4 ;
       [%expect
         {|
-        (8 + %z_7) = %x_5 ∧ (3 + %z_7) = %w_4 ∧ (-4 + %z_7) = %y_6
+        (1 × (%z_7) + 8) = %x_5
+      ∧ (1 × (%z_7) + 3) = %w_4
+      ∧ (1 × (%z_7) + -4) = %y_6
 
       {sat= true;
        rep= [[0 ↦ ];
@@ -322,7 +324,7 @@ let%test_module _ =
       pp_raw r8 ;
       [%expect
         {|
-        (13 × %z_7) = %x_5 ∧ 14 = %y_6
+        (13 × (%z_7)) = %x_5 ∧ 14 = %y_6
     
       {sat= true;
        rep= [[0 ↦ ]; [-1 ↦ ]; [%z_7 ↦ ]; [%y_6 ↦ 14]; [%x_5 ↦ (13 × %z_7)]]} |}]
@@ -361,11 +363,11 @@ let%test_module _ =
         {sat= true;
          rep= [[0 ↦ ]; [-1 ↦ ]; [%z_7 ↦ ]; [%x_5 ↦ (-16 + %z_7)]]}
 
-        (%z_7 - (%x_5 + 8))
+        (1 × (%z_7) + -1 × (%x_5) + -8)
 
         8
 
-        ((%x_5 + 8) - %z_7)
+        (-1 × (%z_7) + 1 × (%x_5) + 8)
 
         -8 |}]
 
@@ -378,13 +380,13 @@ let%test_module _ =
 
     let%expect_test _ =
       pp r11 ;
-      [%expect {| (-16 + %z_7) = %x_5 |}]
+      [%expect {| (1 × (%z_7) + -16) = %x_5 |}]
 
     let r12 = of_eqs [(!16, z - x); (x + !8 - z, z + !16 + !8 - z)]
 
     let%expect_test _ =
       pp r12 ;
-      [%expect {| (-16 + %z_7) = %x_5 |}]
+      [%expect {| (1 × (%z_7) + -16) = %x_5 |}]
 
     let r13 =
       of_eqs
@@ -486,7 +488,7 @@ let%test_module _ =
                [%y_6 ↦ ];
                [%x_5 ↦ ]]}
 
-          (-1 + %y_6) = %y_6^ ∧ %x_5 = %x_5^ |}]
+          (1 × (%y_6) + -1) = %y_6^ ∧ %x_5 = %x_5^ |}]
 
     let r19 = of_eqs [(x, y + z); (x, !0); (y, !0)]
 
diff --git a/sledge/src/test/sh_test.ml b/sledge/src/test/sh_test.ml
index 392a51b48..d5a9ded64 100644
--- a/sledge/src/test/sh_test.ml
+++ b/sledge/src/test/sh_test.ml
@@ -145,11 +145,11 @@ let%test_module _ =
       pp q' ;
       [%expect
         {|
-        ∃ %x_6 .   (-1 + %y_7) = %y_7^ ∧ %x_6 = %x_6^ ∧ emp
-    
-          ((-1 + %y_7) = %y_7^) ∧ emp
+        ∃ %x_6 .   (1 × (%y_7) + -1) = %y_7^ ∧ %x_6 = %x_6^ ∧ emp
+
+          ((1 × (%y_7) + -1) = %y_7^) ∧ emp
 
-          (-1 + %y_7) = %y_7^ ∧ emp |}]
+          (1 × (%y_7) + -1) = %y_7^ ∧ emp |}]
 
     let%expect_test _ =
       let q =
diff --git a/sledge/src/test/solver_test.ml b/sledge/src/test/solver_test.ml
index 8c096db4e..46b5b9505 100644
--- a/sledge/src/test/solver_test.ml
+++ b/sledge/src/test/solver_test.ml
@@ -197,7 +197,7 @@ let%test_module _ =
             (⟨16,%a_2⟩^⟨16,%a1_11⟩) = %a_1
           ∧ 16 = %m_8 = %n_9
           ∧ %a_2 = %a0_10
-          ∧ (16 + %k_5) -[ %k_5, 16 )-> ⟨16,%a1_11⟩ |}]
+          ∧ (1 × (%k_5) + 16) -[ %k_5, 16 )-> ⟨16,%a1_11⟩ |}]
 
     let%expect_test _ =
       infer_frame
@@ -219,7 +219,7 @@ let%test_module _ =
             (⟨16,%a_2⟩^⟨16,%a1_11⟩) = %a_1
           ∧ 16 = %m_8 = %n_9
           ∧ %a_2 = %a0_10
-          ∧ (16 + %k_5) -[ %k_5, 16 )-> ⟨16,%a1_11⟩ |}]
+          ∧ (1 × (%k_5) + 16) -[ %k_5, 16 )-> ⟨16,%a1_11⟩ |}]
 
     let seg_split_symbolically =
       Sh.star
@@ -238,7 +238,7 @@ let%test_module _ =
         {|
         ( infer_frame:
             %l_6
-              -[ %l_6, 16 )-> ⟨(8 × %n_9),%a_2⟩^⟨(16 + (-8 × %n_9)),%a_3⟩
+              -[ %l_6, 16 )-> ⟨(8 × (%n_9)),%a_2⟩^⟨(-8 × (%n_9) + 16),%a_3⟩
           * ( (  2 = %n_9 ∧ emp)
             ∨ (  0 = %n_9 ∧ emp)
             ∨ (  1 = %n_9 ∧ emp)
@@ -249,7 +249,7 @@ let%test_module _ =
             ( (  16 = %m_8
                ∧ 2 = %n_9
                ∧ %a_1 = %a_2
-               ∧ (16 + %l_6) -[ %l_6, 16 )-> ⟨0,%a_3⟩)
+               ∧ (1 × (%l_6) + 16) -[ %l_6, 16 )-> ⟨0,%a_3⟩)
             ∨ (  (⟨8,%a_2⟩^⟨8,%a_3⟩) = %a_1
                ∧ 16 = %m_8
                ∧ 1 = %n_9
@@ -271,9 +271,9 @@ let%test_module _ =
       [%expect
         {|
         ( infer_frame:
-            (0 ≤ (2 + (-1 × %n_9)))
+            (0 ≤ (-1 × (%n_9) + 2))
           ∧ %l_6
-              -[ %l_6, 16 )-> ⟨(8 × %n_9),%a_2⟩^⟨(16 + (-8 × %n_9)),%a_3⟩
+              -[ %l_6, 16 )-> ⟨(8 × (%n_9)),%a_2⟩^⟨(-8 × (%n_9) + 16),%a_3⟩
           \- ∃ %a_1, %m_8 .
               %l_6 -[ %l_6, %m_8 )-> ⟨%m_8,%a_1⟩
         ) infer_frame: |}]