diff --git a/src/main/main.ml b/src/main/main.ml
index 80c6df26..d64dbf9d 100644
--- a/src/main/main.ml
+++ b/src/main/main.ml
@@ -114,9 +114,10 @@ let main () =
   let solver =
     let theories = match syn with
       | Dimacs ->
-        [Sidekick_th_bool.th]
+        (* TODO: eager CNF conversion *)
+        [Sidekick_th_bool.th_dynamic_tseitin]
       | Smtlib ->
-        [Sidekick_th_bool.th] (* TODO: more theories *)
+        [Sidekick_th_bool.th_dynamic_tseitin] (* TODO: more theories *)
     in
     Sidekick_smt.Solver.create ~store_proof:!check ~theories ()
   in
diff --git a/src/smtlib/Process.ml b/src/smtlib/Process.ml
index dbf59206..c1e7f592 100644
--- a/src/smtlib/Process.ml
+++ b/src/smtlib/Process.ml
@@ -7,7 +7,7 @@ type 'a or_error = ('a, string) CCResult.t
 
 module E = CCResult
 module A = Ast
-module Form = Sidekick_th_bool
+module Form = Sidekick_th_bool.Bool_term
 module Fmt = CCFormat
 module Dot = Msat_backend.Dot.Make(Solver.Sat_solver)(Msat_backend.Dot.Default(Solver.Sat_solver))
 
@@ -125,7 +125,7 @@ module Conv = struct
           begin match List.rev l with
             | [] -> Term.true_ tst
             | ret :: hyps ->
-              Form.imply tst hyps ret
+              Form.imply_l tst hyps ret
           end
         | A.Op (A.Eq, l) ->
           let l = List.map (aux subst) l in
@@ -137,7 +137,7 @@ module Conv = struct
           in
           Form.and_l tst (curry_eq l)
         | A.Op (A.Distinct, l) ->
-          Form.distinct tst @@ List.map (aux subst) l
+          Form.distinct_l tst @@ List.map (aux subst) l
         | A.Not f -> Form.not_ tst (aux subst f)
         | A.Bool true -> Term.true_ tst
         | A.Bool false -> Term.false_ tst
