diff --git a/sledge/cli/smtlib.ml b/sledge/cli/smtlib.ml
index 2add29919..e4ea4eb9c 100644
--- a/sledge/cli/smtlib.ml
+++ b/sledge/cli/smtlib.ml
@@ -67,10 +67,10 @@ and x_trm : var_env -> Smt.Ast.term -> Term.t =
     match List.map ~f:(x_trm n) es with
     | e :: es ->
         List.fold es ~init:e ~f:(fun p e ->
-            match Term.const_of e with
+            match Term.get_const e with
             | Some q -> Term.mulq q p
             | None -> (
-              match Term.const_of p with
+              match Term.get_const p with
               | Some q -> Term.mulq q e
               | None -> fail "nonlinear: %a" Smt.Ast.pp_term term () ) )
     | [] -> fail "malformed: %a" Smt.Ast.pp_term term () )
@@ -78,7 +78,7 @@ and x_trm : var_env -> Smt.Ast.term -> Term.t =
     match List.map ~f:(x_trm n) es with
     | e :: es ->
         List.fold es ~init:e ~f:(fun p e ->
-            match Term.const_of e with
+            match Term.get_const e with
             | Some q -> Term.mulq (Q.inv q) p
             | None -> fail "nonlinear: %a" Smt.Ast.pp_term term () )
     | [] -> fail "malformed: %a" Smt.Ast.pp_term term () )
diff --git a/sledge/src/arithmetic.ml b/sledge/src/arithmetic.ml
index a0e21e6e8..9347700dc 100644
--- a/sledge/src/arithmetic.ml
+++ b/sledge/src/arithmetic.ml
@@ -234,6 +234,11 @@ module Representation (Trm : INDETERMINATE) = struct
 
     (* transform *)
 
+    let split_const poly =
+      match Sum.find_and_remove poly Mono.one with
+      | Some (c, p_c) -> (p_c, c)
+      | None -> (poly, Q.zero)
+
     let map poly ~f =
       let p, p' = (poly, Sum.empty) in
       let p, p' =
diff --git a/sledge/src/arithmetic_intf.ml b/sledge/src/arithmetic_intf.ml
index 36b2a9138..dea75ee4b 100644
--- a/sledge/src/arithmetic_intf.ml
+++ b/sledge/src/arithmetic_intf.ml
@@ -48,6 +48,11 @@ module type S = sig
 
   (** Transform *)
 
+  val split_const : t -> t * Q.t
+  (** Splits an arithmetic term into the sum of its constant and
+      non-constant parts. That is, [split_const a] is [(b, c)] such that
+      [a = b + c] and the absolute value of [c] is maximal. *)
+
   val map : t -> f:(trm -> trm) -> t
   (** [map ~f a] is [a] with each indeterminate transformed by [f]. Viewing
       [a] as a polynomial,
diff --git a/sledge/src/fol.ml b/sledge/src/fol.ml
index f6a48c1e3..b39b06802 100644
--- a/sledge/src/fol.ml
+++ b/sledge/src/fol.ml
@@ -855,13 +855,21 @@ module Term = struct
 
   let d_int = function `Trm (Z z) -> Some z | _ -> None
 
-  (** Access *)
-
-  let const_of = function
+  let get_const = function
     | `Trm (Z z) -> Some (Q.of_z z)
     | `Trm (Q q) -> Some q
     | _ -> None
 
+  (** Access *)
+
+  let split_const = function
+    | `Trm (Z z) -> (zero, Q.of_z z)
+    | `Trm (Q q) -> (zero, q)
+    | `Trm (Arith a) ->
+        let a_c, c = Arith.split_const a in
+        (`Trm (_Arith a_c), c)
+    | e -> (e, Q.zero)
+
   (** Traverse *)
 
   let fold_vars = fold_vars
diff --git a/sledge/src/fol.mli b/sledge/src/fol.mli
index ceb118ab4..ae83a148c 100644
--- a/sledge/src/fol.mli
+++ b/sledge/src/fol.mli
@@ -60,9 +60,15 @@ module rec Term : sig
 
   val d_int : t -> Z.t option
 
+  val get_const : t -> Q.t option
+  (** [get_const a] is [Some q] iff [equal a (const q)] *)
+
   (** Access *)
 
-  val const_of : t -> Q.t option
+  val split_const : t -> t * Q.t
+  (** Splits a term into the sum of its constant and non-constant parts.
+      That is, [split_const a] is [(b, c)] such that [a = b + c] and the
+      absolute value of [c] is maximal. *)
 
   (** Query *)
 
diff --git a/sledge/src/sh.ml b/sledge/src/sh.ml
index bd05ca08c..8cac3dbe0 100644
--- a/sledge/src/sh.ml
+++ b/sledge/src/sh.ml
@@ -170,11 +170,7 @@ let pp_block x fs segs =
   | [] -> ()
 
 let pp_heap x ?pre ctx fs heap =
-  let bas_off e =
-    match Term.const_of e with
-    | Some const -> (Term.sub e (Term.rational const), const)
-    | None -> (e, Q.zero)
-  in
+  let bas_off = Term.split_const in
   let cmp s1 s2 =
     [%compare: Term.t * (Term.t * Q.t)]
       (Context.normalize ctx s1.bas, bas_off (Context.normalize ctx s1.loc))