diff --git a/sledge/src/domain_sh.ml b/sledge/src/domain_sh.ml
index 2c8f10cf0..2081bed0c 100644
--- a/sledge/src/domain_sh.ml
+++ b/sledge/src/domain_sh.ml
@@ -30,8 +30,8 @@ let init globals =
             | _ -> violates Llair.GlobalDefn.invariant global
           in
           let len = Term.integer (Z.of_int siz) in
-          let seq = X.term seq in
-          Sh.star q (Sh.seg {loc; bas= loc; len; siz= len; seq})
+          let cnt = X.term seq in
+          Sh.star q (Sh.seg {loc; bas= loc; len; siz= len; cnt})
       | _ -> q )
 
 let join p q =
@@ -93,7 +93,7 @@ let garbage_collect (q : Sh.t) ~wrt =
       let new_set =
         List.fold q.heap current ~f:(fun seg current ->
             if value_determined_by q.ctx current seg.loc then
-              List.fold (Context.class_of q.ctx seg.seq) current
+              List.fold (Context.class_of q.ctx seg.cnt) current
                 ~f:(fun e c ->
                   Term.Set.union c (Term.Set.of_iter (Term.atoms e)) )
             else current )
@@ -324,9 +324,9 @@ let%test_module _ =
     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; seq= a}
-    let seg_a = Sh.seg {loc= a; bas= b; len= n; siz= n; seq= endV}
-    let seg_cycle = Sh.seg {loc= a; bas= b; len= n; siz= n; seq= main}
+    let seg_main = Sh.seg {loc= main; bas= b; len= n; siz= n; cnt= a}
+    let seg_a = Sh.seg {loc= a; bas= b; len= n; siz= n; cnt= endV}
+    let seg_cycle = Sh.seg {loc= a; bas= b; len= n; siz= n; cnt= main}
 
     let%expect_test _ =
       pp (garbage_collect seg_main ~wrt:(Term.Set.of_list [])) ;
diff --git a/sledge/src/exec.ml b/sledge/src/exec.ml
index 9301bf3df..0401d215d 100644
--- a/sledge/src/exec.ml
+++ b/sledge/src/exec.ml
@@ -28,7 +28,7 @@ module Fresh : sig
        ?bas:Term.t
     -> ?len:Term.t
     -> ?siz:Term.t
-    -> ?seq:Term.t
+    -> ?cnt:Term.t
     -> Term.t
     -> Sh.seg t
   (** Segment with fresh variables for omitted arguments. *)
@@ -55,15 +55,15 @@ end = struct
     let xs = Var.Set.add x xs in
     return (Term.var x) {wrt; xs}
 
-  let seg ?bas ?len ?siz ?seq loc =
+  let seg ?bas ?len ?siz ?cnt loc =
     let freshen term nam =
       match term with Some term -> return term | None -> var nam
     in
     let* bas = freshen bas "b" in
     let* len = freshen len "m" in
     let* siz = freshen siz "n" in
-    let* seq = freshen seq "a" in
-    return Sh.{loc; bas; len; siz; seq}
+    let* cnt = freshen cnt "a" in
+    return Sh.{loc; bas; len; siz; cnt}
 
   let assign ~ws ~rs {wrt; xs} =
     let ovs = Var.Set.inter ws rs in
@@ -89,9 +89,11 @@ let gen_spec us specm =
 
 let null_eq ptr = Sh.pure (Formula.eq0 ptr)
 
-let eq_concat (siz, seq) ms =
-  Formula.eq (Term.sized ~siz ~seq)
-    (Term.concat (Array.map ~f:(fun (siz, seq) -> Term.sized ~siz ~seq) ms))
+let eq_concat (siz, cnt) ms =
+  Formula.eq
+    (Term.sized ~siz ~seq:cnt)
+    (Term.concat
+       (Array.map ~f:(fun (siz, cnt) -> Term.sized ~siz ~seq:cnt) ms))
 
 open Fresh.Import
 
@@ -123,7 +125,7 @@ let load_spec reg ptr len =
   let+ sub, ms = Fresh.assign ~ws:(Var.Set.of_ reg) ~rs:foot.us in
   let post =
     Sh.and_
-      (Formula.eq (Term.var reg) (Term.rename sub seg.seq))
+      (Formula.eq (Term.var reg) (Term.rename sub seg.cnt))
       (Sh.rename sub foot)
   in
   {foot; sub; ms; post}
@@ -135,7 +137,7 @@ let load_spec reg ptr len =
 let store_spec ptr exp len =
   let+ seg = Fresh.seg ptr ~siz:len in
   let foot = Sh.seg seg in
