diff --git a/Makefile b/Makefile
index 61ec8b80..bdaf5f5a 100644
--- a/Makefile
+++ b/Makefile
@@ -40,7 +40,7 @@ clean:
 
 TO_INSTALL=META $(addprefix _build/,$(LIB) $(NAME).a $(NAME).cmi)
 
-install: all
+install: lib
 	ocamlfind install msat $(TO_INSTALL)
 
 uninstall:
diff --git a/solver/res.ml b/solver/res.ml
index 7332dbd0..894c1515 100644
--- a/solver/res.ml
+++ b/solver/res.ml
@@ -273,14 +273,14 @@ module Make(St : Solver_types.S) = struct
     aux (to_list c, to_list d)
 
   let unsat_core proof =
-    let rec aux proof =
+    let rec aux acc proof =
       let p = proof () in
       match p.step with
-      | Hypothesis | Lemma _ -> [p.conclusion]
+      | Hypothesis | Lemma _ -> p.conclusion :: acc
       | Resolution (proof1, proof2, _) ->
-        List.rev_append (aux proof1) (aux proof2)
+        aux (aux acc proof1) proof2
     in
-    List.sort_uniq compare_cl (aux proof)
+    List.sort_uniq compare_cl (aux [] proof)
 
   (* Print proof graph *)
   let _i = ref 0
diff --git a/solver/solver.ml b/solver/solver.ml
index bed43a67..b90506fd 100644
--- a/solver/solver.ml
+++ b/solver/solver.ml
@@ -359,19 +359,19 @@ module Make (L : Log_intf.S)(F : Formula_intf.S)
   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 v -> atoms, [init0]
-              | Lemma p -> assert false
-          else
-              a::atoms, init
-      in
-      let atoms, init = List.fold_left aux ([], []) atoms in
-      List.fast_sort (fun a b -> a.var.vid - b.var.vid) atoms, init
+    (* 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 v -> atoms, [init0]
+            | Lemma p -> assert false
+        else
+            a::atoms, init
+    in
+    let atoms, init = List.fold_left aux ([], []) 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