diff --git a/smt/smt.ml b/smt/smt.ml
index 68f866da..0a076f15 100644
--- a/smt/smt.ml
+++ b/smt/smt.ml
@@ -46,11 +46,8 @@ module Tsmt = struct
               Log.debug 10 "Propagating in th : %s" (Log.on_fmt Fsmt.print (s.get i));
               match s.get i with
               | Fsmt.Prop _ -> ()
-              | Fsmt.Equal (i, j) as f ->
-                      env := CC.add_eq !env i j
-              | Fsmt.Distinct (i, j) as f ->
-                      env := CC.add_neq !env i j
-              | _ -> assert false
+              | Fsmt.Equal (i, j) -> env := CC.add_eq !env i j
+              | Fsmt.Distinct (i, j) -> env := CC.add_neq !env i j
           done;
           Sat (current_level ())
       with CC.Unsat x ->
@@ -84,7 +81,6 @@ module Make(Dummy:sig end) = struct
     with SmtSolver.Unsat -> ()
 
   let get_proof () =
-    (* SmtSolver.Proof.learn (SmtSolver.history ()); *)
     match SmtSolver.unsat_conflict () with
     | None -> assert false
     | Some c -> SmtSolver.Proof.prove_unsat c
diff --git a/solver/internal.ml b/solver/internal.ml
index db945ec5..a8508997 100644
--- a/solver/internal.ml
+++ b/solver/internal.ml
@@ -43,7 +43,7 @@ module Make (L : Log_intf.S)(St : Solver_types.S)
     mutable var_inc : float;
     (* increment for variables' activity *)
 
-    trail : (lit, atom) Either.t Vec.t;
+    trail : t Vec.t;
     (* decision stack + propagated atoms *)
 
     trail_lim : int Vec.t;
@@ -114,7 +114,7 @@ module Make (L : Log_intf.S)(St : Solver_types.S)
     learnts = Vec.make 0 dummy_clause; (*updated during parsing*)
     clause_inc = 1.;
     var_inc = 1.;
-    trail = Vec.make 601 (Either.mk_right dummy_atom);
+    trail = Vec.make 601 (of_atom dummy_atom);
     trail_lim = Vec.make 601 (-1);
     user_levels = Vec.make 20 {ul_trail=0;ul_learnt=0;ul_clauses=0};
     qhead = 0;
@@ -148,35 +148,15 @@ module Make (L : Log_intf.S)(St : Solver_types.S)
   let to_float i = float_of_int i
   let to_int f = int_of_float f
 
-  (* Accessors for variables *)
-  let get_var_id v = v.vid
-  let get_var_level v = v.level
-  let get_var_weight v = v.weight
-  let set_var_weight v w = v.weight <- w
-  let set_var_level v l = v.level <- l
-
   (* Accessors for litterals *)
-  let get_lit_id v = v.lid
-  let get_lit_level (v : lit) = v.level
-  let get_lit_weight (v : lit) = v.weight
-  let set_lit_weight (v : lit) w = v.weight <- w
-  let set_lit_level (v : lit) l = v.level <- l
-
-  let get_elt_id e = Either.destruct e get_lit_id get_var_id
-  let get_elt_weight e = Either.destruct e get_lit_weight get_var_weight
-  let get_elt_level e = Either.destruct e get_lit_level get_var_level
-
-  let set_elt_weight e = Either.destruct e set_lit_weight set_var_weight
-  let set_elt_level e = Either.destruct e set_lit_level set_var_level
-
   let f_weight i j =
-    get_elt_weight (St.get_var j) < get_elt_weight (St.get_var i)
+    get_elt_weight (St.get_elt j) < get_elt_weight (St.get_elt i)
 
   let f_filter i =
-    get_elt_level (St.get_var i) < 0
+    get_elt_level (St.get_elt i) < 0
 
   (* Var/clause activity *)
-  let insert_var_order e = Either.destruct e
+  let insert_var_order e = destruct_elt e
       (fun v -> Iheap.insert f_weight env.order v.lid)
       (fun v ->
           Iheap.insert f_weight env.order v.vid;
@@ -192,8 +172,8 @@ module Make (L : Log_intf.S)(St : Solver_types.S)
   let var_bump_activity_aux v =
     v.weight <- v.weight +. env.var_inc;
     if v.weight > 1e100 then begin
-      for i = 0 to (St.nb_vars ()) - 1 do
-        set_elt_weight (St.get_var i) ((get_elt_weight (St.get_var i)) *. 1e-100)
+      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)
       done;
       env.var_inc <- env.var_inc *. 1e-100;
     end;
@@ -203,8 +183,8 @@ module Make (L : Log_intf.S)(St : Solver_types.S)
   let lit_bump_activity_aux (v : lit) =
     v.weight <- v.weight +. env.var_inc;
     if v.weight > 1e100 then begin
-      for i = 0 to (St.nb_vars ()) - 1 do
-        set_elt_weight (St.get_var i) ((get_elt_weight (St.get_var i)) *. 1e-100)
+      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)
       done;
       env.var_inc <- env.var_inc *. 1e-100;
     end;
@@ -231,7 +211,7 @@ module Make (L : Log_intf.S)(St : Solver_types.S)
   let nb_assigns () = Vec.size env.trail
   let nb_clauses () = Vec.size env.clauses
   let nb_learnts () = Vec.size env.learnts
-  let nb_vars    () = St.nb_vars ()
+  let nb_vars    () = St.nb_elt ()
 
   let new_decision_level() =
     Vec.push env.trail_lim (Vec.size env.trail);
@@ -273,22 +253,22 @@ module Make (L : Log_intf.S)(St : Solver_types.S)
       env.qhead <- Vec.get env.trail_lim lvl;
       env.tatoms_qhead <- env.qhead;
       for c = env.qhead to Vec.size env.trail - 1 do
-        Either.destruct (Vec.get env.trail c)
+        destruct (Vec.get env.trail c)
         (fun v ->
             v.assigned <- None;
             v.level <- -1;
-            insert_var_order (Either.mk_left v)
+            insert_var_order (elt_of_lit v)
         )
         (fun a ->
             if a.var.level <= lvl then begin
-              Vec.set env.trail env.qhead (Either.mk_right a);
+              Vec.set env.trail env.qhead (of_atom a);
               env.qhead <- env.qhead + 1
             end else begin
               a.is_true <- false;
               a.neg.is_true <- false;
               a.var.level <- -1;
               a.var.reason <- Bcp None;
-              insert_var_order (Either.mk_right a.var)
+              insert_var_order (elt_of_var a.var)
             end)
       done;
       Th.backtrack (Vec.get env.tenv_queue lvl); (* recover the right tenv *)
@@ -313,14 +293,14 @@ module Make (L : Log_intf.S)(St : Solver_types.S)
       a.is_true <- true;
       a.var.level <- lvl;
       a.var.reason <- reason;
-      Vec.push env.trail (Either.mk_right a);
+      Vec.push env.trail (of_atom a);
       L.debug 2 "Enqueue (%d): %a" (nb_assigns ()) pp_atom a
     end
 
   let enqueue_assign v value lvl =
     v.assigned <- Some value;
     v.level <- lvl;
