diff --git a/src/backend/Coq.ml b/src/backend/Coq.ml
index efdbe8b3..47fa6e3e 100644
--- a/src/backend/Coq.ml
+++ b/src/backend/Coq.ml
@@ -22,12 +22,11 @@ module Make(S : Res.S)(A : Arg with type hyp := S.clause
                                 and type lemma := S.clause
                                 and type assumption := S.clause) = struct
 
-  module M = Map.Make(struct
-      type t = S.St.atom
-      let compare a b = compare a.S.St.aid b.S.St.aid
-    end)
+  module Atom = S.St.Atom
+  module Clause = S.St.Clause
+  module M = Map.Make(S.St.Atom)
 
-  let name c = c.S.St.name
+  let name = S.St.Clause.name
 
   let clause_map c =
     let rec aux acc a i =
@@ -70,27 +69,26 @@ module Make(S : Res.S)(A : Arg with type hyp := S.clause
          )) h1.S.St.atoms
 
   let resolution fmt goal hyp1 hyp2 atom =
-    let a = S.St.(atom.var.pa) in
+    let a = Atom.abs atom in
     let h1, h2 =
-      if Array.exists ((==) a) hyp1.S.St.atoms then hyp1, hyp2
-      else (assert (Array.exists ((==) a) hyp2.S.St.atoms); hyp2, hyp1)
+      if Array.exists (Atom.equal a) hyp1.S.St.atoms then hyp1, hyp2
+      else (assert (Array.exists (Atom.equal a) hyp2.S.St.atoms); hyp2, hyp1)
     in
     (** Print some debug info *)
     Format.fprintf fmt
       "(* Clausal resolution. Goal : %s ; Hyps : %s, %s *)@\n"
       (name goal) (name h1) (name h2);
     (** Prove the goal: intro the axioms, then perform resolution *)
-    if Array.length goal.S.St.atoms = 0 then begin
+    if Array.length goal.S.St.atoms = 0 then (
       let m = M.empty in
       Format.fprintf fmt "exact @[<hov 1>(%a)@].@\n" (resolution_aux m a h1 h2) ();
       false
-    end else begin
+    ) else (
       let m = clause_map goal in
       Format.fprintf fmt "pose proof @[<hov>(fun %a=>@ %a)@ as %s.@]@\n"
         (clause_iter m "%s@ ") goal (resolution_aux m a h1 h2) () (name goal);
       true
-    end
-
+    )
 
   (* Count uses of hypotheses *)
   let incr_use h c =
diff --git a/src/backend/Dimacs.ml b/src/backend/Dimacs.ml
index f2445d9f..a4e35b0f 100644
--- a/src/backend/Dimacs.ml
+++ b/src/backend/Dimacs.ml
@@ -36,10 +36,10 @@ module Make(St : Solver_types_intf.S)(Dummy: sig end) = struct
 
   (* Dimacs & iCNF export *)
   let export_vec name fmt vec =
-    Format.fprintf fmt "c %s@,%a@," name (Vec.print ~sep:"" St.pp_dimacs) vec
+    Format.fprintf fmt "c %s@,%a@," name (Vec.print ~sep:"" St.Clause.pp_dimacs) vec
 
   let export_assumption fmt vec =
-    Format.fprintf fmt "c Local assumptions@,a %a@," St.pp_dimacs vec
+    Format.fprintf fmt "c Local assumptions@,a %a@," St.Clause.pp_dimacs vec
 
   let export_icnf_aux r name map_filter fmt vec =
     let aux fmt _ =
@@ -47,28 +47,28 @@ module Make(St : Solver_types_intf.S)(Dummy: sig end) = struct
         let x = Vec.get vec i in
         match map_filter x with
         | None -> ()
-        | Some _ -> Format.fprintf fmt "%a@," St.pp_dimacs (Vec.get vec i)
+        | Some _ -> Format.fprintf fmt "%a@," St.Clause.pp_dimacs (Vec.get vec i)
       done;
       r := Vec.size vec
     in
     Format.fprintf fmt "c %s@,%a" name aux vec
 
   let map_filter_learnt c =
-    match c.St.cpremise with
+    match St.Clause.premise c with
     | St.Hyp | St.Local -> assert false
     | St.Lemma _ -> Some c
     | St.History l ->
       begin match l with
         | [] -> assert false
         | d :: _ ->
-          begin match d.St.cpremise with
+          begin match St.Clause.premise d with
             | St.Lemma _ -> Some d
             | St.Hyp | St.Local | St.History _ -> None
           end
       end
 
   let filter_vec learnt =
