diff --git a/src/core/gensym.ml b/src/core/gensym.ml
index 09bc2f6e..b8d63461 100644
--- a/src/core/gensym.ml
+++ b/src/core/gensym.ml
@@ -43,6 +43,8 @@ let create tst : t =
   incr id_;
   { tst; self_id; fresh = 0 }
 
+let reset self = self.fresh <- 0
+
 let fresh_term ?(opaque_to_cc = false) (self : t) ~pre (ty : ty) : Term.t =
   let id = self.fresh in
   self.fresh <- 1 + self.fresh;
diff --git a/src/core/gensym.mli b/src/core/gensym.mli
index 00fcd5a8..69684af0 100644
--- a/src/core/gensym.mli
+++ b/src/core/gensym.mli
@@ -17,3 +17,6 @@ val create : Term.store -> t
 
 val fresh_term : ?opaque_to_cc:bool -> t -> pre:string -> ty -> term
 (** Make a fresh term of the given type *)
+
+val reset : t -> unit
+(** Reset to initial state *)