diff --git a/src/util/Backtrackable_tbl.ml b/src/util/Backtrackable_tbl.ml
index 908189c8..cc8f4df1 100644
--- a/src/util/Backtrackable_tbl.ml
+++ b/src/util/Backtrackable_tbl.ml
@@ -16,6 +16,7 @@ module type S = sig
   val remove : _ t -> key -> unit
   val push_level : _ t -> unit
   val pop_levels : _ t -> int -> unit
+  val n_levels : _ t -> int
 end
 
 module type ARG = sig
@@ -49,6 +50,7 @@ module Make(A : ARG) = struct
   let[@inline] iter f self = M.iter f self.tbl
   let[@inline] push_level self = BS.push_level self.undo
   let[@inline] pop_levels self n = BS.pop_levels self.undo n ~f:(apply_undo self)
+  let[@inline] n_levels self = BS.n_levels self.undo
 
   let add self k v : unit =
     if BS.n_levels self.undo > 0 then (
diff --git a/src/util/Backtrackable_tbl.mli b/src/util/Backtrackable_tbl.mli
index 5cbaf139..fe7a6996 100644
--- a/src/util/Backtrackable_tbl.mli
+++ b/src/util/Backtrackable_tbl.mli
@@ -18,6 +18,7 @@ module type S = sig
   val remove : _ t -> key -> unit
   val push_level : _ t -> unit
   val pop_levels : _ t -> int -> unit
+  val n_levels : _ t -> int
 end
 
 module type ARG = sig
diff --git a/src/zarith/sidekick_zarith.ml b/src/zarith/sidekick_zarith.ml
index 8beb008f..dd940b96 100644
--- a/src/zarith/sidekick_zarith.ml
+++ b/src/zarith/sidekick_zarith.ml
@@ -19,7 +19,7 @@ module Rational
   include Q
   let denum = den
   let pp = pp_print
-  let hash a = Hashtbl.hash (Z.hash (num a), Z.hash (den a))
+  let hash a = CCHash.combine2 (Z.hash (num a)) (Z.hash (den a))
 
   let infinity = Q.inf
   let minus_infinity = Q.minus_inf