fix

src/base-solver/sidekick_base_solver.ml

@@ -16,6 +16,7 @@ module Solver_arg = struct
   let is_valid_literal _ = true
   module P = Proof_stub
   type proof = P.t
+  type proof_step = P.proof_step
 end
 
 (** SMT solver, obtained from {!Sidekick_smt_solver} *)

src/smt-solver/Sidekick_smt_solver.ml

@@ -587,7 +587,7 @@ module Make(A : ARG)
         ty_st;
         cc = lazy (
           (* lazily tie the knot *)
-          CC.create ~size:`Big self.tst;
+          CC.create ~size:`Big self.tst self.proof;
         );
         proof;
         th_states=Ths_nil;