-    Vec.push env.trail (Either.mk_left v);
+    Vec.push env.trail (of_lit v);
     L.debug 2 "Enqueue (%d): %a" (nb_assigns ()) St.pp_lit v
 
   let th_eval a =
@@ -371,7 +351,7 @@ module Make (L : Log_intf.S)(St : Solver_types.S)
         | _ ->
                 decr tr_ind;
                 L.debug 20 "Looking at trail element %d" !tr_ind;
-                Either.destruct (Vec.get env.trail !tr_ind)
+                destruct (Vec.get env.trail !tr_ind)
                 (fun v -> L.debug 15 "%a" St.pp_lit v)
                 (fun a -> match a.var.reason with
                     | Bcp (Some d) ->
@@ -396,7 +376,7 @@ module Make (L : Log_intf.S)(St : Solver_types.S)
       blevel, learnt, !history, !is_uip
 
   let get_atom i =
-    Either.destruct (Vec.get env.trail i)
+    destruct (Vec.get env.trail i)
       (fun _ -> assert false) (fun x -> x)
 
   let analyze_sat c_clause =
@@ -647,19 +627,19 @@ module Make (L : Log_intf.S)(St : Solver_types.S)
     ignore (th_eval a);
     a
 
-  let slice_get i = Either.destruct (Vec.get env.trail i)
+  let slice_get i = destruct (Vec.get env.trail i)
       (function {level; term; assigned = Some v} -> Th.Assign (term, v), level | _ -> assert false)
       (fun a -> Th.Lit a.lit, a.var.level)
 
   let slice_push l lemma =
     let atoms = List.rev_map (fun x -> new_atom x) l in
-    Iheap.grow_to_by_double env.order (St.nb_vars ());
-    List.iter (fun a -> insert_var_order (Either.mk_right a.var)) atoms;
+    Iheap.grow_to_by_double env.order (St.nb_elt ());
+    List.iter (fun a -> insert_var_order (elt_of_var a.var)) atoms;
     add_clause (fresh_tname ()) atoms (Lemma lemma)
 
   let slice_propagate f lvl =
     let a = add_atom f in
-    Iheap.grow_to_by_double env.order (St.nb_vars ());
+    Iheap.grow_to_by_double env.order (St.nb_elt ());
     enqueue_bool a lvl (Semantic lvl)
 
   let current_slice () = Th.({
@@ -686,8 +666,8 @@ module Make (L : Log_intf.S)(St : Solver_types.S)
       propagate ()
     | Th.Unsat (l, p) ->
       let l = List.rev_map new_atom l in
-      Iheap.grow_to_by_double env.order (St.nb_vars ());
-      List.iter (fun a -> insert_var_order (Either.mk_right a.var)) l;
+      Iheap.grow_to_by_double 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 (List.length l) true (Lemma p) in
       Some c
 
@@ -698,7 +678,7 @@ module Make (L : Log_intf.S)(St : Solver_types.S)
       let num_props = ref 0 in
       let res = ref None in
       while env.qhead < Vec.size env.trail do
-        Either.destruct (Vec.get env.trail env.qhead)
+        destruct (Vec.get env.trail env.qhead)
           (fun a -> ())
           (fun a ->
              incr num_props;
@@ -787,7 +767,7 @@ module Make (L : Log_intf.S)(St : Solver_types.S)
   (* Decide on a new litteral *)
   let rec pick_branch_lit () =
     let max = Iheap.remove_min f_weight env.order in
-    Either.destruct (St.get_var max)
+    destruct_elt (St.get_elt max)
       (fun v ->
          if v.level >= 0 then
            pick_branch_lit ()
@@ -824,7 +804,7 @@ module Make (L : Log_intf.S)(St : Solver_types.S)
         add_boolean_conflict confl
 
       | None -> (* No Conflict *)
-        if nb_assigns() = St.nb_vars () (* env.nb_init_vars *) then raise Sat;
+        if nb_assigns() = St.nb_elt () (* env.nb_init_vars *) then raise Sat;
         if n_of_conflicts > 0 && !conflictC >= n_of_conflicts then begin
           L.debug 1 "Restarting...";
           env.progress_estimate <- progress_estimate();
@@ -884,15 +864,15 @@ module Make (L : Log_intf.S)(St : Solver_types.S)
     | Sat -> ()
 
   let init_solver ?tag cnf =
-    let nbv = St.nb_vars () in
+    let nbv = St.nb_elt () in
     let nbc = env.nb_init_clauses + List.length cnf in
     Iheap.grow_to_by_double env.order nbv;
     (* List.iter (List.iter (fun a -> insert_var_order a.var)) cnf; *)
-    St.iter_vars insert_var_order;
+    St.iter_elt insert_var_order;
     Vec.grow_to_by_double env.clauses nbc;
     Vec.grow_to_by_double env.learnts nbc;
     env.nb_init_clauses <- nbc;
-    St.iter_vars (fun e -> Either.destruct e
+    St.iter_elt (fun e -> destruct_elt e
                      (fun v -> L.debug 50 " -- %a" St.pp_lit v)
                      (fun a -> L.debug 50 " -- %a" St.pp_atom a.pa)
                  );
@@ -916,7 +896,7 @@ module Make (L : Log_intf.S)(St : Solver_types.S)
 
   let model () =
     let opt = function Some a -> a | None -> assert false in
-    Vec.fold (fun acc e -> Either.destruct e
+    Vec.fold (fun acc e -> destruct e
                  (fun v -> (v.term, opt v.assigned)  :: acc)
                  (fun _ -> acc)
              ) [] env.trail
diff --git a/solver/mcsolver.ml b/solver/mcsolver.ml
index 5e63946d..a1956de9 100644
--- a/solver/mcsolver.ml
+++ b/solver/mcsolver.ml
@@ -7,7 +7,7 @@ Copyright 2014 Simon Cruanes
 module Make (L : Log_intf.S)(E : Expr_intf.S)
     (Th : Plugin_intf.S with type term = E.Term.t and type formula = E.Formula.t) = struct
 
-  module St = Solver_types.Make(L)(E)(Th)
+  module St = Solver_types.McMake(L)(E)(Th)
 
   module M = Internal.Make(L)(St)(Th)
 
diff --git a/solver/solver.ml b/solver/solver.ml
index 59c42889..890b1178 100644
--- a/solver/solver.ml
+++ b/solver/solver.ml
@@ -50,21 +50,22 @@ module Make (L : Log_intf.S)(E : Formula_intf.S)
 
     let current_level = Th.current_level
 
-    let assume s = match Th.assume {
-        Th.start = s.start;
-        Th.length = s.length;
-        Th.get = (function i -> match s.get i with
-            | Lit f, _ -> f | _ -> assert false);
-        Th.push = s.push;
-      } with
-    | Th.Sat _ -> Sat
-    | Th.Unsat (l, p) -> Unsat (l, p)
+    let assume_get s i = match s.get i with
+      | Lit f, _ -> f | _ -> assert false
+
+    let assume s =
+      match Th.assume {
+          Th.start = s.start;
+          Th.length = s.length;
+          Th.get = assume_get s;
+          Th.push = s.push;
+        } with
+      | Th.Sat _ -> Sat
+      | Th.Unsat (l, p) -> Unsat (l, p)
 
     let backtrack = Th.backtrack
 
-    let assign t =
-      Format.printf "Error : %a@." Expr.Term.print t;
-      assert false
+    let assign _ = assert false
 
     let iter_assignable _ _ = ()
 
@@ -75,11 +76,7 @@ module Make (L : Log_intf.S)(E : Formula_intf.S)
     let proof_debug _ = assert false
   end
 
-  module St = struct
-    module M = Solver_types.Make(L)(Expr)(Plugin)
-    include M
-    let mcsat = false
-  end
+  module St = Solver_types.SatMake(L)(E)(Th)
 
   module S = Internal.Make(L)(St)(Plugin)
 
@@ -87,770 +84,3 @@ module Make (L : Log_intf.S)(E : Formula_intf.S)
 
 end
 
-(*
-module Make (L : Log_intf.S)(F : Formula_intf.S)
-    (Th : Theory_intf.S with type formula = F.t) = struct
-
-  module St = Solver_types.Make(F)(Th)
-  module Proof = Res.Make(L)(St)
-
-  open St
-
-  exception Sat
-  exception Unsat
-  exception Restart
-  exception Conflict of clause
-
-  (* a push/pop state *)
-  type user_level = {
-    ul_trail : int; (* height of the decision trail *)
-    ul_clauses : int; (* number of clauses *)
-    ul_learnt : int; (* number of learnt clauses *)
-  }
-
-  (* Singleton type containing the current state *)
-  type env = {
-
-    mutable is_unsat : bool;
-    (* if [true], constraints are already false *)
-
-    mutable unsat_conflict : clause option;
-    (* conflict clause at decision level 0, if any *)
-
-    clauses : clause Vec.t;
-    (* all currently active clauses *)
-
-    learnts : clause Vec.t;
-    (* learnt clauses  *)
-
-    mutable clause_inc : float;
-    (* increment for clauses' activity *)
-
-    mutable var_inc : float;
-    (* increment for variables' activity *)
-
-    trail : atom Vec.t;
-    (* decision stack + propagated atoms *)
-
-    trail_lim : int Vec.t;
-    (* decision levels in [trail]  *)
-
-    user_levels : user_level Vec.t;
-    (* user-defined levels, for {!push} and {!pop} *)
-
-    mutable qhead : int;
-    (* Start offset in the queue of unit facts to propagate, within the trail *)
-
-    mutable simpDB_assigns : int;
-    (* number of toplevel assignments since last call to [simplify ()] *)
-
-    mutable simpDB_props : int;
-    (* remaining number of propagations before the next call to [simplify ()] *)
-
-    order : Iheap.t;
-    (* Heap ordered by variable activity *)
-
-    mutable progress_estimate : float;
-    (* progression estimate, updated by [search ()] *)
-
-    remove_satisfied : bool;
-
-    var_decay : float;
-    (* inverse of the activity factor for variables. Default 1/0.999 *)
-
-    clause_decay : float;
-    (* inverse of the activity factor for clauses. Default 1/0.95 *)
-
-    mutable restart_first : int;
-    (* intial restart limit, default 100 *)
-
-    restart_inc : float;
-    (* multiplicative factor for restart limit, default 1.5 *)
-
-    mutable learntsize_factor : float;
-    (* initial limit for the number of learnt clauses, 1/3 of initial
-        number of clauses by default *)
-
-    learntsize_inc : float;
-    (* multiplicative factor for [learntsize_factor] at each restart, default 1.1 *)
-
-    expensive_ccmin : bool;
-    (* control minimization of conflict clause, default true *)
-
-    polarity_mode : bool;
-    (* default polarity for decision *)
-
-    mutable starts : int;
-    mutable decisions : int;
-    mutable propagations : int;
-    mutable conflicts : int;
-    mutable clauses_literals : int;
-    mutable learnts_literals : int;
-    mutable max_literals : int;
-    mutable tot_literals : int;
-    mutable nb_init_clauses : int;
-    mutable model : var Vec.t;
-    mutable tenv_queue : Th.level Vec.t;
-    mutable tatoms_qhead : int;
-  }
-
-  let env = {
-    is_unsat = false;
-    unsat_conflict = None;
-    clauses = Vec.make 0 dummy_clause; (*updated during parsing*)
-    learnts = Vec.make 0 dummy_clause; (*updated during parsing*)
-    clause_inc = 1.;
-    var_inc = 1.;
-    trail = Vec.make 601 dummy_atom;
-    trail_lim = Vec.make 601 (-1);
-    user_levels = Vec.make 20 {ul_trail=0;ul_learnt=0;ul_clauses=0};
-    qhead = 0;
-    simpDB_assigns = -1;
-    simpDB_props = 0;
-    order = Iheap.init 0; (* updated in solve *)
-    progress_estimate = 0.;
-    remove_satisfied = true;
-    var_decay = 1. /. 0.95;
-    clause_decay = 1. /. 0.999;
-    restart_first = 100;
-    restart_inc = 1.5;
-    learntsize_factor = 1. /. 3. ;
-    learntsize_inc = 1.1;
-    expensive_ccmin = true;
-    polarity_mode = false;
-    starts = 0;
-    decisions = 0;
-    propagations = 0;
-    conflicts = 0;
-    clauses_literals = 0;
-    learnts_literals = 0;
-    max_literals = 0;
-    tot_literals = 0;
-    nb_init_clauses = 0;
-    model = Vec.make 0 dummy_var;
-    tenv_queue = Vec.make 100 Th.dummy;
-    tatoms_qhead = 0;
-  }
-
-  (* Misc functions *)
-  let to_float i = float_of_int i
-  let to_int f = int_of_float f
-
-  let f_weight i j =
-    (St.get_var j).weight < (St.get_var i).weight
-
-  let f_filter i =
-    (St.get_var i).level < 0
-
-
-  (* Var/clause activity *)
-  let insert_var_order v =
-    Iheap.insert f_weight env.order v.vid
-
-  let var_decay_activity () =
-    env.var_inc <- env.var_inc *. env.var_decay
-
-  let clause_decay_activity () =
-    env.clause_inc <- env.clause_inc *. env.clause_decay
-
-  let var_bump_activity v =
-    v.weight <- v.weight +. env.var_inc;
-    if v.weight > 1e100 then begin
-      for i = 0 to (St.nb_vars ()) - 1 do
-        (St.get_var i).weight <- (St.get_var i).weight *. 1e-100
-      done;
-      env.var_inc <- env.var_inc *. 1e-100;
-    end;
-    if Iheap.in_heap env.order v.vid then
-      Iheap.decrease f_weight env.order v.vid
-
-  let clause_bump_activity c =
-    c.activity <- c.activity +. env.clause_inc;
-    if c.activity > 1e20 then begin
-      for i = 0 to (Vec.size env.learnts) - 1 do
-        (Vec.get env.learnts i).activity <-
-          (Vec.get env.learnts i).activity *. 1e-20;
-      done;
-      env.clause_inc <- env.clause_inc *. 1e-20
-    end
-
-  (* Convenient access *)
-  let decision_level () = Vec.size env.trail_lim
-
-  let nb_assigns () = Vec.size env.trail
-  let nb_clauses () = Vec.size env.clauses
-  let nb_learnts () = Vec.size env.learnts
-  let nb_vars    () = St.nb_vars ()
-
-  let new_decision_level() =
-    Vec.push env.trail_lim (Vec.size env.trail);
-    Vec.push env.tenv_queue (Th.current_level ()); (* save the current tenv *)
-    L.debug 5 "New decision level : %d (%d in env queue)(%d in trail)"
-      (Vec.size env.trail_lim) (Vec.size env.tenv_queue) (Vec.size env.trail);
-    ()
-
-  let attach_clause c =
-    Vec.push (Vec.get c.atoms 0).neg.watched c;
-    Vec.push (Vec.get c.atoms 1).neg.watched c;
-    L.debug 8 "%a <-- %a" St.pp_atom (Vec.get c.atoms 0).neg St.pp_clause c;
-    L.debug 8 "%a <-- %a" St.pp_atom (Vec.get c.atoms 1).neg St.pp_clause c;
-    if c.learnt then
-      env.learnts_literals <- env.learnts_literals + Vec.size c.atoms
-    else
-      env.clauses_literals <- env.clauses_literals + Vec.size c.atoms
-
-  let detach_clause c =
-    c.removed <- true;
-        (*
-        Vec.remove (Vec.get c.atoms 0).neg.watched c;
-        Vec.remove (Vec.get c.atoms 1).neg.watched c;
-        *)
-    if c.learnt then
-      env.learnts_literals <- env.learnts_literals - Vec.size c.atoms
-    else
-      env.clauses_literals <- env.clauses_literals - Vec.size c.atoms
-
-  let remove_clause c = detach_clause c
-
-  let satisfied c =
-    Vec.exists (fun atom -> atom.is_true) c.atoms
-
-  (* cancel down to [lvl] excluded *)
-  let cancel_until lvl =
-    L.debug 5 "Bactracking to decision level %d (excluded)" lvl;
-    if decision_level () > lvl then begin
-      env.qhead <- Vec.get env.trail_lim lvl;
-      env.tatoms_qhead <- env.qhead;
-      for c = Vec.size env.trail - 1 downto env.qhead do
-        let a = Vec.get env.trail c in
-        a.is_true <- false;
-        a.neg.is_true <- false;
-        a.var.level <- -1;
-        a.var.reason <- None;
-        a.var.vpremise <- History [];
-        insert_var_order a.var
-      done;
-      Th.backtrack (Vec.get env.tenv_queue lvl); (* recover the right tenv *)
-      Vec.shrink env.trail ((Vec.size env.trail) - env.qhead);
-      Vec.shrink env.trail_lim ((Vec.size env.trail_lim) - lvl);
-      Vec.shrink env.tenv_queue ((Vec.size env.tenv_queue) - lvl)
-    end;
-    assert (Vec.size env.trail_lim = Vec.size env.tenv_queue)
-
-  let report_unsat ({atoms=atoms} as confl) =
-    L.debug 5 "Unsat conflict : %a" St.pp_clause confl;
-    env.unsat_conflict <- Some confl;
-    env.is_unsat <- true;
-    raise Unsat
-
-  let enqueue a lvl reason =
-    assert (not a.is_true && not a.neg.is_true &&
-            a.var.level < 0 && a.var.reason = None && lvl >= 0);
-    assert (lvl = decision_level ());
-    (* keep the reason for proof/unsat-core *)
-    (*let reason = if lvl = 0 then None else reason in*)
-    a.is_true <- true;
-    a.var.level <- lvl;
-    a.var.reason <- reason;
-    L.debug 8 "Enqueue: %a" pp_atom a;
-    Vec.push env.trail a
-
-  (* conflict analysis *)
-  let analyze c_clause =
-    let pathC  = ref 0 in
-    let learnt = ref [] in
-    let cond   = ref true in
-    let blevel = ref 0 in
-    let seen   = ref [] in
-    let c      = ref c_clause in
-    let tr_ind = ref (Vec.size env.trail - 1) in
-    let size   = ref 1 in
-    let history = ref [] in
-    while !cond do
-      if !c.learnt then clause_bump_activity !c;
-      history := !c :: !history;
-      (* visit the current predecessors *)
-      for j = 0 to Vec.size !c.atoms - 1 do
-        let q = Vec.get !c.atoms j in
-        (*printf "I visit %a@." D1.atom q;*)
-        assert (q.is_true || q.neg.is_true && q.var.level >= 0); (* Pas sur *)
-        if not q.var.seen && q.var.level > 0 then begin
-          var_bump_activity q.var;
-          q.var.seen <- true;
-          seen := q :: !seen;
-          if q.var.level >= decision_level () then begin
-            incr pathC
-          end else begin
-            learnt := q :: !learnt;
-            incr size;
-            blevel := max !blevel q.var.level
-          end
-        end
-      done;
-
-      (* look for the next node to expand *)
-      while not (Vec.get env.trail !tr_ind).var.seen do decr tr_ind done;
-      decr pathC;
-      let p = Vec.get env.trail !tr_ind in
-      decr tr_ind;
-      match !pathC, p.var.reason with
-      | 0, _ ->
-        cond := false;
-        learnt := p.neg :: (List.rev !learnt)
-      | n, None   -> assert false
-      | n, Some cl -> c := cl
-    done;
-    List.iter (fun q -> q.var.seen <- false) !seen;
-    !blevel, !learnt, !history, !size
-
-  let record_learnt_clause blevel learnt history size =
-    begin match learnt with
-      | [] -> assert false
-      | [fuip] ->
-        assert (blevel = 0);
-        fuip.var.vpremise <- history;
-        let name = fresh_lname () in
-        let uclause = make_clause name learnt size true history in
-        L.debug 2 "Unit clause learnt : %a" St.pp_clause uclause;
-        Vec.push env.learnts uclause;
-        enqueue fuip 0 (Some uclause)
-      | fuip :: _ ->
-        let name = fresh_lname () in
-        let lclause = make_clause name learnt size true history in
-        L.debug 2 "New clause learnt : %a" St.pp_clause lclause;
-        Vec.push env.learnts lclause;
-        attach_clause lclause;
-        clause_bump_activity lclause;
-        enqueue fuip blevel (Some lclause)
-    end;
-    var_decay_activity ();
-    clause_decay_activity ()
-
-  let add_boolean_conflict confl =
-    env.conflicts <- env.conflicts + 1;
-    if decision_level() = 0 then report_unsat confl; (* Top-level conflict *)
-    let blevel, learnt, history, size = analyze confl in
-    cancel_until blevel;
-    record_learnt_clause blevel learnt (History history) size
-
-  (* Add a new clause *)
-  exception Trivial
-
-  let simplify_zero atoms init0 =
-    (* TODO: could be more efficient than [@] everywhere? *)
-    assert (decision_level () = 0);
-    let aux (atoms, init) a =
-        if a.is_true then raise Trivial;
-        if a.neg.is_true then
-            match a.var.vpremise with
-            | History _ -> atoms, false
-            | Lemma _ -> assert false
-        else
-            a::atoms, init
-    in
-    let atoms, init = List.fold_left aux ([], true) atoms in
-    List.fast_sort (fun a b -> a.var.vid - b.var.vid) atoms, init
-
-  let partition atoms init0 =
-    let rec partition_aux trues unassigned falses init = function
-      | [] -> trues @ unassigned @ falses, init
-      | a::r ->
-        if a.is_true then
-          if a.var.level = 0 then raise Trivial
-          else (a::trues) @ unassigned @ falses @ r, init
-        else if a.neg.is_true then
-          if a.var.level = 0 then match a.var.vpremise with
-          | History v ->
-            partition_aux trues unassigned falses false r
-          | Lemma _ -> assert false
-          else
-          partition_aux trues unassigned (a::falses) init r
-        else partition_aux trues (a::unassigned) falses init r
-    in
-    if decision_level () = 0 then
-        simplify_zero atoms init0
-    else
-        partition_aux [] [] [] true atoms
-
-  let add_clause ?tag name atoms history =
-    if env.is_unsat then raise Unsat;
-    let init_name = name in
-    let init0 = make_clause ?tag init_name atoms (List.length atoms) (history <> History []) history in
-    L.debug 10 "Adding clause : %a" St.pp_clause init0;
-    try
-      if Proof.has_been_proved init0 then raise Trivial;
-      assert (Proof.is_proven init0);
-      let atoms, init = partition atoms init0 in
-      let size = List.length atoms in
-      match atoms with
-      | [] ->
-        report_unsat init0;
-      | a::b::_ ->
-        let name = fresh_name () in
-        let clause =
-            if init then init0
-            else make_clause ?tag (init_name ^ "_" ^ name) atoms size true (History [init0])
-        in
-        L.debug 10 "New clause : %a" St.pp_clause init0;
-        attach_clause clause;
-        Vec.push env.clauses clause;
-        if a.neg.is_true then begin
-          let lvl = List.fold_left (fun m a -> max m a.var.level) 0 atoms in
-          cancel_until lvl;
-          add_boolean_conflict clause
-        end else if b.neg.is_true && not a.is_true && not a.neg.is_true then begin
-          let lvl = List.fold_left (fun m a -> max m a.var.level) 0 atoms in
-          cancel_until lvl;
-          enqueue a lvl (Some clause)
-        end
-      | [a] ->
-        cancel_until 0;
-        a.var.vpremise <- History [init0];
-        enqueue a 0 (Some init0)
-    with Trivial -> ()
-
-
-  (* Decide on a new litteral *)
-  let rec pick_branch_lit () =
-    let max = Iheap.remove_min f_weight env.order in
-    let v = St.get_var max in
-    if v.level>= 0 then  begin
-      assert (v.pa.is_true || v.na.is_true);
-      pick_branch_lit ()
-    end else
-      v
-
-  let progress_estimate () =
-    let prg = ref 0. in
-    let nbv = to_float (nb_vars()) in
-    let lvl = decision_level () in
-    let _F = 1. /. nbv in
-    for i = 0 to lvl do
-      let _beg = if i = 0 then 0 else Vec.get env.trail_lim (i-1) in
-      let _end = if i=lvl then Vec.size env.trail else Vec.get env.trail_lim i in
-      prg := !prg +. _F**(to_float i) *. (to_float (_end - _beg))
-    done;
-    !prg /. nbv
-
-  let propagate_in_clause a c i watched new_sz =
-    let atoms = c.atoms in
-    let first = Vec.get atoms 0 in
-    if first == a.neg then begin (* false lit must be at index 1 *)
-      Vec.set atoms 0 (Vec.get atoms 1);
-      Vec.set atoms 1 first
-    end;
-    let first = Vec.get atoms 0 in
-    if first.is_true then begin
-      (* true clause, keep it in watched *)
-      Vec.set watched !new_sz c;
-      incr new_sz;
-    end
-    else
-      try (* look for another watch lit *)
-        for k = 2 to Vec.size atoms - 1 do
-          let ak = Vec.get atoms k in
-          if not (ak.neg.is_true) then begin
-            (* watch lit found: update and exit *)
-            Vec.set atoms 1 ak;
-            Vec.set atoms k a.neg;
-            Vec.push ak.neg.watched c;
-            L.debug 8 "New watcher (%a) for clause : %a" St.pp_atom ak.neg St.pp_clause c;
-            raise Exit
-          end
-        done;
-        (* no watch lit found *)
-        if first.neg.is_true then begin
-          (* clause is false *)
-          env.qhead <- Vec.size env.trail;
-          for k = i to Vec.size watched - 1 do
-            Vec.set watched !new_sz (Vec.get watched k);
-            incr new_sz;
-          done;
-          L.debug 3 "Conflict found : %a" St.pp_clause c;
-          raise (Conflict c)
-        end
-        else begin
-          (* clause is unit *)
-          Vec.set watched !new_sz c;
-          incr new_sz;
-          L.debug 5 "Unit clause : %a" St.pp_clause c;
-          enqueue first (decision_level ()) (Some c)
-        end
-      with Exit -> ()
-
-  let propagate_atom a res =
-    L.debug 8 "Propagating %a" St.pp_atom a;
-    let watched = a.watched in
-    L.debug 10 "Watching %a :" St.pp_atom a;
-    Vec.iter (fun c -> L.debug 10 "  %a" St.pp_clause c) watched;
-    let new_sz_w = ref 0 in
-    begin
-      try
-        for i = 0 to Vec.size watched - 1 do
-          let c = Vec.get watched i in
-          if not c.removed then propagate_in_clause a c i watched new_sz_w
-        done;
-      with Conflict c ->
-        assert (!res = None);
-        res := Some c
-    end;
-    let dead_part = Vec.size watched - !new_sz_w in
-    Vec.shrink watched dead_part
-
-  (* Propagation (boolean and theory *)
-  let _th_cnumber = ref 0
-  let slice_get i = (Vec.get env.trail i).lit
-  let slice_push l lemma =
-    decr _th_cnumber;
-    let atoms = List.rev_map (fun x -> add_atom x) l in
-    Iheap.grow_to_by_double env.order (St.nb_vars ());
-    List.iter (fun a -> insert_var_order a.var) atoms;
-    add_clause "lemma" atoms (Lemma lemma)
-
-  let current_slice () = Th.({
-      start = env.tatoms_qhead;
-      length = (Vec.size env.trail) - env.tatoms_qhead;
-      get = slice_get;
-      push = slice_push;
-    })
-
-  let rec theory_propagate () =
-    let head = Vec.size env.trail in
-    match Th.assume (current_slice ()) with
-    | Th.Sat _ ->
-      env.tatoms_qhead <- head;
-      propagate ()
-    | Th.Unsat (l, p) ->
-      let l = List.rev_map St.add_atom l in
-      let c = St.make_clause (St.fresh_name ()) l (List.length l) true (Lemma p) in
-      Some c
-
-  and propagate () =
-    if env.qhead = Vec.size env.trail then
-      None
-    else begin
-      let num_props = ref 0 in
-      let res = ref None in
-      while env.qhead < Vec.size env.trail do
-        let a = Vec.get env.trail env.qhead in
-        env.qhead <- env.qhead + 1;
-        incr num_props;
-        propagate_atom a res;
-      done;
-      env.propagations <- env.propagations + !num_props;
-      env.simpDB_props <- env.simpDB_props - !num_props;
-      match !res with
-      | None -> theory_propagate ()
-      | _ -> !res
-    end
-
-  (* heuristic comparison between clauses, by their size (unary/binary or not)
-      and activity *)
-  let f_sort_db c1 c2 =
-    let sz1 = Vec.size c1.atoms in
-    let sz2 = Vec.size c2.atoms in
-    let c = compare c1.activity c2.activity in
-    if sz1 = sz2 && c = 0 then 0
-    else
-    if sz1 > 2 && (sz2 = 2 || c < 0) then -1
-    else 1
-
-  (* returns true if the clause is used as a reason for a propagation,
-      and therefore can be needed in case of conflict. In this case
-      the clause can't be forgotten *)
-  let locked c = false (*
-    Vec.exists
-      (fun v -> match v.reason with
-         | Some c' -> c ==c'
-         | _ -> false
-      ) env.vars
-      *)
-
-  (* remove some learnt clauses *)
-  let reduce_db () = () (*
-    let extra_lim = env.clause_inc /. (to_float (Vec.size env.learnts)) in
-    Vec.sort env.learnts f_sort_db;
-    let lim2 = Vec.size env.learnts in
-    let lim1 = lim2 / 2 in
-    let j = ref 0 in
-    for i = 0 to lim1 - 1 do
-      let c = Vec.get env.learnts i in
-      if Vec.size c.atoms > 2 && not (locked c) then
-        remove_clause c
-      else
-        begin Vec.set env.learnts !j c; incr j end
-    done;
-    for i = lim1 to lim2 - 1 do
-      let c = Vec.get env.learnts i in
-      if Vec.size c.atoms > 2 && not (locked c) && c.activity < extra_lim then
-        remove_clause c
-      else
-        begin Vec.set env.learnts !j c; incr j end
-    done;
-    Vec.shrink env.learnts (lim2 - !j)
-    *)
-
-  (* remove from [vec] the clauses that are satisfied in the current trail *)
-  let remove_satisfied vec =
-    for i = 0 to Vec.size vec - 1 do
-      let c = Vec.get vec i in
-      if satisfied c then remove_clause c
-    done
-
-  module HUC = Hashtbl.Make
-      (struct type t = clause let equal = (==) let hash = Hashtbl.hash end)
-
-  let simplify () =
-    assert (decision_level () = 0);
-    if env.is_unsat then raise Unsat;
-    begin
-      match propagate () with
-      | Some confl -> report_unsat confl
-      | None -> ()
-    end;
-    if nb_assigns() <> env.simpDB_assigns && env.simpDB_props <= 0 then begin
-      if Vec.size env.learnts > 0 then remove_satisfied env.learnts;
-      if env.remove_satisfied then remove_satisfied env.clauses;
-      (*Iheap.filter env.order f_filter f_weight;*)
-      env.simpDB_assigns <- nb_assigns ();
-      env.simpDB_props <- env.clauses_literals + env.learnts_literals;
-    end
-
-  let search n_of_conflicts n_of_learnts =
-    let conflictC = ref 0 in
-    env.starts <- env.starts + 1;
-    while (true) do
-      match propagate () with
-      | Some confl -> (* Conflict *)
-        incr conflictC;
-        add_boolean_conflict confl
-
-      | None -> (* No Conflict *)
-        if nb_assigns() = St.nb_vars () (* env.nb_init_vars *) then raise Sat;
-        if n_of_conflicts >= 0 && !conflictC >= n_of_conflicts then
-          begin
-            env.progress_estimate <- progress_estimate();
-            cancel_until 0;
-            raise Restart
-          end;
-        if decision_level() = 0 then simplify ();
-
-        if n_of_learnts >= 0 &&
-           Vec.size env.learnts - nb_assigns() >= n_of_learnts then
-          reduce_db();
-
-        env.decisions <- env.decisions + 1;
-
-        new_decision_level();
-        let next = pick_branch_lit () in
-        let current_level = decision_level () in
-        assert (next.level < 0);
-        L.debug 5 "Deciding on %a" St.pp_atom next.pa;
-        enqueue next.pa current_level None
-    done
-
-  let check_clause c =
-    let b = ref false in
-    let atoms = c.atoms in
-    for i = 0 to Vec.size atoms - 1 do
-      let a = Vec.get atoms i in
-      b := !b || a.is_true
-    done;
-    assert (!b)
-
-  let check_vec vec =
-    for i = 0 to Vec.size vec - 1 do check_clause (Vec.get vec i) done
-
-  (*
-  let check_model () =
-    check_vec env.clauses;
-    check_vec env.learnts
-  *)
-
-  (* fixpoint of propagation and decisions until a model is found, or a
-     conflict is reached *)
-  let solve () =
-    if env.is_unsat then raise Unsat;
-    let n_of_conflicts = ref (to_float env.restart_first) in
-    let n_of_learnts = ref ((to_float (nb_clauses())) *. env.learntsize_factor) in
-    try
-      while true do
-        begin try
-            search (to_int !n_of_conflicts) (to_int !n_of_learnts);
-          with Restart -> ()
-        end;
-        n_of_conflicts := !n_of_conflicts *. env.restart_inc;
-        n_of_learnts   := !n_of_learnts *. env.learntsize_inc;
-      done;
-    with
-    | Sat -> ()
-
-  let add_clauses ?tag cnf =
-    let aux cl =
-        add_clause ?tag "hyp" cl (History []);
-        match propagate () with
-        | None -> () | Some confl -> report_unsat confl
-    in
-    List.iter aux cnf
-
-  let init_solver ?tag cnf =
-    let nbv = St.nb_vars () in
-    let nbc = env.nb_init_clauses + List.length cnf in
-    Iheap.grow_to_by_double env.order nbv;
-    (* List.iter (List.iter (fun a -> insert_var_order a.var)) cnf; *)
-    St.iter_vars insert_var_order;
-    Vec.grow_to_by_double env.model nbv;
-    Vec.grow_to_by_double env.clauses nbc;
-    Vec.grow_to_by_double env.learnts nbc;
-    env.nb_init_clauses <- nbc;
-    add_clauses ?tag cnf
-
-  let assume ?tag cnf =
-    let cnf = List.rev_map (List.rev_map St.add_atom) cnf in
-    init_solver ?tag cnf
-
-  let eval lit =
-    let var, negated = make_var lit in
-    assert (var.pa.is_true || var.na.is_true);
-    let truth = var.pa.is_true in
-    if negated then not truth else truth
-
-  let hyps () = env.clauses
-
-  let history () = env.learnts
-
-  let unsat_conflict () = env.unsat_conflict
-
-  type level = int
-
-  let base_level = 0
-
-  let current_level () = Vec.size env.user_levels
-
-  let push () =
-    let ul_trail = if Vec.is_empty env.trail_lim
-      then base_level
-      else Vec.last env.trail_lim
-    and ul_clauses = Vec.size env.clauses
-    and ul_learnt = Vec.size env.learnts in
-    Vec.push env.user_levels {ul_trail; ul_clauses;ul_learnt};
-    Vec.size env.user_levels
-
-  let pop l =
-    if l > current_level()
-      then invalid_arg "cannot pop() to level, it is too high";
-    let ul = Vec.get env.user_levels l in
-    (* see whether we can reset [env.is_unsat] *)
-    if env.is_unsat && not (Vec.is_empty env.trail_lim) then (
-      (* level at which the decision that lead to unsat was made *)
-      let last = Vec.last env.trail_lim in
-      if ul.ul_trail < last then env.is_unsat <- false
-    );
-    cancel_until ul.ul_trail;
-    Vec.shrink env.clauses ul.ul_clauses;
-    Vec.shrink env.learnts ul.ul_learnt;
-    ()
-
-  let clear () = pop base_level
-end
-*)
diff --git a/solver/solver_types.ml b/solver/solver_types.ml
index e62d8b7d..0da5a0f5 100644
--- a/solver/solver_types.ml
+++ b/solver/solver_types.ml
@@ -15,7 +15,7 @@ open Printf
 
 module type S = Solver_types_intf.S
 
-module Make (L : Log_intf.S)(E : Expr_intf.S)(Th : Plugin_intf.S with
+module McMake (L : Log_intf.S)(E : Expr_intf.S)(Th : Plugin_intf.S with
     type formula = E.Formula.t and type term = E.Term.t) = struct
 
   (* Flag for Mcsat v.s Pure Sat *)
@@ -115,9 +115,9 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)(Th : Plugin_intf.S with
   let t_map = MT.create 4096
 
   let vars = Vec.make 107 (Either.mk_right dummy_var)
-  let nb_vars () = Vec.size vars
-  let get_var i = Vec.get vars i
-  let iter_vars f = Vec.iter f vars
+  let nb_elt () = Vec.size vars
+  let get_elt i = Vec.get vars i
+  let iter_elt f = Vec.iter f vars
 
   let cpt_mk_var = ref 0
 
@@ -189,6 +189,31 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)(Th : Plugin_intf.S with
 
   let empty_clause = make_clause "Empty" [] 0 false (History [])
 
+  (* Decisions & propagations *)
+  type t = (lit, atom) Either.t
+
+  let of_lit = Either.mk_left
+  let of_atom = Either.mk_right
+  let destruct = Either.destruct
+
+  (* Elements *)
+  let elt_of_lit = Either.mk_left
+  let elt_of_var = Either.mk_right
+
+  let destruct_elt = Either.destruct
+
+  let get_elt_id = function
+    | Either.Left l -> l.lid | Either.Right v ->  v.vid
+  let get_elt_level = function
+    | Either.Left (l :lit) -> l.level | Either.Right v ->  v.level
+  let get_elt_weight = function
+    | Either.Left (l : lit) -> l.weight | Either.Right v ->  v.weight
+
+  let set_elt_level e lvl = match e with
+    | Either.Left (l : lit) -> l.level <- lvl | Either.Right v ->  v.level <- lvl
+  let set_elt_weight e w = match e with
+    | Either.Left (l : lit) -> l.weight <- w | Either.Right v ->  v.weight <- w
+
   (* Name generation *)
   let fresh_lname =
     let cpt = ref 0 in
@@ -282,3 +307,259 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)(Th : Plugin_intf.S with
     bprintf b "%s%s{ %a} cpremise={{%a}}" name (if learnt then "!" else ":") pp_atoms_vec arr pp_premise cp
 
 end
+
+module SatMake (L : Log_intf.S)(E : Formula_intf.S)
+    (Th : Theory_intf.S with type formula = E.t ) = struct
+
+  (* Flag for Mcsat v.s Pure Sat *)
+  let mcsat = false
+
+  (* Types declarations *)
+
+  type term = E.t
+  type formula = E.t
+  type proof = Th.proof
+
+  type lit = {
+    lid : int;
+    term : term;
+    mutable level : int;
+    mutable weight : float;
+    mutable assigned : term option;
+  }
+
+  type var = {
+    vid : int;
+    pa : atom;
+    na : atom;
+    mutable seen : bool;
+    mutable level : int;
+    mutable weight : float;
+    mutable reason : reason;
+  }
+
+  and atom = {
+    aid : int;
+    var : var;
+    neg : atom;
+    lit : formula;
+    mutable is_true : bool;
+    mutable watched : clause Vec.t;
+  }
+
+  and clause = {
+    name : string;
+    tag : int option;
+    atoms : atom Vec.t;
+    learnt : bool;
+    cpremise : premise;
+    mutable activity : float;
+    mutable removed : bool;
+  }
+
+  and reason =
+    | Semantic of int
+    | Bcp of clause option
+
+  and premise =
+    | History of clause list
+    | Lemma of proof
+
+  type elt = var
+
+  (* Dummy values *)
+  let dummy_lit = E.dummy
+
+  let rec dummy_var =
+    { vid = -101;
+      pa = dummy_atom;
+      na = dummy_atom;
+      seen = false;
+      level = -1;
+      weight = -1.;
+      reason = Bcp None;
+    }
+  and dummy_atom =
+    { var = dummy_var;
+      lit = dummy_lit;
+      watched = Obj.magic 0;
+      (* should be [Vec.make_empty dummy_clause]
+         but we have to break the cycle *)
+      neg = dummy_atom;
+      is_true = false;
+      aid = -102 }
+  let dummy_clause =
+    { name = "";
+      tag = None;
+      atoms = Vec.make_empty dummy_atom;
+      activity = -1.;
+      removed = false;
+      learnt = false;
+      cpremise = History [] }
+
+  let () =
+    dummy_atom.watched <- Vec.make_empty dummy_clause
+
+  (* Constructors *)
+  module MF = Hashtbl.Make(E)
+
+  let f_map = MF.create 4096
+
+  let vars = Vec.make 107 dummy_var
+  let nb_elt () = Vec.size vars
+  let get_elt i = Vec.get vars i
+  let iter_elt f = Vec.iter f vars
+
+  let cpt_mk_var = ref 0
+
+  let make_semantic_var _ = assert false
+
+  let make_boolean_var =
+    fun lit ->
+      let lit, negated = E.norm lit 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;
+            seen = false;
+            level = -1;
+            weight = 0.;
+            reason = Bcp 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.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 var;
+        var, negated
+
+  let add_term t = make_semantic_var t
+
+  let add_atom lit =
+    let var, negated = make_boolean_var lit in
+    if negated then var.na else var.pa
+
+  let make_clause ?tag name ali sz_ali is_learnt premise =
+    let atoms = Vec.from_list ali sz_ali dummy_atom in
+    { name  = name;
+      tag = tag;
+      atoms = atoms;
+      removed = false;
+      learnt = is_learnt;
+      activity = 0.;
+      cpremise = premise}
+
+  let empty_clause = make_clause "Empty" [] 0 false (History [])
+
+  (* Decisions & propagations *)
+  type t = atom
+
+  let of_lit _ = assert false
+  let of_atom a = a
+  let destruct e _ f = f e
+
+  (* Elements *)
+  let elt_of_lit _ = assert false
+  let elt_of_var v = v
+
+  let destruct_elt v _ f = f v
+
+  let get_elt_id v = v.vid
+  let get_elt_level v = v.level
+  let get_elt_weight v = v.weight
+
+  let set_elt_level v lvl = v.level <- lvl
+  let set_elt_weight v w = v.weight <- w
+
+  (* Name generation *)
+  let fresh_lname =
+    let cpt = ref 0 in
+    fun () -> incr cpt; "L" ^ (string_of_int !cpt)
+
+  let fresh_hname =
+    let cpt = ref 0 in
+    fun () -> incr cpt; "H" ^ (string_of_int !cpt)
+
+  let fresh_tname =
+    let cpt = ref 0 in
+    fun () -> incr cpt; "T" ^ (string_of_int !cpt)
+
+  let fresh_name =
+    let cpt = ref 0 in
+    fun () -> incr cpt; "C" ^ (string_of_int !cpt)
+
+  (* Iteration over subterms *)
+  let iter_sub _ _ = ()
+
+  (* Proof debug info *)
+  let proof_debug _ = assert false
+
+  (* Pretty printing for atoms and clauses *)
+  let print_lit _ _ = assert false
+
+  let print_atom fmt a = E.print fmt a.lit
+
+  let print_atoms fmt v =
+    print_atom fmt (Vec.get v 0);
+    if (Vec.size v) > 1 then begin
+      for i = 1 to (Vec.size v) - 1 do
+        Format.fprintf fmt " ∨ %a" print_atom (Vec.get v i)
+      done
+    end
+
+  let print_clause fmt c =
+    Format.fprintf fmt "%s : %a" c.name print_atoms c.atoms
+
+  (* Complete debug printing *)
+  let sign a = if a == a.var.pa then "" else "-"
+
+  let level a =
+    match a.var.level, a.var.reason with
+    | n, _ when n < 0 -> assert false
+    | 0, Bcp (Some c) -> sprintf "->0/%s" c.name
+    | 0, Bcp None   -> "@0"
+    | n, Bcp (Some c) -> sprintf "->%d/%s" n c.name
+    | n, Bcp None   -> sprintf "@@%d" n
+    | n, Semantic lvl -> sprintf "::%d/%d" n lvl
+
+  let value a =
+    if a.is_true then sprintf "[T%s]" (level a)
+    else if a.neg.is_true then sprintf "[F%s]" (level a)
+    else "[]"
+
+  let pp_premise b = function
+    | History v -> List.iter (fun {name=name} -> bprintf b "%s," name) v
+    | Lemma _ -> bprintf b "th_lemma"
+
+  let pp_assign _ _ = ()
+
+  let pp_lit b v = bprintf b "%d [lit:()]" (v.lid+1)
+
+  let pp_atom b a =
+    bprintf b "%s%d%s[lit:%s]"
+      (sign a) (a.var.vid+1) (value a) (Log.on_fmt E.print a.lit)
+
+  let pp_atoms_vec b vec =
+    for i = 0 to Vec.size vec - 1 do
+      bprintf b "%a ; " pp_atom (Vec.get vec i)
+    done
+
+  let pp_clause b {name=name; atoms=arr; cpremise=cp; learnt=learnt} =
+    bprintf b "%s%s{ %a} cpremise={{%a}}" name (if learnt then "!" else ":") pp_atoms_vec arr pp_premise cp
+
+end
diff --git a/solver/solver_types.mli b/solver/solver_types.mli
index 658b3108..a0eb10c6 100644
--- a/solver/solver_types.mli
+++ b/solver/solver_types.mli
@@ -13,10 +13,17 @@
 
 module type S = Solver_types_intf.S
 
-module Make :
+module McMake :
   functor (L : Log_intf.S) ->
   functor (E : Expr_intf.S) ->
   functor (Th : Plugin_intf.S with type term = E.Term.t and type formula = E.Formula.t) ->
     S with type term = E.Term.t and type formula = E.Formula.t and type proof = Th.proof
 (** Functor to instantiate the types of clauses for a solver. *)
 
+module SatMake :
+  functor (L : Log_intf.S) ->
+  functor (E : Formula_intf.S) ->
+  functor (Th : Theory_intf.S with type formula = E.t) ->
+    S with type term = E.t and type formula = E.t and type proof = Th.proof
+(** Functor to instantiate the types of clauses for a solver. *)
+
diff --git a/solver/solver_types_intf.ml b/solver/solver_types_intf.ml
index 5f185f86..5e1e8f0f 100644
--- a/solver/solver_types_intf.ml
+++ b/solver/solver_types_intf.ml
@@ -16,6 +16,9 @@ module type S = sig
 
   val mcsat : bool
 
+
+  (** {2 Type definitions} *)
+
   type term
   type formula
   type proof
@@ -65,23 +68,48 @@ module type S = sig
     | History of clause list
     | Lemma of proof
 
-  type elt = (lit, var) Either.t
-  (** Recursive types for literals (atoms) and clauses *)
+  (** {2 Decisions and propagations} *)
+  type t
+  (** Either a lit of an atom *)
+
+  val of_lit : lit -> t
+  val of_atom : atom -> t
+  val destruct : t -> (lit -> 'a) -> (atom -> 'a) -> 'a
+  (** Constructors and destructors *)
+
+  (** {2 Elements} *)
+
+  type elt
+  (** Either a lit of a var *)
+
+  val nb_elt : unit -> int
+  val get_elt : int -> elt
+  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
+  val destruct_elt : elt -> (lit -> 'a) -> (var -> 'a) -> 'a
+  (** Constructors & destructor for elements *)
+
+  val get_elt_id : elt -> int
+  val get_elt_level : elt -> int
+  val get_elt_weight : elt -> float
+  val set_elt_level : elt -> int -> unit
+  val set_elt_weight : elt -> float -> unit
+  (** Accessors for elements *)
+
+  (** {2 Variables, Litterals & Clauses } *)
 
   val dummy_var : var
   val dummy_atom : atom
   val dummy_clause : clause
   (** Dummy values for use in vector dummys *)
 
-  val nb_vars : unit -> int
-  val get_var : int -> elt
-  val iter_vars : (elt -> unit) -> unit
-  (** Read access to the vector of variables created *)
-
-  val add_atom : formula -> atom
-  (** Returns the atom associated with the given formula *)
   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 * bool
   (** Returns the variable linked with the given formula, and wether the atom associated with the formula
       is [var.pa] or [var.na] *)
@@ -95,6 +123,8 @@ module type S = sig
   val make_clause : ?tag:int -> string -> atom list -> int -> bool -> premise -> clause
   (** [make_clause name atoms size learnt premise] creates a clause with the given attributes. *)
 
+  (** {2 Proof management} *)
+
   val fresh_name : unit -> string
   val fresh_lname : unit -> string
   val fresh_tname : unit -> string
@@ -104,6 +134,8 @@ module type S = sig
   val proof_debug : proof -> string * (atom list) * (lit list) * (string option)
   (** Debugging info for proofs (see Plugin_intf). *)
 
+  (** {2 Printing} *)
+
   val print_lit : Format.formatter -> lit -> unit
   val print_atom : Format.formatter -> atom -> unit
   val print_clause : Format.formatter -> clause -> unit