-  let post = Sh.seg {seg with seq= exp} in
+  let post = Sh.seg {seg with cnt= exp} in
   {foot; sub= Var.Subst.empty; ms= Var.Set.empty; post}
 
 (* { d-[b;m)->⟨l,α⟩ }
@@ -145,7 +147,7 @@ let store_spec ptr exp len =
 let memset_spec dst byt len =
   let+ seg = Fresh.seg dst ~siz:len in
   let foot = Sh.seg seg in
-  let post = Sh.seg {seg with seq= Term.splat byt} in
+  let post = Sh.seg {seg with cnt= Term.splat byt} in
   {foot; sub= Var.Subst.empty; ms= Var.Set.empty; post}
 
 (* { d=s * l=0 * d-[b;m)->⟨l,α⟩ }
@@ -170,7 +172,7 @@ let memcpy_dj_spec dst src len =
   let dst_heap = Sh.seg dst_seg in
   let+ src_seg = Fresh.seg src ~siz:len in
   let src_heap = Sh.seg src_seg in
-  let dst_seg' = {dst_seg with seq= src_seg.seq} in
+  let dst_seg' = {dst_seg with cnt= src_seg.cnt} in
   let dst_heap' = Sh.seg dst_seg' in
   let foot = Sh.star dst_heap src_heap in
   let post = Sh.star dst_heap' src_heap in
@@ -200,23 +202,23 @@ let memmov_dj_spec = memcpy_dj_spec
 let memmov_foot dst src len =
   let* bas = Fresh.var "b" in
   let* siz = Fresh.var "m" in
-  let* seq_dst = Fresh.var "a" in
-  let* seq_mid = Fresh.var "a" in
-  let* seq_src = Fresh.var "a" in
+  let* cnt_dst = Fresh.var "a" in
+  let* cnt_mid = Fresh.var "a" in
+  let* cnt_src = Fresh.var "a" in
   let src_dst = Term.sub src dst in
-  let mem_dst = (src_dst, seq_dst) in
+  let mem_dst = (src_dst, cnt_dst) in
   let siz_mid = Term.sub len src_dst in
-  let mem_mid = (siz_mid, seq_mid) in
-  let mem_src = (src_dst, seq_src) in
+  let mem_mid = (siz_mid, cnt_mid) in
+  let mem_src = (src_dst, cnt_src) in
   let mem_dst_mid_src = [|mem_dst; mem_mid; mem_src|] in
   let* siz_dst_mid_src = Fresh.var "m" in
-  let+ seq_dst_mid_src = Fresh.var "a" in
+  let+ cnt_dst_mid_src = Fresh.var "a" in
   let eq_mem_dst_mid_src =
-    eq_concat (siz_dst_mid_src, seq_dst_mid_src) mem_dst_mid_src
+    eq_concat (siz_dst_mid_src, cnt_dst_mid_src) mem_dst_mid_src
   in
   let seg =
     Sh.seg
-      {loc= dst; bas; len= siz; siz= siz_dst_mid_src; seq= seq_dst_mid_src}
+      {loc= dst; bas; len= siz; siz= siz_dst_mid_src; cnt= cnt_dst_mid_src}
   in
   let foot =
     Sh.and_ eq_mem_dst_mid_src
@@ -233,9 +235,9 @@ let memmov_dn_spec dst src len =
   let* bas, siz, _, mem_mid, mem_src, foot = memmov_foot dst src len in
   let mem_mid_src_src = [|mem_mid; mem_src; mem_src|] in
   let* siz_mid_src_src = Fresh.var "m" in
-  let+ seq_mid_src_src = Fresh.var "a" in
+  let+ cnt_mid_src_src = Fresh.var "a" in
   let eq_mem_mid_src_src =
-    eq_concat (siz_mid_src_src, seq_mid_src_src) mem_mid_src_src
+    eq_concat (siz_mid_src_src, cnt_mid_src_src) mem_mid_src_src
   in
   let post =
     Sh.and_ eq_mem_mid_src_src
@@ -244,7 +246,7 @@ let memmov_dn_spec dst src len =
          ; bas
          ; len= siz
          ; siz= siz_mid_src_src
-         ; seq= seq_mid_src_src })
+         ; cnt= cnt_mid_src_src })
   in
   {foot; sub= Var.Subst.empty; ms= Var.Set.empty; post}
 
@@ -256,9 +258,9 @@ let memmov_up_spec dst src len =
   let* bas, siz, mem_src, mem_mid, _, foot = memmov_foot src dst len in
   let mem_src_src_mid = [|mem_src; mem_src; mem_mid|] in
   let* siz_src_src_mid = Fresh.var "m" in
-  let+ seq_src_src_mid = Fresh.var "a" in
+  let+ cnt_src_src_mid = Fresh.var "a" in
   let eq_mem_src_src_mid =
-    eq_concat (siz_src_src_mid, seq_src_src_mid) mem_src_src_mid
+    eq_concat (siz_src_src_mid, cnt_src_src_mid) mem_src_src_mid
   in
   let post =
     Sh.and_ eq_mem_src_src_mid
@@ -267,7 +269,7 @@ let memmov_up_spec dst src len =
          ; bas
          ; len= siz
          ; siz= siz_src_src_mid
-         ; seq= seq_src_src_mid })
+         ; cnt= cnt_src_src_mid })
   in
   {foot; sub= Var.Subst.empty; ms= Var.Set.empty; post}
 
@@ -353,8 +355,8 @@ let calloc_spec reg num len =
   let* sub, ms = Fresh.assign ~ws:(Var.Set.of_ reg) ~rs:(Term.fv siz) in
   let loc = Term.var reg in
   let siz = Term.rename sub siz in
-  let seq = Term.splat Term.zero in
-  let+ seg = Fresh.seg loc ~bas:loc ~len:siz ~siz ~seq in
+  let cnt = Term.splat Term.zero in
+  let+ seg = Fresh.seg loc ~bas:loc ~len:siz ~siz ~cnt in
   let post = Sh.or_ (null_eq (Term.var reg)) (Sh.seg seg) in
   {foot; sub; ms; post}
 
@@ -374,7 +376,7 @@ let posix_memalign_spec reg ptr siz =
       ~rs:(Var.Set.union foot.us (Term.fv siz))
   in
   let* q = Fresh.var "q" in
-  let pseg' = {pseg with seq= q} in
+  let pseg' = {pseg with cnt= q} in
   let+ qseg = Fresh.seg q ~bas:q ~len:siz ~siz in
   let eok = Term.zero in
   let enomem = Term.integer (Z.of_int 12) in
