From c2cfa14e862ef944f2d371e90af11fd0d361cc3f Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Fri, 6 Feb 2015 17:47:29 +0100
Subject: [PATCH] small perf change

---
 solver/res.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

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