diff --git a/sledge/src/symbheap/equality.ml b/sledge/src/symbheap/equality.ml
index 9076fe833..4706f810a 100644
--- a/sledge/src/symbheap/equality.ml
+++ b/sledge/src/symbheap/equality.ml
@@ -233,11 +233,8 @@ let difference r a b =
   let b = canon r b in
   ( if Term.equal a b then Some Z.zero
   else
-    match (Term.typ a, Term.typ b) with
-    | Some typ, _ | _, Some typ -> (
-      match normalize r (Term.sub typ a b) with
-      | Integer {data} -> Some data
-      | _ -> None )
+    match normalize r (Term.sub a b) with
+    | Integer {data} -> Some data
     | _ -> None )
   |>
   [%Trace.retn fun {pf} ->
diff --git a/sledge/src/symbheap/equality_test.ml b/sledge/src/symbheap/equality_test.ml
index f775fd168..ec6027b24 100644
--- a/sledge/src/symbheap/equality_test.ml
+++ b/sledge/src/symbheap/equality_test.ml
@@ -18,10 +18,10 @@ 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 = Term.integer (Z.of_int i) Typ.siz
-    let ( + ) = Term.add Typ.siz
-    let ( - ) = Term.sub Typ.siz
-    let ( * ) = Term.mul Typ.siz
+    let ( ! ) i = Term.integer (Z.of_int i)
+    let ( + ) = Term.add
+    let ( - ) = Term.sub
+    let ( * ) = Term.mul
     let f = Term.convert ~dst:i64 ~src:i8
     let g = Term.rem
     let wrt = Var.Set.empty
@@ -307,7 +307,7 @@ let%test_module _ =
     let%expect_test _ =
       pp r14 ; [%expect {| {sat= true; rep= [[%x_5 ↦ 1]]} |}]
 
-    let%test _ = entails_eq r14 a (Term.bool true)
+    let%test _ = entails_eq r14 a Term.true_
 
     let b = Term.dq y !0
     let r14 = of_eqs [(a, b); (x, !1)]
@@ -318,8 +318,8 @@ let%test_module _ =
         {|
           {sat= true; rep= [[%x_5 ↦ 1]; [(%y_6 ≠ 0) ↦ -1]]} |}]
 
-    let%test _ = entails_eq r14 a (Term.bool true)
-    let%test _ = entails_eq r14 b (Term.bool true)
+    let%test _ = entails_eq r14 a Term.true_
+    let%test _ = entails_eq r14 b Term.true_
 
     let b = Term.dq x !0
     let r15 = of_eqs [(b, b); (x, !1)]
diff --git a/sledge/src/symbheap/exec.ml b/sledge/src/symbheap/exec.ml
index 7e3393c73..08c1ca793 100644
--- a/sledge/src/symbheap/exec.ml
+++ b/sledge/src/symbheap/exec.ml
@@ -32,7 +32,6 @@ let fresh_seg ~loc ?bas ?len ?siz ?arr ?(xs = Var.Set.empty) us =
   {us; xs; seg= {loc; bas; len; siz; arr}}
 
 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
@@ -117,7 +116,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_ (Term.eq dst src) (Sh.and_ (Term.eq len zero) dst_heap)
+    Sh.and_ (Term.eq dst src) (Sh.and_ (Term.eq len Term.zero) dst_heap)
   in
   let post = dst_heap in
   {xs; foot; sub= Var.Subst.empty; ms= Var.Set.empty; post}
@@ -165,9 +164,9 @@ 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 = Term.sub Typ.siz src dst in
+  let src_dst = Term.sub 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 siz_mid = Term.sub 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
@@ -184,7 +183,7 @@ let memmov_foot us dst src len =
   let foot =
     Sh.and_ eq_mem_dst_mid_src
       (Sh.and_ (Term.lt dst src)
-         (Sh.and_ (Term.lt src (Term.add Typ.ptr dst len)) seg))
+         (Sh.and_ (Term.lt src (Term.add dst len)) seg))
   in
   (xs, bas, siz, mem_dst, mem_mid, mem_src, foot)
 
@@ -252,7 +251,7 @@ let memmov_specs us dst src len =
  *)
 let alloc_spec us reg num len =
   let foot = Sh.emp in
-  let siz = Term.mul Typ.siz num len in
+  let siz = Term.mul num len in
   let sub, ms, us =
     assign ~ws:(Set.add Var.Set.empty reg) ~rs:(Term.fv siz) ~us
   in
@@ -324,13 +323,13 @@ let mallocx_spec us reg siz =
  *)
 let calloc_spec us reg num len =
   let foot = Sh.emp in
-  let siz = Term.mul Typ.siz num len in
+  let siz = Term.mul num len in
   let sub, ms, us =
     assign ~ws:(Set.add Var.Set.empty reg) ~rs:(Term.fv siz) ~us
   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 arr = Term.splat ~byt:Term.zero ~siz in
   let {us= _; xs; seg} = fresh_seg ~loc ~bas:loc ~len:siz ~siz ~arr us in
   let post = Sh.or_ (null_eq (Term.var reg)) (Sh.seg seg) in
   {xs; foot; sub; ms; post}
@@ -357,8 +356,8 @@ 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 = Term.integer (Z.of_int 0) Typ.int in
-  let enomem = Term.integer (Z.of_int 12) Typ.int in
+  let eok = Term.zero in
+  let enomem = Term.integer (Z.of_int 12) in
   let post =
     Sh.or_
       (Sh.and_ (Term.eq (Term.var reg) enomem) (Sh.rename sub foot))
@@ -402,12 +401,12 @@ let realloc_spec us reg ptr siz =
                (eq (memory ~siz ~arr:a1)
                   (concat
                      [| memory ~siz:len ~arr:a0
-                      ; memory ~siz:(sub Typ.siz siz len) ~arr:a2 |]))
+                      ; memory ~siz:(sub siz len) ~arr:a2 |]))
              ~els:
                (eq (memory ~siz:len ~arr:a0)
                   (concat
                      [| memory ~siz ~arr:a1
-                      ; memory ~siz:(sub Typ.siz len siz) ~arr:a2 |])))
+                      ; memory ~siz:(sub len siz) ~arr:a2 |])))
          (Sh.seg rseg))
   in
   {xs; foot; sub; ms; post}
