From 4308eba04d0bcb323e9bd37e88d324558b9ede88 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Mon, 11 Oct 2021 23:19:24 -0400
Subject: [PATCH] fix

---
 src/base-solver/sidekick_base_solver.ml | 1 +
 src/smt-solver/Sidekick_smt_solver.ml   | 2 +-
 2 files changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/base-solver/sidekick_base_solver.ml b/src/base-solver/sidekick_base_solver.ml
index 090da86f..47b0e1c5 100644
--- a/src/base-solver/sidekick_base_solver.ml
+++ b/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} *)
diff --git a/src/smt-solver/Sidekick_smt_solver.ml b/src/smt-solver/Sidekick_smt_solver.ml
index a3d3a864..21c6b436 100644
--- a/src/smt-solver/Sidekick_smt_solver.ml
+++ b/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;