diff --git a/src/core/external.ml b/src/core/external.ml
index ae2e0d92..fbce74fe 100644
--- a/src/core/external.ml
+++ b/src/core/external.ml
@@ -84,12 +84,13 @@ module Make
 
   let mk_unsat () : (_,_) unsat_state =
     pp_all 99;
-    let unsat_conflict () = match S.unsat_conflict () with
+    let unsat_conflict () =
+      match S.unsat_conflict () with
       | None -> assert false
       | Some c -> c
     in
     let get_proof () =
-      let c = unsat_conflict() in
+      let c = unsat_conflict () in
       S.Proof.prove_unsat c
     in
     { unsat_conflict; get_proof; }
diff --git a/src/core/internal.ml b/src/core/internal.ml
index bee00c77..ac6acb47 100644
--- a/src/core/internal.ml
+++ b/src/core/internal.ml
@@ -224,7 +224,7 @@ module Make
     | E_lit l -> Iheap.insert f_weight env.order l.lid
     | E_var v ->
       Iheap.insert f_weight env.order v.vid;
-      iter_sub (fun t -> insert_var_order (E_lit t)) v
+      iter_sub (fun t -> insert_var_order (elt_of_lit t)) v
 
   (* Rather than iterate over all the heap when we want to decrease all the
      variables/literals activity, we instead increase the value by which
@@ -358,23 +358,15 @@ module Make
      A clause is attached (to its watching lits) when it is first added,
      either because it is assumed or learnt.
 
-     A clause is detached once it dies (because of pop())
   *)
   let attach_clause c =
-    if not c.attached then begin
-      Log.debugf 60 "Attaching %a" (fun k -> k St.pp_clause c);
-      c.attached <- true;
-      Vec.push c.atoms.(0).neg.watched c;
-      Vec.push c.atoms.(1).neg.watched c;
-    end
-
-  let detach_clause c =
-    if c.attached then begin
-      c.attached <- false;
-      Log.debugf 10 "Removing clause @[%a@]" (fun k->k St.pp_clause c);
-      Vec.remove c.atoms.(0).neg.watched c;
-      Vec.remove c.atoms.(1).neg.watched c;
-    end
+    assert (not c.attached);
+    Log.debugf 60 "Attaching %a" (fun k -> k St.pp_clause c);
+    Array.iter (fun x -> insert_var_order (elt_of_var x.var)) c.atoms;
+    Vec.push c.atoms.(0).neg.watched c;
+    Vec.push c.atoms.(1).neg.watched c;
+    c.attached <- true;
+    ()
 
   (* Is a clause satisfied ? *)
   let satisfied c = Array_util.exists (fun atom -> atom.is_true) c.atoms
@@ -825,7 +817,6 @@ module Make
       let nbv = St.nb_elt () in
       let nbc = env.nb_init_clauses + Stack.length env.clauses_to_add in
       Iheap.grow_to_by_double env.order nbv;
-      St.iter_elt insert_var_order;
       Vec.grow_to_by_double env.clauses_hyps nbc;
       Vec.grow_to_by_double env.clauses_learnt nbc;
       env.nb_init_clauses <- nbc;
@@ -1128,13 +1119,14 @@ module Make
             n_of_learnts   := !n_of_learnts *. env.learntsize_inc
           | Sat ->
             assert (env.elt_head = Vec.size env.elt_queue);
-            Plugin.if_sat (full_slice ());
-            flush_clauses();
-            if is_unsat () then raise Unsat
-            else if env.elt_head = Vec.size env.elt_queue (* sanity check *)
-                 && env.elt_head = St.nb_elt ()
-                 (* this is the important test to know if the search is finished *)
-            then raise Sat
+            begin match Plugin.if_sat (full_slice ()) with
+              | Plugin_intf.Sat -> ()
+              | Plugin_intf.Unsat (l, p) ->
+                let atoms = List.rev_map new_atom l in
+                let c = make_clause (fresh_tname ()) atoms (Lemma p) in
+                Stack.push c env.clauses_to_add
+            end;
+            if Stack.is_empty env.clauses_to_add then raise Sat
         end
       done
     with Sat -> ()
@@ -1206,6 +1198,26 @@ module Make
       List.iter aux l
     | Some _ -> ()
 
+  (* Check satisfiability *)
+  let check_clause c =
+    Array_util.exists (fun a -> a.is_true) c.atoms
+
+  let check_vec v =
+    Vec.for_all check_clause v
+
+  let check_stack s =
+    try
+      Stack.iter (fun c -> if not (check_clause c) then raise Exit) s;
+      true
+    with Exit ->
+      false
+
+  let check () =
+    Stack.is_empty env.clauses_to_add &&
+    check_stack env.clauses_root &&
+    check_vec env.clauses_hyps &&
+    check_vec env.clauses_learnt &&
+    check_vec env.clauses_temp
 
   (* Unsafe access to internal data *)
 