@@ -444,12 +443,12 @@ let rallocx_spec us reg ptr siz =
                (eq (memory ~siz ~arr:a1)
                   (concat
                      [| memory ~siz:len ~arr:a0
-                      ; memory ~siz:(sub Typ.siz siz len) ~arr:a2 |]))
+                      ; memory ~siz:(sub siz len) ~arr:a2 |]))
              ~els:
                (eq (memory ~siz:len ~arr:a0)
                   (concat
                      [| memory ~siz ~arr:a1
-                      ; memory ~siz:(sub Typ.siz len siz) ~arr:a2 |])))
+                      ; memory ~siz:(sub len siz) ~arr:a2 |])))
          (Sh.seg rseg))
   in
   {xs; foot; sub; ms; post}
@@ -488,13 +487,13 @@ let xallocx_spec us reg ptr siz ext =
                (eq (memory ~siz ~arr:a1)
                   (concat
                      [| memory ~siz:len ~arr:a0
-                      ; memory ~siz:(sub Typ.siz siz len) ~arr:a2 |]))
+                      ; memory ~siz:(sub siz len) ~arr:a2 |]))
              ~els:
                (eq (memory ~siz:len ~arr:a0)
                   (concat
                      [| memory ~siz ~arr:a1
-                      ; memory ~siz:(sub Typ.siz len siz) ~arr:a2 |])))
-          (and_ (le siz reg) (le reg (add Typ.siz siz ext))))
+                      ; memory ~siz:(sub len siz) ~arr:a2 |])))
+          (and_ (le siz reg) (le reg (add siz ext))))
       (Sh.seg seg')
   in
   {xs; foot; sub; ms; post}
@@ -529,15 +528,14 @@ let malloc_usable_size_spec us reg ptr =
  *)
 let nallocx_spec us reg siz =
   let xs = Var.Set.empty in
-  let foot = Sh.pure (Term.dq siz zero) in
+  let foot = Sh.pure (Term.dq siz Term.zero) in
   let sub, ms, _ = assign ~ws:(Set.add Var.Set.empty reg) ~rs:foot.us ~us 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 =
