diff --git a/src/core/Sidekick_core.ml b/src/core/Sidekick_core.ml index 4ceea0b0..eda7ceaa 100644 --- a/src/core/Sidekick_core.ml +++ b/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} diff --git a/src/msat-solver/Sidekick_msat_solver.ml b/src/msat-solver/Sidekick_msat_solver.ml index b72aadee..2d2492d0 100644 --- a/src/msat-solver/Sidekick_msat_solver.ml +++ b/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 diff --git a/src/smtlib/Process.ml b/src/smtlib/Process.ml index d3846cef..b38e3a6a 100644 --- a/src/smtlib/Process.ml +++ b/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