diff --git a/src/core/internal.mli b/src/core/internal.mli
index 74870673..0ac8fa72 100644
--- a/src/core/internal.mli
+++ b/src/core/internal.mli
@@ -61,6 +61,9 @@ module Make
   val model : unit -> (St.term * St.term) list
   (** Returns the model found if the formula is satisfiable. *)
 
+  val check : unit -> bool
+  (** Check the satisfiability of the current model. Only has meaning
+      if the solver finished proof search and has returned [Sat]. *)
 
   (** {2 Internal data}
       These functions expose some internal data stored by the solver, as such
diff --git a/src/core/plugin_intf.ml b/src/core/plugin_intf.ml
index afe5c526..8400959f 100644
--- a/src/core/plugin_intf.ml
+++ b/src/core/plugin_intf.ml
@@ -71,14 +71,15 @@ module type S = sig
   (** Assume the formulas in the slice, possibly pushing new formulas to be propagated,
       and returns the result of the new assumptions. *)
 
+  val if_sat : (term, formula, proof) slice -> (formula, proof) res
+  (** Called at the end of the search in case a model has been found. If no new clause is
+      pushed and the function returns [Sat], then proof search ends and 'sat' is returned,
+      else search is resumed. *)
+
   val backtrack : level -> unit
   (** Backtrack to the given level. After a call to [backtrack l], the theory should be in the
       same state as when it returned the value [l], *)
 
-  val if_sat : (term, formula, proof) slice -> unit
-  (** Called at the end of the search in case a model has been found. If no new clause is
-      pushed, then 'sat' is returned, else search is resumed. *)
-
   val assign : term -> term
   (** Returns an assignment value for the given term. *)
 
diff --git a/src/core/theory_intf.ml b/src/core/theory_intf.ml
index 2cdd121f..d02a0017 100644
--- a/src/core/theory_intf.ml
+++ b/src/core/theory_intf.ml
@@ -53,13 +53,13 @@ module type S = sig
   (** Assume the formulas in the slice, possibly pushing new formulas to be propagated,
       and returns the result of the new assumptions. *)
 
+  val if_sat : (formula, proof) slice -> (formula, proof) res
+  (** Called at the end of the search in case a model has been found. If no new clause is
+      pushed, then 'sat' is returned, else search is resumed. *)
+
   val backtrack : level -> unit
   (** Backtrack to the given level. After a call to [backtrack l], the theory should be in the
       same state as when it returned the value [l], *)
 
-  val if_sat : (formula, proof) slice -> unit
-  (** Called at the end of the search in case a model has been found. If no new clause is
-      pushed, then 'sat' is returned, else search is resumed. *)
-
 end
 
diff --git a/src/example/mcsat.ml b/src/example/mcsat.ml
index 9be8e7bc..d5c42683 100644
--- a/src/example/mcsat.ml
+++ b/src/example/mcsat.ml
@@ -90,7 +90,8 @@ module Tsmt = struct
           Plugin_intf.Unknown
       end
 
-  let if_sat _ = ()
+  let if_sat _ =
+    Plugin_intf.Sat
 
 end
 
diff --git a/src/example/smt.ml b/src/example/smt.ml
index 10eafb4c..0f25bcba 100644
--- a/src/example/smt.ml
+++ b/src/example/smt.ml
@@ -46,9 +46,9 @@ module Tsmt = struct
       Log.debug 8 "Making explanation clause...";
       Unsat (to_clause x, ())
 
-  let backtrack l = env := l
+  let if_sat _ = Theory_intf.Sat
 
-  let if_sat _ = ()
+  let backtrack l = env := l
 
 end
 
diff --git a/src/main.ml b/src/main.ml
index 866c29c0..49fb2686 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -287,3 +287,4 @@ let () =
   | Out_of_space ->
     print "Spaceout";
     exit 3
+
diff --git a/src/solver/solver.ml b/src/solver/solver.ml
index 274d3962..8a25c126 100644
--- a/src/solver/solver.ml
+++ b/src/solver/solver.ml
@@ -24,7 +24,7 @@ module DummyTheory(F : Formula_intf.S) = struct
   let current_level () = ()
   let assume _ = Theory_intf.Sat
   let backtrack _ = ()
-  let if_sat _ = ()
+  let if_sat _ = Theory_intf.Sat
 end
 
 module Plugin(E : Formula_intf.S)