-  Term.mul Typ.siz (Option.value_exn (Term.size_of Typ.siz)) n
+let size_of_int_mul n = Term.mul (Option.value_exn (Term.size_of Typ.siz)) n
 
 (* { r-[_;_)->⟨m,_⟩ * i-[_;_)->⟨_,m⟩ * w=0 * n=0 }
  *   mallctl r i w n
@@ -642,11 +640,7 @@ let strlen_spec us reg ptr =
   let foot = Sh.seg seg in
   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 =
-    Term.sub Typ.siz
-      (Term.sub Typ.siz (Term.add Typ.siz b m) p)
-      (Term.integer Z.one Typ.siz)
-  in
+  let ret = Term.sub (Term.sub (Term.add b m) p) Term.one in
   let post =
     Sh.and_
       (Term.eq (Term.var reg) (Term.rename sub ret))
diff --git a/sledge/src/symbheap/sh.ml b/sledge/src/symbheap/sh.ml
index 6c70089c6..8e471f220 100644
--- a/sledge/src/symbheap/sh.ml
+++ b/sledge/src/symbheap/sh.ml
@@ -133,9 +133,7 @@ let rec fv_union init q =
 let fv q = fv_union Var.Set.empty q
 
 let invariant_pure = function
-  | Term.Integer {data; typ} ->
-      assert (Typ.equal Typ.bool typ) ;
-      assert (not (Z.is_false data))
+  | Term.Integer {data} -> assert (not (Z.is_false data))
   | _ -> assert true
 
 let invariant_seg _ = ()
@@ -381,17 +379,15 @@ let rec pure (e : Term.t) =
   ;
   let us = Term.fv e in
   let eq_false b =
-    let cong = Equality.and_eq b (Term.bool false) Equality.true_ in
+    let cong = Equality.and_eq b Term.false_ Equality.true_ in
     {emp with us; cong; pure= [e]}
   in
   ( match e with
-  | Integer {data; typ= _} -> if Z.is_false data then false_ us else emp
+  | Integer {data} -> if Z.is_false data then false_ us else emp
   (* ¬b ==> false = b *)
-  | App {op= App {op= Xor; arg= Integer {data; typ= _}}; arg}
-    when Z.is_true data ->
+  | App {op= App {op= Xor; arg= Integer {data}}; arg} when Z.is_true data ->
       eq_false arg
-  | App {op= App {op= Xor; arg}; arg= Integer {data; typ= _}}
-    when Z.is_true data ->
+  | App {op= App {op= Xor; arg}; arg= Integer {data}} when Z.is_true data ->
       eq_false arg
   | App {op= App {op= And; arg= e1}; arg= e2} -> star (pure e1) (pure e2)
   | App {op= App {op= Or; arg= e1}; arg= e2} -> or_ (pure e1) (pure e2)
@@ -399,7 +395,7 @@ let rec pure (e : Term.t) =
     ->
       or_
         (star (pure cnd) (pure thn))
-        (star (pure (Term.not_ Typ.bool cnd)) (pure els))
+        (star (pure (Term.not_ 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
diff --git a/sledge/src/symbheap/sh_domain.ml b/sledge/src/symbheap/sh_domain.ml
index 2cbd543ba..d4f4bcb5a 100644
--- a/sledge/src/symbheap/sh_domain.ml
+++ b/sledge/src/symbheap/sh_domain.ml
@@ -21,7 +21,7 @@ let init globals =
   Vector.fold globals ~init:Sh.emp ~f:(fun q -> function
     | {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 len = Term.integer (Z.of_int siz) in
         let arr = Term.of_exp arr in
         Sh.star q (Sh.seg {loc; bas= loc; len; siz= len; arr})
     | _ -> q )
diff --git a/sledge/src/symbheap/sh_test.ml b/sledge/src/symbheap/sh_test.ml
index 0e6cab0ca..a70cecbe7 100644
--- a/sledge/src/symbheap/sh_test.ml
+++ b/sledge/src/symbheap/sh_test.ml
@@ -13,7 +13,7 @@ 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 = Term.integer (Z.of_int i) Typ.siz
+    let ( ! ) i = Term.integer (Z.of_int i)
     let ( = ) = Term.eq
     let wrt = Var.Set.empty
     let x_, wrt = Var.fresh "x" ~wrt
diff --git a/sledge/src/symbheap/solver.ml b/sledge/src/symbheap/solver.ml
index b1f0c1cda..fd6d6f07a 100644
--- a/sledge/src/symbheap/solver.ml
+++ b/sledge/src/symbheap/solver.ml
@@ -62,7 +62,7 @@ let single_existential_occurrence xs term =
 
 let special_cases xs = function
   | 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
+      if Set.is_subset (Term.fv e) ~of_:xs then Term.true_ else e
   | e -> e
 
 let excise_term ({us; min; xs} as goal) pure term =
@@ -136,7 +136,7 @@ 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 = Term.integer o_n Typ.siz in
+  let o_n = Term.integer o_n 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
@@ -147,8 +147,7 @@ let excise_seg_sub_prefix ({us; com; min; xs; sub; zs} as goal) msg ssg o_n
          (Term.concat
             [|Term.memory ~siz:n ~arr:a0; Term.memory ~siz:o_n ~arr:a1|]))
       (Sh.star
-         (Sh.seg
-            {loc= Term.add Typ.ptr k n; bas= b; len= m; siz= o_n; arr= a1})
+         (Sh.seg {loc= Term.add k n; bas= b; len= m; siz= o_n; arr= a1})
          (Sh.rem_seg msg min))
   in
   let sub =
@@ -178,7 +177,7 @@ 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 = Term.integer n_o Typ.siz in
+  let n_o = Term.integer n_o 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
@@ -193,11 +192,7 @@ let excise_seg_min_prefix ({us; com; min; xs; sub; zs} as goal) msg ssg n_o
                (Term.memory ~siz:n ~arr:a'))
             (Sh.star
                (Sh.seg
-                  { loc= Term.add Typ.ptr l o
-                  ; bas= b'
-                  ; len= m'
-                  ; siz= n_o
-                  ; arr= a1' })
+                  {loc= Term.add l o; bas= b'; len= m'; siz= n_o; arr= a1'})
                (Sh.rem_seg ssg sub))))
   in
   {goal with us; com; min; xs; sub; zs}
@@ -222,7 +217,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 = Term.integer l_k Typ.siz in
+  let l_k = Term.integer l_k 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 =
@@ -265,9 +260,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 = 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 l_k = Term.integer l_k in
+  let ko_ln = Term.integer ko_ln in
+  let ln = Term.add 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
@@ -315,10 +310,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 = 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 l_k = Term.integer l_k in
+  let ko_l = Term.integer ko_l in
+  let ln_ko = Term.integer ln_ko in
+  let ko = Term.add 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
@@ -371,7 +366,7 @@ 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 = Term.integer k_l Typ.siz in
+  let k_l = Term.integer k_l 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
@@ -412,9 +407,9 @@ 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 = 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 k_l = Term.integer k_l in
+  let ln_ko = Term.integer ln_ko in
+  let ko = Term.add 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
@@ -458,10 +453,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 = 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 k_l = Term.integer k_l in
+  let ln_k = Term.integer ln_k in
+  let ko_ln = Term.integer ko_ln in
+  let ln = Term.add 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
@@ -513,8 +508,8 @@ let excise_seg ({sub} as goal) msg ssg =
     match[@warning "-p"] Z.sign k_l with
     (* k-l < 0 so k < l *)
     | -1 -> (
-        let ko = Term.add Typ.ptr k o in
-        let ln = Term.add Typ.ptr l n in
+        let ko = Term.add k o in
+        let ln = Term.add l n in
         Equality.difference sub.cong ko ln
         >>= fun ko_ln ->
         match[@warning "-p"] Z.sign ko_ln with
@@ -553,8 +548,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 = Term.add Typ.ptr k o in
-        let ln = Term.add Typ.ptr l n in
+        let ko = Term.add k o in
+        let ln = Term.add 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 ce488ceef..bcd34589f 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 = Term.integer (Z.of_int i) Typ.siz
-    let ( + ) = Term.add Typ.ptr
-    let ( - ) = Term.sub Typ.siz
-    let ( * ) = Term.mul Typ.siz
+    let ( ! ) i = Term.integer (Z.of_int i)
+    let ( + ) = Term.add
+    let ( - ) = Term.sub
+    let ( * ) = Term.mul
     let wrt = Var.Set.empty
     let a_, wrt = Var.fresh "a" ~wrt
     let a2_, wrt = Var.fresh "a" ~wrt
diff --git a/sledge/src/symbheap/term.ml b/sledge/src/symbheap/term.ml
index c05aa5a44..5b2a5598d 100644
--- a/sledge/src/symbheap/term.ml
+++ b/sledge/src/symbheap/term.ml
@@ -20,8 +20,8 @@ module rec T : sig
 
   type t =
     (* nary: arithmetic, numeric and pointer *)
-    | Add of {args: qset; typ: Typ.t}
-    | Mul of {args: qset; typ: Typ.t}
+    | Add of {args: qset}
+    | Mul of {args: qset}
     (* pointer and memory constants and operations *)
     | Splat of {byt: t; siz: t}
     | Memory of {siz: t; arr: t}
@@ -62,7 +62,7 @@ module rec T : sig
     | Extract of {unsigned: bool; bits: int}
     | Convert of {unsigned: bool; dst: Typ.t; src: Typ.t}
     (* numeric constants *)
-    | Integer of {data: Z.t; typ: Typ.t}
+    | Integer of {data: Z.t}
     | Float of {data: string}
   [@@deriving compare, equal, hash, sexp]
 
@@ -82,8 +82,8 @@ 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}
+    | Add of {args: qset}
+    | Mul of {args: qset}
     | Splat of {byt: t; siz: t}
     | Memory of {siz: t; arr: t}
     | Concat of {args: t vector}
@@ -114,15 +114,15 @@ and T0 : sig
     | Struct_rec of {elts: t vector}
     | Extract of {unsigned: bool; bits: int}
     | Convert of {unsigned: bool; dst: Typ.t; src: Typ.t}
-    | Integer of {data: Z.t; typ: Typ.t}
+    | Integer of {data: Z.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}
+    | Add of {args: qset}
+    | Mul of {args: qset}
     | Splat of {byt: t; siz: t}
     | Memory of {siz: t; arr: t}
     | Concat of {args: t vector}
@@ -153,7 +153,7 @@ end = struct
     | Struct_rec of {elts: t vector}
     | Extract of {unsigned: bool; bits: int}
     | Convert of {unsigned: bool; dst: Typ.t; src: Typ.t}
-    | Integer of {data: Z.t; typ: Typ.t}
+    | Integer of {data: Z.t}
     | Float of {data: string}
   [@@deriving compare, equal, hash, sexp]
 end
@@ -207,7 +207,6 @@ let rec pp ?is_x fs term =
         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
@@ -308,30 +307,6 @@ 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}} -> Some Typ.bool
-  | App
-      { op= App {op= Div | Rem | 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 is_boolean e = Option.exists ~f:(Typ.equal Typ.bool) (typ_of e)
-
-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
@@ -342,11 +317,9 @@ let rec assert_indeterminate = function
  *     ∏ᵢ xᵢ^nᵢ
  * for (non-constant) indeterminants xᵢ and positive integer exponents nᵢ
  *)
-let assert_monomial add_typ mono =
+let assert_monomial mono =
   match mono with
-  | Mul {typ; args} ->
-      assert (Typ.castable add_typ typ) ;
-      assert (Option.is_some (Typ.prim_bit_size_of typ)) ;
+  | Mul {args} ->
       Qset.iter args ~f:(fun factor exponent ->
           assert (Q.sign exponent > 0) ;
           assert_indeterminate factor |> Fn.id )
@@ -355,7 +328,7 @@ let assert_monomial add_typ mono =
 (* a polynomial term is a monomial multiplied by a non-zero coefficient
  *     c × ∏ᵢ xᵢ
  *)
-let assert_poly_term add_typ mono coeff =
+let assert_poly_term mono coeff =
   assert (not (Q.equal Q.zero coeff)) ;
   match mono with
   | Integer {data} -> assert (Z.equal Z.one data)
@@ -364,8 +337,8 @@ let assert_poly_term add_typ mono coeff =
       | 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
+      assert_monomial mono |> Fn.id
+  | _ -> assert_monomial mono |> Fn.id
 
 (* a polynomial is a linear combination of monomials, e.g.
  *     ∑ᵢ cᵢ × ∏ⱼ xᵢⱼ
@@ -374,13 +347,12 @@ let assert_poly_term add_typ mono coeff =
  *)
 let assert_polynomial poly =
   match poly with
-  | Add {typ; args} ->
+  | Add {args} ->
       ( match Qset.min_elt args with
-      | None -> assert false
-      | Some (Integer _, _) -> assert false
+      | None | 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)
+      Qset.iter args ~f:(fun m c -> assert_poly_term m c |> Fn.id)
   | _ -> assert false
 
 let invariant ?(partial = false) e =
@@ -393,41 +365,23 @@ let invariant ?(partial = false) e =
   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
+  | Integer _ -> assert_arity 0
   | Var _ | Nondet _ | Label _ | Float _ -> assert_arity 0
   | Extract _ -> assert_arity 1
   | 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_arity 1 ;
       assert (Typ.convertible src dst)
   | Add _ -> assert_polynomial e |> Fn.id
-  | Mul {typ} -> assert_monomial typ e |> Fn.id
+  | Mul _ -> assert_monomial e |> Fn.id
   | Eq | Dq | Gt | Ge | Lt | Le | Div | Rem | 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 )
+   |Ashr ->
+      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))
+  | Splat {siz} -> (
+    match siz with
+    | Integer {data} -> assert (not (Z.equal Z.zero data))
+    | _ -> () )
+  | Memory _ -> assert true
   | Ord | Uno | Select -> assert_arity 2
   | Conditional | Update -> assert_arity 3
   | Record -> assert (partial || not (List.is_empty args))
@@ -581,24 +535,19 @@ let fv e = fold_vars e ~f:Set.add ~init:Var.Set.empty
 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 integer data = Integer {data} |> check invariant
+let null = integer Z.zero
+let zero = integer Z.zero
+let one = integer Z.one
+let minus_one = integer Z.minus_one
+let bool b = integer (Z.of_bool b)
+let true_ = bool true
+let false_ = bool false
 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_extract ~unsigned bits arg =
   match arg with
-  | Integer {data} ->
-      integer (Z.extract ~unsigned bits data) (Typ.integer ~bits)
+  | Integer {data} -> integer (Z.extract ~unsigned bits data)
   | _ -> App {op= Extract {unsigned; bits}; arg}
 
 let simp_convert ~unsigned dst src arg =
@@ -606,7 +555,7 @@ let simp_convert ~unsigned dst src arg =
   else
     match (dst, src, arg) with
     | Integer {bits= m}, Integer {bits= n}, Integer {data} ->
-        integer (Z.extract ~unsigned (min m n) data) dst
+        integer (Z.extract ~unsigned (min m n) data)
     | _ -> App {op= Convert {unsigned; dst; src}; arg}
 
 let simp_gt x y =
@@ -637,37 +586,37 @@ let sum_mul_const const sum =
   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 =
+let rec sum_to_term sum =
   match Qset.length sum with
-  | 0 -> zero typ
+  | 0 -> zero
   | 1 -> (
     match Qset.min_elt sum with
-    | Some (Integer _, q) -> rational q typ
+    | Some (Integer _, q) -> rational q
     | Some (arg, q) when Q.equal Q.one q -> arg
-    | _ -> Add {typ; args= sum} )
-  | _ -> Add {typ; args= sum}
+    | _ -> Add {args= sum} )
+  | _ -> Add {args= sum}
 
-and rational Q.{num; den} typ = simp_div (integer num typ) (integer den typ)
+and rational Q.{num; den} = simp_div (integer num) (integer den)
 
 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) ->
-      integer (Z.div i j) typ
+  | Integer {data= i}, Integer {data= j} when not (Z.equal Z.zero j) ->
+      integer (Z.div i j)
   (* 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)
+  | Add {args}, Integer {data} ->
+      sum_to_term (sum_mul_const Q.(inv (of_z data)) args)
   | _ -> App {op= App {op= Div; 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) ->
-      integer (Z.rem i j) typ
+  | Integer {data= i}, Integer {data= j} when not (Z.equal Z.zero j) ->
+      integer (Z.rem i j)
   (* e % 1 ==> 0 *)
-  | _, Integer {data; typ} when Z.equal Z.one data -> integer Z.zero typ
+  | _, Integer {data} when Z.equal Z.one data -> zero
   | _ -> App {op= App {op= Rem; arg= x}; arg= y}
 
 (* Sums of polynomial terms represented by multisets. A sum ∑ᵢ cᵢ × Xᵢ of
@@ -681,8 +630,7 @@ module Sum = struct
     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)
+    | Integer {data} -> Qset.add sum one Q.(coeff * of_z data)
     | _ -> Qset.add sum term coeff
 
   let singleton ?(coeff = Q.one) term = add coeff term empty
@@ -694,7 +642,7 @@ module Sum = struct
   let to_term = sum_to_term
 end
 
-let rec simp_add_ typ es poly =
+let rec simp_add_ es poly =
   (* (coeff × term) + poly *)
   let f term coeff poly =
     match (term, poly) with
@@ -704,18 +652,18 @@ let rec simp_add_ typ es poly =
     | 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
+        rational Q.((coeff * of_z i) + of_z j)
     (* (c × ∑ᵢ cᵢ × Xᵢ) + s ==> (∑ᵢ (c × cᵢ) × Xᵢ) + s *)
-    | Add {args}, _ -> simp_add_ typ (Sum.mul_const coeff args) poly
+    | Add {args}, _ -> simp_add_ (Sum.mul_const coeff args) poly
     (* (c₀ × X₀) + (∑ᵢ₌₁ⁿ cᵢ × Xᵢ) ==> ∑ᵢ₌₀ⁿ cᵢ × Xᵢ *)
-    | _, Add {args} -> Sum.to_term typ (Sum.add coeff term args)
+    | _, Add {args} -> Sum.to_term (Sum.add coeff term args)
     (* (c₁ × X₁) + X₂ ==> ∑ᵢ₌₁² cᵢ × Xᵢ for c₂ = 1 *)
-    | _ -> Sum.to_term typ (Sum.add coeff term (Sum.singleton poly))
+    | _ -> Sum.to_term (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
+let simp_add es = simp_add_ es zero
+let simp_add2 e f = simp_add_ (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
@@ -731,58 +679,56 @@ module Prod = struct
   let union = Qset.union
 end
 
-let rec simp_mul2 typ e f =
+let rec simp_mul2 e f =
   match (e, f) with
   (* c₁ × c₂ ==> c₁×c₂ *)
-  | Integer {data= i}, Integer {data= j} -> integer (Z.mul i j) typ
+  | Integer {data= i}, Integer {data= j} -> integer (Z.mul i j)
   (* 0 × f ==> 0 *)
   | Integer {data}, _ when Z.equal Z.zero data -> e
   (* e × 0 ==> 0 *)
   | _, Integer {data} when Z.equal Z.zero data -> f
   (* c × (∑ᵤ cᵤ × ∏ⱼ yᵤⱼ) ==> ∑ᵤ c × cᵤ × ∏ⱼ yᵤⱼ *)
   | Integer {data}, Add {args} | Add {args}, Integer {data} ->
-      Sum.to_term typ (Sum.mul_const (Q.of_z data) args)
+      Sum.to_term (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)
+      Sum.to_term (Sum.singleton ~coeff:(Q.of_z c) x)
   (* (∏ᵤ₌₀ⁱ xᵤ) × (∏ᵥ₌ᵢ₊₁ⁿ xᵥ) ==> ∏ⱼ₌₀ⁿ xⱼ *)
-  | Mul {args= xs1}, Mul {args= xs2} -> Mul {typ; args= Prod.union xs1 xs2}
+  | Mul {args= xs1}, Mul {args= xs2} -> Mul {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.to_term
         (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} ))
+          | Mul {args} -> Mul {args= Prod.union prod args}
+          | Integer _ as c -> simp_mul2 c m
+          | mono -> Mul {args= Prod.add mono prod} ))
   (* x₀ × (∏ᵢ₌₁ⁿ xᵢ) ==> ∏ᵢ₌₀ⁿ xᵢ *)
-  | Mul {args= xs1}, x | x, Mul {args= xs1} ->
-      Mul {typ; args= Prod.add x xs1}
+  | Mul {args= xs1}, x | x, Mul {args= xs1} -> Mul {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)
+      simp_add (Sum.map ~f:(fun m -> simp_mul2 e m) args)
   (* x₁ × x₂ ==> ∏ᵢ₌₁² xᵢ *)
-  | _ -> Mul {args= Prod.add e (Prod.singleton f); typ}
+  | _ -> Mul {args= Prod.add e (Prod.singleton f)}
 
-let simp_mul typ es =
+let simp_mul es =
   (* (bas ^ pwr) × term *)
   let rec mul_pwr bas pwr term =
     if Q.equal Q.zero pwr then term
-    else mul_pwr bas Q.(pwr - one) (simp_mul2 typ bas term)
+    else mul_pwr bas Q.(pwr - one) (simp_mul2 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_negate x = simp_mul2 minus_one x
 
-let simp_sub typ x y =
+let simp_sub x y =
   match (x, y) with
   (* i - j *)
-  | Integer {data= i}, Integer {data= j} -> integer (Z.sub i j) typ
+  | Integer {data= i}, Integer {data= j} -> integer (Z.sub i j)
   (* x - y ==> x + (-1 * y) *)
-  | _ -> simp_add2 typ x (simp_negate typ y)
+  | _ -> simp_add2 x (simp_negate y)
 
 let simp_cond cnd thn els =
   match cnd with
@@ -796,7 +742,7 @@ let simp_cond cnd thn els =
 let rec simp_and x y =
   match (x, y) with
   (* i && j *)
-  | Integer {data= i; typ}, Integer {data= j} -> integer (Z.logand i j) typ
+  | Integer {data= i}, Integer {data= j} -> integer (Z.logand i j)
   (* e && true ==> e *)
   | (Integer {data}, e | e, Integer {data}) when Z.is_true data -> e
   (* e && false ==> 0 *)
@@ -814,7 +760,7 @@ let rec simp_and x y =
 let rec simp_or x y =
   match (x, y) with
   (* i || j *)
-  | Integer {data= i; typ}, Integer {data= j} -> integer (Z.logor i j) typ
+  | Integer {data= i}, Integer {data= j} -> integer (Z.logor i j)
   (* e || true ==> true *)
   | ((Integer {data} as t), _ | _, (Integer {data} as t))
     when Z.is_true data ->
@@ -829,7 +775,18 @@ let rec simp_or x y =
   | _ when equal x y -> x
   | _ -> App {op= App {op= Or; arg= x}; arg= y}
 
-let rec simp_not (typ : Typ.t) term =
+let rec is_boolean = function
+  | App {op= App {op= Eq | Dq | Gt | Ge | Lt | Le}}
+   |App {op= Convert {dst= Integer {bits= 1}}} ->
+      true
+  | App
+      { op= App {op= Div | Rem | And | Or | Xor | Shl | Lshr | Ashr; arg= x}
+      ; arg= y }
+   |App {op= App {op= App {op= Conditional}; arg= x}; arg= y} ->
+      is_boolean x || is_boolean y
+  | _ -> false
+
+let rec simp_not term =
   match term with
   (* ¬(x = y) ==> x ≠ y *)
   | App {op= App {op= Eq; arg= x}; arg= y} -> simp_dq x y
@@ -849,28 +806,26 @@ let rec simp_not (typ : Typ.t) term =
   | 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} ->
-      simp_or (simp_not typ x) (simp_not typ y)
+      simp_or (simp_not x) (simp_not y)
   (* ¬(a ∨ b) ==> ¬a ∧ ¬b *)
   | App {op= App {op= Or; arg= x}; arg= y} ->
-      simp_and (simp_not typ x) (simp_not typ y)
+      simp_and (simp_not x) (simp_not y)
   (* ¬(c ? t : e) ==> c ? ¬t : ¬e *)
   | App {op= App {op= App {op= Conditional; arg= cnd}; arg= thn}; arg= els}
     ->
-      simp_cond cnd (simp_not typ thn) (simp_not typ els)
+      simp_cond cnd (simp_not thn) (simp_not els)
   (* ¬i ==> -i-1 *)
-  | Integer {data; typ} -> integer (Z.lognot data) typ
+  | Integer {data} -> integer (Z.lognot data)
   (* ¬e ==> true xor e *)
-  | e -> App {op= App {op= Xor; arg= integer (Z.of_bool true) typ}; arg= e}
+  | e -> App {op= App {op= Xor; arg= true_}; arg= e}
 
 and simp_eq x y =
   match (x, y) with
   (* i = j *)
   | Integer {data= i}, Integer {data= j} -> bool (Z.equal i j)
   (* b = false ==> ¬b *)
-  | b, Integer {data} when Z.is_false data && is_boolean b ->
-      simp_not Typ.bool b
-  | Integer {data}, b when Z.is_false data && is_boolean b ->
-      simp_not Typ.bool b
+  | b, Integer {data} when Z.is_false data && is_boolean b -> simp_not b
+  | Integer {data}, b when Z.is_false data && is_boolean b -> simp_not b
   (* b = true ==> b *)
   | b, Integer {data} when Z.is_true data && is_boolean b -> b
   | Integer {data}, b when Z.is_true data && is_boolean b -> b
@@ -892,24 +847,22 @@ and simp_dq x y =
     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 )