diff --git a/src/th-bool/Bool_intf.ml b/src/th-bool/Bool_intf.ml
new file mode 100644
index 00000000..7ca04cec
--- /dev/null
+++ b/src/th-bool/Bool_intf.ml
@@ -0,0 +1,26 @@
+
+(** {1 Signatures for booleans} *)
+
+type 'a view =
+  | B_not of 'a
+  | B_eq of 'a * 'a
+  | B_and of 'a IArray.t
+  | B_or of 'a IArray.t
+  | B_imply of 'a IArray.t * 'a
+  | B_distinct of 'a IArray.t
+  | B_atom of 'a
+
+(** {2 Interface for a representation of boolean terms} *)
+module type BOOL_TERM = sig
+  type t
+  type state
+
+  val equal : t -> t -> bool
+  val hash : t -> int
+
+  val view_as_bool : t -> t view
+  (** View a term as a boolean formula *)
+
+  val make : state -> t view -> t
+  (** Build a boolean term from a formula view *)
+end
diff --git a/src/th-bool/Bool_term.ml b/src/th-bool/Bool_term.ml
new file mode 100644
index 00000000..be17cfd0
--- /dev/null
+++ b/src/th-bool/Bool_term.ml
@@ -0,0 +1,171 @@
+
+module ID = Sidekick_smt.ID
+module T = Sidekick_smt.Term
+module Ty = Sidekick_smt.Ty
+open Sidekick_smt.Solver_types
+
+open Bool_intf
+
+type term = T.t
+type t = T.t
+type state = T.state
+
+type 'a view = 'a Bool_intf.view
+
+exception Not_a_th_term
+
+let id_not = ID.make "not"
+let id_and = ID.make "and"
+let id_or = ID.make "or"
+let id_imply = ID.make "=>"
+let id_distinct = ID.make "distinct"
+
+let equal = T.equal
+let hash = T.hash
+
+let view_id cst_id args =
+  if ID.equal cst_id id_not && IArray.length args=1 then (
+    B_not (IArray.get args 0)
+  ) else if ID.equal cst_id id_and then (
+    B_and args
+  ) else if ID.equal cst_id id_or then (
+    B_or args
+  ) else if ID.equal cst_id id_imply && IArray.length args >= 2 then (
+    (* conclusion is stored first *)
+    let len = IArray.length args in
+    B_imply (IArray.sub args 1 (len-1), IArray.get args 0)
+  ) else if ID.equal cst_id id_distinct then (
+    B_distinct args
+  ) else (
+    raise_notrace Not_a_th_term
+  )
+
+let view_as_bool (t:T.t) : T.t view =
+  match T.view t with
+  | Eq (a,b) -> B_eq (a,b)
+  | App_cst ({cst_id; _}, args) ->
+    begin try view_id cst_id args with Not_a_th_term -> B_atom t end
+  | _ -> B_atom t
+
+module C = struct
+
+  let get_ty _ _ = Ty.prop
+
+  let abs ~self _a =
+    match T.view self with
+    | App_cst ({cst_id;_}, args) when ID.equal cst_id id_not && IArray.length args=1 ->
+      (* [not a] --> [a, false] *)
+      IArray.get args 0, false
+    | _ -> self, true
+
+  let eval id args =
+    let module Value = Sidekick_smt.Value in
+    match view_id id args with
+    | B_not (V_bool b) -> Value.bool (not b)
+    | B_and a when IArray.for_all Value.is_true a -> Value.true_
+    | B_and a when IArray.exists Value.is_false a -> Value.false_
+    | B_or a when IArray.exists Value.is_true a -> Value.true_
+    | B_or a when IArray.for_all Value.is_false a -> Value.false_
+    | B_imply (_, V_bool true) -> Value.true_
+    | B_imply (a,_) when IArray.exists Value.is_false a -> Value.true_
+    | B_imply (a,b) when IArray.for_all Value.is_bool a && Value.is_bool b -> Value.false_
+    | B_eq (a,b) -> Value.bool @@ Value.equal a b
+    | B_atom v -> v
+    | B_distinct a ->
+      if
+        Sequence.diagonal (IArray.to_seq a)
+        |> Sequence.for_all (fun (x,y) -> not @@ Value.equal x y)
+      then Value.true_
+      else Value.false_
+    | B_not _ | B_and _ | B_or _ | B_imply _
+        -> Error.errorf "non boolean value in boolean connective"
+
+  (* no congruence closure for boolean terms *)
+  let relevant _id _ _ = false
+
+  let mk_cst ?(do_cc=false) id : cst =
+    {cst_id=id;
+     cst_view=Cst_def {
+         pp=None; abs; ty=get_ty; relevant; is_value=false; do_cc; eval=eval id; }; }
+
+  let not = mk_cst id_not
+  let and_ = mk_cst id_and
+  let or_ = mk_cst id_or
+  let imply = mk_cst id_imply
+  let distinct = mk_cst id_distinct
+end
+
+let as_id id (t:T.t) : T.t IArray.t option =
+  match T.view t with
+  | App_cst ({cst_id; _}, args) when ID.equal id cst_id -> Some args
+  | _ -> None
+
+(* flatten terms of the given ID *)
+let flatten_id op sign (l:T.t list) : T.t list =
+  CCList.flat_map
+    (fun t -> match as_id op t with
+       | Some args -> IArray.to_list args
+       | None when (sign && T.is_true t) || (not sign && T.is_false t) ->
+         [] (* idempotent *)
+       | None -> [t])
+    l
+
+let and_l st l =
+  match flatten_id id_and true l with
+  | [] -> T.true_ st
+  | l when List.exists T.is_false l -> T.false_ st
+  | [x] -> x
+  | args -> T.app_cst st C.and_ (IArray.of_list args)
+
+let or_l st l =
+  match flatten_id id_or false l with
+  | [] -> T.false_ st
+  | l when List.exists T.is_true l -> T.true_ st
+  | [x] -> x
+  | args -> T.app_cst st C.or_ (IArray.of_list args)
+
+let and_ st a b = and_l st [a;b]
+let or_ st a b = or_l st [a;b]
+let and_a st a = and_l st (IArray.to_list a)
+let or_a st a = or_l st (IArray.to_list a)
+
+let eq = T.eq
+
+let not_ st a =
+  match as_id id_not a, T.view a with
+  | _, Bool false -> T.true_ st
+  | _, Bool true -> T.false_ st
+  | Some args, _ ->
+    assert (IArray.length args = 1);
+    IArray.get args 0
+  | None, _ -> T.app_cst st C.not (IArray.singleton a)
+
+let neq st a b = not_ st @@ eq st a b
+
+let imply_a st xs y =
+  if IArray.is_empty xs then y
+  else T.app_cst st C.imply (IArray.append (IArray.singleton y) xs)
+
+let imply_l st xs y = match xs with
+  | [] -> y
+  | _ -> T.app_cst st C.imply (IArray.of_list @@ y :: xs)
+
+let imply st a b = imply_a st (IArray.singleton a) b
+
+let distinct st a =
+  if IArray.length a <= 1
+  then T.true_ st
+  else T.app_cst st C.distinct a
+
+let distinct_l st = function
+  | [] | [_] -> T.true_ st
+  | xs -> distinct st (IArray.of_list xs)
+
+let make st = function
+  | B_atom t -> t
+  | B_eq (a,b) -> T.eq st a b
+  | B_and l -> and_a st l
+  | B_or l -> or_a st l
+  | B_imply (a,b) -> imply_a st a b
+  | B_not t -> not_ st t
+  | B_distinct l -> distinct st l
diff --git a/src/th-bool/Bool_term.mli b/src/th-bool/Bool_term.mli
new file mode 100644
index 00000000..7b34210e
--- /dev/null
+++ b/src/th-bool/Bool_term.mli
@@ -0,0 +1,23 @@
+
+type 'a view = 'a Bool_intf.view
+
+type term = Sidekick_smt.Term.t
+
+include Bool_intf.BOOL_TERM
+  with type t = term
+   and type state = Sidekick_smt.Term.state
+
+val and_ : state -> term -> term -> term
+val or_ : state -> term -> term -> term
+val not_ : state -> term -> term
+val imply : state -> term -> term -> term
+val imply_a : state -> term IArray.t -> term -> term
+val imply_l : state -> term list -> term -> term
+val eq : state -> term -> term -> term
+val neq : state -> term -> term -> term
+val distinct : state -> term IArray.t -> term
+val distinct_l : state -> term list -> term
+val and_a : state -> term IArray.t -> term
+val and_l : state -> term list -> term
+val or_a : state -> term IArray.t -> term
+val or_l : state -> term list -> term
diff --git a/src/th-bool/Sidekick_th_bool.ml b/src/th-bool/Sidekick_th_bool.ml
index 55ee070f..66542221 100644
--- a/src/th-bool/Sidekick_th_bool.ml
+++ b/src/th-bool/Sidekick_th_bool.ml
@@ -1,23 +1,13 @@
 
 (** {1 Theory of Booleans} *)
 
