diff --git a/src/core/internal.ml b/src/core/internal.ml
index f986ef9a..7bb93c8a 100644
--- a/src/core/internal.ml
+++ b/src/core/internal.ml
@@ -1229,6 +1229,15 @@ module Make
     if l > current_level () then invalid_arg "cannot pop to level, it is too high"
     else if l < current_level () then begin
 
+      (* Filter the current buffer of clauses to remove potential assumptions
+         with too high a user level,
+         or else, with later pushes, these assumptions might be added. *)
+      let cl = Stack.fold (fun acc c ->
+          if c.c_level > l then acc else c :: acc) [] env.clauses_to_add in
+      Stack.clear env.clauses_to_add;
+      List.iter (fun c -> Stack.push c env.clauses_to_add) cl;
+
+      (* Get back the user level *)
       let ul = Vec.get env.user_levels l in
       Vec.shrink env.user_levels (max 0 (Vec.size env.user_levels - l - 1));