@@ -404,8 +406,8 @@ let realloc_spec reg ptr siz =
   let loc = Term.var reg in
   let siz = Term.rename sub siz in
   let* rseg = Fresh.seg loc ~bas:loc ~len:siz ~siz in
-  let a0 = pseg.seq in
-  let a1 = rseg.seq in
+  let a0 = pseg.cnt in
+  let a1 = rseg.cnt in
   let+ a2 = Fresh.var "a" in
   let post =
     Sh.or_
@@ -433,8 +435,8 @@ let rallocx_spec reg ptr siz =
   let loc = Term.var reg in
   let siz = Term.rename sub siz in
   let* rseg = Fresh.seg loc ~bas:loc ~len:siz ~siz in
-  let a0 = pseg.seq in
-  let a1 = rseg.seq in
+  let a0 = pseg.cnt in
+  let a1 = rseg.cnt in
   let+ a2 = Fresh.var "a" in
   let post =
     Sh.or_
@@ -465,8 +467,8 @@ let xallocx_spec reg ptr siz ext =
   let siz = Term.rename sub siz in
   let ext = Term.rename sub ext in
   let* seg' = Fresh.seg ptr ~bas:ptr ~len:reg ~siz:reg in
-  let a0 = seg.seq in
-  let a1 = seg'.seq in
+  let a0 = seg.cnt in
+  let a1 = seg'.cnt in
   let+ a2 = Fresh.var "a" in
   let post =
     Sh.and_
@@ -524,13 +526,13 @@ let size_of_int_mul = Term.mulq (Q.of_int Llair.Typ.(size_of siz))
  *)
 let mallctl_read_spec r i w n =
   let* iseg = Fresh.seg i in
-  let* rseg = Fresh.seg r ~siz:iseg.seq in
+  let* rseg = Fresh.seg r ~siz:iseg.cnt in
   let+ a = Fresh.var "a" in
   let foot =
     Sh.and_ (Formula.eq0 w)
       (Sh.and_ (Formula.eq0 n) (Sh.star (Sh.seg iseg) (Sh.seg rseg)))
   in