-open Sidekick_smt
-open Solver_types
+type term = Sidekick_smt.Term.t
 
-type term = Term.t
+module Intf = Bool_intf
+module Bool_term = Bool_term
+module Th_dyn_tseitin = Th_dyn_tseitin
 
-(* TODO (long term): relevancy propagation *)
-
-(* TODO: Tseitin on the fly when a composite boolean term is asserted.
-  --> maybe, cache the clause inside the literal *)
-
-let id_not = ID.make "not"
-let id_and = ID.make "and"
-let id_or = ID.make "or"
-let id_imply = ID.make "=>"
-let id_distinct = ID.make "distinct"
-
-type 'a view =
+type 'a view = 'a Intf.view =
   | B_not of 'a
   | B_eq of 'a * 'a
   | B_and of 'a IArray.t
@@ -26,235 +16,9 @@ type 'a view =
   | B_distinct of 'a IArray.t
   | B_atom of 'a
 
-exception Not_a_th_term
+module type BOOL_TERM = Intf.BOOL_TERM
 
-let view_id cst_id args =
-  if ID.equal cst_id id_not && IArray.length args=1 then (
-    B_not (IArray.get args 0)
-  ) else if ID.equal cst_id id_and then (
-    B_and args
-  ) else if ID.equal cst_id id_or then (
-    B_or args
-  ) else if ID.equal cst_id id_imply && IArray.length args >= 2 then (
-    (* conclusion is stored first *)
-    let len = IArray.length args in
-    B_imply (IArray.sub args 1 (len-1), IArray.get args 0)
-  ) else if ID.equal cst_id id_distinct then (
-    B_distinct args
-  ) else (
-    raise_notrace Not_a_th_term
-  )
-
-let view (t:Term.t) : term view =
-  match Term.view t with
-  | Eq (a,b) -> B_eq (a,b)
-  | App_cst ({cst_id; _}, args) ->
-    begin try view_id cst_id args with Not_a_th_term -> B_atom t end
-  | _ -> B_atom t
-
-
-module C = struct
-
-  let get_ty _ _ = Ty.prop
-
-  let abs ~self _a =
-    match Term.view self with
-    | App_cst ({cst_id;_}, args) when ID.equal cst_id id_not && IArray.length args=1 ->
-      (* [not a] --> [a, false] *)
-      IArray.get args 0, false
-    | _ -> self, true
-
-  let eval id args = match view_id id args with
-    | B_not (V_bool b) -> Value.bool (not b)
-    | B_and a when IArray.for_all Value.is_true a -> Value.true_
-    | B_and a when IArray.exists Value.is_false a -> Value.false_
-    | B_or a when IArray.exists Value.is_true a -> Value.true_
-    | B_or a when IArray.for_all Value.is_false a -> Value.false_
-    | B_imply (_, V_bool true) -> Value.true_
-    | B_imply (a,_) when IArray.exists Value.is_false a -> Value.true_
-    | B_imply (a,b) when IArray.for_all Value.is_bool a && Value.is_bool b -> Value.false_
-    | B_eq (a,b) -> Value.bool @@ Value.equal a b
-    | B_atom v -> v
-    | B_distinct a ->
-      if
-        Sequence.diagonal (IArray.to_seq a)
-        |> Sequence.for_all (fun (x,y) -> not @@ Value.equal x y)
-      then Value.true_
-      else Value.false_
-    | B_not _ | B_and _ | B_or _ | B_imply _
-        -> Error.errorf "non boolean value in boolean connective"
-
-  (* no congruence closure for boolean terms *)
-  let relevant _id _ _ = false
-
-  let mk_cst ?(do_cc=false) id : Cst.t =
-    {cst_id=id;
-     cst_view=Cst_def {
-         pp=None; abs; ty=get_ty; relevant; is_value=false; do_cc; eval=eval id; }; }
-
-  let not = mk_cst id_not
-  let and_ = mk_cst id_and
-  let or_ = mk_cst id_or
-  let imply = mk_cst id_imply
-  let distinct = mk_cst id_distinct
-end
-
-let as_id id (t:Term.t) : Term.t IArray.t option =
-  match Term.view t with
-  | App_cst ({cst_id; _}, args) when ID.equal id cst_id -> Some args
-  | _ -> None
-
-(* flatten terms of the given ID *)
-let flatten_id op sign (l:Term.t list) : Term.t list =
-  CCList.flat_map
-    (fun t -> match as_id op t with
-       | Some args -> IArray.to_list args
-       | None when (sign && Term.is_true t) || (not sign && Term.is_false t) ->
-         [] (* idempotent *)
-       | None -> [t])
-    l
-
-let and_l st l =
-  match flatten_id id_and true l with
-  | [] -> Term.true_ st
-  | l when List.exists Term.is_false l -> Term.false_ st
-  | [x] -> x
-  | args -> Term.app_cst st C.and_ (IArray.of_list args)
-
-let or_l st l =
-  match flatten_id id_or false l with
-  | [] -> Term.false_ st
-  | l when List.exists Term.is_true l -> Term.true_ st
-  | [x] -> x
-  | args -> Term.app_cst st C.or_ (IArray.of_list args)
-
-let and_ st a b = and_l st [a;b]
-let or_ st a b = or_l st [a;b]
-
-let eq = Term.eq
-
-let not_ st a =
-  match as_id id_not a, Term.view a with
-  | _, Bool false -> Term.true_ st
-  | _, Bool true -> Term.false_ st
-  | Some args, _ ->
-    assert (IArray.length args = 1);
-    IArray.get args 0
-  | None, _ -> Term.app_cst st C.not (IArray.singleton a)
-
-let neq st a b = not_ st @@ eq st a b
-
-let imply st xs y = match xs with
-  | [] -> y
-  | _ -> Term.app_cst st C.imply (IArray.of_list @@ y :: xs)
-
-let distinct st = function
-  | [] | [_] -> Term.true_ st
-  | xs -> Term.app_cst st C.distinct (IArray.of_list xs)
-
-module Lit = struct
-  include Lit
-  let eq tst a b = Lit.atom ~sign:true (eq tst a b)
-  let neq tst a b = neg @@ eq tst a b
-end
-
-type t = {
-  tst: Term.state;
-  expanded: unit Term.Tbl.t; (* set of literals already expanded *)
-}
-
-let pp_c out c = Fmt.fprintf out "(@[<hv>%a@])" (Util.pp_list Lit.pp) c
-
-let tseitin ~final (self:t) (acts:Theory.actions) (lit:Lit.t) (lit_t:term) (v:term view) : unit =
-  let (module A) = acts in
-  Log.debugf 5 (fun k->k "(@[th_bool.tseitin@ %a@])" Lit.pp lit);
-  let expanded () = Term.Tbl.mem self.expanded lit_t in
-  let add_axiom c =
-    Term.Tbl.replace self.expanded lit_t ();
-    A.add_persistent_axiom c
-  in
-  match v with
-  | B_not _ -> assert false (* normalized *)
-  | B_atom _ | B_eq _ -> () (* CC will manage *)
-  | B_distinct l ->
-    let l = IArray.to_list l in
-    if Lit.sign lit then (
-      A.propagate_distinct l ~neq:lit_t lit
-    ) else if final && not @@ expanded () then (
-      (* add clause [distinct t1…tn ∨ ∨_{i,j>i} t_i=j] *)
-      let c =
-        Sequence.diagonal_l l
-        |> Sequence.map (fun (t,u) -> Lit.eq self.tst t u)
-        |> Sequence.to_rev_list
-      in
-      let c = Lit.neg lit :: c in
-      Log.debugf 5 (fun k->k "(@[tseitin.distinct.case-split@ %a@])" pp_c c);
-      add_axiom c
-    )
-  | B_and subs ->
-    if Lit.sign lit then (
-      (* propagate [lit => subs_i] *)
-      IArray.iter
-        (fun sub ->
-           let sublit = Lit.atom sub in
-           A.propagate sublit [lit])
-        subs
-    ) else if final && not @@ expanded () then (
-      (* axiom [¬lit => ∨_i ¬ subs_i] *)
-      let subs = IArray.to_list subs in
-      let c = Lit.neg lit :: List.map (Lit.atom ~sign:false) subs in
-      add_axiom c
-    )
-  | B_or subs ->
-    if not @@ Lit.sign lit then (
-      (* propagate [¬lit => ¬subs_i] *)
-      IArray.iter
-        (fun sub ->
-           let sublit = Lit.atom ~sign:false sub in
-           A.add_local_axiom [Lit.neg lit; sublit])
-        subs
-    ) else if final && not @@ expanded () then (
-      (* axiom [lit => ∨_i subs_i] *)
-      let subs = IArray.to_list subs in
-      let c = Lit.neg lit :: List.map (Lit.atom ~sign:true) subs in
-      add_axiom c
-    )
-  | B_imply (guard,concl) ->
-    if Lit.sign lit && final && not @@ expanded () then (
-      (* axiom [lit => ∨_i ¬guard_i ∨ concl] *)
-      let guard = IArray.to_list guard in
-      let c = Lit.atom concl :: Lit.neg lit :: List.map (Lit.atom ~sign:false) guard in
-      add_axiom c
-    ) else if not @@ Lit.sign lit then (
-      (* propagate [¬lit => ¬concl] *)
-      A.propagate (Lit.atom ~sign:false concl) [lit];
-      (* propagate [¬lit => ∧_i guard_i] *)
-      IArray.iter
-        (fun sub ->
-           let sublit = Lit.atom ~sign:true sub in
-           A.propagate sublit [lit])
-        guard
-    )
-
-let check_ ~final self acts lits =
-  lits
-    (fun lit ->
-       let t = Lit.term lit in
-       match view t with
-       | B_atom _ | B_eq _ -> ()
-       | v -> tseitin ~final self acts lit t v)
-
-let partial_check (self:t) acts (lits:Lit.t Sequence.t) =
-  check_ ~final:false self acts lits
-
-let final_check (self:t) acts (lits:Lit.t Sequence.t) =
-  check_ ~final:true self acts lits
-
-let th =
-  Theory.make
-    ~partial_check
-    ~final_check
-    ~name:"boolean"
-    ~create:(fun tst -> {tst; expanded=Term.Tbl.create 24})
-    ?mk_model:None (* entirely interpreted *)
-    ()
+(** Dynamic Tseitin transformation *)
+let th_dynamic_tseitin =
+  let module Th = Th_dyn_tseitin.Make(Bool_term) in
+  Th.th
diff --git a/src/th-bool/Sidekick_th_bool.mli b/src/th-bool/Sidekick_th_bool.mli
deleted file mode 100644
index c0b47de2..00000000
--- a/src/th-bool/Sidekick_th_bool.mli
+++ /dev/null
@@ -1,35 +0,0 @@
-
-(** {1 Theory of Booleans} *)
-
-open Sidekick_smt
-
-type term = Term.t
-
-type 'a view = private
-  | B_not of 'a
-  | B_eq of 'a * 'a
-  | B_and of 'a IArray.t
-  | B_or of 'a IArray.t
-  | B_imply of 'a IArray.t * 'a
-  | B_distinct of 'a IArray.t
-  | B_atom of 'a
-
-val view : term -> term view
-
-val and_ : Term.state -> term -> term -> term
-val or_ : Term.state -> term -> term -> term
-val not_ : Term.state -> term -> term
-val imply : Term.state -> term list -> term -> term
-val eq : Term.state -> term -> term -> term
-val neq : Term.state -> term -> term -> term
-val distinct : Term.state -> term list -> term
-val and_l : Term.state -> term list -> term
-val or_l : Term.state -> term list -> term
-
-module Lit : sig
-  type t = Lit.t
-  val eq : Term.state -> term -> term -> t
-  val neq : Term.state -> term -> term -> t
-end
-
-val th : Sidekick_smt.Theory.t
diff --git a/src/th-bool/Th_dyn_tseitin.ml b/src/th-bool/Th_dyn_tseitin.ml
new file mode 100644
index 00000000..b00f30f9
--- /dev/null
+++ b/src/th-bool/Th_dyn_tseitin.ml
@@ -0,0 +1,126 @@
+
+(* TODO (long term): relevancy propagation *)
+
+(* TODO: Tseitin on the fly when a composite boolean term is asserted.
+  --> maybe, cache the clause inside the literal *)
+
+module Theory = Sidekick_smt.Theory
+open Bool_intf
+
+module type ARG = Bool_intf.BOOL_TERM
+  with type t = Sidekick_smt.Term.t
+   and type state = Sidekick_smt.Term.state
+
+module Make(Term : ARG) = struct
+  type term = Term.t
+
+  module T_tbl = CCHashtbl.Make(Term)
+
+  module Lit = struct
+    include Sidekick_smt.Lit
+    let eq tst a b = atom ~sign:true (Term.make tst (B_eq (a,b)))
+    let neq tst a b = neg @@ eq tst a b
+  end
+
+  let pp_c out c = Fmt.fprintf out "(@[<hv>%a@])" (Util.pp_list Lit.pp) c
+
+  type t = {
+    tst: Term.state;
+    expanded: unit T_tbl.t; (* set of literals already expanded *)
+  }
+
+  let tseitin ~final (self:t) (acts:Theory.actions) (lit:Lit.t) (lit_t:term) (v:term view) : unit =
+    let (module A) = acts in
+    Log.debugf 5 (fun k->k "(@[th_bool.tseitin@ %a@])" Lit.pp lit);
+    let expanded () = T_tbl.mem self.expanded lit_t in
+    let add_axiom c =
+      T_tbl.replace self.expanded lit_t ();
+      A.add_persistent_axiom c
+    in
+    match v with
+    | B_not _ -> assert false (* normalized *)
+    | B_atom _ | B_eq _ -> () (* CC will manage *)
+    | B_distinct l ->
+      let l = IArray.to_list l in
+      if Lit.sign lit then (
+        A.propagate_distinct l ~neq:lit_t lit
+      ) else if final && not @@ expanded () then (
+        (* add clause [distinct t1…tn ∨ ∨_{i,j>i} t_i=j] *)
+        let c =
+          Sequence.diagonal_l l
+          |> Sequence.map (fun (t,u) -> Lit.eq self.tst t u)
+          |> Sequence.to_rev_list
+        in
+        let c = Lit.neg lit :: c in
+        Log.debugf 5 (fun k->k "(@[tseitin.distinct.case-split@ %a@])" pp_c c);
+        add_axiom c
+      )
+    | B_and subs ->
+      if Lit.sign lit then (
+        (* propagate [lit => subs_i] *)
+        IArray.iter
+          (fun sub ->
+             let sublit = Lit.atom sub in
+             A.propagate sublit [lit])
+          subs
+      ) else if final && not @@ expanded () then (
+        (* axiom [¬lit => ∨_i ¬ subs_i] *)
+        let subs = IArray.to_list subs in
+        let c = Lit.neg lit :: List.map (Lit.atom ~sign:false) subs in
+        add_axiom c
+      )
+    | B_or subs ->
+      if not @@ Lit.sign lit then (
+        (* propagate [¬lit => ¬subs_i] *)
+        IArray.iter
+          (fun sub ->
+             let sublit = Lit.atom ~sign:false sub in
+             A.add_local_axiom [Lit.neg lit; sublit])
+          subs
+      ) else if final && not @@ expanded () then (
+        (* axiom [lit => ∨_i subs_i] *)
+        let subs = IArray.to_list subs in
+        let c = Lit.neg lit :: List.map (Lit.atom ~sign:true) subs in
+        add_axiom c
+      )
+    | B_imply (guard,concl) ->
+      if Lit.sign lit && final && not @@ expanded () then (
+        (* axiom [lit => ∨_i ¬guard_i ∨ concl] *)
+        let guard = IArray.to_list guard in
+        let c = Lit.atom concl :: Lit.neg lit :: List.map (Lit.atom ~sign:false) guard in
+        add_axiom c
+      ) else if not @@ Lit.sign lit then (
+        (* propagate [¬lit => ¬concl] *)
+        A.propagate (Lit.atom ~sign:false concl) [lit];
+        (* propagate [¬lit => ∧_i guard_i] *)
+        IArray.iter
+          (fun sub ->
+             let sublit = Lit.atom ~sign:true sub in
+             A.propagate sublit [lit])
+          guard
+      )
+
+  let check_ ~final self acts lits =
+    lits
+      (fun lit ->
+         let t = Lit.term lit in
+         match Term.view_as_bool t with
+         | B_atom _ | B_eq _ -> ()
+         | v -> tseitin ~final self acts lit t v)
+
+  let partial_check (self:t) acts (lits:Lit.t Sequence.t) =
+    check_ ~final:false self acts lits
+
+  let final_check (self:t) acts (lits:Lit.t Sequence.t) =
+    check_ ~final:true self acts lits
+
+  let th =
+    Theory.make
+      ~partial_check
+      ~final_check
+      ~name:"boolean"
+      ~create:(fun tst -> {tst; expanded=T_tbl.create 24})
+      ?mk_model:None (* entirely interpreted *)
+      ()
+
+end
diff --git a/src/th-bool/Th_dyn_tseitin.mli b/src/th-bool/Th_dyn_tseitin.mli
new file mode 100644
index 00000000..351f534f
--- /dev/null
+++ b/src/th-bool/Th_dyn_tseitin.mli
@@ -0,0 +1,22 @@
+
+(** {1 Dynamic Tseitin conversion}
+
+    This theory performs the conversion of boolean terms into clauses, on
+    the fly, during the proof search. It is a true CDCL(T)-style theory.
+    *)
+
+module type ARG = Bool_intf.BOOL_TERM
+  with type t = Sidekick_smt.Term.t
+   and type state = Sidekick_smt.Term.state
+
+module Make(Term : ARG) : sig
+  type term = Term.t
+
+  module Lit : sig
+    type t = Sidekick_smt.Lit.t
+    val eq : Term.state -> term -> term -> t
+    val neq : Term.state -> term -> term -> t
+  end
+
+  val th : Sidekick_smt.Theory.t
+end