+    | b -> simp_not b )
 
 let simp_xor x y =
   match (x, y) with
   (* i xor j *)
-  | Integer {data= i; typ}, Integer {data= j} -> integer (Z.logxor i j) typ
+  | Integer {data= i}, Integer {data= j} -> integer (Z.logxor i j)
   (* true xor b ==> ¬b *)
-  | Integer {data}, b when Z.is_true data && is_boolean b ->
-      simp_not Typ.bool b
-  | b, Integer {data} when Z.is_true data && is_boolean b ->
-      simp_not Typ.bool b
+  | Integer {data}, b when Z.is_true data && is_boolean b -> simp_not b
+  | b, Integer {data} when Z.is_true data && is_boolean b -> simp_not b
   | _ -> 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 {data= j} when Z.sign j >= 0 ->
-      integer (Z.shift_left i (Z.to_int j)) typ
+  | Integer {data= i}, Integer {data= j} when Z.sign j >= 0 ->
+      integer (Z.shift_left i (Z.to_int j))
   (* e shl 0 ==> e *)
   | e, Integer {data} when Z.equal Z.zero data -> e
   | _ -> App {op= App {op= Shl; arg= x}; arg= y}
@@ -917,8 +870,8 @@ let simp_shl x y =
 let simp_lshr x y =
   match (x, y) with
   (* i lshr j *)