-  let rseg' = {rseg with seq= a} in
+  let rseg' = {rseg with cnt= a} in
   let post = Sh.star (Sh.seg rseg') (Sh.seg iseg) in
   {foot; sub= Var.Subst.empty; ms= Var.Set.empty; post}
 
@@ -543,7 +545,7 @@ let mallctlbymib_read_spec p l r i w n =
   let wl = size_of_int_mul l in
   let* pseg = Fresh.seg p ~siz:wl in
   let* iseg = Fresh.seg i in
-  let m = iseg.seq in
+  let m = iseg.cnt in
   let* rseg = Fresh.seg r ~siz:m in
   let const = Sh.star (Sh.seg pseg) (Sh.seg iseg) in
   let+ a = Fresh.var "a" in
@@ -551,7 +553,7 @@ let mallctlbymib_read_spec p l r i w n =
     Sh.and_ (Formula.eq0 w)
       (Sh.and_ (Formula.eq0 n) (Sh.star const (Sh.seg rseg)))
   in
-  let rseg' = {rseg with seq= a} in
+  let rseg' = {rseg with cnt= a} in
   let post = Sh.star (Sh.seg rseg') const in
   {foot; sub= Var.Subst.empty; ms= Var.Set.empty; post}
 
@@ -596,12 +598,12 @@ let mallctlbymib_specs p j r i w n =
  *)
 let mallctlnametomib_spec p o =
   let* oseg = Fresh.seg o in
-  let n = oseg.seq in
+  let n = oseg.cnt in
   let wn = size_of_int_mul n in
   let* pseg = Fresh.seg p ~siz:wn in
   let+ a = Fresh.var "a" in
   let foot = Sh.star (Sh.seg oseg) (Sh.seg pseg) in
-  let pseg' = {pseg with seq= a} in
+  let pseg' = {pseg with cnt= a} in
   let post = Sh.star (Sh.seg pseg') (Sh.seg oseg) in
   {foot; sub= Var.Subst.empty; ms= Var.Set.empty; post}
 
diff --git a/sledge/src/sh.ml b/sledge/src/sh.ml
index 2539e2c56..2c27dca18 100644
--- a/sledge/src/sh.ml
+++ b/sledge/src/sh.ml
@@ -11,7 +11,7 @@ open Fol
 
 [@@@warning "+9"]
 
-type seg = {loc: Term.t; bas: Term.t; len: Term.t; siz: Term.t; seq: Term.t}
+type seg = {loc: Term.t; bas: Term.t; len: Term.t; siz: Term.t; cnt: Term.t}
 [@@deriving compare, equal, sexp]
 
 type starjunction =
@@ -46,18 +46,18 @@ let map_seg ~f h =
   let bas = f h.bas in
   let len = f h.len in
   let siz = f h.siz in
-  let seq = f h.seq in
+  let cnt = f h.cnt in
   if
     loc == h.loc
     && bas == h.bas
     && len == h.len
     && siz == h.siz
-    && seq == h.seq
+    && cnt == h.cnt
   then h
-  else {loc; bas; len; siz; seq}
+  else {loc; bas; len; siz; cnt}
 
-let fold_terms_seg {loc; bas; len; siz; seq} s ~f =
-  f loc (f bas (f len (f siz (f seq s))))
+let fold_terms_seg {loc; bas; len; siz; cnt} s ~f =
+  f loc (f bas (f len (f siz (f cnt s))))
 
 let fold_vars_seg seg s ~f =
   fold_terms_seg ~f:(Iter.fold ~f << Term.vars) seg s
@@ -109,15 +109,15 @@ let var_strength ?(xs = Var.Set.empty) q =
   in
   var_strength_ xs m q
 
-let pp_chunk x fs (siz, seq) = Term.ppx x fs (Term.sized ~siz ~seq)
+let pp_chunk x fs (siz, cnt) = Term.ppx x fs (Term.sized ~siz ~seq:cnt)
 
-let pp_seg x fs {loc; bas; len; siz; seq} =
+let pp_seg x fs {loc; bas; len; siz; cnt} =
   let term_pp = Term.ppx x in
   Format.fprintf fs "@[<2>%a@ @[@[-[%a)->@]@ %a@]@]" term_pp loc
     (fun fs (bas, len) ->
       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) (pp_chunk x) (siz, seq)
+    (bas, len) (pp_chunk x) (siz, cnt)
 
 let pp_seg_norm ctx fs seg =
   let x _ = None in
@@ -144,7 +144,7 @@ let pp_block x fs segs =
   in
   let term_pp = Term.ppx x in
   let pp_chunks =
-    List.pp "@,^" (fun fs seg -> pp_chunk x fs (seg.siz, seg.seq))
+    List.pp "@,^" (fun fs seg -> pp_chunk x fs (seg.siz, seg.cnt))
   in
   match segs with
   | {loc; bas; len; _} :: _ ->
diff --git a/sledge/src/sh.mli b/sledge/src/sh.mli
index 6677deb91..212b6c393 100644
--- a/sledge/src/sh.mli
+++ b/sledge/src/sh.mli
@@ -9,10 +9,13 @@
 
 open Fol
 
-(** Segment of memory starting at [loc] containing [seq] (a byte-array) of
-    size [siz], contained in an enclosing allocation-block starting at [bas]
-    of length [len]. *)
-type seg = {loc: Term.t; bas: Term.t; len: Term.t; siz: Term.t; seq: Term.t}
+(** Segment of memory. *)
+type seg =
+  { loc: Term.t  (** location (address) where segment starts *)
+  ; bas: Term.t  (** base address of enclosing allocation-block *)
+  ; len: Term.t  (** length of enclosing allocation-block *)
+  ; siz: Term.t  (** size of segment / length of the contents *)
+  ; cnt: Term.t  (** contents of segment, a sequence / byte array *) }
 
 type starjunction = private
   { us: Var.Set.t  (** vocabulary / variable context of formula *)
diff --git a/sledge/src/solver.ml b/sledge/src/solver.ml
index 364008c87..309a5e41c 100644
--- a/sledge/src/solver.ml
+++ b/sledge/src/solver.ml
@@ -194,8 +194,8 @@ let excise_seg_same ({com; min; sub} as goal) msg ssg =
   excise (fun {pf} ->
       pf "@[<hv 2>excise_seg_same@ %a@ \\- %a@]" (Sh.pp_seg_norm sub.ctx)
         msg (Sh.pp_seg_norm sub.ctx) ssg ) ;
-  let {Sh.bas= b; len= m; seq= a} = msg in
-  let {Sh.bas= b'; len= m'; seq= a'} = ssg in
+  let {Sh.bas= b; len= m; cnt= a} = msg in
+  let {Sh.bas= b'; len= m'; cnt= a'} = ssg in
   let com = Sh.star (Sh.seg msg) com in
   let min = Sh.rem_seg msg min in
   let sub =
@@ -223,18 +223,18 @@ let excise_seg_sub_prefix ({us; com; min; xs; sub; zs} as goal) msg ssg o_n
   excise (fun {pf} ->
       pf "@[<hv 2>excise_seg_sub_prefix@ %a@ \\- %a@]"
         (Sh.pp_seg_norm sub.ctx) msg (Sh.pp_seg_norm sub.ctx) ssg ) ;
-  let {Sh.loc= k; bas= b; len= m; siz= o; seq= a} = msg in
-  let {Sh.bas= b'; len= m'; siz= n; seq= a'} = ssg in
+  let {Sh.loc= k; bas= b; len= m; siz= o; cnt= a} = msg in
+  let {Sh.bas= b'; len= m'; siz= n; cnt= a'} = ssg in
   let o_n = Term.integer o_n in
   let a0, us, zs, wrt = fresh_var "a0" us zs ~wrt:(Var.Set.union us xs) in
   let a1, us, zs, _ = fresh_var "a1" us zs ~wrt in
   let xs = Var.Set.diff xs (Term.fv n) in
-  let com = Sh.star (Sh.seg {msg with siz= n; seq= a0}) com in
+  let com = Sh.star (Sh.seg {msg with siz= n; cnt= a0}) com in
   let min =
     Sh.and_
       (eq_concat (o, a) [|(n, a0); (o_n, a1)|])
       (Sh.star
-         (Sh.seg {loc= Term.add k n; bas= b; len= m; siz= o_n; seq= a1})
+         (Sh.seg {loc= Term.add k n; bas= b; len= m; siz= o_n; cnt= a1})
          (Sh.rem_seg msg min))
   in
   let sub =
@@ -263,8 +263,8 @@ let excise_seg_min_prefix ({us; com; min; xs; sub; zs} as goal) msg ssg n_o
   excise (fun {pf} ->
       pf "@[<hv 2>excise_seg_min_prefix@ %a@ \\- %a@]"
         (Sh.pp_seg_norm sub.ctx) msg (Sh.pp_seg_norm sub.ctx) ssg ) ;
-  let {Sh.bas= b; len= m; siz= o; seq= a} = msg in
-  let {Sh.loc= l; bas= b'; len= m'; siz= n; seq= a'} = ssg in
+  let {Sh.bas= b; len= m; siz= o; cnt= a} = msg in
+  let {Sh.loc= l; bas= b'; len= m'; siz= n; cnt= a'} = ssg 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
@@ -276,7 +276,7 @@ let excise_seg_min_prefix ({us; com; min; xs; sub; zs} as goal) msg ssg n_o
             (eq_concat (n, a') [|(o, a); (n_o, a1')|])
             (Sh.star
                (Sh.seg
-                  {loc= Term.add l o; bas= b'; len= m'; siz= n_o; seq= a1'})
+                  {loc= Term.add l o; bas= b'; len= m'; siz= n_o; cnt= a1'})
                (Sh.rem_seg ssg sub))))
   in
   goal |> with_ ~com ~min ~xs ~sub ~zs
@@ -299,20 +299,20 @@ let excise_seg_sub_suffix ({us; com; min; xs; sub; zs} as goal) msg ssg l_k
   excise (fun {pf} ->
       pf "@[<hv 2>excise_seg_sub_suffix@ %a@ \\- %a@]"
         (Sh.pp_seg_norm sub.ctx) msg (Sh.pp_seg_norm sub.ctx) ssg ) ;
-  let {Sh.loc= k; bas= b; len= m; siz= o; seq= a} = msg in
-  let {Sh.loc= l; bas= b'; len= m'; siz= n; seq= a'} = ssg in
+  let {Sh.loc= k; bas= b; len= m; siz= o; cnt= a} = msg in
+  let {Sh.loc= l; bas= b'; len= m'; siz= n; cnt= a'} = ssg in
   let l_k = Term.integer l_k in
   let a0, us, zs, wrt = fresh_var "a0" us zs ~wrt:(Var.Set.union us xs) in
   let a1, us, zs, _ = fresh_var "a1" us zs ~wrt in
   let xs = Var.Set.diff xs (Term.fv n) in
   let com =
-    Sh.star (Sh.seg {loc= l; bas= b; len= m; siz= n; seq= a1}) com
+    Sh.star (Sh.seg {loc= l; bas= b; len= m; siz= n; cnt= a1}) com
   in
   let min =
     Sh.and_
       (eq_concat (o, a) [|(l_k, a0); (n, a1)|])
       (Sh.star
-         (Sh.seg {loc= k; bas= b; len= m; siz= l_k; seq= a0})
+         (Sh.seg {loc= k; bas= b; len= m; siz= l_k; cnt= a0})
          (Sh.rem_seg msg min))
   in
   let sub =
@@ -341,8 +341,8 @@ let excise_seg_sub_infix ({us; com; min; xs; sub; zs} as goal) msg ssg l_k
   excise (fun {pf} ->
       pf "@[<hv 2>excise_seg_sub_infix@ %a@ \\- %a@]"
         (Sh.pp_seg_norm sub.ctx) msg (Sh.pp_seg_norm sub.ctx) ssg ) ;
-  let {Sh.loc= k; bas= b; len= m; siz= o; seq= a} = msg in
-  let {Sh.loc= l; bas= b'; len= m'; siz= n; seq= a'} = ssg in
+  let {Sh.loc= k; bas= b; len= m; siz= o; cnt= a} = msg in
+  let {Sh.loc= l; bas= b'; len= m'; siz= n; cnt= a'} = ssg in
   let l_k = Term.integer l_k in
   let ko_ln = Term.integer ko_ln in
   let ln = Term.add l n in
@@ -351,15 +351,15 @@ let excise_seg_sub_infix ({us; com; min; xs; sub; zs} as goal) msg ssg l_k
   let a2, us, zs, _ = fresh_var "a2" us zs ~wrt in
   let xs = Var.Set.diff xs (Var.Set.union (Term.fv l) (Term.fv n)) in
   let com =
-    Sh.star (Sh.seg {loc= l; bas= b; len= m; siz= n; seq= a1}) com
+    Sh.star (Sh.seg {loc= l; bas= b; len= m; siz= n; cnt= a1}) com
   in
   let min =
     Sh.and_
       (eq_concat (o, a) [|(l_k, a0); (n, a1); (ko_ln, a2)|])
       (Sh.star
-         (Sh.seg {loc= k; bas= b; len= m; siz= l_k; seq= a0})
+         (Sh.seg {loc= k; bas= b; len= m; siz= l_k; cnt= a0})
          (Sh.star
-            (Sh.seg {loc= ln; bas= b; len= m; siz= ko_ln; seq= a2})
+            (Sh.seg {loc= ln; bas= b; len= m; siz= ko_ln; cnt= a2})
             (Sh.rem_seg msg min)))
   in
   let sub =
@@ -388,8 +388,8 @@ let excise_seg_min_skew ({us; com; min; xs; sub; zs} as goal) msg ssg l_k
   excise (fun {pf} ->
       pf "@[<hv 2>excise_seg_min_skew@ %a@ \\- %a@]"
         (Sh.pp_seg_norm sub.ctx) msg (Sh.pp_seg_norm sub.ctx) ssg ) ;
-  let {Sh.loc= k; bas= b; len= m; siz= o; seq= a} = msg in
-  let {Sh.loc= l; bas= b'; len= m'; siz= n; seq= a'} = ssg in
+  let {Sh.loc= k; bas= b; len= m; siz= o; cnt= a} = msg in
+  let {Sh.loc= l; bas= b'; len= m'; siz= n; cnt= a'} = ssg 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
@@ -399,13 +399,13 @@ let excise_seg_min_skew ({us; com; min; xs; sub; zs} as goal) msg ssg l_k
   let a2', xs, zs, _ = fresh_var "a2" xs zs ~wrt in
   let xs = Var.Set.diff xs (Term.fv l) in
   let com =
-    Sh.star (Sh.seg {loc= l; bas= b; len= m; siz= ko_l; seq= a1}) com
+    Sh.star (Sh.seg {loc= l; bas= b; len= m; siz= ko_l; cnt= a1}) com
   in
   let min =
     Sh.and_
       (eq_concat (o, a) [|(l_k, a0); (ko_l, a1)|])
       (Sh.star
-         (Sh.seg {loc= k; bas= b; len= m; siz= l_k; seq= a0})
+         (Sh.seg {loc= k; bas= b; len= m; siz= l_k; cnt= a0})
          (Sh.rem_seg msg min))
   in
   let sub =
@@ -414,7 +414,7 @@ let excise_seg_min_skew ({us; com; min; xs; sub; zs} as goal) msg ssg l_k
          (Sh.and_
             (eq_concat (n, a') [|(ko_l, a1); (ln_ko, a2')|])
             (Sh.star
-               (Sh.seg {loc= ko; bas= b'; len= m'; siz= ln_ko; seq= a2'})
+               (Sh.seg {loc= ko; bas= b'; len= m'; siz= ln_ko; cnt= a2'})
                (Sh.rem_seg ssg sub))))
   in
   goal |> with_ ~us ~com ~min ~xs ~sub ~zs
@@ -438,8 +438,8 @@ let excise_seg_min_suffix ({us; com; min; xs; sub; zs} as goal) msg ssg k_l
   excise (fun {pf} ->
       pf "@[<hv 2>excise_seg_min_suffix@ %a@ \\- %a@]"
         (Sh.pp_seg_norm sub.ctx) msg (Sh.pp_seg_norm sub.ctx) ssg ) ;
-  let {Sh.bas= b; len= m; siz= o; seq= a} = msg in
-  let {Sh.loc= l; bas= b'; len= m'; siz= n; seq= a'} = ssg in
+  let {Sh.bas= b; len= m; siz= o; cnt= a} = msg in
+  let {Sh.loc= l; bas= b'; len= m'; siz= n; cnt= a'} = ssg in
   let k_l = Term.integer k_l in
   let a0', xs, zs, _ = fresh_var "a0" xs zs ~wrt:(Var.Set.union us xs) in
   let com = Sh.star (Sh.seg msg) com in
@@ -450,7 +450,7 @@ let excise_seg_min_suffix ({us; com; min; xs; sub; zs} as goal) msg ssg k_l
          (Sh.and_
             (eq_concat (n, a') [|(k_l, a0'); (o, a)|])
             (Sh.star
-               (Sh.seg {loc= l; bas= b'; len= m'; siz= k_l; seq= a0'})
+               (Sh.seg {loc= l; bas= b'; len= m'; siz= k_l; cnt= a0'})
                (Sh.rem_seg ssg sub))))
   in
   goal |> with_ ~com ~min ~xs ~sub ~zs
@@ -475,8 +475,8 @@ let excise_seg_min_infix ({us; com; min; xs; sub; zs} as goal) msg ssg k_l
   excise (fun {pf} ->
       pf "@[<hv 2>excise_seg_min_infix@ %a@ \\- %a@]"
         (Sh.pp_seg_norm sub.ctx) msg (Sh.pp_seg_norm sub.ctx) ssg ) ;
-  let {Sh.loc= k; bas= b; len= m; siz= o; seq= a} = msg in
-  let {Sh.loc= l; bas= b'; len= m'; siz= n; seq= a'} = ssg in
+  let {Sh.loc= k; bas= b; len= m; siz= o; cnt= a} = msg in
+  let {Sh.loc= l; bas= b'; len= m'; siz= n; cnt= a'} = ssg in
   let k_l = Term.integer k_l in
   let ln_ko = Term.integer ln_ko in
   let ko = Term.add k o in
@@ -490,9 +490,9 @@ let excise_seg_min_infix ({us; com; min; xs; sub; zs} as goal) msg ssg k_l
          (Sh.and_
             (eq_concat (n, a') [|(k_l, a0'); (o, a); (ln_ko, a2')|])
             (Sh.star
-               (Sh.seg {loc= l; bas= b'; len= m'; siz= k_l; seq= a0'})
+               (Sh.seg {loc= l; bas= b'; len= m'; siz= k_l; cnt= a0'})
                (Sh.star
-                  (Sh.seg {loc= ko; bas= b'; len= m'; siz= ln_ko; seq= a2'})
+                  (Sh.seg {loc= ko; bas= b'; len= m'; siz= ln_ko; cnt= a2'})
                   (Sh.rem_seg ssg sub)))))
   in
   goal |> with_ ~com ~min ~xs ~sub ~zs
@@ -516,8 +516,8 @@ let excise_seg_sub_skew ({us; com; min; xs; sub; zs} as goal) msg ssg k_l
   excise (fun {pf} ->
       pf "@[<hv 2>excise_seg_sub_skew@ %a@ \\- %a@]"
         (Sh.pp_seg_norm sub.ctx) msg (Sh.pp_seg_norm sub.ctx) ssg ) ;
-  let {Sh.loc= k; bas= b; len= m; siz= o; seq= a} = msg in
-  let {Sh.loc= l; bas= b'; len= m'; siz= n; seq= a'} = ssg in
+  let {Sh.loc= k; bas= b; len= m; siz= o; cnt= a} = msg in
+  let {Sh.loc= l; bas= b'; len= m'; siz= n; cnt= a'} = ssg 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
@@ -526,13 +526,13 @@ let excise_seg_sub_skew ({us; com; min; xs; sub; zs} as goal) msg ssg k_l
   let a1, us, zs, wrt = fresh_var "a1" us zs ~wrt in
   let a2, us, zs, _ = fresh_var "a2" us zs ~wrt in
   let com =
-    Sh.star (Sh.seg {loc= k; bas= b; len= m; siz= ln_k; seq= a1}) com
+    Sh.star (Sh.seg {loc= k; bas= b; len= m; siz= ln_k; cnt= a1}) com
   in
   let min =
     Sh.and_
       (eq_concat (o, a) [|(ln_k, a1); (ko_ln, a2)|])
       (Sh.star
-         (Sh.seg {loc= ln; bas= b; len= m; siz= ko_ln; seq= a2})
+         (Sh.seg {loc= ln; bas= b; len= m; siz= ko_ln; cnt= a2})
          (Sh.rem_seg msg min))
   in
   let sub =
@@ -541,7 +541,7 @@ let excise_seg_sub_skew ({us; com; min; xs; sub; zs} as goal) msg ssg k_l
          (Sh.and_
             (eq_concat (n, a') [|(k_l, a0'); (ln_k, a1)|])
             (Sh.star
-               (Sh.seg {loc= l; bas= b'; len= m'; siz= k_l; seq= a0'})
+               (Sh.seg {loc= l; bas= b'; len= m'; siz= k_l; cnt= a0'})
                (Sh.rem_seg ssg sub))))
   in
   goal |> with_ ~us ~com ~min ~xs ~sub ~zs
diff --git a/sledge/src/test/sh_test.ml b/sledge/src/test/sh_test.ml
index dfa4f9731..b2a5a6215 100644
--- a/sledge/src/test/sh_test.ml
+++ b/sledge/src/test/sh_test.ml
@@ -58,8 +58,8 @@ let%test_module _ =
     let%expect_test _ =
       pp
         (star
-           (seg {loc= x; bas= x; len= !16; siz= !8; seq= a})
-           (seg {loc= x + !8; bas= x; len= !16; siz= !8; seq= b})) ;
+           (seg {loc= x; bas= x; len= !16; siz= !8; cnt= a})
+           (seg {loc= x + !8; bas= x; len= !16; siz= !8; cnt= b})) ;
       [%expect {|
           %x_6 -[)-> ⟨8,%a_1⟩^⟨8,%b_2⟩ |}]
 
diff --git a/sledge/src/test/solver_test.ml b/sledge/src/test/solver_test.ml
index e71762c1a..0d7098c46 100644
--- a/sledge/src/test/solver_test.ml
+++ b/sledge/src/test/solver_test.ml
@@ -78,7 +78,7 @@ let%test_module _ =
 
     let%expect_test _ =
       check_frame
-        (Sh.seg {loc= l; bas= b; len= m; siz= n; seq= a})
+        (Sh.seg {loc= l; bas= b; len= m; siz= n; cnt= a})
         [] Sh.emp ;
       [%expect
         {|
@@ -87,9 +87,9 @@ let%test_module _ =
 
     let%expect_test _ =
       check_frame
-        (Sh.seg {loc= l; bas= b; len= m; siz= n; seq= a})
+        (Sh.seg {loc= l; bas= b; len= m; siz= n; cnt= a})
         []
-        (Sh.seg {loc= l; bas= b; len= m; siz= n; seq= a}) ;
+        (Sh.seg {loc= l; bas= b; len= m; siz= n; cnt= a}) ;
       [%expect
         {|
         ( infer_frame:
@@ -98,8 +98,8 @@ let%test_module _ =
         ) infer_frame:   emp |}]
 
     let%expect_test _ =
-      let common = Sh.seg {loc= l2; bas= b; len= !10; siz= !10; seq= a2} in
-      let seg1 = Sh.seg {loc= l; bas= b; len= !10; siz= !10; seq= a} in
+      let common = Sh.seg {loc= l2; bas= b; len= !10; siz= !10; cnt= a2} in
+      let seg1 = Sh.seg {loc= l; bas= b; len= !10; siz= !10; cnt= a} in
       let minued = Sh.star common seg1 in
       let subtrahend =
         Sh.and_ (Formula.eq m n)
@@ -120,10 +120,10 @@ let%test_module _ =
     let%expect_test _ =
       check_frame
         (Sh.star
-           (Sh.seg {loc= l; bas= b; len= m; siz= n; seq= a})
-           (Sh.seg {loc= l2; bas= b; len= m; siz= n; seq= a2}))
+           (Sh.seg {loc= l; bas= b; len= m; siz= n; cnt= a})
+           (Sh.seg {loc= l2; bas= b; len= m; siz= n; cnt= a2}))
         []
-        (Sh.seg {loc= l; bas= b; len= m; siz= n; seq= a}) ;
+        (Sh.seg {loc= l; bas= b; len= m; siz= n; cnt= a}) ;
       [%expect
         {|
         ( infer_frame:
@@ -135,10 +135,10 @@ let%test_module _ =
     let%expect_test _ =
       check_frame
         (Sh.star
-           (Sh.seg {loc= l; bas= l; len= !16; siz= !8; seq= a})
-           (Sh.seg {loc= l + !8; bas= l; len= !16; siz= !8; seq= a2}))
+           (Sh.seg {loc= l; bas= l; len= !16; siz= !8; cnt= a})
+           (Sh.seg {loc= l + !8; bas= l; len= !16; siz= !8; cnt= a2}))
         [a3_]
-        (Sh.seg {loc= l; bas= l; len= !16; siz= !16; seq= a3}) ;
+        (Sh.seg {loc= l; bas= l; len= !16; siz= !16; cnt= a3}) ;
       [%expect
         {|
         ( infer_frame:
@@ -148,10 +148,10 @@ let%test_module _ =
     let%expect_test _ =
       check_frame
         (Sh.star
-           (Sh.seg {loc= l; bas= l; len= !16; siz= !8; seq= a})
-           (Sh.seg {loc= l + !8; bas= l; len= !16; siz= !8; seq= a2}))
+           (Sh.seg {loc= l; bas= l; len= !16; siz= !8; cnt= a})
+           (Sh.seg {loc= l + !8; bas= l; len= !16; siz= !8; cnt= a2}))
         [a3_; m_]
-        (Sh.seg {loc= l; bas= l; len= m; siz= !16; seq= a3}) ;
+        (Sh.seg {loc= l; bas= l; len= m; siz= !16; cnt= a3}) ;
       [%expect
         {|
         ( infer_frame:
@@ -164,10 +164,10 @@ let%test_module _ =
     let%expect_test _ =
       check_frame
         (Sh.star
-           (Sh.seg {loc= l; bas= l; len= !16; siz= !8; seq= a})
-           (Sh.seg {loc= l + !8; bas= l; len= !16; siz= !8; seq= a2}))
+           (Sh.seg {loc= l; bas= l; len= !16; siz= !8; cnt= a})
+           (Sh.seg {loc= l + !8; bas= l; len= !16; siz= !8; cnt= a2}))
         [a3_; m_]
-        (Sh.seg {loc= l; bas= l; len= m; siz= m; seq= a3}) ;
+        (Sh.seg {loc= l; bas= l; len= m; siz= m; cnt= a3}) ;
       [%expect
         {|
         ( infer_frame:
@@ -180,12 +180,12 @@ let%test_module _ =
     let%expect_test _ =
       check_frame
         (Sh.star
-           (Sh.seg {loc= k; bas= k; len= !16; siz= !32; seq= a})
-           (Sh.seg {loc= l; bas= l; len= !8; siz= !8; seq= !16}))
+           (Sh.seg {loc= k; bas= k; len= !16; siz= !32; cnt= a})
+           (Sh.seg {loc= l; bas= l; len= !8; siz= !8; cnt= !16}))
         [a2_; m_; n_]
         (Sh.star
-           (Sh.seg {loc= l; bas= l; len= !8; siz= !8; seq= n})
-           (Sh.seg {loc= k; bas= k; len= m; siz= n; seq= a2})) ;
+           (Sh.seg {loc= l; bas= l; len= !8; siz= !8; cnt= n})
+           (Sh.seg {loc= k; bas= k; len= m; siz= n; cnt= a2})) ;
       [%expect
         {|
         ( infer_frame:
@@ -202,12 +202,12 @@ let%test_module _ =
     let%expect_test _ =
       infer_frame
         (Sh.star
-           (Sh.seg {loc= k; bas= k; len= !16; siz= !32; seq= a})
-           (Sh.seg {loc= l; bas= l; len= !8; siz= !8; seq= !16}))
+           (Sh.seg {loc= k; bas= k; len= !16; siz= !32; cnt= a})
+           (Sh.seg {loc= l; bas= l; len= !8; siz= !8; cnt= !16}))
         [a2_; m_; n_]
         (Sh.star
-           (Sh.seg {loc= k; bas= k; len= m; siz= n; seq= a2})
-           (Sh.seg {loc= l; bas= l; len= !8; siz= !8; seq= n})) ;
+           (Sh.seg {loc= k; bas= k; len= m; siz= n; cnt= a2})
+           (Sh.seg {loc= l; bas= l; len= !8; siz= !8; cnt= n})) ;
       [%expect
         {|
         ( infer_frame:
@@ -223,9 +223,9 @@ let%test_module _ =
 
     let seg_split_symbolically =
       Sh.star
-        (Sh.seg {loc= l; bas= l; len= !16; siz= 8 * n; seq= a2})
+        (Sh.seg {loc= l; bas= l; len= !16; siz= 8 * n; cnt= a2})
         (Sh.seg
-           {loc= l + (8 * n); bas= l; len= !16; siz= !16 - (8 * n); seq= a3})
+           {loc= l + (8 * n); bas= l; len= !16; siz= !16 - (8 * n); cnt= a3})
 
     let%expect_test _ =
       check_frame
@@ -233,7 +233,7 @@ let%test_module _ =
            Formula.(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; seq= a}) ;
+        (Sh.seg {loc= l; bas= l; len= m; siz= m; cnt= a}) ;
       [%expect
         {|
         ( infer_frame:
@@ -266,7 +266,7 @@ let%test_module _ =
       infer_frame
         (Sh.and_ (Formula.le n !2) seg_split_symbolically)
         [m_; a_]
-        (Sh.seg {loc= l; bas= l; len= m; siz= m; seq= a}) ;
+        (Sh.seg {loc= l; bas= l; len= m; siz= m; cnt= a}) ;
       [%expect
         {|
         ( infer_frame: