diff --git a/sledge/src/control.ml b/sledge/src/control.ml
index d7780af7c..0246ab7b9 100644
--- a/sledge/src/control.ml
+++ b/sledge/src/control.ml
@@ -13,7 +13,7 @@ type exec_opts =
   { bound: int
   ; skip_throw: bool
   ; function_summaries: bool
-  ; globals: [`Per_function of Var.Set.t Var.Map.t | `Declared of Var.Set.t]
+  ; globals: [`Per_function of Reg.Set.t Reg.Map.t | `Declared of Reg.Set.t]
   }
 
 module Make (Dom : Domain_sig.Dom) = struct
@@ -31,15 +31,15 @@ module Make (Dom : Domain_sig.Dom) = struct
     val pop_throw :
          t
       -> init:'a
-      -> unwind:(Var.t list -> Var.Set.t -> Dom.from_call -> 'a -> 'a)
+      -> unwind:(Reg.t list -> Reg.Set.t -> Dom.from_call -> 'a -> 'a)
       -> (Dom.from_call * Llair.jump * t * 'a) option
   end = struct
     type t =
       | Return of
           { recursive: bool  (** return from a possibly-recursive call *)
           ; dst: Llair.Jump.t
-          ; params: Var.t list
-          ; locals: Var.Set.t
+          ; params: Reg.t list
+          ; locals: Reg.Set.t
           ; from_call: Dom.from_call
           ; stk: t }
       | Throw of Llair.Jump.t * t
@@ -248,9 +248,9 @@ module Make (Dom : Domain_sig.Dom) = struct
       | None -> [%Trace.info "queue empty"] ; ()
   end
 
-  let used_globals : exec_opts -> Var.var -> Var.Set.t =
+  let used_globals : exec_opts -> Reg.reg -> Reg.Set.t =
    fun opts fn ->
-    [%Trace.call fun {pf} -> pf "%a" Var.pp fn]
+    [%Trace.call fun {pf} -> pf "%a" Reg.pp fn]
     ;
     ( match opts.globals with
     | `Declared set -> set
@@ -261,21 +261,21 @@ module Make (Dom : Domain_sig.Dom) = struct
           fail
             "main analysis reached function %a that was not reached by \
              used-globals pre-analysis "
-            Var.pp fn () ) )
+            Reg.pp fn () ) )
     |>
-    [%Trace.retn fun {pf} r -> pf "%a" Var.Set.pp r]
+    [%Trace.retn fun {pf} r -> pf "%a" Reg.Set.pp r]
 
   let exec_jump stk state block Llair.{dst; retreating} =
     Work.add ~prev:block ~retreating stk state dst
 
-  let summary_table = Hashtbl.create (module Var)
+  let summary_table = Hashtbl.create (module Reg)
 
   let exec_call opts stk state block call globals =
     let Llair.{callee; args; areturn; return; recursive} = call in
     let Llair.{name; params; freturn; locals; entry} = callee in
     [%Trace.call fun {pf} ->
-      pf "%a from %a with state %a" Var.pp name.var Var.pp
-        return.dst.parent.name.var Dom.pp state]
+      pf "%a from %a with state %a" Reg.pp name.reg Reg.pp
+        return.dst.parent.name.reg Dom.pp state]
     ;
     let dnf_states =
       if opts.function_summaries then Dom.dnf state else [state]
@@ -290,7 +290,7 @@ module Make (Dom : Domain_sig.Dom) = struct
           else
             let maybe_summary_post =
               let state = fst (domain_call ~summaries:false state) in
-              Hashtbl.find summary_table name.var
+              Hashtbl.find summary_table name.reg
               >>= List.find_map ~f:(Dom.apply_summary state)
             in
             [%Trace.info
@@ -320,23 +320,23 @@ module Make (Dom : Domain_sig.Dom) = struct
     [%Trace.printf
       "@[<v>%t@]" (fun fs ->
           Hashtbl.iteri summary_table ~f:(fun ~key ~data ->
-              Format.fprintf fs "@[<v>%a:@ @[%a@]@]@ " Var.pp key
+              Format.fprintf fs "@[<v>%a:@ @[%a@]@]@ " Reg.pp key
                 (List.pp "@," Dom.pp_summary)
                 data ) )]
 
   let exec_return ~opts stk pre_state (block : Llair.block) exp =
     let Llair.{name; params; freturn; locals} = block.parent in
     [%Trace.call fun {pf} ->
-      pf "from %a with pre_state %a" Var.pp name.var Dom.pp pre_state]
+      pf "from %a with pre_state %a" Reg.pp name.reg Dom.pp pre_state]
     ;
     let summarize post_state =
       if opts.function_summaries then (
-        let globals = used_globals opts name.var in
+        let globals = used_globals opts name.reg in
         let function_summary, post_state =
           Dom.create_summary ~locals post_state
-            ~formals:(Set.union (Var.Set.of_list params) globals)
+            ~formals:(Set.union (Reg.Set.of_list params) globals)
         in
-        Hashtbl.add_multi summary_table ~key:name.var ~data:function_summary ;
+        Hashtbl.add_multi summary_table ~key:name.reg ~data:function_summary ;
         pp_st () ;
         post_state )
       else post_state
@@ -359,7 +359,7 @@ module Make (Dom : Domain_sig.Dom) = struct
           opts.function_summaries
           && List.exists
                (Config.find_list "entry-points")
-               ~f:(String.equal (Var.name name.var))
+               ~f:(String.equal (Reg.name name.reg))
         then summarize exit_state |> (ignore : Dom.t -> unit) ;
         Work.skip )
     |>
@@ -367,7 +367,7 @@ module Make (Dom : Domain_sig.Dom) = struct
 
   let exec_throw stk pre_state (block : Llair.block) exc =
     let func = block.parent in
-    [%Trace.call fun {pf} -> pf "from %a" Var.pp func.name.var]
+    [%Trace.call fun {pf} -> pf "from %a" Reg.pp func.name.reg]
     ;
     let unwind params scope from_call state =
       Dom.retn params (Some func.fthrow) from_call
@@ -390,7 +390,7 @@ module Make (Dom : Domain_sig.Dom) = struct
          Stack.t
       -> Dom.t
       -> Llair.block
-      -> Var.t option
+      -> Reg.t option
       -> Llair.jump
       -> Work.x =
    fun stk state block areturn return ->
@@ -423,7 +423,7 @@ module Make (Dom : Domain_sig.Dom) = struct
               Dom.exec_assume state
                 (Exp.eq ptr
                    (Exp.label
-                      ~parent:(Var.name jump.dst.parent.name.var)
+                      ~parent:(Reg.name jump.dst.parent.name.reg)
                       ~name:jump.dst.lbl))
             with
             | Some state -> exec_jump stk state block jump |> Work.seq x
@@ -439,7 +439,7 @@ module Make (Dom : Domain_sig.Dom) = struct
             List.fold callees ~init:Work.skip ~f:(fun x callee ->
                 ( match
                     Dom.exec_intrinsic ~skip_throw:opts.skip_throw state
-                      areturn callee.name.var args
+                      areturn callee.name.reg args
                   with
                 | Some (Error ()) ->
                     Report.invalid_access_term
@@ -452,7 +452,7 @@ module Make (Dom : Domain_sig.Dom) = struct
                     exec_skip_func stk state block areturn return
                 | None ->
                     exec_call opts stk state block {call with callee}
-                      (used_globals opts callee.name.var) )
+                      (used_globals opts callee.name.reg) )
                 |> Work.seq x ) )
     | Return {exp} -> exec_return ~opts stk state block exp
     | Throw {exc} ->
@@ -481,12 +481,12 @@ module Make (Dom : Domain_sig.Dom) = struct
     let entry_points = Config.find_list "entry-points" in
     List.find_map ~f:(Llair.Func.find pgm.functions) entry_points
     |> function
-    | Some {name= {var}; locals; params= []; entry} ->
+    | Some {name= {reg}; locals; params= []; entry} ->
         Some
           (Work.init
              (fst
                 (Dom.call ~summaries:opts.function_summaries
-                   ~globals:(used_globals opts var) [] None [] ~locals
+                   ~globals:(used_globals opts reg) [] None [] ~locals
                    (Dom.init pgm.globals)))
              entry)
     | _ -> None
@@ -501,9 +501,9 @@ module Make (Dom : Domain_sig.Dom) = struct
     |>
     [%Trace.retn fun {pf} _ -> pf ""]
 
-  let compute_summaries opts pgm : Dom.summary list Var.Map.t =
+  let compute_summaries opts pgm : Dom.summary list Reg.Map.t =
     assert opts.function_summaries ;
     exec_pgm opts pgm ;
-    Hashtbl.fold summary_table ~init:Var.Map.empty ~f:(fun ~key ~data map ->
+    Hashtbl.fold summary_table ~init:Reg.Map.empty ~f:(fun ~key ~data map ->
         match data with [] -> map | _ -> Map.set map ~key ~data )
 end
diff --git a/sledge/src/control.mli b/sledge/src/control.mli
index f7e1543bc..802c5fbce 100644
--- a/sledge/src/control.mli
+++ b/sledge/src/control.mli
@@ -11,11 +11,11 @@ type exec_opts =
   { bound: int  (** Loop/recursion unrolling bound *)
   ; skip_throw: bool  (** Treat throw as unreachable *)
   ; function_summaries: bool  (** Use function summarisation *)
-  ; globals: [`Per_function of Var.Set.t Var.Map.t | `Declared of Var.Set.t]
+  ; globals: [`Per_function of Reg.Set.t Reg.Map.t | `Declared of Reg.Set.t]
         (** Either a per-function used-globals map or a program-wide set *)
   }
 
 module Make (Dom : Domain_sig.Dom) : sig
   val exec_pgm : exec_opts -> Llair.t -> unit
-  val compute_summaries : exec_opts -> Llair.t -> Dom.summary list Var.Map.t
+  val compute_summaries : exec_opts -> Llair.t -> Dom.summary list Reg.Map.t
 end
diff --git a/sledge/src/domain/domain_sig.ml b/sledge/src/domain/domain_sig.ml
index 26b2d169c..428767610 100644
--- a/sledge/src/domain/domain_sig.ml
+++ b/sledge/src/domain/domain_sig.ml
@@ -15,15 +15,15 @@ module type Dom = sig
   val join : t -> t -> t option
   val is_false : t -> bool
   val exec_assume : t -> Exp.t -> t option
-  val exec_kill : t -> Var.t -> t
-  val exec_move : t -> Var.t -> Exp.t -> t
+  val exec_kill : t -> Reg.t -> t
+  val exec_move : t -> Reg.t -> Exp.t -> t
   val exec_inst : t -> Llair.inst -> (t, unit) result
 
   val exec_intrinsic :
        skip_throw:bool
     -> t
-    -> Var.t option
-    -> Var.t
+    -> Reg.t option
+    -> Reg.t
     -> Exp.t list
     -> (t, unit) result option
 
@@ -31,17 +31,17 @@ module type Dom = sig
 
   val call :
        summaries:bool
-    -> globals:Var.Set.t
+    -> globals:Reg.Set.t
     -> Exp.t list
-    -> Var.t option
-    -> Var.t list
-    -> locals:Var.Set.t
+    -> Reg.t option
+    -> Reg.t list
+    -> locals:Reg.Set.t
     -> t
     -> t * from_call
 
   val recursion_beyond_bound : [`skip | `prune]
-  val post : Var.Set.t -> from_call -> t -> t
-  val retn : Var.t list -> Var.t option -> from_call -> t -> t
+  val post : Reg.Set.t -> from_call -> t -> t
+  val retn : Reg.t list -> Reg.t option -> from_call -> t -> t
   val dnf : t -> t list
 
   val resolve_callee :
@@ -52,7 +52,7 @@ module type Dom = sig
   val pp_summary : summary pp
 
   val create_summary :
-    locals:Var.Set.t -> formals:Var.Set.t -> t -> summary * t
+    locals:Reg.Set.t -> formals:Reg.Set.t -> t -> summary * t
 
   val apply_summary : t -> summary -> t option
 end
diff --git a/sledge/src/domain/relation.ml b/sledge/src/domain/relation.ml
index a1fb3f4cc..990fa66ea 100644
--- a/sledge/src/domain/relation.ml
+++ b/sledge/src/domain/relation.ml
@@ -12,8 +12,8 @@ module type State_domain_sig = sig
   include Domain_sig.Dom
 
   val create_summary :
-       locals:Var.Set.t
-    -> formals:Var.Set.t
+       locals:Reg.Set.t
+    -> formals:Reg.Set.t
     -> entry:t
     -> current:t
     -> summary * t
@@ -77,8 +77,8 @@ module Make (State_domain : State_domain_sig) = struct
       pf
         "@[<v>@[actuals: (@[%a@])@ formals: (@[%a@])@]@ locals: {@[%a@]}@ \
          globals: {@[%a@]}@ current: %a@]"
-        (List.pp ",@ " Exp.pp) (List.rev actuals) (List.pp ",@ " Var.pp)
-        (List.rev formals) Var.Set.pp locals Var.Set.pp globals
+        (List.pp ",@ " Exp.pp) (List.rev actuals) (List.pp ",@ " Reg.pp)
+        (List.rev formals) Reg.Set.pp locals Reg.Set.pp globals
         State_domain.pp current]
     ;
     let caller_current, state_from_call =
@@ -91,7 +91,7 @@ module Make (State_domain : State_domain_sig) = struct
     [%Trace.retn fun {pf} (reln, _) -> pf "@,%a" pp reln]
 
   let post locals {state_from_call; caller_entry} (_, current) =
-    [%Trace.call fun {pf} -> pf "locals: %a" Var.Set.pp locals]
+    [%Trace.call fun {pf} -> pf "locals: %a" Reg.Set.pp locals]
     ;
     (caller_entry, State_domain.post locals state_from_call current)
     |>
diff --git a/sledge/src/domain/relation.mli b/sledge/src/domain/relation.mli
index 0e28b3f15..6ef12d598 100644
--- a/sledge/src/domain/relation.mli
+++ b/sledge/src/domain/relation.mli
@@ -12,8 +12,8 @@ module type State_domain_sig = sig
   include Domain_sig.Dom
 
   val create_summary :
-       locals:Var.Set.t
-    -> formals:Var.Set.t
+       locals:Reg.Set.t
+    -> formals:Reg.Set.t
     -> entry:t
     -> current:t
     -> summary * t
diff --git a/sledge/src/domain/unit.ml b/sledge/src/domain/unit.ml
index 8b628f1cf..5978bcc15 100644
--- a/sledge/src/domain/unit.ml
+++ b/sledge/src/domain/unit.ml
@@ -29,8 +29,8 @@ let retn _ _ _ _ = ()
 let dnf () = [()]
 
 let resolve_callee lookup ptr _ =
-  match Var.of_exp ptr with
-  | Some callee -> (lookup (Var.name callee), ())
+  match Reg.of_exp ptr with
+  | Some callee -> (lookup (Reg.name callee), ())
   | None -> ([], ())
 
 type summary = unit
diff --git a/sledge/src/domain/used_globals.ml b/sledge/src/domain/used_globals.ml
index e91e39248..479733b09 100644
--- a/sledge/src/domain/used_globals.ml
+++ b/sledge/src/domain/used_globals.ml
@@ -7,11 +7,11 @@
 
 (** Used-globals abstract domain *)
 
-type t = Var.Set.t [@@deriving equal, sexp_of]
+type t = Reg.Set.t [@@deriving equal, sexp_of]
 
-let pp = Set.pp Var.pp
+let pp = Set.pp Reg.pp
 let report_fmt_thunk = Fn.flip pp
-let empty = Var.Set.empty
+let empty = Reg.Set.empty
 
 let init globals =
   [%Trace.info
@@ -24,10 +24,10 @@ let is_false _ = false
 let post _ _ state = state
 let retn _ _ from_call post = Set.union from_call post
 let dnf t = [t]
-let add_if_global gs v = if Var.global v then Set.add gs v else gs
+let add_if_global gs v = if Reg.global v then Set.add gs v else gs
 
 let used_globals ?(init = empty) exp =
-  Exp.fold_vars exp ~init ~f:add_if_global
+  Exp.fold_regs exp ~init ~f:add_if_global
 
 let exec_assume st exp = Some (used_globals ~init:st exp)
 let exec_kill st _ = st
@@ -44,7 +44,7 @@ let exec_inst st inst =
     Result.iter ~f:(fun uses -> pf "post:{%a}" pp uses)]
 
 let exec_intrinsic ~skip_throw:_ st _ intrinsic actuals =
-  let name = Var.name intrinsic in
+  let name = Reg.name intrinsic in
   if
     List.exists
       [ "malloc"; "aligned_alloc"; "calloc"; "posix_memalign"; "realloc"
@@ -66,11 +66,11 @@ let call ~summaries:_ ~globals:_ actuals _ _ ~locals:_ st =
 
 let resolve_callee lookup ptr st =
   let st = used_globals ~init:st ptr in
-  match Var.of_exp ptr with
-  | Some callee -> (lookup (Var.name callee), st)
+  match Reg.of_exp ptr with
+  | Some callee -> (lookup (Reg.name callee), st)
   | None -> ([], st)
 
-(* A function summary is the set of global variables accessed by that
+(* A function summary is the set of global registers accessed by that
    function and its transitive callees *)
 type summary = t
 
diff --git a/sledge/src/domain/used_globals.mli b/sledge/src/domain/used_globals.mli
index c20d91544..ee281a6dc 100644
--- a/sledge/src/domain/used_globals.mli
+++ b/sledge/src/domain/used_globals.mli
@@ -7,4 +7,4 @@
 
 (** Used-globals abstract domain *)
 
-include Domain_sig.Dom with type summary = Var.Set.t
+include Domain_sig.Dom with type summary = Reg.Set.t
diff --git a/sledge/src/llair/exp.ml b/sledge/src/llair/exp.ml
index 51643fe88..3704cd674 100644
--- a/sledge/src/llair/exp.ml
+++ b/sledge/src/llair/exp.ml
@@ -58,7 +58,7 @@ module rec T : sig
     | Memory of {siz: t; arr: t}
     | Concat of {args: t vector}
     (* nullary *)
-    | Var of {id: int; name: string; global: bool}
+    | Reg of {id: int; name: string; global: bool}
     | Nondet of {msg: string}
     | Label of {parent: string; name: string}
     (* curried application *)
@@ -123,7 +123,7 @@ and T0 : sig
     | Splat of {byt: t; siz: t}
     | Memory of {siz: t; arr: t}
     | Concat of {args: t vector}
-    | Var of {id: int; name: string; global: bool}
+    | Reg of {id: int; name: string; global: bool}
     | Nondet of {msg: string}
     | Label of {parent: string; name: string}
     | App of {op: t; arg: t}
@@ -167,7 +167,7 @@ end = struct
     | Splat of {byt: t; siz: t}
     | Memory of {siz: t; arr: t}
     | Concat of {args: t vector}
-    | Var of {id: int; name: string; global: bool}
+    | Reg of {id: int; name: string; global: bool}
     | Nondet of {msg: string}
     | Label of {parent: string; name: string}
     | App of {op: t; arg: t}
@@ -236,10 +236,10 @@ let uncurry =
   uncurry_ []
 
 let rec pp ?is_x fs exp =
-  let get_var_style var =
+  let get_reg_style reg =
     match is_x with
     | None -> `None
-    | Some is_x -> if not (is_x var) then `Bold else `Cyan
+    | Some is_x -> if not (is_x reg) then `Bold else `Cyan
   in
   let pp_ pp fs exp =
     let pf fmt =
@@ -247,12 +247,12 @@ let rec pp ?is_x fs exp =
       Format.kfprintf (fun fs -> Format.pp_close_box fs ()) fs fmt
     in
     match exp with
-    | Var {name; id= 0; global= true} as var ->
-        Trace.pp_styled (get_var_style var) "%@%s" fs name
-    | Var {name; id= 0; global= false} as var ->
-        Trace.pp_styled (get_var_style var) "%%%s" fs name
-    | Var {name; id; _} as var ->
-        Trace.pp_styled (get_var_style var) "%%%s_%d" fs name id
+    | Reg {name; id= 0; global= true} as reg ->
+        Trace.pp_styled (get_reg_style reg) "%@%s" fs name
+    | Reg {name; id= 0; global= false} as reg ->
+        Trace.pp_styled (get_reg_style reg) "%%%s" fs name
+    | Reg {name; id; _} as reg ->
+        Trace.pp_styled (get_reg_style reg) "%%%s_%d" fs name id
     | Nondet {msg} -> pf "nondet \"%s\"" msg
     | Label {name} -> pf "%s" name
     | Integer {data; typ= Pointer _} when Z.equal Z.zero data -> pf "null"
@@ -455,7 +455,7 @@ let invariant ?(partial = false) e =
         assert_arity 0 ;
         assert (Z.numbits data <= bits) )
   | Integer _ -> assert false
-  | Var {id; global; _} ->
+  | Reg {id; global; _} ->
       assert_arity 0 ;
       assert ((not global) || id = 0)
   | Nondet _ | Label _ | Float _ -> assert_arity 0
@@ -500,13 +500,13 @@ let bits_of_int exp =
     | None -> violates invariant exp )
   | _ -> fail "bits_of_int" ()
 
-(** Variables are the expressions constructed by [Var] *)
-module Var = struct
+(** Registers are the expressions constructed by [Reg] *)
+module Reg = struct
   include T
 
   let pp = pp
 
-  type var = t
+  type reg = t
 
   module Set = struct
     include (
@@ -553,7 +553,7 @@ module Var = struct
       if !@status = 0 then demangled else None
 
   let pp_demangled fs = function
-    | Var {name} -> (
+    | Reg {name} -> (
       match demangle name with
       | Some demangled when not (String.equal name demangled) ->
           Format.fprintf fs "“%s”" demangled
@@ -562,25 +562,25 @@ module Var = struct
 
   let invariant x =
     Invariant.invariant [%here] x [%sexp_of: t]
-    @@ fun () -> match x with Var _ -> invariant x | _ -> assert false
+    @@ fun () -> match x with Reg _ -> invariant x | _ -> assert false
 
-  let id = function Var {id} -> id | x -> violates invariant x
-  let name = function Var {name} -> name | x -> violates invariant x
-  let global = function Var {global} -> global | x -> violates invariant x
+  let id = function Reg {id} -> id | x -> violates invariant x
+  let name = function Reg {name} -> name | x -> violates invariant x
+  let global = function Reg {global} -> global | x -> violates invariant x
 
   let of_exp = function
-    | Var _ as v -> Some (v |> check invariant)
+    | Reg _ as x -> Some (x |> check invariant)
     | _ -> None
 
   let program ?global name =
-    Var {id= 0; name; global= Option.is_some global} |> check invariant
+    Reg {id= 0; name; global= Option.is_some global} |> check invariant
 
   let fresh name ~(wrt : Set.t) =
     let max = match Set.max_elt wrt with None -> 0 | Some max -> id max in
-    let x' = Var {name; id= max + 1; global= false} in
+    let x' = Reg {name; id= max + 1; global= false} in
     (x', Set.add wrt x')
 
-  (** Variable renaming substitutions *)
+  (** Register renaming substitutions *)
   module Subst = struct
     type t = T.t Map.M(T).t [@@deriving compare, equal, sexp]
 
@@ -675,15 +675,15 @@ let fold_exps e ~init ~f =
 
 let iter_exps e ~f = fold_exps e ~init:() ~f:(fun () e -> f e)
 
-let fold_vars e ~init ~f =
+let fold_regs e ~init ~f =
   fold_exps e ~init ~f:(fun z -> function
-    | Var _ as v -> f z (v :> Var.t) | _ -> z )
+    | Reg _ as x -> f z (x :> Reg.t) | _ -> z )
 
-let fv e = fold_vars e ~f:Set.add ~init:Var.Set.empty
+let fv e = fold_regs e ~f:Set.add ~init:Reg.Set.empty
 
 (** Construct *)
 
-let var x = x
+let reg x = x
 let nondet msg = Nondet {msg} |> check invariant
 let label ~parent ~name = Label {parent; name} |> check invariant
 let integer data typ = Integer {data; typ} |> check invariant
@@ -1331,7 +1331,7 @@ let map e ~f =
 let rename sub e =
   let rec rename_ sub e =
     match e with
-    | Var _ -> Var.Subst.apply sub e
+    | Reg _ -> Reg.Subst.apply sub e
     | _ -> map ~f:(rename_ sub) e
   in
   rename_ sub e |> check (invariant ~partial:true)
@@ -1349,7 +1349,7 @@ let is_false = function
 let rec is_constant e =
   let is_constant_bin x y = is_constant x && is_constant y in
   match e with
-  | Var _ | Nondet _ -> false
+  | Reg _ | Nondet _ -> false
   | App {op= x; arg= y} | Splat {byt= x; siz= y} | Memory {siz= x; arr= y}
     ->
       is_constant_bin x y
@@ -1413,4 +1413,4 @@ let solve e f =
   solve_ e f empty_map
   |>
   [%Trace.retn fun {pf} ->
-    function Some s -> pf "%a" Var.Subst.pp s | None -> pf "false"]
+    function Some s -> pf "%a" Reg.Subst.pp s | None -> pf "false"]
diff --git a/sledge/src/llair/exp.mli b/sledge/src/llair/exp.mli
index d65546bce..0acc9a7a1 100644
--- a/sledge/src/llair/exp.mli
+++ b/sledge/src/llair/exp.mli
@@ -27,10 +27,10 @@ and t = private
       (** Iterated concatenation of a single byte *)
   | Memory of {siz: t; arr: t}  (** Size-tagged byte-array *)
   | Concat of {args: t vector}  (** Byte-array concatenation *)
-  | Var of {id: int; name: string; global: bool}
+  | Reg of {id: int; name: string; global: bool}
       (** Local variable / virtual register *)
   | Nondet of {msg: string}
-      (** Anonymous local variable with arbitrary value, representing
+      (** Anonymous register with arbitrary value, representing
           non-deterministic approximation of value described by [msg] *)
   | Label of {parent: string; name: string}
       (** Address of named code block within parent function *)
@@ -81,28 +81,28 @@ val pp_full : ?is_x:(exp -> bool) -> t pp
 val pp : t pp
 val invariant : ?partial:bool -> t -> unit
 
-(** Exp.Var is re-exported as Var *)
-module Var : sig
+(** Exp.Reg is re-exported as Reg *)
+module Reg : sig
   type t = private exp [@@deriving compare, equal, hash, sexp]
-  type var = t
+  type reg = t
 
   include Comparator.S with type t := t
 
   module Set : sig
-    type t = (var, comparator_witness) Set.t
+    type t = (reg, comparator_witness) Set.t
     [@@deriving compare, equal, sexp]
 
     val pp_full : ?is_x:(exp -> bool) -> t pp
     val pp : t pp
     val empty : t
-    val of_option : var option -> t
-    val of_list : var list -> t
+    val of_option : reg option -> t
+    val of_list : reg list -> t
+    val of_vector : reg vector -> t
     val union_list : t list -> t
-    val of_vector : var vector -> t
   end
 
   module Map : sig
-    type 'a t = (var, 'a, comparator_witness) Map.t
+    type 'a t = (reg, 'a, comparator_witness) Map.t
     [@@deriving compare, equal, sexp]
 
     val empty : 'a t
@@ -126,7 +126,7 @@ module Var : sig
     val pp : t pp
     val empty : t
     val freshen : Set.t -> wrt:Set.t -> t
-    val extend : t -> replace:var -> with_:var -> t
+    val extend : t -> replace:reg -> with_:reg -> t
     val invert : t -> t
     val exclude : t -> Set.t -> t
     val restrict : t -> Set.t -> t
@@ -140,7 +140,7 @@ end
 
 (** Construct *)
 
-val var : Var.t -> t
+val reg : Reg.t -> t
 val nondet : string -> t
 val label : parent:string -> name:string -> t
 val null : t
@@ -200,18 +200,18 @@ val size_of : Typ.t -> t option
 (** Access *)
 
 val iter : t -> f:(t -> unit) -> unit
-val fold_vars : t -> init:'a -> f:('a -> Var.t -> 'a) -> 'a
+val fold_regs : t -> init:'a -> f:('a -> Reg.t -> 'a) -> 'a
 val fold_exps : t -> init:'a -> f:('a -> t -> 'a) -> 'a
 val fold : t -> init:'a -> f:(t -> 'a -> 'a) -> 'a
 
 (** Transform *)
 
 val map : t -> f:(t -> t) -> t
-val rename : Var.Subst.t -> t -> t
+val rename : Reg.Subst.t -> t -> t
 
 (** Query *)
 
-val fv : t -> Var.Set.t
+val fv : t -> Reg.Set.t
 val is_true : t -> bool
 val is_false : t -> bool
 val typ : t -> Typ.t option
diff --git a/sledge/src/llair/frontend.ml b/sledge/src/llair/frontend.ml
index a7fb3d175..4d21eb448 100644
--- a/sledge/src/llair/frontend.ml
+++ b/sledge/src/llair/frontend.ml
@@ -288,9 +288,10 @@ let xlate_float : Llvm.llvalue -> Exp.t =
   let data = suffix_after_last_space (Llvm.string_of_llvalue llv) in
   Exp.float data
 
