diff --git a/plugins/qcheck-stm/test/sequence_model.ml b/plugins/qcheck-stm/test/sequence_model.ml
index 847555d7..eb0f74e5 100644
--- a/plugins/qcheck-stm/test/sequence_model.ml
+++ b/plugins/qcheck-stm/test/sequence_model.ml
@@ -2,3 +2,10 @@ type 'a t = 'a list ref
 
 let create () = ref []
 let add x s = s := x :: !s
+
+let pop q =
+  match !q with
+  | [] -> None
+  | x :: xs ->
+      q := xs;
+      Some x
diff --git a/plugins/qcheck-stm/test/sequence_model.mli b/plugins/qcheck-stm/test/sequence_model.mli
index 939ae4be..cfdd40a2 100644
--- a/plugins/qcheck-stm/test/sequence_model.mli
+++ b/plugins/qcheck-stm/test/sequence_model.mli
@@ -9,3 +9,10 @@ val add : 'a -> 'a t -> unit
 (*@ add v t
     modifies t.contents
     ensures t.contents = Sequence.cons v (old t.contents) *)
+
+val pop : 'a t -> 'a option
+(*@ o = pop q
+    modifies q.contents
+    ensures q.contents = match o with
+                          | None -> old q.contents
+                          | Some _ -> Sequence.tl (old q.contents) *)