diff --git a/src/base/proof-trace/.ocamlformat-ignore b/src/base/proof-trace/.ocamlformat-ignore
deleted file mode 100644
index 72400434..00000000
--- a/src/base/proof-trace/.ocamlformat-ignore
+++ /dev/null
@@ -1 +0,0 @@
-proof_ser.bare
diff --git a/src/base/proof-trace/Storage.ml b/src/base/proof-trace/Storage.ml
deleted file mode 100644
index 4a3c4288..00000000
--- a/src/base/proof-trace/Storage.ml
+++ /dev/null
@@ -1,32 +0,0 @@
-module CS = Chunk_stack
-
-type t = No_store | In_memory of CS.Buf.t | On_disk of string * out_channel
-
-let pp out = function
-  | No_store -> Fmt.string out "no-store"
-  | In_memory _ -> Fmt.string out "in-memory"
-  | On_disk (file, _) -> Fmt.fprintf out "(on-file %S)" file
-
-let nop_ _ = ()
-
-let iter_chunks_ (r : CS.Reader.t) k =
-  let rec loop () =
-    CS.Reader.next r ~finish:nop_ ~yield:(fun b i _len ->
-        let step = Proof_ser.Bare.of_bytes_exn Proof_ser.Step.decode b ~off:i in
-        k step;
-        loop ())
-  in
-  loop ()
-
-let iter_steps_backward (self : t) : Proof_ser.Step.t Iter.t =
-  let module CS = Chunk_stack in
-  fun yield ->
-    match self with
-    | No_store -> ()
-    | In_memory buf ->
-      let r = CS.Reader.from_buf buf in
-      iter_chunks_ r yield
-    | On_disk (file, _oc) ->
-      let ic = open_in file in
-      let iter = CS.Reader.from_channel_backward ~close_at_end:true ic in
-      iter_chunks_ iter yield
diff --git a/src/base/proof-trace/Storage.mli b/src/base/proof-trace/Storage.mli
deleted file mode 100644
index fd4e3695..00000000
--- a/src/base/proof-trace/Storage.mli
+++ /dev/null
@@ -1,7 +0,0 @@
-type t =
-  | No_store
-  | In_memory of Chunk_stack.Buf.t
-  | On_disk of string * out_channel
-
-val pp : Format.formatter -> t -> unit
-val iter_steps_backward : t -> Proof_ser.Step.t Iter.t
diff --git a/src/base/proof-trace/dune b/src/base/proof-trace/dune
deleted file mode 100644
index c07abe8c..00000000
--- a/src/base/proof-trace/dune
+++ /dev/null
@@ -1,14 +0,0 @@
-(library
- (name sidekick_base_proof_trace)
- (public_name sidekick-base.proof-trace)
- (libraries sidekick.util)
- (flags :standard -w -32 -warn-error -a+8 -open Sidekick_util))
-
-; generate (de)ser + types from .bare file
-
-(rule
- (targets proof_ser.ml)
- (deps proof_ser.bare)
- (mode promote) ; not required in releases
- (action
-  (run bare-codegen --pp --standalone %{deps} -o %{targets})))
diff --git a/src/base/proof-trace/proof_ser.bare b/src/base/proof-trace/proof_ser.bare
deleted file mode 100644
index 23d658a7..00000000
--- a/src/base/proof-trace/proof_ser.bare
+++ /dev/null
@@ -1,149 +0,0 @@
-
-type ID i32
-type Lit ID
-
-type Clause {
-  lits: []Lit
-}
-
-type Step_input {
-  c: Clause
-}
-
-# clause, RUP with previous steps
-type Step_rup {
-  res: Clause
-  hyps: []ID
-}
-
-# TODO: remove?
-# lit <-> expr
-type Step_bridge_lit_expr {
-  lit: Lit
-  expr: ID
-}
-
-# prove congruence closure lemma `\/_{e\in eqns} e`
-type Step_cc {
-  eqns: []ID
-}
-
-# prove t=u using some previous steps and unit equations,
-# and add clause (t=u) with given ID
-type Step_preprocess {
-  t: ID
-  u: ID
-  using: []ID
-}
-
-type Step_clause_rw {
-  c: ID
-  res: Clause
-  using: []ID
-}
-
-type Step_unsat {
-  c: ID
-}
-
-# rewrite `c` with the unit clause `rw_with` of the form `t=u`  *)
-type Step_proof_p1 {
-  rw_with: ID
-  c: ID
-}
-
-# resolve `c` with the unit clause `unit` of the form `|- t`  *)
-type Step_proof_r1 {
-  unit: ID
-  c: ID
-}
-
-# resolve `c1` with `c2` on pivot `pivot` *)
-type Step_proof_res {
-  pivot: ID
-  c1: ID
-  c2: ID
-}
-
-type Step_bool_tauto {
-  lits: []Lit
-}
-
-type Step_bool_c {
-  rule: string
-  exprs: []ID
-}
-
-type Step_true {
-  true_: ID
-}
-
-type Fun_decl {
-  f: string
-}
-
-# define c := rhs
-type Expr_def {
-  c: ID
-  rhs: ID
-}
-
-type Expr_bool {
-  b: bool
-}
-
-type Expr_if {
-  cond: ID
-  then_: ID
-  else_: ID
-}
-
-type Expr_not {
-  f: ID
-}
-
-type Expr_eq {
-  lhs: ID
-  rhs: ID
-}
-
-type Expr_app {
-  f: ID
-  args: []ID
-}
-
-type Expr_isa {
-  c: ID
-  arg: ID
-}
-
-type Step_view
-  ( Step_input
-  | Step_unsat
-  | Step_rup
-  | Step_bridge_lit_expr
-  | Step_cc
-  | Step_preprocess
-  | Step_clause_rw
-  | Step_bool_tauto
-  | Step_bool_c
-  | Step_proof_p1
-  | Step_proof_r1
-  | Step_proof_res
-  | Step_true
-  | Fun_decl
-  | Expr_def
-  | Expr_bool
-  | Expr_if
-  | Expr_not
-  | Expr_isa
-  | Expr_eq
-  | Expr_app
-  )
-
-type Step {
-  id: ID
-  view: Step_view
-}
-
-
diff --git a/src/base/proof-trace/proof_ser.ml b/src/base/proof-trace/proof_ser.ml
deleted file mode 100644
index 471c3b82..00000000
--- a/src/base/proof-trace/proof_ser.ml
+++ /dev/null
@@ -1,1167 +0,0 @@
-(* generated from "proof_ser.bare" using bare-codegen *)
-[@@@ocaml.warning "-26-27"]
-
-(* embedded runtime library *)
-module Bare = struct
-  
-module String_map = Map.Make(String)
-
-module type INPUT = sig
-  val read_byte : unit -> char
-  val read_i16 : unit -> int
-  val read_i32 : unit -> int32
-  val read_i64 : unit -> int64
-  val read_exact : bytes -> int -> int -> unit
-end
-type input = (module INPUT)
-
-let input_of_bytes ?(off=0) ?len (b:bytes) : input =
-  let off = ref off in
-  let len = match len with
-    | None -> Bytes.length b - !off
-    | Some l -> l
-  in
-  if !off + len > Bytes.length b then invalid_arg "input_of_bytes";
-  let[@inline] check_ n = if !off + n > len then invalid_arg "input exhausted" in
-  let module M = struct
-    let read_byte () = check_ 1; let c = Bytes.get b !off in incr off; c
-    let read_i16 () = check_ 2; let r = Bytes.get_int16_le b !off in off := !off + 2; r
-    let read_i32 () = check_ 4; let r = Bytes.get_int32_le b !off in off := !off + 4; r
-    let read_i64 () = check_ 8; let r = Bytes.get_int64_le b !off in off := !off + 8; r
-    let read_exact into i len = check_ len; Bytes.blit b !off into i len; off := !off + len
-  end in
-  (module M)
-
-module Decode = struct
-  type t = input
-
-  let[@inline] of_input (i:input) : t = i
-  let of_bytes ?off ?len b = of_input (input_of_bytes ?off ?len b)
-  let of_string ?off ?len s = of_bytes ?off ?len (Bytes.unsafe_of_string s)
-
-  type 'a dec = t -> 'a
-
-  let uint (self:t) : int64 =
-    let rec loop () =
-      let c = let (module M) = self in M.read_byte() in
-      let c = Char.code c in
-      if c land 0b1000_0000 <> 0 then (
-        let rest = loop() in
-        let c = Int64.of_int (c land 0b0111_1111) in
-        Int64.(logor (shift_left rest 7) c)
-      ) else (
-        Int64.of_int c (* done *)
-      )
-    in
-    loop()
-
-  let int (self:t) : int64 =
-    let open Int64 in
-    let i = uint self in
-    let sign_bit = logand 0b1L i in (* true if negative *)
-    let sign = equal sign_bit 0L in
-    let res =
-      if sign then (
-        shift_right_logical i 1
-      ) else (
-        (* put sign back *)
-        logor (shift_left 1L 63) (shift_right_logical (lognot i) 1)
-      )
-    in
-    res
-
-  let i8 (self:t) : char = let (module M) = self in M.read_byte()
-  let u8 = i8
-
-  let i16 (self:t) = let (module M) = self in M.read_i16()
-  let u16 = i16
-
-  let i32 (self:t) = let (module M) = self in M.read_i32()
-  let u32 = i32
-
-  let i64 (self:t) = let (module M) = self in M.read_i64()
-  let u64 = i64
-
-  let[@inline] bool self : bool =
-    let c = i8 self in
-    Char.code c <> 0
-
-  let f32 (self:t) : float =
-    let i = i32 self in
-    Int32.float_of_bits i
-
-  let f64 (self:t) : float =
-    let i = i64 self in
-    Int64.float_of_bits i
-
-  let data_of ~size (self:t) : bytes =
-    let b = Bytes.create size in
-    let (module M) = self in
-    M.read_exact b 0 size;
-    b
-
-  let data self : bytes =
-    let size = uint self in
-    if Int64.compare size (Int64.of_int Sys.max_string_length) > 0 then
-      invalid_arg "Decode.data: string too large";
-    let size = Int64.to_int size in (* fits, because of previous test *)
-    data_of ~size self
-
-  let string self : string =
-    Bytes.unsafe_to_string (data self)
-
-  let[@inline] optional dec self : _ option =
-    let c = u8 self in
-    if Char.code c = 0 then None else Some (dec self)
-end
-
-module type OUTPUT = sig
-  val write_byte : char -> unit
-  val write_i16 : int -> unit
-  val write_i32 : int32 -> unit
-  val write_i64 : int64 -> unit
-  val write_exact : bytes -> int -> int -> unit
-  val flush : unit -> unit
-end
-
-type output = (module OUTPUT)
-
-let output_of_buffer (buf:Buffer.t) : output =
-  let module M = struct
-    let[@inline] write_byte c = Buffer.add_char buf c
-    let[@inline] write_i16 c = Buffer.add_int16_le buf c
-    let[@inline] write_i32 c = Buffer.add_int32_le buf c
-    let[@inline] write_i64 c = Buffer.add_int64_le buf c
-    let write_exact b i len = Buffer.add_subbytes buf b i len
-    let flush _ = ()
-  end in
-  (module M)
-
-module Encode = struct
-  type t = output
-
-  let[@inline] of_output (o:output) : t = o
-  let[@inline] of_buffer buf : t = of_output @@ output_of_buffer buf
-
-  type 'a enc = t -> 'a -> unit
-
-  (* no need to check for overflow below *)
-  external unsafe_chr : int -> char = "%identity"
-
-  let uint (self:t) (i:int64) : unit =
-    let module I = Int64 in
-    let i = ref i in
-    let continue = ref true in
-    while !continue do
-      let j = I.logand 0b0111_1111L !i in
-      if !i = j then (
-        continue := false;
-        let j = I.to_int j in
-        let (module M) = self in
-        M.write_byte (unsafe_chr j)
-      ) else (
-        (* set bit 8 to [1] *)
-        let lsb = I.to_int (I.logor 0b1000_0000L j) in
-        let lsb = (unsafe_chr lsb) in
-        let (module M) = self in
-        M.write_byte lsb;
-        i := I.shift_right_logical !i 7;
-      )
-    done
-
-  let[@inline] int (self:t) i =
-    let open Int64 in
-    let ui = logxor (shift_left i 1) (shift_right i 63) in
-    uint self ui
-
-  let[@inline] i8 (self:t) x = let (module M) = self in M.write_byte x
-  let u8 = i8
-  let[@inline] i16 (self:t) x = let (module M) = self in M.write_i16 x
-  let u16 = i16
-  let[@inline] i32 (self:t) x = let (module M) = self in M.write_i32 x
-  let u32 = i32
-  let[@inline] i64 (self:t) x = let (module M) = self in M.write_i64 x
-  let u64 = i64
-
-  let bool self x = i8 self (if x then Char.chr 1 else Char.chr 0)
-
-  let f64 (self:t) x = i64 self (Int64.bits_of_float x)
-
-  let data_of ~size (self:t) x =
-    if size <> Bytes.length x then failwith "invalid length for Encode.data_of";
-    let (module M) = self in
-    M.write_exact x 0 size
-
-  let data (self:t) x =
-    uint self (Int64.of_int (Bytes.length x));
-    let (module M) = self in
-    M.write_exact x 0 (Bytes.length x)
-
-  let[@inline] string self x = data self (Bytes.unsafe_of_string x)
-
-  let[@inline] optional enc self x : unit =
-    match x with
-    | None -> u8 self (Char.chr 0)
-    | Some x ->
-      u8 self (Char.chr 1);
-      enc self x
-end
-
-module Pp = struct
-  type 'a t = Format.formatter -> 'a -> unit
-  type 'a iter = ('a -> unit) -> unit
-  let unit out () = Format.pp_print_string out "()"
-  let int8 out c = Format.fprintf out "%d" (Char.code c)
-  let int out x = Format.fprintf out "%d" x
-  let int32 out x = Format.fprintf out "%ld" x
-  let int64 out x = Format.fprintf out "%Ld" x
-  let float out x = Format.fprintf out "%h" x
-  let bool = Format.pp_print_bool
-  let string out x = Format.fprintf out "%S" x
-  let data out x = string out (Bytes.unsafe_to_string x)
-  let option ppelt out x = match x with
-    | None -> Format.fprintf out "None"
-    | Some x -> Format.fprintf out "(Some %a)" ppelt x
-  let array ppelt out x =
-    Format.fprintf out "[@[";
-    Array.iteri (fun i x ->
-        if i>0 then Format.fprintf out ";@ ";
-        ppelt out x)
-      x;
-    Format.fprintf out "@]]"
-  let iter ppelt out xs =
-    Format.fprintf out "[@[";
-    let i = ref 0 in
-    xs (fun x ->
-        if !i>0 then Format.fprintf out ",@ ";
-        incr i;
-        ppelt out x);
-    Format.fprintf out "@]]"
-  let list ppelt out l = iter ppelt out (fun f->List.iter f l)
-end
-
-let to_string (e:'a Encode.enc) (x:'a) =
-  let buf = Buffer.create 32 in
-  e (Encode.of_buffer buf) x;
-  Buffer.contents buf
-
-let of_bytes_exn ?off ?len dec b =
-  let i = Decode.of_bytes ?off ?len b in
-  dec i
-
-let of_bytes ?off ?len dec bs =
-  try Ok (of_bytes_exn ?off ?len dec bs)
-  with
-  | Invalid_argument e | Failure e -> Error e
-  | End_of_file -> Error "end of file"
-
-let of_string_exn ?off ?len dec s = of_bytes_exn ?off ?len dec (Bytes.unsafe_of_string s)
-let of_string ?off ?len dec s = of_bytes ?off ?len dec (Bytes.unsafe_of_string s)
-
-
-(*$inject
-  let to_s f x =
-    let buf = Buffer.create 32 in
-    let out = Encode.of_buffer buf in
-    f out x;
-    Buffer.contents buf
-
-  let of_s f x =
-    let i = Decode.of_string x in
-    f i
-*)
-
-(*$= & ~printer:Int64.to_string
-  37L (of_s Decode.uint (to_s Encode.uint 37L))
-  42L (of_s Decode.uint (to_s Encode.uint 42L))
-  0L (of_s Decode.uint (to_s Encode.uint 0L))
-  105542252L (of_s Decode.uint (to_s Encode.uint 105542252L))
-  Int64.max_int (of_s Decode.uint (to_s Encode.uint Int64.max_int))
-*)
-
-(*$= & ~printer:Int64.to_string
-  37L (of_s Decode.int (to_s Encode.int 37L))
-  42L (of_s Decode.int (to_s Encode.int 42L))
-  0L (of_s Decode.int (to_s Encode.int 0L))
-  105542252L (of_s Decode.int (to_s Encode.int 105542252L))
-  Int64.max_int (of_s Decode.int (to_s Encode.int Int64.max_int))
-  Int64.min_int (of_s Decode.int (to_s Encode.int Int64.min_int))
-  (-1209433446454112432L) (of_s Decode.int (to_s Encode.int (-1209433446454112432L)))
-  (-3112855215860398414L) (of_s Decode.int (to_s Encode.int (-3112855215860398414L)))
-*)
-
-(*$=
-  1 (let s = to_s Encode.int (-1209433446454112432L) in 0x1 land (Char.code s.[0]))
-*)
-
-(*$Q & ~count:1000
-  Q.(int64) (fun s -> \
-    s = (of_s Decode.uint (to_s Encode.uint s)))
-  Q.(small_nat) (fun n -> \
-    let n = Int64.of_int n in \
-    n = (of_s Decode.uint (to_s Encode.uint n)))
-*)
-
-(*$Q & ~count:1000
-  Q.(int64) (fun s -> \
-    s = (of_s Decode.int (to_s Encode.int s)))
-  Q.(small_signed_int) (fun n -> \
-    let n = Int64.of_int n in \
-    n = (of_s Decode.int (to_s Encode.int n)))
-*)
-
-(*$R
-    for i=0 to 1_000 do
-      let i = Int64.of_int i in
-      assert_equal ~printer:Int64.to_string i (of_s Decode.int (to_s Encode.int i))
-    done
-*)
-
-(*$R
-    for i=0 to 1_000 do
-      let i = Int64.of_int i in
-      assert_equal ~printer:Int64.to_string i (of_s Decode.uint (to_s Encode.uint i))
-    done
-*)
-
-(*$Q & ~count:1000
-  Q.(string) (fun s -> \
-    s = (of_s Decode.string (to_s Encode.string s)))
-*)
-
-end
-
-module ID = struct
-  type t = int32
-  
-  (** @raise Invalid_argument in case of error. *)
-  let decode (dec: Bare.Decode.t) : t =
-    Bare.Decode.i32 dec
-  
-  let encode (enc: Bare.Encode.t) (self: t) : unit =
-    Bare.Encode.i32 enc self
-  
-  let pp out (self:t) : unit =
-    Bare.Pp.int32 out self
-  
-end
-
-module Lit = struct
-  type t = ID.t
-  
-  (** @raise Invalid_argument in case of error. *)
-  let decode (dec: Bare.Decode.t) : t =
-    ID.decode dec
-  
-  let encode (enc: Bare.Encode.t) (self: t) : unit =
-    ID.encode enc self
-  
-  let pp out (self:t) : unit =
-    ID.pp out self
-  
-end
-
-module Clause = struct
-  type t = {
-    lits: Lit.t array;
-  }
-  
-  (** @raise Invalid_argument in case of error. *)
-  let decode (dec: Bare.Decode.t) : t =
-    let lits =
-      (let len = Bare.Decode.uint dec in
-       if len>Int64.of_int Sys.max_array_length then invalid_arg "array too big";
-       Array.init (Int64.to_int len) (fun _ -> Lit.decode dec)) in
-    {lits; }
-  
-  let encode (enc: Bare.Encode.t) (self: t) : unit =
-    begin
-      (let arr = self.lits in
-       Bare.Encode.uint enc (Int64.of_int (Array.length arr));
-       Array.iter (fun xi -> Lit.encode enc xi) arr);
-    end
-  
-  let pp out (self:t) : unit =
-    (fun out x ->
-     begin
-       Format.fprintf out "{ @[";
-       Format.fprintf out "lits=%a;@ " (Bare.Pp.array Lit.pp) x.lits;
-       Format.fprintf out "@]}";
-     end) out self
-
-end
-
-module Step_input = struct
-  type t = {
-    c: Clause.t;
-  }
-  
-  (** @raise Invalid_argument in case of error. *)
-  let decode (dec: Bare.Decode.t) : t =
-    let c = Clause.decode dec in {c; }
-  
-  let encode (enc: Bare.Encode.t) (self: t) : unit =
-    begin Clause.encode enc self.c; end
-  
-  let pp out (self:t) : unit =
-    (fun out x ->
-     begin
-       Format.fprintf out "{ @[";
-       Format.fprintf out "c=%a;@ " Clause.pp x.c;
-       Format.fprintf out "@]}";
-     end) out self
-
-end
-
-module Step_rup = struct
-  type t = {
-    res: Clause.t;
-    hyps: ID.t array;
-  }
-  
-  (** @raise Invalid_argument in case of error. *)
-  let decode (dec: Bare.Decode.t) : t =
-    let res = Clause.decode dec in
-    let hyps =
-      (let len = Bare.Decode.uint dec in
-       if len>Int64.of_int Sys.max_array_length then invalid_arg "array too big";
-       Array.init (Int64.to_int len) (fun _ -> ID.decode dec)) in
-    {res; hyps; }
-  
-  let encode (enc: Bare.Encode.t) (self: t) : unit =
-    begin
-      Clause.encode enc self.res;
-      (let arr = self.hyps in
-       Bare.Encode.uint enc (Int64.of_int (Array.length arr));
-       Array.iter (fun xi -> ID.encode enc xi) arr);
-    end
-  
-  let pp out (self:t) : unit =
-    (fun out x ->
-     begin
-       Format.fprintf out "{ @[";
-       Format.fprintf out "res=%a;@ " Clause.pp x.res;
-       Format.fprintf out "hyps=%a;@ " (Bare.Pp.array ID.pp) x.hyps;
-       Format.fprintf out "@]}";
-     end) out self
-
-end
-
-module Step_bridge_lit_expr = struct
-  type t = {
-    lit: Lit.t;
-    expr: ID.t;
-  }
-  
-  (** @raise Invalid_argument in case of error. *)
-  let decode (dec: Bare.Decode.t) : t =
-    let lit = Lit.decode dec in let expr = ID.decode dec in {lit; expr; }
-  
-  let encode (enc: Bare.Encode.t) (self: t) : unit =
-    begin Lit.encode enc self.lit; ID.encode enc self.expr; end
-  
-  let pp out (self:t) : unit =
-    (fun out x ->
-     begin
-       Format.fprintf out "{ @[";
-       Format.fprintf out "lit=%a;@ " Lit.pp x.lit;
-       Format.fprintf out "expr=%a;@ " ID.pp x.expr;
-       Format.fprintf out "@]}";
-     end) out self
-
-end
-
-module Step_cc = struct
-  type t = {
-    eqns: ID.t array;
-  }
-  
-  (** @raise Invalid_argument in case of error. *)
-  let decode (dec: Bare.Decode.t) : t =
-    let eqns =
-      (let len = Bare.Decode.uint dec in
-       if len>Int64.of_int Sys.max_array_length then invalid_arg "array too big";
-       Array.init (Int64.to_int len) (fun _ -> ID.decode dec)) in
-    {eqns; }
-  
-  let encode (enc: Bare.Encode.t) (self: t) : unit =
-    begin
-      (let arr = self.eqns in
-       Bare.Encode.uint enc (Int64.of_int (Array.length arr));
-       Array.iter (fun xi -> ID.encode enc xi) arr);
-    end
-  
-  let pp out (self:t) : unit =
-    (fun out x ->
-     begin
-       Format.fprintf out "{ @[";
-       Format.fprintf out "eqns=%a;@ " (Bare.Pp.array ID.pp) x.eqns;
-       Format.fprintf out "@]}";
-     end) out self
-
-end
-
-module Step_preprocess = struct
-  type t = {
-    t: ID.t;
-    u: ID.t;
-    using: ID.t array;
-  }
-  
-  (** @raise Invalid_argument in case of error. *)
-  let decode (dec: Bare.Decode.t) : t =
-    let t = ID.decode dec in
-    let u = ID.decode dec in
-    let using =
-      (let len = Bare.Decode.uint dec in
-       if len>Int64.of_int Sys.max_array_length then invalid_arg "array too big";
-       Array.init (Int64.to_int len) (fun _ -> ID.decode dec)) in
-    {t; u; using; }
-  
-  let encode (enc: Bare.Encode.t) (self: t) : unit =
-    begin
-      ID.encode enc self.t;
-      ID.encode enc self.u;
-      (let arr = self.using in
-       Bare.Encode.uint enc (Int64.of_int (Array.length arr));
-       Array.iter (fun xi -> ID.encode enc xi) arr);
-    end
-  
-  let pp out (self:t) : unit =
-    (fun out x ->
-     begin
-       Format.fprintf out "{ @[";
-       Format.fprintf out "t=%a;@ " ID.pp x.t;
-       Format.fprintf out "u=%a;@ " ID.pp x.u;
-       Format.fprintf out "using=%a;@ " (Bare.Pp.array ID.pp) x.using;
-       Format.fprintf out "@]}";
-     end) out self
-
-end
-
-module Step_clause_rw = struct
-  type t = {
-    c: ID.t;
-    res: Clause.t;
-    using: ID.t array;
-  }
-  
-  (** @raise Invalid_argument in case of error. *)
-  let decode (dec: Bare.Decode.t) : t =
-    let c = ID.decode dec in
-    let res = Clause.decode dec in
-    let using =
-      (let len = Bare.Decode.uint dec in
-       if len>Int64.of_int Sys.max_array_length then invalid_arg "array too big";
-       Array.init (Int64.to_int len) (fun _ -> ID.decode dec)) in
-    {c; res; using; }
-  
-  let encode (enc: Bare.Encode.t) (self: t) : unit =
-    begin
-      ID.encode enc self.c;
-      Clause.encode enc self.res;
-      (let arr = self.using in
-       Bare.Encode.uint enc (Int64.of_int (Array.length arr));
-       Array.iter (fun xi -> ID.encode enc xi) arr);
-    end
-  
-  let pp out (self:t) : unit =
-    (fun out x ->
-     begin
-       Format.fprintf out "{ @[";
-       Format.fprintf out "c=%a;@ " ID.pp x.c;
-       Format.fprintf out "res=%a;@ " Clause.pp x.res;
-       Format.fprintf out "using=%a;@ " (Bare.Pp.array ID.pp) x.using;
-       Format.fprintf out "@]}";
-     end) out self
-
-end
-
-module Step_unsat = struct
-  type t = {
-    c: ID.t;
-  }
-  
-  (** @raise Invalid_argument in case of error. *)
-  let decode (dec: Bare.Decode.t) : t =
-    let c = ID.decode dec in {c; }
-  
-  let encode (enc: Bare.Encode.t) (self: t) : unit =
-    begin ID.encode enc self.c; end
-  
-  let pp out (self:t) : unit =
-    (fun out x ->
-     begin
-       Format.fprintf out "{ @[";
-       Format.fprintf out "c=%a;@ " ID.pp x.c;
-       Format.fprintf out "@]}";
-     end) out self
-
-end
-
-module Step_proof_p1 = struct
-  type t = {
-    rw_with: ID.t;
-    c: ID.t;
-  }
-  
-  (** @raise Invalid_argument in case of error. *)
-  let decode (dec: Bare.Decode.t) : t =
-    let rw_with = ID.decode dec in let c = ID.decode dec in {rw_with; c; }
-  
-  let encode (enc: Bare.Encode.t) (self: t) : unit =
-    begin ID.encode enc self.rw_with; ID.encode enc self.c; end
-  
-  let pp out (self:t) : unit =
-    (fun out x ->
-     begin
-       Format.fprintf out "{ @[";
-       Format.fprintf out "rw_with=%a;@ " ID.pp x.rw_with;
-       Format.fprintf out "c=%a;@ " ID.pp x.c;
-       Format.fprintf out "@]}";
-     end) out self
-
-end
-
-module Step_proof_r1 = struct
-  type t = {
-    unit: ID.t;
-    c: ID.t;
-  }
-  
-  (** @raise Invalid_argument in case of error. *)
-  let decode (dec: Bare.Decode.t) : t =
-    let unit = ID.decode dec in let c = ID.decode dec in {unit; c; }
-  
-  let encode (enc: Bare.Encode.t) (self: t) : unit =
-    begin ID.encode enc self.unit; ID.encode enc self.c; end
-  
-  let pp out (self:t) : unit =
-    (fun out x ->
-     begin
-       Format.fprintf out "{ @[";
-       Format.fprintf out "unit=%a;@ " ID.pp x.unit;
-       Format.fprintf out "c=%a;@ " ID.pp x.c;
-       Format.fprintf out "@]}";
-     end) out self
-
-end
-
-module Step_proof_res = struct
-  type t = {
-    pivot: ID.t;
-    c1: ID.t;
-    c2: ID.t;
-  }
-  
-  (** @raise Invalid_argument in case of error. *)
-  let decode (dec: Bare.Decode.t) : t =
-    let pivot = ID.decode dec in
-    let c1 = ID.decode dec in
-    let c2 = ID.decode dec in
-    {pivot; c1; c2; }
-  
-  let encode (enc: Bare.Encode.t) (self: t) : unit =
-    begin
-      ID.encode enc self.pivot;
-      ID.encode enc self.c1;
-      ID.encode enc self.c2;
-    end
-  
-  let pp out (self:t) : unit =
-    (fun out x ->
-     begin
-       Format.fprintf out "{ @[";
-       Format.fprintf out "pivot=%a;@ " ID.pp x.pivot;
-       Format.fprintf out "c1=%a;@ " ID.pp x.c1;
-       Format.fprintf out "c2=%a;@ " ID.pp x.c2;
-       Format.fprintf out "@]}";
-     end) out self
-
-end
-
-module Step_bool_tauto = struct
-  type t = {
-    lits: Lit.t array;
-  }
-  
-  (** @raise Invalid_argument in case of error. *)
-  let decode (dec: Bare.Decode.t) : t =
-    let lits =
-      (let len = Bare.Decode.uint dec in
-       if len>Int64.of_int Sys.max_array_length then invalid_arg "array too big";
-       Array.init (Int64.to_int len) (fun _ -> Lit.decode dec)) in
-    {lits; }
-  
-  let encode (enc: Bare.Encode.t) (self: t) : unit =
-    begin
-      (let arr = self.lits in
-       Bare.Encode.uint enc (Int64.of_int (Array.length arr));
-       Array.iter (fun xi -> Lit.encode enc xi) arr);
-    end
-  
-  let pp out (self:t) : unit =
-    (fun out x ->
-     begin
-       Format.fprintf out "{ @[";
-       Format.fprintf out "lits=%a;@ " (Bare.Pp.array Lit.pp) x.lits;
-       Format.fprintf out "@]}";
-     end) out self
-
-end
-
-module Step_bool_c = struct
-  type t = {
-    rule: string;
-    exprs: ID.t array;
-  }
-  
-  (** @raise Invalid_argument in case of error. *)
-  let decode (dec: Bare.Decode.t) : t =
-    let rule = Bare.Decode.string dec in
-    let exprs =
-      (let len = Bare.Decode.uint dec in
-       if len>Int64.of_int Sys.max_array_length then invalid_arg "array too big";
-       Array.init (Int64.to_int len) (fun _ -> ID.decode dec)) in
-    {rule; exprs; }
-  
-  let encode (enc: Bare.Encode.t) (self: t) : unit =
-    begin
-      Bare.Encode.string enc self.rule;
-      (let arr = self.exprs in
-       Bare.Encode.uint enc (Int64.of_int (Array.length arr));
-       Array.iter (fun xi -> ID.encode enc xi) arr);
-    end
-  
-  let pp out (self:t) : unit =
-    (fun out x ->
-     begin
-       Format.fprintf out "{ @[";
-       Format.fprintf out "rule=%a;@ " Bare.Pp.string x.rule;
-       Format.fprintf out "exprs=%a;@ " (Bare.Pp.array ID.pp) x.exprs;
-       Format.fprintf out "@]}";
-     end) out self
-
-end
-
-module Step_true = struct
-  type t = {
-    true_: ID.t;
-  }
-  
-  (** @raise Invalid_argument in case of error. *)
-  let decode (dec: Bare.Decode.t) : t =
-    let true_ = ID.decode dec in {true_; }
-  
-  let encode (enc: Bare.Encode.t) (self: t) : unit =
-    begin ID.encode enc self.true_; end
-  
-  let pp out (self:t) : unit =
-    (fun out x ->
-     begin
-       Format.fprintf out "{ @[";
-       Format.fprintf out "true_=%a;@ " ID.pp x.true_;
-       Format.fprintf out "@]}";
-     end) out self
-
-end
-
-module Fun_decl = struct
-  type t = {
-    f: string;
-  }
-  
-  (** @raise Invalid_argument in case of error. *)
-  let decode (dec: Bare.Decode.t) : t =
-    let f = Bare.Decode.string dec in {f; }
-  
-  let encode (enc: Bare.Encode.t) (self: t) : unit =
-    begin Bare.Encode.string enc self.f; end
-  
-  let pp out (self:t) : unit =
-    (fun out x ->
-     begin
-       Format.fprintf out "{ @[";
-       Format.fprintf out "f=%a;@ " Bare.Pp.string x.f;
-       Format.fprintf out "@]}";
-     end) out self
-
-end
-
-module Expr_def = struct
-  type t = {
-    c: ID.t;
-    rhs: ID.t;
-  }
-  
-  (** @raise Invalid_argument in case of error. *)
-  let decode (dec: Bare.Decode.t) : t =
-    let c = ID.decode dec in let rhs = ID.decode dec in {c; rhs; }
-  
-  let encode (enc: Bare.Encode.t) (self: t) : unit =
-    begin ID.encode enc self.c; ID.encode enc self.rhs; end
-  
-  let pp out (self:t) : unit =
-    (fun out x ->
-     begin
-       Format.fprintf out "{ @[";
-       Format.fprintf out "c=%a;@ " ID.pp x.c;
-       Format.fprintf out "rhs=%a;@ " ID.pp x.rhs;
-       Format.fprintf out "@]}";
-     end) out self
-
-end
-
-module Expr_bool = struct
-  type t = {
-    b: bool;
-  }
-  
-  (** @raise Invalid_argument in case of error. *)
-  let decode (dec: Bare.Decode.t) : t =
-    let b = Bare.Decode.bool dec in {b; }
-  
-  let encode (enc: Bare.Encode.t) (self: t) : unit =
-    begin Bare.Encode.bool enc self.b; end
-  
-  let pp out (self:t) : unit =
-    (fun out x ->
-     begin
-       Format.fprintf out "{ @[";
-       Format.fprintf out "b=%a;@ " Bare.Pp.bool x.b;
-       Format.fprintf out "@]}";
-     end) out self
-
-end
-
-module Expr_if = struct
-  type t = {
-    cond: ID.t;
-    then_: ID.t;
-    else_: ID.t;
-  }
-  
-  (** @raise Invalid_argument in case of error. *)
-  let decode (dec: Bare.Decode.t) : t =
-    let cond = ID.decode dec in
-    let then_ = ID.decode dec in
-    let else_ = ID.decode dec in
-    {cond; then_; else_; }
-  
-  let encode (enc: Bare.Encode.t) (self: t) : unit =
-    begin
-      ID.encode enc self.cond;
-      ID.encode enc self.then_;
-      ID.encode enc self.else_;
-    end
-  
-  let pp out (self:t) : unit =
-    (fun out x ->
-     begin
-       Format.fprintf out "{ @[";
-       Format.fprintf out "cond=%a;@ " ID.pp x.cond;
-       Format.fprintf out "then_=%a;@ " ID.pp x.then_;
-       Format.fprintf out "else_=%a;@ " ID.pp x.else_;
-       Format.fprintf out "@]}";
-     end) out self
-
-end
-
-module Expr_not = struct
-  type t = {
-    f: ID.t;
-  }
-  
-  (** @raise Invalid_argument in case of error. *)
-  let decode (dec: Bare.Decode.t) : t =
-    let f = ID.decode dec in {f; }
-  
-  let encode (enc: Bare.Encode.t) (self: t) : unit =
-    begin ID.encode enc self.f; end
-  
-  let pp out (self:t) : unit =
-    (fun out x ->
-     begin
-       Format.fprintf out "{ @[";
-       Format.fprintf out "f=%a;@ " ID.pp x.f;
-       Format.fprintf out "@]}";
-     end) out self
-
-end
-
-module Expr_eq = struct
-  type t = {
-    lhs: ID.t;
-    rhs: ID.t;
-  }
-  
-  (** @raise Invalid_argument in case of error. *)
-  let decode (dec: Bare.Decode.t) : t =
-    let lhs = ID.decode dec in let rhs = ID.decode dec in {lhs; rhs; }
-  
-  let encode (enc: Bare.Encode.t) (self: t) : unit =
-    begin ID.encode enc self.lhs; ID.encode enc self.rhs; end
-  
-  let pp out (self:t) : unit =
-    (fun out x ->
-     begin
-       Format.fprintf out "{ @[";
-       Format.fprintf out "lhs=%a;@ " ID.pp x.lhs;
-       Format.fprintf out "rhs=%a;@ " ID.pp x.rhs;
-       Format.fprintf out "@]}";
-     end) out self
-
-end
-
-module Expr_app = struct
-  type t = {
-    f: ID.t;
-    args: ID.t array;
-  }
-  
-  (** @raise Invalid_argument in case of error. *)
-  let decode (dec: Bare.Decode.t) : t =
-    let f = ID.decode dec in
-    let args =
-      (let len = Bare.Decode.uint dec in
-       if len>Int64.of_int Sys.max_array_length then invalid_arg "array too big";
-       Array.init (Int64.to_int len) (fun _ -> ID.decode dec)) in
-    {f; args; }
-  
-  let encode (enc: Bare.Encode.t) (self: t) : unit =
-    begin
-      ID.encode enc self.f;
-      (let arr = self.args in
-       Bare.Encode.uint enc (Int64.of_int (Array.length arr));
-       Array.iter (fun xi -> ID.encode enc xi) arr);
-    end
-  
-  let pp out (self:t) : unit =
-    (fun out x ->
-     begin
-       Format.fprintf out "{ @[";
-       Format.fprintf out "f=%a;@ " ID.pp x.f;
-       Format.fprintf out "args=%a;@ " (Bare.Pp.array ID.pp) x.args;
-       Format.fprintf out "@]}";
-     end) out self
-
-end
-
-module Expr_isa = struct
-  type t = {
-    c: ID.t;
-    arg: ID.t;
-  }
-  
-  (** @raise Invalid_argument in case of error. *)
-  let decode (dec: Bare.Decode.t) : t =
-    let c = ID.decode dec in let arg = ID.decode dec in {c; arg; }
-  
-  let encode (enc: Bare.Encode.t) (self: t) : unit =
-    begin ID.encode enc self.c; ID.encode enc self.arg; end
-  
-  let pp out (self:t) : unit =
-    (fun out x ->
-     begin
-       Format.fprintf out "{ @[";
-       Format.fprintf out "c=%a;@ " ID.pp x.c;
-       Format.fprintf out "arg=%a;@ " ID.pp x.arg;
-       Format.fprintf out "@]}";
-     end) out self
-
-end
-
-module Step_view = struct
-  type t =
-    | Step_input of Step_input.t
-    | Step_unsat of Step_unsat.t
-    | Step_rup of Step_rup.t
-    | Step_bridge_lit_expr of Step_bridge_lit_expr.t
-    | Step_cc of Step_cc.t
-    | Step_preprocess of Step_preprocess.t
-    | Step_clause_rw of Step_clause_rw.t
-    | Step_bool_tauto of Step_bool_tauto.t
-    | Step_bool_c of Step_bool_c.t
-    | Step_proof_p1 of Step_proof_p1.t
-    | Step_proof_r1 of Step_proof_r1.t
-    | Step_proof_res of Step_proof_res.t
-    | Step_true of Step_true.t
-    | Fun_decl of Fun_decl.t
-    | Expr_def of Expr_def.t
-    | Expr_bool of Expr_bool.t
-    | Expr_if of Expr_if.t
-    | Expr_not of Expr_not.t
-    | Expr_isa of Expr_isa.t
-    | Expr_eq of Expr_eq.t
-    | Expr_app of Expr_app.t
-    
-  
-  (** @raise Invalid_argument in case of error. *)
-  let decode (dec: Bare.Decode.t) : t =
-    let tag = Bare.Decode.uint dec in
-    match tag with
-    | 0L -> Step_input (Step_input.decode dec)
-    | 1L -> Step_unsat (Step_unsat.decode dec)
-    | 2L -> Step_rup (Step_rup.decode dec)
-    | 3L -> Step_bridge_lit_expr (Step_bridge_lit_expr.decode dec)
-    | 4L -> Step_cc (Step_cc.decode dec)
-    | 5L -> Step_preprocess (Step_preprocess.decode dec)
-    | 6L -> Step_clause_rw (Step_clause_rw.decode dec)
-    | 7L -> Step_bool_tauto (Step_bool_tauto.decode dec)
-    | 8L -> Step_bool_c (Step_bool_c.decode dec)
-    | 9L -> Step_proof_p1 (Step_proof_p1.decode dec)
-    | 10L -> Step_proof_r1 (Step_proof_r1.decode dec)
-    | 11L -> Step_proof_res (Step_proof_res.decode dec)
-    | 12L -> Step_true (Step_true.decode dec)
-    | 13L -> Fun_decl (Fun_decl.decode dec)
-    | 14L -> Expr_def (Expr_def.decode dec)
-    | 15L -> Expr_bool (Expr_bool.decode dec)
-    | 16L -> Expr_if (Expr_if.decode dec)
-    | 17L -> Expr_not (Expr_not.decode dec)
-    | 18L -> Expr_isa (Expr_isa.decode dec)
-    | 19L -> Expr_eq (Expr_eq.decode dec)
-    | 20L -> Expr_app (Expr_app.decode dec)
-    | _ -> invalid_arg
-      (Printf.sprintf "unknown union tag Step_view.t: %Ld" tag)
-    
-  
-  let encode (enc: Bare.Encode.t) (self: t) : unit =
-    match self with
-    | Step_input x ->
-      Bare.Encode.uint enc 0L;
-      Step_input.encode enc x
-    | Step_unsat x ->
-      Bare.Encode.uint enc 1L;
-      Step_unsat.encode enc x
-    | Step_rup x ->
-      Bare.Encode.uint enc 2L;
-      Step_rup.encode enc x
-    | Step_bridge_lit_expr x ->
-      Bare.Encode.uint enc 3L;
-      Step_bridge_lit_expr.encode enc x
-    | Step_cc x ->
-      Bare.Encode.uint enc 4L;
-      Step_cc.encode enc x
-    | Step_preprocess x ->
-      Bare.Encode.uint enc 5L;
-      Step_preprocess.encode enc x
-    | Step_clause_rw x ->
-      Bare.Encode.uint enc 6L;
-      Step_clause_rw.encode enc x
-    | Step_bool_tauto x ->
-      Bare.Encode.uint enc 7L;
-      Step_bool_tauto.encode enc x
-    | Step_bool_c x ->
-      Bare.Encode.uint enc 8L;
-      Step_bool_c.encode enc x
-    | Step_proof_p1 x ->
-      Bare.Encode.uint enc 9L;
-      Step_proof_p1.encode enc x
-    | Step_proof_r1 x ->
-      Bare.Encode.uint enc 10L;
-      Step_proof_r1.encode enc x
-    | Step_proof_res x ->
-      Bare.Encode.uint enc 11L;
-      Step_proof_res.encode enc x
-    | Step_true x ->
-      Bare.Encode.uint enc 12L;
-      Step_true.encode enc x
-    | Fun_decl x ->
-      Bare.Encode.uint enc 13L;
-      Fun_decl.encode enc x
-    | Expr_def x ->
-      Bare.Encode.uint enc 14L;
-      Expr_def.encode enc x
-    | Expr_bool x ->
-      Bare.Encode.uint enc 15L;
-      Expr_bool.encode enc x
-    | Expr_if x ->
-      Bare.Encode.uint enc 16L;
-      Expr_if.encode enc x
-    | Expr_not x ->
-      Bare.Encode.uint enc 17L;
-      Expr_not.encode enc x
-    | Expr_isa x ->
-      Bare.Encode.uint enc 18L;
-      Expr_isa.encode enc x
-    | Expr_eq x ->
-      Bare.Encode.uint enc 19L;
-      Expr_eq.encode enc x
-    | Expr_app x ->
-      Bare.Encode.uint enc 20L;
-      Expr_app.encode enc x
-    
-    
-    let pp out (self:t) : unit =
-      match self with
-      | Step_input x ->
-        Format.fprintf out "(@[Step_input@ %a@])" Step_input.pp x
-      | Step_unsat x ->
-        Format.fprintf out "(@[Step_unsat@ %a@])" Step_unsat.pp x
-      | Step_rup x ->
-        Format.fprintf out "(@[Step_rup@ %a@])" Step_rup.pp x
-      | Step_bridge_lit_expr x ->
-        Format.fprintf out "(@[Step_bridge_lit_expr@ %a@])" Step_bridge_lit_expr.pp x
-      | Step_cc x ->
-        Format.fprintf out "(@[Step_cc@ %a@])" Step_cc.pp x
-      | Step_preprocess x ->
-        Format.fprintf out "(@[Step_preprocess@ %a@])" Step_preprocess.pp x
-      | Step_clause_rw x ->
-        Format.fprintf out "(@[Step_clause_rw@ %a@])" Step_clause_rw.pp x
-      | Step_bool_tauto x ->
-        Format.fprintf out "(@[Step_bool_tauto@ %a@])" Step_bool_tauto.pp x
-      | Step_bool_c x ->
-        Format.fprintf out "(@[Step_bool_c@ %a@])" Step_bool_c.pp x
-      | Step_proof_p1 x ->
-        Format.fprintf out "(@[Step_proof_p1@ %a@])" Step_proof_p1.pp x
-      | Step_proof_r1 x ->
-        Format.fprintf out "(@[Step_proof_r1@ %a@])" Step_proof_r1.pp x
-      | Step_proof_res x ->
-        Format.fprintf out "(@[Step_proof_res@ %a@])" Step_proof_res.pp x
-      | Step_true x ->
-        Format.fprintf out "(@[Step_true@ %a@])" Step_true.pp x
-      | Fun_decl x ->
-        Format.fprintf out "(@[Fun_decl@ %a@])" Fun_decl.pp x
-      | Expr_def x ->
-        Format.fprintf out "(@[Expr_def@ %a@])" Expr_def.pp x
-      | Expr_bool x ->
-        Format.fprintf out "(@[Expr_bool@ %a@])" Expr_bool.pp x
-      | Expr_if x ->
-        Format.fprintf out "(@[Expr_if@ %a@])" Expr_if.pp x
-      | Expr_not x ->
-        Format.fprintf out "(@[Expr_not@ %a@])" Expr_not.pp x
-      | Expr_isa x ->
-        Format.fprintf out "(@[Expr_isa@ %a@])" Expr_isa.pp x
-      | Expr_eq x ->
-        Format.fprintf out "(@[Expr_eq@ %a@])" Expr_eq.pp x
-      | Expr_app x ->
-        Format.fprintf out "(@[Expr_app@ %a@])" Expr_app.pp x
-      
-      
-end
-
-module Step = struct
-  type t = {
-    id: ID.t;
-    view: Step_view.t;
-  }
-  
-  (** @raise Invalid_argument in case of error. *)
-  let decode (dec: Bare.Decode.t) : t =
-    let id = ID.decode dec in let view = Step_view.decode dec in {id; view; }
-  
-  let encode (enc: Bare.Encode.t) (self: t) : unit =
-    begin ID.encode enc self.id; Step_view.encode enc self.view; end
-  
-  let pp out (self:t) : unit =
-    (fun out x ->
-     begin
-       Format.fprintf out "{ @[";
-       Format.fprintf out "id=%a;@ " ID.pp x.id;
-       Format.fprintf out "view=%a;@ " Step_view.pp x.view;
-       Format.fprintf out "@]}";
-     end) out self
-
-end
-
-
diff --git a/src/base/proof-trace/sidekick_base_proof_trace.ml b/src/base/proof-trace/sidekick_base_proof_trace.ml
deleted file mode 100644
index 1d01e517..00000000
--- a/src/base/proof-trace/sidekick_base_proof_trace.ml
+++ /dev/null
@@ -1,10 +0,0 @@
-(** Proof trace with serialization
-
-    This library is useful to serialize a series of reasoning steps
-    in memory or into a file, to be able to reconstruct a proper
-    proof later. *)
-
-module Proof_ser = Proof_ser
-module Storage = Storage
-
-let iter_steps_backward = Storage.iter_steps_backward
diff --git a/src/proof-trace-bare-dump/dune b/src/proof-trace-bare-dump/dune
deleted file mode 100644
index 8b273b7e..00000000
--- a/src/proof-trace-bare-dump/dune
+++ /dev/null
@@ -1,5 +0,0 @@
-(executable
- (name proof_trace_dump)
- (modes native)
- (libraries containers sidekick.util sidekick-base.proof-trace)
- (flags :standard -w -32 -warn-error -a+8 -open Sidekick_util))
diff --git a/src/proof-trace-bare-dump/proof_trace_dump.ml b/src/proof-trace-bare-dump/proof_trace_dump.ml
deleted file mode 100644
index 6c9b33eb..00000000
--- a/src/proof-trace-bare-dump/proof_trace_dump.ml
+++ /dev/null
@@ -1,44 +0,0 @@
-module CS = Chunk_stack
-module Pr_trace = Sidekick_base_proof_trace
-module Proof_ser = Pr_trace.Proof_ser
-
-let file = ref ""
-let quiet = ref false
-
-let parse_file () : unit =
-  Log.debugf 2 (fun k -> k "parsing file %S" !file);
-
-  CS.Reader.with_file_backward !file @@ fun reader ->
-  (* TODO: use the storage module function
-     Pr_trace.iter_steps_backward (Pr_trace.Storage.
-  *)
-  let n = ref 0 in
-  let rec display_steps () =
-    CS.Reader.next reader
-      ~finish:(fun () -> ())
-      ~yield:(fun b i _len ->
-        let decode = Proof_ser.Bare.Decode.of_bytes b ~off:i in
-        let step = Proof_ser.Step.decode decode in
-        incr n;
-        if not !quiet then Format.printf "@[<2>%a@]@." Proof_ser.Step.pp step;
-        display_steps ())
-  in
-  display_steps ();
-  Format.printf "read %d steps@." !n;
-  ()
-
-let () =
-  let opts =
-    [
-      ( "--bt",
-        Arg.Unit (fun () -> Printexc.record_backtrace true),
-        " enable stack traces" );
-      "-d", Arg.Int Log.set_debug, "<lvl> sets the debug verbose level";
-      "-q", Arg.Set quiet, " quiet: do not print steps";
-    ]
-    |> Arg.align
-  in
-  Arg.parse opts (fun f -> file := f) "proof-trace-dump <file>";
-  if !file = "" then failwith "please provide a file";
-
-  parse_file ()
diff --git a/src/proof-trace/.ocamlformat-ignore b/src/proof-trace/.ocamlformat-ignore
deleted file mode 100644
index 1b13589e..00000000
--- a/src/proof-trace/.ocamlformat-ignore
+++ /dev/null
@@ -1 +0,0 @@
-proof_ser.ml
diff --git a/src/sat/tracer.ml b/src/sat/tracer.ml
new file mode 100644
index 00000000..dc846105
--- /dev/null
+++ b/src/sat/tracer.ml
@@ -0,0 +1,31 @@
+module Tr = Sidekick_trace
+
+class type t =
+  object
+    method assert_clause : id:int -> Lit.t Iter.t -> Tr.Entry_id.t
+    method delete_clause : id:int -> Lit.t Iter.t -> unit
+    method unsat_clause : id:int -> Tr.Entry_id.t
+    method encode_lit : Lit.t -> Ser_value.t
+  end
+
+class dummy : t =
+  object
+    method assert_clause ~id:_ _ = Tr.Entry_id.dummy
+    method delete_clause ~id:_ _ = ()
+    method unsat_clause ~id:_ = Tr.Entry_id.dummy
+    method encode_lit _ = Ser_value.null
+  end
+
+let dummy : t = new dummy
+let assert_clause (self : #t) ~id c : Tr.Entry_id.t = self#assert_clause ~id c
+
+let assert_clause' (self : #t) ~id c : unit =
+  ignore (self#assert_clause ~id c : Tr.Entry_id.t)
+
+let unsat_clause (self : #t) ~id : Tr.Entry_id.t = self#unsat_clause ~id
+
+let unsat_clause' (self : #t) ~id : unit =
+  ignore (self#unsat_clause ~id : Tr.Entry_id.t)
+
+let delete_clause (self : #t) ~id c = self#delete_clause ~id c
+let encode_lit (self : #t) lit = self#encode_lit lit
diff --git a/src/sat/tracer.mli b/src/sat/tracer.mli
new file mode 100644
index 00000000..e9f30ebf
--- /dev/null
+++ b/src/sat/tracer.mli
@@ -0,0 +1,24 @@
+(** Tracer for clauses and literals *)
+
+module Tr = Sidekick_trace
+
+(** Tracer for clauses. *)
+class type t =
+  object
+    method assert_clause : id:int -> Lit.t Iter.t -> Tr.Entry_id.t
+    method delete_clause : id:int -> Lit.t Iter.t -> unit
+    method unsat_clause : id:int -> Tr.Entry_id.t
+    method encode_lit : Lit.t -> Ser_value.t
+  end
+
+class dummy : t
+
+val dummy : t
+(** Dummy tracer, recording nothing. *)
+
+val assert_clause : #t -> id:int -> Lit.t Iter.t -> Tr.Entry_id.t
+val assert_clause' : #t -> id:int -> Lit.t Iter.t -> unit
+val delete_clause : #t -> id:int -> Lit.t Iter.t -> unit
+val unsat_clause : #t -> id:int -> Tr.Entry_id.t
+val unsat_clause' : #t -> id:int -> unit
+val encode_lit : #t -> Lit.t -> Ser_value.t
diff --git a/src/trace/entry_view.ml b/src/trace/entry_view.ml
deleted file mode 100644
index 060620cc..00000000
--- a/src/trace/entry_view.ml
+++ /dev/null
@@ -1,6 +0,0 @@
-
-
-type t = ..
-(** Extensible type, each entry uses its own.
-
-   See {!Entry.t}. *)