feat(check-cc): add statistics

src/core/Sidekick_core.ml

@@ -328,6 +328,7 @@ module type SOLVER_INTERNAL = sig
   type solver = t
 
   val tst : t -> term_state
+  val stats : t -> Stat.t
 
   (** {3 Literals}
 

src/msat-solver/Sidekick_msat_solver.ml

@@ -193,6 +193,7 @@ module Make(A : ARG)
 
     let[@inline] cc (t:t) = Lazy.force t.cc
     let[@inline] tst t = t.tst
+    let stats t = t.stat
 
     let simplifier self = self.simp
     let simp_t self (t:Term.t) : Term.t = Simplify.normalize self.simp t

src/smtlib/Process.ml

@@ -458,7 +458,11 @@ module Check_cc = struct
   let theory =
     Solver.mk_theory ~name:"cc-check"
       ~create_and_setup:(fun si ->
-          Solver.Solver_internal.on_cc_conflict si (check_conflict si))
+          let n_calls = Stat.mk_int (Solver.Solver_internal.stats si) "check-cc.call" in
+          Solver.Solver_internal.on_cc_conflict si
+            (fun c ->
+               Stat.incr n_calls;
+               check_conflict si c))
       ()
 
 end