diff --git a/src/util/Backtrack_stack.ml b/src/util/Backtrack_stack.ml index b4d955da..87e8b702 100644 --- a/src/util/Backtrack_stack.ml +++ b/src/util/Backtrack_stack.ml @@ -8,7 +8,7 @@ type 'a t = { let create() : _ t = {vec=Vec.create(); lvls=Vec.create()} -let[@inline] n_levels self : int = Vec.size self.vec +let[@inline] n_levels self : int = Vec.size self.lvls let[@inline] push self x : unit = Vec.push self.vec x @@ -21,9 +21,10 @@ let[@inline] push_if_nonzero_level self x : unit = let[@inline] push_level (self:_ t) : unit = Vec.push self.lvls (Vec.size self.vec) - let pop_levels (self:_ t) (n:int) ~f : unit = - if n > n_levels self then invalid_arg "Backtrack_stack.pop_levels"; + if n > n_levels self then ( + Error.errorf "Backtrack_stack.pop_levels %d (size: %d)" n (n_levels self); + ); if n > 0 then ( let new_lvl = n_levels self - n in let i = Vec.get self.lvls new_lvl in