diff --git a/src/util/Backtrack_stack.ml b/src/util/Backtrack_stack.ml
index 81b78f37..eca78296 100644
--- a/src/util/Backtrack_stack.ml
+++ b/src/util/Backtrack_stack.ml
@@ -27,7 +27,7 @@ let pop_levels (self:_ t) (n:int) ~f : unit =
     let new_lvl = n_levels self - n in
     let i = Vec.get self.lvls new_lvl in
     while Vec.size self.vec > i do
-      let x = Vec.pop self.vec in
+      let x = Vec.pop_exn self.vec in
       f x
     done;
     Vec.shrink self.lvls new_lvl
diff --git a/src/util/Vec.ml b/src/util/Vec.ml
index 89759a51..bd2778d9 100644
--- a/src/util/Vec.ml
+++ b/src/util/Vec.ml
@@ -15,12 +15,20 @@ let[@inline] shrink t i =
   assert (i<=t.sz);
   t.sz <- i
 
-let[@inline] pop t =
+let[@inline] pop_exn t =
   if t.sz = 0 then invalid_arg "vec.pop";
   let x = Array.unsafe_get t.data (t.sz - 1) in
   t.sz <- t.sz - 1;
   x
 
+let[@inline] pop t =
+  if t.sz = 0 then None
+  else (
+    let x = Array.unsafe_get t.data (t.sz - 1) in
+    t.sz <- t.sz - 1;
+    Some x
+  )
+
 let[@inline] size t = t.sz
 
 let[@inline] is_empty t = t.sz = 0
diff --git a/src/util/Vec.mli b/src/util/Vec.mli
index d00f060f..109afad5 100644
--- a/src/util/Vec.mli
+++ b/src/util/Vec.mli
@@ -32,10 +32,12 @@ val shrink : 'a t -> int -> unit
 (** [shrink vec sz] resets size of [vec] to [sz].
     Assumes [sz >=0 && sz <= size vec] *)
 
-val pop : 'a t -> 'a
+val pop_exn : 'a t -> 'a
 (** Pop last element and return it.
     @raise Invalid_argument if the vector is empty *)
 
+val pop : 'a t -> 'a option
+
 val size : 'a t -> int
 
 val is_empty : 'a t -> bool