-    let lemmas = Vec.make (Vec.size learnt) St.dummy_clause in
+    let lemmas = Vec.make (Vec.size learnt) St.Clause.dummy in
     Vec.iter (fun c ->
         match map_filter_learnt c with
         | None -> ()
@@ -77,17 +77,13 @@ module Make(St : Solver_types_intf.S)(Dummy: sig end) = struct
     lemmas
 
   let export fmt ~hyps ~history ~local =
-    assert (Vec.for_all (function
-        | { St.cpremise = St.Hyp; _} -> true | _ -> false
-      ) hyps);
+    assert (Vec.for_all (fun c -> St.Clause.premise c = St.Hyp) hyps);
     (* Learnt clauses, then filtered to only keep only
        the theory lemmas; all other learnt clauses should be logical
        consequences of the rest. *)
     let lemmas = filter_vec history in
     (* Local assertions *)
-    assert (Vec.for_all (function
-        | { St.cpremise = St.Local; _} -> true | _ -> false
-      ) local);
+    assert (Vec.for_all (fun c -> St.Local = St.Clause.premise c) local);
     (* Number of atoms and clauses *)
     let n = St.nb_elt () in
     let m = Vec.size local + Vec.size hyps + Vec.size lemmas in
@@ -102,15 +98,16 @@ module Make(St : Solver_types_intf.S)(Dummy: sig end) = struct
   let icnf_lemmas = ref 0
 
   let export_icnf fmt ~hyps ~history ~local =
-    assert (Vec.for_all (function
-        | { St.cpremise = St.Hyp; _} -> true | _ -> false
-      ) hyps);
+    assert (Vec.for_all (fun c -> St.Clause.premise c = St.Hyp) hyps);
     let lemmas = history in
     (* Local assertions *)
-    let l = List.map (function
-        | {St.cpremise = St.Local; atoms = [| a |];_ } -> a
-        | _ -> assert false) (Vec.to_list local) in
-    let local = St.make_clause "local (tmp)" l St.Local in
+    let l = List.map
+        (fun c -> match St.Clause.premise c, St.Clause.atoms c with
+             | St.Local, [| a |] -> a
+             | _ -> assert false)
+        (Vec.to_list local)
+    in
+    let local = St.Clause.make l St.Local in
     (* Number of atoms and clauses *)
     Format.fprintf fmt
       "@[<v>%s@,%a%a%a@]@."
diff --git a/src/backend/Dot.ml b/src/backend/Dot.ml
index 78c160cb..2fde8287 100644
--- a/src/backend/Dot.ml
+++ b/src/backend/Dot.ml
@@ -31,20 +31,22 @@ module type Arg = sig
 end
 
 module Default(S : Res.S) = struct
+  module Atom = S.St.Atom
+  module Clause = S.St.Clause
 
-  let print_atom = S.St.print_atom
+  let print_atom = Atom.pp
 
   let hyp_info c =
     "hypothesis", Some "LIGHTBLUE",
-    [ fun fmt () -> Format.fprintf fmt "%s" c.S.St.name]
+    [ fun fmt () -> Format.fprintf fmt "%s" @@ Clause.name c]
 
   let lemma_info c =
     "lemma", Some "BLUE",
-    [ fun fmt () -> Format.fprintf fmt "%s" c.S.St.name]
+    [ fun fmt () -> Format.fprintf fmt "%s" @@ Clause.name c]
 
   let assumption_info c =
     "assumption", Some "PURPLE",
-    [ fun fmt () -> Format.fprintf fmt "%s" c.S.St.name]
+    [ fun fmt () -> Format.fprintf fmt "%s" @@ Clause.name c]
 
 end
 
@@ -53,15 +55,17 @@ module Make(S : Res.S)(A : Arg with type atom := S.atom
                                 and type hyp := S.clause
                                 and type lemma := S.clause
                                 and type assumption := S.clause) = struct
+  module Atom = S.St.Atom
+  module Clause = S.St.Clause
 
-  let node_id n = n.S.conclusion.S.St.name
+  let node_id n = Clause.name n.S.conclusion
 
   let res_node_id n = (node_id n) ^ "_res"
 
   let proof_id p = node_id (S.expand p)
 
   let print_clause fmt c =
-    let v = c.S.St.atoms in
+    let v = Clause.atoms c in
     if Array.length v = 0 then
       Format.fprintf fmt "⊥"
     else
@@ -149,9 +153,11 @@ module Simple(S : Res.S)
               and type lemma := S.lemma
               and type assumption = S.St.formula) =
   Make(S)(struct
+    module Atom = S.St.Atom
+    module Clause = S.St.Clause
 
     (* Some helpers *)
-    let lit a = a.S.St.lit
+    let lit = Atom.lit
 
     let get_assumption c =
       match S.to_list c with
@@ -159,13 +165,13 @@ module Simple(S : Res.S)
       | _ -> assert false
 
     let get_lemma c =
-      match c.S.St.cpremise with
+      match Clause.premise c with
       | S.St.Lemma p -> p
       | _ -> assert false
 
     (* Actual functions *)
     let print_atom fmt a =
-      A.print_atom fmt a.S.St.lit
+      A.print_atom fmt (Atom.lit a)
 
     let hyp_info c =
       A.hyp_info (List.map lit (S.to_list c))
diff --git a/src/core/Internal.ml b/src/core/Internal.ml
index 078747ef..6ddc4287 100644
--- a/src/core/Internal.ml
+++ b/src/core/Internal.ml
@@ -16,11 +16,11 @@ module Make
   open St
 
   module H = Heap.Make(struct
-    type t = St.elt
-    let[@inline] cmp i j = get_elt_weight j < get_elt_weight i (* comparison by weight *)
-    let dummy = elt_of_var St.dummy_var
-    let idx = get_elt_idx
-    let set_idx = set_elt_idx
+    type t = St.Elt.t
+    let[@inline] cmp i j = Elt.weight j < Elt.weight i (* comparison by weight *)
+    let dummy = Elt.of_var St.Var.dummy
+    let idx = Elt.idx
+    let set_idx = Elt.set_idx
   end)
 
   exception Sat
@@ -61,9 +61,8 @@ module Make
     mutable next_decision : atom option;
     (* When the last conflict was a semantic one, this stores the next decision to make *)
 
-    elt_queue : t Vec.t;
-    (* decision stack + propagated elements (atoms or assignments).
-       Also called "trail" in some solvers. *)
+    trail : trail_elt Vec.t;
+    (* decision stack + propagated elements (atoms or assignments). *)
 
     elt_levels : int Vec.t;
     (* decision levels in [trail]  *)
@@ -74,19 +73,19 @@ module Make
     (* user levels in [clauses_temp] *)
 
     mutable th_head : int;
-    (* Start offset in the queue {!elt_queue} of
+    (* Start offset in the queue {!trail} of
        unit facts not yet seen by the theory. *)
     mutable elt_head : int;
-    (* Start offset in the queue {!elt_queue} of
+    (* Start offset in the queue {!trail} of
        unit facts to propagate, within the trail *)
 
     (* invariant:
        - during propagation, th_head <= elt_head
-       - then, once elt_head reaches length elt_queue, Th.assume is
+       - then, once elt_head reaches length trail, Th.assume is
          called so that th_head can catch up with elt_head
        - this is repeated until a fixpoint is reached;
        - before a decision (and after the fixpoint),
-         th_head = elt_head = length elt_queue
+         th_head = elt_head = length trail
     *)
 
 
@@ -139,9 +138,9 @@ module Make
     unsat_conflict = None;
     next_decision = None;
 
-    clauses_hyps = Vec.make 0 dummy_clause;
-    clauses_learnt = Vec.make 0 dummy_clause;
-    clauses_temp = Vec.make 0 dummy_clause;
+    clauses_hyps = Vec.make 0 Clause.dummy;
+    clauses_learnt = Vec.make 0 Clause.dummy;
+    clauses_temp = Vec.make 0 Clause.dummy;
 
     clauses_root = Stack.create ();
     clauses_to_add = Stack.create ();
@@ -149,7 +148,7 @@ module Make
     th_head = 0;
     elt_head = 0;
 
-    elt_queue = Vec.make 601 (of_atom dummy_atom);
+    trail = Vec.make 601 (Trail_elt.of_atom Atom.dummy);
     elt_levels = Vec.make 601 (-1);
     th_levels = Vec.make 100 Plugin.dummy;
     user_levels = Vec.make 10 (-1);
@@ -212,15 +211,18 @@ module Make
   (* When we have a new literal,
      we need to first create the list of its subterms. *)
   let atom (f:St.formula) : atom =
-    let res = add_atom f in
-    if St.mcsat then
+    let res = Atom.make f in
+    if St.mcsat then (
       begin match res.var.v_assignable with
         | Some _ -> ()
         | None ->
           let l = ref [] in
-          Plugin.iter_assignable (fun t -> l := add_term t :: !l) res.var.pa.lit;
+          Plugin.iter_assignable
+            (fun t -> l := Lit.make t :: !l)
+            res.var.pa.lit;
           res.var.v_assignable <- Some !l;
       end;
+    );
     res
 
   (* Variable and literal activity.
@@ -238,14 +240,14 @@ module Make
     end
 
   and insert_subterms_order (v:St.var) : unit =
-    iter_sub (fun t -> insert_var_order (elt_of_lit t)) v
+    iter_sub (fun t -> insert_var_order (Elt.of_lit t)) v
 
   (* Add new litterals/atoms on which to decide on, even if there is no
      clause that constrains it.
      We could maybe check if they have already has been decided before
      inserting them into the heap, if it appears that it helps performance. *)
   let new_lit t =
-    let l = add_term t in
+    let l = Lit.make t in
     insert_var_order (E_lit l)
 
   let new_atom p =
@@ -264,13 +266,13 @@ module Make
   (* increase activity of [v] *)
   let var_bump_activity_aux v =
     v.v_weight <- v.v_weight +. env.var_incr;
-    if v.v_weight > 1e100 then begin
+    if v.v_weight > 1e100 then (
       for i = 0 to (St.nb_elt ()) - 1 do
-        set_elt_weight (St.get_elt i) ((get_elt_weight (St.get_elt i)) *. 1e-100)
+        Elt.set_weight (St.get_elt i) ((Elt.weight (St.get_elt i)) *. 1e-100)
       done;
       env.var_incr <- env.var_incr *. 1e-100;
-    end;
-    let elt = elt_of_var v in
+    );
+    let elt = Elt.of_var v in
     if H.in_heap elt then (
       H.decrease env.order elt
     )
@@ -278,13 +280,13 @@ module Make
   (* increase activity of literal [l] *)
   let lit_bump_activity_aux (l:lit): unit =
     l.l_weight <- l.l_weight +. env.var_incr;
-    if l.l_weight > 1e100 then begin
+    if l.l_weight > 1e100 then (
       for i = 0 to (St.nb_elt ()) - 1 do
-        set_elt_weight (St.get_elt i) ((get_elt_weight (St.get_elt i)) *. 1e-100)
+        Elt.set_weight (St.get_elt i) ((Elt.weight (St.get_elt i)) *. 1e-100)
       done;
       env.var_incr <- env.var_incr *. 1e-100;
-    end;
-    let elt = elt_of_lit l in
+    );
+    let elt = Elt.of_lit l in
     if H.in_heap elt then (
       H.decrease env.order elt
     )
@@ -297,13 +299,13 @@ module Make
   (* increase activity of clause [c] *)
   let clause_bump_activity (c:clause) : unit =
     c.activity <- c.activity +. env.clause_incr;
-    if c.activity > 1e20 then begin
+    if c.activity > 1e20 then (
       for i = 0 to (Vec.size env.clauses_learnt) - 1 do
         (Vec.get env.clauses_learnt i).activity <-
           (Vec.get env.clauses_learnt i).activity *. 1e-20;
       done;
       env.clause_incr <- env.clause_incr *. 1e-20
-    end
+    )
 
   (* Simplification of clauses.
 
@@ -329,20 +331,23 @@ module Make
     let duplicates = ref [] in
     let res = ref [] in
     Array.iter (fun a ->
-        if seen a then duplicates := a :: !duplicates
-        else (mark a; res := a :: !res)
-      ) clause.atoms;
+        if Atom.seen a then duplicates := a :: !duplicates
+        else (
+          Atom.mark a;
+          res := a :: !res
+        ))
+      clause.atoms;
     List.iter
       (fun a ->
-         if seen_both a.var then trivial := true;
-         clear a.var)
+         if Var.seen_both a.var then trivial := true;
+         Var.clear a.var)
       !res;
     if !trivial then
       raise Trivial
     else if !duplicates = [] then
       clause
     else
-      make_clause (fresh_lname ()) !res (History [clause])
+      Clause.make !res (History [clause])
 
   (* Partition literals for new clauses, into:
      - true literals (maybe makes the clause trivial if the lit is proved true at level 0)
@@ -353,20 +358,20 @@ module Make
   *)
   let partition atoms : atom list * clause list =
     let rec partition_aux trues unassigned falses history i =
-      if i >= Array.length atoms then
+      if i >= Array.length atoms then (
         trues @ unassigned @ falses, history
-      else begin
+      ) else (
         let a = atoms.(i) in
-        if a.is_true then
+        if a.is_true then (
           let l = a.var.v_level in
           if l = 0 then
             raise Trivial (* A var true at level 0 gives a trivially true clause *)
           else
             (a :: trues) @ unassigned @ falses @
             (arr_to_list atoms (i + 1)), history
-        else if a.neg.is_true then
+        ) else if a.neg.is_true then (
           let l = a.var.v_level in
-          if l = 0 then begin
+          if l = 0 then (
             match a.var.reason with
             | Some (Bcp cl) ->
               partition_aux trues unassigned falses (cl :: history) (i + 1)
@@ -381,11 +386,13 @@ module Make
             | None | Some Decision -> assert false
             (* The var must have a reason, and it cannot be a decision/assumption,
                since its level is 0. *)
-          end else
+          ) else (
             partition_aux trues unassigned (a::falses) history (i + 1)
-        else
+          )
+        ) else (
           partition_aux trues (a::unassigned) falses history (i + 1)
-      end
+        )
+      )
     in
     partition_aux [] [] [] [] 0
 
@@ -398,9 +405,9 @@ module Make
      i.e we have indeed reached a propagation fixpoint before making
      a new decision *)
   let new_decision_level() =
-    assert (env.th_head = Vec.size env.elt_queue);
-    assert (env.elt_head = Vec.size env.elt_queue);
-    Vec.push env.elt_levels (Vec.size env.elt_queue);
+    assert (env.th_head = Vec.size env.trail);
+    assert (env.elt_head = Vec.size env.trail);
+    Vec.push env.elt_levels (Vec.size env.trail);
     Vec.push env.th_levels (Plugin.current_level ()); (* save the current theory state *)
     ()
 
@@ -411,11 +418,11 @@ module Make
 
   *)
   let attach_clause c =
-    assert (not c.attached);
-    Log.debugf debug (fun k -> k "Attaching %a" St.pp_clause c);
+    assert (not @@ Clause.attached c);
+    Log.debugf debug (fun k -> k "Attaching %a" Clause.debug c);
     Vec.push c.atoms.(0).neg.watched c;
     Vec.push c.atoms.(1).neg.watched c;
-    c.attached <- true;
+    Clause.set_attached c true;
     ()
 
   (* Backtracking.
@@ -425,9 +432,9 @@ module Make
   let cancel_until lvl =
     assert (lvl >= base_level ());
     (* Nothing to do if we try to backtrack to a non-existent level. *)
-    if decision_level () <= lvl then
+    if decision_level () <= lvl then (
       Log.debugf debug (fun k -> k "Already at level <= %d" lvl)
-    else begin
+    ) else (
       Log.debugf info (fun k -> k "Backtracking to lvl %d" lvl);
       (* We set the head of the solver and theory queue to what it was. *)
       let head = ref (Vec.get env.elt_levels lvl) in
@@ -435,29 +442,29 @@ module Make
       env.th_head <- !head;
       (* Now we need to cleanup the vars that are not valid anymore
          (i.e to the right of elt_head in the queue. *)
-      for c = env.elt_head to Vec.size env.elt_queue - 1 do
-        match (Vec.get env.elt_queue c) with
+      for c = env.elt_head to Vec.size env.trail - 1 do
+        match (Vec.get env.trail c) with
         (* A literal is unassigned, we nedd to add it back to
            the heap of potentially assignable literals, unless it has
            a level lower than [lvl], in which case we just move it back. *)
         | Lit l ->
-          if l.l_level <= lvl then begin
-            Vec.set env.elt_queue !head (of_lit l);
+          if l.l_level <= lvl then (
+            Vec.set env.trail !head (Trail_elt.of_lit l);
             head := !head + 1
-          end else begin
+          ) else (
             l.assigned <- None;
             l.l_level <- -1;
-            insert_var_order (elt_of_lit l)
-          end
+            insert_var_order (Elt.of_lit l)
+          )
         (* A variable is not true/false anymore, one of two things can happen: *)
         | Atom a ->
-          if a.var.v_level <= lvl then begin
+          if a.var.v_level <= lvl then (
             (* It is a late propagation, which has a level
                lower than where we backtrack, so we just move it to the head
                of the queue, to be propagated again. *)
-            Vec.set env.elt_queue !head (of_atom a);
+            Vec.set env.trail !head (Trail_elt.of_atom a);
             head := !head + 1
-          end else begin
+          ) else (
             (* it is a result of bolean propagation, or a semantic propagation
                with a level higher than the level to which we backtrack,
                in that case, we simply unset its value and reinsert it into the heap. *)
@@ -465,23 +472,23 @@ module Make
             a.neg.is_true <- false;
             a.var.v_level <- -1;
             a.var.reason <- None;
-            insert_var_order (elt_of_var a.var)
-          end
+            insert_var_order (Elt.of_var a.var)
+          )
       done;
       (* Recover the right theory state. *)
       Plugin.backtrack (Vec.get env.th_levels lvl);
       (* Resize the vectors according to their new size. *)
-      Vec.shrink env.elt_queue !head;
+      Vec.shrink env.trail !head;
       Vec.shrink env.elt_levels lvl;
       Vec.shrink env.th_levels lvl;
-    end;
+    );
     assert (Vec.size env.elt_levels = Vec.size env.th_levels);
     ()
 
   (* Unsatisfiability is signaled through an exception, since it can happen
      in multiple places (adding new clauses, or solving for instance). *)
   let report_unsat confl : _ =
-    Log.debugf info (fun k -> k "@[Unsat conflict: %a@]" St.pp_clause confl);
+    Log.debugf info (fun k -> k "@[Unsat conflict: %a@]" Clause.debug confl);
     env.unsat_conflict <- Some confl;
     raise Unsat
 
@@ -505,18 +512,18 @@ module Make
                with only one formula (which is [a]). So we explicitly create that clause
                and set it as the cause for the propagation of [a], that way we can
                rebuild the whole resolution tree when we want to prove [a]. *)
-            let c' = make_clause (fresh_lname ()) l (History (cl :: history)) in
+            let c' = Clause.make l (History (cl :: history)) in
             Log.debugf debug
-              (fun k -> k "Simplified reason: @[<v>%a@,%a@]" St.pp_clause cl St.pp_clause c');
+              (fun k -> k "Simplified reason: @[<v>%a@,%a@]" Clause.debug cl Clause.debug c');
             Bcp c'
           )
         | _ ->
           Log.debugf error
             (fun k ->
                k "@[<v 2>Failed at reason simplification:@,%a@,%a@]"
-                 (Vec.print ~sep:"" St.pp_atom)
-                 (Vec.from_list l St.dummy_atom)
-                 St.pp_clause cl);
+                 (Vec.print ~sep:"" Atom.debug)
+                 (Vec.from_list l Atom.dummy)
+                 Clause.debug cl);
           assert false
       end
     | r -> r
@@ -524,10 +531,10 @@ module Make
   (* Boolean propagation.
      Wrapper function for adding a new propagated formula. *)
   let enqueue_bool a ~level:lvl reason : unit =
-    if a.neg.is_true then begin
-      Log.debugf error (fun k->k "Trying to enqueue a false literal: %a" St.pp_atom a);
+    if a.neg.is_true then (
+      Log.debugf error (fun k->k "Trying to enqueue a false literal: %a" Atom.debug a);
       assert false
-    end;
+    );
     assert (not a.is_true && a.var.v_level < 0 &&
             a.var.reason = None && lvl >= 0);
     let reason =
@@ -537,34 +544,35 @@ module Make
     a.is_true <- true;
     a.var.v_level <- lvl;
     a.var.reason <- Some reason;
-    Vec.push env.elt_queue (of_atom a);
+    Vec.push env.trail (Trail_elt.of_atom a);
     Log.debugf debug
-      (fun k->k "Enqueue (%d): %a" (Vec.size env.elt_queue) pp_atom a)
+      (fun k->k "Enqueue (%d): %a" (Vec.size env.trail) Atom.debug a);
+    ()
 
   let enqueue_semantic a terms =
-    if a.is_true then ()
-    else begin
-      let l = List.map St.add_term terms in
+    if not a.is_true then (
+      let l = List.map Lit.make terms in
       let lvl = List.fold_left (fun acc {l_level; _} ->
           assert (l_level > 0); max acc l_level) 0 l in
       H.grow_to_at_least env.order (St.nb_elt ());
       enqueue_bool a ~level:lvl Semantic
-    end
+    )
 
   (* MCsat semantic assignment *)
   let enqueue_assign l value lvl =
     match l.assigned with
     | Some _ ->
       Log.debugf error
-        (fun k -> k "Trying to assign an already assigned literal: %a" St.pp_lit l);
+        (fun k -> k "Trying to assign an already assigned literal: %a" Lit.debug l);
       assert false
     | None ->
       assert (l.l_level < 0);
       l.assigned <- Some value;
       l.l_level <- lvl;
-      Vec.push env.elt_queue (of_lit l);
+      Vec.push env.trail (Trail_elt.of_lit l);
       Log.debugf debug
-        (fun k -> k "Enqueue (%d): %a" (Vec.size env.elt_queue) pp_lit l)
+        (fun k -> k "Enqueue (%d): %a" (Vec.size env.trail) Lit.debug l);
+      ()
 
   (* swap elements of array *)
   let[@inline] swap_arr a i j =
@@ -574,11 +582,17 @@ module Make
       a.(j) <- tmp;
     )
 
+  let[@inline] put_high_level_atoms_first (arr:atom array) : unit =
+    Array.sort
+      (fun a b -> compare b.var.v_level a.var.v_level)
+      arr
+
+  (* FIXME
   (* move atoms assigned at high levels first *)
   let[@inline] put_high_level_atoms_first (arr:atom array) : unit =
     Array.iteri
       (fun i a ->
-         if i>0 && a.var.v_level > arr.(0).var.v_level then (
+         if i>0 && Atom.level a > Atom.level arr.(0) then (
            (* move first to second, [i]-th to first, second to [i] *)
            if i=1 then (
              swap_arr arr 0 1;
@@ -588,10 +602,11 @@ module Make
              arr.(0) <- arr.(i);
              arr.(i) <- tmp;
            );
-         ) else if i>1 && a.var.v_level > arr.(1).var.v_level then (
+         ) else if i>1 && Atom.level a > Atom.level arr.(1) then (
            swap_arr arr 1 i;
          ))
       arr
+     *)
 
   (* evaluate an atom for MCsat, if it's not assigned
      by boolean propagation/decision *)
@@ -636,7 +651,7 @@ module Make
   }
 
   let get_atom i =
-    match Vec.get env.elt_queue i with
+    match Vec.get env.trail i with
     | Lit _ -> assert false | Atom x -> x
 
   (* conflict analysis for SAT
@@ -650,20 +665,20 @@ module Make
     let blevel = ref 0 in
     let seen   = ref [] in
     let c      = ref (Some c_clause) in
-    let tr_ind = ref (Vec.size env.elt_queue - 1) in
+    let tr_ind = ref (Vec.size env.trail - 1) in
     let history = ref [] in
     assert (decision_level () > 0);
     let conflict_level =
       Array.fold_left (fun acc p -> max acc p.var.v_level) 0 c_clause.atoms
     in
     Log.debugf debug
-      (fun k -> k "Analyzing conflict (%d): %a" conflict_level St.pp_clause c_clause);
+      (fun k -> k "Analyzing conflict (%d): %a" conflict_level Clause.debug c_clause);
     while !cond do
       begin match !c with
         | None ->
           Log.debug debug "  skipping resolution for semantic propagation"
         | Some clause ->
-          Log.debugf debug (fun k->k"  Resolving clause: %a"  St.pp_clause clause);
+          Log.debugf debug (fun k->k"  Resolving clause: %a"  Clause.debug clause);
           begin match clause.cpremise with
             | History _ -> clause_bump_activity clause
             | Hyp | Local | Lemma _ -> ()
@@ -673,36 +688,36 @@ module Make
           for j = 0 to Array.length clause.atoms - 1 do
             let q = clause.atoms.(j) in
             assert (q.is_true || q.neg.is_true && q.var.v_level >= 0); (* unsure? *)
-            if q.var.v_level <= 0 then begin
+            if q.var.v_level <= 0 then (
               assert (q.neg.is_true);
               match q.var.reason with
               | Some Bcp cl -> history := cl :: !history
               | _ -> assert false
-            end;
-            if not (seen_both q.var) then (
-              mark q;
-              mark q.neg;
+            );
+            if not (Var.seen_both q.var) then (
+              Atom.mark q;
+              Atom.mark q.neg;
               seen := q :: !seen;
-              if q.var.v_level > 0 then begin
+              if q.var.v_level > 0 then (
                 var_bump_activity q.var;
-                if q.var.v_level >= conflict_level then begin
+                if q.var.v_level >= conflict_level then (
                   incr pathC;
-                end else begin
+                ) else (
                   learnt := q :: !learnt;
                   blevel := max !blevel q.var.v_level
-                end
-              end
+                )
+              )
             )
           done
       end;
 
       (* look for the next node to expand *)
       while
-        let a = Vec.get env.elt_queue !tr_ind in
-        Log.debugf debug (fun k -> k "  looking at: %a" St.pp a);
+        let a = Vec.get env.trail !tr_ind in
+        Log.debugf debug (fun k -> k "  looking at: %a" Trail_elt.debug a);
         match a with
         | Atom q ->
-          (not (seen_both q.var)) ||
+          (not (Var.seen_both q.var)) ||
           (q.var.v_level < conflict_level)
         | Lit _ -> true
       do
@@ -725,7 +740,7 @@ module Make
         c := Some cl
       | _ -> assert false
     done;
-    List.iter (fun q -> clear q.var) !seen;
+    List.iter (fun q -> Var.clear q.var) !seen;
     let l = List.fast_sort (fun p q -> compare q.var.v_level p.var.v_level) !learnt in
     let level, is_uip = backtrack_lvl l in
     { cr_backtrack_lvl = level;
@@ -748,26 +763,24 @@ module Make
       | [] -> assert false
       | [fuip] ->
         assert (cr.cr_backtrack_lvl = 0);
-        if fuip.neg.is_true then
+        if fuip.neg.is_true then (
           report_unsat confl
-        else begin
-          let name = fresh_lname () in
-          let uclause = make_clause name cr.cr_learnt (History cr.cr_history) in
+        ) else (
+          let uclause = Clause.make cr.cr_learnt (History cr.cr_history) in
           Vec.push env.clauses_learnt uclause;
           (* no need to attach [uclause], it is true at level 0 *)
           enqueue_bool fuip ~level:0 (Bcp uclause)
-        end
+        )
       | fuip :: _ ->
-        let name = fresh_lname () in
-        let lclause = make_clause name cr.cr_learnt (History cr.cr_history) in
+        let lclause = Clause.make cr.cr_learnt (History cr.cr_history) in
         Vec.push env.clauses_learnt lclause;
         attach_clause lclause;
         clause_bump_activity lclause;
-        if cr.cr_is_uip then
+        if cr.cr_is_uip then (
           enqueue_bool fuip ~level:cr.cr_backtrack_lvl (Bcp lclause)
-        else begin
+        ) else (
           env.next_decision <- Some fuip.neg
-        end
+        )
     end;
     var_decay_activity ();
     clause_decay_activity ()
@@ -778,7 +791,7 @@ module Make
      - report unsat if conflict at level 0
   *)
   let add_boolean_conflict (confl:clause): unit =
-    Log.debugf info (fun k -> k "Boolean conflict: %a" St.pp_clause confl);
+    Log.debugf info (fun k -> k "Boolean conflict: %a" Clause.debug confl);
     env.next_decision <- None;
     env.conflicts <- env.conflicts + 1;
     assert (decision_level() >= base_level ());
@@ -799,14 +812,14 @@ module Make
   (* Add a new clause, simplifying, propagating, and backtracking if
      the clause is false in the current trail *)
   let add_clause (init:clause) : unit =
-    Log.debugf debug (fun k -> k "Adding clause: @[<hov>%a@]" St.pp_clause init);
+    Log.debugf debug (fun k -> k "Adding clause: @[<hov>%a@]" Clause.debug init);
     (* Insertion of new lits is done before simplification. Indeed, else a lit in a
        trivial clause could end up being not decided on, which is a bug. *)
-    Array.iter (fun x -> insert_var_order (elt_of_var x.var)) init.atoms;
+    Array.iter (fun x -> insert_var_order (Elt.of_var x.var)) init.atoms;
     let vec = clause_vector init in
     try
       let c = eliminate_doublons init in
-      Log.debugf debug (fun k -> k "Doublons eliminated: %a" St.pp_clause c);
+      Log.debugf debug (fun k -> k "Doublons eliminated: %a" Clause.debug c);
       let atoms, history = partition c.atoms in
       let clause =
         if history = []
@@ -815,9 +828,9 @@ module Make
           List.iteri (fun i a -> c.atoms.(i) <- a) atoms;
           c
         )
-        else make_clause (fresh_name ()) atoms (History (c :: history))
+        else Clause.make atoms (History (c :: history))
       in
-      Log.debugf info (fun k->k "New clause: @[<hov>%a@]" St.pp_clause clause);
+      Log.debugf info (fun k->k "New clause: @[<hov>%a@]" Clause.debug clause);
       match atoms with
       | [] ->
         (* Report_unsat will raise, and the current clause will be lost if we do not
@@ -827,14 +840,14 @@ module Make
         report_unsat clause
       | [a]   ->
         cancel_until (base_level ());
-        if a.neg.is_true then begin
+        if a.neg.is_true then (
           (* Since we cannot propagate the atom [a], in order to not lose
              the information that [a] must be true, we add clause to the list
              of clauses to add, so that it will be e-examined later. *)
           Log.debug debug "Unit clause, adding to clauses to add";
           Stack.push clause env.clauses_to_add;
           report_unsat clause
-        end else if a.is_true then begin
+        ) else if a.is_true then (
           (* If the atom is already true, then it should be because of a local hyp.
              However it means we can't propagate it at level 0. In order to not lose
              that information, we store the clause in a stack of clauses that we will
@@ -843,30 +856,30 @@ module Make
           assert (0 < a.var.v_level && a.var.v_level <= base_level ());
           Stack.push clause env.clauses_root;
           ()
-        end else begin
-          Log.debugf debug (fun k->k "Unit clause, propagating: %a" St.pp_atom a);
+        ) else (
+          Log.debugf debug (fun k->k "Unit clause, propagating: %a" Atom.debug a);
           Vec.push vec clause;
           enqueue_bool a ~level:0 (Bcp clause)
-        end
+        )
       | a::b::_ ->
         Vec.push vec clause;
-        if a.neg.is_true then begin
+        if a.neg.is_true then (
           (* Atoms need to be sorted in decreasing order of decision level,
              or we might watch the wrong literals. *)
           put_high_level_atoms_first clause.atoms;
           attach_clause clause;
           add_boolean_conflict clause
-        end else begin
+        ) else (
           attach_clause clause;
-          if b.neg.is_true && not a.is_true && not a.neg.is_true then begin
+          if b.neg.is_true && not a.is_true && not a.neg.is_true then (
             let lvl = List.fold_left (fun m a -> max m a.var.v_level) 0 atoms in
             cancel_until (max lvl (base_level ()));
             enqueue_bool a ~level:lvl (Bcp clause)
-          end
-        end
+          )
+        )
     with Trivial ->
       Vec.push vec init;
-      Log.debugf info (fun k->k "Trivial clause ignored : @[%a@]" St.pp_clause init)
+      Log.debugf info (fun k->k "Trivial clause ignored : @[%a@]" Clause.debug init)
 
   let flush_clauses () =
     if not (Stack.is_empty env.clauses_to_add) then begin
@@ -900,13 +913,13 @@ module Make
       atoms.(1) <- first
     ) else assert (a.neg == atoms.(1));
     let first = atoms.(0) in
-    if first.is_true
+    if Atom.is_true first
     then Watch_kept (* true clause, keep it in watched *)
     else (
       try (* look for another watch lit *)
         for k = 2 to Array.length atoms - 1 do
           let ak = atoms.(k) in
-          if not (ak.neg.is_true) then begin
+          if not (ak.neg.is_true) then (
             (* watch lit found: update and exit *)
             atoms.(1) <- ak;
             atoms.(k) <- a.neg;
@@ -915,22 +928,22 @@ module Make
             assert (Vec.get a.watched i == c);
             Vec.fast_remove a.watched i;
             raise Exit
-          end
+          )
         done;
         (* no watch lit found *)
-        if first.neg.is_true then begin
+        if first.neg.is_true then (
           (* clause is false *)
-          env.elt_head <- Vec.size env.elt_queue;
+          env.elt_head <- Vec.size env.trail;
           raise (Conflict c)
-        end else begin
+        ) else (
           match th_eval first with
           | None -> (* clause is unit, keep the same watches, but propagate *)
             enqueue_bool first ~level:(decision_level ()) (Bcp c)
           | Some true -> ()
           | Some false ->
-            env.elt_head <- Vec.size env.elt_queue;
+            env.elt_head <- Vec.size env.trail;
             raise (Conflict c)
-        end;
+        );
         Watch_kept
       with Exit ->
         Watch_removed
@@ -948,7 +961,7 @@ module Make
           if i >= Vec.size watched then ()
           else (
             let c = Vec.get watched i in
-            assert c.attached;
+            assert (Clause.attached c);
             let j = match propagate_in_clause a c i with
               | Watch_kept -> i+1
               | Watch_removed -> i (* clause at this index changed *)
@@ -970,7 +983,7 @@ module Make
     a
 
   let slice_get i =
-    match Vec.get env.elt_queue i with
+    match Vec.get env.trail i with
     | Atom a ->
       Plugin_intf.Lit a.lit
     | Lit {term; assigned = Some v; _} ->
@@ -979,8 +992,8 @@ module Make
 
   let slice_push (l:formula list) (lemma:proof): unit =
     let atoms = List.rev_map create_atom l in
-    let c = make_clause (fresh_tname ()) atoms (Lemma lemma) in
-    Log.debugf info (fun k->k "Pushing clause %a" St.pp_clause c);
+    let c = Clause.make atoms (Lemma lemma) in
+    Log.debugf info (fun k->k "Pushing clause %a" Clause.debug c);
     Stack.push c env.clauses_to_add
 
   let slice_propagate f = function
@@ -989,24 +1002,24 @@ module Make
       enqueue_semantic a l
     | Plugin_intf.Consequence (causes, proof) ->
       let l = List.rev_map atom causes in
-      if List.for_all (fun a -> a.is_true) l then
+      if List.for_all (fun a -> a.is_true) l then (
         let p = atom f in
-        let c = make_clause (fresh_tname ())
-            (p :: List.map (fun a -> a.neg) l) (Lemma proof) in
+        let c = Clause.make (p :: List.map Atom.neg l) (Lemma proof) in
         if p.is_true then ()
-        else if p.neg.is_true then
+        else if p.neg.is_true then (
           Stack.push c env.clauses_to_add
-        else begin
+        ) else (
           H.grow_to_at_least env.order (St.nb_elt ());
           insert_subterms_order p.var;
           enqueue_bool p ~level:(decision_level ()) (Bcp c)
-        end
-      else
-        raise (Invalid_argument "Msat.Internal.slice_propagate")
+        )
+      ) else (
+        invalid_arg "Msat.Internal.slice_propagate"
+      )
 
   let current_slice (): (_,_,_) Plugin_intf.slice = {
     Plugin_intf.start = env.th_head;
-    length = (Vec.size env.elt_queue) - env.th_head;
+    length = (Vec.size env.trail) - env.th_head;
     get = slice_get;
     push = slice_push;
     propagate = slice_propagate;
@@ -1015,7 +1028,7 @@ module Make
   (* full slice, for [if_sat] final check *)
   let full_slice () : (_,_,_) Plugin_intf.slice = {
     Plugin_intf.start = 0;
-    length = Vec.size env.elt_queue;
+    length = Vec.size env.trail;
     get = slice_get;
     push = slice_push;
     propagate = (fun _ -> assert false);
@@ -1025,11 +1038,11 @@ module Make
      need to inform the theory of those assumptions, so it can do its job.
      @return the conflict clause, if the theory detects unsatisfiability *)
   let rec theory_propagate (): clause option =
-    assert (env.elt_head = Vec.size env.elt_queue);
+    assert (env.elt_head = Vec.size env.trail);
     assert (env.th_head <= env.elt_head);
-    if env.th_head = env.elt_head then
+    if env.th_head = env.elt_head then (
       None (* fixpoint/no propagation *)
-    else begin
+    ) else (
       let slice = current_slice () in
       env.th_head <- env.elt_head; (* catch up *)
       match Plugin.assume slice with
@@ -1039,10 +1052,10 @@ module Make
         (* conflict *)
         let l = List.rev_map create_atom l in
         H.grow_to_at_least env.order (St.nb_elt ());
-        List.iter (fun a -> insert_var_order (elt_of_var a.var)) l;
-        let c = St.make_clause (St.fresh_tname ()) l (Lemma p) in
+        List.iter (fun a -> insert_var_order (Elt.of_var a.var)) l;
+        let c = St.Clause.make l (Lemma p) in
         Some c
-    end
+    )
 
   (* fixpoint between boolean propagation and theory propagation
      @return a conflict clause, if any *)
@@ -1050,14 +1063,14 @@ module Make
     (* First, treat the stack of lemmas added by the theory, if any *)
     flush_clauses ();
     (* Now, check that the situation is sane *)
-    assert (env.elt_head <= Vec.size env.elt_queue);
-    if env.elt_head = Vec.size env.elt_queue then
+    assert (env.elt_head <= Vec.size env.trail);
+    if env.elt_head = Vec.size env.trail then
       theory_propagate ()
     else begin
       let num_props = ref 0 in
       let res = ref None in
-      while env.elt_head < Vec.size env.elt_queue do
-        begin match Vec.get env.elt_queue env.elt_head with
+      while env.elt_head < Vec.size env.trail do
+        begin match Vec.get env.trail env.elt_head with
           | Lit _ -> ()
           | Atom a ->
             incr num_props;
@@ -1080,10 +1093,10 @@ module Make
   (* Decide on a new literal, and enqueue it into the trail *)
   let rec pick_branch_aux atom: unit =
     let v = atom.var in
-    if v.v_level >= 0 then begin
+    if v.v_level >= 0 then (
       assert (v.pa.is_true || v.na.is_true);
       pick_branch_lit ()
-    end else match Plugin.eval atom.lit with
+    ) else match Plugin.eval atom.lit with
       | Plugin_intf.Unknown ->
         env.decisions <- env.decisions + 1;
         new_decision_level();
@@ -1099,22 +1112,20 @@ module Make
       env.next_decision <- None;
       pick_branch_aux atom
     | None ->
-      begin try
-          begin match H.remove_min env.order with
-            | E_lit l ->
-              if l.l_level >= 0 then
-                pick_branch_lit ()
-              else begin
-                let value = Plugin.assign l.term in
-                env.decisions <- env.decisions + 1;
-                new_decision_level();
-                let current_level = decision_level () in
-                enqueue_assign l value current_level
-              end
-            | E_var v ->
-              pick_branch_aux v.pa
-          end
-        with Not_found -> raise Sat
+      begin match H.remove_min env.order with
+        | E_lit l ->
+          if Lit.level l >= 0 then
+            pick_branch_lit ()
+          else (
+            let value = Plugin.assign l.term in
+            env.decisions <- env.decisions + 1;
+            new_decision_level();
+            let current_level = decision_level () in
+            enqueue_assign l value current_level
+          )
+        | E_var v ->
+          pick_branch_aux v.pa
+        | exception Not_found -> raise Sat
       end
 
   (* do some amount of search, until the number of conflicts or clause learnt
@@ -1130,32 +1141,32 @@ module Make
            might 'forget' the initial conflict clause, and only add the
            analyzed backtrack clause. So in those case, we use add_clause
            to make sure the initial conflict clause is also added. *)
-        if confl.attached then
+        if Clause.attached confl then
           add_boolean_conflict confl
         else
           add_clause confl
 
       | None -> (* No Conflict *)
-        assert (env.elt_head = Vec.size env.elt_queue);
+        assert (env.elt_head = Vec.size env.trail);
         assert (env.elt_head = env.th_head);
-        if Vec.size env.elt_queue = St.nb_elt ()
+        if Vec.size env.trail = St.nb_elt ()
         then raise Sat;
-        if n_of_conflicts > 0 && !conflictC >= n_of_conflicts then begin
+        if n_of_conflicts > 0 && !conflictC >= n_of_conflicts then (
           Log.debug info "Restarting...";
           cancel_until (base_level ());
           raise Restart
-        end;
+        );
         (* if decision_level() = 0 then simplify (); *)
 
         if n_of_learnts >= 0 &&
-           Vec.size env.clauses_learnt - Vec.size env.elt_queue >= n_of_learnts
+           Vec.size env.clauses_learnt - Vec.size env.trail >= n_of_learnts
         then reduce_db();
 
         pick_branch_lit ()
     done
 
   let eval_level lit =
-    let var, negated = make_boolean_var lit in
+    let var, negated = Var.make lit in
     if not var.pa.is_true && not var.na.is_true
     then raise UndecidedLit
     else assert (var.v_level >= 0);
@@ -1176,7 +1187,7 @@ module Make
       (fun acc e -> match e with
          | Lit v -> (v.term, opt v.assigned)  :: acc
          | Atom _ -> acc)
-      [] env.elt_queue
+      [] env.trail
 
   (* fixpoint of propagation and decisions until a model is found, or a
      conflict is reached *)
@@ -1194,13 +1205,13 @@ module Make
             n_of_conflicts := !n_of_conflicts *. env.restart_inc;
             n_of_learnts   := !n_of_learnts *. env.learntsize_inc
           | Sat ->
-            assert (env.elt_head = Vec.size env.elt_queue);
+            assert (env.elt_head = Vec.size env.trail);
             begin match Plugin.if_sat (full_slice ()) with
               | Plugin_intf.Sat -> ()
               | Plugin_intf.Unsat (l, p) ->
                 let atoms = List.rev_map create_atom l in
-                let c = make_clause (fresh_tname ()) atoms (Lemma p) in
-                Log.debugf info (fun k -> k "Theory conflict clause: %a" St.pp_clause c);
+                let c = Clause.make atoms (Lemma p) in
+                Log.debugf info (fun k -> k "Theory conflict clause: %a" Clause.debug c);
                 Stack.push c env.clauses_to_add
             end;
             if Stack.is_empty env.clauses_to_add then raise Sat
@@ -1212,8 +1223,8 @@ module Make
     List.iter
       (fun l ->
          let atoms = List.rev_map atom l in
-         let c = make_clause ?tag (fresh_hname ()) atoms Hyp in
-         Log.debugf debug (fun k -> k "Assuming clause: @[<hov 2>%a@]" pp_clause c);
+         let c = Clause.make ?tag atoms Hyp in
+         Log.debugf debug (fun k -> k "Assuming clause: @[<hov 2>%a@]" Clause.debug c);
          Stack.push c env.clauses_to_add)
       cnf
 
@@ -1223,13 +1234,14 @@ module Make
     cancel_until (base_level ());
     Log.debugf debug
       (fun k -> k "@[<v>Status:@,@[<hov 2>trail: %d - %d@,%a@]"
-          env.elt_head env.th_head (Vec.print ~sep:"" St.pp) env.elt_queue);
+          env.elt_head env.th_head (Vec.print ~sep:"" Trail_elt.debug) env.trail);
     begin match propagate () with
       | Some confl ->
         report_unsat confl
       | None ->
         Log.debugf debug
-          (fun k -> k "@[<v>Current trail:@,@[<hov>%a@]@]" (Vec.print ~sep:"" St.pp) env.elt_queue);
+          (fun k -> k "@[<v>Current trail:@,@[<hov>%a@]@]"
+              (Vec.print ~sep:"" Trail_elt.debug) env.trail);
         Log.debug info "Creating new user level";
         new_decision_level ();
         Vec.push env.user_levels (Vec.size env.clauses_temp);
@@ -1260,24 +1272,24 @@ module Make
   let local l =
     let aux lit =
       let a = atom lit in
-      Log.debugf info (fun k-> k "Local assumption: @[%a@]" pp_atom a);
+      Log.debugf info (fun k-> k "Local assumption: @[%a@]" Atom.debug a);
       assert (decision_level () = base_level ());
-      if a.is_true then ()
-      else
-        let c = make_clause (fresh_hname ()) [a] Local in
-        Log.debugf debug (fun k -> k "Temp clause: @[%a@]" pp_clause c);
+      if not a.is_true then (
+        let c = Clause.make [a] Local in
+        Log.debugf debug (fun k -> k "Temp clause: @[%a@]" Clause.debug c);
         Vec.push env.clauses_temp c;
-        if a.neg.is_true then begin
+        if a.neg.is_true then (
           (* conflict between assumptions: UNSAT *)
           report_unsat c;
-        end else begin
+        ) else (
           (* Grow the heap, because when the lit is backtracked,
              it will be added to the heap. *)
           H.grow_to_at_least env.order (St.nb_elt ());
           (* make a decision, propagate *)
           let level = decision_level() in
           enqueue_bool a ~level (Bcp c);
-        end
+        )
+      )
     in
     assert (base_level () > 0);
     match env.unsat_conflict with
@@ -1295,11 +1307,11 @@ module Make
         else if a.neg.is_true then false
         else raise UndecidedLit) c.atoms in
     let res = Array.exists (fun x -> x) tmp in
-    if not res then begin
+    if not res then (
       Log.debugf debug
-        (fun k -> k "Clause not satisfied: @[<hov>%a@]" St.pp_clause c);
+        (fun k -> k "Clause not satisfied: @[<hov>%a@]" Clause.debug c);
       false
-    end else
+    ) else
       true
 
   let check_vec v =
@@ -1327,7 +1339,7 @@ module Make
 
   let temp () = env.clauses_temp
 
-  let trail () = env.elt_queue
+  let trail () = env.trail
 
 end
 
diff --git a/src/core/Internal.mli b/src/core/Internal.mli
index ca0aef17..bdbbb29e 100644
--- a/src/core/Internal.mli
+++ b/src/core/Internal.mli
@@ -92,7 +92,7 @@ module Make
       These functions expose some internal data stored by the solver, as such
       great care should be taken to ensure not to mess with the values returned. *)
 
-  val trail : unit -> St.t Vec.t
+  val trail : unit -> St.trail_elt Vec.t
   (** Returns the current trail.
       *DO NOT MUTATE* *)
 
diff --git a/src/core/Res.ml b/src/core/Res.ml
index 5d9f5e26..f164b940 100644
--- a/src/core/Res.ml
+++ b/src/core/Res.ml
@@ -24,11 +24,10 @@ module Make(St : Solver_types.S) = struct
   let info = 10
   let debug = 80
 
-  (* Misc functions *)
   let equal_atoms a b = St.(a.aid) = St.(b.aid)
   let compare_atoms a b = Pervasives.compare St.(a.aid) St.(b.aid)
 
-  let print_clause = St.pp_clause
+  let print_clause = St.Clause.pp
 
   let merge = List.merge compare_atoms
 
@@ -52,19 +51,19 @@ module Make(St : Solver_types.S) = struct
     resolved, List.rev new_clause
 
   (* Compute the set of doublons of a clause *)
-  let list c = List.sort compare_atoms (Array.to_list St.(c.atoms))
+  let list c = List.sort St.Atom.compare (Array.to_list St.(c.atoms))
 
   let analyze cl =
     let rec aux duplicates free = function
       | [] -> duplicates, free
       | [ x ] -> duplicates, x :: free
       | x :: ((y :: r) as l) ->
-        if equal_atoms x y then
+        if x == y then
           count duplicates (x :: free) x [y] r
         else
           aux duplicates (x :: free) l
     and count duplicates free x acc = function
-      | (y :: r) when equal_atoms x y ->
+      | (y :: r) when x == y ->
         count duplicates free x (y :: acc) r
       | l ->
         aux (acc :: duplicates) free l
@@ -96,7 +95,8 @@ module Make(St : Solver_types.S) = struct
   let cmp_cl c d =
     let rec aux = function
       | [], [] -> 0
-      | a :: r, a' :: r' -> begin match compare_atoms a a' with
+      | a :: r, a' :: r' ->
+        begin match compare_atoms a a' with
           | 0 -> aux (r, r')
           | x -> x
         end
@@ -117,32 +117,32 @@ module Make(St : Solver_types.S) = struct
     assert St.(a.var.v_level >= 0);
     match St.(a.var.reason) with
     | Some St.Bcp c ->
-      Log.debugf debug (fun k->k "Analysing: @[%a@ %a@]" St.pp_atom a St.pp_clause c);
-      if Array.length c.St.atoms = 1 then begin
-        Log.debugf debug (fun k -> k "Old reason: @[%a@]" St.pp_atom a);
+      Log.debugf debug (fun k->k "Analysing: @[%a@ %a@]" St.Atom.debug a St.Clause.debug c);
+      if Array.length c.St.atoms = 1 then (
+        Log.debugf debug (fun k -> k "Old reason: @[%a@]" St.Atom.debug a);
         c
-      end else begin
+      ) else (
         assert (a.St.neg.St.is_true);
         let r = St.History (c :: (Array.fold_left aux [] c.St.atoms)) in
-        let c' = St.make_clause (fresh_pcl_name ()) [a.St.neg] r in
+        let c' = St.Clause.make [a.St.neg] r in
         a.St.var.St.reason <- Some St.(Bcp c');
         Log.debugf debug
-          (fun k -> k "New reason: @[%a@ %a@]" St.pp_atom a St.pp_clause c');
+          (fun k -> k "New reason: @[%a@ %a@]" St.Atom.debug a St.Clause.debug c');
         c'
-      end
+      )
     | _ ->
-      Log.debugf error (fun k -> k "Error while proving atom %a" St.pp_atom a);
+      Log.debugf error (fun k -> k "Error while proving atom %a" St.Atom.debug a);
       raise (Resolution_error "Cannot prove atom")
 
   let prove_unsat conflict =
     if Array.length conflict.St.atoms = 0 then conflict
-    else begin
-      Log.debugf info (fun k -> k "Proving unsat from: @[%a@]" St.pp_clause conflict);
+    else (
+      Log.debugf info (fun k -> k "Proving unsat from: @[%a@]" St.Clause.debug conflict);
       let l = Array.fold_left (fun acc a -> set_atom_proof a :: acc) [] conflict.St.atoms in
-      let res = St.make_clause (fresh_pcl_name ()) [] (St.History (conflict :: l)) in
-      Log.debugf info (fun k -> k "Proof found: @[%a@]" St.pp_clause res);
+      let res = St.Clause.make [] (St.History (conflict :: l)) in
+      Log.debugf info (fun k -> k "Proof found: @[%a@]" St.Clause.debug res);
       res
-    end
+    )
 
   let prove_atom a =
     if St.(a.is_true && a.var.v_level = 0) then
@@ -166,27 +166,26 @@ module Make(St : Solver_types.S) = struct
   let rec chain_res (c, cl) = function
     | d :: r ->
       Log.debugf debug
-        (fun k -> k "  Resolving clauses : @[%a@\n%a@]" St.pp_clause c St.pp_clause d);
+        (fun k -> k "  Resolving clauses : @[%a@\n%a@]" St.Clause.debug c St.Clause.debug d);
       let dl = to_list d in
       begin match resolve (merge cl dl) with
         | [ a ], l ->
           begin match r with
             | [] -> (l, c, d, a)
             | _ ->
-              let new_clause = St.make_clause (fresh_pcl_name ())
-                  l (St.History [c; d]) in
+              let new_clause = St.Clause.make l (St.History [c; d]) in
               chain_res (new_clause, l) r
           end
         | _ ->
           Log.debugf error
-            (fun k -> k "While resolving clauses:@[<hov>%a@\n%a@]" St.pp_clause c St.pp_clause d);
+            (fun k -> k "While resolving clauses:@[<hov>%a@\n%a@]" St.Clause.debug c St.Clause.debug d);
           raise (Resolution_error "Clause mismatch")
       end
     | _ ->
       raise (Resolution_error "Bad history")
 
   let expand conclusion =
-    Log.debugf debug (fun k -> k "Expanding : @[%a@]" St.pp_clause conclusion);
+    Log.debugf debug (fun k -> k "Expanding : @[%a@]" St.Clause.debug conclusion);
     match conclusion.St.cpremise with
     | St.Lemma l ->
       {conclusion; step = Lemma l; }
@@ -195,7 +194,7 @@ module Make(St : Solver_types.S) = struct
     | St.Local ->
       { conclusion; step = Assumption; }
     | St.History [] ->
-      Log.debugf error (fun k -> k "Empty history for clause: %a" St.pp_clause conclusion);
+      Log.debugf error (fun k -> k "Empty history for clause: %a" St.Clause.debug conclusion);
       raise (Resolution_error "Empty history")
     | St.History [ c ] ->
       let duplicates, res = analyze (list c) in
@@ -240,7 +239,7 @@ module Make(St : Solver_types.S) = struct
     let rec aux res acc = function
       | [] -> res, acc
       | c :: r ->
-        if not c.St.visited then begin
+        if not c.St.visited then (
           c.St.visited <- true;
           match c.St.cpremise with
           | St.Hyp | St.Local | St.Lemma _ -> aux (c :: res) acc r
@@ -248,8 +247,9 @@ module Make(St : Solver_types.S) = struct
             let l = List.fold_left (fun acc c ->
                 if not c.St.visited then c :: acc else acc) r h in
             aux res (c :: acc) l
-        end else
+        ) else (
           aux res acc r
+        )
     in
     let res, tmp = aux [] [] [proof] in
     List.iter (fun c -> c.St.visited <- false) res;
diff --git a/src/core/Solver.ml b/src/core/Solver.ml
index 5cc0994b..3dab855e 100644
--- a/src/core/Solver.ml
+++ b/src/core/Solver.ml
@@ -6,36 +6,7 @@ Copyright 2016 Simon Cruanes
 
 module type S = Solver_intf.S
 
-type ('term, 'form) sat_state = ('term, 'form) Solver_intf.sat_state = {
-  eval: 'form -> bool;
-  (** Returns the valuation of a formula in the current state
-      of the sat solver.
-      @raise UndecidedLit if the literal is not decided *)
-  eval_level: 'form -> bool * int;
-  (** Return the current assignement of the literals, as well as its
-      decision level. If the level is 0, then it is necessary for
-      the atom to have this value; otherwise it is due to choices
-      that can potentially be backtracked.
-      @raise UndecidedLit if the literal is not decided *)
-  iter_trail : ('form -> unit) -> ('term -> unit) -> unit;
-  (** Iter thorugh the formulas and terms in order of decision/propagation
-      (starting from the first propagation, to the last propagation). *)
-  model: unit -> ('term * 'term) list;
-  (** Returns the model found if the formula is satisfiable. *)
-}
-
-type ('clause, 'proof) unsat_state = ('clause, 'proof) Solver_intf.unsat_state = {
-  unsat_conflict : unit -> 'clause;
-  (** Returns the unsat clause found at the toplevel *)
-  get_proof : unit -> 'proof;
-  (** returns a persistent proof of the empty clause from the Unsat result. *)
-}
-
-type 'clause export = 'clause Solver_intf.export = {
-  hyps: 'clause Vec.t;
-  history: 'clause Vec.t;
-  local: 'clause Vec.t;
-}
+open Solver_intf
 
 module Make
     (St : Solver_types.S)
@@ -65,10 +36,10 @@ module Make
       (fun k -> k
         "@[<v>%s - Full resume:@,@[<hov 2>Trail:@\n%a@]@,@[<hov 2>Temp:@\n%a@]@,@[<hov 2>Hyps:@\n%a@]@,@[<hov 2>Lemmas:@\n%a@]@,@]@."
           status
-          (Vec.print ~sep:"" St.pp) (S.trail ())
-          (Vec.print ~sep:"" St.pp_clause) (S.temp ())
-          (Vec.print ~sep:"" St.pp_clause) (S.hyps ())
-          (Vec.print ~sep:"" St.pp_clause) (S.history ())
+          (Vec.print ~sep:"" St.Trail_elt.debug) (S.trail ())
+          (Vec.print ~sep:"" St.Clause.debug) (S.temp ())
+          (Vec.print ~sep:"" St.Clause.debug) (S.hyps ())
+          (Vec.print ~sep:"" St.Clause.debug) (S.history ())
       )
 
   let mk_sat () : (_,_) sat_state =
@@ -77,8 +48,8 @@ module Make
     let iter f f' =
       Vec.iter (function
           | St.Atom a -> f a.St.lit
-          | St.Lit l -> f' l.St.term
-        ) t
+          | St.Lit l -> f' l.St.term)
+        t
     in
     {
       eval = S.eval;
diff --git a/src/core/Solver_types.ml b/src/core/Solver_types.ml
index 29245d33..9f46d043 100644
--- a/src/core/Solver_types.ml
+++ b/src/core/Solver_types.ml
@@ -73,7 +73,7 @@ module McMake (E : Expr_intf.S)() = struct
   }
 
   and clause = {
-    name : string;
+    name : int;
     tag : int option;
     atoms : atom array;
     mutable cpremise : premise;
@@ -97,8 +97,9 @@ module McMake (E : Expr_intf.S)() = struct
     | E_lit of lit
     | E_var of var
 
-  (* Dummy values *)
-  let dummy_lit = E.Formula.dummy
+  type trail_elt =
+    | Lit of lit
+    | Atom of atom
 
   let rec dummy_var =
     { vid = -101;
@@ -113,7 +114,7 @@ module McMake (E : Expr_intf.S)() = struct
     }
   and dummy_atom =
     { var = dummy_var;
-      lit = dummy_lit;
+      lit = E.Formula.dummy;
       watched = Obj.magic 0;
       (* should be [Vec.make_empty dummy_clause]
          but we have to break the cycle *)
@@ -121,7 +122,7 @@ module McMake (E : Expr_intf.S)() = struct
       is_true = false;
       aid = -102 }
   let dummy_clause =
-    { name = "";
+    { name = -1;
       tag = None;
       atoms = [| |];
       activity = -1.;
@@ -129,13 +130,13 @@ module McMake (E : Expr_intf.S)() = struct
       visited = false;
       cpremise = History [] }
 
-  let () =
-    dummy_atom.watched <- Vec.make_empty dummy_clause
+  let () = dummy_atom.watched <- Vec.make_empty dummy_clause
 
   (* Constructors *)
   module MF = Hashtbl.Make(E.Formula)
   module MT = Hashtbl.Make(E.Term)
 
+  (* TODO: embed a state `t` with these inside *)
   let f_map = MF.create 4096
   let t_map = MT.create 4096
 
@@ -146,229 +147,286 @@ module McMake (E : Expr_intf.S)() = struct
 
   let cpt_mk_var = ref 0
 
-  let make_semantic_var t =
-    try MT.find t_map t
-    with Not_found ->
-      let res = {
-        lid = !cpt_mk_var;
-        term = t;
-        l_weight = 1.;
-        l_idx= -1;
-        l_level = -1;
-        assigned = None;
-      } in
-      incr cpt_mk_var;
-      MT.add t_map t res;
-      Vec.push vars (E_lit res);
-      res
+  let name_of_clause c = match c.cpremise with
+    | Hyp -> "H" ^ string_of_int c.name
+    | Local -> "L" ^ string_of_int c.name
+    | Lemma _ -> "T" ^ string_of_int c.name
+    | History _ -> "C" ^ string_of_int c.name
 
-  let make_boolean_var : formula -> var * Expr_intf.negated =
-    fun t ->
-      let lit, negated = E.Formula.norm t in
-      try
-        MF.find f_map lit, negated
+  module Lit = struct
+    type t = lit
+    let[@inline] term l = l.term
+    let[@inline] level l = l.l_level
+    let[@inline] set_level l lvl = l.l_level <- lvl
+
+    let[@inline] assigned l = l.assigned
+    let[@inline] set_assigned l t = l.assigned <- t
+
+    let[@inline] weight l = l.l_weight
+    let[@inline] set_weight l w = l.l_weight <- w
+
+    let make t =
+      try MT.find t_map t
       with Not_found ->
-        let cpt_fois_2 = !cpt_mk_var lsl 1 in
-        let rec var  =
-          { vid = !cpt_mk_var;
-            pa = pa;
-            na = na;
-            v_fields = Var_fields.empty;
-            v_level = -1;
-            v_idx= -1;
-            v_weight = 0.;
-            v_assignable = None;
-            reason = None;
-          }
-        and pa =
-          { var = var;
-            lit = lit;
-            watched = Vec.make 10 dummy_clause;
-            neg = na;
-            is_true = false;
-            aid = cpt_fois_2 (* aid = vid*2 *) }
-        and na =
-          { var = var;
-            lit = E.Formula.neg lit;
-            watched = Vec.make 10 dummy_clause;
-            neg = pa;
-            is_true = false;
-            aid = cpt_fois_2 + 1 (* aid = vid*2+1 *) } in
-        MF.add f_map lit var;
+        let res = {
+          lid = !cpt_mk_var;
+          term = t;
+          l_weight = 1.;
+          l_idx= -1;
+          l_level = -1;
+          assigned = None;
+        } in
         incr cpt_mk_var;
-        Vec.push vars (E_var var);
-        var, negated
+        MT.add t_map t res;
+        Vec.push vars (E_lit res);
+        res
 
-  let add_term t = make_semantic_var t
+    let debug_assign fmt v =
+      match v.assigned with
+      | None ->
+        Format.fprintf fmt ""
+      | Some t ->
+        Format.fprintf fmt "@[<hov>@@%d->@ %a@]" v.l_level E.Term.print t
 
-  let add_atom lit =
-    let var, negated = make_boolean_var lit in
-    match negated with
-    | Formula_intf.Negated -> var.na
-    | Formula_intf.Same_sign -> var.pa
+    let pp out v = E.Term.print out v.term
+    let debug out v =
+      Format.fprintf out "%d[%a][lit:@[<hov>%a@]]"
+        (v.lid+1) debug_assign v E.Term.print v.term
+  end
 
-  let make_clause ?tag name ali premise =
-    let atoms = Array.of_list ali in
-    { name  = name;
-      tag = tag;
-      atoms = atoms;
-      attached = false;
-      visited = false;
-      activity = 0.;
-      cpremise = premise}
+  module Var = struct
+    type t = var
+    let dummy = dummy_var
+    let[@inline] level v = v.v_level
+    let[@inline] set_level v lvl = v.v_level <- lvl
+    let[@inline] pos v = v.pa
+    let[@inline] neg v = v.na
+    let[@inline] reason v = v.reason
+    let[@inline] set_reason v r = v.reason <- r
+    let[@inline] assignable v = v.v_assignable
+    let[@inline] set_assignable v x = v.v_assignable <- x
+    let[@inline] weight v = v.v_weight
+    let[@inline] set_weight v w = v.v_weight <- w
 
-  let empty_clause = make_clause "Empty" [] (History [])
+    let make : formula -> var * Expr_intf.negated =
+      fun t ->
+        let lit, negated = E.Formula.norm t in
+        try
+          MF.find f_map lit, negated
+        with Not_found ->
+          let cpt_fois_2 = !cpt_mk_var lsl 1 in
+          let rec var  =
+            { vid = !cpt_mk_var;
+              pa = pa;
+              na = na;
+              v_fields = Var_fields.empty;
+              v_level = -1;
+              v_idx= -1;
+              v_weight = 0.;
+              v_assignable = None;
+              reason = None;
+            }
+          and pa =
+            { var = var;
+              lit = lit;
+              watched = Vec.make 10 dummy_clause;
+              neg = na;
+              is_true = false;
+              aid = cpt_fois_2 (* aid = vid*2 *) }
+          and na =
+            { var = var;
+              lit = E.Formula.neg lit;
+              watched = Vec.make 10 dummy_clause;
+              neg = pa;
+              is_true = false;
+              aid = cpt_fois_2 + 1 (* aid = vid*2+1 *) } in
+          MF.add f_map lit var;
+          incr cpt_mk_var;
+          Vec.push vars (E_var var);
+          var, negated
 
-  (* Marking helpers *)
-  let clear v = v.v_fields <- Var_fields.empty
+    (* Marking helpers *)
+    let[@inline] clear v =
+      v.v_fields <- Var_fields.empty
 
-  let seen a =
-    let pos = (a == a.var.pa) in
-    let field = if pos then v_field_seen_pos else v_field_seen_neg in
-    Var_fields.get field a.var.v_fields
+    let[@inline] seen_both v =
+      Var_fields.get v_field_seen_pos v.v_fields &&
+      Var_fields.get v_field_seen_neg v.v_fields
+  end
 
-  let seen_both v =
-    Var_fields.get v_field_seen_pos v.v_fields &&
-    Var_fields.get v_field_seen_neg v.v_fields
+  module Atom = struct
+    type t = atom
+    let dummy = dummy_atom
+    let[@inline] level a = a.var.v_level
+    let[@inline] var a = a.var
+    let[@inline] neg a = a.neg
+    let[@inline] abs a = a.var.pa
+    let[@inline] lit a = a.lit
+    let[@inline] equal a b = a == b
+    let[@inline] compare a b = Pervasives.compare a.aid b.aid
+    let[@inline] reason a = Var.reason a.var
+    let[@inline] id a = a.aid
+    let[@inline] is_true a = a.is_true
+    let[@inline] is_false a = a.neg.is_true
 
-  let mark a =
-    let pos = (a == a.var.pa) in
-    let field = if pos then v_field_seen_pos else v_field_seen_neg in
-    a.var.v_fields <- Var_fields.set field true a.var.v_fields
+    let[@inline] seen a =
+      let pos = equal a (abs a) in
+      if pos
+      then Var_fields.get v_field_seen_pos a.var.v_fields
+      else Var_fields.get v_field_seen_neg a.var.v_fields
 
-  (* Decisions & propagations *)
-  type t =
-    | Lit of lit
-    | Atom of atom
+    let[@inline] mark a =
+      let pos = equal a (abs a) in
+      if pos
+      then a.var.v_fields <- Var_fields.set v_field_seen_pos true a.var.v_fields
+      else a.var.v_fields <- Var_fields.set v_field_seen_neg true a.var.v_fields
 
-  let of_lit l = Lit l
-  let of_atom a = Atom a
+    let[@inline] make lit =
+      let var, negated = Var.make lit in
+      match negated with
+      | Formula_intf.Negated -> var.na
+      | Formula_intf.Same_sign -> var.pa
+
+    let pp fmt a = E.Formula.print fmt a.lit
+
+    let pp_a fmt v =
+      if Array.length v = 0 then (
+        Format.fprintf fmt "∅"
+      ) else (
+        pp fmt v.(0);
+        if (Array.length v) > 1 then begin
+          for i = 1 to (Array.length v) - 1 do
+            Format.fprintf fmt " ∨ %a" pp v.(i)
+          done
+        end
+      )
+
+    (* Complete debug printing *)
+    let sign a = if a == a.var.pa then "+" else "-"
+
+    let debug_reason fmt = function
+      | n, _ when n < 0 ->
+        Format.fprintf fmt "%%"
+      | n, None ->
+        Format.fprintf fmt "%d" n
+      | n, Some Decision ->
+        Format.fprintf fmt "@@%d" n
+      | n, Some Bcp c ->
+        Format.fprintf fmt "->%d/%s" n (name_of_clause c)
+      | n, Some Semantic ->
+        Format.fprintf fmt "::%d" n
+
+    let pp_level fmt a =
+      debug_reason fmt (a.var.v_level, a.var.reason)
+
+    let debug_value fmt a =
+      if a.is_true then
+        Format.fprintf fmt "T%a" pp_level a
+      else if a.neg.is_true then
+        Format.fprintf fmt "F%a" pp_level a
+      else
+        Format.fprintf fmt ""
+
+    let debug out a =
+      Format.fprintf out "%s%d[%a][atom:@[<hov>%a@]]"
+        (sign a) (a.var.vid+1) debug_value a E.Formula.print a.lit
+
+    let debug_a out vec =
+      Array.iter (fun a -> Format.fprintf out "%a@ " debug a) vec
+  end
 
   (* Elements *)
-  let[@inline] elt_of_lit l = E_lit l
-  let[@inline] elt_of_var v = E_var v
+  module Elt = struct
+    type t = elt
+    let[@inline] of_lit l = E_lit l
+    let[@inline] of_var v = E_var v
 
-  let get_elt_id = function
-    | E_lit l -> l.lid | E_var v ->  v.vid
-  let get_elt_level = function
-    | E_lit l -> l.l_level | E_var v ->  v.v_level
-  let get_elt_idx = function
-    | E_lit l -> l.l_idx | E_var v ->  v.v_idx
-  let get_elt_weight = function
-    | E_lit l -> l.l_weight | E_var v ->  v.v_weight
+    let[@inline] id = function
+      | E_lit l -> l.lid | E_var v ->  v.vid
+    let[@inline] level = function
+      | E_lit l -> l.l_level | E_var v ->  v.v_level
+    let[@inline] idx = function
+      | E_lit l -> l.l_idx | E_var v ->  v.v_idx
+    let[@inline] weight = function
+      | E_lit l -> l.l_weight | E_var v ->  v.v_weight
 
-  let set_elt_level e lvl = match e with
-    | E_lit l -> l.l_level <- lvl | E_var v ->  v.v_level <- lvl
-  let set_elt_idx e i = match e with
-    | E_lit l -> l.l_idx <- i | E_var v ->  v.v_idx <- i
-  let set_elt_weight e w = match e with
-    | E_lit l -> l.l_weight <- w | E_var v ->  v.v_weight <- w
+    let[@inline] set_level e lvl = match e with
+      | E_lit l -> l.l_level <- lvl | E_var v ->  v.v_level <- lvl
+    let[@inline] set_idx e i = match e with
+      | E_lit l -> l.l_idx <- i | E_var v ->  v.v_idx <- i
+    let[@inline] set_weight e w = match e with
+      | E_lit l -> l.l_weight <- w | E_var v ->  v.v_weight <- w
+  end
 
-  (* Name generation *)
-  let fresh_lname =
-    let cpt = ref 0 in
-    fun () -> incr cpt; "L" ^ (string_of_int !cpt)
+  module Trail_elt = struct
+    type t = trail_elt
+    let[@inline] of_lit l = Lit l
+    let[@inline] of_atom a = Atom a
 
-  let fresh_hname =
-    let cpt = ref 0 in
-    fun () -> incr cpt; "H" ^ (string_of_int !cpt)
+    let debug fmt = function
+      | Lit l -> Lit.debug fmt l
+      | Atom a -> Atom.debug fmt a
+  end
 
-  let fresh_tname =
-    let cpt = ref 0 in
-    fun () -> incr cpt; "T" ^ (string_of_int !cpt)
+  module Clause = struct
+    type t = clause
+    let dummy = dummy_clause
 
-  let fresh_name =
-    let cpt = ref 0 in
-    fun () -> incr cpt; "C" ^ (string_of_int !cpt)
+    let make =
+      let n = ref 0 in
+      fun ?tag ali premise ->
+        let atoms = Array.of_list ali in
+        let name = !n in
+        incr n;
+        { name;
+          tag = tag;
+          atoms = atoms;
+          visited = false;
+          attached = false;
+          activity = 0.;
+          cpremise = premise}
 
-  (* Pretty printing for atoms and clauses *)
-  let print_lit fmt v = E.Term.print fmt v.term
+    let empty = make [] (History [])
+    let name = name_of_clause
+    let[@inline] atoms c = c.atoms
+    let[@inline] tag c = c.tag
 
-  let print_atom fmt a = E.Formula.print fmt a.lit
+    let[@inline] premise c = c.cpremise
+    let[@inline] set_premise c p = c.cpremise <- p
 
-  let print_atoms fmt v =
-    if Array.length v = 0 then
-      Format.fprintf fmt "∅"
-    else begin
-      print_atom fmt v.(0);
-      if (Array.length v) > 1 then begin
-        for i = 1 to (Array.length v) - 1 do
-          Format.fprintf fmt " ∨ %a" print_atom v.(i)
-        done
-      end
-    end
+    let[@inline] visited c = c.visited
+    let[@inline] set_visited c b = c.visited <- b
 
-  let print_clause fmt c =
-    Format.fprintf fmt "%s : %a" c.name print_atoms c.atoms
+    let[@inline] attached c = c.attached
+    let[@inline] set_attached c b = c.attached <- b
 
-  (* Complete debug printing *)
-  let sign a = if a == a.var.pa then "+" else "-"
+    let[@inline] activity c = c.activity
+    let[@inline] set_activity c w = c.activity <- w
 
-  let pp_reason fmt = function
-    | n, _ when n < 0 ->
-      Format.fprintf fmt "%%"
-    | n, None ->
-      Format.fprintf fmt "%d" n
-    | n, Some Decision ->
-      Format.fprintf fmt "@@%d" n
-    | n, Some Bcp c ->
-      Format.fprintf fmt "->%d/%s" n c.name
-    | n, Some Semantic ->
-      Format.fprintf fmt "::%d" n
+    let pp fmt c =
+      Format.fprintf fmt "%s : %a" (name c) Atom.pp_a c.atoms
 
-  let pp_level fmt a =
-    pp_reason fmt (a.var.v_level, a.var.reason)
+    let debug_premise out = function
+      | Hyp -> Format.fprintf out "hyp"
+      | Local -> Format.fprintf out "local"
+      | Lemma _ -> Format.fprintf out "th_lemma"
+      | History v ->
+        List.iter (fun c -> Format.fprintf out "%s,@ " (name_of_clause c)) v
 
-  let pp_value fmt a =
-    if a.is_true then
-      Format.fprintf fmt "T%a" pp_level a
-    else if a.neg.is_true then
-      Format.fprintf fmt "F%a" pp_level a
-    else
-      Format.fprintf fmt ""
+    let debug out ({atoms=arr; cpremise=cp;_}as c) =
+      Format.fprintf out "%s@[<hov>{@[<hov>%a@]}@ cpremise={@[<hov>%a@]}@]"
+        (name c) Atom.debug_a arr debug_premise cp
 
-  let pp_premise out = function
-    | Hyp -> Format.fprintf out "hyp"
-    | Local -> Format.fprintf out "local"
-    | Lemma _ -> Format.fprintf out "th_lemma"
-    | History v -> List.iter (fun { name; _ } -> Format.fprintf out "%s,@ " name) v
-
-  let pp_assign fmt v =
-    match v.assigned with
-    | None ->
-      Format.fprintf fmt ""
-    | Some t ->
-      Format.fprintf fmt "@[<hov>@@%d->@ %a@]" v.l_level E.Term.print t
-
-  let pp_lit out v =
-    Format.fprintf out "%d[%a][lit:@[<hov>%a@]]"
-      (v.lid+1) pp_assign v E.Term.print v.term
-
-  let pp_atom out a =
-    Format.fprintf out "%s%d[%a][atom:@[<hov>%a@]]"
-      (sign a) (a.var.vid+1) pp_value a E.Formula.print a.lit
-
-  let pp_atoms_vec out vec =
-    Array.iter (fun a -> Format.fprintf out "%a@ " pp_atom a) vec
-
-  let pp_clause out {name=name; atoms=arr; cpremise=cp;_} =
-    Format.fprintf out "%s@[<hov>{@[<hov>%a@]}@ cpremise={@[<hov>%a@]}@]"
-      name pp_atoms_vec arr pp_premise cp
-
-  let pp_dimacs fmt {atoms;_} =
-    let aux fmt a =
-      Array.iter (fun p ->
+    let pp_dimacs fmt {atoms;_} =
+      let aux fmt a =
+        Array.iter (fun p ->
           Format.fprintf fmt "%s%d "
             (if p == p.var.pa then "-" else "")
             (p.var.vid+1)
         ) a
-    in
-    Format.fprintf fmt "%a0" aux atoms
-
-  let pp fmt = function
-    | Lit l -> pp_lit fmt l
-    | Atom a -> pp_atom fmt a
-
+      in
+      Format.fprintf fmt "%a0" aux atoms
+  end
 end
 
 
diff --git a/src/core/Solver_types_intf.ml b/src/core/Solver_types_intf.ml
index 6e69c570..08f011cc 100644
--- a/src/core/Solver_types_intf.ml
+++ b/src/core/Solver_types_intf.ml
@@ -24,6 +24,8 @@ Copyright 2016 Simon Cruanes
 
 module Var_fields = BitField.Make()
 
+type 'a printer = Format.formatter -> 'a -> unit
+
 module type S = sig
   (** The signatures of clauses used in the Solver. *)
 
@@ -86,7 +88,7 @@ module type S = sig
       [a.neg] wraps the theory negation of [f]. *)
 
   and clause = {
-    name : string;              (** Clause name, mainly for printing, unique. *)
+    name : int;                 (** Clause name, mainly for printing, unique. *)
     tag : int option;           (** User-provided tag for clauses. *)
     atoms : atom array;         (** The atoms that constitute the clause.*)
     mutable cpremise : premise; (** The premise of the clause, i.e. the justification
@@ -124,15 +126,11 @@ module type S = sig
       satisfied by the solver. *)
 
   (** {2 Decisions and propagations} *)
-  type t =
+  type trail_elt =
     | Lit of lit
     | Atom of atom (**)
   (** Either a lit of an atom *)
 
-  val of_lit : lit -> t
-  val of_atom : atom -> t
-  (** Constructors and destructors *)
-
   (** {2 Elements} *)
 
   type elt =
@@ -145,77 +143,136 @@ module type S = sig
   val iter_elt : (elt -> unit) -> unit
   (** Read access to the vector of variables created *)
 
-  val elt_of_lit : lit -> elt
-  val elt_of_var : var -> elt
-  (** Constructors & destructor for elements *)
+  (** {2 Variables, Literals & Clauses } *)
 
-  val get_elt_id : elt -> int
-  val get_elt_level : elt -> int
-  val get_elt_idx : elt -> int
-  val get_elt_weight : elt -> float
-  val set_elt_level : elt -> int -> unit
-  val set_elt_idx : elt -> int -> unit
-  val set_elt_weight : elt -> float -> unit
-  (** Accessors for elements *)
+  module Lit : sig
+    type t = lit
+    val term : t -> term
+    val make : term -> t
+    (** Returns the variable associated with the term *)
 
-  (** {2 Variables, Litterals & Clauses } *)
+    val level : t -> int
+    val set_level : t -> int -> unit
 
-  val dummy_var : var
-  val dummy_atom : atom
-  val dummy_clause : clause
-  (** Dummy values for use in vector dummys *)
+    val assigned : t -> term option
+    val set_assigned : t -> term option -> unit
+    val weight : t -> float
+    val set_weight : t -> float -> unit
 
-  val add_term : term -> lit
-  (** Returns the variable associated with the term *)
-  val add_atom : formula -> atom
-  (** Returns the atom associated with the given formula *)
-  val make_boolean_var : formula -> var * Formula_intf.negated
-  (** Returns the variable linked with the given formula, and whether the atom associated with the formula
-      is [var.pa] or [var.na] *)
+    val pp : t printer
+    val debug : t printer
+  end
 
-  val empty_clause : clause
-  (** The empty clause *)
-  val make_clause : ?tag:int -> string -> atom list -> premise -> clause
-  (** [make_clause name atoms size premise] creates a clause with the given attributes. *)
+  module Var : sig
+    type t = var
+    val dummy : t
 
 
-  (** {2 Helpers} *)
+    val pos : t -> atom
+    val neg : t -> atom
 
-  val mark : atom -> unit
-  (** Mark the atom as seen, using the 'seen' field in the variable. *)
+    val level : t -> int
+    val set_level : t -> int -> unit
+    val reason : t -> reason option
+    val set_reason : t -> reason option -> unit
+    val assignable : t -> lit list option
+    val set_assignable : t -> lit list option -> unit
+    val weight : t -> float
+    val set_weight : t -> float -> unit
 
-  val seen : atom -> bool
-  (** Returns wether the atom has been marked as seen. *)
+    val make : formula -> t * Formula_intf.negated
+    (** Returns the variable linked with the given formula,
+        and whether the atom associated with the formula
+        is [var.pa] or [var.na] *)
 
-  val seen_both : var -> bool
-  (** both atoms have been seen? *)
+    val seen_both : t -> bool
+    (** both atoms have been seen? *)
 
-  val clear : var -> unit
-  (** Clear the 'seen' field of the variable. *)
+    val clear : t -> unit
+    (** Clear the 'seen' field of the variable. *)
+  end
 
+  module Atom : sig
+    type t = atom
+    val dummy : t
+    val level : t -> int
+    val reason : t -> reason option
+    val lit : t -> formula
+    val equal : t -> t -> bool
+    val compare : t -> t -> int
+    val var : t -> Var.t
+    val abs : t -> t (** positive atom *)
+    val neg : t -> t
+    val id : t -> int
+    val is_true : t -> bool
+    val is_false : t -> bool
 
-  (** {2 Clause names} *)
+    val make : formula -> t
+    (** Returns the atom associated with the given formula *)
 
-  val fresh_name : unit -> string
-  val fresh_lname : unit -> string
-  val fresh_tname : unit -> string
-  val fresh_hname : unit -> string
-  (** Fresh names for clauses *)
+    val mark : t -> unit
+    (** Mark the atom as seen, using the 'seen' field in the variable. *)
 
-  (** {2 Printing} *)
+    val seen : t -> bool
+    (** Returns wether the atom has been marked as seen. *)
 
-  val print_lit : Format.formatter -> lit -> unit
-  val print_atom : Format.formatter -> atom -> unit
-  val print_clause : Format.formatter -> clause -> unit
-  (** Pretty printing functions for atoms and clauses *)
+    val pp : t printer
+    val pp_a : t array printer
+    val debug : t printer
+    val debug_a : t array printer
+  end
 
-  val pp : Format.formatter -> t -> unit
-  val pp_lit : Format.formatter -> lit -> unit
-  val pp_atom : Format.formatter -> atom -> unit
-  val pp_clause : Format.formatter -> clause -> unit
-  val pp_dimacs : Format.formatter -> clause -> unit
-  val pp_reason : Format.formatter -> (int * reason option) -> unit
-  (** Debug function for atoms and clauses (very verbose) *)
+  module Elt : sig
+    type t = elt
 
+    val of_lit : Lit.t -> t
+    val of_var : Var.t -> t
+
+    val id : t -> int
+    val level : t -> int
+    val idx : t -> int
+    val weight : t -> float
+
+    val set_level : t -> int -> unit
+    val set_idx : t -> int -> unit
+    val set_weight : t -> float -> unit
+  end
+
+  module Clause : sig
+    type t = clause
+    val dummy : t
+
+    val name : t -> string
+    val atoms : t -> Atom.t array
+    val tag : t -> int option
+    val premise : t -> premise
+    val set_premise : t -> premise -> unit
+
+    val visited : t -> bool
+    val set_visited : t -> bool -> unit
+    val attached : t -> bool
+    val set_attached : t -> bool -> unit
+    val activity : t -> float
+    val set_activity : t -> float -> unit
+
+    val empty : t
+    (** The empty clause *)
+
+    val make : ?tag:int -> Atom.t list -> premise -> clause
+    (** [make_clause name atoms size premise] creates a clause with the given attributes. *)
+
+    val pp : t printer
+    val pp_dimacs : t printer
+    val debug : t printer
+  end
+
+  module Trail_elt : sig
+    type t = trail_elt
+
+    val of_lit : Lit.t -> t
+    val of_atom : Atom.t -> t
+    (** Constructors and destructors *)
+    val debug : t printer
+  end
 end
 
diff --git a/src/main/main.ml b/src/main/main.ml
index ddaf697c..7c81de71 100644
--- a/src/main/main.ml
+++ b/src/main/main.ml
@@ -41,7 +41,7 @@ module Make
     let check_clause c =
       let l = List.map (function a ->
           Log.debugf 99
-            (fun k -> k "Checking value of %a" S.St.pp_atom (S.St.add_atom a));
+            (fun k -> k "Checking value of %a" S.St.Atom.debug (S.St.Atom.make a));
           state.Msat.eval a) c in
       List.exists (fun x -> x) l
     in