-let xlate_name ?global llv = Var.program ?global (find_name llv)
+let xlate_name ?global : Llvm.llvalue -> Reg.t =
+ fun llv -> Reg.program ?global (find_name llv)
 
-let xlate_name_opt : Llvm.llvalue -> Var.t option =
+let xlate_name_opt : Llvm.llvalue -> Reg.t option =
  fun instr ->
   match Llvm.classify_type (Llvm.type_of instr) with
   | Void -> None
@@ -357,11 +358,11 @@ and xlate_value ?(inline = false) : x -> Llvm.llvalue -> Exp.t =
         let fname = Llvm.value_name func in
         match xlate_intrinsic_exp fname with
         | Some intrinsic when inline || should_inline llv -> intrinsic x llv
-        | _ -> Exp.var (xlate_name llv) )
+        | _ -> Exp.reg (xlate_name llv) )
     | Instruction (Invoke | Alloca | Load | PHI | LandingPad | VAArg)
      |Argument ->
-        Exp.var (xlate_name llv)
-    | Function | GlobalVariable -> Exp.var (xlate_global x llv).var
+        Exp.reg (xlate_name llv)
+    | Function | GlobalVariable -> Exp.reg (xlate_global x llv).reg
     | GlobalAlias -> xlate_value x (Llvm.operand llv 0)
     | ConstantInt -> xlate_int x llv
     | ConstantFP -> xlate_float llv
@@ -407,7 +408,7 @@ and xlate_value ?(inline = false) : x -> Llvm.llvalue -> Exp.t =
           | Select | GetElementPtr | ExtractElement | InsertElement
           | ShuffleVector | ExtractValue | InsertValue ) as opcode ) ->
         if inline || should_inline llv then xlate_opcode x llv opcode
-        else Exp.var (xlate_name llv)
+        else Exp.reg (xlate_name llv)
     | ConstantExpr -> xlate_opcode x llv (Llvm.constexpr_opcode llv)
     | GlobalIFunc -> todo "ifuncs: %a" pp_llvalue llv ()
     | Instruction (CatchPad | CleanupPad | CatchSwitch) ->
@@ -630,15 +631,15 @@ type pop_thunk = Loc.t -> Llair.inst list
 let pop_stack_frame_of_function :
     Llvm.llvalue -> Llvm.llbasicblock -> pop_thunk =
  fun func entry_blk ->
-  let append_stack_vars blk vars =
+  let append_stack_regs blk regs =
     Llvm.fold_right_instrs
-      (fun instr vars ->
+      (fun instr regs ->
         match Llvm.instr_opcode instr with
-        | Alloca -> xlate_name instr :: vars
-        | _ -> vars )
-      blk vars
+        | Alloca -> xlate_name instr :: regs
+        | _ -> regs )
+      blk regs
   in
-  let entry_vars = append_stack_vars entry_blk [] in
+  let entry_regs = append_stack_regs entry_blk [] in
   Llvm.iter_blocks
     (fun blk ->
       if not (Poly.equal entry_blk blk) then
@@ -652,8 +653,8 @@ let pop_stack_frame_of_function :
           blk )
     func ;
   let pop retn_loc =
-    List.map entry_vars ~f:(fun var ->
-        Llair.Inst.free ~ptr:(Exp.var var) ~loc:retn_loc )
+    List.map entry_regs ~f:(fun reg ->
+        Llair.Inst.free ~ptr:(Exp.reg reg) ~loc:retn_loc )
   in
   pop
 
@@ -690,7 +691,7 @@ let landingpad_typs : x -> Llvm.llvalue -> Typ.t * Typ.t * Llvm.lltype =
     the PHIs of [dst] translated to a move. *)
 let xlate_jump :
        x
-    -> ?reg_exps:(Var.var * Exp.t) list
+    -> ?reg_exps:(Reg.reg * Exp.t) list
     -> Llvm.llvalue
     -> Llvm.llbasicblock
     -> Loc.t
@@ -753,7 +754,7 @@ let pp_code fs (insts, term, blocks) =
 
 let rec xlate_func_name x llv =
   match Llvm.classify_value llv with
-  | Function -> Exp.var (xlate_name ~global:() llv)
+  | Function -> Exp.reg (xlate_name ~global:() llv)
   | ConstantExpr -> xlate_opcode x llv (Llvm.constexpr_opcode llv)
   | Argument | Instruction _ -> xlate_value x llv
   | GlobalAlias -> xlate_func_name x (Llvm.operand llv 0)
@@ -1076,8 +1077,8 @@ let xlate_instr :
          passing a value for the selector which the handler code tests to
          e.g. either cleanup or rethrow. *)
       let i32, tip, cxa_exception = landingpad_typs x instr in
-      let exc = Exp.var (Var.program (find_name instr ^ ".exc")) in
-      let ti = Var.program (name ^ ".ti") in
+      let exc = Exp.reg (Reg.program (find_name instr ^ ".exc")) in
+      let ti = Reg.program (name ^ ".ti") in
       (* std::type_info* ti = ((__cxa_exception* )exc - 1)->exceptionType *)
       let load_ti =
         let typ = cxa_exception in
@@ -1093,7 +1094,7 @@ let xlate_instr :
         let len = Exp.integer (Z.of_int (size_of x typ)) Typ.siz in
         Llair.Inst.load ~reg:ti ~ptr ~len ~loc
       in
-      let ti = Exp.var ti in
+      let ti = Exp.reg ti in
       let typeid = xlate_llvm_eh_typeid_for x tip ti in
       let lbl = name ^ ".unwind" in
       let param = xlate_name instr in
@@ -1245,10 +1246,10 @@ let xlate_function : x -> Llvm.llvalue -> Llair.func =
   let freturn =
     match name.typ with
     | Pointer {elt= Function {return= Some _; _}} ->
-        Some (Var.program "freturn")
+        Some (Reg.program "freturn")
     | _ -> None
   in
-  let fthrow = Var.program "fthrow" in
+  let fthrow = Reg.program "fthrow" in
   ( match Llvm.block_begin llf with
   | Before entry_blk ->
       let pop = pop_stack_frame_of_function llf entry_blk in
diff --git a/sledge/src/llair/global.ml b/sledge/src/llair/global.ml
index 4397be474..634a847c7 100644
--- a/sledge/src/llair/global.ml
+++ b/sledge/src/llair/global.ml
@@ -7,27 +7,27 @@
 
 (** Global variables *)
 
-type t = {var: Var.t; init: (Exp.t * int) option; typ: Typ.t; loc: Loc.t}
+type t = {reg: Reg.t; init: (Exp.t * int) option; typ: Typ.t; loc: Loc.t}
 [@@deriving compare, equal, hash, sexp]
 
-let pp fs {var} =
-  let name = Var.name var in
+let pp fs {reg} =
+  let name = Reg.name reg in
   let pf pp =
     Format.pp_open_box fs 2 ;
     Format.kfprintf (fun fs -> Format.pp_close_box fs ()) fs pp
   in
-  pf "@%s%a" name Var.pp_demangled var
+  pf "@%s%a" name Reg.pp_demangled reg
 
-let pp_defn fs {var; init; typ; loc} =
-  Format.fprintf fs "@[<2>%a %a%a%a@]" Typ.pp typ Var.pp var Loc.pp loc
+let pp_defn fs {reg; init; typ; loc} =
+  Format.fprintf fs "@[<2>%a %a%a%a@]" Typ.pp typ Reg.pp reg Loc.pp loc
     (Option.pp "@ = @[%a@]" (fun fs (init, _) -> Exp.pp fs init))
     init
 
 let invariant g =
   Invariant.invariant [%here] g [%sexp_of: t]
   @@ fun () ->
-  let {var; typ} = g in
+  let {reg; typ} = g in
   assert (Typ.is_sized typ) ;
-  assert (Var.global var)
+  assert (Reg.global reg)
 
-let mk ?init var typ loc = {var; init; typ; loc} |> check invariant
+let mk ?init reg typ loc = {reg; init; typ; loc} |> check invariant
diff --git a/sledge/src/llair/global.mli b/sledge/src/llair/global.mli
index a545f6eb3..0d22cfc88 100644
--- a/sledge/src/llair/global.mli
+++ b/sledge/src/llair/global.mli
@@ -8,7 +8,7 @@
 (** Global variables *)
 
 type t = private
-  {var: Var.t; init: (Exp.t * int) option; typ: Typ.t; loc: Loc.t}
+  {reg: Reg.t; init: (Exp.t * int) option; typ: Typ.t; loc: Loc.t}
 [@@deriving compare, equal, hash, sexp]
 
 val pp : t pp
@@ -16,4 +16,4 @@ val pp_defn : t pp
 
 include Invariant.S with type t := t
 
-val mk : ?init:Exp.t * int -> Var.t -> Typ.t -> Loc.t -> t
+val mk : ?init:Exp.t * int -> Reg.t -> Typ.t -> Loc.t -> t
diff --git a/sledge/src/llair/llair.ml b/sledge/src/llair/llair.ml
index cb573ff27..37835a476 100644
--- a/sledge/src/llair/llair.ml
+++ b/sledge/src/llair/llair.ml
@@ -10,15 +10,15 @@
 [@@@warning "+9"]
 
 type inst =
-  | Move of {reg_exps: (Var.t * Exp.t) vector; loc: Loc.t}
-  | Load of {reg: Var.t; ptr: Exp.t; len: Exp.t; loc: Loc.t}
+  | Move of {reg_exps: (Reg.t * Exp.t) vector; loc: Loc.t}
+  | Load of {reg: Reg.t; ptr: Exp.t; len: Exp.t; loc: Loc.t}
   | Store of {ptr: Exp.t; exp: Exp.t; len: Exp.t; loc: Loc.t}
   | Memset of {dst: Exp.t; byt: Exp.t; len: Exp.t; loc: Loc.t}
   | Memcpy of {dst: Exp.t; src: Exp.t; len: Exp.t; loc: Loc.t}
   | Memmov of {dst: Exp.t; src: Exp.t; len: Exp.t; loc: Loc.t}
-  | Alloc of {reg: Var.t; num: Exp.t; len: Exp.t; loc: Loc.t}
+  | Alloc of {reg: Reg.t; num: Exp.t; len: Exp.t; loc: Loc.t}
   | Free of {ptr: Exp.t; loc: Loc.t}
-  | Nondet of {reg: Var.t option; msg: string; loc: Loc.t}
+  | Nondet of {reg: Reg.t option; msg: string; loc: Loc.t}
   | Abort of {loc: Loc.t}
 [@@deriving sexp]
 
@@ -31,7 +31,7 @@ and 'a call =
   { callee: 'a
   ; typ: Typ.t
   ; args: Exp.t list
-  ; areturn: Var.t option
+  ; areturn: Reg.t option
   ; return: jump
   ; throw: jump option
   ; mutable recursive: bool
@@ -57,10 +57,10 @@ and cfg = block vector
 (* [entry] is not part of [cfg] since it cannot be jumped to, only called. *)
 and func =
   { name: Global.t
-  ; params: Var.t list
-  ; freturn: Var.t option
-  ; fthrow: Var.t
-  ; locals: Var.Set.t
+  ; params: Reg.t list
+  ; freturn: Reg.t option
+  ; fthrow: Reg.t
+  ; locals: Reg.Set.t
   ; entry: block
   ; cfg: cfg }
 
@@ -87,7 +87,7 @@ let sexp_of_term = function
           { callee: Exp.t
           ; typ: Typ.t
           ; args: Exp.t list
-          ; areturn: Var.t option
+          ; areturn: Reg.t option
           ; return: jump
           ; throw: jump option
           ; recursive: bool
@@ -102,7 +102,7 @@ let sexp_of_block {lbl; cmnd; term; parent; sort_index} =
     { lbl: label
     ; cmnd: cmnd
     ; term: term
-    ; parent: Var.t = parent.name.var
+    ; parent: Reg.t = parent.name.reg
     ; sort_index: int }]
 
 let sexp_of_cfg v = [%sexp_of: block vector] v
@@ -110,10 +110,10 @@ let sexp_of_cfg v = [%sexp_of: block vector] v
 let sexp_of_func {name; params; freturn; fthrow; locals; entry; cfg} =
   [%sexp
     { name: Global.t
-    ; params: Var.t list
-    ; freturn: Var.t option
-    ; fthrow: Var.t
-    ; locals: Var.Set.t
+    ; params: Reg.t list
+    ; freturn: Reg.t option
+    ; fthrow: Reg.t
+    ; locals: Reg.Set.t
     ; entry: block
     ; cfg: cfg }]
 
@@ -131,10 +131,10 @@ let pp_inst fs inst =
   match inst with
   | Move {reg_exps; loc} ->
       let regs, exps = Vector.unzip reg_exps in
-      pf "@[<2>@[%a@]@ := @[%a@];@]\t%a" (Vector.pp ",@ " Var.pp) regs
+      pf "@[<2>@[%a@]@ := @[%a@];@]\t%a" (Vector.pp ",@ " Reg.pp) regs
         (Vector.pp ",@ " Exp.pp) exps Loc.pp loc
   | Load {reg; ptr; len; loc} ->
-      pf "@[<2>%a@ := load %a@ %a;@]\t%a" Var.pp reg Exp.pp len Exp.pp ptr
+      pf "@[<2>%a@ := load %a@ %a;@]\t%a" Reg.pp reg Exp.pp len Exp.pp ptr
         Loc.pp loc
   | Store {ptr; exp; len; loc} ->
       pf "@[<2>store %a@ %a@ %a;@]\t%a" Exp.pp len Exp.pp ptr Exp.pp exp
@@ -149,19 +149,19 @@ let pp_inst fs inst =
       pf "@[<2>memmov %a %a %a;@]\t%a" Exp.pp len Exp.pp dst Exp.pp src
         Loc.pp loc
   | Alloc {reg; num; len; loc} ->
-      pf "@[<2>%a@ := alloc [%a x %a];@]\t%a" Var.pp reg Exp.pp num Exp.pp
+      pf "@[<2>%a@ := alloc [%a x %a];@]\t%a" Reg.pp reg Exp.pp num Exp.pp
         len Loc.pp loc
   | Free {ptr; loc} -> pf "@[<2>free %a;@]\t%a" Exp.pp ptr Loc.pp loc
   | Nondet {reg; msg; loc} ->
       pf "@[<2>%anondet \"%s\";@]\t%a"
-        (Option.pp "%a := " Var.pp)
+        (Option.pp "%a := " Reg.pp)
         reg msg Loc.pp loc
   | Abort {loc} -> pf "@[<2>abort;@]\t%a" Loc.pp loc
 
 let pp_args pp_arg fs args =
   Format.fprintf fs "@ (@[%a@])" (List.pp ",@ " pp_arg) (List.rev args)
 
-let pp_param fs var = Var.pp fs var
+let pp_param fs reg = Reg.pp fs reg
 
 let pp_jump fs {dst; retreating} =
   Format.fprintf fs "@[<2>%s%%%s@]"
@@ -190,7 +190,7 @@ let pp_term fs term =
         tbl Loc.pp loc
   | Call {callee; args; areturn; return; throw; recursive; loc; _} ->
       pf "@[<2>@[<7>%acall @[<2>%s%a%a@]@]@ @[returnto %a%a;@]@]\t%a"
-        (Option.pp "%a := " Var.pp)
+        (Option.pp "%a := " Reg.pp)
         areturn
         (if recursive then "↑" else "")
         Exp.pp callee (pp_args Exp.pp) args pp_jump return
@@ -219,13 +219,13 @@ let rec dummy_block =
   ; sort_index= 0 }
 
 and dummy_func =
-  let dummy_var = Var.program ~global:() "dummy" in
+  let dummy_reg = Reg.program ~global:() "dummy" in
   let dummy_ptr_typ = Typ.pointer ~elt:(Typ.opaque ~name:"dummy") in
-  { name= Global.mk dummy_var dummy_ptr_typ Loc.none
+  { name= Global.mk dummy_reg dummy_ptr_typ Loc.none
   ; params= []
   ; freturn= None
-  ; fthrow= dummy_var
-  ; locals= Var.Set.empty
+  ; fthrow= dummy_reg
+  ; locals= Reg.Set.empty
   ; entry= dummy_block
   ; cfg= Vector.empty }
 
@@ -270,7 +270,7 @@ module Inst = struct
      |Abort _ ->
         vs
 
-  let locals inst = union_locals inst Var.Set.empty
+  let locals inst = union_locals inst Reg.Set.empty
 
   let fold_exps inst ~init ~f =
     match inst with
@@ -408,7 +408,7 @@ module Func = struct
       ( match name.typ with
       | Pointer {elt= Function {return; _}} -> return
       | _ -> None )
-      (Option.pp " %a := " Var.pp)
+      (Option.pp " %a := " Reg.pp)
       freturn Global.pp name (pp_args pp_param) params
       (fun fs ->
         if is_undefined func then Format.fprintf fs " #%i@]" sort_index
@@ -451,7 +451,7 @@ module Func = struct
       let locals_block locals block =
         locals_cmnd (Term.union_locals block.term locals) block.cmnd
       in
-      let init = locals_block Var.Set.empty entry in
+      let init = locals_block Reg.Set.empty entry in
       Vector.fold ~f:locals_block cfg ~init
     in
     let func = {name; params; freturn; fthrow; locals; entry; cfg} in
@@ -509,17 +509,17 @@ module Block_label = struct
 end
 
 module BlockQ = Hash_queue.Make (Block_label)
-module FuncQ = Hash_queue.Make (Var)
+module FuncQ = Hash_queue.Make (Reg)
 
 let set_derived_metadata functions =
   let compute_roots functions =
     let roots = FuncQ.create () in
     Map.iter functions ~f:(fun func ->
-        FuncQ.enqueue_back_exn roots func.name.var func ) ;
+        FuncQ.enqueue_back_exn roots func.name.reg func ) ;
     Map.iter functions ~f:(fun func ->
         Func.fold_term func ~init:() ~f:(fun () -> function
           | Call {callee; _} -> (
-            match Var.of_exp callee with
+            match Reg.of_exp callee with
             | Some callee ->
                 FuncQ.remove roots callee |> (ignore : [> ] -> unit)
             | None -> () )
@@ -543,7 +543,7 @@ let set_derived_metadata functions =
         | Iswitch {tbl; _} -> Vector.iter tbl ~f:jump
         | Call ({callee; return; throw; _} as call) ->
             ( match
-                Var.of_exp callee >>| Var.name >>= Func.find functions
+                Reg.of_exp callee >>| Reg.name >>= Func.find functions
               with
             | Some func ->
                 if Set.mem ancestors func.entry then call.recursive <- true
@@ -575,7 +575,7 @@ let set_derived_metadata functions =
     List.fold functions
       ~init:(Map.empty (module String))
       ~f:(fun m func ->
-        Map.add_exn m ~key:(Var.name func.name.var) ~data:func )
+        Map.add_exn m ~key:(Reg.name func.name.reg) ~data:func )
   in
   let roots = compute_roots functions in
   let tips_to_roots = topsort functions roots in
@@ -589,7 +589,7 @@ let invariant pgm =
   assert (
     not
       (Vector.contains_dup pgm.globals ~compare:(fun g1 g2 ->
-           Var.compare g1.Global.var g2.Global.var )) )
+           Reg.compare g1.Global.reg g2.Global.reg )) )
 
 let mk ~globals ~functions =
   { globals= Vector.of_list_rev globals
diff --git a/sledge/src/llair/llair.mli b/sledge/src/llair/llair.mli
index 1636efd54..430cbe8e5 100644
--- a/sledge/src/llair/llair.mli
+++ b/sledge/src/llair/llair.mli
@@ -10,10 +10,10 @@
 
 (** Instructions for memory manipulation or other non-control effects. *)
 type inst = private
-  | Move of {reg_exps: (Var.t * Exp.t) vector; loc: Loc.t}
+  | Move of {reg_exps: (Reg.t * Exp.t) vector; loc: Loc.t}
       (** Move each value [exp] into corresponding register [reg]. All of
           the moves take effect simultaneously. *)
-  | Load of {reg: Var.t; ptr: Exp.t; len: Exp.t; loc: Loc.t}
+  | Load of {reg: Reg.t; ptr: Exp.t; len: Exp.t; loc: Loc.t}
       (** Read a [len]-byte value from the contents of memory at address
           [ptr] into [reg]. *)
   | Store of {ptr: Exp.t; exp: Exp.t; len: Exp.t; loc: Loc.t}
@@ -25,12 +25,12 @@ type inst = private
           if ranges overlap. *)
   | Memmov of {dst: Exp.t; src: Exp.t; len: Exp.t; loc: Loc.t}
       (** Copy [len] bytes starting from address [src] to [dst]. *)
-  | Alloc of {reg: Var.t; num: Exp.t; len: Exp.t; loc: Loc.t}
+  | Alloc of {reg: Reg.t; num: Exp.t; len: Exp.t; loc: Loc.t}
       (** Allocate a block of memory large enough to store [num] elements of
           [len] bytes each and bind [reg] to the first address. *)
   | Free of {ptr: Exp.t; loc: Loc.t}
       (** Deallocate the previously allocated block at address [ptr]. *)
-  | Nondet of {reg: Var.t option; msg: string; loc: Loc.t}
+  | Nondet of {reg: Reg.t option; msg: string; loc: Loc.t}
       (** Bind [reg] to an arbitrary value, representing non-deterministic
           approximation of behavior described by [msg]. *)
   | Abort of {loc: Loc.t}  (** Trigger abnormal program termination *)
@@ -49,7 +49,7 @@ and 'a call =
   { callee: 'a
   ; typ: Typ.t  (** Type of the callee. *)
   ; args: Exp.t list  (** Stack of arguments, first-arg-last. *)
-  ; areturn: Var.t option  (** Register to receive return value. *)
+  ; areturn: Reg.t option  (** Register to receive return value. *)
   ; return: jump  (** Return destination. *)
   ; throw: jump option  (** Handler destination. *)
   ; mutable recursive: bool
@@ -89,10 +89,10 @@ and cfg
     parameters are the function parameters. *)
 and func = private
   { name: Global.t
-  ; params: Var.t list  (** Formal parameters, first-param-last stack *)
-  ; freturn: Var.t option
-  ; fthrow: Var.t
-  ; locals: Var.Set.t  (** Local variables *)
+  ; params: Reg.t list  (** Formal parameters, first-param-last stack *)
+  ; freturn: Reg.t option
+  ; fthrow: Reg.t
+  ; locals: Reg.Set.t  (** Local registers *)
   ; entry: block
   ; cfg: cfg }
 
@@ -112,18 +112,18 @@ module Inst : sig
   type t = inst
 
   val pp : t pp
-  val move : reg_exps:(Var.t * Exp.t) vector -> loc:Loc.t -> inst
-  val load : reg:Var.t -> ptr:Exp.t -> len:Exp.t -> loc:Loc.t -> inst
+  val move : reg_exps:(Reg.t * Exp.t) vector -> loc:Loc.t -> inst
+  val load : reg:Reg.t -> ptr:Exp.t -> len:Exp.t -> loc:Loc.t -> inst
   val store : ptr:Exp.t -> exp:Exp.t -> len:Exp.t -> loc:Loc.t -> inst
   val memset : dst:Exp.t -> byt:Exp.t -> len:Exp.t -> loc:Loc.t -> inst
   val memcpy : dst:Exp.t -> src:Exp.t -> len:Exp.t -> loc:Loc.t -> inst
   val memmov : dst:Exp.t -> src:Exp.t -> len:Exp.t -> loc:Loc.t -> inst
-  val alloc : reg:Var.t -> num:Exp.t -> len:Exp.t -> loc:Loc.t -> inst
+  val alloc : reg:Reg.t -> num:Exp.t -> len:Exp.t -> loc:Loc.t -> inst
   val free : ptr:Exp.t -> loc:Loc.t -> inst
-  val nondet : reg:Var.t option -> msg:string -> loc:Loc.t -> inst
+  val nondet : reg:Reg.t option -> msg:string -> loc:Loc.t -> inst
   val abort : loc:Loc.t -> inst
   val loc : inst -> Loc.t
-  val locals : inst -> Var.Set.t
+  val locals : inst -> Reg.Set.t
   val fold_exps : inst -> init:'a -> f:('a -> Exp.t -> 'a) -> 'a
 end
 
@@ -154,7 +154,7 @@ module Term : sig
        func:Exp.t
     -> typ:Typ.t
     -> args:Exp.t list
-    -> areturn:Var.t option
+    -> areturn:Reg.t option
     -> return:jump
     -> throw:jump option
     -> loc:Loc.t
@@ -184,18 +184,18 @@ module Func : sig
 
   val mk :
        name:Global.t
-    -> params:Var.t list
-    -> freturn:Var.t option
-    -> fthrow:Var.t
+    -> params:Reg.t list
+    -> freturn:Reg.t option
+    -> fthrow:Reg.t
     -> entry:block
     -> cfg:block vector
     -> func
 
   val mk_undefined :
        name:Global.t
-    -> params:Var.t list
-    -> freturn:Var.t option
-    -> fthrow:Var.t
+    -> params:Reg.t list
+    -> freturn:Reg.t option
+    -> fthrow:Reg.t
     -> t
 
   val find : functions -> string -> func option
diff --git a/sledge/src/llair/reg.ml b/sledge/src/llair/reg.ml
new file mode 100644
index 000000000..bccfa565a
--- /dev/null
+++ b/sledge/src/llair/reg.ml
@@ -0,0 +1,10 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+(** Variables *)
+
+include Exp.Reg
diff --git a/sledge/src/llair/reg.mli b/sledge/src/llair/reg.mli
new file mode 100644
index 000000000..568b21b70
--- /dev/null
+++ b/sledge/src/llair/reg.mli
@@ -0,0 +1,10 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+(** Variables *)
+
+include module type of Exp.Reg
diff --git a/sledge/src/report.ml b/sledge/src/report.ml
index 0e8dde708..ff91c5561 100644
--- a/sledge/src/report.ml
+++ b/sledge/src/report.ml
@@ -16,8 +16,8 @@ let unknown_call call =
       (fun fs (call : Llair.Term.t) ->
         match call with
         | Call {callee} -> (
-          match Var.of_exp callee with
-          | Some var -> Var.pp_demangled fs var
+          match Reg.of_exp callee with
+          | Some reg -> Reg.pp_demangled fs reg
           | None -> Exp.pp fs callee )
         | _ -> () )
       call Llair.Term.pp call]
diff --git a/sledge/src/sledge.ml b/sledge/src/sledge.ml
index a7933e77f..16a3a0935 100644
--- a/sledge/src/sledge.ml
+++ b/sledge/src/sledge.ml
@@ -75,14 +75,14 @@ let used_globals pgm preanalyze =
         { bound= 1
         ; skip_throw= false
         ; function_summaries= true
-        ; globals= `Declared Var.Set.empty }
+        ; globals= `Declared Reg.Set.empty }
         pgm
     in
-    `Per_function (Map.map summary_table ~f:Var.Set.union_list)
+    `Per_function (Map.map summary_table ~f:Reg.Set.union_list)
   else
     `Declared
-      (Vector.fold pgm.globals ~init:Var.Set.empty ~f:(fun acc g ->
-           Set.add acc g.var ))
+      (Vector.fold pgm.globals ~init:Reg.Set.empty ~f:(fun acc g ->
+           Set.add acc g.reg ))
 
 let analyze =
   let%map_open bound =
diff --git a/sledge/src/symbheap/equality.ml b/sledge/src/symbheap/equality.ml
index 1837d9231..9076fe833 100644
--- a/sledge/src/symbheap/equality.ml
+++ b/sledge/src/symbheap/equality.ml
@@ -7,11 +7,11 @@
 
 (** Equality over uninterpreted functions and linear rational arithmetic *)
 
-type 'a exp_map = 'a Map.M(Exp).t [@@deriving compare, equal, sexp]
+type 'a term_map = 'a Map.M(Term).t [@@deriving compare, equal, sexp]
 
-let empty_map = Map.empty (module Exp)
+let empty_map = Map.empty (module Term)
 
-type subst = Exp.t exp_map [@@deriving compare, equal, sexp]
+type subst = Term.t term_map [@@deriving compare, equal, sexp]
 
 (** see also [invariant] *)
 type t =
@@ -24,7 +24,7 @@ type t =
 
 let classes r =
   Map.fold r.rep ~init:empty_map ~f:(fun ~key ~data cls ->
-      if Exp.equal key data then cls
+      if Term.equal key data then cls
       else Map.add_multi cls ~key:data ~data:key )
 
 (** Pretty-printing *)
@@ -36,17 +36,17 @@ let pp fs {sat; rep} =
     in
     Format.fprintf fs "[@[<hv>%a@]]" (List.pp ";@ " pp_assoc) alist
   in
-  let pp_exp_v fs (k, v) = if not (Exp.equal k v) then Exp.pp fs v 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 Exp.pp pp_exp_v)
+    (pp_alist Term.pp pp_term_v)
     (Map.to_alist rep)
 
 let pp_classes ?is_x fs r =
   List.pp "@ @<2>∧ "
     (fun fs (key, data) ->
-      Format.fprintf fs "@[%a@ = %a@]" (Exp.pp_full ?is_x) key
-        (List.pp "@ = " (Exp.pp_full ?is_x))
-        (List.sort ~compare:Exp.compare data) )
+      Format.fprintf fs "@[%a@ = %a@]" (Term.pp_full ?is_x) key
+        (List.pp "@ = " (Term.pp_full ?is_x))
+        (List.sort ~compare:Term.compare data) )
     fs
     (Map.to_alist (classes r))
 
@@ -66,17 +66,17 @@ let pp_diff fs (r, s) =
     | k, `Unequal vv ->
         Format.fprintf fs "[@[%a@ @<2>↦ %a@]]" pp_key k pp_sdiff_val vv
   in
