diff --git a/src/base/Proof_stub.ml b/src/base/Proof_stub.ml
index 8c97947b..c617b9d4 100644
--- a/src/base/Proof_stub.ml
+++ b/src/base/Proof_stub.ml
@@ -8,7 +8,7 @@ type t = unit
 type dproof = t -> unit
 
 let create () : t = ()
-let enabled _ = false
+let with_proof _ _ = ()
 
 let begin_subproof _ = ()
 let end_subproof _ = ()
@@ -26,5 +26,5 @@ let lemma_isa_split _ _ = ()
 let lemma_bool_tauto _ _ = ()
 let lemma_bool_c _ _ _ = ()
 let lemma_bool_equiv _ _ _ = ()
-let lemma_ite_true _ ~a:_ ~ite:_  = ()
-let lemma_ite_false _ ~a:_ ~ite:_  = ()
+let lemma_ite_true ~a:_ ~ite:_ _ = ()
+let lemma_ite_false ~a:_ ~ite:_ _ = ()
diff --git a/src/base/Proof_stub.mli b/src/base/Proof_stub.mli
index 17a6bf59..e73fed02 100644
--- a/src/base/Proof_stub.mli
+++ b/src/base/Proof_stub.mli
@@ -9,14 +9,14 @@ include Sidekick_core.PROOF
 
 val create : unit -> t
 
-val lemma_bool_tauto : t -> Lit.t Iter.t -> unit
-val lemma_bool_c : t -> string -> term list -> unit
-val lemma_bool_equiv : t -> term -> term -> unit
-val lemma_ite_true : t -> a:term -> ite:term -> unit
-val lemma_ite_false : t -> a:term -> ite:term -> unit
+val lemma_bool_tauto : Lit.t Iter.t -> t -> unit
+val lemma_bool_c : string -> term list -> t -> unit
+val lemma_bool_equiv : term -> term -> t -> unit
+val lemma_ite_true : a:term -> ite:term -> t -> unit
+val lemma_ite_false : a:term -> ite:term -> t -> unit
 
-val lemma_lra : t -> Lit.t Iter.t -> unit
+val lemma_lra : Lit.t Iter.t -> t -> unit
 
-val lemma_isa_split : t -> Lit.t Iter.t -> unit
-val lemma_isa_disj : t -> Lit.t Iter.t -> unit
-val lemma_cstor_inj : t -> Lit.t Iter.t -> unit
+val lemma_isa_split : Lit.t Iter.t -> t -> unit
+val lemma_isa_disj : Lit.t Iter.t -> t -> unit
+val lemma_cstor_inj : Lit.t Iter.t -> t -> unit
diff --git a/src/cc/Sidekick_cc.ml b/src/cc/Sidekick_cc.ml
index 7fc3faff..949e1230 100644
--- a/src/cc/Sidekick_cc.ml
+++ b/src/cc/Sidekick_cc.ml
@@ -660,7 +660,7 @@ module Make (A: CC_ARG)
         let lits = explain_equal cc ~th lits b rb in
         let emit_proof p =
           let p_lits = Iter.of_list lits |> Iter.map Lit.neg in
-          P.lemma_cc p p_lits in
+          P.lemma_cc p_lits p in
         raise_conflict_ cc ~th:!th acts (List.rev_map Lit.neg lits) emit_proof
       );
       (* We will merge [r_from] into [r_into].
@@ -779,7 +779,7 @@ module Make (A: CC_ARG)
                let emit_proof p =
                  (* make a tautology, not a true guard *)
                  let p_lits = Iter.cons lit (Iter.of_list lits |> Iter.map Lit.neg) in
-                 P.lemma_cc p p_lits
+                 P.lemma_cc p_lits p
                in
                lits, emit_proof
              ) in
@@ -850,7 +850,7 @@ module Make (A: CC_ARG)
     let lits = List.rev_map Lit.neg lits in
     let emit_proof p =
       let p_lits = Iter.of_list lits in
-      P.lemma_cc p p_lits
+      P.lemma_cc p_lits p
     in
     raise_conflict_ cc ~th:!th acts lits emit_proof
 
diff --git a/src/core/Sidekick_core.ml b/src/core/Sidekick_core.ml
index 5945210f..ffcc279d 100644
--- a/src/core/Sidekick_core.ml
+++ b/src/core/Sidekick_core.ml
@@ -150,7 +150,7 @@ module type CC_PROOF = sig
   type t
   type lit
 
-  val lemma_cc : t -> lit Iter.t -> unit
+  val lemma_cc : lit Iter.t -> t -> unit
   (** [lemma_cc proof lits] asserts that [lits] form a tautology for the theory
       of uninterpreted functions. *)
 end
@@ -169,17 +169,18 @@ module type SAT_PROOF = sig
   type dproof = t -> unit
   (** A delayed proof, used to produce proofs on demand from theories. *)
 
