diff --git a/sledge/lib/term.ml b/sledge/lib/term.ml
index 0f31eee2e..37d73fb4f 100644
--- a/sledge/lib/term.ml
+++ b/sledge/lib/term.ml
@@ -1075,6 +1075,16 @@ let map e ~f =
       e
   | Var _ | Label _ | Nondet _ | Float _ | Integer _ -> e
 
+let fold_map e ~init ~f =
+  let s = ref init in
+  let f x =
+    let s', x' = f !s x in
+    s := s' ;
+    x'
+  in
+  let e' = map e ~f in
+  (!s, e')
+
 (** Pre-order transformation that preserves cycles. Each subterm [x] from
     root to leaves is presented to [f]. If [f x = Some x'] then the subterms
     of [x] are not traversed and [x] is transformed to [x']. Otherwise
diff --git a/sledge/lib/term.mli b/sledge/lib/term.mli
index 5adb1c9c9..d3bf77563 100644
--- a/sledge/lib/term.mli
+++ b/sledge/lib/term.mli
@@ -234,6 +234,7 @@ val size_of : Typ.t -> t
 (** Transform *)
 
 val map : t -> f:(t -> t) -> t
+val fold_map : t -> init:'a -> f:('a -> t -> 'a * t) -> 'a * t
 val rename : Var.Subst.t -> t -> t
 
 (** Traverse *)