-  let pp_sdiff_exp_map =
-    let pp_sdiff_exp fs (u, v) =
-      Format.fprintf fs "-- %a ++ %a" Exp.pp u Exp.pp v
+  let pp_sdiff_term_map =
+    let pp_sdiff_term fs (u, v) =
+      Format.fprintf fs "-- %a ++ %a" Term.pp u Term.pp v
     in
-    pp_sdiff_map (pp_sdiff_elt Exp.pp Exp.pp pp_sdiff_exp) Exp.equal
+    pp_sdiff_map (pp_sdiff_elt Term.pp Term.pp pp_sdiff_term) Term.equal
   in
   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 = pp_sdiff_exp_map "rep" fs r.rep s.rep in
+  let pp_rep fs = pp_sdiff_term_map "rep" fs r.rep s.rep in
   Format.fprintf fs "@[{@[<hv>%t%t@]}@]" pp_sat pp_rep
 
 (** Invariant *)
@@ -85,68 +85,68 @@ let pp_diff fs (r, s) =
 let in_car r e = Map.mem r.rep e
 
 let rec iter_max_solvables e ~f =
-  match Exp.classify e with
-  | `Interpreted -> Exp.iter ~f:(iter_max_solvables ~f) e
+  match Term.classify e with
+  | `Interpreted -> Term.iter ~f:(iter_max_solvables ~f) e
   | _ -> f e
 
 let invariant r =
   Invariant.invariant [%here] r [%sexp_of: t]
   @@ fun () ->
   Map.iteri r.rep ~f:(fun ~key:a ~data:_ ->
-      (* no interpreted exps in carrier *)
-      assert (Poly.(Exp.classify a <> `Interpreted)) ;
-      (* carrier is closed under sub-expressions *)
+      (* no interpreted terms in carrier *)
+      assert (Poly.(Term.classify a <> `Interpreted)) ;
+      (* carrier is closed under subterms *)
       iter_max_solvables a ~f:(fun b ->
           assert (
             in_car r b
-            || Trace.fail "@[subexp %a of %a not in carrier of@ %a@]" Exp.pp
-                 b Exp.pp a pp r ) ) )
+            || Trace.fail "@[subterm %a of %a not in carrier of@ %a@]"
+                 Term.pp b Term.pp a pp r ) ) )
 
 (** Core operations *)
 
 let true_ = {sat= true; rep= empty_map} |> check invariant
 
-(** apply a subst to an exp *)
+(** apply a subst to a term *)
 let apply s a = try Map.find_exn s a with Caml.Not_found -> a
 
-(** apply a subst to maximal non-interpreted subexps *)
+(** apply a subst to maximal non-interpreted subterms *)
 let rec norm s a =
-  match Exp.classify a with
-  | `Interpreted -> Exp.map ~f:(norm s) a
-  | `Simplified -> apply s (Exp.map ~f:(norm s) a)
+  match Term.classify a with
+  | `Interpreted -> Term.map ~f:(norm s) a
+  | `Simplified -> apply s (Term.map ~f:(norm s) a)
   | `Atomic | `Uninterpreted -> apply s a
 
-(** exps are congruent if equal after normalizing subexps *)
+(** terms are congruent if equal after normalizing subterms *)
 let congruent r a b =
