diff --git a/src/smt-solver/Sidekick_smt_solver.ml b/src/smt-solver/Sidekick_smt_solver.ml
index 2ea87077..a53d5a58 100644
--- a/src/smt-solver/Sidekick_smt_solver.ml
+++ b/src/smt-solver/Sidekick_smt_solver.ml
@@ -508,137 +508,6 @@ module Make(A : ARG)
   (** the parametrized SAT Solver *)
   module Sat_solver = Sidekick_sat.Make_cdcl_t(Solver_internal)
 
-  (* TODO: move somewhere else? where it can be used to implement the new
-     proof module?
-  module Pre_proof = struct
-    module SP = Sat_solver.Proof
-    module SC = Sat_solver.Clause
-
-    type t = {
-      solver: Sat_solver.t;
-      msat: Sat_solver.Proof.t;
-      tdefs: (term*term) list; (* term definitions *)
-      p: P.t lazy_t;
-    }
-
-    let to_proof (self:t) : P.t = Lazy.force self.p
-
-    let pp_dot =
-      let module Dot =
-        Sidekick_backend.Dot.Make(Sat_solver)(Sidekick_backend.Dot.Default(Sat_solver)) in
-      let pp out self = Dot.pp (Sat_solver.store self.solver) out self.msat in
-      Some pp
-
-    (* export to proof {!P.t}, translating Msat-level proof ising:
-       - [stepc name cl proof] to bind [name] to given clause and proof
-       - [deft name t] to define [name] as a shortcut for [t] (tseitin, etc.).
-         Checker will always expand these. (TODO)
-       - [steps <defc>+] for a structure proof with definitions, returning last one
-       - [subproof (assms <lit>* ) (proof)] which uses [proof] to get
-         clause [c] under given assumptions (each assm is a lit),
-         and return [-a1 \/ … \/ -an \/ c], discharging assumptions
-    *)
-    let conv_proof (store:Sat_solver.store) (msat:Sat_solver.Proof.t) (t_defs:_ list) : P.t =
-      let assms = ref [] in
-      let steps = ref [] in
-
-      let n_step = ref 0 in
-      let n_tbl_: string SC.Tbl.t = SC.Tbl.create 32 in (* node.concl -> unique idx *)
-
-      (* name of an already processed proof node *)
-      let find_proof_name (p:Sat_solver.Proof.t) : string =
-        try SC.Tbl.find n_tbl_ (SP.conclusion p)
-        with Not_found ->
-          Error.errorf
-            "msat-solver.pre-proof.to_proof: cannot find proof step with conclusion %a"
-            (SC.pp store) (SP.conclusion p)
-      in
-
-      let add_step s = steps := s :: !steps in
-
-      (* convert [n_init] into a proof step and adds it to [steps] *)
-      let tr_node_to_step () (n_init:SP.proof_node) : unit =
-        let {SP.conclusion=c; step} = n_init in
-
-        if SC.Tbl.mem n_tbl_ c then ()
-        else (
-          let name = Printf.sprintf "c%d" !n_step in
-          incr n_step;
-
-          SC.Tbl.add n_tbl_ c name;
-
-          (* build conclusion of proof step *)
-          let tr_atom a : P.lit =
-            let sign = Sat_solver.Atom.sign a in
-            let t = Lit.term (Sat_solver.Atom.formula store a) in
-            P.lit_mk sign t
-          in
-          let concl = List.rev_map tr_atom @@ Sat_solver.Clause.atoms_l store c in
-
-          (* proof for the node *)
-          let pr_step : P.t =
-            match step with
-            | SP.Hypothesis pr -> pr (* FIXME: should this have a special rule? *)
-
-            | SP.Assumption ->
-              (* push into assumptions and introduce a name for it *)
-              let name = Printf.sprintf "a%d" !n_step in
-              let lit = match concl with
-                | [l] -> l
-                | _ -> Error.errorf "assumption with non-unit clause %a" (SC.pp store) c
-              in
-              incr n_step;
-              assms := (name, lit) :: !assms;
-              P.ref_by_name name
-
-            | Lemma pr -> pr
-
-            | Duplicate (c, _) ->
-              let n = find_proof_name c in
-              let p = P.ref_by_name n in
-              (* NOTE: we do not represent this form of transformation for now.
-                 Quip should be able to process clauses as sets. *)
-              p
-
-            | Hyper_res { hr_init=init; hr_steps=steps } ->
-              let proof_init = P.ref_by_name @@ find_proof_name init in
-              let tr_step (pivot,p') : P.hres_step =
-                (* unit resolution? *)
-                let is_r1_step = SC.n_atoms store (SP.conclusion p') = 1 in
-                let proof_p' = P.ref_by_name @@ find_proof_name p' in
-                if is_r1_step then (
-                  P.r1 proof_p'
-                ) else (
-                  let pivot = Lit.term (Sat_solver.Atom.formula store pivot) in
-                  P.r proof_p' ~pivot
-                )
-              in
-              P.hres_iter proof_init
-                (Iter.of_list steps |> Iter.map tr_step)
-          in
-
-          let step = P.stepc ~name concl pr_step in
-          add_step step;
-        )
-      in
-
-      (* this should traverse from the leaves, so that order of [steps] is correct *)
-      Sat_solver.Proof.fold store tr_node_to_step () msat;
-      let assms = !assms in
-
-      (* gather all term definitions *)
-      let t_defs = CCList.map (fun (c,rhs) -> P.deft c rhs) t_defs in
-      P.composite_l ~assms (CCList.append t_defs (List.rev !steps))
-
-    let make solver (msat: Sat_solver.Proof.t) (tdefs: _ list) : t =
-      { solver; msat; tdefs; p=lazy (conv_proof (Sat_solver.store solver) msat tdefs) }
-
-    let check self = SP.check (Sat_solver.store self.solver) self.msat
-    let pp_debug out self = P.pp_debug ~sharing:false out (to_proof self)
-    let output oc (self:t) = P.Quip.output oc (to_proof self)
-  end
-     *)
-
   (* main solver state *)
   type t = {
     si: Solver_internal.t;