diff --git a/META b/META
index 30e06fbb..f2ed910c 100644
--- a/META
+++ b/META
@@ -1,7 +1,7 @@
 name="msat"
 version="dev"
 description="MSAT is a modular SAT solver, plus extensions"
-requires="num unix"
+requires=""
 archive(byte) = "msat.cma"
 archive(byte, plugin) = "msat.cma"
 archive(native) = "msat.cmxa"
diff --git a/_tags b/_tags
index ee34cae3..05d4a2a6 100644
--- a/_tags
+++ b/_tags
@@ -1,5 +1,5 @@
-<util/*.cmx>: for-pack(Msat), package(unix)
-<util/*.native>: package(unix)
+<util/*.cmx>: for-pack(Msat)
+#<util/*.native>: 
 <smt/*.cmx>: for-pack(Msat)
 <sat/*.cmx>: for-pack(Msat)
 <solver/*.cmx>: for-pack(Msat)
diff --git a/opam b/opam
index eb0bf60a..d58df2f7 100644
--- a/opam
+++ b/opam
@@ -15,7 +15,7 @@ remove: [
 ]
 depends: [
   "ocamlfind" {build}
-  "base-unix"
+  "ocamlbuild" {build}
 ]
 available: [
   ocaml-version >= "4.02.1"
diff --git a/util/timer.ml b/util/timer.ml
deleted file mode 100644
index 4122d1ba..00000000
--- a/util/timer.ml
+++ /dev/null
@@ -1,35 +0,0 @@
-(**************************************************************************)
-(*                                                                        *)
-(*                                  Cubicle                               *)
-(*             Combining model checking algorithms and SMT solvers        *)
-(*                                                                        *)
-(*                  Sylvain Conchon and Alain Mebsout                     *)
-(*                  Universite Paris-Sud 11                               *)
-(*                                                                        *)
-(*  Copyright 2011. This file is distributed under the terms of the       *)
-(*  Apache Software License version 2.0                                   *)
-(*                                                                        *)
-(**************************************************************************)
-
-module type S = sig
-  val start : unit -> unit
-  val pause : unit -> unit
-  val get : unit -> float
-end
-
-module Make (X : sig end) = struct
-
-  open Unix
-
-  let u = ref 0.0
-
-  let cpt = ref 0.0
-
-  let start () = u:=(times()).tms_utime
-
-  let pause () = cpt := !cpt +. ((times()).tms_utime -. !u)
-
-  let get () =
-    !cpt
-
-end
diff --git a/util/timer.mli b/util/timer.mli
deleted file mode 100644
index 7e244b57..00000000
--- a/util/timer.mli
+++ /dev/null
@@ -1,20 +0,0 @@
-(**************************************************************************)
-(*                                                                        *)
-(*                                  Cubicle                               *)
-(*             Combining model checking algorithms and SMT solvers        *)
-(*                                                                        *)
-(*                  Sylvain Conchon and Alain Mebsout                     *)
-(*                  Universite Paris-Sud 11                               *)
-(*                                                                        *)
-(*  Copyright 2011. This file is distributed under the terms of the       *)
-(*  Apache Software License version 2.0                                   *)
-(*                                                                        *)
-(**************************************************************************)
-
-module type S = sig
-  val start : unit -> unit
-  val pause : unit -> unit
-  val get : unit -> float
-end
-
-module Make (X : sig end) : S