-  Exp.equal (Exp.map ~f:(norm r.rep) a) (Exp.map ~f:(norm r.rep) b)
+  Term.equal (Term.map ~f:(norm r.rep) a) (Term.map ~f:(norm r.rep) b)
 
 (** [lookup r a] is [b'] if [a ~ b = b'] for some equation [b = b'] in rep *)
 let lookup r a =
   With_return.with_return
   @@ fun {return} ->
   (* congruent specialized to assume [a] canonized and [b] non-interpreted *)
-  let semi_congruent r a b = Exp.equal a (Exp.map ~f:(apply r.rep) b) in
+  let semi_congruent r a b = Term.equal a (Term.map ~f:(apply r.rep) b) in
   Map.iteri r.rep ~f:(fun ~key ~data ->
       if semi_congruent r a key then return data ) ;
   a
 
-(** rewrite an exp into canonical form using rep and, for uninterpreted
-    exps, congruence composed with rep *)
+(** rewrite a term into canonical form using rep and, for uninterpreted
+    terms, congruence composed with rep *)
 let rec canon r a =
-  match Exp.classify a with
-  | `Interpreted -> Exp.map ~f:(canon r) a
-  | `Simplified | `Uninterpreted -> lookup r (Exp.map ~f:(canon r) a)
+  match Term.classify a with
+  | `Interpreted -> Term.map ~f:(canon r) a
+  | `Simplified | `Uninterpreted -> lookup r (Term.map ~f:(canon r) a)
   | `Atomic -> apply r.rep a
 
-(** add an exp to the carrier *)
+(** add a term to the carrier *)
 let rec extend a r =
-  match Exp.classify a with
-  | `Interpreted | `Simplified -> Exp.fold ~f:extend a ~init:r
+  match Term.classify a with
+  | `Interpreted | `Simplified -> Term.fold ~f:extend a ~init:r
   | `Uninterpreted ->
       Map.find_or_add r.rep a
         ~if_found:(fun _ -> r)
         ~default:a
-        ~if_added:(fun rep -> Exp.fold ~f:extend a ~init:{r with rep})
+        ~if_added:(fun rep -> Term.fold ~f:extend a ~init:{r with rep})
   | `Atomic -> r
 
 let extend a r = extend a r |> check invariant
@@ -155,15 +155,15 @@ let compose r s =
   let rep = Map.map ~f:(norm s) r.rep in
   let rep =
     Map.merge_skewed rep s ~combine:(fun ~key v1 v2 ->
-        if Exp.equal v1 v2 then v1
-        else fail "domains intersect: %a" Exp.pp key () )
+        if Term.equal v1 v2 then v1
+        else fail "domains intersect: %a" Term.pp key () )
   in
   {r with rep}
 
 let merge a b r =
-  [%Trace.call fun {pf} -> pf "%a@ %a@ %a" Exp.pp a Exp.pp b pp r]
+  [%Trace.call fun {pf} -> pf "%a@ %a@ %a" Term.pp a Term.pp b pp r]
   ;
-  ( match Exp.solve a b with
+  ( match Term.solve a b with
   | Some s -> compose r s
   | None -> {r with sat= false} )
   |>
@@ -171,15 +171,15 @@ let merge a b r =
     pf "%a" pp_diff (r, r') ;
     invariant r']
 
-(** find an unproved equation between congruent exps *)
+(** find an unproved equation between congruent terms *)
 let find_missing r =
   With_return.with_return
   @@ fun {return} ->
   Map.iteri r.rep ~f:(fun ~key:a ~data:a' ->
       Map.iteri r.rep ~f:(fun ~key:b ~data:b' ->
           if
-            Exp.compare a b < 0
-            && (not (Exp.equal a' b'))
+            Term.compare a b < 0
+            && (not (Term.equal a' b'))
             && congruent r a b
           then return (Some (a', b')) ) ) ;
   None
@@ -207,15 +207,15 @@ let and_eq a b r =
     let b' = canon r b in
     let r = extend a' r in
     let r = extend b' r in
-    if Exp.equal a' b' then r else close (merge a' b' r)
+    if Term.equal a' b' then r else close (merge a' b' r)
 
 (** Exposed interface *)
 
 let is_true {sat; rep} =
-  sat && Map.for_alli rep ~f:(fun ~key:a ~data:a' -> Exp.equal a a')
+  sat && Map.for_alli rep ~f:(fun ~key:a ~data:a' -> Term.equal a a')
 
 let is_false {sat} = not sat
-let entails_eq r d e = Exp.equal (canon r d) (canon r e)
+let entails_eq r d e = Term.equal (canon r d) (canon r e)
 
 let entails r s =
   Map.for_alli s.rep ~f:(fun ~key:e ~data:e' -> entails_eq r e e')
@@ -227,15 +227,15 @@ let class_of r e =
   e' :: Map.find_multi (classes r) e'
 
 let difference r a b =
-  [%Trace.call fun {pf} -> pf "%a@ %a@ %a" Exp.pp a Exp.pp b pp r]
+  [%Trace.call fun {pf} -> pf "%a@ %a@ %a" Term.pp a Term.pp b pp r]
   ;
   let a = canon r a in
   let b = canon r b in
-  ( if Exp.equal a b then Some Z.zero
+  ( if Term.equal a b then Some Z.zero
   else
-    match (Exp.typ a, Exp.typ b) with
+    match (Term.typ a, Term.typ b) with
     | Some typ, _ | _, Some typ -> (
-      match normalize r (Exp.sub typ a b) with
+      match normalize r (Term.sub typ a b) with
       | Integer {data} -> Some data
       | _ -> None )
     | _ -> None )
@@ -265,17 +265,17 @@ let or_ r s =
     let rs = merge_mems rs s r in
     rs
 
-(* assumes that f is injective and for any set of exps E, f[E] is disjoint
+(* assumes that f is injective and for any set of terms E, f[E] is disjoint
    from E *)
-let map_exps ({sat= _; rep} as r) ~f =
+let map_terms ({sat= _; rep} as r) ~f =
   [%Trace.call fun {pf} -> pf "%a" pp r]
   ;
   let map m =
     Map.fold m ~init:m ~f:(fun ~key ~data m ->
         let key' = f key in
         let data' = f data in
-        if Exp.equal key' key then
-          if Exp.equal data' data then m else Map.set m ~key ~data:data'
+        if Term.equal key' key then
+          if Term.equal data' data then m else Map.set m ~key ~data:data'
         else Map.remove m key |> Map.add_exn ~key:key' ~data:data' )
   in
   let rep' = map rep in
@@ -285,12 +285,12 @@ let map_exps ({sat= _; rep} as r) ~f =
     pf "%a" pp_diff (r, r') ;
     invariant r']
 
-let rename r sub = map_exps r ~f:(Exp.rename sub)
+let rename r sub = map_terms r ~f:(Term.rename sub)
 
-let fold_exps r ~init ~f =
+let fold_terms r ~init ~f =
   Map.fold r.rep ~f:(fun ~key ~data z -> f (f z data) key) ~init
 
 let fold_vars r ~init ~f =
-  fold_exps r ~init ~f:(fun init -> Exp.fold_vars ~f ~init)
+  fold_terms r ~init ~f:(fun init -> Term.fold_vars ~f ~init)
 
 let fv e = fold_vars e ~f:Set.add ~init:Var.Set.empty
diff --git a/sledge/src/symbheap/equality.mli b/sledge/src/symbheap/equality.mli
index 52d236d72..6dcdf15eb 100644
--- a/sledge/src/symbheap/equality.mli
+++ b/sledge/src/symbheap/equality.mli
@@ -11,14 +11,14 @@
 type t [@@deriving compare, equal, sexp]
 
 val pp : t pp
-val pp_classes : ?is_x:(Exp.t -> bool) -> t pp
+val pp_classes : ?is_x:(Term.t -> bool) -> t pp
 
 include Invariant.S with type t := t
 
 val true_ : t
-(** The diagonal relation, which only equates each exp with itself. *)
+(** The diagonal relation, which only equates each term with itself. *)
 
-val and_eq : Exp.t -> Exp.t -> t -> t
+val and_eq : Term.t -> Term.t -> t -> t
 (** Conjoin an equation to a relation. *)
 
 val and_ : t -> t -> t
@@ -31,7 +31,7 @@ val rename : t -> Var.Subst.t -> t
 (** Apply a renaming substitution to the relation. *)
 
 val fv : t -> Var.Set.t
-(** The variables occurring in the exps of the relation. *)
+(** The variables occurring in the terms of the relation. *)
 
 val is_true : t -> bool
 (** Test if the relation is diagonal. *)
@@ -39,24 +39,24 @@ val is_true : t -> bool
 val is_false : t -> bool
 (** Test if the relation is empty / inconsistent. *)
 
-val entails_eq : t -> Exp.t -> Exp.t -> bool
+val entails_eq : t -> Term.t -> Term.t -> bool
 (** Test if an equation is entailed by a relation. *)
 
 val entails : t -> t -> bool
 (** Test if one relation entails another. *)
 
-val class_of : t -> Exp.t -> Exp.t list
-(** Equivalence class of [e]: all the expressions in [f] in the relation
-    such that [e = f] is implied by the 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 -> Exp.t -> Exp.t
-(** Normalize an exp [e] to [e'] such that [e = e'] is implied by the
-    relation, where [e'] and its sub-exps are expressed in terms of the
+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 difference : t -> Exp.t -> Exp.t -> Z.t option
+val difference : t -> Term.t -> Term.t -> Z.t option
 (** The difference as an offset. [difference r a b = Some k] if [r] implies
     [a = b+k], or [None] if [a] and [b] are not equal up to an integer
     offset. *)
 
-val fold_exps : t -> init:'a -> f:('a -> Exp.t -> 'a) -> 'a
+val fold_terms : t -> init:'a -> f:('a -> Term.t -> 'a) -> 'a
diff --git a/sledge/src/symbheap/equality_test.ml b/sledge/src/symbheap/equality_test.ml
index e63fb626f..20327461b 100644
--- a/sledge/src/symbheap/equality_test.ml
+++ b/sledge/src/symbheap/equality_test.ml
@@ -18,12 +18,12 @@ let%test_module _ =
     let of_eqs = List.fold ~init:true_ ~f:(fun r (a, b) -> and_eq a b r)
     let i8 = Typ.integer ~bits:8
     let i64 = Typ.integer ~bits:64
-    let ( ! ) i = Exp.integer (Z.of_int i) Typ.siz
-    let ( + ) = Exp.add Typ.siz
-    let ( - ) = Exp.sub Typ.siz
-    let ( * ) = Exp.mul Typ.siz
-    let f = Exp.convert ~dst:i64 ~src:i8
-    let g = Exp.rem
+    let ( ! ) i = Term.integer (Z.of_int i) Typ.siz
+    let ( + ) = Term.add Typ.siz
+    let ( - ) = Term.sub Typ.siz
+    let ( * ) = Term.mul Typ.siz
+    let f = Term.convert ~dst:i64 ~src:i8
+    let g = Term.rem
     let wrt = Var.Set.empty
     let t_, wrt = Var.fresh "t" ~wrt
     let u_, wrt = Var.fresh "u" ~wrt
@@ -32,13 +32,13 @@ let%test_module _ =
     let x_, wrt = Var.fresh "x" ~wrt
     let y_, wrt = Var.fresh "y" ~wrt
     let z_, _ = Var.fresh "z" ~wrt
-    let t = Exp.var t_
-    let u = Exp.var u_
-    let v = Exp.var v_
-    let w = Exp.var w_
-    let x = Exp.var x_
-    let y = Exp.var y_
-    let z = Exp.var z_
+    let t = Term.var t_
+    let u = Term.var u_
+    let v = Term.var v_
+    let w = Term.var w_
+    let x = Term.var x_
+    let y = Term.var y_
+    let z = Term.var z_
     let f1 = of_eqs [(!0, !1)]
 
     let%test _ = is_false f1
@@ -212,9 +212,9 @@ let%test_module _ =
       %v_3 = %w_4 = %x_5 = %y_6 = %z_7 |}]
 
     let%expect_test _ =
-      printf (List.pp " , " Exp.pp) (Equality.class_of r7 t) ;
-      printf (List.pp " , " Exp.pp) (Equality.class_of r7 x) ;
-      printf (List.pp " , " Exp.pp) (Equality.class_of r7 z) ;
+      printf (List.pp " , " Term.pp) (Equality.class_of r7 t) ;
+      printf (List.pp " , " Term.pp) (Equality.class_of r7 x) ;
+      printf (List.pp " , " Term.pp) (Equality.class_of r7 z) ;
       [%expect
         {|
         %t_1
@@ -235,7 +235,7 @@ let%test_module _ =
       {sat= true;
        rep= [[%w_4 ↦ %v_3]; [%x_5 ↦ %v_3]; [%y_6 ↦ %v_3]; [%z_7 ↦ %v_3]]} |}]
 
-    let%test _ = normalize r7' w |> Exp.equal v
+    let%test _ = normalize r7' w |> Term.equal v
 
     let%test _ =
       entails_eq (of_eqs [(g w x, g y z); (x, z)]) (g w x) (g w z)
@@ -275,10 +275,10 @@ let%test_module _ =
     let%expect_test _ =
       pp_classes r10 ;
       pp r10 ;
-      Format.printf "@.%a@." Exp.pp (z - (x + !8)) ;
-      Format.printf "@.%a@." Exp.pp (normalize r10 (z - (x + !8))) ;
-      Format.printf "@.%a@." Exp.pp (x + !8 - z) ;
-      Format.printf "@.%a@." Exp.pp (normalize r10 (x + !8 - z)) ;
+      Format.printf "@.%a@." Term.pp (z - (x + !8)) ;
+      Format.printf "@.%a@." Term.pp (normalize r10 (z - (x + !8))) ;
+      Format.printf "@.%a@." Term.pp (x + !8 - z) ;
+      Format.printf "@.%a@." Term.pp (normalize r10 (x + !8 - z)) ;
       [%expect
         {|
       (%z_7 + -16) = %x_5
@@ -308,7 +308,7 @@ let%test_module _ =
 
     let%expect_test _ = pp_classes r12 ; [%expect {| (%z_7 + -16) = %x_5 |}]
 
-    let r13 = of_eqs [(Exp.eq x !2, y); (Exp.dq x !2, z); (y, z)]
+    let r13 = of_eqs [(Term.eq x !2, y); (Term.dq x !2, z); (y, z)]
 
     let%expect_test _ =
       pp r13 ;
@@ -319,15 +319,15 @@ let%test_module _ =
 
     let%test _ = not (is_false r13) (* incomplete *)
 
-    let a = Exp.dq x !0
+    let a = Term.dq x !0
     let r14 = of_eqs [(a, a); (x, !1)]
 
     let%expect_test _ =
       pp r14 ; [%expect {| {sat= true; rep= [[%x_5 ↦ 1]]} |}]
 
-    let%test _ = entails_eq r14 a (Exp.bool true)
+    let%test _ = entails_eq r14 a (Term.bool true)
 
-    let b = Exp.dq y !0
+    let b = Term.dq y !0
     let r14 = of_eqs [(a, b); (x, !1)]
 
     let%expect_test _ =
@@ -336,10 +336,10 @@ let%test_module _ =
         {|
           {sat= true; rep= [[%x_5 ↦ 1]; [(%y_6 ≠ 0) ↦ -1]]} |}]
 
-    let%test _ = entails_eq r14 a (Exp.bool true)
-    let%test _ = entails_eq r14 b (Exp.bool true)
+    let%test _ = entails_eq r14 a (Term.bool true)
+    let%test _ = entails_eq r14 b (Term.bool true)
 
-    let b = Exp.convert ~dst:i64 ~src:i8 (Exp.dq x !0)
+    let b = Term.convert ~dst:i64 ~src:i8 (Term.dq x !0)
     let r15 = of_eqs [(b, b); (x, !1)]
 
     let%expect_test _ =
diff --git a/sledge/src/symbheap/exec.ml b/sledge/src/symbheap/exec.ml
index 3b33e3d46..7e3393c73 100644
--- a/sledge/src/symbheap/exec.ml
+++ b/sledge/src/symbheap/exec.ml
@@ -17,11 +17,13 @@ type xseg = {us: Var.Set.t; xs: Var.Set.t; seg: Sh.seg}
 
 let fresh_var nam us xs =
   let var, us = Var.fresh nam ~wrt:us in
-  (Exp.var var, us, Set.add xs var)
+  (Term.var var, us, Set.add xs var)
 
 let fresh_seg ~loc ?bas ?len ?siz ?arr ?(xs = Var.Set.empty) us =
-  let freshen exp nam us xs =
-    match exp with Some exp -> (exp, us, xs) | None -> fresh_var nam us xs
+  let freshen term nam us xs =
+    match term with
+    | Some term -> (term, us, xs)
+    | None -> fresh_var nam us xs
   in
   let bas, us, xs = freshen bas "b" us xs in
   let len, us, xs = freshen len "m" us xs in
@@ -29,8 +31,8 @@ let fresh_seg ~loc ?bas ?len ?siz ?arr ?(xs = Var.Set.empty) us =
   let arr, us, xs = freshen arr "a" us xs in
   {us; xs; seg= {loc; bas; len; siz; arr}}
 
-let null_eq ptr = Sh.pure (Exp.eq Exp.null ptr)
-let zero = Exp.integer Z.zero Typ.siz
+let null_eq ptr = Sh.pure (Term.eq Term.null ptr)
+let zero = Term.integer Z.zero Typ.siz
 
 (* Overwritten variables renaming and remaining modified variables. [ws] are
    the written variables; [rs] are the variables read or in the
@@ -63,12 +65,12 @@ let move_spec us reg_exps =
   let ws, rs =
     Vector.fold reg_exps ~init:(Var.Set.empty, Var.Set.empty)
       ~f:(fun (ws, rs) (reg, exp) ->
-        (Set.add ws reg, Set.union rs (Exp.fv exp)) )
+        (Set.add ws reg, Set.union rs (Term.fv exp)) )
   in
   let sub, ms, _ = assign ~ws ~rs ~us in
   let post =
     Vector.fold reg_exps ~init:Sh.emp ~f:(fun post (reg, exp) ->
-        Sh.and_ (Exp.eq (Exp.var reg) (Exp.rename sub exp)) post )
+        Sh.and_ (Term.eq (Term.var reg) (Term.rename sub exp)) post )
   in
   {xs; foot; sub; ms; post}
 
@@ -82,7 +84,7 @@ let load_spec us reg ptr len =
   let sub, ms, _ = assign ~ws:(Set.add Var.Set.empty reg) ~rs:foot.us ~us in
   let post =
     Sh.and_
-      (Exp.eq (Exp.var reg) (Exp.rename sub seg.arr))
+      (Term.eq (Term.var reg) (Term.rename sub seg.arr))
       (Sh.rename sub foot)
   in
   {xs; foot; sub; ms; post}
@@ -104,7 +106,7 @@ let store_spec us ptr exp len =
 let memset_spec us dst byt len =
   let {us= _; xs; seg} = fresh_seg ~loc:dst ~siz:len us in
   let foot = Sh.seg seg in
-  let post = Sh.seg {seg with arr= Exp.splat ~byt ~siz:len} in
+  let post = Sh.seg {seg with arr= Term.splat ~byt ~siz:len} in
   {xs; foot; sub= Var.Subst.empty; ms= Var.Set.empty; post}
 
 (* { d=s * l=0 * d-[b;m)->⟨l,α⟩ }
@@ -115,7 +117,7 @@ let memcpy_eq_spec us dst src len =
   let {us= _; xs; seg} = fresh_seg ~loc:dst ~len us in
   let dst_heap = Sh.seg seg in
   let foot =
-    Sh.and_ (Exp.eq dst src) (Sh.and_ (Exp.eq len zero) dst_heap)
+    Sh.and_ (Term.eq dst src) (Sh.and_ (Term.eq len zero) dst_heap)
   in
   let post = dst_heap in
   {xs; foot; sub= Var.Subst.empty; ms= Var.Set.empty; post}
@@ -145,7 +147,7 @@ let memcpy_specs us dst src len =
 let memmov_eq_spec us dst src len =
   let {us= _; xs; seg= dst_seg} = fresh_seg ~loc:dst ~len us in
   let dst_heap = Sh.seg dst_seg in
-  let foot = Sh.and_ (Exp.eq dst src) dst_heap in
+  let foot = Sh.and_ (Term.eq dst src) dst_heap in
   let post = dst_heap in
   {xs; foot; sub= Var.Subst.empty; ms= Var.Set.empty; post}
 
@@ -163,17 +165,17 @@ let memmov_foot us dst src len =
   let arr_dst, us, xs = fresh_var "a" us xs in
   let arr_mid, us, xs = fresh_var "a" us xs in
   let arr_src, us, xs = fresh_var "a" us xs in
-  let src_dst = Exp.sub Typ.siz src dst in
-  let mem_dst = Exp.memory ~siz:src_dst ~arr:arr_dst in
-  let siz_mid = Exp.sub Typ.siz len src_dst in
-  let mem_mid = Exp.memory ~siz:siz_mid ~arr:arr_mid in
-  let mem_src = Exp.memory ~siz:src_dst ~arr:arr_src in
-  let mem_dst_mid_src = Exp.concat [|mem_dst; mem_mid; mem_src|] in
+  let src_dst = Term.sub Typ.siz src dst in
+  let mem_dst = Term.memory ~siz:src_dst ~arr:arr_dst in
+  let siz_mid = Term.sub Typ.siz len src_dst in
+  let mem_mid = Term.memory ~siz:siz_mid ~arr:arr_mid in
+  let mem_src = Term.memory ~siz:src_dst ~arr:arr_src in
+  let mem_dst_mid_src = Term.concat [|mem_dst; mem_mid; mem_src|] in
   let siz_dst_mid_src, us, xs = fresh_var "m" us xs in
   let arr_dst_mid_src, _, xs = fresh_var "a" us xs in
   let eq_mem_dst_mid_src =
-    Exp.eq mem_dst_mid_src
-      (Exp.memory ~siz:siz_dst_mid_src ~arr:arr_dst_mid_src)
+    Term.eq mem_dst_mid_src
+      (Term.memory ~siz:siz_dst_mid_src ~arr:arr_dst_mid_src)
   in
   let seg =
     Sh.seg
@@ -181,8 +183,8 @@ let memmov_foot us dst src len =
   in
   let foot =
     Sh.and_ eq_mem_dst_mid_src
-      (Sh.and_ (Exp.lt dst src)
-         (Sh.and_ (Exp.lt src (Exp.add Typ.ptr dst len)) seg))
+      (Sh.and_ (Term.lt dst src)
+         (Sh.and_ (Term.lt src (Term.add Typ.ptr dst len)) seg))
   in
   (xs, bas, siz, mem_dst, mem_mid, mem_src, foot)
 
@@ -194,12 +196,12 @@ let memmov_dn_spec us dst src len =
   let xs, bas, siz, _, mem_mid, mem_src, foot =
     memmov_foot us dst src len
   in
-  let mem_mid_src_src = Exp.concat [|mem_mid; mem_src; mem_src|] in
+  let mem_mid_src_src = Term.concat [|mem_mid; mem_src; mem_src|] in
   let siz_mid_src_src, us, xs = fresh_var "m" us xs in
   let arr_mid_src_src, _, xs = fresh_var "a" us xs in
   let eq_mem_mid_src_src =
-    Exp.eq mem_mid_src_src
-      (Exp.memory ~siz:siz_mid_src_src ~arr:arr_mid_src_src)
+    Term.eq mem_mid_src_src
+      (Term.memory ~siz:siz_mid_src_src ~arr:arr_mid_src_src)
   in
   let post =
     Sh.and_ eq_mem_mid_src_src
@@ -220,12 +222,12 @@ let memmov_up_spec us dst src len =
   let xs, bas, siz, mem_src, mem_mid, _, foot =
     memmov_foot us src dst len
   in
-  let mem_src_src_mid = Exp.concat [|mem_src; mem_src; mem_mid|] in
+  let mem_src_src_mid = Term.concat [|mem_src; mem_src; mem_mid|] in
   let siz_src_src_mid, us, xs = fresh_var "m" us xs in
   let arr_src_src_mid, _, xs = fresh_var "a" us xs in
   let eq_mem_src_src_mid =
-    Exp.eq mem_src_src_mid
-      (Exp.memory ~siz:siz_src_src_mid ~arr:arr_src_src_mid)
+    Term.eq mem_src_src_mid
+      (Term.memory ~siz:siz_src_src_mid ~arr:arr_src_src_mid)
   in
   let post =
     Sh.and_ eq_mem_src_src_mid
@@ -250,12 +252,12 @@ let memmov_specs us dst src len =
  *)
 let alloc_spec us reg num len =
   let foot = Sh.emp in
-  let siz = Exp.mul Typ.siz num len in
+  let siz = Term.mul Typ.siz num len in
   let sub, ms, us =
-    assign ~ws:(Set.add Var.Set.empty reg) ~rs:(Exp.fv siz) ~us
+    assign ~ws:(Set.add Var.Set.empty reg) ~rs:(Term.fv siz) ~us
   in
-  let loc = Exp.var reg in
-  let siz = Exp.rename sub siz in
+  let loc = Term.var reg in
+  let siz = Term.rename sub siz in
   let {us= _; xs; seg} = fresh_seg ~loc ~bas:loc ~len:siz ~siz us in
   let post = Sh.seg seg in
   {xs; foot; sub; ms; post}
@@ -293,12 +295,12 @@ let dallocx_spec us ptr =
 let malloc_spec us reg siz =
   let foot = Sh.emp in
   let sub, ms, us =
-    assign ~ws:(Set.add Var.Set.empty reg) ~rs:(Exp.fv siz) ~us
+    assign ~ws:(Set.add Var.Set.empty reg) ~rs:(Term.fv siz) ~us
   in
-  let loc = Exp.var reg in
-  let siz = Exp.rename sub siz in
+  let loc = Term.var reg in
+  let siz = Term.rename sub siz in
   let {us= _; xs; seg} = fresh_seg ~loc ~bas:loc ~len:siz ~siz us in
-  let post = Sh.or_ (null_eq (Exp.var reg)) (Sh.seg seg) in
+  let post = Sh.or_ (null_eq (Term.var reg)) (Sh.seg seg) in
   {xs; foot; sub; ms; post}
 
 (* { s≠0 }
@@ -306,14 +308,14 @@ let malloc_spec us reg siz =
  * { r=0 ∨ ∃α'. r-[r;sΘ)->⟨sΘ,α'⟩ }
  *)
 let mallocx_spec us reg siz =
-  let foot = Sh.pure Exp.(dq siz zero) in
+  let foot = Sh.pure Term.(dq siz zero) in
   let sub, ms, us =
-    assign ~ws:(Set.add Var.Set.empty reg) ~rs:(Exp.fv siz) ~us
+    assign ~ws:(Set.add Var.Set.empty reg) ~rs:(Term.fv siz) ~us
   in
-  let loc = Exp.var reg in
-  let siz = Exp.rename sub siz in
+  let loc = Term.var reg in
+  let siz = Term.rename sub siz in
   let {us= _; xs; seg} = fresh_seg ~loc ~bas:loc ~len:siz ~siz us in
-  let post = Sh.or_ (null_eq (Exp.var reg)) (Sh.seg seg) in
+  let post = Sh.or_ (null_eq (Term.var reg)) (Sh.seg seg) in
   {xs; foot; sub; ms; post}
 
 (* { emp }
@@ -322,18 +324,18 @@ let mallocx_spec us reg siz =
  *)
 let calloc_spec us reg num len =
   let foot = Sh.emp in
-  let siz = Exp.mul Typ.siz num len in
+  let siz = Term.mul Typ.siz num len in
   let sub, ms, us =
-    assign ~ws:(Set.add Var.Set.empty reg) ~rs:(Exp.fv siz) ~us
+    assign ~ws:(Set.add Var.Set.empty reg) ~rs:(Term.fv siz) ~us
   in
-  let loc = Exp.var reg in
-  let siz = Exp.rename sub siz in
-  let arr = Exp.splat ~byt:(Exp.integer Z.zero Typ.byt) ~siz in
+  let loc = Term.var reg in
+  let siz = Term.rename sub siz in
+  let arr = Term.splat ~byt:(Term.integer Z.zero Typ.byt) ~siz in
   let {us= _; xs; seg} = fresh_seg ~loc ~bas:loc ~len:siz ~siz ~arr us in
-  let post = Sh.or_ (null_eq (Exp.var reg)) (Sh.seg seg) in
+  let post = Sh.or_ (null_eq (Term.var reg)) (Sh.seg seg) in
   {xs; foot; sub; ms; post}
 
-let size_of_ptr = Option.value_exn (Exp.size_of Typ.ptr)
+let size_of_ptr = Option.value_exn (Term.size_of Typ.ptr)
 
 (* { p-[_;_)->⟨W,_⟩ }
  *   posix_memalign r p s
@@ -347,7 +349,7 @@ let posix_memalign_spec us reg ptr siz =
   let sub, ms, us =
     assign
       ~ws:(Set.add Var.Set.empty reg)
-      ~rs:(Set.union foot.us (Exp.fv siz))
+      ~rs:(Set.union foot.us (Term.fv siz))
       ~us
   in
   let q, us, xs = fresh_var "q" us xs in
@@ -355,13 +357,13 @@ let posix_memalign_spec us reg ptr siz =
   let {us= _; xs; seg= qseg} =
     fresh_seg ~loc:q ~bas:q ~len:siz ~siz ~xs us
   in
-  let eok = Exp.integer (Z.of_int 0) Typ.int in
-  let enomem = Exp.integer (Z.of_int 12) Typ.int in
+  let eok = Term.integer (Z.of_int 0) Typ.int in
+  let enomem = Term.integer (Z.of_int 12) Typ.int in
   let post =
     Sh.or_
-      (Sh.and_ (Exp.eq (Exp.var reg) enomem) (Sh.rename sub foot))
+      (Sh.and_ (Term.eq (Term.var reg) enomem) (Sh.rename sub foot))
       (Sh.and_
-         (Exp.eq (Exp.var reg) eok)
+         (Term.eq (Term.var reg) eok)
          (Sh.rename sub (Sh.star (Sh.seg pseg') (Sh.seg qseg))))
   in
   {xs; foot; sub; ms; post}
@@ -381,20 +383,20 @@ let realloc_spec us reg ptr siz =
   let sub, ms, us =
     assign
       ~ws:(Set.add Var.Set.empty reg)
-      ~rs:(Set.union foot.us (Exp.fv siz))
+      ~rs:(Set.union foot.us (Term.fv siz))
       ~us
   in
-  let loc = Exp.var reg in
-  let siz = Exp.rename sub siz in
+  let loc = Term.var reg in
+  let siz = Term.rename sub siz in
   let {us; xs; seg= rseg} = fresh_seg ~loc ~bas:loc ~len:siz ~siz ~xs us in
   let a0 = pseg.arr in
   let a1 = rseg.arr in
   let a2, _, xs = fresh_var "a" us xs in
   let post =
     Sh.or_
-      (Sh.and_ Exp.(eq loc null) (Sh.rename sub foot))
+      (Sh.and_ Term.(eq loc null) (Sh.rename sub foot))
       (Sh.and_
-         Exp.(
+         Term.(
            conditional ~cnd:(le len siz)
              ~thn:
                (eq (memory ~siz ~arr:a1)
@@ -422,21 +424,21 @@ let rallocx_spec us reg ptr siz =
     fresh_seg ~loc:ptr ~bas:ptr ~len ~siz:len ~xs us
   in
   let pheap = Sh.seg pseg in
-  let foot = Sh.and_ Exp.(dq siz zero) pheap in
+  let foot = Sh.and_ Term.(dq siz zero) pheap in
   let sub, ms, us =
     assign ~ws:(Set.add Var.Set.empty reg) ~rs:foot.us ~us
   in
-  let loc = Exp.var reg in
-  let siz = Exp.rename sub siz in
+  let loc = Term.var reg in
+  let siz = Term.rename sub siz in
   let {us; xs; seg= rseg} = fresh_seg ~loc ~bas:loc ~len:siz ~siz ~xs us in
   let a0 = pseg.arr in
   let a1 = rseg.arr in
   let a2, _, xs = fresh_var "a" us xs in
   let post =
     Sh.or_
-      (Sh.and_ Exp.(eq loc null) (Sh.rename sub pheap))
+      (Sh.and_ Term.(eq loc null) (Sh.rename sub pheap))
       (Sh.and_
-         Exp.(
+         Term.(
            conditional ~cnd:(le len siz)
              ~thn:
                (eq (memory ~siz ~arr:a1)
@@ -460,17 +462,17 @@ let rallocx_spec us reg ptr siz =
 let xallocx_spec us reg ptr siz ext =
   let len, us, xs = fresh_var "m" us Var.Set.empty in
   let {us; xs; seg} = fresh_seg ~loc:ptr ~bas:ptr ~len ~siz:len ~xs us in
-  let foot = Sh.and_ Exp.(dq siz zero) (Sh.seg seg) in
+  let foot = Sh.and_ Term.(dq siz zero) (Sh.seg seg) in
   let sub, ms, us =
     assign
       ~ws:(Set.add Var.Set.empty reg)
-      ~rs:Set.(union foot.us (union (Exp.fv siz) (Exp.fv ext)))
+      ~rs:Set.(union foot.us (union (Term.fv siz) (Term.fv ext)))
       ~us
   in
-  let reg = Exp.var reg in
-  let ptr = Exp.rename sub ptr in
-  let siz = Exp.rename sub siz in
-  let ext = Exp.rename sub ext in
+  let reg = Term.var reg in
+  let ptr = Term.rename sub ptr in
+  let siz = Term.rename sub siz in
+  let ext = Term.rename sub ext in
   let {us; xs; seg= seg'} =
     fresh_seg ~loc:ptr ~bas:ptr ~len:reg ~siz:reg ~xs us
   in
@@ -479,7 +481,7 @@ let xallocx_spec us reg ptr siz ext =
   let a2, _, xs = fresh_var "a" us xs in
   let post =
     Sh.and_
-      Exp.(
+      Term.(
         and_
           (conditional ~cnd:(le len siz)
              ~thn:
@@ -506,7 +508,7 @@ let sallocx_spec us reg ptr =
   let {us; xs; seg} = fresh_seg ~loc:ptr ~bas:ptr ~len ~siz:len ~xs us in
   let foot = Sh.seg seg in
   let sub, ms, _ = assign ~ws:(Set.add Var.Set.empty reg) ~rs:foot.us ~us in
-  let post = Sh.and_ Exp.(eq (var reg) len) (Sh.rename sub foot) in
+  let post = Sh.and_ Term.(eq (var reg) len) (Sh.rename sub foot) in
   {xs; foot; sub; ms; post}
 
 (* { p-[p;m)->⟨m,α⟩ }
@@ -518,7 +520,7 @@ let malloc_usable_size_spec us reg ptr =
   let {us; xs; seg} = fresh_seg ~loc:ptr ~bas:ptr ~len ~siz:len ~xs us in
   let foot = Sh.seg seg in
   let sub, ms, _ = assign ~ws:(Set.add Var.Set.empty reg) ~rs:foot.us ~us in
-  let post = Sh.and_ Exp.(le len (var reg)) (Sh.rename sub foot) in
+  let post = Sh.and_ Term.(le len (var reg)) (Sh.rename sub foot) in
   {xs; foot; sub; ms; post}
 
 (* { s≠0 }
@@ -527,15 +529,15 @@ let malloc_usable_size_spec us reg ptr =
  *)
 let nallocx_spec us reg siz =
   let xs = Var.Set.empty in
-  let foot = Sh.pure (Exp.dq siz zero) in
+  let foot = Sh.pure (Term.dq siz zero) in
   let sub, ms, _ = assign ~ws:(Set.add Var.Set.empty reg) ~rs:foot.us ~us in
-  let loc = Exp.var reg in
-  let siz = Exp.rename sub siz in
-  let post = Sh.or_ (null_eq loc) (Sh.pure (Exp.eq loc siz)) in
+  let loc = Term.var reg in
+  let siz = Term.rename sub siz in
+  let post = Sh.or_ (null_eq loc) (Sh.pure (Term.eq loc siz)) in
   {xs; foot; sub; ms; post}
 
 let size_of_int_mul n =
-  Exp.mul Typ.siz (Option.value_exn (Exp.size_of Typ.siz)) n
+  Term.mul Typ.siz (Option.value_exn (Term.size_of Typ.siz)) n
 
 (* { r-[_;_)->⟨m,_⟩ * i-[_;_)->⟨_,m⟩ * w=0 * n=0 }
  *   mallctl r i w n
@@ -547,8 +549,8 @@ let mallctl_read_spec us r i w n =
   let a, _, xs = fresh_var "a" us xs in
   let foot =
     Sh.and_
-      Exp.(eq w null)
-      (Sh.and_ Exp.(eq n zero) (Sh.star (Sh.seg iseg) (Sh.seg rseg)))
+      Term.(eq w null)
+      (Sh.and_ Term.(eq n zero) (Sh.star (Sh.seg iseg) (Sh.seg rseg)))
   in
   let rseg' = {rseg with arr= a} in
   let post = Sh.star (Sh.seg rseg') (Sh.seg iseg) in
@@ -569,8 +571,8 @@ let mallctlbymib_read_spec us p l r i w n =
   let a, _, xs = fresh_var "a" us xs in
   let foot =
     Sh.and_
-      Exp.(eq w null)
-      (Sh.and_ Exp.(eq n zero) (Sh.star const (Sh.seg rseg)))
+      Term.(eq w null)
+      (Sh.and_ Term.(eq n zero) (Sh.star const (Sh.seg rseg)))
   in
   let rseg' = {rseg with arr= a} in
   let post = Sh.star (Sh.seg rseg') const in
@@ -583,7 +585,7 @@ let mallctlbymib_read_spec us p l r i w n =
 let mallctl_write_spec us r i w n =
   let {us= _; xs; seg} = fresh_seg ~loc:w ~siz:n us in
   let post = Sh.seg seg in
-  let foot = Sh.and_ Exp.(eq r null) (Sh.and_ Exp.(eq i zero) post) in
+  let foot = Sh.and_ Term.(eq r null) (Sh.and_ Term.(eq i zero) post) in
   {xs; foot; sub= Var.Subst.empty; ms= Var.Set.empty; post}
 
 (* { p-[_;_)->⟨W×l,_⟩ * r=0 * i=0 * w-[_;_)->⟨n,_⟩ }
@@ -596,7 +598,7 @@ let mallctlbymib_write_spec us p l r i w n =
   let {us; xs; seg= pseg} = fresh_seg ~loc:p ~siz:wl us in
   let {us= _; xs; seg= wseg} = fresh_seg ~loc:w ~siz:n ~xs us in
   let post = Sh.star (Sh.seg pseg) (Sh.seg wseg) in
-  let foot = Sh.and_ Exp.(eq r null) (Sh.and_ Exp.(eq i zero) post) in
+  let foot = Sh.and_ Term.(eq r null) (Sh.and_ Term.(eq i zero) post) in
   {xs; foot; sub= Var.Subst.empty; ms= Var.Set.empty; post}
 
 let mallctl_specs us r i w n =
@@ -641,12 +643,14 @@ let strlen_spec us reg ptr =
   let sub, ms, _ = assign ~ws:(Set.add Var.Set.empty reg) ~rs:foot.us ~us in
   let {Sh.loc= p; bas= b; len= m; _} = seg in
   let ret =
-    Exp.sub Typ.siz
-      (Exp.sub Typ.siz (Exp.add Typ.siz b m) p)
-      (Exp.integer Z.one Typ.siz)
+    Term.sub Typ.siz
+      (Term.sub Typ.siz (Term.add Typ.siz b m) p)
+      (Term.integer Z.one Typ.siz)
   in
   let post =
-    Sh.and_ (Exp.eq (Exp.var reg) (Exp.rename sub ret)) (Sh.rename sub foot)
+    Sh.and_
+      (Term.eq (Term.var reg) (Term.rename sub ret))
+      (Sh.rename sub foot)
   in
   {xs; foot; sub; ms; post}
 
@@ -705,20 +709,38 @@ let inst : Sh.t -> Llair.inst -> (Sh.t, unit) result =
  fun pre inst ->
   [%Trace.info
     "@[<2>exec inst %a from@ @[{ %a@ }@]@]" Llair.Inst.pp inst Sh.pp pre] ;
-  assert (Set.disjoint (Sh.fv pre) (Llair.Inst.locals inst)) ;
+  assert (
+    Set.disjoint (Sh.fv pre) (Var.Set.of_regs (Llair.Inst.locals inst)) ) ;
   let us = pre.us in
   match inst with
-  | Move {reg_exps; _} -> exec_spec pre (move_spec us reg_exps)
-  | Load {reg; ptr; len; _} -> exec_spec pre (load_spec us reg ptr len)
-  | Store {ptr; exp; len; _} -> exec_spec pre (store_spec us ptr exp len)
-  | Memset {dst; byt; len; _} -> exec_spec pre (memset_spec us dst byt len)
+  | Move {reg_exps; _} ->
+      exec_spec pre
+        (move_spec us
+           (Vector.map reg_exps ~f:(fun (r, e) ->
+                (Var.of_reg r, Term.of_exp e) )))
+  | Load {reg; ptr; len; _} ->
+      exec_spec pre
+        (load_spec us (Var.of_reg reg) (Term.of_exp ptr) (Term.of_exp len))
+  | Store {ptr; exp; len; _} ->
+      exec_spec pre
+        (store_spec us (Term.of_exp ptr) (Term.of_exp exp) (Term.of_exp len))
+  | Memset {dst; byt; len; _} ->
+      exec_spec pre
+        (memset_spec us (Term.of_exp dst) (Term.of_exp byt)
+           (Term.of_exp len))
   | Memcpy {dst; src; len; _} ->
-      exec_specs pre (memcpy_specs us dst src len)
+      exec_specs pre
+        (memcpy_specs us (Term.of_exp dst) (Term.of_exp src)
+           (Term.of_exp len))
   | Memmov {dst; src; len; _} ->
-      exec_specs pre (memmov_specs us dst src len)
-  | Alloc {reg; num; len; _} -> exec_spec pre (alloc_spec us reg num len)
-  | Free {ptr; _} -> exec_spec pre (free_spec us ptr)
-  | Nondet {reg= Some reg; _} -> Ok (kill pre reg)
+      exec_specs pre
+        (memmov_specs us (Term.of_exp dst) (Term.of_exp src)
+           (Term.of_exp len))
+  | Alloc {reg; num; len; _} ->
+      exec_spec pre
+        (alloc_spec us (Var.of_reg reg) (Term.of_exp num) (Term.of_exp len))
+  | Free {ptr; _} -> exec_spec pre (free_spec us (Term.of_exp ptr))
+  | Nondet {reg= Some reg; _} -> Ok (kill pre (Var.of_reg reg))
   | Nondet {reg= None; _} -> Ok pre
   | Abort _ -> Error ()
 
@@ -728,13 +750,13 @@ let intrinsic ~skip_throw :
        Sh.t
     -> Var.t option
     -> Var.t
-    -> Exp.t list
+    -> Term.t list
     -> (Sh.t, unit) result option =
  fun pre areturn intrinsic actuals ->
   [%Trace.info
     "@[<2>exec intrinsic@ @[%a%a(@[%a@])@] from@ @[{ %a@ }@]@]"
       (Option.pp "%a := " Var.pp)
-      areturn Var.pp intrinsic (List.pp ",@ " Exp.pp) (List.rev actuals)
+      areturn Var.pp intrinsic (List.pp ",@ " Term.pp) (List.rev actuals)
       Sh.pp pre] ;
   let us = pre.us in
   let name =
diff --git a/sledge/src/symbheap/exec.mli b/sledge/src/symbheap/exec.mli
index c379acc39..f91ce13c8 100644
--- a/sledge/src/symbheap/exec.mli
+++ b/sledge/src/symbheap/exec.mli
@@ -7,9 +7,9 @@
 
 (** Symbolic Execution *)
 
-val assume : Sh.t -> Exp.t -> Sh.t option
+val assume : Sh.t -> Term.t -> Sh.t option
 val kill : Sh.t -> Var.t -> Sh.t
-val move : Sh.t -> Var.t -> Exp.t -> Sh.t
+val move : Sh.t -> Var.t -> Term.t -> Sh.t
 val inst : Sh.t -> Llair.inst -> (Sh.t, unit) result
 
 val intrinsic :
@@ -17,5 +17,5 @@ val intrinsic :
   -> Sh.t
   -> Var.t option
   -> Var.t
-  -> Exp.t list
+  -> Term.t list
   -> (Sh.t, unit) result option
diff --git a/sledge/src/symbheap/sh.ml b/sledge/src/symbheap/sh.ml
index 7ac767768..5ee90ae70 100644
--- a/sledge/src/symbheap/sh.ml
+++ b/sledge/src/symbheap/sh.ml
@@ -9,14 +9,14 @@
 
 [@@@warning "+9"]
 
-type seg = {loc: Exp.t; bas: Exp.t; len: Exp.t; siz: Exp.t; arr: Exp.t}
+type seg = {loc: Term.t; bas: Term.t; len: Term.t; siz: Term.t; arr: Term.t}
 [@@deriving compare, equal, sexp]
 
 type starjunction =
   { us: Var.Set.t
   ; xs: Var.Set.t
   ; cong: Equality.t
-  ; pure: Exp.t list
+  ; pure: Term.t list
   ; heap: seg list
   ; djns: disjunction list }
 [@@deriving compare, equal, sexp]
@@ -29,12 +29,12 @@ let map_seg {loc; bas; len; siz; arr} ~f =
   {loc= f loc; bas= f bas; len= f len; siz= f siz; arr= f arr}
 
 let pp_seg ?is_x fs {loc; bas; len; siz; arr} =
-  let exp_pp = Exp.pp_full ?is_x in
-  Format.fprintf fs "@[<2>%a@ @[@[-[%a)->@]@ %a@]@]" exp_pp loc
+  let term_pp = Term.pp_full ?is_x in
+  Format.fprintf fs "@[<2>%a@ @[@[-[%a)->@]@ %a@]@]" term_pp loc
     (fun fs (bas, len) ->
-      if (not (Exp.equal loc bas)) || not (Exp.equal len siz) then
-        Format.fprintf fs " %a, %a " exp_pp bas exp_pp len )
-    (bas, len) exp_pp (Exp.memory ~siz ~arr)
+      if (not (Term.equal loc bas)) || not (Term.equal len siz) then
+        Format.fprintf fs " %a, %a " term_pp bas term_pp len )
+    (bas, len) term_pp (Term.memory ~siz ~arr)
 
 let pp_seg_norm cong fs seg =
   pp_seg fs (map_seg seg ~f:(Equality.normalize cong))
@@ -46,7 +46,7 @@ let pp_us ?(pre = ("" : _ fmt)) fs us =
 let rec pp vs all_xs fs {us; xs; cong; pure; heap; djns} =
   Format.pp_open_hvbox fs 0 ;
   let all_xs = Set.union all_xs xs in
-  let is_x var = Set.mem all_xs (Option.value_exn (Var.of_exp var)) in
+  let is_x var = Set.mem all_xs (Option.value_exn (Var.of_term var)) in
   pp_us fs us ;
   let xs_i_vs, xs_d_vs = Set.inter_diff vs xs in
   if not (Set.is_empty xs_i_vs) then (
@@ -57,15 +57,15 @@ let rec pp vs all_xs fs {us; xs; cong; pure; heap; djns} =
   let first = Equality.is_true cong in
   if not first then Format.fprintf fs "  " ;
   Equality.pp_classes ~is_x fs cong ;
-  let pure_exps =
+  let pure_terms =
     List.filter_map pure ~f:(fun e ->
         let e' = Equality.normalize cong e in
-        if Exp.is_true e' then None else Some e' )
+        if Term.is_true e' then None else Some e' )
   in
   List.pp
     ~pre:(if first then "  " else "@ @<2>∧ ")
-    "@ @<2>∧ " (Exp.pp_full ~is_x) fs pure_exps ;
-  let first = first && List.is_empty pure_exps in
+    "@ @<2>∧ " (Term.pp_full ~is_x) fs pure_terms ;
+  let first = first && List.is_empty pure_terms in
   if List.is_empty heap then
     Format.fprintf fs
       ( if first then if List.is_empty djns then "  emp" else ""
@@ -78,11 +78,12 @@ let rec pp vs all_xs fs {us; xs; cong; pure; heap; djns} =
          (List.map ~f:(map_seg ~f:(Equality.normalize cong)) heap)
          ~compare:(fun s1 s2 ->
            let b_o = function
-             | Exp.App {op= App {op= Add _; arg}; arg= Integer {data; _}} ->
+             | Term.App {op= App {op= Add _; arg}; arg= Integer {data; _}}
+               ->
                  (arg, data)
              | e -> (e, Z.zero)
            in
-           [%compare: Exp.t * (Exp.t * Z.t)]
+           [%compare: Term.t * (Term.t * Z.t)]
              (s1.bas, b_o s1.loc)
              (s2.bas, b_o s2.loc) )) ;
   let first = first && List.is_empty heap in
@@ -105,34 +106,34 @@ and pp_djn vs all_xs fs = function
 let pp = pp Var.Set.empty Var.Set.empty
 let pp_djn = pp_djn Var.Set.empty Var.Set.empty
 
-let fold_exps_seg {loc; bas; len; siz; arr} ~init ~f =
-  let f b z = Exp.fold_exps b ~init:z ~f in
+let fold_terms_seg {loc; bas; len; siz; arr} ~init ~f =
+  let f b z = Term.fold_terms b ~init:z ~f in
   f loc (f bas (f len (f siz (f arr init))))
 
 let fold_vars_seg seg ~init ~f =
-  fold_exps_seg seg ~init ~f:(fun init -> Exp.fold_vars ~f ~init)
+  fold_terms_seg seg ~init ~f:(fun init -> Term.fold_vars ~f ~init)
 
 let fv_seg seg = fold_vars_seg seg ~f:Set.add ~init:Var.Set.empty
 
-let fold_exps fold_exps {us= _; xs= _; cong; pure; heap; djns} ~init ~f =
-  Equality.fold_exps ~init cong ~f
+let fold_terms fold_terms {us= _; xs= _; cong; pure; heap; djns} ~init ~f =
+  Equality.fold_terms ~init cong ~f
   |> fun init ->
-  List.fold ~init pure ~f:(fun init -> Exp.fold_exps ~f ~init)
+  List.fold ~init pure ~f:(fun init -> Term.fold_terms ~f ~init)
   |> fun init ->
-  List.fold ~init heap ~f:(fun init -> fold_exps_seg ~f ~init)
+  List.fold ~init heap ~f:(fun init -> fold_terms_seg ~f ~init)
   |> fun init ->
-  List.fold ~init djns ~f:(fun init -> List.fold ~init ~f:fold_exps)
+  List.fold ~init djns ~f:(fun init -> List.fold ~init ~f:fold_terms)
 
 let rec fv_union init q =
   Set.diff
-    (fold_exps fv_union q ~init ~f:(fun init ->
-         Exp.fold_vars ~f:Set.add ~init ))
+    (fold_terms fv_union q ~init ~f:(fun init ->
+         Term.fold_vars ~f:Set.add ~init ))
     q.xs
 
 let fv q = fv_union Var.Set.empty q
 
 let invariant_pure = function
-  | Exp.Integer {data; typ} ->
+  | Term.Integer {data; typ} ->
       assert (Typ.equal Typ.bool typ) ;
       assert (not (Z.is_false data))
   | _ -> assert true
@@ -186,11 +187,11 @@ let rec simplify {us; xs; cong; pure; heap; djns} =
 (** Quantification and Vocabulary *)
 
 let rename_seg sub ({loc; bas; len; siz; arr} as h) =
-  let loc = Exp.rename sub loc in
-  let bas = Exp.rename sub bas in
-  let len = Exp.rename sub len in
-  let siz = Exp.rename sub siz in
-  let arr = Exp.rename sub arr in
+  let loc = Term.rename sub loc in
+  let bas = Term.rename sub bas in
+  let len = Term.rename sub len in
+  let siz = Term.rename sub siz in
+  let arr = Term.rename sub arr in
   ( if
     loc == h.loc && bas == h.bas && len == h.len && siz == h.siz
     && arr == h.arr
@@ -203,7 +204,7 @@ let rename_seg sub ({loc; bas; len; siz; arr} as h) =
     invariant *)
 let rec apply_subst sub ({us= _; xs= _; cong; pure; heap; djns} as q) =
   let cong = Equality.rename cong sub in
-  let pure = List.map_preserving_phys_equal pure ~f:(Exp.rename sub) in
+  let pure = List.map_preserving_phys_equal pure ~f:(Term.rename sub) in
   let heap = List.map_preserving_phys_equal heap ~f:(rename_seg sub) in
   let djns =
     List.map_preserving_phys_equal djns ~f:(fun d ->
@@ -375,10 +376,10 @@ let or_ q1 q2 =
     invariant q ;
     assert (Set.equal q.us (Set.union q1.us q2.us))]
 
-let rec pure (e : Exp.t) =
-  [%Trace.call fun {pf} -> pf "%a" Exp.pp e]
+let rec pure (e : Term.t) =
+  [%Trace.call fun {pf} -> pf "%a" Term.pp e]
   ;
-  let us = Exp.fv e in
+  let us = Term.fv e in
   ( match e with
   | Integer {data; typ= Integer {bits= 1}} ->
       if Z.is_false data then false_ us else emp
@@ -388,7 +389,7 @@ let rec pure (e : Exp.t) =
     ->
       or_
         (star (pure cnd) (pure thn))
-        (star (pure (Exp.not_ Typ.bool cnd)) (pure els))
+        (star (pure (Term.not_ Typ.bool cnd)) (pure els))
   | App {op= App {op= Eq; arg= e1}; arg= e2} ->
       let cong = Equality.(and_eq e1 e2 true_) in
       if Equality.is_false cong then false_ us
@@ -401,7 +402,7 @@ let and_ e q = star (pure e) q
 
 let seg pt =
   let us = fv_seg pt in
-  if Exp.equal Exp.null pt.loc then false_ us
+  if Term.equal Term.null pt.loc then false_ us
   else {emp with us; heap= [pt]} |> check invariant
 
 (** Update *)
@@ -423,9 +424,10 @@ let is_emp = function
 let is_false = function
   | {djns= [[]]; _} -> true
   | {cong; pure; heap; _} ->
-      List.exists pure ~f:(fun b -> Exp.is_false (Equality.normalize cong b))
+      List.exists pure ~f:(fun b ->
+          Term.is_false (Equality.normalize cong b) )
       || List.exists heap ~f:(fun seg ->
-             Equality.entails_eq cong seg.loc Exp.null )
+             Equality.entails_eq cong seg.loc Term.null )
 
 let rec pure_approx ({us; xs; cong; pure; heap= _; djns} as q) =
   let heap = emp.heap in
diff --git a/sledge/src/symbheap/sh.mli b/sledge/src/symbheap/sh.mli
index 94198f72f..c8a61a992 100644
--- a/sledge/src/symbheap/sh.mli
+++ b/sledge/src/symbheap/sh.mli
@@ -11,13 +11,13 @@
     size [siz], contained in an enclosing allocation-block starting at [bas]
     of length [len]. Byte-array expressions are either [Var]iables or
     [Splat] vectors. *)
-type seg = {loc: Exp.t; bas: Exp.t; len: Exp.t; siz: Exp.t; arr: Exp.t}
+type seg = {loc: Term.t; bas: Term.t; len: Term.t; siz: Term.t; arr: Term.t}
 
 type starjunction = private
   { us: Var.Set.t  (** vocabulary / variable context of formula *)
   ; xs: Var.Set.t  (** existentially-bound variables *)
   ; cong: Equality.t  (** congruence induced by rest of formula *)
-  ; pure: Exp.t list  (** conjunction of pure boolean constraints *)
+  ; pure: Term.t list  (** conjunction of pure boolean constraints *)
   ; heap: seg list  (** star-conjunction of segment atomic formulas *)
   ; djns: disjunction list  (** star-conjunction of disjunctions *) }
 
@@ -25,7 +25,7 @@ and disjunction = starjunction list
 
 type t = starjunction [@@deriving equal, compare, sexp]
 
-val pp_seg : ?is_x:(Exp.t -> bool) -> seg pp
+val pp_seg : ?is_x:(Term.t -> bool) -> seg pp
 val pp_seg_norm : Equality.t -> seg pp
 val pp_us : ?pre:('a, 'a) fmt -> Var.Set.t pp
 val pp : t pp
@@ -53,10 +53,10 @@ val or_ : t -> t -> t
 (** Disjoin formulas, extending to a common vocabulary, and avoiding
     capturing existentials. *)
 
-val pure : Exp.t -> t
+val pure : Term.t -> t
 (** Atomic pure boolean constraint formula. *)
 
-val and_ : Exp.t -> t -> t
+val and_ : Term.t -> t -> t
 (** Conjoin a boolean constraint to a formula. *)
 
 val and_cong : Equality.t -> t -> t
@@ -65,7 +65,7 @@ val and_cong : Equality.t -> t -> t
 
 (** Update *)
 
-val with_pure : Exp.t list -> t -> t
+val with_pure : Term.t list -> t -> t
 (** [with_pure pure q] is [{q with pure}], which assumes that [q.pure] and
     [pure] are defined in the same vocabulary, induce the same congruence,
     etc. It can essentially only be used when [pure] is logically equivalent
diff --git a/sledge/src/symbheap/sh_domain.ml b/sledge/src/symbheap/sh_domain.ml
index 391b406b9..2cbd543ba 100644
--- a/sledge/src/symbheap/sh_domain.ml
+++ b/sledge/src/symbheap/sh_domain.ml
@@ -19,29 +19,38 @@ let report_fmt_thunk = Fn.flip pp
 
 let init globals =
   Vector.fold globals ~init:Sh.emp ~f:(fun q -> function
-    | {Global.var; init= Some (arr, siz)} ->
-        let loc = Exp.var var in
-        let len = Exp.integer (Z.of_int siz) Typ.siz in
+    | {Global.reg; init= Some (arr, siz)} ->
+        let loc = Term.var (Var.of_reg reg) in
+        let len = Term.integer (Z.of_int siz) Typ.siz in
+        let arr = Term.of_exp arr in
         Sh.star q (Sh.seg {loc; bas= loc; len; siz= len; arr})
     | _ -> q )
 
 let join l r = Some (Sh.or_ l r)
 let is_false = Sh.is_false
-let exec_assume = Exec.assume
-let exec_kill = Exec.kill
-let exec_move = Exec.move
+let exec_assume q b = Exec.assume q (Term.of_exp b)
+let exec_kill q r = Exec.kill q (Var.of_reg r)
+let exec_move q r e = Exec.move q (Var.of_reg r) (Term.of_exp e)
 let exec_inst = Exec.inst
-let exec_intrinsic = Exec.intrinsic
+
+let exec_intrinsic ~skip_throw q r i es =
+  Exec.intrinsic ~skip_throw q
+    (Option.map ~f:Var.of_reg r)
+    (Var.of_reg i)
+    (List.map ~f:Term.of_exp es)
+
 let dnf = Sh.dnf
 
-let exp_eq_class_has_only_vars_in fvs cong exp =
+let term_eq_class_has_only_vars_in fvs cong term =
   [%Trace.call fun {pf} ->
-    pf "@[<v> fvs: @[%a@] @,cong: @[%a@] @,exp: @[%a@]@]" Var.Set.pp fvs
-      Equality.pp cong Exp.pp exp]
+    pf "@[<v> fvs: @[%a@] @,cong: @[%a@] @,term: @[%a@]@]" Var.Set.pp fvs
+      Equality.pp cong Term.pp term]
   ;
-  let exp_has_only_vars_in fvs exp = Set.is_subset (Exp.fv exp) ~of_:fvs in
-  let exp_eq_class = Equality.class_of cong exp in
-  List.exists ~f:(exp_has_only_vars_in fvs) exp_eq_class
+  let term_has_only_vars_in fvs term =
+    Set.is_subset (Term.fv term) ~of_:fvs
+  in
+  let term_eq_class = Equality.class_of cong term in
+  List.exists ~f:(term_has_only_vars_in fvs) term_eq_class
   |>
   [%Trace.retn fun {pf} -> pf "%b"]
 
@@ -55,16 +64,16 @@ let garbage_collect (q : t) ~wrt =
     else
       let new_set =
         List.fold ~init:current q.heap ~f:(fun current seg ->
-            if exp_eq_class_has_only_vars_in current q.cong seg.loc then
+            if term_eq_class_has_only_vars_in current q.cong seg.loc then
               List.fold (Equality.class_of q.cong seg.arr) ~init:current
-                ~f:(fun c e -> Set.union c (Exp.fv e))
+                ~f:(fun c e -> Set.union c (Term.fv e))
             else current )
       in
       all_reachable_vars current new_set q
   in
   let r_vars = all_reachable_vars Var.Set.empty wrt q in
   Sh.filter_heap q ~f:(fun seg ->
-      exp_eq_class_has_only_vars_in r_vars q.cong seg.loc )
+      term_eq_class_has_only_vars_in r_vars q.cong seg.loc )
   |>
   [%Trace.retn fun {pf} -> pf "%a" pp]
 
@@ -79,15 +88,19 @@ let call ~summaries ~globals actuals areturn formals ~locals q =
     pf
       "@[<hv>actuals: (@[%a@])@ formals: (@[%a@])@ locals: {@[%a@]}@ \
        globals: {@[%a@]}@ q: %a@]"
-      (List.pp ",@ " Exp.pp) (List.rev actuals) (List.pp ",@ " Var.pp)
-      (List.rev formals) Var.Set.pp locals Var.Set.pp globals pp q]
+      (List.pp ",@ " Exp.pp) (List.rev actuals) (List.pp ",@ " Reg.pp)
+      (List.rev formals) Reg.Set.pp locals Reg.Set.pp globals pp q]
   ;
+  let actuals = List.map ~f:Term.of_exp actuals in
+  let areturn = Option.map ~f:Var.of_reg areturn in
+  let formals = List.map ~f:Var.of_reg formals in
+  let locals = Var.Set.of_regs locals in
   let q', freshen_locals =
     Sh.freshen q ~wrt:(Set.add_list formals locals)
   in
   let and_eq q formal actual =
-    let actual' = Exp.rename freshen_locals actual in
-    Sh.and_ (Exp.eq (Exp.var formal) actual') q
+    let actual' = Term.rename freshen_locals actual in
+    Sh.and_ (Term.eq (Term.var formal) actual') q
   in
   let and_eqs formals actuals q =
     List.fold2_exn ~f:and_eq formals actuals ~init:q
@@ -101,7 +114,8 @@ let call ~summaries ~globals actuals areturn formals ~locals q =
        them *)
     let formals_set = Var.Set.of_list formals in
     let function_summary_pre =
-      garbage_collect q'' ~wrt:(Set.union formals_set globals)
+      garbage_collect q''
+        ~wrt:(Set.union formals_set (Var.Set.of_regs globals))
     in
     [%Trace.info "function summary pre %a" pp function_summary_pre] ;
     let foot = Sh.exists formals_set function_summary_pre in
@@ -124,8 +138,9 @@ let recursion_beyond_bound = `prune
 (** Leave scope of locals: existentially quantify locals. *)
 let post locals _ q =
   [%Trace.call fun {pf} ->
-    pf "@[<hv>locals: {@[%a@]}@ q: %a@]" Var.Set.pp locals Sh.pp q]
+    pf "@[<hv>locals: {@[%a@]}@ q: %a@]" Reg.Set.pp locals Sh.pp q]
   ;
+  let locals = Var.Set.of_regs locals in
   Sh.exists locals q
   |>
   [%Trace.retn fun {pf} -> pf "%a" Sh.pp]
@@ -136,13 +151,15 @@ let post locals _ q =
 let retn formals freturn {areturn; subst; frame} q =
   [%Trace.call fun {pf} ->
     pf "@[<v>formals: {@[%a@]}@ subst: %a@ q: %a@ frame: %a@]"
-      (List.pp ", " Var.pp) formals Var.Subst.pp (Var.Subst.invert subst) pp
+      (List.pp ", " Reg.pp) formals Var.Subst.pp (Var.Subst.invert subst) pp
       q pp frame]
   ;
+  let formals = List.map ~f:Var.of_reg formals in
+  let freturn = Option.map ~f:Var.of_reg freturn in
   let q =
     match (areturn, freturn) with
-    | Some areturn, Some freturn -> exec_move q areturn (Exp.var freturn)
-    | Some areturn, None -> exec_kill q areturn
+    | Some areturn, Some freturn -> Exec.move q areturn (Term.var freturn)
+    | Some areturn, None -> Exec.kill q areturn
     | _ -> q
   in
   let q = Sh.exists (Set.add_list formals (Var.Set.of_option freturn)) q in
@@ -152,8 +169,8 @@ let retn formals freturn {areturn; subst; frame} q =
   [%Trace.retn fun {pf} -> pf "%a" pp]
 
 let resolve_callee lookup ptr q =
-  match Var.of_exp ptr with
-  | Some callee -> (lookup (Var.name callee), q)
+  match Reg.of_exp ptr with
+  | Some callee -> (lookup (Reg.name callee), q)
   | None -> ([], q)
 
 type summary = {xs: Var.Set.t; foot: t; post: t}
@@ -164,16 +181,18 @@ let pp_summary fs {xs; foot; post} =
 
 let create_summary ~locals ~formals ~entry ~current:(post : Sh.t) =
   [%Trace.call fun {pf} ->
-    pf "formals %a@ entry: %a@ current: %a" Var.Set.pp formals pp entry pp
+    pf "formals %a@ entry: %a@ current: %a" Reg.Set.pp formals pp entry pp
       post]
   ;
+  let locals = Var.Set.of_regs locals in
+  let formals = Var.Set.of_regs formals in
   let foot = Sh.exists locals entry in
   let foot, subst = Sh.freshen ~wrt:(Set.union foot.us post.us) foot in
   let restore_formals q =
     Set.fold formals ~init:q ~f:(fun q var ->
-        let var = Exp.var var in
-        let renamed_var = Exp.rename subst var in
-        Sh.and_ (Exp.eq renamed_var var) q )
+        let var = Term.var var in
+        let renamed_var = Term.rename subst var in
+        Sh.and_ (Term.eq renamed_var var) q )
   in
   (* Add back the original formals name *)
   let post = Sh.rename subst post in
