diff --git a/sledge/lib/equality.ml b/sledge/lib/equality.ml
index ec88f3214..cebade643 100644
--- a/sledge/lib/equality.ml
+++ b/sledge/lib/equality.ml
@@ -189,18 +189,10 @@ let prefer e f =
     | ApN (Concat, _) -> 3
     | _ -> 4
   in
-  let rec height e =
-    match (e : Term.t) with
-    | Ap2 (Memory, _, x) -> 1 + height x
-    | Ap3 (Extract, x, _, _) -> 1 + height x
-    | ApN (Concat, xs) ->
-        1 + IArray.fold ~init:0 ~f:(fun h x -> max h (height x)) xs
-    | _ -> 0
-  in
   let o = compare (rank e) (rank f) in
   if o <> 0 then o
   else
-    let o = compare (height e) (height f) in
+    let o = compare (Term.height e) (Term.height f) in
     if o <> 0 then o else Term.compare e f
 
 (** orient equations based on representative preference *)
diff --git a/sledge/lib/term.ml b/sledge/lib/term.ml
index 6b3988344..eef8ff13c 100644
--- a/sledge/lib/term.ml
+++ b/sledge/lib/term.ml
@@ -1178,6 +1178,20 @@ let fv e = fold_vars e ~f:Set.add ~init:Var.Set.empty
 let is_true = function Integer {data} -> Z.is_true data | _ -> false
 let is_false = function Integer {data} -> Z.is_false data | _ -> false
 
+let height e =
+  let height_ height_ = function
+    | Var _ -> 0
+    | Ap1 (_, a) -> 1 + height_ a
+    | Ap2 (_, a, b) -> 1 + max (height_ a) (height_ b)
+    | Ap3 (_, a, b, c) -> 1 + max (height_ a) (max (height_ b) (height_ c))
+    | ApN (_, v) | RecN (_, v) ->
+        1 + IArray.fold v ~init:0 ~f:(fun m a -> max m (height_ a))
+    | Add qs | Mul qs ->
+        1 + Qset.fold qs ~init:0 ~f:(fun a _ m -> max m (height_ a))
+    | Label _ | Nondet _ | Float _ | Integer _ -> 0
+  in
+  fix height_ (fun _ -> 0) e
+
 (** Solve *)
 
 let solve_zero_eq ?for_ e =
diff --git a/sledge/lib/term.mli b/sledge/lib/term.mli
index d3bf77563..8e601fe76 100644
--- a/sledge/lib/term.mli
+++ b/sledge/lib/term.mli
@@ -250,6 +250,7 @@ val fold_terms : t -> init:'a -> f:('a -> t -> 'a) -> 'a
 val fv : t -> Var.Set.t
 val is_true : t -> bool
 val is_false : t -> bool
+val height : t -> int
 
 (** Solve *)