-  | Integer {data= i; typ}, Integer {data= j} when Z.sign j >= 0 ->
-      integer (Z.shift_right_trunc i (Z.to_int j)) typ
+  | Integer {data= i}, Integer {data= j} when Z.sign j >= 0 ->
+      integer (Z.shift_right_trunc i (Z.to_int j))
   (* e lshr 0 ==> e *)
   | e, Integer {data} when Z.equal Z.zero data -> e
   | _ -> App {op= App {op= Lshr; arg= x}; arg= y}
@@ -926,8 +879,8 @@ let simp_lshr x y =
 let simp_ashr x y =
   match (x, y) with
   (* i ashr j *)
-  | Integer {data= i; typ}, Integer {data= j} when Z.sign j >= 0 ->
-      integer (Z.shift_right i (Z.to_int j)) typ
+  | Integer {data= i}, Integer {data= j} when Z.sign j >= 0 ->
+      integer (Z.shift_right i (Z.to_int j))
   (* e ashr 0 ==> e *)
   | e, Integer {data} when Z.equal Z.zero data -> e
   | _ -> App {op= App {op= Ashr; arg= x}; arg= y}
@@ -1005,22 +958,10 @@ let app1 ?(partial = false) op arg =
 
 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 addN args = simp_add args |> check invariant