@@ -227,11 +246,11 @@ let%test_module _ =
     let n_, wrt = Var.fresh "n" ~wrt
     let b_, wrt = Var.fresh "b" ~wrt
     let end_, _ = Var.fresh "end" ~wrt
-    let a = Exp.var a_
-    let main = Exp.var main_
-    let b = Exp.var b_
-    let n = Exp.var n_
-    let endV = Exp.var end_
+    let a = Term.var a_
+    let main = Term.var main_
+    let b = Term.var b_
+    let n = Term.var n_
+    let endV = Term.var end_
     let seg_main = Sh.seg {loc= main; bas= b; len= n; siz= n; arr= a}
     let seg_a = Sh.seg {loc= a; bas= b; len= n; siz= n; arr= endV}
     let seg_cycle = Sh.seg {loc= a; bas= b; len= n; siz= n; arr= main}
diff --git a/sledge/src/symbheap/sh_domain.mli b/sledge/src/symbheap/sh_domain.mli
index 3f6e03004..9a7260bbf 100644
--- a/sledge/src/symbheap/sh_domain.mli
+++ b/sledge/src/symbheap/sh_domain.mli
@@ -10,10 +10,10 @@
 include Domain_sig.Dom
 
 (* formals should include all the parameters of the summary. That is both
-   formals and globals.*)
+   formals and globals. *)
 val create_summary :
-     locals:Var.Set.t
-  -> formals:Var.Set.t
+     locals:Reg.Set.t
+  -> formals:Reg.Set.t
   -> entry:t
   -> current:t
   -> summary * t
diff --git a/sledge/src/symbheap/sh_test.ml b/sledge/src/symbheap/sh_test.ml
index 3cb8be62d..0e6cab0ca 100644
--- a/sledge/src/symbheap/sh_test.ml
+++ b/sledge/src/symbheap/sh_test.ml
@@ -13,13 +13,13 @@ let%test_module _ =
     let pp = Format.printf "@\n%a@." Sh.pp
     let pp_djn = Format.printf "@\n%a@." Sh.pp_djn
     let ( ~$ ) = Var.Set.of_list
-    let ( ! ) i = Exp.integer (Z.of_int i) Typ.siz
-    let ( = ) = Exp.eq
+    let ( ! ) i = Term.integer (Z.of_int i) Typ.siz
+    let ( = ) = Term.eq
     let wrt = Var.Set.empty
     let x_, wrt = Var.fresh "x" ~wrt
     let y_, _ = Var.fresh "y" ~wrt
-    let x = Exp.var x_
-    let y = Exp.var y_
+    let x = Term.var x_
+    let y = Term.var y_
 
     let%expect_test _ =
       let p = Sh.(exists ~$[x_] (extend_us ~$[x_] emp)) in
diff --git a/sledge/src/symbheap/solver.ml b/sledge/src/symbheap/solver.ml
index 68ecaceb3..b1f0c1cda 100644
--- a/sledge/src/symbheap/solver.ml
+++ b/sledge/src/symbheap/solver.ml
@@ -44,15 +44,15 @@ let fresh_var name vs zs ~wrt =
   let v, wrt = Var.fresh name ~wrt in
   let vs = Set.add vs v in
   let zs = Set.add zs v in
-  let v = Exp.var v in
+  let v = Term.var v in
   (v, vs, zs, wrt)
 
 type occurrences = Zero | One of Var.t | Many
 
-let single_existential_occurrence xs exp =
+let single_existential_occurrence xs term =
   let exception Multiple_existential_occurrences in
   try
