diff --git a/sledge/src/trm.ml b/sledge/src/trm.ml
index 93ad112e4..00405165c 100644
--- a/sledge/src/trm.ml
+++ b/sledge/src/trm.ml
@@ -496,3 +496,4 @@ let subtrms e = Iter.from_labelled_iter (iter_subtrms e)
 (** Query *)
 
 let fv e = Var.Set.of_iter (vars e)
+let rec height e = 1 + Iter.fold ~f:(fun x -> max (height x)) (subtrms e) 0
diff --git a/sledge/src/trm.mli b/sledge/src/trm.mli
index 67120bfe0..a7229fc2d 100644
--- a/sledge/src/trm.mli
+++ b/sledge/src/trm.mli
@@ -96,6 +96,7 @@ val map : t -> f:(t -> t) -> t
 val seq_size_exn : t -> t
 val seq_size : t -> t option
 val fv : t -> Var.Set.t
+val height : t -> int
 
 (** Traverse *)