diff --git a/src/sat/Solver.ml b/src/sat/Solver.ml
index 58a9a986..891274e2 100644
--- a/src/sat/Solver.ml
+++ b/src/sat/Solver.ml
@@ -14,579 +14,518 @@ module type PLUGIN_CDCL_T = Solver_intf.PLUGIN_CDCL_T
 let invalid_argf fmt =
   Format.kasprintf (fun msg -> invalid_arg ("sidekick.sat: " ^ msg)) fmt
 
-module Make (Plugin : PLUGIN) = struct
-  module Step_vec = Proof_trace.Step_vec
+(* ### types ### *)
 
-  type theory = Plugin.t
+(* a boolean variable (positive int) *)
+module Var0 : sig
+  include Int_id.S
+end = struct
+  include Int_id.Make ()
+end
 
-  module Clause_pool_id : sig
-    type t = private int
+type var = Var0.t
 
-    val _unsafe_of_int : int -> t
-  end = struct
-    type t = int
+(* a signed atom. +v is (v << 1), -v is (v<<1 | 1) *)
+module Atom0 : sig
+  include Int_id.S
 
-    let _unsafe_of_int x = x
-  end
+  val neg : t -> t
+  val sign : t -> bool
+  val of_var : var -> t
+  val var : t -> var
+  val pa : var -> t
+  val na : var -> t
 
-  (* ### types ### *)
+  module AVec : Vec_sig.S with type elt := t
+  module ATbl : CCHashtbl.S with type key = t
+end = struct
+  include Int_id.Make ()
 
-  (* a boolean variable (positive int) *)
-  module Var0 : sig
-    include Int_id.S
-  end = struct
-    include Int_id.Make ()
-  end
+  let[@inline] neg i = i lxor 1
+  let[@inline] sign i = i land 1 = 0
+  let[@inline] pa v = (v : var :> int) lsl 1
+  let of_var = pa
+  let[@inline] var a = Var0.of_int_unsafe (a lsr 1)
+  let[@inline] na v = ((v : var :> int) lsl 1) lor 1
 
-  type var = Var0.t
+  module AVec = Veci
+  module ATbl = CCHashtbl.Make (CCInt)
+end
 
-  (* a signed atom. +v is (v << 1), -v is (v<<1 | 1) *)
-  module Atom0 : sig
-    include Int_id.S
+module Clause0 : sig
+  include Int_id.S
+  module Tbl : Hashtbl.S with type key = t
+  module CVec : Vec_sig.S with type elt := t
+end = struct
+  include Int_id.Make ()
+  module Tbl = Util.Int_tbl
+  module CVec = Veci
+end
 
-    val neg : t -> t
-    val sign : t -> bool
-    val of_var : var -> t
-    val var : t -> var
-    val abs : t -> t
-    val pa : var -> t
-    val na : var -> t
+module Step_vec = Proof_trace.Step_vec
 
-    module AVec : Vec_sig.S with type elt := t
-    module ATbl : CCHashtbl.S with type key = t
-  end = struct
-    include Int_id.Make ()
+type atom = Atom0.t
 
-    let[@inline] neg i = i lxor 1
-    let[@inline] sign i = i land 1 = 0
-    let[@inline] pa v = (v : var :> int) lsl 1
-    let of_var = pa
-    let[@inline] abs a = a land lnot 1
-    let[@inline] var a = Var0.of_int_unsafe (a lsr 1)
-    let[@inline] na v = ((v : var :> int) lsl 1) lor 1
+type clause = Clause0.t
+and reason = Decision | Bcp of clause | Bcp_lazy of clause lazy_t
 
-    module AVec = Veci
-    module ATbl = CCHashtbl.Make (CCInt)
-  end
+module AVec = Atom0.AVec
+(** Vector of atoms *)
 
-  type atom = Atom0.t
+module ATbl = Atom0.ATbl
+(** Hashtbl of atoms *)
 
-  module Clause0 : sig
-    include Int_id.S
-    module Tbl : Hashtbl.S with type key = t
-    module CVec : Vec_sig.S with type elt := t
-  end = struct
-    include Int_id.Make ()
-    module Tbl = Util.Int_tbl
-    module CVec = Veci
-  end
+module CVec = Clause0.CVec
+(** Vector of clauses *)
 
-  type clause = Clause0.t
-  and reason = Decision | Bcp of clause | Bcp_lazy of clause lazy_t
+(* ### stores ### *)
 
-  module AVec = Atom0.AVec
-  (** Vector of atoms *)
+module Lit_tbl = Hashtbl.Make (Lit)
 
-  module ATbl = Atom0.ATbl
-  (** Hashtbl of atoms *)
+(* variable/atom store *)
+module Store = struct
+  type cstore = {
+    c_lits: atom array Vec.t; (* storage for clause content *)
+    c_activity: Vec_float.t;
+    c_recycle_idx: Veci.t; (* recycle clause numbers that were GC'd *)
+    c_proof: Step_vec.t; (* clause -> proof_rule for its proof *)
+    c_attached: Bitvec.t;
+    c_marked: Bitvec.t;
+    c_removable: Bitvec.t;
+    c_dead: Bitvec.t;
+  }
 
-  module CVec = Clause0.CVec
-  (** Vector of clauses *)
+  type t = {
+    (* variables *)
+    v_of_lit: var Lit_tbl.t; (* lit -> var *)
+    v_level: int Vec.t; (* decision/assignment level, or -1 *)
+    v_heap_idx: int Vec.t; (* index in priority heap *)
+    v_weight: Vec_float.t; (* heuristic activity *)
+    v_reason: reason option Vec.t; (* reason for assignment *)
+    v_seen: Bitvec.t; (* generic temporary marker *)
+    v_default_polarity: Bitvec.t; (* default polarity in decisions *)
+    mutable v_count: int;
+    (* atoms *)
+    a_is_true: Bitvec.t;
+    a_seen: Bitvec.t;
+    a_form: Lit.t Vec.t;
+    (* TODO: store watches in clauses instead *)
+    a_watched: Clause0.CVec.t Vec.t;
+    a_proof_lvl0: Proof_step.id ATbl.t;
+    (* atom -> proof for it to be true at level 0 *)
+    stat_n_atoms: int Stat.counter;
+    (* clauses *)
+    c_store: cstore;
+  }
 
-  (* ### stores ### *)
+  type store = t
 
-  module Lit_tbl = Hashtbl.Make (Lit)
-
-  (* variable/atom store *)
-  module Store = struct
-    type cstore = {
-      c_lits: atom array Vec.t; (* storage for clause content *)
-      c_activity: Vec_float.t;
-      c_recycle_idx: Veci.t; (* recycle clause numbers that were GC'd *)
-      c_proof: Step_vec.t; (* clause -> proof_rule for its proof *)
-      c_attached: Bitvec.t;
-      c_marked: Bitvec.t;
-      c_removable: Bitvec.t;
-      c_dead: Bitvec.t;
+  let create ?(size = `Big) ~stat () : t =
+    let size_map =
+      match size with
+      | `Tiny -> 8
+      | `Small -> 16
+      | `Big -> 4096
+    in
+    let stat_n_atoms = Stat.mk_int stat "sat.n-atoms" in
+    {
+      v_of_lit = Lit_tbl.create size_map;
+      v_level = Vec.create ();
+      v_heap_idx = Vec.create ();
+      v_weight = Vec_float.create ();
+      v_reason = Vec.create ();
+      v_seen = Bitvec.create ();
+      v_default_polarity = Bitvec.create ();
+      v_count = 0;
+      a_is_true = Bitvec.create ();
+      a_form = Vec.create ();
+      a_watched = Vec.create ();
+      a_seen = Bitvec.create ();
+      a_proof_lvl0 = ATbl.create 16;
+      stat_n_atoms;
+      c_store =
+        {
+          c_lits = Vec.create ();
+          c_activity = Vec_float.create ();
+          c_recycle_idx = Veci.create ~cap:0 ();
+          c_proof = Step_vec.create ~cap:0 ();
+          c_dead = Bitvec.create ();
+          c_attached = Bitvec.create ();
+          c_removable = Bitvec.create ();
+          c_marked = Bitvec.create ();
+        };
     }
 
-    type t = {
-      (* variables *)
-      v_of_lit: var Lit_tbl.t; (* lit -> var *)
-      v_level: int Vec.t; (* decision/assignment level, or -1 *)
-      v_heap_idx: int Vec.t; (* index in priority heap *)
-      v_weight: Vec_float.t; (* heuristic activity *)
-      v_reason: reason option Vec.t; (* reason for assignment *)
-      v_seen: Bitvec.t; (* generic temporary marker *)
-      v_default_polarity: Bitvec.t; (* default polarity in decisions *)
-      mutable v_count: int;
-      (* atoms *)
-      a_is_true: Bitvec.t;
-      a_seen: Bitvec.t;
-      a_form: Lit.t Vec.t;
-      (* TODO: store watches in clauses instead *)
-      a_watched: Clause0.CVec.t Vec.t;
-      a_proof_lvl0: Proof_step.id ATbl.t;
-      (* atom -> proof for it to be true at level 0 *)
-      stat_n_atoms: int Stat.counter;
-      (* clauses *)
-      c_store: cstore;
-    }
+  (** iterate on variables *)
+  let iter_vars self f =
+    Vec.iteri self.v_level ~f:(fun i _ -> f (Var0.of_int_unsafe i))
 
-    type store = t
+  module Var = struct
+    include Var0
 
-    let create ?(size = `Big) ~stat () : t =
-      let size_map =
-        match size with
-        | `Tiny -> 8
-        | `Small -> 16
-        | `Big -> 4096
-      in
-      let stat_n_atoms = Stat.mk_int stat "sat.n-atoms" in
-      {
-        v_of_lit = Lit_tbl.create size_map;
-        v_level = Vec.create ();
-        v_heap_idx = Vec.create ();
-        v_weight = Vec_float.create ();
-        v_reason = Vec.create ();
-        v_seen = Bitvec.create ();
-        v_default_polarity = Bitvec.create ();
-        v_count = 0;
-        a_is_true = Bitvec.create ();
-        a_form = Vec.create ();
-        a_watched = Vec.create ();
-        a_seen = Bitvec.create ();
-        a_proof_lvl0 = ATbl.create 16;
-        stat_n_atoms;
-        c_store =
-          {
-            c_lits = Vec.create ();
-            c_activity = Vec_float.create ();
-            c_recycle_idx = Veci.create ~cap:0 ();
-            c_proof = Step_vec.create ~cap:0 ();
-            c_dead = Bitvec.create ();
-            c_attached = Bitvec.create ();
-            c_removable = Bitvec.create ();
-            c_marked = Bitvec.create ();
-          };
-      }
+    let[@inline] level self v = Vec.get self.v_level (v : var :> int)
+    let[@inline] set_level self v l = Vec.set self.v_level (v : var :> int) l
+    let[@inline] reason self v = Vec.get self.v_reason (v : var :> int)
+    let[@inline] set_reason self v r = Vec.set self.v_reason (v : var :> int) r
+    let[@inline] weight self v = Vec_float.get self.v_weight (v : var :> int)
 
-    (** Number of variables *)
-    let[@inline] n_vars self : int = Vec.size self.v_level
+    let[@inline] set_weight self v w =
+      Vec_float.set self.v_weight (v : var :> int) w
 
-    (** iterate on variables *)
-    let iter_vars self f =
-      Vec.iteri self.v_level ~f:(fun i _ -> f (Var0.of_int_unsafe i))
+    let[@inline] mark self v = Bitvec.set self.v_seen (v : var :> int) true
+    let[@inline] unmark self v = Bitvec.set self.v_seen (v : var :> int) false
+    let[@inline] marked self v = Bitvec.get self.v_seen (v : var :> int)
 
-    module Var = struct
-      include Var0
+    let[@inline] set_default_pol self v b =
+      Bitvec.set self.v_default_polarity (v : var :> int) b
 
-      let[@inline] level self v = Vec.get self.v_level (v : var :> int)
-      let[@inline] set_level self v l = Vec.set self.v_level (v : var :> int) l
-      let[@inline] reason self v = Vec.get self.v_reason (v : var :> int)
+    let[@inline] default_pol self v =
+      Bitvec.get self.v_default_polarity (v : var :> int)
 
-      let[@inline] set_reason self v r =
-        Vec.set self.v_reason (v : var :> int) r
+    let[@inline] heap_idx self v = Vec.get self.v_heap_idx (v : var :> int)
 
-      let[@inline] weight self v = Vec_float.get self.v_weight (v : var :> int)
+    let[@inline] set_heap_idx self v i =
+      Vec.set self.v_heap_idx (v : var :> int) i
+  end
 
-      let[@inline] set_weight self v w =
-        Vec_float.set self.v_weight (v : var :> int) w
+  module Atom = struct
+    include Atom0
 
-      let[@inline] mark self v = Bitvec.set self.v_seen (v : var :> int) true
-      let[@inline] unmark self v = Bitvec.set self.v_seen (v : var :> int) false
-      let[@inline] marked self v = Bitvec.get self.v_seen (v : var :> int)
+    let[@inline] lit self a = Vec.get self.a_form (a : atom :> int)
+    let lit = lit
+    let[@inline] mark self a = Bitvec.set self.a_seen (a : atom :> int) true
+    let[@inline] unmark self a = Bitvec.set self.a_seen (a : atom :> int) false
+    let[@inline] marked self a = Bitvec.get self.a_seen (a : atom :> int)
+    let[@inline] watched self a = Vec.get self.a_watched (a : atom :> int)
+    let[@inline] is_true self a = Bitvec.get self.a_is_true (a : atom :> int)
 
-      let[@inline] set_default_pol self v b =
-        Bitvec.set self.v_default_polarity (v : var :> int) b
+    let[@inline] set_is_true self a b =
+      Bitvec.set self.a_is_true (a : atom :> int) b
 
-      let[@inline] default_pol self v =
-        Bitvec.get self.v_default_polarity (v : var :> int)
+    let[@inline] is_false self a = is_true self (neg a)
+    let[@inline] has_value self a = is_true self a || is_false self a
+    let[@inline] reason self a = Var.reason self (var a)
+    let[@inline] level self a = Var.level self (var a)
+    let[@inline] marked_both self a = marked self a && marked self (neg a)
+    let proof_lvl0 self a = ATbl.get self.a_proof_lvl0 a
+    let set_proof_lvl0 self a p = ATbl.replace self.a_proof_lvl0 a p
+    let pp self fmt a = Lit.pp fmt (lit self a)
 
-      let[@inline] heap_idx self v = Vec.get self.v_heap_idx (v : var :> int)
+    let pp_a self fmt v =
+      if Array.length v = 0 then
+        Format.fprintf fmt "@<1>∅"
+      else (
+        pp self fmt v.(0);
+        if Array.length v > 1 then
+          for i = 1 to Array.length v - 1 do
+            Format.fprintf fmt " @<1>∨ %a" (pp self) v.(i)
+          done
+      )
 
-      let[@inline] set_heap_idx self v i =
-        Vec.set self.v_heap_idx (v : var :> int) i
-    end
+    (* Complete debug printing *)
 
-    module Atom = struct
-      include Atom0
+    let[@inline] pp_sign a =
+      if sign a then
+        "+"
+      else
+        "-"
 
-      let[@inline] lit self a = Vec.get self.a_form (a : atom :> int)
-      let lit = lit
-      let[@inline] mark self a = Bitvec.set self.a_seen (a : atom :> int) true
+    (* print level+reason of assignment *)
+    let debug_reason _self out = function
+      | n, _ when n < 0 -> Format.fprintf out "%%"
+      | n, None -> Format.fprintf out "%d" n
+      | n, Some Decision -> Format.fprintf out "@@%d" n
+      | n, Some (Bcp c) -> Format.fprintf out "->%d/%d" n (c :> int)
+      | n, Some (Bcp_lazy _) -> Format.fprintf out "->%d/<lazy>" n
 
-      let[@inline] unmark self a =
-        Bitvec.set self.a_seen (a : atom :> int) false
+    let pp_level self out a =
+      let v = var a in
+      debug_reason self out (Var.level self v, Var.reason self v)
 
-      let[@inline] marked self a = Bitvec.get self.a_seen (a : atom :> int)
-      let[@inline] watched self a = Vec.get self.a_watched (a : atom :> int)
-      let[@inline] is_true self a = Bitvec.get self.a_is_true (a : atom :> int)
-
-      let[@inline] set_is_true self a b =
-        Bitvec.set self.a_is_true (a : atom :> int) b
-
-      let[@inline] is_false self a = is_true self (neg a)
-      let[@inline] has_value self a = is_true self a || is_false self a
-      let[@inline] reason self a = Var.reason self (var a)
-      let[@inline] level self a = Var.level self (var a)
-      let[@inline] marked_both self a = marked self a && marked self (neg a)
-      let proof_lvl0 self a = ATbl.get self.a_proof_lvl0 a
-      let set_proof_lvl0 self a p = ATbl.replace self.a_proof_lvl0 a p
-      let pp self fmt a = Lit.pp fmt (lit self a)
-
-      let pp_a self fmt v =
-        if Array.length v = 0 then
-          Format.fprintf fmt "@<1>∅"
-        else (
-          pp self fmt v.(0);
-          if Array.length v > 1 then
-            for i = 1 to Array.length v - 1 do
-              Format.fprintf fmt " @<1>∨ %a" (pp self) v.(i)
-            done
-        )
-
-      (* Complete debug printing *)
-
-      let[@inline] pp_sign a =
-        if sign a then
-          "+"
-        else
-          "-"
-
-      (* print level+reason of assignment *)
-      let debug_reason _self out = function
-        | n, _ when n < 0 -> Format.fprintf out "%%"
-        | n, None -> Format.fprintf out "%d" n
-        | n, Some Decision -> Format.fprintf out "@@%d" n
-        | n, Some (Bcp c) -> Format.fprintf out "->%d/%d" n (c :> int)
-        | n, Some (Bcp_lazy _) -> Format.fprintf out "->%d/<lazy>" n
-
-      let pp_level self out a =
-        let v = var a in
-        debug_reason self out (Var.level self v, Var.reason self v)
-
-      let debug_value self out (a : atom) =
-        if is_true self a then
-          Format.fprintf out "T%a" (pp_level self) a
-        else if is_false self a then
-          Format.fprintf out "F%a" (pp_level self) a
-        else
-          ()
-
-      let debug self out a =
-        Format.fprintf out "%s%d[%a][atom:@[<hov>%a@]]" (pp_sign a)
-          (var a : var :> int)
-          (debug_value self) a Lit.pp (lit self a)
-
-      let debug_a self out vec =
-        Array.iter (fun a -> Format.fprintf out "@[%a@]@ " (debug self) a) vec
-
-      let debug_l self out l =
-        List.iter (fun a -> Format.fprintf out "@[%a@]@ " (debug self) a) l
-    end
-
-    module Clause : sig
-      include module type of Clause0 with type t = Clause0.t
-
-      (** Make a clause with the given atoms *)
-
-      val make_a : store -> removable:bool -> atom array -> Proof_step.id -> t
-      val make_l : store -> removable:bool -> atom list -> Proof_step.id -> t
-      val make_vec : store -> removable:bool -> atom Vec.t -> Proof_step.id -> t
-      val n_atoms : store -> t -> int
-      val marked : store -> t -> bool
-      val set_marked : store -> t -> bool -> unit
-      val attached : store -> t -> bool
-      val set_attached : store -> t -> bool -> unit
-      val removable : store -> t -> bool
-      val set_removable : store -> t -> bool -> unit
-      val dead : store -> t -> bool
-      val set_dead : store -> t -> bool -> unit
-
-      val dealloc : store -> t -> unit
-      (** Delete the clause *)
-
-      val set_proof_step : store -> t -> Proof_step.id -> unit
-      val proof_step : store -> t -> Proof_step.id
-      val activity : store -> t -> float
-      val set_activity : store -> t -> float -> unit
-      val iter : store -> f:(atom -> unit) -> t -> unit
-      val fold : store -> f:('a -> atom -> 'a) -> 'a -> t -> 'a
-      val for_all : store -> f:(atom -> bool) -> t -> bool
-      val exists : store -> f:(atom -> bool) -> t -> bool
-      val atoms_a : store -> t -> atom array
-      val lits_l : store -> t -> Lit.t list
-      val lits_a : store -> t -> Lit.t array
-      val lits_iter : store -> t -> Lit.t Iter.t
-      val short_name : store -> t -> string
-      val pp : store -> Format.formatter -> t -> unit
-      val debug : store -> Format.formatter -> t -> unit
-    end = struct
-      include Clause0
-
-      (* TODO: store watch lists inside clauses *)
-
-      let make_a (store : store) ~removable (atoms : atom array) proof_step : t
-          =
-        let {
-          c_recycle_idx;
-          c_lits;
-          c_activity;
-          c_attached;
-          c_dead;
-          c_removable;
-          c_marked;
-          c_proof;
-        } =
-          store.c_store
-        in
-        (* allocate new ID *)
-        let cid =
-          if Veci.is_empty c_recycle_idx then
-            Vec.size c_lits
-          else
-            Veci.pop c_recycle_idx
-        in
-
-        (* allocate space *)
-        (let new_len = cid + 1 in
-         Vec.ensure_size c_lits ~elt:[||] new_len;
-         Vec_float.ensure_size c_activity new_len;
-         Step_vec.ensure_size c_proof new_len;
-         Bitvec.ensure_size c_attached new_len;
-         Bitvec.ensure_size c_dead new_len;
-         Bitvec.ensure_size c_removable new_len;
-         Bitvec.ensure_size c_marked new_len;
-
-         Bitvec.set c_removable cid removable);
-
-        Vec.set c_lits cid atoms;
-        Step_vec.set c_proof cid proof_step;
-
-        let c = of_int_unsafe cid in
-        c
-
-      let make_l store ~removable atoms proof_rule : t =
-        make_a store ~removable (Array.of_list atoms) proof_rule
-
-      let make_vec store ~removable atoms proof_rule : t =
-        make_a store ~removable (Vec.to_array atoms) proof_rule
-
-      let[@inline] n_atoms (store : store) (c : t) : int =
-        Array.length (Vec.get store.c_store.c_lits (c : t :> int))
-
-      let[@inline] iter (store : store) ~f c =
-        let { c_lits; _ } = store.c_store in
-        Array.iter f (Vec.get c_lits (c : t :> int))
-
-      exception Early_exit
-
-      let for_all store ~f c =
-        try
-          iter store c ~f:(fun x -> if not (f x) then raise_notrace Early_exit);
-          true
-        with Early_exit -> false
-
-      let exists store ~f c =
-        try
-          iter store c ~f:(fun x -> if f x then raise_notrace Early_exit);
-          false
-        with Early_exit -> true
-
-      let fold (store : store) ~f acc c =
-        let { c_lits; _ } = store.c_store in
-        Array.fold_left f acc (Vec.get c_lits (c : t :> int))
-
-      let[@inline] marked store c =
-        Bitvec.get store.c_store.c_marked (c : t :> int)
-
-      let[@inline] set_marked store c b =
-        Bitvec.set store.c_store.c_marked (c : t :> int) b
-
-      let[@inline] attached store c =
-        Bitvec.get store.c_store.c_attached (c : t :> int)
-
-      let[@inline] set_attached store c b =
-        Bitvec.set store.c_store.c_attached (c : t :> int) b
-
-      let[@inline] dead store c = Bitvec.get store.c_store.c_dead (c : t :> int)
-
-      let[@inline] set_dead store c b =
-        Bitvec.set store.c_store.c_dead (c : t :> int) b
-
-      let[@inline] removable store c =
-        Bitvec.get store.c_store.c_removable (c : t :> int)
-
-      let[@inline] set_removable store c b =
-        Bitvec.set store.c_store.c_removable (c : t :> int) b
-
-      let[@inline] set_proof_step store c p =
-        Step_vec.set store.c_store.c_proof (c : t :> int) p
-
-      let[@inline] proof_step store c =
-        Step_vec.get store.c_store.c_proof (c : t :> int)
-
-      let dealloc store c : unit =
-        assert (dead store c);
-        let {
-          c_lits;
-          c_recycle_idx;
-          c_activity;
-          c_proof = _;
-          c_dead;
-          c_removable;
-          c_attached;
-          c_marked;
-        } =
-          store.c_store
-        in
-
-        (* clear data *)
-        let cid = (c : t :> int) in
-        Bitvec.set c_attached cid false;
-        Bitvec.set c_dead cid false;
-        Bitvec.set c_removable cid false;
-        Bitvec.set c_marked cid false;
-        Vec.set c_lits cid [||];
-        Vec_float.set c_activity cid 0.;
-
-        Veci.push c_recycle_idx cid;
-        (* recycle idx *)
+    let debug_value self out (a : atom) =
+      if is_true self a then
+        Format.fprintf out "T%a" (pp_level self) a
+      else if is_false self a then
+        Format.fprintf out "F%a" (pp_level self) a
+      else
         ()
 
-      let copy_flags store c1 c2 : unit =
-        set_removable store c2 (removable store c1);
-        ()
+    let debug self out a =
+      Format.fprintf out "%s%d[%a][atom:@[<hov>%a@]]" (pp_sign a)
+        (var a : var :> int)
+        (debug_value self) a Lit.pp (lit self a)
 
-      let[@inline] activity store c =
-        Vec_float.get store.c_store.c_activity (c : t :> int)
+    let debug_a self out vec =
+      Array.iter (fun a -> Format.fprintf out "@[%a@]@ " (debug self) a) vec
+  end
 
-      let[@inline] set_activity store c f =
-        Vec_float.set store.c_store.c_activity (c : t :> int) f
+  module Clause : sig
+    include module type of Clause0 with type t = Clause0.t
 
-      let[@inline] make_removable store l proof_rule : t =
-        make_l store ~removable:true l proof_rule
+    (** Make a clause with the given atoms *)
 
-      let[@inline] make_removable_a store a proof_rule =
-        make_a store ~removable:true a proof_rule
+    val make_a : store -> removable:bool -> atom array -> Proof_step.id -> t
+    val make_l : store -> removable:bool -> atom list -> Proof_step.id -> t
+    val n_atoms : store -> t -> int
+    val marked : store -> t -> bool
+    val set_marked : store -> t -> bool -> unit
+    val attached : store -> t -> bool
+    val set_attached : store -> t -> bool -> unit
+    val removable : store -> t -> bool
+    val dead : store -> t -> bool
+    val set_dead : store -> t -> bool -> unit
 
-      let[@inline] make_permanent store l proof_rule : t =
-        let c = make_l store ~removable:false l proof_rule in
-        assert (not (removable store c));
-        (* permanent by default *)
-        c
+    val dealloc : store -> t -> unit
+    (** Delete the clause *)
 
-      let[@inline] atoms_a store c : atom array =
-        Vec.get store.c_store.c_lits (c : t :> int)
+    val proof_step : store -> t -> Proof_step.id
+    val activity : store -> t -> float
+    val set_activity : store -> t -> float -> unit
+    val iter : store -> f:(atom -> unit) -> t -> unit
+    val fold : store -> f:('a -> atom -> 'a) -> 'a -> t -> 'a
+    val for_all : store -> f:(atom -> bool) -> t -> bool
+    val atoms_a : store -> t -> atom array
+    val lits_l : store -> t -> Lit.t list
+    val lits_a : store -> t -> Lit.t array
+    val lits_iter : store -> t -> Lit.t Iter.t
+    val short_name : store -> t -> string
+    val pp : store -> Format.formatter -> t -> unit
+    val debug : store -> Format.formatter -> t -> unit
+  end = struct
+    include Clause0
 
-      let lits_l store c : Lit.t list =
-        let arr = atoms_a store c in
-        Util.array_to_list_map (Atom.lit store) arr
+    (* TODO: store watch lists inside clauses *)
 
-      let lits_a store c : Lit.t array =
-        let arr = atoms_a store c in
-        Array.map (Atom.lit store) arr
-
-      let lits_iter store c : Lit.t Iter.t =
-        let arr = atoms_a store c in
-        Iter.of_array arr |> Iter.map (Atom.lit store)
-
-      let short_name _store c = Printf.sprintf "cl[%d]" (c : t :> int)
-
-      let pp store fmt c =
-        Format.fprintf fmt "(cl[%d] : %a"
-          (c : t :> int)
-          (Atom.pp_a store) (atoms_a store c)
-
-      let debug store out c =
-        let atoms = atoms_a store c in
-        Format.fprintf out "(@[cl[%d]@ {@[<hov>%a@]}@])"
-          (c : t :> int)
-          (Atom.debug_a store) atoms
-    end
-
-    (* allocate new variable *)
-    let alloc_var_uncached_ ?default_pol:(pol = true) self (form : Lit.t) : var
-        =
+    let make_a (store : store) ~removable (atoms : atom array) proof_step : t =
       let {
-        v_count;
-        v_of_lit;
-        v_level;
-        v_heap_idx;
-        v_weight;
-        v_reason;
-        v_seen;
-        v_default_polarity;
-        stat_n_atoms;
-        a_is_true;
-        a_seen;
-        a_watched;
-        a_form;
-        c_store = _;
-        a_proof_lvl0 = _;
+        c_recycle_idx;
+        c_lits;
+        c_activity;
+        c_attached;
+        c_dead;
+        c_removable;
+        c_marked;
+        c_proof;
       } =
-        self
+        store.c_store
+      in
+      (* allocate new ID *)
+      let cid =
+        if Veci.is_empty c_recycle_idx then
+          Vec.size c_lits
+        else
+          Veci.pop c_recycle_idx
       in
 
-      let v_idx = v_count in
-      let v = Var.of_int_unsafe v_idx in
+      (* allocate space *)
+      (let new_len = cid + 1 in
+       Vec.ensure_size c_lits ~elt:[||] new_len;
+       Vec_float.ensure_size c_activity new_len;
+       Step_vec.ensure_size c_proof new_len;
+       Bitvec.ensure_size c_attached new_len;
+       Bitvec.ensure_size c_dead new_len;
+       Bitvec.ensure_size c_removable new_len;
+       Bitvec.ensure_size c_marked new_len;
 
-      Stat.incr stat_n_atoms;
+       Bitvec.set c_removable cid removable);
 
-      self.v_count <- 1 + v_idx;
-      Lit_tbl.add v_of_lit form v;
-      Vec.push v_level (-1);
-      Vec.push v_heap_idx (-1);
-      Vec.push v_reason None;
-      Vec_float.push v_weight 0.;
-      Bitvec.ensure_size v_seen v_idx;
-      Bitvec.ensure_size v_default_polarity v_idx;
-      Bitvec.set v_default_polarity v_idx pol;
+      Vec.set c_lits cid atoms;
+      Step_vec.set c_proof cid proof_step;
 
-      assert (Vec.size a_form = 2 * (v : var :> int));
-      Bitvec.ensure_size a_is_true (2 * (v : var :> int));
-      Bitvec.ensure_size a_seen (2 * (v : var :> int));
-      Vec.push a_form form;
-      Vec.push a_watched (CVec.create ~cap:0 ());
-      Vec.push a_form (Lit.neg form);
-      Vec.push a_watched (CVec.create ~cap:0 ());
-      assert (Vec.get a_form (Atom.of_var v : atom :> int) == form);
+      let c = of_int_unsafe cid in
+      c
 
-      v
+    let make_l store ~removable atoms proof_rule : t =
+      make_a store ~removable (Array.of_list atoms) proof_rule
 
-    (* create new variable *)
-    let alloc_var (self : t) ?default_pol (lit : Lit.t) :
-        var * Solver_intf.same_sign =
-      let lit, same_sign = Lit.norm_sign lit in
-      try Lit_tbl.find self.v_of_lit lit, same_sign
-      with Not_found ->
-        let v = alloc_var_uncached_ ?default_pol self lit in
-        v, same_sign
+    let[@inline] n_atoms (store : store) (c : t) : int =
+      Array.length (Vec.get store.c_store.c_lits (c : t :> int))
 
-    let clear_var (self : t) (v : var) : unit =
-      Var.unmark self v;
-      Atom.unmark self (Atom.pa v);
-      Atom.unmark self (Atom.na v);
+    let[@inline] iter (store : store) ~f c =
+      let { c_lits; _ } = store.c_store in
+      Array.iter f (Vec.get c_lits (c : t :> int))
+
+    exception Early_exit
+
+    let for_all store ~f c =
+      try
+        iter store c ~f:(fun x -> if not (f x) then raise_notrace Early_exit);
+        true
+      with Early_exit -> false
+
+    let fold (store : store) ~f acc c =
+      let { c_lits; _ } = store.c_store in
+      Array.fold_left f acc (Vec.get c_lits (c : t :> int))
+
+    let[@inline] marked store c =
+      Bitvec.get store.c_store.c_marked (c : t :> int)
+
+    let[@inline] set_marked store c b =
+      Bitvec.set store.c_store.c_marked (c : t :> int) b
+
+    let[@inline] attached store c =
+      Bitvec.get store.c_store.c_attached (c : t :> int)
+
+    let[@inline] set_attached store c b =
+      Bitvec.set store.c_store.c_attached (c : t :> int) b
+
+    let[@inline] dead store c = Bitvec.get store.c_store.c_dead (c : t :> int)
+
+    let[@inline] set_dead store c b =
+      Bitvec.set store.c_store.c_dead (c : t :> int) b
+
+    let[@inline] removable store c =
+      Bitvec.get store.c_store.c_removable (c : t :> int)
+
+    let[@inline] proof_step store c =
+      Step_vec.get store.c_store.c_proof (c : t :> int)
+
+    let dealloc store c : unit =
+      assert (dead store c);
+      let {
+        c_lits;
+        c_recycle_idx;
+        c_activity;
+        c_proof = _;
+        c_dead;
+        c_removable;
+        c_attached;
+        c_marked;
+      } =
+        store.c_store
+      in
+
+      (* clear data *)
+      let cid = (c : t :> int) in
+      Bitvec.set c_attached cid false;
+      Bitvec.set c_dead cid false;
+      Bitvec.set c_removable cid false;
+      Bitvec.set c_marked cid false;
+      Vec.set c_lits cid [||];
+      Vec_float.set c_activity cid 0.;
+
+      Veci.push c_recycle_idx cid;
+      (* recycle idx *)
       ()
 
-    let atom_of_var_ v same_sign : atom =
-      if same_sign then
-        Atom.pa v
-      else
-        Atom.na v
+    let[@inline] activity store c =
+      Vec_float.get store.c_store.c_activity (c : t :> int)
 
-    let alloc_atom (self : t) ?default_pol lit : atom =
-      let var, same_sign = alloc_var self ?default_pol lit in
-      atom_of_var_ var same_sign
+    let[@inline] set_activity store c f =
+      Vec_float.set store.c_store.c_activity (c : t :> int) f
 
-    let find_atom (self : t) lit : atom option =
-      let lit, same_sign = Lit.norm_sign lit in
-      match Lit_tbl.find self.v_of_lit lit with
-      | v -> Some (atom_of_var_ v same_sign)
-      | exception Not_found -> None
+    let[@inline] atoms_a store c : atom array =
+      Vec.get store.c_store.c_lits (c : t :> int)
+
+    let lits_l store c : Lit.t list =
+      let arr = atoms_a store c in
+      Util.array_to_list_map (Atom.lit store) arr
+
+    let lits_a store c : Lit.t array =
+      let arr = atoms_a store c in
+      Array.map (Atom.lit store) arr
+
+    let lits_iter store c : Lit.t Iter.t =
+      let arr = atoms_a store c in
+      Iter.of_array arr |> Iter.map (Atom.lit store)
+
+    let short_name _store c = Printf.sprintf "cl[%d]" (c : t :> int)
+
+    let pp store fmt c =
+      Format.fprintf fmt "(cl[%d] : %a"
+        (c : t :> int)
+        (Atom.pp_a store) (atoms_a store c)
+
+    let debug store out c =
+      let atoms = atoms_a store c in
+      Format.fprintf out "(@[cl[%d]@ {@[<hov>%a@]}@])"
+        (c : t :> int)
+        (Atom.debug_a store) atoms
   end
 
+  (* allocate new variable *)
+  let alloc_var_uncached_ ?default_pol:(pol = true) self (form : Lit.t) : var =
+    let {
+      v_count;
+      v_of_lit;
+      v_level;
+      v_heap_idx;
+      v_weight;
+      v_reason;
+      v_seen;
+      v_default_polarity;
+      stat_n_atoms;
+      a_is_true;
+      a_seen;
+      a_watched;
+      a_form;
+      c_store = _;
+      a_proof_lvl0 = _;
+    } =
+      self
+    in
+
+    let v_idx = v_count in
+    let v = Var.of_int_unsafe v_idx in
+
+    Stat.incr stat_n_atoms;
+
+    self.v_count <- 1 + v_idx;
+    Lit_tbl.add v_of_lit form v;
+    Vec.push v_level (-1);
+    Vec.push v_heap_idx (-1);
+    Vec.push v_reason None;
+    Vec_float.push v_weight 0.;
+    Bitvec.ensure_size v_seen v_idx;
+    Bitvec.ensure_size v_default_polarity v_idx;
+    Bitvec.set v_default_polarity v_idx pol;
+
+    assert (Vec.size a_form = 2 * (v : var :> int));
+    Bitvec.ensure_size a_is_true (2 * (v : var :> int));
+    Bitvec.ensure_size a_seen (2 * (v : var :> int));
+    Vec.push a_form form;
+    Vec.push a_watched (CVec.create ~cap:0 ());
+    Vec.push a_form (Lit.neg form);
+    Vec.push a_watched (CVec.create ~cap:0 ());
+    assert (Vec.get a_form (Atom.of_var v : atom :> int) == form);
+
+    v
+
+  (* create new variable *)
+  let alloc_var (self : t) ?default_pol (lit : Lit.t) :
+      var * Solver_intf.same_sign =
+    let lit, same_sign = Lit.norm_sign lit in
+    try Lit_tbl.find self.v_of_lit lit, same_sign
+    with Not_found ->
+      let v = alloc_var_uncached_ ?default_pol self lit in
+      v, same_sign
+
+  let clear_var (self : t) (v : var) : unit =
+    Var.unmark self v;
+    Atom.unmark self (Atom.pa v);
+    Atom.unmark self (Atom.na v);
+    ()
+
+  let atom_of_var_ v same_sign : atom =
+    if same_sign then
+      Atom.pa v
+    else
+      Atom.na v
+
+  let alloc_atom (self : t) ?default_pol lit : atom =
+    let var, same_sign = alloc_var self ?default_pol lit in
+    atom_of_var_ var same_sign
+
+  let find_atom (self : t) lit : atom option =
+    let lit, same_sign = Lit.norm_sign lit in
+    match Lit_tbl.find self.v_of_lit lit with
+    | v -> Some (atom_of_var_ v same_sign)
+    | exception Not_found -> None
+end
+
+module Make (Plugin : PLUGIN) = struct
+  type theory = Plugin.t
+  type clause = Clause0.t
   type store = Store.t
 
   module Atom = Store.Atom
@@ -665,8 +604,6 @@ module Make (Plugin : PLUGIN) = struct
     let descr = P.descr
     let add c = Vec.push clauses_ c
     let iter ~f = Vec.iter ~f clauses_
-    let push_level () = ()
-    let pop_levels _ = ()
     let size () = Vec.size clauses_
     let needs_gc () = size () > !P.max_size
 
@@ -699,7 +636,6 @@ module Make (Plugin : PLUGIN) = struct
               end)
               ())
 
-  let[@inline] cp_descr_ (module P : CLAUSE_POOL) : string = P.descr ()
   let[@inline] cp_size_ (module P : CLAUSE_POOL) : int = P.size ()
   let[@inline] cp_needs_gc_ (module P : CLAUSE_POOL) : bool = P.needs_gc ()
   let[@inline] cp_add_ (module P : CLAUSE_POOL) c : unit = P.add c
@@ -718,10 +654,8 @@ module Make (Plugin : PLUGIN) = struct
 
     val create : unit -> t
     val is_empty : t -> bool
-    val clear : t -> unit
     val clear_on_backtrack : t -> unit
     val add_clause_learnt : t -> clause -> unit
-    val add_clause_pool : t -> clause -> clause_pool -> unit
     val propagate_atom : t -> atom -> lvl:int -> clause lazy_t -> unit
     val add_decision : t -> atom -> unit
 
@@ -794,9 +728,6 @@ module Make (Plugin : PLUGIN) = struct
       && CVec.is_empty clauses_to_add_learnt
       && Vec.is_empty decisions && Vec.is_empty propagate
 
-    let add_clause_pool (self : t) c pool =
-      Vec.push self.clauses_to_add_in_pool (c, pool)
-
     let add_clause_learnt (self : t) c = CVec.push self.clauses_to_add_learnt c
 
     let propagate_atom self p ~lvl c =
@@ -1027,13 +958,6 @@ module Make (Plugin : PLUGIN) = struct
   *)
   exception Trivial
 
-  (* [arr_to_list a i] converts [a.(i), ... a.(length a-1)] into a list *)
-  let arr_to_list arr i : _ list =
-    if i >= Array.length arr then
-      []
-    else
-      Array.to_list (Array.sub arr i (Array.length arr - i))
-
   (* get/build the proof for [a], which must be an atom true at level 0.
      This uses a global cache to avoid repeated computations, as many clauses
      might resolve against a given 0-level atom. *)
@@ -1259,35 +1183,6 @@ module Make (Plugin : PLUGIN) = struct
       Format.fprintf out "(@[unsat-cause@ :false %a@])"
         (Clause.debug self.store) c
 
-  let prove_unsat self (us : clause) : clause =
-    if Proof_trace.enabled self.proof && Clause.n_atoms self.store us > 0 then (
-      (* reduce [c] to an empty clause, all its literals should be false at level 0 *)
-      Log.debugf 1 (fun k ->
-          k "(@[sat.prove-unsat@ :from %a@])" (Clause.debug self.store) us);
-
-      (* accumulate proofs of all level-0 lits *)
-      let pvec = self.temp_step_vec in
-      assert (Step_vec.is_empty pvec);
-      Clause.iter self.store us ~f:(fun a ->
-          assert (Atom.is_false self.store a && Atom.level self.store a = 0);
-          match Atom.reason self.store a with
-          | Some (Bcp c | Bcp_lazy (lazy c)) ->
-            let p = Clause.proof_step self.store c in
-            Step_vec.push pvec p
-          | _ -> assert false);
-
-      let p_empty =
-        Proof_trace.add_step self.proof
-        @@ Proof_sat.sat_redundant_clause Iter.empty
-             ~hyps:(Step_vec.to_iter pvec)
-      in
-      Step_vec.clear pvec;
-      let c_empty = Clause.make_l self.store [] ~removable:false p_empty in
-
-      c_empty
-    ) else
-      us
-
   (* Unsatisfiability is signaled through an exception, since it can happen
      in multiple places (adding new clauses, or solving for instance). *)
   let report_unsat self (us : unsat_cause) : _ =
@@ -1836,8 +1731,6 @@ module Make (Plugin : PLUGIN) = struct
 
   exception Th_conflict of Clause.t
 
-  let[@inline] slice_get st i = AVec.get st.trail i
-
   let acts_add_clause self ?(keep = false) (l : Lit.t list) (p : Proof_step.id)
       : unit =
     let atoms = List.rev_map (make_atom_ self) l in
@@ -1848,18 +1741,6 @@ module Make (Plugin : PLUGIN) = struct
     (* will be added later, even if we backtrack *)
     Delayed_actions.add_clause_learnt self.delayed_actions c
 
-  let acts_add_clause_in_pool self ~pool (l : Lit.t list) (p : Proof_step.id) :
-      unit =
-    let atoms = List.rev_map (make_atom_ self) l in
-    let removable = true in
-    let c = Clause.make_l self.store ~removable atoms p in
-    let pool = Vec.get self.clause_pools (pool : Clause_pool_id.t :> int) in
-    Log.debugf 5 (fun k ->
-        k "(@[sat.th.add-clause-in-pool@ %a@ :pool %s@])"
-          (Clause.debug self.store) c (cp_descr_ pool));
-    (* will be added later, even if we backtrack *)
-    Delayed_actions.add_clause_pool self.delayed_actions c pool
-
   let acts_add_decision_lit (self : t) (f : Lit.t) (sign : bool) : unit =
     let store = self.store in
     let a = make_atom_ self f in
@@ -2328,7 +2209,6 @@ module Make (Plugin : PLUGIN) = struct
       raise UndecidedLit
 
   let[@inline] eval st lit = fst @@ eval_level st lit
-  let[@inline] unsat_conflict st = st.unsat_at_0
 
   (* fixpoint of propagation and decisions until a model is found, or a
      conflict is reached *)
@@ -2439,8 +2319,6 @@ module Make (Plugin : PLUGIN) = struct
     pp_all self 99 "SAT";
     let t = self.trail in
     let module M = struct
-      type lit = Lit.t
-
       let iter_trail f = AVec.iter ~f:(fun a -> f (Atom.lit self.store a)) t
       let[@inline] eval f = eval self (make_atom_ self f)
       let[@inline] eval_level f = eval_level self (make_atom_ self f)
@@ -2684,4 +2562,4 @@ module Pure_sat = Make (struct
   let final_check () _ = ()
   let has_theory = false
 end)
-[@@inline] [@@specialise]
+[@@specialise]
diff --git a/src/sat/dune b/src/sat/dune
index 56fdf8e7..7a17aa9b 100644
--- a/src/sat/dune
+++ b/src/sat/dune
@@ -2,5 +2,6 @@
  (name sidekick_sat)
  (public_name sidekick.sat)
  (synopsis "Pure OCaml SAT solver implementation for sidekick")
+ (private_modules heap heap_intf)
  (libraries iter sidekick.util sidekick.core)
  (flags :standard -w +32 -open Sidekick_util))