-  val enabled : t -> bool
-  (** Do we emit proofs at all? *)
+  val with_proof : t -> (t -> unit) -> unit
+  (** If proof is enabled, call [f] on it to emit steps.
+      if proof is disabled, the callback won't even be called. *)
 
-  val emit_input_clause : t -> lit Iter.t -> unit
+  val emit_input_clause : lit Iter.t -> t -> unit
   (** Emit an input clause. *)
 
-  val emit_redundant_clause : t -> lit Iter.t -> unit
+  val emit_redundant_clause : lit Iter.t -> t -> unit
   (** Emit a clause deduced by the SAT solver, redundant wrt axioms.
       The clause must be RUP wrt previous clauses. *)
 
-  val del_clause : t -> lit Iter.t -> unit
+  val del_clause : lit Iter.t -> t -> unit
   (** Forget a clause. Only useful for performance considerations. *)
   (* TODO: replace with something index-based? *)
 end
@@ -215,20 +216,17 @@ module type PROOF = sig
   (** [end_subproof p] ends the current active subproof, the last result
       of which is kept. *)
 
-  val define_term : t -> term -> term -> unit
+  val define_term : term -> term -> t -> unit
   (** [define_term p cst u] defines the new constant [cst] as being equal
       to [u]. *)
 
-  val lemma_true : t -> term -> unit
+  val lemma_true : term -> t -> unit
   (** [lemma_true p (true)] asserts the clause [(true)] *)
 
-  val lemma_preprocess : t -> term -> term -> unit
+  val lemma_preprocess : term -> term -> t -> unit
   (** [lemma_preprocess p t u] asserts that [t = u] is a tautology
       and that [t] has been preprocessed into [u].
       From now on, [t] and [u] will be used interchangeably. *)
-
-  val enabled : t -> bool
-  (** Is proof production enabled? *)
 end
 
 (** Literals
@@ -662,9 +660,11 @@ module type SOLVER_INTERNAL = sig
   val ty_st : t -> ty_store
   val stats : t -> Stat.t
 
+  val with_proof : t -> (proof -> unit) -> unit
+
   (** {3 Actions for the theories} *)
 
-  type actions
+  type theory_actions
   (** Handle that the theories can use to perform actions. *)
 
   type lit = Lit.t
@@ -685,7 +685,7 @@ module type SOLVER_INTERNAL = sig
      and type proof = proof
      and type P.t = proof
      and type P.lit = lit
-     and type Actions.t = actions
+     and type Actions.t = theory_actions
 
   val cc : t -> CC.t
   (** Congruence closure for this solver *)
@@ -702,19 +702,21 @@ module type SOLVER_INTERNAL = sig
     val clear : t -> unit
     (** Reset internal cache, etc. *)
 
-    type hook = t -> term -> (term * dproof) option
+    val with_proof : t -> (proof -> unit) -> unit
+
+    type hook = t -> term -> term option
     (** Given a term, try to simplify it. Return [None] if it didn't change.
 
         A simple example could be a hook that takes a term [t],
         and if [t] is [app "+" (const x) (const y)] where [x] and [y] are number,
         returns [Some (const (x+y))], and [None] otherwise. *)
 
-    val normalize : t -> term -> (term * dproof) option
+    val normalize : t -> term -> term option
     (** Normalize a term using all the hooks. This performs
         a fixpoint, i.e. it only stops when no hook applies anywhere inside
         the term. *)
 
-    val normalize_t : t -> term -> term * dproof
+    val normalize_t : t -> term -> term
     (** Normalize a term using all the hooks, along with a proof that the
         simplification is correct.
         returns [t, refl t] if no simplification occurred. *)
@@ -727,58 +729,99 @@ module type SOLVER_INTERNAL = sig
 
   val simplifier : t -> Simplify.t
 
-  val simplify_t : t -> term -> (term * dproof) option
-  (** Simplify input term, returns [Some (u, |- t=u)] if some
+  val simplify_t : t -> term -> term option
+  (** Simplify input term, returns [Some u] if some
       simplification occurred. *)
 
-  val simp_t : t -> term -> term * dproof
-  (** [simp_t si t] returns [u, |- t=u] even if no simplification occurred
+  val simp_t : t -> term -> term
+  (** [simp_t si t] returns [u] even if no simplification occurred
       (in which case [t == u] syntactically).
+      It emits [|- t=u].
       (see {!simplifier}) *)
 
+  (** {3 Preprocessors}
+      These preprocessors turn mixed, raw literals (possibly simplified) into
+      literals suitable for reasoning.
+      Typically some clauses are also added to the solver. *)
+
+  module type PREPROCESS_ACTS = sig
+    val mk_lit : ?sign:bool -> term -> lit
+    (** creates a new literal for a boolean term. *)
+
+    val add_clause : lit list -> dproof -> unit
+    (** pushes a new clause into the SAT solver. *)
+
+    val add_lit : ?default_pol:bool -> lit -> unit
+    (** Ensure the literal will be decided/handled by the SAT solver. *)
+  end
+
+  type preprocess_actions = (module PREPROCESS_ACTS)
+  (** Actions available to the preprocessor *)
+
+  type preprocess_hook =
+    t ->
+    preprocess_actions ->
+    term -> term option
+  (** Given a term, try to preprocess it. Return [None] if it didn't change,
+      or [Some (u)] if [t=u].
+      Can also add clauses to define new terms.
+
+      Preprocessing might transform terms to make them more amenable
+      to reasoning, e.g. by removing boolean formulas via Tseitin encoding,
+      adding clauses that encode their meaning in the same move.
+
+      @param preprocess_actions actions available during preprocessing.
+  *)
+
+  val on_preprocess : t -> preprocess_hook -> unit
+  (** Add a hook that will be called when terms are preprocessed *)
+
+  val preprocess_acts_of_acts : t -> theory_actions -> preprocess_actions
+  (** Obtain preprocessor actions, from theory actions *)
+
   (** {3 hooks for the theory} *)
 
-  val raise_conflict : t -> actions -> lit list -> dproof -> 'a
+  val raise_conflict : t -> theory_actions -> lit list -> dproof -> 'a
   (** Give a conflict clause to the solver *)
 
-  val push_decision : t -> actions -> lit -> unit
+  val push_decision : t -> theory_actions -> lit -> unit
   (** Ask the SAT solver to decide the given literal in an extension of the
       current trail. This is useful for theory combination.
       If the SAT solver backtracks, this (potential) decision is removed
       and forgotten. *)
 
-  val propagate: t -> actions -> lit -> reason:(unit -> lit list * dproof) -> unit
+  val propagate: t -> theory_actions -> lit -> reason:(unit -> lit list * dproof) -> unit
   (** Propagate a boolean using a unit clause.
       [expl => lit] must be a theory lemma, that is, a T-tautology *)
 
-  val propagate_l: t -> actions -> lit -> lit list -> dproof -> unit
+  val propagate_l: t -> theory_actions -> lit -> lit list -> dproof -> unit
   (** Propagate a boolean using a unit clause.
       [expl => lit] must be a theory lemma, that is, a T-tautology *)
 
-  val add_clause_temp : t -> actions -> lit list -> dproof -> unit
+  val add_clause_temp : t -> theory_actions -> lit list -> dproof -> unit
   (** Add local clause to the SAT solver. This clause will be
       removed when the solver backtracks. *)
 
-  val add_clause_permanent : t -> actions -> lit list -> dproof -> unit
+  val add_clause_permanent : t -> theory_actions -> lit list -> dproof -> unit
   (** Add toplevel clause to the SAT solver. This clause will
       not be backtracked. *)
 
-  val mk_lit : t -> actions -> ?sign:bool -> term -> lit
+  val mk_lit : t -> theory_actions -> ?sign:bool -> term -> lit
   (** Create a literal. This automatically preprocesses the term. *)
 
-  val preprocess_term :
-    t -> add_clause:(Lit.t list -> dproof -> unit) -> term -> term * dproof
-  (** Preprocess a term. *)
+  val preprocess_term : t -> preprocess_actions -> term -> term
+  (** Preprocess a term. The preprocessing proof is automatically emitted. *)
 
-  val add_lit : t -> actions -> lit -> unit
+  val add_lit : t -> theory_actions -> ?default_pol:bool -> lit -> unit
   (** Add the given literal to the SAT solver, so it gets assigned
-      a boolean value *)
+      a boolean value.
+      @param default_pol default polarity for the corresponding atom *)
 
-  val add_lit_t : t -> actions -> ?sign:bool -> term -> unit
+  val add_lit_t : t -> theory_actions -> ?sign:bool -> term -> unit
   (** Add the given (signed) bool term to the SAT solver, so it gets assigned
       a boolean value *)
 
-  val cc_raise_conflict_expl : t -> actions -> CC.Expl.t -> 'a
+  val cc_raise_conflict_expl : t -> theory_actions -> CC.Expl.t -> 'a
   (** Raise a conflict with the given congruence closure explanation.
       it must be a theory tautology that [expl ==> absurd].
       To be used in theories. *)
@@ -789,12 +832,12 @@ module type SOLVER_INTERNAL = sig
   val cc_are_equal : t -> term -> term -> bool
   (** Are these two terms equal in the congruence closure? *)
 
-  val cc_merge : t -> actions -> CC.N.t -> CC.N.t -> CC.Expl.t -> unit
+  val cc_merge : t -> theory_actions -> CC.N.t -> CC.N.t -> CC.Expl.t -> unit
   (** Merge these two nodes in the congruence closure, given this explanation.
       It must be a theory tautology that [expl ==> n1 = n2].
       To be used in theories. *)
 
-  val cc_merge_t : t -> actions -> term -> term -> CC.Expl.t -> unit
+  val cc_merge_t : t -> theory_actions -> term -> term -> CC.Expl.t -> unit
   (** Merge these two terms in the congruence closure, given this explanation.
       See {!cc_merge} *)
 
@@ -806,10 +849,10 @@ module type SOLVER_INTERNAL = sig
   (** Return [true] if the term is explicitly in the congruence closure.
       To be used in theories *)
 
-  val on_cc_pre_merge : t -> (CC.t -> actions -> CC.N.t -> CC.N.t -> CC.Expl.t -> unit) -> unit
+  val on_cc_pre_merge : t -> (CC.t -> theory_actions -> CC.N.t -> CC.N.t -> CC.Expl.t -> unit) -> unit
   (** Callback for when two classes containing data for this key are merged (called before) *)
 
-  val on_cc_post_merge : t -> (CC.t -> actions -> CC.N.t -> CC.N.t -> unit) -> unit
+  val on_cc_post_merge : t -> (CC.t -> theory_actions -> CC.N.t -> CC.N.t -> unit) -> unit
   (** Callback for when two classes containing data for this key are merged (called after)*)
 
   val on_cc_new_term : t -> (CC.t -> CC.N.t -> term -> unit) -> unit
@@ -826,7 +869,7 @@ module type SOLVER_INTERNAL = sig
   val on_cc_propagate : t -> (CC.t -> lit -> (unit -> lit list * dproof) -> unit) -> unit
   (** Callback called on every CC propagation *)
 
-  val on_partial_check : t -> (t -> actions -> lit Iter.t -> unit) -> unit
+  val on_partial_check : t -> (t -> theory_actions -> lit Iter.t -> unit) -> unit
   (** Register callbacked to be called with the slice of literals
       newly added on the trail.
 
@@ -834,7 +877,7 @@ module type SOLVER_INTERNAL = sig
       to be complete, only correct. It's given only the slice of
       the trail consisting in new literals. *)
 
-  val on_final_check: t -> (t -> actions -> lit Iter.t -> unit) -> unit
+  val on_final_check: t -> (t -> theory_actions -> lit Iter.t -> unit) -> unit
   (** Register callback to be called during the final check.
 
       Must be complete (i.e. must raise a conflict if the set of literals is
@@ -842,31 +885,6 @@ module type SOLVER_INTERNAL = sig
       is given the whole trail.
   *)
 
-  (** {3 Preprocessors}
-      These preprocessors turn mixed, raw literals (possibly simplified) into
-      literals suitable for reasoning.
-      Typically some clauses are also added to the solver. *)
-
-  type preprocess_hook =
-    t ->
-    mk_lit:(term -> lit) ->
-    add_clause:(lit list -> dproof -> unit) ->
-    term -> (term * dproof) option
-  (** Given a term, try to preprocess it. Return [None] if it didn't change,
-      or [Some (u,p)] if [t=u] and [p] is a proof of [t=u].
-      Can also add clauses to define new terms.
-
-      Preprocessing might transform terms to make them more amenable
-      to reasoning, e.g. by removing boolean formulas via Tseitin encoding,
-      adding clauses that encode their meaning in the same move.
-
-      @param mk_lit creates a new literal for a boolean term.
-      @param add_clause pushes a new clause into the SAT solver.
-  *)
-
-  val on_preprocess : t -> preprocess_hook -> unit
-  (** Add a hook that will be called when terms are preprocessed *)
-
   (** {3 Model production} *)
 
   type model_hook =
@@ -1041,13 +1059,12 @@ module type SOLVER = sig
 
   val add_theory_l : t -> theory list -> unit
 
-  val mk_lit_t : t -> ?sign:bool -> term -> lit * dproof
-  (** [mk_lit_t _ ~sign t] returns [lit, pr]
-      where [lit] is a internal representation of [± t],
-      and [pr] is a proof of [|- lit = (± t)] *)
+  val mk_lit_t : t -> ?sign:bool -> term -> lit
+  (** [mk_lit_t _ ~sign t] returns [lit'],
+      where [lit'] is [preprocess(lit)] and [lit] is
+      an internal representation of [± t].
 
-  val mk_lit_t' : t -> ?sign:bool -> term -> lit
-  (** Like {!mk_lit_t} but skips the proof *)
+      The proof of [|- lit = lit'] is directly added to the solver's proof. *)
 
   val add_clause : t -> lit IArray.t -> dproof -> unit
   (** [add_clause solver cs] adds a boolean clause to the solver.
diff --git a/src/lra/sidekick_arith_lra.ml b/src/lra/sidekick_arith_lra.ml
index f31285cf..abadae5f 100644
--- a/src/lra/sidekick_arith_lra.ml
+++ b/src/lra/sidekick_arith_lra.ml
@@ -60,7 +60,7 @@ module type ARG = sig
   val has_ty_real : term -> bool
   (** Does this term have the type [Real] *)
 
-  val lemma_lra : S.proof -> S.Lit.t Iter.t -> unit
+  val lemma_lra : S.Lit.t Iter.t -> S.proof -> unit
 
   module Gensym : sig
     type t
@@ -233,29 +233,18 @@ module Make(A : ARG) : S with module A = A = struct
         );
         proxy
 
-  let add_clause_lra_ ~add_clause lits =
-    let emit_proof p =
-      A.lemma_lra p (Iter.of_list lits)
-    in
-    add_clause lits emit_proof
+  let add_clause_lra_ (module PA:SI.PREPROCESS_ACTS) lits =
+    let pr = A.lemma_lra (Iter.of_list lits) in
+    PA.add_clause lits pr
 
   (* preprocess linear expressions away *)
-  let preproc_lra (self:state) si ~mk_lit ~add_clause
-      (t:T.t) : (T.t * _) option =
-    Log.debugf 50 (fun k->k "lra.preprocess %a" T.pp t);
+  let preproc_lra (self:state) si (module PA:SI.PREPROCESS_ACTS)
+      (t:T.t) : T.t option =
+    Log.debugf 50 (fun k->k "(@[lra.preprocess@ %a@])" T.pp t);
     let tst = SI.tst si in
 
-    let sub_proofs_ = ref [] in
-
     (* preprocess subterm *)
-    let preproc_t t =
-      let u, p_t_eq_u = SI.preprocess_term ~add_clause si t in
-      if t != u then (
-        (* add [|- t=u] to hyps *)
-        sub_proofs_ := (t,u,p_t_eq_u) :: !sub_proofs_;
-      );
-      u
-    in
+    let preproc_t t = SI.preprocess_term si (module PA) t in
 
     (* tell the CC this term exists *)
     let declare_term_to_cc t =
@@ -274,12 +263,12 @@ module Make(A : ARG) : S with module A = A = struct
         T.Tbl.add self.encoded_eqs t ();
 
         (* encode [t <=> (u1 /\ u2)] *)
-        let lit_t = mk_lit t in
-        let lit_u1 = mk_lit u1 in
-        let lit_u2 = mk_lit u2 in
-        add_clause_lra_ ~add_clause [SI.Lit.neg lit_t; lit_u1];
-        add_clause_lra_ ~add_clause [SI.Lit.neg lit_t; lit_u2];
-        add_clause_lra_ ~add_clause
+        let lit_t = PA.mk_lit t in
+        let lit_u1 = PA.mk_lit u1 in
+        let lit_u2 = PA.mk_lit u2 in
+        add_clause_lra_ (module PA) [SI.Lit.neg lit_t; lit_u1];
+        add_clause_lra_ (module PA) [SI.Lit.neg lit_t; lit_u2];
+        add_clause_lra_ (module PA)
           [SI.Lit.neg lit_u1; SI.Lit.neg lit_u2; lit_t];
       );
       None
@@ -309,14 +298,14 @@ module Make(A : ARG) : S with module A = A = struct
 
           let new_t = A.mk_lra tst (LRA_simplex_pred (proxy, op, le_const)) in
           begin
-            let lit = mk_lit new_t in
+            let lit = PA.mk_lit new_t in
             let constr = SimpSolver.Constraint.mk proxy op le_const in
             SimpSolver.declare_bound self.simplex constr (Tag.Lit lit);
           end;
 
           Log.debugf 10 (fun k->k "lra.preprocess:@ %a@ :into %a" T.pp t T.pp new_t);
-          (* FIXME: by def proxy + LRA *)
-          Some (new_t, (fun _ -> ()))
+          (* FIXME: emit proof: by def proxy + LRA *)
+          Some new_t
 
         | Some (coeff, v), pred ->
           (* [c . v <= const] becomes a direct simplex constraint [v <= const/c] *)
@@ -335,15 +324,14 @@ module Make(A : ARG) : S with module A = A = struct
 
           let new_t = A.mk_lra tst (LRA_simplex_pred (v, op, q)) in
           begin
-            let lit = mk_lit new_t in
+            let lit = PA.mk_lit new_t in
             let constr = SimpSolver.Constraint.mk v op q in
             SimpSolver.declare_bound self.simplex constr (Tag.Lit lit);
           end;
 
           Log.debugf 10 (fun k->k "lra.preprocess@ :%a@ :into %a" T.pp t T.pp new_t);
           (* FIXME: preprocess proof *)
-          let emit_proof _ = () in
-          Some (new_t, emit_proof)
+          Some new_t
       end
 
     | LRA_op _ | LRA_mult _ ->
@@ -357,9 +345,7 @@ module Make(A : ARG) : S with module A = A = struct
         declare_term_to_cc proxy;
 
         (* FIXME: proof by def of proxy *)
-        let emit_proof _ = () in
-
-        Some (proxy, emit_proof)
+        Some proxy
       ) else (
         (* a bit more complicated: we cannot just define [proxy := le_comb]
            because of the coefficient.
@@ -382,29 +368,30 @@ module Make(A : ARG) : S with module A = A = struct
         declare_term_to_cc proxy;
         declare_term_to_cc proxy2;
 
-        add_clause [
-          mk_lit (A.mk_lra tst (LRA_simplex_pred (proxy2, Leq, A.Q.neg le_const)))
+        PA.add_clause [
+          PA.mk_lit (A.mk_lra tst (LRA_simplex_pred (proxy2, Leq, A.Q.neg le_const)))
         ] (fun _ -> ()); (* TODO: by-def proxy2 + LRA *)
-        add_clause [
-          mk_lit (A.mk_lra tst (LRA_simplex_pred (proxy2, Geq, A.Q.neg le_const)))
+        PA.add_clause [
+          PA.mk_lit (A.mk_lra tst (LRA_simplex_pred (proxy2, Geq, A.Q.neg le_const)))
         ] (fun _ -> ()); (* TODO: by-def proxy2 + LRA *)
 
         (* FIXME: actual proof *)
-        let emit_proof _ = () in
-        Some (proxy, emit_proof)
+        Some proxy
       )
 
     | LRA_other t when A.has_ty_real t -> None
-    | LRA_const _ | LRA_simplex_pred _ | LRA_simplex_var _ | LRA_other _ -> None
+    | LRA_const _ | LRA_simplex_pred _ | LRA_simplex_var _ | LRA_other _ ->
+      Log.debug 0 "LRA NONE";
+      None
 
-  let simplify (self:state) (_recurse:_) (t:T.t) : (T.t * SI.dproof) option =
+  let simplify (self:state) (_recurse:_) (t:T.t) : T.t option =
     match A.view_as_lra t with
     | LRA_op _ | LRA_mult _ ->
       let le = as_linexp_id t in
       if LE.is_const le then (
         let c = LE.const le in
         (* FIXME: proof *)
-        Some (A.mk_lra self.tst (LRA_const c), (fun _ -> ()))
+        Some (A.mk_lra self.tst (LRA_const c))
       ) else None
     | LRA_pred (pred, l1, l2) ->
       let le = LE.(as_linexp_id l1 - as_linexp_id l2) in
@@ -419,7 +406,7 @@ module Make(A : ARG) : S with module A = A = struct
           | Neq -> A.Q.(c <> zero)
         in
         (* FIXME: proof *)
-        Some (A.mk_bool self.tst is_true, (fun _ -> ()))
+        Some (A.mk_bool self.tst is_true)
       ) else None
     | _ -> None
 
@@ -433,8 +420,8 @@ module Make(A : ARG) : S with module A = A = struct
       |> CCList.flat_map (Tag.to_lits si)
       |>  List.rev_map SI.Lit.neg
     in
-    let emit_proof p = A.lemma_lra p (Iter.of_list confl) in
-    SI.raise_conflict si acts confl emit_proof
+    let pr = A.lemma_lra (Iter.of_list confl) in
+    SI.raise_conflict si acts confl pr
 
   let on_propagate_ si acts lit ~reason =
     match lit with
@@ -443,10 +430,8 @@ module Make(A : ARG) : S with module A = A = struct
       SI.propagate si acts lit
         ~reason:(fun() ->
            let lits = CCList.flat_map (Tag.to_lits si) reason in
-           let emit_proof p =
-             A.lemma_lra p Iter.(cons lit (of_list lits))
-           in
-           CCList.flat_map (Tag.to_lits si) reason, emit_proof)
+           let pr = A.lemma_lra Iter.(cons lit (of_list lits)) in
+           CCList.flat_map (Tag.to_lits si) reason, pr)
     | _ -> ()
 
   let check_simplex_ self si acts : SimpSolver.Subst.t =
@@ -594,7 +579,7 @@ module Make(A : ARG) : S with module A = A = struct
     );
     ()
 
-  let final_check_ (self:state) si (acts:SI.actions) (_trail:_ Iter.t) : unit =
+  let final_check_ (self:state) si (acts:SI.theory_actions) (_trail:_ Iter.t) : unit =
     Log.debug 5 "(th-lra.final-check)";
     Profile.with_ "lra.final-check" @@ fun () ->
 
diff --git a/src/main/pure_sat_solver.ml b/src/main/pure_sat_solver.ml
index bac32b19..e591f870 100644
--- a/src/main/pure_sat_solver.ml
+++ b/src/main/pure_sat_solver.ml
@@ -38,26 +38,26 @@ end = struct
       }
   type dproof = t -> unit
 
-  let[@inline] enabled = function
-    | Dummy -> false
-    | Inner _ -> true
+  let[@inline] with_proof pr f = match pr with
+    | Dummy -> ()
+    | Inner _ -> f pr
 
   let emit_lits_ buf lits =
     lits (fun i -> bpf buf "%d " i)
 
-  let emit_input_clause self lits =
+  let emit_input_clause lits self =
     match self with
     | Dummy -> ()
     | Inner {buf} ->
       bpf buf "i "; emit_lits_ buf lits; bpf buf "0\n"
 
-  let emit_redundant_clause self lits =
+  let emit_redundant_clause lits self =
     match self with
     | Dummy -> ()
     | Inner {buf} ->
       bpf buf "r "; emit_lits_ buf lits; bpf buf "0\n"
 
-  let del_clause self lits =
+  let del_clause lits self =
     match self with
     | Dummy -> ()
     | Inner {buf} ->
diff --git a/src/sat/Solver.ml b/src/sat/Solver.ml
index bbe83970..2b31da92 100644
--- a/src/sat/Solver.ml
+++ b/src/sat/Solver.ml
@@ -1402,7 +1402,7 @@ module Make(Plugin : PLUGIN)
     let atoms = List.rev_map (make_atom_ self) l in
     let removable = not keep in
     let c = Clause.make_l self.store ~removable atoms in
-    if Proof.enabled self.proof then dp self.proof;
+    Proof.with_proof self.proof dp;
     Log.debugf 5 (fun k->k "(@[sat.th.add-clause@ %a@])" (Clause.debug self.store) c);
     Vec.push self.clauses_to_add c
 
@@ -1415,11 +1415,11 @@ module Make(Plugin : PLUGIN)
       self.next_decisions <- a :: self.next_decisions
     )
 
-  let acts_raise self (l:lit list) (pr:dproof) : 'a =
+  let acts_raise self (l:lit list) (dp:dproof) : 'a =
     let atoms = List.rev_map (make_atom_ self) l in
     (* conflicts can be removed *)
     let c = Clause.make_l self.store ~removable:true atoms in
-    if Proof.enabled self.proof then pr self.proof;
+    Proof.with_proof self.proof dp;
     Log.debugf 5 (fun k->k "(@[@{<yellow>sat.th.raise-conflict@}@ %a@])"
                      (Clause.debug self.store) c);
     raise_notrace (Th_conflict c)
@@ -1444,7 +1444,7 @@ module Make(Plugin : PLUGIN)
         let l = List.rev_map (fun f -> Atom.neg @@ make_atom_ self f) lits in
         check_consequence_lits_false_ self l;
         let c = Clause.make_l store ~removable:true (p :: l) in
-        if Proof.enabled self.proof then dp self.proof;
+        Proof.with_proof self.proof dp;
         raise_notrace (Th_conflict c)
       ) else (
         insert_var_order self (Atom.var p);
@@ -1458,7 +1458,7 @@ module Make(Plugin : PLUGIN)
              (otherwise the propagated lit would have been backtracked and
              discarded already.) *)
           check_consequence_lits_false_ self l;
-          if Proof.enabled self.proof then dp self.proof;
+          Proof.with_proof self.proof dp;
           Clause.make_l store ~removable:true (p :: l)
         ) in
         let level = decision_level self in
@@ -1481,7 +1481,7 @@ module Make(Plugin : PLUGIN)
     let a = make_atom_ self f in
     eval_atom_ self a
 
-  let[@inline] acts_mk_lit self ?default_pol f : unit =
+  let[@inline] acts_add_lit self ?default_pol f : unit =
     ignore (make_atom_ ?default_pol self f : atom)
 
   let[@inline] current_slice st : _ Solver_intf.acts =
@@ -1491,7 +1491,7 @@ module Make(Plugin : PLUGIN)
       type nonrec lit = lit
       let iter_assumptions=acts_iter st ~full:false st.th_head
       let eval_lit= acts_eval_lit st
-      let mk_lit=acts_mk_lit st
+      let add_lit=acts_add_lit st
       let add_clause = acts_add_clause st
       let propagate = acts_propagate st
       let raise_conflict c pr=acts_raise st c pr
@@ -1507,7 +1507,7 @@ module Make(Plugin : PLUGIN)
       type nonrec lit = lit
       let iter_assumptions=acts_iter st ~full:true st.th_head
       let eval_lit= acts_eval_lit st
-      let mk_lit=acts_mk_lit st
+      let add_lit=acts_add_lit st
       let add_clause = acts_add_clause st
       let propagate = acts_propagate st
       let raise_conflict c pr=acts_raise st c pr
@@ -1830,9 +1830,8 @@ module Make(Plugin : PLUGIN)
       (fun l ->
          let atoms = Util.array_of_list_map (make_atom_ self) l in
          let c = Clause.make_a self.store ~removable:false atoms in
-         if Proof.enabled self.proof then (
-           Proof.emit_input_clause self.proof (Iter.of_list l)
-         );
+         Proof.with_proof self.proof
+           (Proof.emit_input_clause (Iter.of_list l));
          Log.debugf 10 (fun k -> k "(@[sat.assume-clause@ @[<hov 2>%a@]@])"
                            (Clause.debug self.store) c);
          Vec.push self.clauses_to_add c)
@@ -1843,6 +1842,7 @@ module Make(Plugin : PLUGIN)
   let[@inline] proof st = st.proof
 
   let[@inline] add_lit self ?default_pol lit =
+    Log.debugf 0 (fun k->k"add lit %a" Lit.pp lit); (* XXX *)
     ignore (make_atom_ self lit ?default_pol : atom)
   let[@inline] set_default_pol (self:t) (lit:lit) (pol:bool) : unit =
     let a = make_atom_ self lit ~default_pol:pol in
@@ -1906,7 +1906,7 @@ module Make(Plugin : PLUGIN)
   let add_clause_atoms_ self (c:atom array) dp : unit =
     try
       let c = Clause.make_a self.store ~removable:false c in
-      if Proof.enabled self.proof then dp self.proof;
+      Proof.with_proof self.proof dp;
       add_clause_ self c
     with
     | E_unsat (US_false c) ->
@@ -1921,12 +1921,12 @@ module Make(Plugin : PLUGIN)
     add_clause_atoms_ self c dp
 
   let add_input_clause self (c:lit list) =
-    let emit_proof p = Proof.emit_input_clause p (Iter.of_list c) in
-    add_clause self c emit_proof
+    let dp = Proof.emit_input_clause (Iter.of_list c) in
+    add_clause self c dp
 
   let add_input_clause_a self c =
-    let emit_proof p = Proof.emit_input_clause p (Iter.of_array c) in
-    add_clause_a self c emit_proof
+    let dp = Proof.emit_input_clause (Iter.of_array c) in
+    add_clause_a self c dp
 
   let solve ?(assumptions=[]) (self:t) : res =
     cancel_until self 0;
diff --git a/src/sat/Solver_intf.ml b/src/sat/Solver_intf.ml
index ab9fc650..a53533c2 100644
--- a/src/sat/Solver_intf.ml
+++ b/src/sat/Solver_intf.ml
@@ -93,8 +93,8 @@ module type ACTS = sig
   val eval_lit: lit -> lbool
   (** Obtain current value of the given literal *)
 
-  val mk_lit: ?default_pol:bool -> lit -> unit
-  (** Map the given lit to a literal, which will be decided by the
+  val add_lit: ?default_pol:bool -> lit -> unit
+  (** Map the given lit to an internal atom, which will be decided by the
       SAT solver. *)
 
   val add_clause: ?keep:bool -> lit list -> dproof -> unit
diff --git a/src/smt-solver/Sidekick_smt_solver.ml b/src/smt-solver/Sidekick_smt_solver.ml
index d8c728e8..4a5156bd 100644
--- a/src/smt-solver/Sidekick_smt_solver.ml
+++ b/src/smt-solver/Sidekick_smt_solver.ml
@@ -103,27 +103,28 @@ module Make(A : ARG)
           next: th_states;
         } -> th_states
 
-    type actions = sat_acts
+    type theory_actions = sat_acts
 
     module Simplify = struct
       type t = {
         tst: term_store;
         ty_st: ty_store;
+        proof: proof;
         mutable hooks: hook list;
         cache: Term.t Term.Tbl.t;
       }
-      and hook = t -> term -> (term * dproof) option
+      and hook = t -> term -> term option
+
+      let create tst ty_st ~proof : t =
+        {tst; ty_st; proof; hooks=[]; cache=Term.Tbl.create 32;}
 
-      let create tst ty_st : t =
-        {tst; ty_st; hooks=[]; cache=Term.Tbl.create 32;}
       let[@inline] tst self = self.tst
       let[@inline] ty_st self = self.ty_st
+      let[@inline] with_proof self f = P.with_proof self.proof f
       let add_hook self f = self.hooks <- f :: self.hooks
       let clear self = Term.Tbl.clear self.cache
 
-      let normalize (self:t) (t:Term.t) : (Term.t * dproof) option =
-        let sub_proofs_: dproof list ref = ref [] in
-
+      let normalize (self:t) (t:Term.t) : Term.t option =
         (* compute and cache normal form of [t] *)
         let rec aux t : Term.t =
           match Term.Tbl.find self.cache t with
@@ -140,33 +141,31 @@ module Make(A : ARG)
           | h :: hooks_tl ->
             match h self t with
             | None -> aux_rec t hooks_tl
-            | Some (u, _) when Term.equal t u -> aux_rec t hooks_tl
-            | Some (u, pr_t_u) ->
-              sub_proofs_ := pr_t_u :: !sub_proofs_;
-              aux u
+            | Some u when Term.equal t u -> aux_rec t hooks_tl
+            | Some u -> aux u (* fixpoint *)
         in
         let u = aux t in
         if Term.equal t u then None
         else (
           (* proof: [sub_proofs |- t=u] by CC + subproof *)
-          let emit_proof p =
-            if not (T.Term.equal t u) then (
-              P.begin_subproof p;
-              List.iter (fun dp -> dp p) !sub_proofs_;
-              P.lemma_preprocess p t u;
-              P.end_subproof p;
-            )
-          in
-          Some (u, emit_proof)
+          P.with_proof self.proof (P.lemma_preprocess t u);
+          Some u
         )
 
       let normalize_t self t =
         match normalize self t with
-        | Some (u,pr) -> u, pr
-        | None -> t, (fun _ -> ())
+        | Some u -> u
+        | None -> t
     end
     type simplify_hook = Simplify.hook
 
+    module type PREPROCESS_ACTS = sig
+      val mk_lit : ?sign:bool -> term -> lit
+      val add_clause : lit list -> dproof -> unit
+      val add_lit : ?default_pol:bool -> lit -> unit
+    end
+    type preprocess_actions = (module PREPROCESS_ACTS)
+
     type t = {
       tst: Term.store; (** state for managing terms *)
       ty_st: Ty.store;
@@ -181,19 +180,18 @@ module Make(A : ARG)
       simp: Simplify.t;
       mutable preprocess: preprocess_hook list;
       mutable mk_model: model_hook list;
-      preprocess_cache: (Term.t * dproof list) Term.Tbl.t;
+      preprocess_cache: Term.t Term.Tbl.t;
       mutable t_defs : (term*term) list; (* term definitions *)
       mutable th_states : th_states; (** Set of theories *)
-      mutable on_partial_check: (t -> actions -> lit Iter.t -> unit) list;
-      mutable on_final_check: (t -> actions -> lit Iter.t -> unit) list;
+      mutable on_partial_check: (t -> theory_actions -> lit Iter.t -> unit) list;
+      mutable on_final_check: (t -> theory_actions -> lit Iter.t -> unit) list;
       mutable level: int;
     }
 
     and preprocess_hook =
       t ->
-      mk_lit:(term -> lit) ->
-      add_clause:(lit list -> dproof -> unit) ->
-      term -> (term * dproof) option
+      preprocess_actions ->
+      term -> term option
 
     and model_hook =
       recurse:(t -> CC.N.t -> term) ->
@@ -208,6 +206,7 @@ module Make(A : ARG)
     let[@inline] cc (t:t) = Lazy.force t.cc
     let[@inline] tst t = t.tst
     let[@inline] ty_st t = t.ty_st
+    let[@inline] with_proof self f = Proof.with_proof self.proof f
     let stats t = t.stat
 
     let define_const (self:t) ~const ~rhs : unit =
@@ -215,24 +214,24 @@ module Make(A : ARG)
 
     let simplifier self = self.simp
     let simplify_t self (t:Term.t) : _ option = Simplify.normalize self.simp t
-    let simp_t self (t:Term.t) : Term.t * dproof = Simplify.normalize_t self.simp t
+    let simp_t self (t:Term.t) : Term.t = Simplify.normalize_t self.simp t
 
     let add_simplifier (self:t) f : unit = Simplify.add_hook self.simp f
 
     let on_preprocess self f = self.preprocess <- f :: self.preprocess
     let on_model_gen self f = self.mk_model <- f :: self.mk_model
 
-    let push_decision (_self:t) (acts:actions) (lit:lit) : unit =
+    let push_decision (_self:t) (acts:theory_actions) (lit:lit) : unit =
       let (module A) = acts in
       let sign = Lit.sign lit in
       A.add_decision_lit (Lit.abs lit) sign
 
-    let[@inline] raise_conflict self (acts:actions) c proof : 'a =
+    let[@inline] raise_conflict self (acts:theory_actions) c proof : 'a =
       let (module A) = acts in
       Stat.incr self.count_conflict;
       A.raise_conflict c proof
 
-    let[@inline] propagate self (acts:actions) p ~reason : unit =
+    let[@inline] propagate self (acts:theory_actions) p ~reason : unit =
       let (module A) = acts in
       Stat.incr self.count_propagate;
       A.propagate p (Sidekick_sat.Consequence reason)
@@ -240,139 +239,176 @@ module Make(A : ARG)
     let[@inline] propagate_l self acts p cs proof : unit =
       propagate self acts p ~reason:(fun()->cs,proof)
 
-    let add_sat_clause_ self (acts:actions) ~keep lits (proof:dproof) : unit =
+    let add_sat_clause_ self (acts:theory_actions) ~keep lits (proof:dproof) : unit =
       let (module A) = acts in
       Stat.incr self.count_axiom;
       A.add_clause ~keep lits proof
 
-    let preprocess_term_ (self:t) ~add_clause (t:term) : term * dproof =
-      let mk_lit t = Lit.atom self.tst t in (* no further simplification *)
+    let add_sat_lit self ?default_pol (acts:theory_actions) (lit:Lit.t) : unit =
+      let (module A) = acts in
+      A.add_lit ?default_pol lit
+
+    (* actual preprocessing logic, acting on terms.
+       this calls all the preprocessing hooks on subterms, ensuring
+       a fixpoint. *)
+    let preprocess_term_ (self:t) (module A:PREPROCESS_ACTS) (t:term) : term =
+      let mk_lit_nopreproc t = Lit.atom self.tst t in (* no further simplification *)
 
       (* compute and cache normal form [u] of [t].
-         Also cache a list of proofs [ps] such
-         that [ps |- t=u] by CC. *)
-      let rec aux t : term * dproof list =
-        match Term.Tbl.find self.preprocess_cache t with
-        | u, ps ->
-          u, ps
-        | exception Not_found ->
-          let sub_p: _ list ref = ref [] in
 
+         Also cache a list of proofs [ps] such that [ps |- t=u] by CC.
+         It is important that we cache the proofs here, because
+         next time we preprocess [t], we will have to re-emit the same
+         proofs, even though we will not do any actual preprocessing work.
+      *)
+      let rec aux t : term =
+        match Term.Tbl.find self.preprocess_cache t with
+        | u -> u
+        | exception Not_found ->
           (* try rewrite at root *)
