diff --git a/common/iheap.ml b/common/iheap.ml
index 63e12aa5..228e78eb 100644
--- a/common/iheap.ml
+++ b/common/iheap.ml
@@ -13,7 +13,7 @@
 
 type t = {heap : int Vec.t; indices : int Vec.t }
 
-let dummy = -100
+let dummy = 0
 
 let init sz =
   { heap    =  Vec.init sz (fun i -> i) dummy;
@@ -96,6 +96,11 @@ let size s = Vec.size s.heap
 
 let is_empty s = Vec.is_empty s.heap
 
+let clear {heap; indices} =
+  Vec.clear heap;
+  Vec.clear indices;
+  ()
+
 let insert cmp s n =
   if not (in_heap s n) then
     begin
@@ -123,6 +128,7 @@ let update cmp s n =
 *)
 
 let remove_min cmp ({heap=heap; indices=indices} as s) =
+  if Vec.size heap=0 then raise Not_found;
   let x = Vec.get heap 0 in
   Vec.set heap 0 (Vec.last heap); (*heap.last()*)
   Vec.set indices (Vec.get heap 0) 0;
diff --git a/common/iheap.mli b/common/iheap.mli
index dbbea23f..0c5ace86 100644
--- a/common/iheap.mli
+++ b/common/iheap.mli
@@ -12,15 +12,44 @@
 (**************************************************************************)
 
 type t
+(** Heap of integers, whose priority is increased or decreased
+    incrementally (see {!decrease} for instance) *)
 
 val init : int -> t
+(** Create a heap with the given number of values inside.
+    [init len] contains integers from [0] to [len-1]. *)
+
 val in_heap : t -> int -> bool
+(** [in_heap h x] returns [true] iff [x] is among the integers that belong to
+    the heap. *)
+
 val decrease : (int -> int -> bool) -> t -> int -> unit
+(** [decrease cmp h x] decreases the value associated to [x] within [h],
+    according to the comparison function [cmp] *)
+
 (*val increase : (int -> int -> bool) -> t -> int -> unit*)
+
 val size : t -> int
+(** Number of integers within the heap *)
+
 val is_empty : t -> bool
+
+val clear : t -> unit
+(** Clear the content of the heap *)
+
 val insert : (int -> int -> bool) -> t -> int -> unit
+(** Insert a new integer into the heap, according to the given comparison *)
+
 val grow_to_by_double: t -> int -> unit
+(** Augment the internal capacity of the heap until it reaches at
+    least the given integer *)
+
 (*val update : (int -> int -> bool) -> t -> int -> unit*)
+
 val remove_min : (int -> int -> bool) -> t -> int
+(** Remove and return the integer that has the lowest value from the heap
+    @raise Not_found if the heap is empty *)
+
 val filter : t -> (int -> bool) -> (int -> int -> bool) -> unit
+(** Filter out values that don't satisfy the predicate. A comparison
+    function is used to re-order the heap *)
diff --git a/common/vec.ml b/common/vec.ml
index 791f62ea..5738d626 100644
--- a/common/vec.ml
+++ b/common/vec.ml
@@ -119,6 +119,16 @@ let fold f acc t =
       _fold f acc' t (i+1)
   in _fold f acc t 0
 