+let mulN args = simp_mul args |> 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 memory ~siz ~arr = simp_memory siz arr |> check invariant
 
 let simp_concat xs =
   if Vector.length xs = 1 then Vector.get xs 0
@@ -1044,11 +985,7 @@ let simp_splat byt siz =
   | 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 splat ~byt ~siz = simp_splat byt siz |> check invariant
 let eq = app2 Eq
 let dq = app2 Dq
 let gt = app2 Gt
@@ -1057,16 +994,16 @@ let lt = app2 Lt
 let le = app2 Le
 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 neg = simp_negate
+let add = simp_add2
+let sub = simp_sub
+let mul = simp_mul2
 let div = app2 Div
 let rem = app2 Rem
 let and_ = app2 And
 let or_ = app2 Or
 let xor = app2 Xor
-let not_ = check1 simp_not
+let not_ = simp_not
 let shl = app2 Shl
 let lshr = app2 Lshr
 let ashr = app2 Ashr
@@ -1103,6 +1040,10 @@ let extract ?(unsigned = false) ~bits term =
 let convert ?(unsigned = false) ~dst ~src term =
   app1 (Convert {unsigned; dst; src}) term
 
+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))) else None )
+
 let rec of_exp (e : Exp.t) =
   let unsigned op typ x y =
     match Typ.prim_bit_size_of typ with