-    Exp.fold_vars exp ~init:Zero ~f:(fun seen var ->
+    Term.fold_vars term ~init:Zero ~f:(fun seen var ->
         if not (Set.mem xs var) then seen
         else
           match seen with
@@ -61,32 +61,32 @@ let single_existential_occurrence xs exp =
   with Multiple_existential_occurrences -> Many
 
 let special_cases xs = function
-  | Exp.App {op= App {op= Eq; arg= Var _}; arg= Var _} as e ->
-      if Set.is_subset (Exp.fv e) ~of_:xs then Exp.bool true else e
+  | Term.App {op= App {op= Eq; arg= Var _}; arg= Var _} as e ->
+      if Set.is_subset (Term.fv e) ~of_:xs then Term.bool true else e
   | e -> e
 
-let excise_exp ({us; min; xs} as goal) pure exp =
-  let exp' = Equality.normalize min.cong exp in
-  let exp' = special_cases xs exp' in
-  [%Trace.info "exp': %a" Exp.pp exp'] ;
-  if Exp.is_true exp' then Some ({goal with pgs= true}, pure)
+let excise_term ({us; min; xs} as goal) pure term =
+  let term' = Equality.normalize min.cong term in
+  let term' = special_cases xs term' in
+  [%Trace.info "term': %a" Term.pp term'] ;
+  if Term.is_true term' then Some ({goal with pgs= true}, pure)
   else
-    match single_existential_occurrence xs exp' with
+    match single_existential_occurrence xs term' with
     | Zero -> None
     | One x ->
         Some
           ( { goal with
               us= Set.add us x
-            ; min= Sh.and_ exp' min
+            ; min= Sh.and_ term' min
             ; xs= Set.remove xs x
             ; pgs= true }
           , pure )
-    | Many -> Some (goal, exp' :: pure)
+    | Many -> Some (goal, term' :: pure)
 
 let excise_pure ({sub} as goal) =
   [%Trace.info "@[<2>excise_pure@ %a@]" pp goal] ;
-  List.fold_option sub.pure ~init:(goal, []) ~f:(fun (goal, pure) exp ->
-      excise_exp goal pure exp )
+  List.fold_option sub.pure ~init:(goal, []) ~f:(fun (goal, pure) term ->
+      excise_term goal pure term )
   >>| fun (goal, pure) -> {goal with sub= Sh.with_pure pure sub}
 
 (*   [k; o)
@@ -111,8 +111,8 @@ let excise_seg_same ({com; min; sub} as goal) msg ssg =
   let com = Sh.star (Sh.seg msg) com in
   let min = Sh.rem_seg msg min in
   let sub =
-    Sh.and_ (Exp.eq b b')
-      (Sh.and_ (Exp.eq m m') (Sh.and_ (Exp.eq a a') (Sh.rem_seg ssg sub)))
+    Sh.and_ (Term.eq b b')
+      (Sh.and_ (Term.eq m m') (Sh.and_ (Term.eq a a') (Sh.rem_seg ssg sub)))
   in
   {goal with com; min; sub}
 
@@ -136,24 +136,24 @@ let excise_seg_sub_prefix ({us; com; min; xs; sub; zs} as goal) msg ssg o_n
       msg (Sh.pp_seg_norm sub.cong) ssg pp goal] ;
   let {Sh.loc= k; bas= b; len= m; siz= o; arr= a} = msg in
   let {Sh.bas= b'; len= m'; siz= n; arr= a'} = ssg in
-  let o_n = Exp.integer o_n Typ.siz in
+  let o_n = Term.integer o_n Typ.siz in
   let a0, us, zs, wrt = fresh_var "a0" us zs ~wrt:(Set.union us xs) in
   let a1, us, zs, _ = fresh_var "a1" us zs ~wrt in
   let com = Sh.star (Sh.seg {msg with siz= n; arr= a0}) com in
   let min =
     Sh.and_
-      (Exp.eq
-         (Exp.memory ~siz:o ~arr:a)
-         (Exp.concat
-            [|Exp.memory ~siz:n ~arr:a0; Exp.memory ~siz:o_n ~arr:a1|]))
+      (Term.eq
+         (Term.memory ~siz:o ~arr:a)
+         (Term.concat
+            [|Term.memory ~siz:n ~arr:a0; Term.memory ~siz:o_n ~arr:a1|]))
       (Sh.star
          (Sh.seg
-            {loc= Exp.add Typ.ptr k n; bas= b; len= m; siz= o_n; arr= a1})
+            {loc= Term.add Typ.ptr k n; bas= b; len= m; siz= o_n; arr= a1})
          (Sh.rem_seg msg min))
   in
   let sub =
-    Sh.and_ (Exp.eq b b')
-      (Sh.and_ (Exp.eq m m') (Sh.and_ (Exp.eq a0 a') (Sh.rem_seg ssg sub)))
+    Sh.and_ (Term.eq b b')
+      (Sh.and_ (Term.eq m m') (Sh.and_ (Term.eq a0 a') (Sh.rem_seg ssg sub)))
   in
   {goal with us; com; min; sub; zs}
 
@@ -178,21 +178,22 @@ let excise_seg_min_prefix ({us; com; min; xs; sub; zs} as goal) msg ssg n_o
       msg (Sh.pp_seg_norm sub.cong) ssg pp goal] ;
   let {Sh.bas= b; len= m; siz= o; arr= a} = msg in
   let {Sh.loc= l; bas= b'; len= m'; siz= n; arr= a'} = ssg in
-  let n_o = Exp.integer n_o Typ.siz in
+  let n_o = Term.integer n_o Typ.siz in
   let com = Sh.star (Sh.seg msg) com in
   let min = Sh.rem_seg msg min in
   let a1', xs, zs, _ = fresh_var "a1" xs zs ~wrt:(Set.union us xs) in
   let sub =
-    Sh.and_ (Exp.eq b b')
-      (Sh.and_ (Exp.eq m m')
+    Sh.and_ (Term.eq b b')
+      (Sh.and_ (Term.eq m m')
          (Sh.and_
-            (Exp.eq
-               (Exp.concat
-                  [|Exp.memory ~siz:o ~arr:a; Exp.memory ~siz:n_o ~arr:a1'|])
-               (Exp.memory ~siz:n ~arr:a'))
+            (Term.eq
+               (Term.concat
+                  [| Term.memory ~siz:o ~arr:a
+                   ; Term.memory ~siz:n_o ~arr:a1' |])
+               (Term.memory ~siz:n ~arr:a'))
             (Sh.star
                (Sh.seg
-                  { loc= Exp.add Typ.ptr l o
+                  { loc= Term.add Typ.ptr l o
                   ; bas= b'
                   ; len= m'
                   ; siz= n_o
@@ -221,7 +222,7 @@ let excise_seg_sub_suffix ({us; com; min; xs; sub; zs} as goal) msg ssg l_k
       msg (Sh.pp_seg_norm sub.cong) ssg pp goal] ;
   let {Sh.loc= k; bas= b; len= m; siz= o; arr= a} = msg in
   let {Sh.loc= l; bas= b'; len= m'; siz= n; arr= a'} = ssg in
-  let l_k = Exp.integer l_k Typ.siz in
+  let l_k = Term.integer l_k Typ.siz in
   let a0, us, zs, wrt = fresh_var "a0" us zs ~wrt:(Set.union us xs) in
   let a1, us, zs, _ = fresh_var "a1" us zs ~wrt in
   let com =
@@ -229,17 +230,17 @@ let excise_seg_sub_suffix ({us; com; min; xs; sub; zs} as goal) msg ssg l_k
   in
   let min =
     Sh.and_
-      (Exp.eq
-         (Exp.memory ~siz:o ~arr:a)
-         (Exp.concat
-            [|Exp.memory ~siz:l_k ~arr:a0; Exp.memory ~siz:n ~arr:a1|]))
+      (Term.eq
+         (Term.memory ~siz:o ~arr:a)
+         (Term.concat
+            [|Term.memory ~siz:l_k ~arr:a0; Term.memory ~siz:n ~arr:a1|]))
       (Sh.star
          (Sh.seg {loc= k; bas= b; len= m; siz= l_k; arr= a0})
          (Sh.rem_seg msg min))
   in
   let sub =
-    Sh.and_ (Exp.eq b b')
-      (Sh.and_ (Exp.eq m m') (Sh.and_ (Exp.eq a1 a') (Sh.rem_seg ssg sub)))
+    Sh.and_ (Term.eq b b')
+      (Sh.and_ (Term.eq m m') (Sh.and_ (Term.eq a1 a') (Sh.rem_seg ssg sub)))
   in
   {goal with us; com; min; sub; zs}
 
@@ -264,8 +265,9 @@ let excise_seg_sub_infix ({us; com; min; xs; sub; zs} as goal) msg ssg l_k
       msg (Sh.pp_seg_norm sub.cong) ssg pp goal] ;
   let {Sh.loc= k; bas= b; len= m; siz= o; arr= a} = msg in
   let {Sh.loc= l; bas= b'; len= m'; siz= n; arr= a'} = ssg in
-  let l_k = Exp.integer l_k Typ.siz and ko_ln = Exp.integer ko_ln Typ.siz in
-  let ln = Exp.add Typ.ptr l n in
+  let l_k = Term.integer l_k Typ.siz
+  and ko_ln = Term.integer ko_ln Typ.siz in
+  let ln = Term.add Typ.ptr l n in
   let a0, us, zs, wrt = fresh_var "a0" us zs ~wrt:(Set.union us xs) in
   let a1, us, zs, wrt = fresh_var "a1" us zs ~wrt in
   let a2, us, zs, _ = fresh_var "a2" us zs ~wrt in
@@ -274,12 +276,12 @@ let excise_seg_sub_infix ({us; com; min; xs; sub; zs} as goal) msg ssg l_k
   in
   let min =
     Sh.and_
-      (Exp.eq
-         (Exp.memory ~siz:o ~arr:a)
-         (Exp.concat
-            [| Exp.memory ~siz:l_k ~arr:a0
-             ; Exp.memory ~siz:n ~arr:a1
-             ; Exp.memory ~siz:ko_ln ~arr:a2 |]))
+      (Term.eq
+         (Term.memory ~siz:o ~arr:a)
+         (Term.concat
+            [| Term.memory ~siz:l_k ~arr:a0
+             ; Term.memory ~siz:n ~arr:a1
+             ; Term.memory ~siz:ko_ln ~arr:a2 |]))
       (Sh.star
          (Sh.seg {loc= k; bas= b; len= m; siz= l_k; arr= a0})
          (Sh.star
@@ -287,8 +289,8 @@ let excise_seg_sub_infix ({us; com; min; xs; sub; zs} as goal) msg ssg l_k
             (Sh.rem_seg msg min)))
   in
   let sub =
-    Sh.and_ (Exp.eq b b')
-      (Sh.and_ (Exp.eq m m') (Sh.and_ (Exp.eq a1 a') (Sh.rem_seg ssg sub)))
+    Sh.and_ (Term.eq b b')
+      (Sh.and_ (Term.eq m m') (Sh.and_ (Term.eq a1 a') (Sh.rem_seg ssg sub)))
   in
   {goal with us; com; min; sub; zs}
 
@@ -313,10 +315,10 @@ let excise_seg_min_skew ({us; com; min; xs; sub; zs} as goal) msg ssg l_k
       msg (Sh.pp_seg_norm sub.cong) ssg pp goal] ;
   let {Sh.loc= k; bas= b; len= m; siz= o; arr= a} = msg in
   let {Sh.loc= l; bas= b'; len= m'; siz= n; arr= a'} = ssg in
-  let l_k = Exp.integer l_k Typ.siz in
-  let ko_l = Exp.integer ko_l Typ.siz in
-  let ln_ko = Exp.integer ln_ko Typ.siz in
-  let ko = Exp.add Typ.ptr k o in
+  let l_k = Term.integer l_k Typ.siz in
+  let ko_l = Term.integer ko_l Typ.siz in
+  let ln_ko = Term.integer ln_ko Typ.siz in
+  let ko = Term.add Typ.ptr k o in
   let a0, us, zs, wrt = fresh_var "a0" us zs ~wrt:(Set.union us xs) in
   let a1, us, zs, wrt = fresh_var "a1" us zs ~wrt in
   let a2', xs, zs, _ = fresh_var "a2" xs zs ~wrt in
@@ -325,23 +327,23 @@ let excise_seg_min_skew ({us; com; min; xs; sub; zs} as goal) msg ssg l_k
   in
   let min =
     Sh.and_
-      (Exp.eq
-         (Exp.memory ~siz:o ~arr:a)
-         (Exp.concat
-            [|Exp.memory ~siz:l_k ~arr:a0; Exp.memory ~siz:ko_l ~arr:a1|]))
+      (Term.eq
+         (Term.memory ~siz:o ~arr:a)
+         (Term.concat
+            [|Term.memory ~siz:l_k ~arr:a0; Term.memory ~siz:ko_l ~arr:a1|]))
       (Sh.star
          (Sh.seg {loc= k; bas= b; len= m; siz= l_k; arr= a0})
          (Sh.rem_seg msg min))
   in
   let sub =
-    Sh.and_ (Exp.eq b b')
-      (Sh.and_ (Exp.eq m m')
+    Sh.and_ (Term.eq b b')
+      (Sh.and_ (Term.eq m m')
          (Sh.and_
-            (Exp.eq
-               (Exp.concat
-                  [| Exp.memory ~siz:ko_l ~arr:a1
-                   ; Exp.memory ~siz:ln_ko ~arr:a2' |])
-               (Exp.memory ~siz:n ~arr:a'))
+            (Term.eq
+               (Term.concat
+                  [| Term.memory ~siz:ko_l ~arr:a1
+                   ; Term.memory ~siz:ln_ko ~arr:a2' |])
+               (Term.memory ~siz:n ~arr:a'))
             (Sh.star
                (Sh.seg {loc= ko; bas= b'; len= m'; siz= ln_ko; arr= a2'})
                (Sh.rem_seg ssg sub))))
@@ -369,18 +371,19 @@ let excise_seg_min_suffix ({us; com; min; xs; sub; zs} as goal) msg ssg k_l
       msg (Sh.pp_seg_norm sub.cong) ssg pp goal] ;
   let {Sh.bas= b; len= m; siz= o; arr= a} = msg in
   let {Sh.loc= l; bas= b'; len= m'; siz= n; arr= a'} = ssg in
-  let k_l = Exp.integer k_l Typ.siz in
+  let k_l = Term.integer k_l Typ.siz in
   let a0', xs, zs, _ = fresh_var "a0" xs zs ~wrt:(Set.union us xs) in
   let com = Sh.star (Sh.seg msg) com in
   let min = Sh.rem_seg msg min in
   let sub =
-    Sh.and_ (Exp.eq b b')
-      (Sh.and_ (Exp.eq m m')
+    Sh.and_ (Term.eq b b')
+      (Sh.and_ (Term.eq m m')
          (Sh.and_
-            (Exp.eq
-               (Exp.concat
-                  [|Exp.memory ~siz:k_l ~arr:a0'; Exp.memory ~siz:o ~arr:a|])
-               (Exp.memory ~siz:n ~arr:a'))
+            (Term.eq
+               (Term.concat
+                  [| Term.memory ~siz:k_l ~arr:a0'
+                   ; Term.memory ~siz:o ~arr:a |])
+               (Term.memory ~siz:n ~arr:a'))
             (Sh.star
                (Sh.seg {loc= l; bas= b'; len= m'; siz= k_l; arr= a0'})
                (Sh.rem_seg ssg sub))))
@@ -409,23 +412,23 @@ let excise_seg_min_infix ({us; com; min; xs; sub; zs} as goal) msg ssg k_l
       msg (Sh.pp_seg_norm sub.cong) ssg pp goal] ;
   let {Sh.loc= k; bas= b; len= m; siz= o; arr= a} = msg in
   let {Sh.loc= l; bas= b'; len= m'; siz= n; arr= a'} = ssg in
-  let k_l = Exp.integer k_l Typ.siz in
-  let ln_ko = Exp.integer ln_ko Typ.siz in
-  let ko = Exp.add Typ.ptr k o in
+  let k_l = Term.integer k_l Typ.siz in
+  let ln_ko = Term.integer ln_ko Typ.siz in
+  let ko = Term.add Typ.ptr k o in
   let a0', xs, zs, wrt = fresh_var "a0" xs zs ~wrt:(Set.union us xs) in
   let a2', xs, zs, _ = fresh_var "a2" xs zs ~wrt in
   let com = Sh.star (Sh.seg msg) com in
   let min = Sh.rem_seg msg min in
   let sub =
-    Sh.and_ (Exp.eq b b')
-      (Sh.and_ (Exp.eq m m')
+    Sh.and_ (Term.eq b b')
+      (Sh.and_ (Term.eq m m')
          (Sh.and_
-            (Exp.eq
-               (Exp.concat
-                  [| Exp.memory ~siz:k_l ~arr:a0'
-                   ; Exp.memory ~siz:o ~arr:a
-                   ; Exp.memory ~siz:ln_ko ~arr:a2' |])
-               (Exp.memory ~siz:n ~arr:a'))
+            (Term.eq
+               (Term.concat
+                  [| Term.memory ~siz:k_l ~arr:a0'
+                   ; Term.memory ~siz:o ~arr:a
+                   ; Term.memory ~siz:ln_ko ~arr:a2' |])
+               (Term.memory ~siz:n ~arr:a'))
             (Sh.star
                (Sh.seg {loc= l; bas= b'; len= m'; siz= k_l; arr= a0'})
                (Sh.star
@@ -455,10 +458,10 @@ let excise_seg_sub_skew ({us; com; min; xs; sub; zs} as goal) msg ssg k_l
       msg (Sh.pp_seg_norm sub.cong) ssg pp goal] ;
   let {Sh.loc= k; bas= b; len= m; siz= o; arr= a} = msg in
   let {Sh.loc= l; bas= b'; len= m'; siz= n; arr= a'} = ssg in
-  let k_l = Exp.integer k_l Typ.siz in
-  let ln_k = Exp.integer ln_k Typ.siz in
-  let ko_ln = Exp.integer ko_ln Typ.siz in
-  let ln = Exp.add Typ.ptr l n in
+  let k_l = Term.integer k_l Typ.siz in
+  let ln_k = Term.integer ln_k Typ.siz in
+  let ko_ln = Term.integer ko_ln Typ.siz in
+  let ln = Term.add Typ.ptr l n in
   let a0', xs, zs, wrt = fresh_var "a0" xs zs ~wrt:(Set.union us xs) in
   let a1, us, zs, wrt = fresh_var "a1" us zs ~wrt in
   let a2, us, zs, _ = fresh_var "a2" us zs ~wrt in
@@ -467,23 +470,23 @@ let excise_seg_sub_skew ({us; com; min; xs; sub; zs} as goal) msg ssg k_l
   in
   let min =
     Sh.and_
-      (Exp.eq
-         (Exp.memory ~siz:o ~arr:a)
-         (Exp.concat
-            [|Exp.memory ~siz:ln_k ~arr:a1; Exp.memory ~siz:ko_ln ~arr:a2|]))
+      (Term.eq
+         (Term.memory ~siz:o ~arr:a)
+         (Term.concat
+            [|Term.memory ~siz:ln_k ~arr:a1; Term.memory ~siz:ko_ln ~arr:a2|]))
       (Sh.star
          (Sh.seg {loc= ln; bas= b; len= m; siz= ko_ln; arr= a2})
          (Sh.rem_seg msg min))
   in
   let sub =
-    Sh.and_ (Exp.eq b b')
-      (Sh.and_ (Exp.eq m m')
+    Sh.and_ (Term.eq b b')
+      (Sh.and_ (Term.eq m m')
          (Sh.and_
-            (Exp.eq
-               (Exp.concat
-                  [| Exp.memory ~siz:k_l ~arr:a0'
-                   ; Exp.memory ~siz:ln_k ~arr:a1 |])
-               (Exp.memory ~siz:n ~arr:a'))
+            (Term.eq
+               (Term.concat
+                  [| Term.memory ~siz:k_l ~arr:a0'
+                   ; Term.memory ~siz:ln_k ~arr:a1 |])
+               (Term.memory ~siz:n ~arr:a'))
             (Sh.star
                (Sh.seg {loc= l; bas= b'; len= m'; siz= k_l; arr= a0'})
                (Sh.rem_seg ssg sub))))
@@ -504,13 +507,14 @@ let excise_seg ({sub} as goal) msg ssg =
     || not (Equality.entails_eq sub.cong m m')
   then
     Some
-      {goal with sub= Sh.and_ (Exp.eq b b') (Sh.and_ (Exp.eq m m') goal.sub)}
+      { goal with
+        sub= Sh.and_ (Term.eq b b') (Sh.and_ (Term.eq m m') goal.sub) }
   else
     match[@warning "-p"] Z.sign k_l with
     (* k-l < 0 so k < l *)
     | -1 -> (
-        let ko = Exp.add Typ.ptr k o in
-        let ln = Exp.add Typ.ptr l n in
+        let ko = Term.add Typ.ptr k o in
+        let ln = Term.add Typ.ptr l n in
         Equality.difference sub.cong ko ln
         >>= fun ko_ln ->
         match[@warning "-p"] Z.sign ko_ln with
@@ -535,7 +539,7 @@ let excise_seg ({sub} as goal) msg ssg =
     (* k-l = 0 so k = l *)
     | 0 -> (
       match Equality.difference sub.cong o n with
-      | None -> Some {goal with sub= Sh.and_ (Exp.eq o n) goal.sub}
+      | None -> Some {goal with sub= Sh.and_ (Term.eq o n) goal.sub}
       | Some o_n -> (
         match[@warning "-p"] Z.sign o_n with
         (* o-n < 0      [k; o)
@@ -549,8 +553,8 @@ let excise_seg ({sub} as goal) msg ssg =
         | 1 -> Some (excise_seg_sub_prefix goal msg ssg o_n) ) )
     (* k-l > 0 so k > l *)
     | 1 -> (
-        let ko = Exp.add Typ.ptr k o in
-        let ln = Exp.add Typ.ptr l n in
+        let ko = Term.add Typ.ptr k o in
+        let ln = Term.add Typ.ptr l n in
         Equality.difference sub.cong ko ln
         >>= fun ko_ln ->
         match[@warning "-p"] Z.sign ko_ln with
diff --git a/sledge/src/symbheap/solver_test.ml b/sledge/src/symbheap/solver_test.ml
index e68c71260..ce488ceef 100644
--- a/sledge/src/symbheap/solver_test.ml
+++ b/sledge/src/symbheap/solver_test.ml
@@ -22,10 +22,10 @@ let%test_module _ =
       Solver.infer_frame p (Var.Set.of_list xs) q
       |> fun r -> assert (Option.is_some r)
 
-    let ( ! ) i = Exp.integer (Z.of_int i) Typ.siz
-    let ( + ) = Exp.add Typ.ptr
-    let ( - ) = Exp.sub Typ.siz
-    let ( * ) = Exp.mul Typ.siz
+    let ( ! ) i = Term.integer (Z.of_int i) Typ.siz
+    let ( + ) = Term.add Typ.ptr
+    let ( - ) = Term.sub Typ.siz
+    let ( * ) = Term.mul Typ.siz
     let wrt = Var.Set.empty
     let a_, wrt = Var.fresh "a" ~wrt
     let a2_, wrt = Var.fresh "a" ~wrt
@@ -36,15 +36,15 @@ let%test_module _ =
     let l2_, wrt = Var.fresh "l" ~wrt
     let m_, wrt = Var.fresh "m" ~wrt
     let n_, _ = Var.fresh "n" ~wrt
-    let a = Exp.var a_
-    let a2 = Exp.var a2_
-    let a3 = Exp.var a3_
-    let b = Exp.var b_
-    let k = Exp.var k_
-    let l = Exp.var l_
-    let l2 = Exp.var l2_
-    let m = Exp.var m_
-    let n = Exp.var n_
+    let a = Term.var a_
+    let a2 = Term.var a2_
+    let a3 = Term.var a3_
+    let b = Term.var b_
+    let k = Term.var k_
+    let l = Term.var l_
+    let l2 = Term.var l2_
+    let m = Term.var m_
+    let n = Term.var n_
 
     let%expect_test _ =
       check_frame Sh.emp [] Sh.emp ;
@@ -61,7 +61,7 @@ let%test_module _ =
         ) infer_frame:   false |}]
 
     let%expect_test _ =
-      check_frame Sh.emp [n_; m_] (Sh.and_ (Exp.eq m n) Sh.emp) ;
+      check_frame Sh.emp [n_; m_] (Sh.and_ (Term.eq m n) Sh.emp) ;
       [%expect
         {|
         ( infer_frame:   emp \- ∃ %m_8, %n_9 .   %m_8 = %n_9 ∧ emp
@@ -93,7 +93,7 @@ let%test_module _ =
       let seg1 = Sh.seg {loc= l; bas= b; len= !10; siz= !10; arr= a} in
       let minued = Sh.star common seg1 in
       let subtrahend =
-        Sh.and_ (Exp.eq m n)
+        Sh.and_ (Term.eq m n)
           (Sh.exists
              (Var.Set.of_list [m_])
              (Sh.extend_us (Var.Set.of_list [m_]) common))
@@ -235,7 +235,7 @@ let%test_module _ =
     let%expect_test _ =
       check_frame
         (Sh.and_
-           Exp.(or_ (or_ (eq n !0) (eq n !1)) (eq n !2))
+           Term.(or_ (or_ (eq n !0) (eq n !1)) (eq n !2))
            seg_split_symbolically)
         [m_; a_]
         (Sh.seg {loc= l; bas= l; len= m; siz= m; arr= a}) ;
@@ -272,7 +272,7 @@ let%test_module _ =
     (* Incompleteness: equivalent to above but using ≤ instead of ∨ *)
     let%expect_test _ =
       infer_frame
-        (Sh.and_ (Exp.le n !2) seg_split_symbolically)
+        (Sh.and_ (Term.le n !2) seg_split_symbolically)
         [m_; a_]
         (Sh.seg {loc= l; bas= l; len= m; siz= m; arr= a}) ;
       [%expect
diff --git a/sledge/src/symbheap/term.ml b/sledge/src/symbheap/term.ml
new file mode 100644
index 000000000..9a699550e
--- /dev/null
+++ b/sledge/src/symbheap/term.ml
@@ -0,0 +1,1465 @@
+(*
+ * 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 *)
+
+(** Z wrapped to treat bounded and unsigned operations *)
+module Z = struct
+  include Z
+
+  (** Interpret as a bounded integer with specified signedness and width. *)
+  let clamp ~signed bits z =
+    if signed then Z.signed_extract z 0 bits else Z.extract z 0 bits
+
+  let clamp_cmp ~signed bits op x y =
+    op (clamp ~signed bits x) (clamp ~signed bits y)
+
+  let clamp_bop ~signed bits op x y =
+    clamp ~signed bits (op (clamp ~signed bits x) (clamp ~signed bits y))
+
+  let beq ~bits x y = clamp_cmp ~signed:true bits Z.equal x y
+  let bleq ~bits x y = clamp_cmp ~signed:true bits Z.leq x y
+  let bgeq ~bits x y = clamp_cmp ~signed:true bits Z.geq x y
+  let blt ~bits x y = clamp_cmp ~signed:true bits Z.lt x y
+  let bgt ~bits x y = clamp_cmp ~signed:true bits Z.gt x y
+  let buleq ~bits x y = clamp_cmp ~signed:false bits Z.leq x y
+  let bugeq ~bits x y = clamp_cmp ~signed:false bits Z.geq x y
+  let bult ~bits x y = clamp_cmp ~signed:false bits Z.lt x y
+  let bugt ~bits x y = clamp_cmp ~signed:false bits Z.gt x y
+  let bsub ~bits x y = clamp_bop ~signed:true bits Z.sub x y
+  let bmul ~bits x y = clamp_bop ~signed:true bits Z.mul x y
+  let bdiv ~bits x y = clamp_bop ~signed:true bits Z.div x y
+  let brem ~bits x y = clamp_bop ~signed:true bits Z.rem x y
+  let budiv ~bits x y = clamp_bop ~signed:false bits Z.div x y
+  let burem ~bits x y = clamp_bop ~signed:false bits Z.rem x y
+  let blogand ~bits x y = clamp_bop ~signed:true bits Z.logand x y
+  let blogor ~bits x y = clamp_bop ~signed:true bits Z.logor x y
+  let blogxor ~bits x y = clamp_bop ~signed:true bits Z.logxor x y
+  let bshift_left ~bits z i = Z.shift_left (clamp bits ~signed:true z) i
+  let bshift_right ~bits z i = Z.shift_right (clamp bits ~signed:true z) i
+
+  let bshift_right_trunc ~bits z i =
+    Z.shift_right_trunc (clamp bits ~signed:true z) i
+end
+
+module rec T : sig
+  type qset = Qset.M(T).t [@@deriving compare, equal, hash, sexp]
+
+  type t =
+    (* nary: arithmetic, numeric and pointer *)
+    | Add of {args: qset; typ: Typ.t}
+    | Mul of {args: qset; typ: Typ.t}
+    (* pointer and memory constants and operations *)
+    | Splat of {byt: t; siz: t}
+    | Memory of {siz: t; arr: t}
+    | Concat of {args: t vector}
+    (* nullary *)
+    | Var of {id: int; name: string}
+    | Nondet of {msg: string}
+    | Label of {parent: string; name: string}
+    (* curried application *)
+    | App of {op: t; arg: t}
+    (* binary: comparison *)
+    | Eq
+    | Dq
+    | Gt
+    | Ge
+    | Lt
+    | Le
+    | Ugt
+    | Uge
+    | Ult
+    | Ule
+    | Ord
+    | Uno
+    (* binary: arithmetic, numeric and pointer *)
+    | Div
+    | Udiv
+    | Rem
+    | Urem
+    (* binary: boolean / bitwise *)
+    | And
+    | Or
+    | Xor
+    | Shl
+    | Lshr
+    | Ashr
+    (* ternary: conditional *)
+    | Conditional
+    (* array/struct constants and operations *)
+    | Record
+    | Select
+    | Update
+    | Struct_rec of {elts: t vector}  (** NOTE: may be cyclic *)
+    (* unary: conversion *)
+    | Convert of {signed: bool; dst: Typ.t; src: Typ.t}
+    (* numeric constants *)
+    | Integer of {data: Z.t; typ: Typ.t}
+    | Float of {data: string}
+  [@@deriving compare, equal, hash, sexp]
+
+  (* Note: solve (and invariant) requires Qset.min_elt to return a
+     non-coefficient, so Integer terms must compare higher than any valid
+     monomial *)
+
+  type comparator_witness
+
+  val comparator : (t, comparator_witness) Comparator.t
+end = struct
+  include T0 include Comparator.Make (T0)
+end
+
+(* auxiliary definition for safe recursive module initialization *)
+and T0 : sig
+  type qset = Qset.M(T).t [@@deriving compare, equal, hash, sexp]
+
+  type t =
+    | Add of {args: qset; typ: Typ.t}
+    | Mul of {args: qset; typ: Typ.t}
+    | Splat of {byt: t; siz: t}
+    | Memory of {siz: t; arr: t}
+    | Concat of {args: t vector}
+    | Var of {id: int; name: string}
+    | Nondet of {msg: string}
+    | Label of {parent: string; name: string}
+    | App of {op: t; arg: t}
+    | Eq
+    | Dq
+    | Gt
+    | Ge
+    | Lt
+    | Le
+    | Ugt
+    | Uge
+    | Ult
+    | Ule
+    | Ord
+    | Uno
+    | Div
+    | Udiv
+    | Rem
+    | Urem
+    | And
+    | Or
+    | Xor
+    | Shl
+    | Lshr
+    | Ashr
+    | Conditional
+    | Record
+    | Select
+    | Update
+    | Struct_rec of {elts: t vector}
+    | Convert of {signed: bool; dst: Typ.t; src: Typ.t}
+    | Integer of {data: Z.t; typ: Typ.t}
+    | Float of {data: string}
+  [@@deriving compare, equal, hash, sexp]
+end = struct
+  type qset = Qset.M(T).t [@@deriving compare, equal, hash, sexp]
+
+  type t =
+    | Add of {args: qset; typ: Typ.t}
+    | Mul of {args: qset; typ: Typ.t}
+    | Splat of {byt: t; siz: t}
+    | Memory of {siz: t; arr: t}
+    | Concat of {args: t vector}
+    | Var of {id: int; name: string}
+    | Nondet of {msg: string}
+    | Label of {parent: string; name: string}
+    | App of {op: t; arg: t}
+    | Eq
+    | Dq
+    | Gt
+    | Ge
+    | Lt
+    | Le
+    | Ugt
+    | Uge
+    | Ult
+    | Ule
+    | Ord
+    | Uno
+    | Div
+    | Udiv
+    | Rem
+    | Urem
+    | And
+    | Or
+    | Xor
+    | Shl
+    | Lshr
+    | Ashr
+    | Conditional
+    | Record
+    | Select
+    | Update
+    | Struct_rec of {elts: t vector}
+    | Convert of {signed: bool; dst: Typ.t; src: Typ.t}
+    | Integer of {data: Z.t; typ: Typ.t}
+    | Float of {data: string}
+  [@@deriving compare, equal, hash, sexp]
+end
+
+(* suppress spurious "Warning 60: unused module T0." *)
+type _t = T0.t
+
+include T
+
+let empty_map = Map.empty (module T)
+let empty_qset = Qset.empty (module T)
+
+let fix (f : (t -> 'a as 'f) -> 'f) (bot : 'f) (e : t) : 'a =
+  let rec fix_f seen e =
+    match e with
+    | Struct_rec _ ->
+        if List.mem ~equal:( == ) seen e then f bot e
+        else f (fix_f (e :: seen)) e
+    | _ -> f (fix_f seen) e
+  in
+  let rec fix_f_seen_nil e =
+    match e with Struct_rec _ -> f (fix_f [e]) e | _ -> f fix_f_seen_nil e
+  in
+  fix_f_seen_nil e
+
+let fix_flip (f : ('z -> t -> 'a as 'f) -> 'f) (bot : 'f) (z : 'z) (e : t) =
+  fix (fun f' e z -> f (fun z e -> f' e z) z e) (fun e z -> bot z e) e z
+
+let uncurry =
+  let rec uncurry_ acc_args = function
+    | App {op; arg} -> uncurry_ (arg :: acc_args) op
+    | op -> (op, acc_args)
+  in
+  uncurry_ []
+
+let rec pp ?is_x fs term =
+  let get_var_style var =
+    match is_x with
+    | None -> `None
+    | Some is_x -> if not (is_x var) then `Bold else `Cyan
+  in
+  let pp_ 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 {name; id= 0} as var ->
+        Trace.pp_styled (get_var_style var) "%%%s" fs name
+    | Var {name; id} as var ->
+        Trace.pp_styled (get_var_style var) "%%%s_%d" fs name id
+    | Nondet {msg} -> pf "nondet \"%s\"" msg
+    | Label {name} -> pf "%s" name
+    | Integer {data; typ= Pointer _} when Z.equal Z.zero data -> pf "null"
+    | Splat {byt; siz} -> pf "%a^%a" pp byt pp siz
+    | Memory {siz; arr} -> pf "@<1>⟨%a,%a@<1>⟩" pp siz pp arr
+    | Concat {args} -> pf "%a" (Vector.pp "@,^" pp) args
+    | Integer {data} -> Trace.pp_styled `Magenta "%a" fs Z.pp data
+    | Float {data} -> pf "%s" data
+    | Eq -> pf "="
+    | Dq -> pf "@<1>≠"
+    | Gt -> pf ">"
+    | Ge -> pf "@<1>≥"
+    | Lt -> pf "<"
+    | Le -> pf "@<1>≤"
+    | Ugt -> pf "u>"
+    | Uge -> pf "@<2>u≥"
+    | Ult -> pf "u<"
+    | Ule -> pf "@<2>u≤"
+    | Ord -> pf "ord"
+    | Uno -> pf "uno"
+    | 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
+    | Div -> pf "/"
+    | Udiv -> pf "udiv"
+    | Rem -> pf "rem"
+    | Urem -> pf "urem"
+    | And -> pf "&&"
+    | Or -> pf "||"
+    | Xor -> pf "xor"
+    | App
+        {op= App {op= Xor; arg}; arg= Integer {data; typ= Integer {bits= 1}}}
+      when Z.is_true data ->
+        pf "¬%a" pp arg
+    | App
+        {op= App {op= Xor; arg= Integer {data; typ= Integer {bits= 1}}}; arg}
+      when Z.is_true data ->
+        pf "¬%a" pp arg
+    | Shl -> pf "shl"
+    | Lshr -> pf "lshr"
+    | Ashr -> pf "ashr"
+    | Conditional -> pf "(_?_:_)"
+    | App {op= Conditional; arg= cnd} -> pf "(%a@ ? _:_)" pp cnd
+    | App {op= App {op= Conditional; arg= cnd}; arg= thn} ->
+        pf "(%a@ ? %a@ : _)" pp cnd pp thn
+    | App {op= App {op= App {op= Conditional; arg= cnd}; arg= thn}; arg= els}
+      ->
+        pf "(%a@ ? %a@ : %a)" pp cnd pp thn pp els
+    | Select -> pf "_[_]"
+    | App {op= Select; arg= rcd} -> pf "%a[_]" pp rcd
+    | App {op= App {op= Select; arg= rcd}; arg= idx} ->
+        pf "%a[%a]" pp rcd pp idx
+    | Update -> pf "[_|_→_]"
+    | App {op= Update; arg= rcd} -> pf "[%a@ @[| _→_@]]" pp rcd
+    | App {op= App {op= Update; arg= rcd}; arg= elt} ->
+        pf "[%a@ @[| _→ %a@]]" pp rcd pp elt
+    | App {op= App {op= App {op= Update; arg= rcd}; arg= elt}; arg= idx} ->
+        pf "[%a@ @[| %a → %a@]]" pp rcd pp idx pp elt
+    | Record -> pf "{_}"
+    | App {op; arg} -> (
+      match uncurry term with
+      | Record, elts -> pf "{%a}" pp_record elts
+      | op, [x; y] -> pf "(%a@ %a %a)" pp x pp op pp y
+      | _ -> pf "(%a@ %a)" pp op pp arg )
+    | Struct_rec {elts} -> pf "{|%a|}" (Vector.pp ",@ " pp) elts
+    | Convert {dst; src} -> pf "(%a)(%a)" Typ.pp dst Typ.pp src
+  in
+  fix_flip pp_ (fun _ _ -> ()) fs term
+
+and pp_record fs elts =
+  [%Trace.fprintf
+    fs "%a"
+      (fun fs elts ->
+        let elta = Array.of_list elts in
+        match
+          String.init (Array.length elta) ~f:(fun i ->
+              match elta.(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@]" (List.pp ",@ " pp) elts )
+      elts]
+
+type term = t
+
+let pp_t = pp ?is_x:None
+let pp_full = pp
+let pp = pp_t
+
+(** Invariant *)
+
+let rec typ_of = function
+  | Add {typ} | Mul {typ} | Integer {typ} | App {op= Convert {dst= typ}} ->
+      Some typ
+  | App {op= App {op= Eq | Dq | Gt | Ge | Lt | Le | Ugt | Uge | Ult | Ule}}
+    ->
+      Some Typ.bool
+  | App
+      { op=
+          App
+            { op=
+                Div | Udiv | Rem | Urem | And | Or | Xor | Shl | Lshr | Ashr
+            ; arg= x }
+      ; arg= y } -> (
+    match typ_of x with Some _ as t -> t | None -> typ_of y )
+  | App {op= App {op= App {op= Conditional}; arg= thn}; arg= els} -> (
+    match typ_of thn with Some _ as t -> t | None -> typ_of els )
+  | _ -> None
+
+let typ = typ_of
+
+let type_check e typ =
+  assert (
+    Option.for_all ~f:(Typ.castable typ) (typ_of e)
+    || fail "%a@ : %a not <:@ %a" pp e Typ.pp
+         (Option.value_exn (typ_of e))
+         Typ.pp typ )
+
+let type_check2 e f typ = type_check e typ ; type_check f typ
+
+(* an indeterminate (factor of a monomial) is any non-Add/Mul/Integer term *)
+let rec assert_indeterminate = function
+  | App {op} -> assert_indeterminate op
+  | Integer _ | 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 add_typ mono =
+  match mono with
+  | Mul {typ; args} ->
+      assert (Typ.castable add_typ typ) ;
+      assert (Option.is_some (Typ.prim_bit_size_of typ)) ;
+      Qset.iter args ~f:(fun factor exponent ->
+          assert (Q.sign exponent > 0) ;
+          assert_indeterminate factor |> Fn.id )
+  | _ -> assert_indeterminate mono |> Fn.id
+
+(* a polynomial term is a monomial multiplied by a non-zero coefficient
+ *     c × ∏ᵢ xᵢ
+ *)
+let assert_poly_term add_typ mono coeff =
+  assert (not (Q.equal Q.zero coeff)) ;
+  match mono with
+  | Integer {data} -> assert (Z.equal Z.one data)
+  | Mul {args} ->
+      ( match Qset.min_elt args with
+      | None | Some (Integer _, _) -> assert false
+      | Some (_, n) -> assert (Qset.length args > 1 || not (Q.equal Q.one n))
+      ) ;
+      assert_monomial add_typ mono |> Fn.id
+  | _ -> assert_monomial add_typ mono |> Fn.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 {typ; args} ->
+      ( match Qset.min_elt args with
+      | None -> assert false
+      | Some (Integer _, _) -> 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 typ m c |> Fn.id)
+  | _ -> assert false
+
+let invariant ?(partial = false) e =
+  Invariant.invariant [%here] e [%sexp_of: t]
+  @@ fun () ->
+  let op, args = uncurry e in
+  let assert_arity arity =
+    let nargs = List.length args in
+    assert (nargs = arity || (partial && nargs < arity))
+  in
+  match op with
+  | App _ -> fail "uncurry cannot return App" ()
+  | Integer {data; typ= (Integer _ | Pointer _) as typ} -> (
+    match Typ.prim_bit_size_of typ with
+    | None -> assert false
+    | Some bits ->
+        assert_arity 0 ;
+        assert (Z.numbits data <= bits) )
+  | Integer _ -> assert false
+  | Var _ | Nondet _ | Label _ | Float _ -> assert_arity 0
+  | Convert {dst; src} ->
+      ( match args with
+      | [Integer {typ= Integer _ as typ}] -> assert (Typ.equal src typ)
+      | [arg] ->
+          assert (Option.for_all ~f:(Typ.convertible src) (typ_of arg))
+      | _ -> assert_arity 1 ) ;
+      assert (Typ.convertible src dst)
+  | Add _ -> assert_polynomial e |> Fn.id
+  | Mul {typ} -> assert_monomial typ e |> Fn.id
+  | Eq | Dq | Gt | Ge | Lt | Le | Ugt | Uge | Ult | Ule | Div | Udiv | Rem
+   |Urem | And | Or | Xor | Shl | Lshr | Ashr -> (
+    match args with
+    | [x; y] -> (
+      match (typ_of x, typ_of y) with
+      | Some typ, Some typ' -> assert (Typ.castable typ typ')
+      | _ -> assert true )
+    | _ -> assert_arity 2 )
+  | Concat {args} -> assert (Vector.length args <> 1)
+  | Splat {byt; siz} -> (
+      assert (Option.exists ~f:(Typ.convertible Typ.byt) (typ_of byt)) ;
+      assert (Option.exists ~f:(Typ.convertible Typ.siz) (typ_of siz)) ;
+      match siz with
+      | Integer {data} -> assert (not (Z.equal Z.zero data))
+      | _ -> () )
+  | Memory {siz} ->
+      assert (Option.for_all ~f:(Typ.convertible Typ.siz) (typ_of siz))
+  | Ord | Uno | Select -> assert_arity 2
+  | Conditional | Update -> assert_arity 3
+  | Record -> assert (partial || not (List.is_empty args))
+  | Struct_rec {elts} ->
+      assert (not (Vector.is_empty elts)) ;
+      assert_arity 0
+
+let bits_of_int term =
+  match term with
+  | Integer {typ} -> (
+    match Typ.prim_bit_size_of typ with
+    | Some bits -> bits
+    | None -> violates invariant term )
+  | _ -> fail "bits_of_int" ()
+
+(** Variables are the terms constructed by [Var] *)
+module Var = struct
+  include T
+
+  let pp = pp
+
+  type var = t
+
+  let of_reg (r : Reg.t) =
+    match (r :> Exp.t) with
+    | Reg {id; name} -> Var {id; name}
+    | _ -> violates Reg.invariant r
+
+  module Set = struct
+    include (
+      Set :
+        module type of Set with type ('elt, 'cmp) t := ('elt, 'cmp) Set.t )
+
+    type t = Set.M(T).t [@@deriving compare, equal, sexp]
+
+    let pp_full ?is_x vs = Set.pp (pp_full ?is_x) vs
+    let pp = pp_full ?is_x:None
+    let empty = Set.empty (module T)
+    let of_option = Option.fold ~f:Set.add ~init:empty
+    let of_list = Set.of_list (module T)
+    let of_vector = Set.of_vector (module T)
+    let of_regs = Set.fold ~init:empty ~f:(fun s r -> add s (of_reg r))
+  end
+
+  module Map = struct
+    include (
+      Map :
+        module type of Map
+        with type ('key, 'value, 'cmp) t := ('key, 'value, 'cmp) Map.t )
+
+    type 'v t = 'v Map.M(T).t [@@deriving compare, equal, sexp]
+
+    let empty = Map.empty (module T)
+  end
+
+  let demangle =
+    let open Ctypes in
+    let cxa_demangle =
+      (* char *__cxa_demangle(const char *, char *, size_t *, int * ) *)
+      Foreign.foreign "__cxa_demangle"
+        ( string @-> ptr char @-> ptr size_t @-> ptr int
+        @-> returning string_opt )
+    in
+    let null_ptr_char = from_voidp char null in
+    let null_ptr_size_t = from_voidp size_t null in
+    let status = allocate int 0 in
+    fun mangled ->
+      let demangled =
+        cxa_demangle mangled null_ptr_char null_ptr_size_t status
+      in
+      if !@status = 0 then demangled else None
+
+  let pp_demangled fs = function
+    | Var {name} -> (
+      match demangle name with
+      | Some demangled when not (String.equal name demangled) ->
+          Format.fprintf fs "“%s”" demangled
+      | _ -> () )
+    | _ -> ()
+
+  let invariant x =
+    Invariant.invariant [%here] x [%sexp_of: t]
+    @@ fun () -> match x with Var _ -> invariant x | _ -> assert false
+
+  let id = function Var {id} -> id | x -> violates invariant x
+  let name = function Var {name} -> name | x -> violates invariant x
+
+  let of_term = function
+    | Var _ as v -> Some (v |> check invariant)
+    | _ -> None
+
+  let program name = Var {id= 0; name} |> check invariant
+
+  let fresh name ~(wrt : Set.t) =
+    let max = match Set.max_elt wrt with None -> 0 | Some max -> id max in
+    let x' = Var {name; id= max + 1} in
+    (x', Set.add wrt x')
+
+  (** Variable renaming substitutions *)
+  module Subst = struct
+    type t = T.t Map.M(T).t [@@deriving compare, equal, sexp]
+
+    let invariant s =
+      Invariant.invariant [%here] s [%sexp_of: t]
+      @@ fun () ->
+      let domain, range =
+        Map.fold s ~init:(Set.empty, Set.empty)
+          ~f:(fun ~key ~data (domain, range) ->
+            assert (not (Set.mem range data)) ;
+            (Set.add domain key, Set.add range data) )
+      in
+      assert (Set.disjoint domain range)
+
+    let pp fs s =
+      Format.fprintf fs "@[<1>[%a]@]"
+        (List.pp ",@ " (fun fs (k, v) ->
+             Format.fprintf fs "@[[%a ↦ %a]@]" pp_t k pp_t v ))
+        (Map.to_alist s)
+
+    let empty = empty_map
+    let is_empty = Map.is_empty
+
+    let freshen vs ~wrt =
+      let xs = Set.inter wrt vs in
+      let wrt = Set.union wrt vs in
+      Set.fold xs ~init:(empty, wrt) ~f:(fun (sub, wrt) x ->
+          let x', wrt = fresh (name x) ~wrt in
+          let sub = Map.add_exn sub ~key:x ~data:x' in
+          (sub, wrt) )
+      |> fst |> check invariant
+
+    let extend sub ~replace ~with_ =
+      ( match Map.add sub ~key:replace ~data:with_ with
+      | `Duplicate -> sub
+      | `Ok sub ->
+          Map.map_preserving_phys_equal sub ~f:(fun v ->
+              if T.equal v replace then with_ else v ) )
+      |> check invariant
+
+    let invert sub =
+      Map.fold sub ~init:empty ~f:(fun ~key ~data sub' ->
+          Map.add_exn sub' ~key:data ~data:key )
+      |> check invariant
+
+    let exclude sub vs =
+      Set.fold vs ~init:sub ~f:Map.remove |> check invariant
+
+    let restrict sub vs =
+      Map.filter_keys ~f:(Set.mem vs) sub |> check invariant
+
+    let domain sub =
+      Map.fold sub ~init:Set.empty ~f:(fun ~key ~data:_ domain ->
+          Set.add domain key )
+
+    let range sub =
+      Map.fold sub ~init:Set.empty ~f:(fun ~key:_ ~data range ->
+          Set.add range data )
+
+    let apply sub v = try Map.find_exn sub v with Caml.Not_found -> v
+
+    let apply_set sub vs =
+      Map.fold sub ~init:vs ~f:(fun ~key ~data vs ->
+          let vs' = Set.remove vs key in
+          if Set.to_tree vs' == Set.to_tree vs then vs
+          else (
+            assert (not (Set.equal vs' vs)) ;
+            Set.add vs' data ) )
+
+    let close_set sub vs =
+      Map.fold sub ~init:vs ~f:(fun ~key:_ ~data vs -> Set.add vs data)
+  end
+end
+
+let fold_terms e ~init ~f =
+  let fold_terms_ fold_terms_ e z =
+    let z =
+      match e with
+      | App {op= x; arg= y}
+       |Splat {byt= x; siz= y}
+       |Memory {siz= x; arr= y} ->
+          fold_terms_ y (fold_terms_ x z)
+      | Add {args} | Mul {args} ->
+          Qset.fold args ~init:z ~f:(fun arg _ z -> fold_terms_ arg z)
+      | Concat {args} | Struct_rec {elts= args} ->
+          Vector.fold args ~init:z ~f:(fun z elt -> fold_terms_ elt z)
+      | _ -> z
+    in
+    f z e
+  in
+  fix fold_terms_ (fun _ z -> z) e init
+
+let iter_terms e ~f = fold_terms e ~init:() ~f:(fun () e -> f e)
+
+let fold_vars e ~init ~f =
+  fold_terms e ~init ~f:(fun z -> function
+    | Var _ as v -> f z (v :> Var.t) | _ -> z )
+
+let fv e = fold_vars e ~f:Set.add ~init:Var.Set.empty
+
+(** Construct *)
+
+let var x = x
+let nondet msg = Nondet {msg} |> check invariant
+let label ~parent ~name = Label {parent; name} |> check invariant
+let integer data typ = Integer {data; typ} |> check invariant
+let null = integer Z.zero Typ.ptr
+let bool b = integer (Z.of_bool b) Typ.bool
+let float data = Float {data} |> check invariant
+
+let zero (typ : Typ.t) =
+  match typ with Float _ -> float "0" | _ -> integer Z.zero typ
+
+let one (typ : Typ.t) =
+  match typ with Float _ -> float "1" | _ -> integer Z.one typ
+
+let minus_one (typ : Typ.t) =
+  match typ with Float _ -> float "-1" | _ -> integer Z.minus_one typ
+
+let simp_convert signed (dst : Typ.t) src arg =
+  match (dst, arg) with
+  | _ when Typ.castable dst src -> arg
+  | Integer {bits= m}, Integer {data; typ= Integer {bits= n}} ->
+      integer (Z.clamp ~signed (min m n) data) dst
+  | _ -> App {op= Convert {signed; dst; src}; arg}
+
+let simp_gt x y =
+  match (x, y) with
+  | Integer {data= i}, Integer {data= j; typ= Integer {bits}} ->
+      bool (Z.bgt ~bits i j)
+  | _ -> App {op= App {op= Gt; arg= x}; arg= y}
+
+let simp_ugt x y =
+  match (x, y) with
+  | Integer {data= i}, Integer {data= j; typ= Integer {bits}} ->
+      bool (Z.bugt ~bits i j)
+  | _ -> App {op= App {op= Ugt; arg= x}; arg= y}
+
+let simp_ge x y =
+  match (x, y) with
+  | Integer {data= i}, Integer {data= j; typ= Integer {bits}} ->
+      bool (Z.bgeq ~bits i j)
+  | _ -> App {op= App {op= Ge; arg= x}; arg= y}
+
+let simp_uge x y =
+  match (x, y) with
+  | Integer {data= i}, Integer {data= j; typ= Integer {bits}} ->
+      bool (Z.bugeq ~bits i j)
+  | _ -> App {op= App {op= Uge; arg= x}; arg= y}
+
+let simp_lt x y =
+  match (x, y) with
+  | Integer {data= i}, Integer {data= j; typ= Integer {bits}} ->
+      bool (Z.blt ~bits i j)
+  | _ -> App {op= App {op= Lt; arg= x}; arg= y}
+
+let simp_ult x y =
+  match (x, y) with
+  | Integer {data= i}, Integer {data= j; typ= Integer {bits}} ->
+      bool (Z.bult ~bits i j)
+  | _ -> App {op= App {op= Ult; arg= x}; arg= y}
+
+let simp_le x y =
+  match (x, y) with
+  | Integer {data= i}, Integer {data= j; typ= Integer {bits}} ->
+      bool (Z.bleq ~bits i j)
+  | _ -> App {op= App {op= Le; arg= x}; arg= y}
+
+let simp_ule x y =
+  match (x, y) with
+  | Integer {data= i}, Integer {data= j; typ= Integer {bits}} ->
+      bool (Z.buleq ~bits i j)
+  | _ -> App {op= App {op= Ule; arg= x}; arg= y}
+
+let simp_ord x y = App {op= App {op= Ord; arg= x}; arg= y}
+let simp_uno x y = App {op= App {op= Uno; arg= x}; arg= y}
+
+let sum_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
+
+let rec sum_to_term typ sum =
+  match Qset.length sum with
+  | 0 -> zero typ
+  | 1 -> (
+    match Qset.min_elt sum with
+    | Some (Integer _, q) -> rational q typ
+    | Some (arg, q) when Q.equal Q.one q -> arg
+    | _ -> Add {typ; args= sum} )
+  | _ -> Add {typ; args= sum}
+
+and rational Q.{num; den} typ =
+  let bits = Option.value_exn (Typ.prim_bit_size_of typ) in
+  simp_div
+    (integer (Z.clamp ~signed:true bits num) typ)
+    (integer (Z.clamp ~signed:true bits den) typ)
+
+and simp_div x y =
+  match (x, y) with
+  (* i / j *)
+  | Integer {data= i; typ}, Integer {data= j} when not (Z.equal Z.zero j) ->
+      let bits = Option.value_exn (Typ.prim_bit_size_of typ) in
+      integer (Z.bdiv ~bits i j) typ
+  (* e / 1 ==> e *)
+  | e, Integer {data} when Z.equal Z.one data -> e
+  (* (∑ᵢ cᵢ × Xᵢ) / z ==> ∑ᵢ cᵢ/z × Xᵢ *)
+  | Add {typ; args}, Integer {data} ->
+      sum_to_term typ (sum_mul_const Q.(inv (of_z data)) args)
+  | _ -> App {op= App {op= Div; arg= x}; arg= y}
+
+let simp_udiv x y =
+  match (x, y) with
+  (* i u/ j *)
+  | Integer {data= i; typ}, Integer {data= j} when not (Z.equal Z.zero j) ->
+      let bits = Option.value_exn (Typ.prim_bit_size_of typ) in
+      integer (Z.budiv ~bits i j) typ
+  (* e u/ 1 ==> e *)
+  | e, Integer {data} when Z.equal Z.one data -> e
+  | _ -> App {op= App {op= Udiv; arg= x}; arg= y}
+
+let simp_rem x y =
+  match (x, y) with
+  (* i % j *)
+  | Integer {data= i; typ}, Integer {data= j} when not (Z.equal Z.zero j) ->
+      let bits = Option.value_exn (Typ.prim_bit_size_of typ) in
+      integer (Z.brem ~bits i j) typ
+  (* e % 1 ==> 0 *)
+  | _, Integer {data; typ} when Z.equal Z.one data -> integer Z.zero typ
+  | _ -> App {op= App {op= Rem; arg= x}; arg= y}
+
+let simp_urem x y =
+  match (x, y) with
+  (* i u% j *)
+  | Integer {data= i; typ}, Integer {data= j} when not (Z.equal Z.zero j) ->
+      let bits = Option.value_exn (Typ.prim_bit_size_of typ) in
+      integer (Z.burem ~bits i j) typ
+  (* e u% 1 ==> 0 *)
+  | _, Integer {data; typ} when Z.equal Z.one data -> integer Z.zero typ
+  | _ -> App {op= App {op= Urem; arg= x}; arg= y}
+
+(* 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 = empty_qset
+
+  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; typ} ->
+        Qset.add sum (integer Z.one typ) Q.(coeff * of_z data)
+    | _ -> Qset.add sum term coeff
+
+  let singleton ?(coeff = Q.one) term = add coeff term empty
+
+  let map sum ~f =
+    Qset.fold sum ~init:empty ~f:(fun e c sum -> add c (f e) sum)
+
+  let mul_const = sum_mul_const
+  let to_term = sum_to_term
+end
+
+let rec simp_add_ typ es poly =
+  (* (coeff × term) + poly *)
+  let f term coeff poly =
+    match (term, poly) with
+    (* (0 × e) + s ==> 0 (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) typ
+    (* (c × ∑ᵢ cᵢ × Xᵢ) + s ==> (∑ᵢ (c × cᵢ) × Xᵢ) + s *)
+    | Add {args}, _ -> simp_add_ typ (Sum.mul_const coeff args) poly
+    (* (c₀ × X₀) + (∑ᵢ₌₁ⁿ cᵢ × Xᵢ) ==> ∑ᵢ₌₀ⁿ cᵢ × Xᵢ *)
+    | _, Add {args} -> Sum.to_term typ (Sum.add coeff term args)
+    (* (c₁ × X₁) + X₂ ==> ∑ᵢ₌₁² cᵢ × Xᵢ for c₂ = 1 *)
+    | _ -> Sum.to_term typ (Sum.add coeff term (Sum.singleton poly))
+  in
+  Qset.fold ~f es ~init:poly
+
+let simp_add typ es = simp_add_ typ es (zero typ)
+let simp_add2 typ e f = simp_add_ typ (Sum.singleton e) f
+
+(* 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 = empty_qset
+
+  let add term prod =
+    assert (match term with Integer _ -> false | _ -> true) ;
+    Qset.add prod term Q.one
+
+  let singleton term = add term empty
+  let union = Qset.union
+end
+
+let rec simp_mul2 typ e f =
+  match (e, f) with
+  (* c₁ × c₂ ==> c₁×c₂ *)
+  | Integer {data= i}, Integer {data= j} ->
+      integer (Z.bmul ~bits:(bits_of_int e) i j) typ
+  (* 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 typ (Sum.mul_const (Q.of_z data) args)
+  (* c₁ × x₁ ==> ∑ᵢ₌₁ cᵢ × xᵢ *)
+  | Integer {data= c}, x | x, Integer {data= c} ->
+      Sum.to_term typ (Sum.singleton ~coeff:(Q.of_z c) x)
+  (* (∏ᵤ₌₀ⁱ xᵤ) × (∏ᵥ₌ᵢ₊₁ⁿ xᵥ) ==> ∏ⱼ₌₀ⁿ xⱼ *)
+  | Mul {args= xs1}, Mul {args= xs2} -> Mul {typ; args= Prod.union xs1 xs2}
+  (* (∏ᵢ xᵢ) × (∑ᵤ cᵤ × ∏ⱼ yᵤⱼ) ==> ∑ᵤ cᵤ × ∏ᵢ xᵢ × ∏ⱼ yᵤⱼ *)
+  | (Mul {args= prod} as m), Add {args= sum}
+   |Add {args= sum}, (Mul {args= prod} as m) ->
+      Sum.to_term typ
+        (Sum.map sum ~f:(function
+          | Mul {args} -> Mul {typ; args= Prod.union prod args}
+          | Integer _ as c -> simp_mul2 typ c m
+          | mono -> Mul {typ; args= Prod.add mono prod} ))
+  (* x₀ × (∏ᵢ₌₁ⁿ xᵢ) ==> ∏ᵢ₌₀ⁿ xᵢ *)
+  | Mul {args= xs1}, x | x, Mul {args= xs1} ->
+      Mul {typ; args= Prod.add x xs1}
+  (* e × (∑ᵤ cᵤ × ∏ⱼ yᵤⱼ) ==> ∑ᵤ e × cᵤ × ∏ⱼ yᵤⱼ *)
+  | Add {args}, e | e, Add {args} ->
+      simp_add typ (Sum.map ~f:(fun m -> simp_mul2 typ e m) args)
+  (* x₁ × x₂ ==> ∏ᵢ₌₁² xᵢ *)
+  | _ -> Mul {args= Prod.add e (Prod.singleton f); typ}
+
+let simp_mul typ 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 typ bas term)
+  in
+  let one = one typ in
+  Qset.fold es ~init: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) )
+
+let simp_negate typ x = simp_mul2 typ (minus_one typ) x
+
+let simp_sub typ x y =
+  match (x, y) with
+  (* i - j *)
+  | Integer {data= i}, Integer {data= j} ->
+      let bits = Option.value_exn (Typ.prim_bit_size_of typ) in
+      integer (Z.bsub ~bits i j) typ
+  (* x - y ==> x + (-1 * y) *)
+  | _ -> simp_add2 typ x (simp_negate typ y)
+
+let simp_cond cnd thn els =
+  match cnd with
+  (* ¬(true ? t : e) ==> t *)
+  | Integer {data; typ= Integer {bits= 1}} when Z.is_true data -> thn
+  (* ¬(false ? t : e) ==> e *)
+  | Integer {data; typ= Integer {bits= 1}} when Z.is_false data -> els
+  | _ ->
+      App {op= App {op= App {op= Conditional; arg= cnd}; arg= thn}; arg= els}
+
+let rec simp_and x y =
+  match (x, y) with
+  (* i && j *)
+  | Integer {data= i; typ}, Integer {data= j} ->
+      let bits = Option.value_exn (Typ.prim_bit_size_of typ) in
+      integer (Z.blogand ~bits i j) typ
+  (* e && true ==> e *)
+  | Integer {data; typ= Integer {bits= 1}}, e
+   |e, Integer {data; typ= Integer {bits= 1}}
+    when Z.is_true data ->
+      e
+  (* e && false ==> 0 *)
+  | (Integer {data; typ= Integer {bits= 1}} as f), _
+   |_, (Integer {data; typ= Integer {bits= 1}} as f)
+    when Z.is_false data ->
+      f
+  (* e && (c ? t : f) ==> (c ? e && t : e && f) *)
+  | e, App {op= App {op= App {op= Conditional; arg= c}; arg= t}; arg= f}
+   |App {op= App {op= App {op= Conditional; arg= c}; arg= t}; arg= f}, e ->
+      simp_cond c (simp_and e t) (simp_and e f)
+  (* e && e ==> e *)
+  | _ when equal x y -> x
+  | _ -> App {op= App {op= And; arg= x}; arg= y}
+
+let rec simp_or x y =
+  match (x, y) with
+  (* i || j *)
+  | Integer {data= i; typ}, Integer {data= j} ->
+      let bits = Option.value_exn (Typ.prim_bit_size_of typ) in
+      integer (Z.blogor ~bits i j) typ
+  (* e || true ==> true *)
+  | (Integer {data; typ= Integer {bits= 1}} as t), _
+   |_, (Integer {data; typ= Integer {bits= 1}} as t)
+    when Z.is_true data ->
+      t
+  (* e || false ==> e *)
+  | Integer {data; typ= Integer {bits= 1}}, e
+   |e, Integer {data; typ= Integer {bits= 1}}
+    when Z.is_false data ->
+      e
+  (* e || (c ? t : f) ==> (c ? e || t : e || f) *)
+  | e, App {op= App {op= App {op= Conditional; arg= c}; arg= t}; arg= f}
+   |App {op= App {op= App {op= Conditional; arg= c}; arg= t}; arg= f}, e ->
+      simp_cond c (simp_or e t) (simp_or e f)
+  (* e || e ==> e *)
+  | _ when equal x y -> x
+  | _ -> App {op= App {op= Or; arg= x}; arg= y}
+
+let rec simp_not (typ : Typ.t) term =
+  match (term, typ) with
+  (* ¬(x = y) ==> x ≠ y *)
+  | App {op= App {op= Eq; arg= x}; arg= y}, _ -> simp_dq x y
+  (* ¬(x ≠ y) ==> x = y *)
+  | App {op= App {op= Dq; arg= x}; arg= y}, _ -> simp_eq x y
+  (* ¬(x > y) ==> x <= y *)
+  | App {op= App {op= Gt; arg= x}; arg= y}, _ -> simp_le x y
+  (* ¬(x >= y) ==> x < y *)
+  | App {op= App {op= Ge; arg= x}; arg= y}, _ -> simp_lt x y
+  (* ¬(x < y) ==> x >= y *)
+  | App {op= App {op= Lt; arg= x}; arg= y}, _ -> simp_ge x y
+  (* ¬(x <= y) ==> x > y *)
+  | App {op= App {op= Le; arg= x}; arg= y}, _ -> simp_gt x y
+  (* ¬(x u> y) ==> x u<= y *)
+  | App {op= App {op= Ugt; arg= x}; arg= y}, _ -> simp_ule x y
+  (* ¬(x u>= y) ==> x u< y *)
+  | App {op= App {op= Uge; arg= x}; arg= y}, _ -> simp_ult x y
+  (* ¬(x u< y) ==> x u>= y *)
+  | App {op= App {op= Ult; arg= x}; arg= y}, _ -> simp_uge x y
+  (* ¬(x u<= y) ==> x u> y *)
+  | App {op= App {op= Ule; arg= x}; arg= y}, _ -> simp_ugt x y
+  (* ¬(x ≠ nan ∧ y ≠ nan) ==> x = nan ∨ y = nan *)
+  | App {op= App {op= Ord; arg= x}; arg= y}, _ -> simp_uno x y
+  (* ¬(x = nan ∨ y = nan) ==> x ≠ nan ∧ y ≠ nan *)
+  | App {op= App {op= Uno; arg= x}; arg= y}, _ -> simp_ord x y
+  (* ¬(a ∧ b) ==> ¬a ∨ ¬b *)
+  | App {op= App {op= And; arg= x}; arg= y}, Integer {bits= 1} ->
+      simp_or (simp_not typ x) (simp_not typ y)
+  (* ¬(a ∨ b) ==> ¬a ∧ ¬b *)
+  | App {op= App {op= Or; arg= x}; arg= y}, Integer {bits= 1} ->
+      simp_and (simp_not typ x) (simp_not typ y)
+  (* ¬(c ? t : e) ==> c ? ¬t : ¬e *)
+  | ( App {op= App {op= App {op= Conditional; arg= cnd}; arg= thn}; arg= els}
+    , Integer {bits= 1} ) ->
+      simp_cond cnd (simp_not typ thn) (simp_not typ els)
+  (* ¬false ==> true ¬true ==> false *)
+  | Integer {data}, Integer {bits= 1} -> bool (Z.is_false data)
+  (* ¬b ==> false = b *)
+  | b, Integer {bits= 1} -> App {op= App {op= Eq; arg= bool false}; arg= b}
+  (* ¬e ==> true xor e *)
+  | e, _ ->
+      App {op= App {op= Xor; arg= integer (Z.of_bool true) typ}; arg= e}
+
+and simp_eq x y =
+  match (x, y) with
+  | Integer {data= i; typ}, Integer {data= j} ->
+      let bits = Option.value_exn (Typ.prim_bit_size_of typ) in
+      (* i = j *)
+      bool (Z.beq ~bits i j)
+  | b, Integer {data; typ= Integer {bits= 1}}
+   |Integer {data; typ= Integer {bits= 1}}, b ->
+      if Z.is_false data then (* b = false ==> ¬b *)
+        simp_not Typ.bool b
+      else (* b = true ==> b *)
+        b
+  (* e = (c ? t : f) ==> (c ? e = t : e = f) *)
+  | e, App {op= App {op= App {op= Conditional; arg= c}; arg= t}; arg= f}
+   |App {op= App {op= App {op= Conditional; arg= c}; arg= t}; arg= f}, e ->
+      simp_cond c (simp_eq e t) (simp_eq e f)
+  (* e = e ==> true *)
+  | x, y when equal x y -> bool true
+  | x, y -> App {op= App {op= Eq; arg= x}; arg= y}
+
+and simp_dq x y =
+  match (x, y) with
+  (* e ≠ (c ? t : f) ==> (c ? e ≠ t : e ≠ f) *)
+  | e, App {op= App {op= App {op= Conditional; arg= c}; arg= t}; arg= f}
+   |App {op= App {op= App {op= Conditional; arg= c}; arg= t}; arg= f}, e ->
+      simp_cond c (simp_dq e t) (simp_dq e f)
+  | _ -> (
+    match simp_eq x y with
+    | App {op= App {op= Eq; arg= x}; arg= y} ->
+        App {op= App {op= Dq; arg= x}; arg= y}
+    | b -> simp_not Typ.bool b )
+
+let simp_xor x y =
+  match (x, y) with
+  (* i xor j *)
+  | Integer {data= i; typ}, Integer {data= j} ->
+      let bits = Option.value_exn (Typ.prim_bit_size_of typ) in
+      integer (Z.blogxor ~bits i j) typ
+  (* true xor b ==> ¬b *)
+  | Integer {data; typ= Integer {bits= 1}}, b
+   |b, Integer {data; typ= Integer {bits= 1}}
+    when Z.is_true data ->
+      simp_not Typ.bool b
+  | _ -> App {op= App {op= Xor; arg= x}; arg= y}
+
+let simp_shl x y =
+  match (x, y) with
+  (* i shl j *)
+  | Integer {data= i; typ= Integer {bits} as typ}, Integer {data= j}
+    when Z.sign j >= 0 && Z.lt j (Z.of_int bits) ->
+      integer (Z.bshift_left ~bits i (Z.to_int j)) typ
+  (* e shl 0 ==> e *)
+  | e, Integer {data} when Z.equal Z.zero data -> e
+  | _ -> App {op= App {op= Shl; arg= x}; arg= y}
+
+let simp_lshr x y =
+  match (x, y) with
+  (* i lshr j *)
+  | Integer {data= i; typ= Integer {bits} as typ}, Integer {data= j}
+    when Z.sign j >= 0 && Z.lt j (Z.of_int bits) ->
+      integer (Z.bshift_right_trunc ~bits i (Z.to_int j)) typ
+  (* e lshr 0 ==> e *)
+  | e, Integer {data} when Z.equal Z.zero data -> e
+  | _ -> App {op= App {op= Lshr; arg= x}; arg= y}
+
+let simp_ashr x y =
+  match (x, y) with
+  (* i ashr j *)
+  | Integer {data= i; typ= Integer {bits} as typ}, Integer {data= j}
+    when Z.sign j >= 0 && Z.lt j (Z.of_int bits) ->
+      integer (Z.bshift_right ~bits i (Z.to_int j)) typ
+  (* e ashr 0 ==> e *)
+  | e, Integer {data} when Z.equal Z.zero data -> e
+  | _ -> App {op= App {op= Ashr; arg= x}; arg= y}
+
+(** Access *)
+
+let iter e ~f =
+  match e with
+  | App {op= x; arg= y} | Splat {byt= x; siz= y} | Memory {siz= x; arr= y}
+    ->
+      f x ; f y
+  | Add {args} | Mul {args} -> Qset.iter ~f:(fun arg _ -> f arg) args
+  | Concat {args} | Struct_rec {elts= args} -> Vector.iter ~f args
+  | _ -> ()
+
+let fold e ~init:s ~f =
+  match e with
+  | App {op= x; arg= y} | Splat {byt= x; siz= y} | Memory {siz= x; arr= y}
+    ->
+      f y (f x s)
+  | Add {args} | Mul {args} ->
+      Qset.fold ~f:(fun e _ s -> f e s) args ~init:s
+  | Concat {args} | Struct_rec {elts= args} ->
+      Vector.fold ~f:(fun s e -> f e s) args ~init:s
+  | _ -> s
+
+let is_subterm ~sub ~sup =
+  With_return.with_return
+  @@ fun {return} ->
+  iter_terms sup ~f:(fun e -> if equal sub e then return true) ;
+  false
+
+let app1 ?(partial = false) op arg =
+  ( match (op, arg) with
+  | App {op= Eq; arg= x}, y -> simp_eq x y
+  | App {op= Dq; arg= x}, y -> simp_dq x y
+  | App {op= Gt; arg= x}, y -> simp_gt x y
+  | App {op= Ge; arg= x}, y -> simp_ge x y
+  | App {op= Lt; arg= x}, y -> simp_lt x y
+  | App {op= Le; arg= x}, y -> simp_le x y
+  | App {op= Ugt; arg= x}, y -> simp_ugt x y
+  | App {op= Uge; arg= x}, y -> simp_uge x y
+  | App {op= Ult; arg= x}, y -> simp_ult x y
+  | App {op= Ule; arg= x}, y -> simp_ule x y
+  | App {op= Ord; arg= x}, y -> simp_ord x y
+  | App {op= Uno; arg= x}, y -> simp_uno x y
+  | App {op= Div; arg= x}, y -> simp_div x y
+  | App {op= Udiv; arg= x}, y -> simp_udiv x y
+  | App {op= Rem; arg= x}, y -> simp_rem x y
+  | App {op= Urem; arg= x}, y -> simp_urem x y
+  | App {op= And; arg= x}, y -> simp_and x y
+  | App {op= Or; arg= x}, y -> simp_or x y
+  | App {op= Xor; arg= x}, y -> simp_xor x y
+  | App {op= Shl; arg= x}, y -> simp_shl x y
+  | App {op= Lshr; arg= x}, y -> simp_lshr x y
+  | App {op= Ashr; arg= x}, y -> simp_ashr x y
+  | App {op= App {op= Conditional; arg= x}; arg= y}, z -> simp_cond x y z
+  | Convert {signed; dst; src}, x -> simp_convert signed dst src x
+  | _ -> App {op; arg} )
+  |> check (invariant ~partial)
+  |> check (fun e ->
+         (* every App subterm of output appears in input *)
+         match op with
+         | App {op= Eq | Dq | Xor} -> ()
+         | _ -> (
+           match e with
+           | App {op= App {op= App {op= Conditional}}} -> ()
+           | _ ->
+               iter e ~f:(function
+                 | App {op= Eq | Dq} -> ()
+                 | App _ as a ->
+                     assert (
+                       is_subterm ~sub:a ~sup:op
+                       || is_subterm ~sub:a ~sup:arg
+                       || Trace.fail
+                            "simplifying %a %a@ yields %a@ with new \
+                             subterm %a"
+                            pp op pp arg pp e pp a )
+                 | _ -> () ) ) )
+
+let app2 op x y = app1 (app1 ~partial:true op x) y
+let app3 op x y z = app1 (app1 ~partial:true (app1 ~partial:true op x) y) z
+let addN typ args = simp_add typ args |> check invariant
+let mulN typ args = simp_mul typ args |> check invariant
+
+let check1 op typ x =
+  type_check x typ ;
+  op typ x |> check invariant
+
+let check2 op typ x y =
+  type_check2 x y typ ;
+  op typ x y |> check invariant
+
+let simp_memory siz arr = Memory {siz; arr}
+
+let memory ~siz ~arr =
+  type_check siz Typ.siz ;
+  simp_memory siz arr |> check invariant
+
+let simp_concat xs =
+  if Vector.length xs = 1 then Vector.get xs 0
+  else
+    let args =
+      if Vector.for_all xs ~f:(function Concat _ -> false | _ -> true)
+      then xs
+      else
+        Vector.concat
+          (Vector.fold_right xs ~init:[] ~f:(fun x s ->
+               match x with
+               | Concat {args} -> args :: s
+               | x -> Vector.of_array [|x|] :: s ))
+    in
+    Concat {args}
+
+let concat xs = simp_concat (Vector.of_array xs) |> check invariant
+
+let simp_splat byt siz =
+  match siz with
+  | Integer {data} when Z.equal Z.zero data -> concat [||]
+  | _ -> Splat {byt; siz}
+
+let splat ~byt ~siz =
+  type_check byt Typ.byt ;
+  type_check siz Typ.siz ;
+  simp_splat byt siz |> check invariant
+
+let eq = app2 Eq
+let dq = app2 Dq
+let gt = app2 Gt
+let ge = app2 Ge
+let lt = app2 Lt
+let le = app2 Le
+let ugt = app2 Ugt
+let uge = app2 Uge
+let ult = app2 Ult
+let ule = app2 Ule
+let ord = app2 Ord
+let uno = app2 Uno
+let neg = check1 simp_negate
+let add = check2 simp_add2
+let sub = check2 simp_sub
+let mul = check2 simp_mul2
+let div = app2 Div
+let udiv = app2 Udiv
+let rem = app2 Rem
+let urem = app2 Urem
+let and_ = app2 And
+let or_ = app2 Or
+let xor = app2 Xor
+let not_ = check1 simp_not
+let shl = app2 Shl
+let lshr = app2 Lshr
+let ashr = app2 Ashr
+let conditional ~cnd ~thn ~els = app3 Conditional cnd thn els
+let record elts = List.fold ~f:app1 ~init:Record elts
+let select ~rcd ~idx = app2 Select rcd idx
+let update ~rcd ~elt ~idx = app3 Update rcd elt idx
+
+let struct_rec key =
+  let memo_id = Hashtbl.create key in
+  let dummy = null in
+  Staged.stage
+  @@ fun ~id elt_thks ->
+  match Hashtbl.find memo_id id with
+  | None ->
+      (* Add placeholder to prevent computing [elts] in calls to
+         [struct_rec] from [elt_thks] for recursive occurrences of [id]. *)
+      let elta = Array.create ~len:(Vector.length elt_thks) dummy in
+      let elts = Vector.of_array elta in
+      Hashtbl.set memo_id ~key:id ~data:elts ;
+      Vector.iteri elt_thks ~f:(fun i (lazy elt) -> elta.(i) <- elt) ;
+      Struct_rec {elts} |> check invariant
+  | Some elts ->
+      (* Do not check invariant as invariant will be checked above after the
+         thunks are forced, before which invariant-checking may spuriously
+         fail. Note that it is important that the value constructed here
+         shares the array in the memo table, so that the update after
+         forcing the recursive thunks also updates this value. *)
+      Struct_rec {elts}
+
+let convert ?(signed = false) ~dst ~src term =
+  app1 (Convert {signed; dst; src}) term
+
+let rec of_exp (e : Exp.t) =
+  let of_exps exps =
+    Qset.fold exps ~init:empty_qset ~f:(fun e q ts ->
+        Qset.add ts (of_exp e) q )
+  in
+  match e with
+  | Add {args; typ} -> Add {args= of_exps args; typ}
+  | Mul {args; typ} -> Mul {args= of_exps args; typ}
+  | Splat {byt; siz} -> Splat {byt= of_exp byt; siz= of_exp siz}
+  | Memory {siz; arr} -> Memory {siz= of_exp siz; arr= of_exp arr}
+  | Concat {args} -> Concat {args= Vector.map ~f:of_exp args}
+  | Reg {id; name} -> Var {id; name}
+  | Nondet {msg} -> Nondet {msg}
+  | Label {parent; name} -> Label {parent; name}
+  | App {op; arg} -> App {op= of_exp op; arg= of_exp arg}
+  | Eq -> Eq
+  | Dq -> Dq
+  | Gt -> Gt
+  | Ge -> Ge
+  | Lt -> Lt
+  | Le -> Le
+  | Ugt -> Ugt
+  | Uge -> Uge
+  | Ult -> Ult
+  | Ule -> Ule
+  | Ord -> Ord
+  | Uno -> Uno
+  | Div -> Div
+  | Udiv -> Udiv
+  | Rem -> Rem
+  | Urem -> Urem
+  | And -> And
+  | Or -> Or
+  | Xor -> Xor
+  | Shl -> Shl
+  | Lshr -> Lshr
+  | Ashr -> Ashr
+  | Conditional -> Conditional
+  | Record -> Record
+  | Select -> Select
+  | Update -> Update
+  | Struct_rec {elts} ->
+      Staged.unstage
+        (struct_rec (module Exp))
+        ~id:e
+        (Vector.map elts ~f:(fun e -> lazy (of_exp e)))
+  | Convert {signed; dst; src} -> Convert {signed; dst; src}
+  | Integer {data; typ} -> Integer {data; typ}
+  | Float {data} -> Float {data}
+
+let size_of t =
+  Option.bind (Typ.prim_bit_size_of t) ~f:(fun n ->
+      if n % 8 = 0 then Some (integer (Z.of_int (n / 8)) Typ.siz) else None
+  )
+
+(** Transform *)
+
+let map e ~f =
+  let map_ : (t -> t) -> t -> t =
+   fun map_ e ->
+    let map_bin mk ~f x y =
+      let x' = f x in
+      let y' = f y in
+      if x' == x && y' == y then e else mk x' y'
+    in
+    let map_vector mk ~f args =
+      let args' = Vector.map_preserving_phys_equal ~f args in
+      if args' == args then e else mk args'
+    in
+    let map_qset mk typ ~f args =
+      let args' = Qset.map ~f:(fun arg q -> (f arg, q)) args in
+      if args' == args then e else mk typ args'
+    in
+    match e with
+    | App {op; arg} -> map_bin (app1 ~partial:true) ~f op arg
+    | Add {args; typ} -> map_qset addN typ ~f args
+    | Mul {args; typ} -> map_qset mulN typ ~f args
+    | Splat {byt; siz} -> map_bin simp_splat ~f byt siz
+    | Memory {siz; arr} -> map_bin simp_memory ~f siz arr
+    | Concat {args} -> map_vector simp_concat ~f args
+    | Struct_rec {elts= args} -> Struct_rec {elts= Vector.map args ~f:map_}
+    | _ -> e
+  in
+  fix map_ (fun e -> e) e
+
+let rename sub e =
+  let rec rename_ sub e =
+    match e with
+    | Var _ -> Var.Subst.apply sub e
+    | _ -> map ~f:(rename_ sub) e
+  in
+  rename_ sub e |> check (invariant ~partial:true)
+
+(** Query *)
+
+let is_true = function
+  | Integer {data; typ= Integer {bits= 1}} -> Z.is_true data
+  | _ -> false
+
+let is_false = function
+  | Integer {data; typ= Integer {bits= 1}} -> Z.is_false data
+  | _ -> false
+
+let rec is_constant e =
+  let is_constant_bin x y = is_constant x && is_constant y in
+  match e with
+  | Var _ | Nondet _ -> false
+  | App {op= x; arg= y} | Splat {byt= x; siz= y} | Memory {siz= x; arr= y}
+    ->
+      is_constant_bin x y
+  | Add {args} | Mul {args} ->
+      Qset.for_all ~f:(fun arg _ -> is_constant arg) args
+  | Concat {args} | Struct_rec {elts= args} ->
+      Vector.for_all ~f:is_constant args
+  | _ -> true
+
+let classify = function
+  | Add _ | Mul _ -> `Interpreted
+  | App {op= Eq | Dq | App {op= Eq | Dq}} -> `Simplified
+  | App _ -> `Uninterpreted
+  | _ -> `Atomic
+
+let solve e f =
+  [%Trace.call fun {pf} -> pf "%a@ %a" pp e pp f]
+  ;
+  let rec solve_ e f s =
+    let solve_uninterp e f =
+      let ord = compare e f in
+      match (is_constant e, is_constant f) with
+      | true, true when ord <> 0 -> None
+      (* orient equation to discretionarily prefer term that is constant or
+         compares smaller as class representative *)
+      | true, false -> Some (Map.add_exn s ~key:f ~data:e)
+      | false, true -> Some (Map.add_exn s ~key:e ~data:f)
+      | _ ->
+          let key, data = if ord > 0 then (e, f) else (f, e) in
+          Some (Map.add_exn s ~key ~data)
+    in
+    let concat_size args =
+      Vector.fold_until args ~init:(integer Z.zero Typ.siz)
+        ~f:(fun sum -> function
+          | Memory {siz} -> Continue (add Typ.siz siz sum) | _ -> Stop None
+          )
+        ~finish:(fun _ -> None)
+    in
+    match (e, f) with
+    | (Add {typ} | Mul {typ} | Integer {typ}), _
+     |_, (Add {typ} | Mul {typ} | Integer {typ}) -> (
+      match sub typ e f with
+      | Add {args} ->
+          let c, q = Qset.min_elt_exn args in
+          let n = Sum.to_term typ (Qset.remove args c) in
+          let d = rational (Q.neg q) typ in
+          let r = div n d in
+          Some (Map.add_exn s ~key:c ~data:r)
+      | e_f -> solve_uninterp e_f (zero typ) )
+    | Concat {args= ms}, Concat {args= ns} -> (
+      match (concat_size ms, concat_size ns) with
+      | Some p, Some q -> solve_uninterp e f >>= solve_ p q
+      | _ -> solve_uninterp e f )
+    | Memory {siz= m}, Concat {args= ns} | Concat {args= ns}, Memory {siz= m}
+      -> (
+      match concat_size ns with
+      | Some p -> solve_uninterp e f >>= solve_ p m
+      | _ -> solve_uninterp e f )
+    | _ -> solve_uninterp e f
+  in
+  solve_ e f empty_map
+  |>
+  [%Trace.retn fun {pf} ->
+    function Some s -> pf "%a" Var.Subst.pp s | None -> pf "false"]
diff --git a/sledge/src/symbheap/term.mli b/sledge/src/symbheap/term.mli
new file mode 100644
index 000000000..e7dddf643
--- /dev/null
+++ b/sledge/src/symbheap/term.mli
@@ -0,0 +1,219 @@
+(*
+ * 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 complex arithmetic, bitwise-logical,
+    etc. operations over literal values and variables.
+
+    Terms for operations that are uninterpreted in the analyzer are
+    represented in curried form, where [App] is an application of a function
+    symbol to an argument. This is done to simplify the definition of
+    'subterm' and make it explicit. The specific constructor functions
+    indicate and check the expected arity of the function symbols. *)
+
+type comparator_witness
+
+type qset = (t, comparator_witness) Qset.t
+
+and t = private
+  | Add of {args: qset; typ: Typ.t}  (** Addition *)
+  | Mul of {args: qset; typ: Typ.t}  (** Multiplication *)
+  | Splat of {byt: t; siz: t}
+      (** Iterated concatenation of a single byte *)
+  | Memory of {siz: t; arr: t}  (** Size-tagged byte-array *)
+  | Concat of {args: t vector}  (** Byte-array concatenation *)
+  | Var of {id: int; name: string}  (** Local variable / virtual register *)
+  | Nondet of {msg: string}
+      (** Anonymous local variable with arbitrary value, representing
+          non-deterministic approximation of value described by [msg] *)
+  | Label of {parent: string; name: string}
+      (** Address of named code block within parent function *)
+  | App of {op: t; arg: t}
+      (** Application of function symbol to argument, curried *)
+  | Eq  (** Equal test *)
+  | Dq  (** Disequal test *)
+  | Gt  (** Greater-than test *)
+  | Ge  (** Greater-than-or-equal test *)
+  | Lt  (** Less-than test *)
+  | Le  (** Less-than-or-equal test *)
+  | Ugt  (** Unsigned greater-than test *)
+  | Uge  (** Unsigned greater-than-or-equal test *)
+  | Ult  (** Unsigned less-than test *)
+  | Ule  (** Unsigned less-than-or-equal test *)
+  | Ord  (** Ordered test (neither arg is nan) *)
+  | Uno  (** Unordered test (some arg is nan) *)
+  | Div  (** Division *)
+  | Udiv  (** Unsigned division *)
+  | Rem  (** Remainder of division *)
+  | Urem  (** Remainder of unsigned division *)
+  | And  (** Conjunction, boolean or bitwise *)
+  | Or  (** Disjunction, boolean or bitwise *)
+  | Xor  (** Exclusive-or, bitwise *)
+  | Shl  (** Shift left, bitwise *)
+  | Lshr  (** Logical shift right, bitwise *)
+  | Ashr  (** Arithmetic shift right, bitwise *)
+  | Conditional  (** If-then-else *)
+  | Record  (** Record (array / struct) constant *)
+  | Select  (** Select an index from a record *)
+  | Update  (** Constant record with updated index *)
+  | Struct_rec of {elts: t vector}
+      (** Struct constant that may recursively refer to itself
+          (transitively) from [elts]. NOTE: represented by cyclic values. *)
+  | Convert of {signed: bool; dst: Typ.t; src: Typ.t}
+      (** Convert between specified types, possibly with loss of information *)
+  | Integer of {data: Z.t; typ: Typ.t}
+      (** Integer constant, or if [typ] is a [Pointer], null pointer value
+          that never refers to an object *)
+  | Float of {data: string}  (** Floating-point constant *)
+[@@deriving compare, equal, hash, sexp]
+
+val comparator : (t, comparator_witness) Comparator.t
+
+type term = t
+
+val pp_full : ?is_x:(term -> bool) -> t pp
+val pp : t pp
+val invariant : ?partial:bool -> t -> unit
+
+(** Term.Var is re-exported as Var *)
+module Var : sig
+  type t = private term [@@deriving compare, equal, hash, sexp]
+  type var = t
+
+  include Comparator.S with type t := t
+
+  module Set : sig
+    type t = (var, comparator_witness) Set.t
+    [@@deriving compare, equal, sexp]
+
+    val pp_full : ?is_x:(term -> bool) -> t pp
+    val pp : t pp
+    val empty : t
+    val of_option : var option -> t
+    val of_list : var list -> t
+    val of_vector : var vector -> t
+    val of_regs : Reg.Set.t -> t
+  end
+
+  module Map : sig
+    type 'a t = (var, 'a, comparator_witness) Map.t
+    [@@deriving compare, equal, sexp]
+
+    val empty : 'a t
+  end
+
+  val pp : t pp
+  val pp_demangled : t pp
+
+  include Invariant.S with type t := t
+
+  val of_reg : Reg.t -> t
+  val of_term : term -> t option
+  val program : string -> t
+  val fresh : string -> wrt:Set.t -> t * Set.t
+  val id : t -> int
+  val name : t -> string
+
+  module Subst : sig
+    type t [@@deriving compare, equal, sexp]
+
+    val pp : t pp
+    val empty : t
+    val freshen : Set.t -> wrt:Set.t -> t
+    val extend : t -> replace:var -> with_:var -> t
+    val invert : t -> t
+    val exclude : t -> Set.t -> t
+    val restrict : t -> Set.t -> t
+    val is_empty : t -> bool
+    val domain : t -> Set.t
+    val range : t -> Set.t
+    val apply_set : t -> Set.t -> Set.t
+    val close_set : t -> Set.t -> Set.t
+  end
+end
+
+(** Construct *)
+
+val of_exp : Exp.t -> t
+val var : Var.t -> t
+val nondet : string -> t
+val label : parent:string -> name:string -> t
+val null : t
+val splat : byt:t -> siz:t -> t
+val memory : siz:t -> arr:t -> t
+val concat : t array -> t
+val bool : bool -> t
+val integer : Z.t -> Typ.t -> t
+val rational : Q.t -> Typ.t -> t
+val float : string -> t
+val eq : t -> t -> t
+val dq : t -> t -> t
+val gt : t -> t -> t
+val ge : t -> t -> t
+val lt : t -> t -> t
+val le : t -> t -> t
+val ugt : t -> t -> t
+val uge : t -> t -> t
+val ult : t -> t -> t
+val ule : t -> t -> t
+val ord : t -> t -> t
+val uno : t -> t -> t
+val neg : Typ.t -> t -> t
+val add : Typ.t -> t -> t -> t
+val sub : Typ.t -> t -> t -> t
+val mul : Typ.t -> t -> t -> t
+val div : t -> t -> t
+val udiv : t -> t -> t
+val rem : t -> t -> t
+val urem : t -> t -> t
+val and_ : t -> t -> t
+val or_ : t -> t -> t
+val xor : t -> t -> t
+val not_ : Typ.t -> t -> t
+val shl : t -> t -> t
+val lshr : t -> t -> t
+val ashr : t -> t -> t
+val conditional : cnd:t -> thn:t -> els:t -> t
+val record : t list -> t
+val select : rcd:t -> idx:t -> t
+val update : rcd:t -> elt:t -> idx:t -> t
+
+val struct_rec :
+     (module Hashtbl.Key with type t = 'id)
+  -> (id:'id -> t lazy_t vector -> t) Staged.t
+(** [struct_rec Id id element_thunks] constructs a possibly-cyclic [Struct]
+    value. Cycles are detected using [Id]. The caller of [struct_rec Id]
+    must ensure that a single unstaging of [struct_rec Id] is used for each
+    complete cyclic value. Also, the caller must ensure that recursive calls
+    to [struct_rec Id] provide [id] values that uniquely identify at least
+    one point on each cycle. Failure to obey these requirements will lead to
+    stack overflow. *)
+
+val convert : ?signed:bool -> dst:Typ.t -> src:Typ.t -> t -> t
+val size_of : Typ.t -> t option
+
+(** Access *)
+
+val iter : t -> f:(t -> unit) -> unit
+val fold_vars : t -> init:'a -> f:('a -> Var.t -> 'a) -> 'a
+val fold_terms : t -> init:'a -> f:('a -> t -> 'a) -> 'a
+val fold : t -> init:'a -> f:(t -> 'a -> 'a) -> 'a
+
+(** Transform *)
+
+val map : t -> f:(t -> t) -> t
+val rename : Var.Subst.t -> t -> t
+
+(** Query *)
+
+val fv : t -> Var.Set.t
+val is_true : t -> bool
+val is_false : t -> bool
+val typ : t -> Typ.t option
+val classify : t -> [> `Atomic | `Interpreted | `Simplified | `Uninterpreted]
+val solve : t -> t -> (t, t, comparator_witness) Map.t option
diff --git a/sledge/src/llair/exp_test.ml b/sledge/src/symbheap/term_test.ml
similarity index 81%
rename from sledge/src/llair/exp_test.ml
rename to sledge/src/symbheap/term_test.ml
index 6cc5b954a..6f23d2670 100644
--- a/sledge/src/llair/exp_test.ml
+++ b/sledge/src/symbheap/term_test.ml
@@ -9,48 +9,50 @@ let%test_module _ =
   ( module struct
     (* let () = Trace.init ~margin:68 ~config:all () *)
     let () = Trace.init ~margin:68 ~config:none ()
-    let pp = Format.printf "@\n%a@." Exp.pp
+    let pp = Format.printf "@\n%a@." Term.pp
     let char = Typ.integer ~bits:8
-    let ( ! ) i = Exp.integer (Z.of_int i) char
-    let ( + ) = Exp.add char
-    let ( - ) = Exp.sub char
-    let ( * ) = Exp.mul char
-    let ( = ) = Exp.eq
-    let ( != ) = Exp.dq
-    let ( > ) = Exp.gt
-    let ( >= ) = Exp.ge
-    let ( < ) = Exp.lt
-    let ( <= ) = Exp.le
-    let ( && ) = Exp.and_
-    let ( || ) = Exp.or_
-    let ( ~~ ) = Exp.not_ Typ.bool
+    let ( ! ) i = Term.integer (Z.of_int i) char
+    let ( + ) = Term.add char
+    let ( - ) = Term.sub char
+    let ( * ) = Term.mul char
+    let ( = ) = Term.eq
+    let ( != ) = Term.dq
+    let ( > ) = Term.gt
+    let ( >= ) = Term.ge
+    let ( < ) = Term.lt
+    let ( <= ) = Term.le
+    let ( && ) = Term.and_
+    let ( || ) = Term.or_
+    let ( ~~ ) = Term.not_ Typ.bool
     let wrt = Var.Set.empty
     let y_, wrt = Var.fresh "y" ~wrt
     let z_, _ = Var.fresh "z" ~wrt
-    let y = Exp.var y_
-    let z = Exp.var z_
+    let y = Term.var y_
+    let z = Term.var z_
 
     let%test "booleans distinct" =
-      Exp.is_false
-        (Exp.eq
-           (Exp.integer Z.minus_one Typ.bool)
-           (Exp.integer Z.zero Typ.bool))
+      Term.is_false
+        (Term.eq
+           (Term.integer Z.minus_one Typ.bool)
+           (Term.integer Z.zero Typ.bool))
 
     let%test "unsigned booleans distinct" =
-      Exp.is_false
-        (Exp.eq (Exp.integer Z.one Typ.bool) (Exp.integer Z.zero Typ.bool))
+      Term.is_false
+        (Term.eq
+           (Term.integer Z.one Typ.bool)
+           (Term.integer Z.zero Typ.bool))
 
     let%test "boolean overflow" =
-      Exp.is_true
-        (Exp.eq
-           (Exp.integer Z.minus_one Typ.bool)
-           (Exp.integer Z.one Typ.bool))
+      Term.is_true
+        (Term.eq
+           (Term.integer Z.minus_one Typ.bool)
+           (Term.integer Z.one Typ.bool))
 
     let%test "unsigned boolean overflow" =
-      Exp.is_true
-        (Exp.uge
-           (Exp.integer Z.minus_one Typ.bool)
-           (Exp.integer Z.one Typ.bool))
+      Term.is_true
+        (Term.uge
+           (Term.integer Z.minus_one Typ.bool)
+           (Term.integer Z.one Typ.bool))
 
     let%expect_test _ =
       pp (!42 + !13) ;
@@ -176,19 +178,19 @@ let%test_module _ =
       [%expect {| 0 |}]
 
     let%expect_test _ =
-      pp (!3 * y = z = Exp.bool true) ;
+      pp (!3 * y = z = Term.bool true) ;
       [%expect {| ((3 × %y_1) = %z_2) |}]
 
     let%expect_test _ =
-      pp (Exp.bool true = (!3 * y = z)) ;
+      pp (Term.bool true = (!3 * y = z)) ;
       [%expect {| ((3 × %y_1) = %z_2) |}]
 
     let%expect_test _ =
-      pp (!3 * y = z = Exp.bool false) ;
+      pp (!3 * y = z = Term.bool false) ;
       [%expect {| ((3 × %y_1) ≠ %z_2) |}]
 
     let%expect_test _ =
-      pp (Exp.bool false = (!3 * y = z)) ;
+      pp (Term.bool false = (!3 * y = z)) ;
       [%expect {| ((3 × %y_1) ≠ %z_2) |}]
 
     let%expect_test _ =
@@ -208,11 +210,11 @@ let%test_module _ =
       [%expect {| ((-3 × %y_1 + 4) = %y_1) |}]
 
     let%expect_test _ =
-      pp (Exp.sub Typ.bool (Exp.bool true) (z = !4)) ;
+      pp (Term.sub Typ.bool (Term.bool true) (z = !4)) ;
       [%expect {| (-1 × (%z_2 = 4) + -1) |}]
 
     let%expect_test _ =
-      pp (Exp.add Typ.bool (Exp.bool true) (z = !4) = (z = !4)) ;
+      pp (Term.add Typ.bool (Term.bool true) (z = !4) = (z = !4)) ;
       [%expect {| (((%z_2 = 4) + -1) = (%z_2 = 4)) |}]
 
     let%expect_test _ =
@@ -244,9 +246,9 @@ let%test_module _ =
       [%expect {| ((%y_1 < 2) && (%z_2 ≥ 3)) |}]
 
     let%expect_test _ =
-      pp Exp.(eq z null) ;
-      pp Exp.(eq null z) ;
-      pp Exp.(dq (eq null z) (bool false)) ;
+      pp Term.(eq z null) ;
+      pp Term.(eq null z) ;
+      pp Term.(dq (eq null z) (bool false)) ;
       [%expect
         {|
         (%z_2 = null)
diff --git a/sledge/src/llair/exp_test.mli b/sledge/src/symbheap/term_test.mli
similarity index 100%
rename from sledge/src/llair/exp_test.mli
rename to sledge/src/symbheap/term_test.mli
diff --git a/sledge/src/llair/var.ml b/sledge/src/symbheap/var.ml
similarity index 92%
rename from sledge/src/llair/var.ml
rename to sledge/src/symbheap/var.ml
index bcc0b0865..0b93a52e0 100644
--- a/sledge/src/llair/var.ml
+++ b/sledge/src/symbheap/var.ml
@@ -7,4 +7,4 @@
 
 (** Variables *)
 
-include Exp.Var
+include Term.Var
diff --git a/sledge/src/llair/var.mli b/sledge/src/symbheap/var.mli
similarity index 86%
rename from sledge/src/llair/var.mli
rename to sledge/src/symbheap/var.mli
index 64bdc2169..d4d909555 100644
--- a/sledge/src/llair/var.mli
+++ b/sledge/src/symbheap/var.mli
@@ -7,4 +7,4 @@
 
 (** Variables *)
 
-include module type of Exp.Var
+include module type of Term.Var