diff --git a/sledge/src/sh.ml b/sledge/src/sh.ml
index 0d79d2706..ae3673c7e 100644
--- a/sledge/src/sh.ml
+++ b/sledge/src/sh.ml
@@ -150,12 +150,12 @@ let pp_block x fs segs =
     | {loc; bas; len; _} :: _ -> (
         Term.equal loc bas
         &&
-        match len with
-        | Integer {data} -> (
+        match Term.d_int len with
+        | Some data -> (
           match
             List.fold segs ~init:(Some Z.zero) ~f:(fun len seg ->
-                match (len, seg.siz) with
-                | Some len, Integer {data} -> Some (Z.add len data)
+                match (len, Term.d_int seg.siz) with
+                | Some len, Some data -> Some (Z.add len data)
                 | _ -> None )
           with
           | Some blk_len -> Z.equal data blk_len
@@ -286,8 +286,9 @@ let fv ?ignore_cong q =
   in
   fv_union Var.Set.empty q
 
-let invariant_pure = function
-  | Term.Integer {data} -> assert (not (Z.is_false data))
+let invariant_pure b =
+  match Term.d_int b with
+  | Some data -> assert (not (Z.is_false data))
   | _ -> assert true
 
 let invariant_seg _ = ()
diff --git a/sledge/src/term.ml b/sledge/src/term.ml
index a53536937..c944d9d50 100644
--- a/sledge/src/term.ml
+++ b/sledge/src/term.ml
@@ -1140,6 +1140,10 @@ module Var = struct
   end
 end
 
+(** Destruct *)
+
+let d_int = function Integer {data} -> Some data | _ -> None
+
 (** Transform *)
 
 let map e ~f =
diff --git a/sledge/src/term.mli b/sledge/src/term.mli
index 55c56e359..321bba929 100644
--- a/sledge/src/term.mli
+++ b/sledge/src/term.mli
@@ -237,6 +237,10 @@ val rec_record : int -> t
 (* convert *)
 val of_exp : Llair.Exp.t -> t
 
+(** Destruct *)
+
+val d_int : t -> Z.t option
+
 (** Transform *)
 
 val map : t -> f:(t -> t) -> t