diff --git a/src/util/Backtrackable_ref.ml b/src/util/Backtrackable_ref.ml
new file mode 100644
index 00000000..bc91cfd5
--- /dev/null
+++ b/src/util/Backtrackable_ref.ml
@@ -0,0 +1,29 @@
+
+type 'a t = {
+  mutable cur: 'a;
+  stack: 'a Vec.t;
+  copy: ('a -> 'a) option;
+}
+
+let create ?copy x: _ t =
+  {cur=x; stack=Vec.create(); copy}
+
+let[@inline] get self = self.cur
+let[@inline] set self x = self.cur <- x
+let[@inline] update self f = self.cur <- f self.cur
+
+let[@inline] n_levels self = Vec.size self.stack
+
+let[@inline] push_level self : unit =
+  let x = self.cur in
+  let x = match self.copy with None -> x | Some f -> f x in
+  Vec.push self.stack x
+
+let pop_levels self n : unit =
+  assert (n>=0);
+  if n > Vec.size self.stack then invalid_arg "Backtrackable_ref.pop_levels";
+  let i = Vec.size self.stack-n in
+  let x = Vec.get self.stack i in
+  self.cur <- x;
+  Vec.shrink self.stack i;
+  ()
diff --git a/src/util/Backtrackable_ref.mli b/src/util/Backtrackable_ref.mli
new file mode 100644
index 00000000..55acb2d3
--- /dev/null
+++ b/src/util/Backtrackable_ref.mli
@@ -0,0 +1,30 @@
+
+(** {1 Backtrackable ref} *)
+
+type 'a t
+
+val create : ?copy:('a -> 'a) -> 'a -> 'a t
+(** Create a backtrackable reference holding the given value initially.
+    @param copy if provided, will be used to copy the value when [push_level]
+    is called. *)
+
+val set : 'a t -> 'a -> unit
+(** Set the reference's current content *)
+
+val get : 'a t -> 'a
+(** Get the reference's current content *)
+
+val update : 'a t -> ('a -> 'a) -> unit
+(** Update the reference's current content *)
+
+val push_level : _ t -> unit
+(** Push a backtracking level, copying the current value on top of some
+    stack. The [copy] function will be used if it was provided in {!create}. *)
+
+val n_levels : _ t -> int
+(** Number of saved values *)
+
+val pop_levels : _ t -> int -> unit
+(** Pop [n] levels, restoring to the value the reference was storing [n] calls
+    to [push_level] earlier.
+    @raise Invalid_argument if [n] is bigger than [n_levels]. *)
diff --git a/src/util/Sidekick_util.ml b/src/util/Sidekick_util.ml
index 7a0b1577..0f31094a 100644
--- a/src/util/Sidekick_util.ml
+++ b/src/util/Sidekick_util.ml
@@ -22,6 +22,7 @@ module Int_map = Util.Int_map
 module IArray = IArray
 module Backtrack_stack = Backtrack_stack
 module Backtrackable_tbl = Backtrackable_tbl
+module Backtrackable_ref = Backtrackable_ref
 
 module Log = Log
 module Error = Error