diff --git a/src/core/internal.ml b/src/core/internal.ml
index efcb5657..b7050eb6 100644
--- a/src/core/internal.ml
+++ b/src/core/internal.ml
@@ -437,7 +437,7 @@ module Make
     end
 
   (* Is a clause satisfied ? *)
-  let satisfied c = Array.exists (fun atom -> atom.is_true) c.atoms
+  let satisfied c = Array_util.exists (fun atom -> atom.is_true) c.atoms
 
   (* Backtracking.
      Used to backtrack, i.e cancel down to [lvl] excluded,
@@ -717,7 +717,7 @@ module Make
   let add_boolean_conflict confl =
     env.next_decision <- None;
     env.conflicts <- env.conflicts + 1;
-    if decision_level() = 0 || Array.for_all (fun a -> a.var.v_level = 0) confl.atoms then
+    if decision_level() = 0 || Array_util.for_all (fun a -> a.var.v_level = 0) confl.atoms then
       report_unsat confl; (* Top-level conflict *)
     let blevel, learnt, history, is_uip = analyze confl in
     cancel_until blevel;
diff --git a/src/util/array_util.ml b/src/util/array_util.ml
new file mode 100644
index 00000000..2c3894ee
--- /dev/null
+++ b/src/util/array_util.ml
@@ -0,0 +1,24 @@
+
+(*
+MSAT is free software, using the Apache license, see file LICENSE
+Copyright 2014 Guillaume Bury
+Copyright 2014 Simon Cruanes
+*)
+
+(** {1 Utils for Arrays} *)
+
+let exists p a =
+  let n = Array.length a in
+  let rec loop i =
+    if i = n then false
+    else if p (Array.unsafe_get a i) then true
+    else loop (succ i) in
+  loop 0
+
+let for_all p a =
+  let n = Array.length a in
+  let rec loop i =
+    if i = n then true
+    else if p (Array.unsafe_get a i) then loop (succ i)
+    else false in
+  loop 0