-          let t1 = aux_rec ~sub_p t self.preprocess in
+          let t1 = aux_rec t self.preprocess in
 
           (* map subterms *)
-          let t2 =
-            Term.map_shallow self.tst
-              (fun t_sub ->
-                 let u_sub, ps_t = aux t_sub in
-                 if not (Term.equal t_sub u_sub) then (
-                   sub_p := List.rev_append ps_t !sub_p;
-                 );
-                 u_sub)
-              t1
-          in
+          let t2 = Term.map_shallow self.tst aux t1 in
 
           let u =
             if not (Term.equal t t2) then (
-              (* fixpoint *)
-              let v, ps_t2_v = aux t2 in
-              if not (Term.equal t2 v) then (
-                sub_p := List.rev_append ps_t2_v !sub_p
-              );
-              v
+              aux t2 (* fixpoint *)
             ) else (
               t2
             )
           in
 
+          (* signal boolean subterms, so as to decide them
+             in the SAT solver *)
+          if Ty.is_bool (Term.ty u) then (
+            Log.debugf 5
+              (fun k->k "(@[solver.map-bool-subterm-to-lit@ :subterm %a@])" Term.pp u);
+
+            (* make a literal (already preprocessed) *)
+            let lit = mk_lit_nopreproc u in
+            (* ensure that SAT solver has a boolean atom for [u] *)
+            A.add_lit lit;
+
+            (* also map [sub] to this atom in the congruence closure, for propagation *)
+            let cc = cc self in
+            CC.set_as_lit cc (CC.add_term cc u) lit;
+          );
+
           if t != u then (
             Log.debugf 5
               (fun k->k "(@[smt-solver.preprocess.term@ :from %a@ :to %a@])"
                   Term.pp t Term.pp u);
           );
 