@@ -1116,14 +1057,12 @@ let rec of_exp (e : Exp.t) =
   | Reg {name} -> var (Var {id= 0; name})
   | Nondet {msg} -> nondet msg
   | Label {parent; name} -> label ~parent ~name
-  | Integer {data; typ= Integer {bits} as typ} ->
-      integer (Z.signed_extract data 0 bits) typ
-  | Integer {data; typ} -> integer data typ
+  | Integer {data} -> integer data
   | Float {data} -> float data
   | Ap1 (Convert {unsigned; dst}, src, arg) ->
       convert ~unsigned ~dst ~src (of_exp arg)
   | Ap1 (Select idx, _, arg) ->
-      select ~rcd:(of_exp arg) ~idx:(integer (Z.of_int idx) Typ.siz)
+      select ~rcd:(of_exp arg) ~idx:(integer (Z.of_int idx))
   | Ap2 (Eq, _, x, y) -> eq (of_exp x) (of_exp y)
   | Ap2 (Dq, _, x, y) -> dq (of_exp x) (of_exp y)
   | Ap2 (Gt, _, x, y) -> gt (of_exp x) (of_exp y)
@@ -1136,9 +1075,9 @@ let rec of_exp (e : Exp.t) =
   | Ap2 (Ule, typ, x, y) -> unsigned le typ x y
   | Ap2 (Ord, _, x, y) -> ord (of_exp x) (of_exp y)
   | Ap2 (Uno, _, x, y) -> uno (of_exp x) (of_exp y)
-  | Ap2 (Add, typ, x, y) -> add typ (of_exp x) (of_exp y)
-  | Ap2 (Sub, typ, x, y) -> sub typ (of_exp x) (of_exp y)
-  | Ap2 (Mul, typ, x, y) -> mul typ (of_exp x) (of_exp y)
+  | Ap2 (Add, _, x, y) -> add (of_exp x) (of_exp y)
+  | Ap2 (Sub, _, x, y) -> sub (of_exp x) (of_exp y)
+  | Ap2 (Mul, _, x, y) -> mul (of_exp x) (of_exp y)
   | Ap2 (Div, _, x, y) -> div (of_exp x) (of_exp y)
   | Ap2 (Rem, _, x, y) -> rem (of_exp x) (of_exp y)
   | Ap2 (Udiv, typ, x, y) -> unsigned div typ x y
@@ -1151,7 +1090,7 @@ let rec of_exp (e : Exp.t) =
   | Ap2 (Ashr, _, x, y) -> ashr (of_exp x) (of_exp y)
   | Ap2 (Update idx, _, rcd, elt) ->
       update ~rcd:(of_exp rcd) ~elt:(of_exp elt)
-        ~idx:(integer (Z.of_int idx) Typ.siz)
+        ~idx:(integer (Z.of_int idx))
   | Ap3 (Conditional, _, cnd, thn, els) ->
       conditional ~cnd:(of_exp cnd) ~thn:(of_exp thn) ~els:(of_exp els)
   | ApN (Record, _, elts) ->
@@ -1162,11 +1101,6 @@ let rec of_exp (e : Exp.t) =
         ~id:e
         (Vector.map elts ~f:(fun e -> lazy (of_exp e)))
 
-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 =
@@ -1181,14 +1115,14 @@ let map e ~f =
       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 map_qset mk ~f args =
       let args' = Qset.map ~f:(fun arg q -> (f arg, q)) args in
-      if args' == args then e else mk typ args'
+      if args' == args then e else mk 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
+    | Add {args} -> map_qset addN ~f args
+    | Mul {args} -> map_qset mulN ~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
@@ -1246,23 +1180,21 @@ let solve e f =
           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
-          )
+      Vector.fold_until args ~init:zero
+        ~f:(fun sum -> function Memory {siz} -> Continue (add 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 _ | Mul _ | Integer _), _ | _, (Add _ | Mul _ | Integer _) -> (
+      match sub 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 n = Sum.to_term (Qset.remove args c) in
+          let d = rational (Q.neg q) in
           let r = div n d in
           Some (Map.add_exn s ~key:c ~data:r)
-      | e_f -> solve_uninterp e_f (zero typ) )
+      | e_f -> solve_uninterp e_f zero )
     | 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
diff --git a/sledge/src/symbheap/term.mli b/sledge/src/symbheap/term.mli
index 23bb4958f..9228a7742 100644
--- a/sledge/src/symbheap/term.mli
+++ b/sledge/src/symbheap/term.mli
@@ -21,8 +21,8 @@ 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 *)
+  | Add of {args: qset}  (** Addition *)
+  | Mul of {args: qset}  (** Multiplication *)
   | Splat of {byt: t; siz: t}
       (** Iterated concatenation of a single byte *)
   | Memory of {siz: t; arr: t}  (** Size-tagged byte-array *)