+exception ExitVec
+
+let exists p t =
+  try
+    for i = 0 to t.sz - 1 do
+      if p (Array.unsafe_get t.data i) then raise ExitVec
+    done;
+    false
+  with ExitVec -> true
+
 (*
 template<class V, class T>
 static inline void remove(V& ts, const T& t)
diff --git a/common/vec.mli b/common/vec.mli
index d5db6ffb..bc990b7f 100644
--- a/common/vec.mli
+++ b/common/vec.mli
@@ -90,3 +90,6 @@ val iter : ('a -> unit) -> 'a t -> unit
 val fold : ('b -> 'a -> 'b) -> 'b -> 'a t -> 'b
 (** Fold over elements *)
 
+val exists : ('a -> bool) -> 'a t -> bool
+(** Does there exist an element that satisfies the predicate? *)
+
diff --git a/docs/mcsat-vmcai2013.pdf b/docs/mcsat-vmcai2013.pdf
new file mode 100644
index 00000000..e89e32d7
Binary files /dev/null and b/docs/mcsat-vmcai2013.pdf differ
diff --git a/docs/mcsat_design.pdf b/docs/mcsat_design.pdf
new file mode 100644
index 00000000..60ed51f0
Binary files /dev/null and b/docs/mcsat_design.pdf differ
diff --git a/docs/minisat.pdf b/docs/minisat.pdf
new file mode 100644
index 00000000..21de5cdf
Binary files /dev/null and b/docs/minisat.pdf differ
diff --git a/sat/sat.ml b/sat/sat.ml
index 869befec..01105aca 100644
--- a/sat/sat.ml
+++ b/sat/sat.ml
@@ -23,9 +23,9 @@ module Fsat = struct
   let neg a = - a
   let norm a = abs a, a < 0
 
-  let hash = Hashtbl.hash
-  let equal = (=)
-  let compare = Pervasives.compare
+  let hash (a:int) = Hashtbl.hash a
+  let equal (a:int) b = a=b
+  let compare (a:int) b = Pervasives.compare a b
 
   let _str = Hstring.make ""
   let label a = _str
@@ -107,14 +107,14 @@ module Make(Dummy : sig end) = struct
   let solve () =
     try
       SatSolver.solve ();
-      assert false
-    with
-    | SatSolver.Sat -> Sat
-    | SatSolver.Unsat _ -> Unsat
+      Sat
+    with SatSolver.Unsat _ -> Unsat
 
   let assume l =
     incr _i;
-    SatSolver.assume l !_i
+    try
+      SatSolver.assume l !_i
+    with SatSolver.Unsat _ -> ()
 
   let eval = SatSolver.eval
 end
diff --git a/sat/sat.mli b/sat/sat.mli
index 1ef2fdc4..bf3bc55f 100644
--- a/sat/sat.mli
+++ b/sat/sat.mli
@@ -26,7 +26,8 @@ module Make(Dummy: sig end) : sig
   val hash : atom -> int
   val equal : atom -> atom -> bool
   val compare : atom -> atom -> int
-  (** Usual hash and comparison functions. For now, directly uses Pervasives and Hashtbl builtins. *)
+  (** Usual hash and comparison functions. For now, directly uses
+      [Pervasives] and [Hashtbl] builtins. *)
 
   val print_atom : Format.formatter -> atom -> unit
   (** Print the atom on the given formatter. *)
diff --git a/sat/solver.ml b/sat/solver.ml
index c1dc90cd..dd8789fc 100644
--- a/sat/solver.ml
+++ b/sat/solver.ml
@@ -22,57 +22,80 @@ module Make (F : Formula_intf.S)
   exception Restart
   exception Conflict of clause
 
+  (* Singleton type containing the current state *)
   type env = {
-    (* si true_, les contraintes sont deja fausses *)
+
     mutable is_unsat : bool;
+    (* if [true], constraints are already false *)
+
     mutable unsat_core : clause list;
-    (* clauses du probleme *)
-    mutable clauses : clause Vec.t;
-    (* clauses apprises *)
-    mutable learnts : clause Vec.t;
-    (* valeur de l'increment pour l'activite des clauses *)
+    (* clauses that imply false, if any  *)
+
+    clauses : clause Vec.t;
+    (* all currently active clauses *)
+
+    learnts : clause Vec.t;
+    (* learnt clauses  *)
+
     mutable clause_inc : float;
-    (* valeur de l'increment pour l'activite des variables *)
+    (* increment for clauses' activity *)
+
     mutable var_inc : float;
-    (* un vecteur des variables du probleme *)
-    mutable vars : var Vec.t;
-    (* la pile de decisions avec les faits impliques *)
-    mutable trail : atom Vec.t;
-    (* une pile qui pointe vers les niveaux de decision dans trail *)
-    mutable trail_lim : int Vec.t;
-    (* Tete de la File des faits unitaires a propager.
-       	   C'est un index vers le trail *)
+    (* increment for variables' activity *)
+
+    vars : var Vec.t;
+    (* all boolean variables *)
+
+    trail : atom Vec.t;
+    (* decision stack + propagated atoms *)
+
+    trail_lim : int Vec.t;
+    (* decision levels in [trail]  *)
+
+    levels : int Vec.t;
+    (* user-defined levels. Subset of [trail_lim] *)
+
     mutable qhead : int;
-    (* Nombre des assignements top-level depuis la derniere
-       execution de 'simplify()' *)
+    (* Start offset in the queue of unit facts to propagate, within the trail *)
+
     mutable simpDB_assigns : int;
-    (* Nombre restant de propagations a faire avant la prochaine
-       execution de 'simplify()' *)
+    (* number of toplevel assignments since last call to [simplify ()] *)
+
     mutable simpDB_props : int;
-    (* Un tas ordone en fonction de l'activite des variables *)
-    mutable order : Iheap.t;
-    (* estimation de progressions, mis a jour par 'search()' *)
+    (* 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;
-    (* inverse du facteur d'acitivte des variables, vaut 1/0.999 par defaut *)
+
     var_decay : float;
-    (* inverse du facteur d'activite des clauses, vaut 1/0.95 par defaut *)
+    (* inverse of the activity factor for variables. Default 1/0.999 *)
+
     clause_decay : float;
-    (* la limite de restart initiale, vaut 100 par defaut *)
+    (* inverse of the activity factor for clauses. Default 1/0.95 *)
+
     mutable restart_first : int;
-    (* facteur de multiplication de restart limite, vaut 1.5 par defaut*)
+    (* intial restart limit, default 100 *)
+
     restart_inc : float;
-    (* limite initiale du nombre de clause apprises, vaut 1/3
-       des clauses originales par defaut *)
+    (* multiplicative factor for restart limit, default 1.5 *)
+
     mutable learntsize_factor : float;
-    (* multiplier learntsize_factor par cette valeur a chaque restart,
-       vaut 1.1 par defaut *)
+    (* initial limit for the number of learnt clauses, 1/3 of initial
+        number of clauses by default *)
+
     learntsize_inc : float;
-    (* controler la minimisation des clauses conflit, vaut true par defaut *)
+    (* multiplicative factor for [learntsize_factor] at each restart, default 1.1 *)
+
     expensive_ccmin : bool;
-    (* controle la polarite a choisir lors de la decision *)
+    (* control minimization of conflict clause, default true *)
+
     polarity_mode : bool;
+    (* default polarity for decision *)
 
     mutable starts : int;
     mutable decisions : int;
@@ -90,28 +113,21 @@ module Make (F : Formula_intf.S)
     mutable tatoms_queue : atom Queue.t;
   }
 
-  type state = {
-    env : env;
-    st_cpt_mk_var: int;
-    st_ma : varmap;
-  }
-
-  type t = state
-
   let env = {
     is_unsat = false;
     unsat_core = [] ;
-    clauses = Vec.make 0 dummy_clause; (*sera mis a jour lors du parsing*)
-    learnts = Vec.make 0 dummy_clause; (*sera mis a jour lors du parsing*)
+    clauses = Vec.make 0 dummy_clause; (*updated during parsing*)
+    learnts = Vec.make 0 dummy_clause; (*updated during parsing*)
     clause_inc = 1.;
     var_inc = 1.;
-    vars = Vec.make 0 dummy_var; (*sera mis a jour lors du parsing*)
+    vars = Vec.make 0 dummy_var; (*updated during parsing*)
     trail = Vec.make 601 dummy_atom;
-    trail_lim = Vec.make 601 (-105);
+    trail_lim = Vec.make 601 (-1);
+    levels =  Vec.make 20 (-1);
     qhead = 0;
     simpDB_assigns = -1;
     simpDB_props = 0;
-    order = Iheap.init 0; (* sera mis a jour dans solve *)
+    order = Iheap.init 0; (* updated in solve *)
     progress_estimate = 0.;
     remove_satisfied = true;
     var_decay = 1. /. 0.95;
@@ -138,7 +154,6 @@ module Make (F : Formula_intf.S)
     tatoms_queue = Queue.create ();
   }
 
-
   let f_weight i j =
     (Vec.get env.vars j).weight < (Vec.get env.vars i).weight
 
@@ -214,14 +229,9 @@ module Make (F : Formula_intf.S)
   let remove_clause c = detach_clause c
 
   let satisfied c =
-    try
-      for i = 0 to Vec.size c.atoms - 1 do
-        if (Vec.get c.atoms i).is_true then raise Exit
-      done;
-      false
-    with Exit -> true
+    Vec.exists (fun atom -> atom.is_true) c.atoms
 
-  (* annule tout jusqu'a lvl *exclu*  *)
+  (* cancel down to [lvl] excluded *)
   let cancel_until lvl =
     Log.debug 5 "Bactracking to decision level %d (excluded)" lvl;
     if decision_level () > lvl then begin
@@ -255,7 +265,7 @@ module Make (F : Formula_intf.S)
   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);
-    (* Garder la reason car elle est utile pour les unsat-core *)
+    (* 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;
@@ -278,22 +288,22 @@ module Make (F : Formula_intf.S)
   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 (* le literal faux doit etre dans .(1) *)
+    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
-      (* clause vraie, la garder dans les watched *)
+      (* true clause, keep it in watched *)
       Vec.set watched !new_sz c;
       incr new_sz;
     end
     else
-      try (* chercher un nouveau watcher *)
+      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
-            (* Watcher Trouve: mettre a jour et sortir *)
+            (* watch lit found: update and exit *)
             Vec.set atoms 1 ak;
             Vec.set atoms k a.neg;
             Vec.push ak.neg.watched c;
@@ -301,9 +311,9 @@ module Make (F : Formula_intf.S)
             raise Exit
           end
         done;
-        (* Watcher NON Trouve *)
+        (* no watch lit found *)
         if first.neg.is_true then begin
-          (* la clause est fausse *)
+          (* 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);
@@ -313,7 +323,7 @@ module Make (F : Formula_intf.S)
           raise (Conflict c)
         end
         else begin
-          (* la clause est unitaire *)
+          (* clause is unit *)
           Vec.set watched !new_sz c;
           incr new_sz;
           Log.debug 5 "Unit clause : %a" St.pp_clause c;
@@ -375,6 +385,7 @@ module Make (F : Formula_intf.S)
       (* eprintf "th inconsistent : %a @." Ex.print dep; *)
       Some dep
 
+  (* boolean propagation, using unit clauses *)
   let propagate () =
     let num_props = ref 0 in
     let res = ref None in
@@ -390,6 +401,7 @@ module Make (F : Formula_intf.S)
     env.simpDB_props <- env.simpDB_props - !num_props;
     !res
 
+  (* conflict analysis *)
   let analyze c_clause =
     let pathC  = ref 0 in
     let learnt = ref [] in
@@ -437,6 +449,8 @@ module Make (F : Formula_intf.S)
     List.iter (fun q -> q.var.seen <- false) !seen;
     !blevel, !learnt, !history, !size
 
+  (* 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
@@ -446,18 +460,18 @@ module Make (F : Formula_intf.S)
     if sz1 > 2 && (sz2 = 2 || c < 0) then -1
     else 1
 
-  let locked c = false(*
-      try
-        for i = 0 to Vec.size env.vars - 1 do
-          match (Vec.get env.vars i).reason with
-            | Some c' when c ==c' -> raise Exit
-            | _ -> ()
-        done;
-        false
-      with Exit -> true*)
+  (* 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 =
+    Vec.exists
+      (fun v -> match v.reason with
+        | Some c' -> c ==c'
+        | _ -> false
+      ) env.vars
 
-  let reduce_db () = ()
-    (*
+  (* 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
@@ -478,8 +492,8 @@ module Make (F : Formula_intf.S)
           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 =
     let j = ref 0 in
     let k = Vec.size vec - 1 in
@@ -633,7 +647,7 @@ module Make (F : Formula_intf.S)
     var_decay_activity ();
     clause_decay_activity ()
 
-  let check_inconsistence_of dep =
+  let check_inconsistency_of dep =
     try
       let env = ref (Th.empty()) in ();
       Ex.iter_atoms
@@ -657,7 +671,7 @@ module Make (F : Formula_intf.S)
         ) dep ([], 0, 0, [])
     in
     if atoms = [] then begin
-      (* check_inconsistence_of dep; *)
+      (* check_inconsistency_of dep; *)
       report_t_unsat dep
       (* une conjonction de faits unitaires etaient deja unsat *)
     end;
@@ -711,8 +725,6 @@ module Make (F : Formula_intf.S)
     List.iter (fun q -> q.var.seen <- false) !seen;
     !blevel, !learnt, !history, !size
 
-
-
   let add_boolean_conflict confl =
     env.conflicts <- env.conflicts + 1;
     if decision_level() = 0 then report_b_unsat confl; (* Top-level conflict *)
@@ -740,7 +752,7 @@ module Make (F : Formula_intf.S)
           record_learnt_clause blevel learnt history size
 
         | None ->
-          if nb_assigns () = env.nb_init_vars then raise Sat;
+          if nb_assigns() = env.nb_init_vars then raise Sat;
           if n_of_conflicts >= 0 && !conflictC >= n_of_conflicts then
             begin
               env.progress_estimate <- progress_estimate();
@@ -779,28 +791,30 @@ module Make (F : Formula_intf.S)
     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 env.unsat_core);
     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
-        (try search (to_int !n_of_conflicts) (to_int !n_of_learnts);
-         with Restart -> ());
+        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 ->
-      (*check_model ();*)
-      raise Sat
+    | Sat -> ()
     | (Unsat cl) as e ->
       (* check_unsat_core cl; *)
       raise e
 
   exception Trivial
 
+  (* TODO: could be more efficient than [@] everywhere? *)
   let partition atoms init =
     let rec partition_aux trues unassigned falses init = function
       | [] -> trues @ unassigned @ falses, init
@@ -888,87 +902,38 @@ module Make (F : Formula_intf.S)
     let cnf = List.map (List.map St.add_atom) cnf in
     init_solver cnf ~cnumber
 
-  let clear () =
-    let empty_theory = Th.empty () in
-    env.is_unsat <- false;
-    env.unsat_core <- [];
-    env.clauses <- Vec.make 0 dummy_clause;
-    env.learnts <- Vec.make 0 dummy_clause;
-    env.clause_inc <- 1.;
-    env.var_inc <- 1.;
-    env.vars <- Vec.make 0 dummy_var;
-    env.qhead <- 0;
-    env.simpDB_assigns <- -1;
-    env.simpDB_props <- 0;
-    env.order <- Iheap.init 0; (* sera mis a jour dans solve *)
-    env.progress_estimate <- 0.;
-    env.restart_first <- 100;
-    env.starts <- 0;
-    env.decisions <- 0;
-    env.propagations <- 0;
-    env.conflicts <- 0;
-    env.clauses_literals <- 0;
-    env.learnts_literals <- 0;
-    env.max_literals <- 0;
-    env.tot_literals <- 0;
-    env.nb_init_vars <- 0;
-    env.nb_init_clauses <- 0;
-    env.tenv <- empty_theory;
-    env.model <- Vec.make 0 dummy_var;
-    env.trail <- Vec.make 601 dummy_atom;
-    env.trail_lim <- Vec.make 601 (-105);
-    env.tenv_queue <- Vec.make 100 Th.dummy;
-    env.tatoms_queue <- Queue.create ();
-    St.clear ()
-
-  let copy (v : 'a) : 'a = Marshal.from_string (Marshal.to_string v []) 0
-
-  let save () =
-    let sv =
-      { env = env;
-        st_cpt_mk_var = !St.cpt_mk_var;
-        st_ma = !St.ma }
-    in
-    copy sv
-
-  let restore { env = s_env; st_cpt_mk_var = st_cpt_mk_var; st_ma = st_ma } =
-    env.is_unsat <- s_env.is_unsat;
-    env.unsat_core <- s_env.unsat_core;
-    env.clauses <- s_env.clauses;
-    env.learnts <- s_env.learnts;
-    env.clause_inc <- s_env.clause_inc;
-    env.var_inc <- s_env.var_inc;
-    env.vars <- s_env.vars;
-    env.qhead <- s_env.qhead;
-    env.simpDB_assigns <- s_env.simpDB_assigns;
-    env.simpDB_props <- s_env.simpDB_props;
-    env.order <- s_env.order;
-    env.progress_estimate <- s_env.progress_estimate;
-    env.restart_first <- s_env.restart_first;
-    env.starts <- s_env.starts;
-    env.decisions <- s_env.decisions;
-    env.propagations <- s_env.propagations;
-    env.conflicts <- s_env.conflicts;
-    env.clauses_literals <- s_env.clauses_literals;
-    env.learnts_literals <- s_env.learnts_literals;
-    env.max_literals <- s_env.max_literals;
-    env.tot_literals <- s_env.tot_literals;
-    env.nb_init_vars <- s_env.nb_init_vars;
-    env.nb_init_clauses <- s_env.nb_init_clauses;
-    env.tenv <- s_env.tenv;
-    env.model <- s_env.model;
-    env.trail <- s_env.trail;
-    env.trail_lim <- s_env.trail_lim;
-    env.tenv_queue <- s_env.tenv_queue;
-    env.tatoms_queue <- s_env.tatoms_queue;
-    env.learntsize_factor <- s_env.learntsize_factor;
-    St.cpt_mk_var := st_cpt_mk_var;
-    St.ma := st_ma
-
   let eval lit =
     let var, negated = make_var lit in
     let truth = var.pa.is_true in
     if negated then not truth else truth
 
+  type level = int
+
+  let base_level = 0
+
+  let current_level() =
+    if Vec.is_empty env.levels then base_level else Vec.last env.levels
+
+  let push () =
+    let l = if Vec.is_empty env.trail_lim
+      then base_level
+      else Vec.last env.trail_lim
+    in
+    Vec.push env.levels l;
+    l
+
+  let pop l =
+    if l > current_level()
+      then invalid_arg "cannot pop() to level, it is too high";
+    let i = Vec.get env.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 i < last then env.is_unsat <- false
+    );
+    cancel_until i
+
+  let clear () = pop base_level
 end
 
diff --git a/sat/solver.mli b/sat/solver.mli
index 97f93d01..3f472335 100644
--- a/sat/solver.mli
+++ b/sat/solver.mli
@@ -14,34 +14,44 @@
 module Make (F : Formula_intf.S)
     (St : Solver_types.S with type formula = F.t)
     (Ex : Explanation.S with type atom = St.atom)
-    (Th : Theory_intf.S with type formula = F.t and type explanation = Ex.t) : sig
-  (** Functor to create a SMT Solver parametrised by the atomic formulas and a theory. *)
-
-  exception Sat
+    (Th : Theory_intf.S with type formula = F.t and type explanation = Ex.t) :
+sig
+  (** Functor to create a SMT Solver parametrised by the atomic
+      formulas and a theory. *)
+  
   exception Unsat of St.clause list
-  (** Exceptions raised by the [solve] function to return the nature of the current set of assummtions.
-      Once the [Unsat] exception is raised, the solver needs to be cleared before anything else is done. *)
-
-  type t
-  (** The type of the state of the sat solver. Mutable.*)
 
   val solve : unit -> unit
   (** Try and solves the current set of assumptions.
-      @raise Sat if the current set of assummptions is satisfiable.
-      @raise Unsat if the current set of assumptions is unsatisfiable *)
+      @return () if the current set of clauses is satisfiable
+      @raise Unsat if a toplevel conflict is found *)
 
-  val assume : F.t list list -> cnumber : int -> unit
-  (** Add the list of clauses to the current set of assumptions. Modifies the sat solver state in place. *)
-
-  val clear : unit -> unit
-  (** Resets everything done. Basically returns the solver to a state similar to when the module was created. *)
+  val assume : F.t list list -> cnumber:int -> unit
+  (** Add the list of clauses to the current set of assumptions.
+      Modifies the sat solver state in place.
+      @raise Unsat if a conflict is detect when adding the clauses *)
 
   val eval : F.t -> bool
-  (** Returns the valuation of a formula in the current state of the sat solver. *)
+  (** Returns the valuation of a formula in the current state
+      of the sat solver. *)
 
-  val save : unit -> t
-  val restore : t -> unit
-  (** Functions to be replaced by push&pop functions. *)
+  type level
+  (** Abstract notion of assumption level. *)
 
+  val base_level : level
+  (** Level with no assumption at all, corresponding to the empty solver *)
+
+  val current_level : unit -> level
+  (** The current level *)
+
+  val push : unit -> level
+  (** Create a new level that extends the previous one. *)
+
+  val pop : level -> unit
+  (** Go back to the given level, forgetting every assumption added since.
+      @raise Invalid_argument if the current level is below the argument *)
+
+  val clear : unit -> unit
+  (** Return to level {!base_level} *)
 end
 
diff --git a/sat/theory_intf.ml b/sat/theory_intf.ml
index a6d1e169..1dce23ab 100644
--- a/sat/theory_intf.ml
+++ b/sat/theory_intf.ml
@@ -40,6 +40,7 @@ module type S = sig
   val assume : cs:bool -> formula -> explanation -> t -> t
   (** Return a new theory state with the formula as assumption.
       @raise Inconsistent if the new state would be inconsistent. *)
+  (* TODO: remove (apparently) useless [cs] parameter *)
 
 end