-          Term.Tbl.add self.preprocess_cache t (u,!sub_p);
-          u, !sub_p
+          Term.Tbl.add self.preprocess_cache t u;
+          u
 
       (* try each function in [hooks] successively *)
-      and aux_rec ~sub_p t hooks : term =
+      and aux_rec t hooks : term =
         match hooks with
         | [] -> t
         | h :: hooks_tl ->
-          match h self ~mk_lit ~add_clause t with
-          | None -> aux_rec ~sub_p t hooks_tl
-          | Some (u, ps_t_u) ->
-            sub_p := ps_t_u :: !sub_p;
-            let v, ps_u_v = aux u in
-            if t != v then (
-              sub_p := List.rev_append ps_u_v !sub_p;
-            );
-            v
+          match h self (module A) t with
+          | None -> aux_rec t hooks_tl
+          | Some u -> aux u
       in
 
-      let t1, p_t_t1 = simp_t self t in
+      P.begin_subproof self.proof;
 
-      let u, ps_t1_u = aux t1 in
+      (* simplify the term *)
+      let t1 = simp_t self t in
 
-      let emit_proof_t_eq_u =
-        if t != u then (
-          let hyps =
-            if t == t1 then ps_t1_u
-            else p_t_t1 :: ps_t1_u in
-          let emit_proof p =
-            P.begin_subproof p;
-            List.iter (fun dp -> dp p) hyps;
-            P.lemma_preprocess p t u;
-            P.end_subproof p;
-          in
-          emit_proof
-        ) else (fun _->())
-      in
-
-      u, emit_proof_t_eq_u
-
-    (* return preprocessed lit + proof they are equal *)
-    let preprocess_lit_ (self:t) ~add_clause (lit:lit) : lit * dproof =
-      let t, p = Lit.term lit |> preprocess_term_ self ~add_clause in
-      let lit' = Lit.atom self.tst ~sign:(Lit.sign lit) t in
-
-      if not (Lit.equal lit lit') then (
-        Log.debugf 10
-          (fun k->k "(@[smt-solver.preprocess.lit@ :lit %a@ :into %a@])"
-              Lit.pp lit Lit.pp lit');
+      (* preprocess *)
+      let u = aux t1 in
+      (* emit [|- t=u] *)
+      if not (Term.equal t u) then (
+        P.with_proof self.proof (P.lemma_preprocess t u);
       );
 
-      lit', p
+      P.end_subproof self.proof;
+      u
+
+    (* return preprocessed lit + proof they are equal *)
+    let preprocess_lit_ (self:t) (module A0:PREPROCESS_ACTS) (lit:lit) : lit =
+
+      (* create literal and preprocess it with [pacts], which uses [A0]
+         for the base operations, and preprocesses new literals and clauses
+         recursively. *)
+      let rec mk_lit ?sign t =
+        Log.debug 0 "A.MK_LIT";
+        let u = preprocess_term_ self (Lazy.force pacts) t in
+        if not (Term.equal t u) then (
+          Log.debugf 10
+            (fun k->k "(@[smt-solver.preprocess.t@ :t %a@ :into %a@])"
+                Term.pp t Term.pp u);
+        );
+        Lit.atom self.tst ?sign u
+
+      and preprocess_lit (lit:lit) : lit =
+        let t = Lit.term lit in
+        let sign = Lit.sign lit in
+        mk_lit ~sign t
+
+      (* wrap [A0] so that all operations go throught preprocessing *)
+      and pacts = lazy (
+        (module struct
+          let add_lit ?default_pol lit =
+            let lit = preprocess_lit lit in
+            A0.add_lit lit
+          let add_clause c pr =
+            Stat.incr self.count_preprocess_clause;
+            let c = CCList.map preprocess_lit c in
+            A0.add_clause c pr
+          let mk_lit = mk_lit
+        end : PREPROCESS_ACTS)
+      ) in
+
+      preprocess_lit lit
 
     (* add a clause using [acts] *)
     let add_clause_ self acts lits (proof:dproof) : unit =
-      Stat.incr self.count_preprocess_clause;
       add_sat_clause_ self acts ~keep:true lits proof
 
-    (* FIXME: should we store the proof somewhere? *)
-    let mk_lit self acts ?sign t : Lit.t =
-      let add_clause = add_clause_ self acts in
-      let lit, _p =
-        preprocess_lit_ self ~add_clause @@ Lit.atom self.tst ?sign t
-      in
-      lit
-
-    let[@inline] preprocess_term self ~add_clause (t:term) : term * dproof =
-      preprocess_term_ self ~add_clause t
-
-    let[@inline] add_clause_temp self acts lits (proof:dproof) : unit =
-      add_sat_clause_ self acts ~keep:false lits proof
-
-    let[@inline] add_clause_permanent self acts lits (proof:dproof) : unit =
-      add_sat_clause_ self acts ~keep:true lits proof
-
-    let[@inline] add_lit _self (acts:actions) lit : unit =
+    let[@inline] add_lit _self (acts:theory_actions) ?default_pol lit : unit =
       let (module A) = acts in
-      A.mk_lit lit
+      A.add_lit ?default_pol lit
+
+    let preprocess_acts_of_acts (self:t) (acts:theory_actions) : preprocess_actions =
+      (module struct
+        let mk_lit ?sign t = Lit.atom self.tst ?sign t
+        let add_clause = add_clause_ self acts
+        let add_lit = add_lit self acts
+      end)
+
+    let preprocess_clause_ (self:t) (acts:theory_actions) (c:lit list) : lit list =
+      let pacts = preprocess_acts_of_acts self acts in
+      let c = CCList.map (preprocess_lit_ self pacts) c in
+      c
+
+    (* make literal and preprocess it *)
+    let[@inline] mk_plit (self:t) (pacts:preprocess_actions) ?sign (t:term) : lit =
+      let lit = Lit.atom self.tst ?sign t in
+      preprocess_lit_ self pacts lit
+
+    let[@inline] preprocess_term self (pacts:preprocess_actions) (t:term) : term =
+      preprocess_term_ self pacts t
+
+    let[@inline] add_clause_temp self acts c (proof:dproof) : unit =
+      let c = preprocess_clause_ self acts c in
+      add_sat_clause_ self acts ~keep:false c proof
+
+    let[@inline] add_clause_permanent self acts c (proof:dproof) : unit =
+      let c = preprocess_clause_ self acts c in
+      add_sat_clause_ self acts ~keep:true c proof
+
+    let[@inline] mk_lit (self:t) (acts:theory_actions) ?sign t : lit =
+      let pacts = preprocess_acts_of_acts self acts in
+      mk_plit self pacts ?sign t
 
     let add_lit_t self acts ?sign t =
-      let lit = mk_lit self acts ?sign t in
+      let pacts = preprocess_acts_of_acts self acts in
+      let lit = mk_plit self pacts ?sign t in
       add_lit self acts lit
 
     let on_final_check self f = self.on_final_check <- f :: self.on_final_check
@@ -420,7 +456,7 @@ module Make(A : ARG)
     exception E_loop_exit
 
     (* handle a literal assumed by the SAT solver *)
-    let assert_lits_ ~final (self:t) (acts:actions) (lits:Lit.t Iter.t) : unit =
+    let assert_lits_ ~final (self:t) (acts:theory_actions) (lits:Lit.t Iter.t) : unit =
       Log.debugf 2
         (fun k->k "(@[<hv1>@{<green>smt-solver.assume_lits@}%s[lvl=%d]@ %a@])"
             (if final then "[final]" else "") self.level (Util.pp_iter ~sep:"; " Lit.pp) lits);
@@ -448,7 +484,7 @@ module Make(A : ARG)
       );
       ()
 
-    let[@inline] iter_atoms_ (acts:actions) : _ Iter.t =
+    let[@inline] iter_atoms_ (acts:theory_actions) : _ Iter.t =
       fun f ->
         let (module A) = acts in
         A.iter_assumptions f
@@ -481,7 +517,7 @@ module Make(A : ARG)
         proof;
         th_states=Ths_nil;
         stat;
-        simp=Simplify.create tst ty_st;
+        simp=Simplify.create tst ty_st ~proof;
         on_progress=(fun () -> ());
         preprocess=[];
         mk_model=[];
@@ -507,6 +543,7 @@ module Make(A : ARG)
     si: Solver_internal.t;
     solver: Sat_solver.t;
     stat: Stat.t;
+    proof: P.t;
     count_clause: int Stat.counter;
     count_solve: int Stat.counter;
     (* config: Config.t *)
@@ -554,7 +591,7 @@ module Make(A : ARG)
     Log.debug 5 "smt-solver.create";
     let si = Solver_internal.create ~stat ~proof tst ty_st () in
     let self = {
-      si;
+      si; proof;
       solver=Sat_solver.create ~proof ?size si;
       stat;
       count_clause=Stat.mk_int stat "solver.add-clause";
@@ -567,7 +604,7 @@ module Make(A : ARG)
       let t_true = Term.bool tst true in
       Sat_solver.add_clause self.solver
         [Lit.atom tst t_true]
-        (fun p -> P.lemma_true p t_true)
+        (P.lemma_true t_true)
     end;
     self
 
@@ -577,65 +614,25 @@ module Make(A : ARG)
   let[@inline] tst self = Solver_internal.tst self.si
   let[@inline] ty_st self = Solver_internal.ty_st self.si
 
-  (* map boolean subterms to literals *)
-  let add_bool_subterms_ (self:t) (t:Term.t) : unit =
-    Term.iter_dag t
-    |> Iter.filter (fun t -> Ty.is_bool @@ Term.ty t)
-    |> Iter.filter
-      (fun t -> match A.cc_view t with
-         | Sidekick_core.CC_view.Not _ -> false (* will process the subterm just later *)
-         | _ -> true)
-    |> Iter.filter (fun t -> A.is_valid_literal t)
-    |> Iter.iter
-      (fun sub ->
-         Log.debugf 5 (fun k->k "(@[solver.map-bool-subterm-to-lit@ :subterm %a@])" Term.pp sub);
-         (* ensure that SAT solver has a boolean atom for [sub] *)
-         let lit = Lit.atom self.si.tst sub in
-         Sat_solver.add_lit self.solver lit;
-         (* also map [sub] to this atom in the congruence closure, for propagation *)
-         let cc = cc self in
-         CC.set_as_lit cc (CC.add_term cc sub) lit;
-         ())
+  let preprocess_acts_of_solver_
+      (self:t) : (module Solver_internal.PREPROCESS_ACTS) =
+    (module struct
+      let mk_lit ?sign t = Lit.atom ?sign self.si.tst t
+      let add_lit ?default_pol lit =
+        Sat_solver.add_lit self.solver ?default_pol lit
+      let add_clause c pr =
+        Sat_solver.add_clause self.solver c pr
+    end)
 
-  (* preprocess literals, making them ready for being added to the solver *)
-  let rec preprocess_lit_ self lit : Lit.t * dproof =
-    let lit, proof =
-      Solver_internal.preprocess_lit_
-      ~add_clause:(fun lits proof ->
-          (* recursively add these sub-literals, so they're also properly processed *)
-          Stat.incr self.si.count_preprocess_clause;
-          let pr_l = ref [] in
-          let lits =
-            CCList.map
-              (fun lit ->
-                 let a, pr = preprocess_lit_ self lit in
-                 (* FIXME                 if not (P.is_trivial_refl pr) then ( *)
-                   pr_l := pr :: !pr_l;
-                   (*                  ); *)
-                 a)
-              lits
-          in
-          let emit_proof p = List.iter (fun dp -> dp p) !pr_l; in
-          Sat_solver.add_clause self.solver lits emit_proof)
-      self.si lit
-    in
-    Sat_solver.add_lit self.solver lit;
-    lit, proof
+  (* preprocess literal *)
+  let preprocess_lit_ (self:t) (lit:lit) : lit =
+    let pacts = preprocess_acts_of_solver_ self in
+    Solver_internal.preprocess_lit_ self.si pacts lit
 
-  (* FIXME: should we just add the proof instead? *)
-  let[@inline] preprocess_lit' self lit : Lit.t =
-    fst (preprocess_lit_ self lit)
-
-  (* FIXME: should we just assert the proof instead? or do we wait because
-     we're most likely in a subproof? *)
-  let rec mk_lit_t (self:t) ?sign (t:term) : lit * dproof =
-    let lit = Lit.atom ?sign self.si.tst t in
-    let lit, proof = preprocess_lit_ self lit in
-    Sat_solver.add_lit self.solver lit;
-    add_bool_subterms_ self (Lit.term lit);
-    lit, proof
-
-  let[@inline] mk_lit_t' self ?sign lit = mk_lit_t self ?sign lit |> fst
+  (* make a literal from a term, ensuring it is properly preprocessed *)
+  let mk_lit_t (self:t) ?sign (t:term) : lit =
+    let pacts = preprocess_acts_of_solver_ self in
+    Solver_internal.mk_plit self.si pacts ?sign t
 
   (** {2 Result} *)
 
@@ -699,12 +696,11 @@ module Make(A : ARG)
 
   let assert_terms self c =
     let c = CCList.map (fun t -> Lit.atom (tst self) t) c in
-    let emit_proof p =
-      P.emit_input_clause p (Iter.of_list c)
-    in
-    (* FIXME: just emit proofs on the fly? *)
-    let c = CCList.map (preprocess_lit' self) c in
-    add_clause_l self c emit_proof
+    let c = CCList.map (preprocess_lit_ self) c in
+    (* TODO: if c != c0 then P.emit_redundant_clause c
+       because we jsut preprocessed it away? *)
+    let dp = P.emit_input_clause (Iter.of_list c) in
+    add_clause_l self c dp
 
   let assert_term self t = assert_terms self [t]
 
diff --git a/src/smtlib/Process.ml b/src/smtlib/Process.ml
index 2c3a4cfe..fbef278e 100644
--- a/src/smtlib/Process.ml
+++ b/src/smtlib/Process.ml
@@ -233,7 +233,7 @@ let process_stmt
       (* FIXME: how to map [l] to [assumptions] in proof? *)
       let assumptions =
         List.map
-          (fun (sign,t) -> Solver.mk_lit_t' solver ~sign t)
+          (fun (sign,t) -> Solver.mk_lit_t solver ~sign t)
           l
       in
       solve
@@ -253,33 +253,24 @@ let process_stmt
       if pp_cnf then (
         Format.printf "(@[<hv1>assert@ %a@])@." Term.pp t
       );
-      let lit = Solver.mk_lit_t' solver t in
+      let lit = Solver.mk_lit_t solver t in
       Solver.add_clause solver (IArray.singleton lit)
-        (fun p -> Solver.P.emit_input_clause p (Iter.singleton lit));
+        (Solver.P.emit_input_clause (Iter.singleton lit));
       E.return()
 
     | Statement.Stmt_assert_clause c_ts ->
       if pp_cnf then (
         Format.printf "(@[<hv1>assert-clause@ %a@])@." (Util.pp_list Term.pp) c_ts
       );
-      let pr_l = ref [] in
-      let c =
-        List.map
-          (fun t ->
-             let lit, pr = Solver.mk_lit_t solver t in
-             pr_l := pr :: !pr_l;
-             lit)
-          c_ts in
+
+      let c = CCList.map (fun t -> Solver.mk_lit_t solver t) c_ts in
 
       (* proof of assert-input + preprocessing *)
       let emit_proof p =
         let module P = Solver.P in
-        P.begin_subproof p;
         let tst = Solver.tst solver in
-        P.emit_input_clause p (Iter.of_list c_ts |> Iter.map (Lit.atom tst));
-        List.iter (fun dp -> dp p) !pr_l;
-        P.emit_redundant_clause p (Iter.of_list c);
-        P.end_subproof p;
+        P.emit_input_clause (Iter.of_list c_ts |> Iter.map (Lit.atom tst)) p;
+        P.emit_redundant_clause (Iter.of_list c) p;
       in
 
       Solver.add_clause solver (IArray.of_list c) emit_proof;
diff --git a/src/th-bool-static/Sidekick_th_bool_static.ml b/src/th-bool-static/Sidekick_th_bool_static.ml
index 9989a000..5edf0ae8 100644
--- a/src/th-bool-static/Sidekick_th_bool_static.ml
+++ b/src/th-bool-static/Sidekick_th_bool_static.ml
@@ -36,20 +36,20 @@ module type ARG = sig
       Only enable if some theories are susceptible to
       create boolean formulas during the proof search. *)
 
-  val lemma_bool_tauto : S.P.t -> S.Lit.t Iter.t -> unit
+  val lemma_bool_tauto : S.Lit.t Iter.t -> S.P.t -> unit
   (** Boolean tautology lemma (clause) *)
 
-  val lemma_bool_c : S.P.t -> string -> term list -> unit
+  val lemma_bool_c : string -> term list -> S.P.t -> unit
   (** Basic boolean logic lemma for a clause [|- c].
       [proof_bool_c b name cs] is the rule designated by [name]. *)
 
-  val lemma_bool_equiv : S.P.t -> term -> term -> unit
+  val lemma_bool_equiv : term -> term -> S.P.t -> unit
   (** Boolean tautology lemma (equivalence) *)
 
-  val lemma_ite_true : S.P.t -> a:term -> ite:term -> unit
+  val lemma_ite_true : a:term -> ite:term -> S.P.t -> unit
   (** lemma [a => ite a b c = b] *)
 
-  val lemma_ite_false : S.P.t -> a:term -> ite:term -> unit
+  val lemma_ite_false : a:term -> ite:term -> S.P.t -> unit
   (** lemma [¬a => ite a b c = c] *)
 
   (** Fresh symbol generator.
@@ -102,7 +102,7 @@ module Make(A : ARG) : S with module A = A = struct
   type state = {
     tst: T.store;
     ty_st: Ty.store;
-    cnf: (Lit.t * SI.dproof) T.Tbl.t; (* tseitin CNF *)
+    cnf: Lit.t T.Tbl.t; (* tseitin CNF *)
     gensym: A.Gensym.t;
   }
 
@@ -118,14 +118,16 @@ module Make(A : ARG) : S with module A = A = struct
   let is_true t = match T.as_bool t with Some true -> true | _ -> false
   let is_false t = match T.as_bool t with Some false -> true | _ -> false
 
-  let simplify (self:state) (simp:SI.Simplify.t) (t:T.t) : (T.t * SI.dproof) option =
+  let simplify (self:state) (simp:SI.Simplify.t) (t:T.t) : T.t option =
     let tst = self.tst in
     let ret u =
-      let emit_proof p =
-        A.lemma_bool_equiv p t u;
-        A.S.P.lemma_preprocess p t u;
-      in
-      Some (u, emit_proof)
+      if not (T.equal t u) then (
+        SI.Simplify.with_proof simp (fun p ->
+          A.lemma_bool_equiv t u p;
+          A.S.P.lemma_preprocess t u p;
+        );
+      );
+      Some u
     in
     match A.view_as_bool t with
     | B_bool _ -> None
@@ -148,14 +150,14 @@ module Make(A : ARG) : S with module A = A = struct
     | B_ite (a,b,c) ->
       (* directly simplify [a] so that maybe we never will simplify one
          of the branches *)
-      let a, pr_a = SI.Simplify.normalize_t simp a in
+      let a = SI.Simplify.normalize_t simp a in
       begin match A.view_as_bool a with
         | B_bool true ->
-          let emit_proof p = pr_a p; A.lemma_ite_true p ~a ~ite:t in
-          Some (b, emit_proof)
+          SI.Simplify.with_proof simp (A.lemma_ite_true ~a ~ite:t);
+          Some b
         | B_bool false ->
-          let emit_proof p = pr_a p; A.lemma_ite_false p ~a ~ite:t in
-          Some (c, emit_proof)
+          SI.Simplify.with_proof simp (A.lemma_ite_false ~a ~ite:t);
+          Some c
         | _ ->
           None
       end
@@ -186,136 +188,124 @@ module Make(A : ARG) : S with module A = A = struct
     proxy, mk_lit proxy
 
   (* preprocess "ite" away *)
-  let preproc_ite self si ~mk_lit ~add_clause (t:T.t) : (T.t * SI.dproof) option =
+  let preproc_ite self si (module PA:SI.PREPROCESS_ACTS) (t:T.t) : T.t option =
     match A.view_as_bool t with
     | B_ite (a,b,c) ->
-      let a, pr_a = SI.simp_t si a in
+      let a = SI.simp_t si a in
       begin match A.view_as_bool a with
         | B_bool true ->
           (* [a=true |- ite a b c=b], [|- a=true] ==> [|- t=b] *)
-          let emit_proof p = pr_a p; A.lemma_ite_true p ~a ~ite:t in
-          Some (b, emit_proof)
+          SI.with_proof si (A.lemma_ite_true ~a ~ite:t);
+          Some b
         | B_bool false ->
           (* [a=false |- ite a b c=c], [|- a=false] ==> [|- t=c] *)
-          let emit_proof p = pr_a p; A.lemma_ite_false p ~a ~ite:t in
-          Some (c, emit_proof)
+          SI.with_proof si (A.lemma_ite_false ~a ~ite:t);
+          Some c
         | _ ->
           let t_ite = fresh_term self ~for_t:t ~pre:"ite" (T.ty b) in
           SI.define_const si ~const:t_ite ~rhs:t;
-          let lit_a = mk_lit a in
-          add_clause [Lit.neg lit_a; mk_lit (eq self.tst t_ite b)]
-            (fun p -> A.lemma_ite_true p ~a ~ite:t);
-          add_clause [lit_a; mk_lit (eq self.tst t_ite c)]
+          SI.with_proof si (SI.P.define_term t_ite t);
+          let lit_a = PA.mk_lit a in
+          PA.add_clause [Lit.neg lit_a; PA.mk_lit (eq self.tst t_ite b)]
+            (fun p -> A.lemma_ite_true ~a ~ite:t p);
+          PA.add_clause [lit_a; PA.mk_lit (eq self.tst t_ite c)]
             (fun p -> A.lemma_ite_false p ~a ~ite:t);
-          Some (t_ite, fun p -> SI.P.define_term p t_ite t)
+          Some t_ite
       end
     | _ -> None
 
   (* TODO: polarity? *)
-  let cnf (self:state) (si:SI.t) ~mk_lit ~add_clause (t:T.t) : (T.t * SI.dproof) option =
-    let rec get_lit_and_proof_ (t:T.t) : Lit.t * _ =
+  let cnf (self:state) (si:SI.t) (module PA:SI.PREPROCESS_ACTS) (t:T.t) : T.t option =
+    let rec get_lit (t:T.t) : Lit.t =
       let t_abs, t_sign = T.abs self.tst t in
-      let lit_abs, pr =
+      let lit_abs =
         match T.Tbl.find self.cnf t_abs with
-        | lit_pr -> lit_pr (* cached *)
+        | lit -> lit (* cached *)
         | exception Not_found ->
           (* compute and cache *)
-          let lit, pr = get_lit_uncached si t_abs in
+          let lit = get_lit_uncached si t_abs in
           if not (T.equal (Lit.term lit) t_abs) then (
-            T.Tbl.add self.cnf t_abs (lit, pr);
+            T.Tbl.add self.cnf t_abs lit;
             Log.debugf 20
               (fun k->k "(@[sidekick.bool.add-lit@ :lit %a@ :for-t %a@])"
                   Lit.pp lit T.pp t_abs);
           );
-          lit, pr
+          lit
       in
 
       let lit = if t_sign then lit_abs else Lit.neg lit_abs in
-      lit, pr
+      lit
 
-    and equiv_ si ~get_lit ~is_xor ~for_t t_a t_b : Lit.t * SI.dproof =
+    and equiv_ si ~get_lit ~is_xor ~for_t t_a t_b : Lit.t =
       let a = get_lit t_a in
       let b = get_lit t_b in
       let a = if is_xor then Lit.neg a else a in (* [a xor b] is [(¬a) = b] *)
-      let t_proxy, proxy = fresh_lit ~for_t ~mk_lit ~pre:"equiv_" self in
+      let t_proxy, proxy = fresh_lit ~for_t ~mk_lit:PA.mk_lit ~pre:"equiv_" self in
 
       SI.define_const si ~const:t_proxy ~rhs:for_t;
+      SI.with_proof si (SI.P.define_term t_proxy for_t);
+
       let add_clause c pr =
-        add_clause c pr
+        PA.add_clause c pr
       in
 
       (* proxy => a<=> b,
          ¬proxy => a xor b *)
       add_clause [Lit.neg proxy; Lit.neg a; b]
-        (fun p ->
-           if is_xor then A.lemma_bool_c p "xor-e+" [t_proxy]
-           else A.lemma_bool_c p "eq-e" [t_proxy; t_a]);
+        (if is_xor then A.lemma_bool_c "xor-e+" [t_proxy]
+         else A.lemma_bool_c "eq-e" [t_proxy; t_a]);
       add_clause [Lit.neg proxy; Lit.neg b; a]
-        (fun p ->
-           if is_xor then A.lemma_bool_c p "xor-e-" [t_proxy]
-           else A.lemma_bool_c p "eq-e" [t_proxy; t_b]);
+        (if is_xor then A.lemma_bool_c "xor-e-" [t_proxy]
+         else A.lemma_bool_c "eq-e" [t_proxy; t_b]);
       add_clause [proxy; a; b]
-        (fun p -> if is_xor then A.lemma_bool_c p "xor-i" [t_proxy; t_a]
-          else A.lemma_bool_c p "eq-i+" [t_proxy]);
+        (if is_xor then A.lemma_bool_c "xor-i" [t_proxy; t_a]
+         else A.lemma_bool_c "eq-i+" [t_proxy]);
       add_clause [proxy; Lit.neg a; Lit.neg b]
-        (fun p ->
-           if is_xor then A.lemma_bool_c p "xor-i" [t_proxy; t_b]
-           else A.lemma_bool_c p "eq-i-" [t_proxy]);
-      proxy, (fun p->SI.P.define_term p t_proxy for_t)
+        (if is_xor then A.lemma_bool_c "xor-i" [t_proxy; t_b]
+         else A.lemma_bool_c "eq-i-" [t_proxy]);
+      proxy
 
     (* make a literal for [t], with a proof of [|- abs(t) = abs(lit)] *)
-    and get_lit_uncached si t : Lit.t * SI.dproof =
-      let sub_p = ref [] in
-
-      let get_lit t =
-        let lit, pr = get_lit_and_proof_ t in
-        if Lit.term lit != t then (
-          sub_p := pr :: !sub_p;
-        );
-        lit
-      in
-
+    and get_lit_uncached si t : Lit.t =
       match A.view_as_bool t with
-      | B_bool b -> mk_lit (T.bool self.tst b), (fun _->())
-      | B_opaque_bool t -> mk_lit t, (fun _->())
+      | B_bool b -> PA.mk_lit (T.bool self.tst b)
+      | B_opaque_bool t -> PA.mk_lit t
       | B_not u ->
-        let lit, pr = get_lit_and_proof_ u in
-        Lit.neg lit, pr
+        let lit = get_lit u in
+        Lit.neg lit
 
       | B_and l ->
         let t_subs = Iter.to_list l in
         let subs = List.map get_lit t_subs in
-        let t_proxy, proxy = fresh_lit ~for_t:t ~mk_lit ~pre:"and_" self in
+        let t_proxy, proxy = fresh_lit ~for_t:t ~mk_lit:PA.mk_lit ~pre:"and_" self in
         SI.define_const si ~const:t_proxy ~rhs:t;
+        SI.with_proof si (SI.P.define_term t_proxy t);
         (* add clauses *)
         List.iter2
           (fun t_u u ->
-             add_clause
+             PA.add_clause
                [Lit.neg proxy; u]
-               (fun p -> A.lemma_bool_c p "and-e" [t_proxy; t_u]))
+               (A.lemma_bool_c "and-e" [t_proxy; t_u]))
           t_subs subs;
-        add_clause (proxy :: List.map Lit.neg subs)
-          (fun p -> A.lemma_bool_c p "and-i" [t_proxy]);
-        let emit_proof p =
-          SI.P.define_term p t_proxy t;
-        in
-        proxy, emit_proof
+        PA.add_clause (proxy :: List.map Lit.neg subs)
+          (A.lemma_bool_c "and-i" [t_proxy]);
+        proxy
 
       | B_or l ->
         let t_subs = Iter.to_list l in
         let subs = List.map get_lit t_subs in
-        let t_proxy, proxy = fresh_lit ~for_t:t ~mk_lit ~pre:"or_" self in
+        let t_proxy, proxy = fresh_lit ~for_t:t ~mk_lit:PA.mk_lit ~pre:"or_" self in
         SI.define_const si ~const:t_proxy ~rhs:t;
+        SI.with_proof si (SI.P.define_term t_proxy t);
         (* add clauses *)
         List.iter2
           (fun t_u u ->
-             add_clause [Lit.neg u; proxy]
-               (fun p -> A.lemma_bool_c p "or-i" [t_proxy; t_u]))
+             PA.add_clause [Lit.neg u; proxy]
+               (A.lemma_bool_c "or-i" [t_proxy; t_u]))
           t_subs subs;
-        add_clause (Lit.neg proxy :: subs)
-          (fun p -> A.lemma_bool_c p "or-e" [t_proxy]);
-        let emit_proof p = SI.P.define_term p t_proxy t in
-        proxy, emit_proof
+        PA.add_clause (Lit.neg proxy :: subs)
+          (A.lemma_bool_c "or-e" [t_proxy]);
+        proxy
 
       | B_imply (t_args, t_u) ->
         (* transform into [¬args \/ u] on the fly *)
@@ -325,35 +315,35 @@ module Make(A : ARG) : S with module A = A = struct
         let subs = u :: args in
 
         (* now the or-encoding *)
-        let t_proxy, proxy = fresh_lit ~for_t:t ~mk_lit ~pre:"implies_" self in
+        let t_proxy, proxy = fresh_lit ~for_t:t ~mk_lit:PA.mk_lit ~pre:"implies_" self in
         SI.define_const si ~const:t_proxy ~rhs:t;
+        SI.with_proof si (SI.P.define_term t_proxy t);
 
         (* add clauses *)
         List.iter2
           (fun t_u u ->
-             add_clause [Lit.neg u; proxy]
-               (fun p -> A.lemma_bool_c p "imp-i" [t_proxy; t_u]))
+             PA.add_clause [Lit.neg u; proxy]
+               (A.lemma_bool_c "imp-i" [t_proxy; t_u]))
           (t_u::t_args) subs;
-        add_clause (Lit.neg proxy :: subs)
-          (fun p -> A.lemma_bool_c p "imp-e" [t_proxy]);
-        let emit_proof p = SI.P.define_term p t_proxy t in
-        proxy, emit_proof
+        PA.add_clause (Lit.neg proxy :: subs)
+          (A.lemma_bool_c "imp-e" [t_proxy]);
+        proxy
 
-      | B_ite _ | B_eq _ | B_neq _ -> mk_lit t, (fun _ ->())
+      | B_ite _ | B_eq _ | B_neq _ -> PA.mk_lit t
       | B_equiv (a,b) -> equiv_ si ~get_lit ~for_t:t ~is_xor:false a b
       | B_xor  (a,b) -> equiv_ si ~get_lit ~for_t:t ~is_xor:true a b
-      | B_atom u -> mk_lit u, (fun _->())
+      | B_atom u -> PA.mk_lit u
     in
 
-    let lit, pr = get_lit_and_proof_ t in
+    let lit = get_lit t in
     let u = Lit.term lit in
     (* put sign back as a "not" *)
     let u = if Lit.sign lit then u else A.mk_bool self.tst (B_not u) in
-    if T.equal u t then None else Some (u, pr)
+    if T.equal u t then None else Some u
 
   (* check if new terms were added to the congruence closure, that can be turned
      into clauses *)
-  let check_new_terms (self:state) si (acts:SI.actions) (_trail:_ Iter.t) : unit =
+  let check_new_terms (self:state) si (acts:SI.theory_actions) (_trail:_ Iter.t) : unit =
     let cc_ = SI.cc si in
     let all_terms =
       let open SI in
@@ -362,15 +352,14 @@ module Make(A : ARG) : S with module A = A = struct
       |> Iter.map CC.N.term
     in
     let cnf_of t =
-      cnf self si t
-        ~mk_lit:(SI.mk_lit si acts) ~add_clause:(SI.add_clause_permanent si acts)
+      let pacts = SI.preprocess_acts_of_acts si acts in
+      cnf self si pacts t
     in
     begin
       all_terms
         (fun t -> match cnf_of t with
            | None -> ()
-           | Some (u, _pr_t_u) ->
-             (* FIXME: what to do with pr_t_u? emit it? *)
+           | Some u ->
              Log.debugf 5
                (fun k->k "(@[th-bool-static.final-check.cnf@ %a@ :yields %a@])"
                    T.pp t T.pp u);
diff --git a/src/th-data/Sidekick_th_data.ml b/src/th-data/Sidekick_th_data.ml
index 9a1f4521..51a3b42d 100644
--- a/src/th-data/Sidekick_th_data.ml
+++ b/src/th-data/Sidekick_th_data.ml
@@ -74,9 +74,9 @@ module type ARG = sig
   val ty_is_finite : S.T.Ty.t -> bool
   val ty_set_is_finite : S.T.Ty.t -> bool -> unit
 
-  val lemma_isa_split : S.proof -> S.Lit.t Iter.t -> unit
-  val lemma_isa_disj : S.proof -> S.Lit.t Iter.t -> unit
-  val lemma_cstor_inj : S.proof -> S.Lit.t Iter.t -> unit
+  val lemma_isa_split : S.Lit.t Iter.t -> S.proof -> unit
+  val lemma_isa_disj : S.Lit.t Iter.t -> S.proof -> unit
+  val lemma_cstor_inj : S.Lit.t Iter.t -> S.proof -> unit
 end
 
 (** Helper to compute the cardinality of types *)
@@ -496,7 +496,7 @@ module Make(A : ARG) : S with module A = A = struct
       end;
       g
 
-    let check (self:t) (solver:SI.t) (acts:SI.actions) : unit =
+    let check (self:t) (solver:SI.t) (acts:SI.theory_actions) : unit =
       let cc = SI.cc solver in
       (* create graph *)
       let g = mk_graph self cc in
@@ -574,19 +574,19 @@ module Make(A : ARG) : S with module A = A = struct
         |> Iter.to_rev_list
       in
       SI.add_clause_permanent solver acts c
-        (fun p -> A.lemma_isa_split p (Iter.of_list c));
+        (A.lemma_isa_split (Iter.of_list c));
       Iter.diagonal_l c
         (fun (c1,c2) ->
-           let emit_proof p =
-             A.lemma_isa_disj p (Iter.of_list [SI.Lit.neg c1; SI.Lit.neg c2]) in
+           let pr =
+             A.lemma_isa_disj (Iter.of_list [SI.Lit.neg c1; SI.Lit.neg c2]) in
            SI.add_clause_permanent solver acts
-             [SI.Lit.neg c1; SI.Lit.neg c2] emit_proof);
+             [SI.Lit.neg c1; SI.Lit.neg c2] pr);
     )
 
   (* on final check, check acyclicity,
      then make sure we have done case split on all terms that
      need it. *)
-  let on_final_check (self:t) (solver:SI.t) (acts:SI.actions) trail =
+  let on_final_check (self:t) (solver:SI.t) (acts:SI.theory_actions) trail =
     Profile.with_ "data.final-check" @@ fun () ->
     check_is_a self solver acts trail;
 
diff --git a/src/th-data/Sidekick_th_data.mli b/src/th-data/Sidekick_th_data.mli
index 2a4b62f3..6366159d 100644
--- a/src/th-data/Sidekick_th_data.mli
+++ b/src/th-data/Sidekick_th_data.mli
@@ -74,9 +74,9 @@ module type ARG = sig
 
   (* TODO: should we store this ourself? would be simpler… *)
 
-  val lemma_isa_split : S.proof -> S.Lit.t Iter.t -> unit
-  val lemma_isa_disj : S.proof -> S.Lit.t Iter.t -> unit
-  val lemma_cstor_inj : S.proof -> S.Lit.t Iter.t -> unit
+  val lemma_isa_split : S.Lit.t Iter.t -> S.proof -> unit
+  val lemma_isa_disj : S.Lit.t Iter.t -> S.proof -> unit
+  val lemma_cstor_inj : S.Lit.t Iter.t -> S.proof -> unit
 end
 
 module type S = sig