@@ -67,7 +67,7 @@ and t = private
           integer. If [src] is a [Float] type and [dst] is an [Integer]
           type, then [unsigned] indidates that the result should be the
           nearest non-negative value. *)
-  | Integer of {data: Z.t; typ: Typ.t}
+  | Integer of {data: Z.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 *)
@@ -127,17 +127,21 @@ 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 true_ : t
+val false_ : t
 val null : t
+val zero : t
+val one : t
+val minus_one : 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 integer : Z.t -> t
+val rational : Q.t -> t
 val float : string -> t
 val eq : t -> t -> t
 val dq : t -> t -> t
@@ -147,16 +151,16 @@ val lt : t -> t -> t
 val le : 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 neg : t -> t
+val add : t -> t -> t
+val sub : t -> t -> t
+val mul : t -> t -> t
 val div : t -> t -> t
 val rem : 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 not_ : t -> t
 val shl : t -> t -> t
 val lshr : t -> t -> t
 val ashr : t -> t -> t
@@ -167,6 +171,7 @@ val update : rcd:t -> elt:t -> idx:t -> t
 val extract : ?unsigned:bool -> bits:int -> t -> t
 val convert : ?unsigned:bool -> dst:Typ.t -> src:Typ.t -> t -> t
 val size_of : Typ.t -> t option
+val of_exp : Exp.t -> t
 
 (** Access *)
 
@@ -185,6 +190,5 @@ val rename : Var.Subst.t -> t -> t
 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/symbheap/term_test.ml b/sledge/src/symbheap/term_test.ml
index 893864cd3..7a93ca492 100644
--- a/sledge/src/symbheap/term_test.ml
+++ b/sledge/src/symbheap/term_test.ml
@@ -10,11 +10,10 @@ let%test_module _ =
     (* let () = Trace.init ~margin:68 ~config:all () *)
     let () = Trace.init ~margin:68 ~config:none ()
     let pp = Format.printf "@\n%a@." Term.pp
-    let char = Typ.integer ~bits:8
-    let ( ! ) i = Term.integer (Z.of_int i) char
-    let ( + ) = Term.add char
-    let ( - ) = Term.sub char
-    let ( * ) = Term.mul char
+    let ( ! ) i = Term.integer (Z.of_int i)
+    let ( + ) = Term.add
+    let ( - ) = Term.sub
+    let ( * ) = Term.mul
     let ( = ) = Term.eq
     let ( != ) = Term.dq
     let ( > ) = Term.gt
@@ -23,7 +22,7 @@ let%test_module _ =
     let ( <= ) = Term.le
     let ( && ) = Term.and_
     let ( || ) = Term.or_
-    let ( ~~ ) = Term.not_ Typ.bool
+    let ( ~~ ) = Term.not_
     let wrt = Var.Set.empty
     let y_, wrt = Var.fresh "y" ~wrt
     let z_, _ = Var.fresh "z" ~wrt
@@ -31,16 +30,10 @@ let%test_module _ =
     let z = Term.var z_
 
     let%test "booleans distinct" =
-      Term.is_false
-        (Term.eq
-           (Term.integer Z.minus_one Typ.bool)
-           (Term.integer Z.zero Typ.bool))
+      Term.is_false (Term.eq Term.minus_one Term.zero)
 
     let%test "unsigned booleans distinct" =
-      Term.is_false
-        (Term.eq
-           (Term.integer Z.one Typ.bool)
-           (Term.integer Z.zero Typ.bool))
+      Term.is_false (Term.eq Term.one Term.zero)
 
     let%test "boolean overflow" =
       Term.is_true
@@ -182,19 +175,19 @@ let%test_module _ =
       [%expect {| 0 |}]
 
     let%expect_test _ =
-      pp (!3 * y = z = Term.bool true) ;
+      pp (!3 * y = z = Term.true_) ;
       [%expect {| ((3 × %y_1) = %z_2) |}]
 
     let%expect_test _ =
-      pp (Term.bool true = (!3 * y = z)) ;
+      pp (Term.true_ = (!3 * y = z)) ;
       [%expect {| ((3 × %y_1) = %z_2) |}]
 
     let%expect_test _ =
-      pp (!3 * y = z = Term.bool false) ;
+      pp (!3 * y = z = Term.false_) ;
       [%expect {| ((3 × %y_1) ≠ %z_2) |}]
 
     let%expect_test _ =
-      pp (Term.bool false = (!3 * y = z)) ;
+      pp (Term.false_ = (!3 * y = z)) ;
       [%expect {| ((3 × %y_1) ≠ %z_2) |}]
 
     let%expect_test _ =
@@ -214,11 +207,11 @@ let%test_module _ =
       [%expect {| ((-3 × %y_1 + 4) = %y_1) |}]
 
     let%expect_test _ =
-      pp (Term.sub Typ.bool (Term.bool true) (z = !4)) ;
+      pp (Term.sub Term.true_ (z = !4)) ;
       [%expect {| (-1 × (%z_2 = 4) + -1) |}]
 
     let%expect_test _ =
-      pp (Term.add Typ.bool (Term.bool true) (z = !4) = (z = !4)) ;
+      pp (Term.add Term.true_ (z = !4) = (z = !4)) ;
       [%expect {| (((%z_2 = 4) + -1) = (%z_2 = 4)) |}]
 
     let%expect_test _ =
@@ -252,14 +245,14 @@ let%test_module _ =
     let%expect_test _ =
       pp Term.(eq z null) ;
       pp Term.(eq null z) ;
-      pp Term.(dq (eq null z) (bool false)) ;
+      pp Term.(dq (eq null z) false_) ;
       [%expect
         {|
-        (%z_2 = null)
+        (%z_2 = 0)
 
-        (null = %z_2)
+        (0 = %z_2)
 
-        (null = %z_2) |}]
+        (0 = %z_2) |}]
 
     let%expect_test _ =
       let z1 = z + !1 in