diff --git a/.gitignore b/.gitignore
index ee79f402..f07c6d70 100644
--- a/.gitignore
+++ b/.gitignore
@@ -8,5 +8,6 @@ _build/
 *.docdir
 src/util/log.ml
 doc/index.html
-
-msat
+*.exe
+.merlin
+*.install
diff --git a/.merlin b/.merlin
deleted file mode 100644
index cfd63256..00000000
--- a/.merlin
+++ /dev/null
@@ -1,20 +0,0 @@
-S src/core
-S src/solver
-S src/sat
-S src/smt
-S src/mcsat
-S src/backend
-S src/util
-S tests
-
-B _build/src/
-B _build/src/core
-B _build/src/solver
-B _build/src/sat
-B _build/src/smt
-B _build/src/mcsat
-B _build/src/util
-B _build/src/backend
-B _build/tests
-
-PKG dolmen
diff --git a/META b/META
deleted file mode 100644
index 993b7f01..00000000
--- a/META
+++ /dev/null
@@ -1,31 +0,0 @@
-# meta
-name="msat"
-version="dev"
-description="MSAT is a modular SAT solver, plus extensions"
-requires=""
-archive(byte) = "msat.cma"
-archive(byte, plugin) = "msat.cma"
-archive(native) = "msat.cmxa"
-archive(native, plugin) = "msat.cmxs"
-
-package "sat" (
- version = "dev"
- description = "SAT solver instance"
- requires = "msat"
- archive(byte) = "msat_sat.cma"
- archive(byte, plugin) = "msat_sat.cma"
- archive(native) = "msat_sat.cmxa"
- archive(native, plugin) = "msat_sat.cmxs"
- exists_if = "msat_sat.cma"
-)
-
-package "smt" (
- version = "dev"
- description = "SMT solver instance"
- requires = "msat"
- archive(byte) = "msat_smt.cma"
- archive(byte, plugin) = "msat_smt.cma"
- archive(native) = "msat_smt.cmxa"
- archive(native, plugin) = "msat_smt.cmxs"
- exists_if = "msat_smt.cma"
-)
diff --git a/Makefile b/Makefile
index 942abc33..f58123ad 100644
--- a/Makefile
+++ b/Makefile
@@ -1,62 +1,68 @@
 # copyright (c) 2014, guillaume bury
+# copyright (c) 2017, simon cruanes
 
-LOG=build.log
-COMP=ocamlbuild -log $(LOG) -use-ocamlfind
-FLAGS=
-DOC=src/msat.docdir/index.html
 BIN=main.native
 TEST_BIN=tests/test_api.native
 
 NAME=msat
+J?=3
+TIMEOUT?=30
+TARGETS=src/bin/main.exe
+OPTS= -j $(J)
 
 LIB=$(addprefix $(NAME), .cma .cmxa .cmxs)
 
 all: lib test
 
-lib:
-	$(COMP) $(FLAGS) $(LIB)
+build:
+	jbuilder build $(OPTS) @install
 
-doc:
-	$(COMP) $(FLAGS) $(DOC)
+build-dev:
+	jbuilder build $(OPTS) @install --dev
 
-bin:
-	$(COMP) $(FLAGS) $(BIN)
-	cp $(BIN) $(NAME) && rm $(BIN)
-
-test_bin:
-	$(COMP) $(FLAGS) $(TEST_BIN)
-
-test: bin test_bin
+test: build
 	@echo "run API tests…"
-	@./test_api.native
+	jbuilder runtest
 	@echo "run benchmarks…"
 	# @/usr/bin/time -f "%e" ./tests/run smt
 	@/usr/bin/time -f "%e" ./tests/run mcsat
 
 enable_log:
-	cd src/util; ln -sf log_real.ml log.ml
+	cd src/core; ln -sf log_real.ml log.ml
 
 disable_log:
-	cd src/util; ln -sf log_dummy.ml log.ml
+	cd src/core; ln -sf log_dummy.ml log.ml
 
 clean:
-	$(COMP) -clean
-	rm -rf $(NAME)
+	jbuilder clean
 
-TO_INSTALL_LIB=$(addsuffix .a, $(NAME)) $(addsuffix .cmi, $(NAME))
-TO_INSTALL=META $(addprefix _build/src/,$(LIB) $(TO_INSTALL_LIB))
-
-install: lib
-	ocamlfind install $(NAME) $(TO_INSTALL)
-	if [ -d "$(NAME).docdir" ]; then \
-		mkdir -p $(DOCDIR) ; \
-		cp -v $(NAME).docdir/*.html $(NAME).docdir/*.css $(DOCDIR) ; \
-	fi
+install: build-install
+	jbuilder install
 
 uninstall:
-	ocamlfind remove $(NAME)
-	rm -rf $(DOCDIR)
+	jbuilder uninstall
+
+doc:
+	jbuilder build $(OPTS) @doc
+
 
 reinstall: | uninstall install
 
+ocp-indent:
+	@which ocp-indent > /dev/null || { \
+	  	echo 'ocp-indent not found; please run `opam install ocp-indent`'; \
+		exit 1 ; \
+	  }
+
+reindent: ocp-indent
+	@find src '(' -name '*.ml' -or -name '*.mli' ')' -print0 | xargs -0 echo "reindenting: "
+	@find src '(' -name '*.ml' -or -name '*.mli' ')' -print0 | xargs -0 ocp-indent -i
+
+WATCH=build-dev
+watch:
+	while find src/ -print0 | xargs -0 inotifywait -e delete_self -e modify ; do \
+		echo "============ at `date` ==========" ; \
+		make $(WATCH); \
+	done
+
 .PHONY: clean doc all bench install uninstall remove reinstall enable_log disable_log bin test
diff --git a/_tags b/_tags
deleted file mode 100644
index 31793d6e..00000000
--- a/_tags
+++ /dev/null
@@ -1,35 +0,0 @@
-# colors
-true: bin_annot, color(always)
-
-# optimization options
-true: inline(100), optimize(3), unbox_closures, unbox_closures_factor(20)
-
-# Include paths
-<src>: include
-<src/core>: include
-<src/solver>: include
-<src/backend>: include
-<src/util>: include
-<src/sat>: include
-<src/smt>: include
-<src/mcsat>: include
-
-# Pack options
-<src/core/*.cmx>: for-pack(Msat)
-<src/solver/*.cmx>: for-pack(Msat)
-<src/backend/*.cmx>: for-pack(Msat)
-<src/util/*.cmx>: for-pack(Msat)
-<src/sat/sat.cmx>: for-pack(Msat)
-<src/sat/expr_sat.cmx>: for-pack(Msat)
-
-# Testing dependencies
-<src/main.*>: package(dolmen)
-<src/util/type.*>: package(dolmen)
-<src/sat/type_sat.*>: package(dolmen)
-<src/smt/type_smt.*>: package(dolmen)
-
-# more warnings
-<src/**/*.ml>: warn_K, warn_Y, warn_X
-<src/**/*.ml>: short_paths, safe_string, strict_sequence
-<src/**/*.cm*>: debug
-
diff --git a/opam b/msat.opam
similarity index 66%
rename from opam
rename to msat.opam
index a1ac6cd4..4131742c 100644
--- a/opam
+++ b/msat.opam
@@ -3,27 +3,26 @@ name: "msat"
 license: "Apache"
 version: "dev"
 author: ["Sylvain Conchon" "Alain Mebsout" "Stephane Lecuyer" "Simon Cruanes" "Guillaume Bury"]
-maintainer: ["guillaume.bury@gmail.com" "simon.cruanes@inria.fr"]
+maintainer: ["guillaume.bury@gmail.com" "simon.cruanes.2007@m4x.org"]
 build: [
-    [make "disable_log"]
-    [make "lib"]
+    [make "build"]
 ]
 build-doc: [
     [make "doc"]
 ]
 install: [
-    [make "DOCDIR=%{doc}%" "install"]
+    [make "install"]
 ]
 remove: [
-    [make "DOCDIR=%{doc}%" "uninstall"]
+    [make "uninstall"]
 ]
 depends: [
   "ocamlfind" {build}
-  "ocamlbuild" {build}
+  "jbuilder" {build}
   "dolmen" {test & = "dev" }
 ]
 available: [
-  ocaml-version >= "4.00.1"
+  ocaml-version >= "4.03.0"
 ]
 tags: [ "sat" "smt" ]
 homepage: "https://github.com/Gbury/mSAT"
diff --git a/msat_solver.opam b/msat_solver.opam
new file mode 100644
index 00000000..8b090d0b
--- /dev/null
+++ b/msat_solver.opam
@@ -0,0 +1,31 @@
+opam-version: "1.2"
+name: "msat"
+license: "Apache"
+version: "dev"
+author: ["Sylvain Conchon" "Alain Mebsout" "Stephane Lecuyer" "Simon Cruanes" "Guillaume Bury"]
+maintainer: ["guillaume.bury@gmail.com" "simon.cruanes.2007@m4x.org"]
+build: [
+    [make "build"]
+]
+build-doc: [
+    [make "doc"]
+]
+install: [
+    [make "install"]
+]
+remove: [
+    [make "uninstall"]
+]
+depends: [
+  "ocamlfind" {build}
+  "jbuilder" {build}
+  "dolmen"
+]
+available: [
+  ocaml-version >= "4.03.0"
+]
+tags: [ "sat" "smt" ]
+homepage: "https://github.com/Gbury/mSAT"
+dev-repo: "https://github.com/Gbury/mSAT.git"
+bug-reports: "https://github.com/Gbury/mSAT/issues/"
+
diff --git a/myocamlbuild.ml b/myocamlbuild.ml
deleted file mode 100644
index 818b0017..00000000
--- a/myocamlbuild.ml
+++ /dev/null
@@ -1,16 +0,0 @@
-
-(* This file is free software, part of mSAT. See file "LICENSE" for more information. *)
-
-open Ocamlbuild_plugin;;
-
-let doc_intro = "src/doc.txt";;
-
-dispatch begin function
-  | After_rules ->
-    (* Documentation index *)
-    dep ["ocaml"; "doc"; "extension:html"] & [doc_intro] ;
-    flag ["ocaml"; "doc"; "extension:html"]
-    & S [ A "-t"; A "mSAT doc"; A "-intro"; P doc_intro ];
-  | _ -> ()
-end
-
diff --git a/src/backend/Coq.ml b/src/backend/Coq.ml
index 51bd105c..efdbe8b3 100644
--- a/src/backend/Coq.ml
+++ b/src/backend/Coq.ml
@@ -2,6 +2,7 @@
 MSAT is free software, using the Apache license, see file LICENSE
 Copyright 2015 Guillaume Bury
 *)
+open Msat
 
 module type S = Backend_intf.S
 
@@ -71,8 +72,8 @@ module Make(S : Res.S)(A : Arg with type hyp := S.clause
   let resolution fmt goal hyp1 hyp2 atom =
     let a = S.St.(atom.var.pa) in
     let h1, h2 =
-      if Array_util.exists ((==) a) hyp1.S.St.atoms then hyp1, hyp2
-      else (assert (Array_util.exists ((==) a) hyp2.S.St.atoms); hyp2, hyp1)
+      if Array.exists ((==) a) hyp1.S.St.atoms then hyp1, hyp2
+      else (assert (Array.exists ((==) a) hyp2.S.St.atoms); hyp2, hyp1)
     in
     (** Print some debug info *)
     Format.fprintf fmt
diff --git a/src/backend/Coq.mli b/src/backend/Coq.mli
index 61c42785..205319b6 100644
--- a/src/backend/Coq.mli
+++ b/src/backend/Coq.mli
@@ -8,6 +8,7 @@ Copyright 2015 Guillaume Bury
     This module provides an easy way to produce coq scripts
     corresponding to the resolution proofs output by the
     sat solver. *)
+open Msat
 
 module type S = Backend_intf.S
 (** Interface for exporting proofs. *)
diff --git a/src/backend/Dedukti.ml b/src/backend/Dedukti.ml
index fb1089e9..a4a842d1 100644
--- a/src/backend/Dedukti.ml
+++ b/src/backend/Dedukti.ml
@@ -3,6 +3,8 @@ MSAT is free software, using the Apache license, see file LICENSE
 Copyright 2015 Guillaume Bury
 *)
 
+open Msat
+
 module type S = Backend_intf.S
 
 module type Arg = sig
diff --git a/src/backend/Dedukti.mli b/src/backend/Dedukti.mli
index 449b82fb..e24deb9a 100644
--- a/src/backend/Dedukti.mli
+++ b/src/backend/Dedukti.mli
@@ -9,6 +9,8 @@ Copyright 2014 Simon Cruanes
     Work in progress...
 *)
 
+open Msat
+
 module type S = Backend_intf.S
 
 module type Arg = sig
diff --git a/src/backend/Dimacs.ml b/src/backend/Dimacs.ml
index 7afda874..239e8604 100644
--- a/src/backend/Dimacs.ml
+++ b/src/backend/Dimacs.ml
@@ -4,6 +4,8 @@ Copyright 2014 Guillaume Bury
 Copyright 2014 Simon Cruanes
 *)
 
+open Msat
+
 module type S = sig
 
   type clause
diff --git a/src/backend/Dimacs.mli b/src/backend/Dimacs.mli
index 0bb18a94..dcd11b47 100644
--- a/src/backend/Dimacs.mli
+++ b/src/backend/Dimacs.mli
@@ -10,6 +10,8 @@ Copyright 2014 Simon Cruanes
     iCNF formats.
 *)
 
+open Msat
+
 module type S = sig
 
   type clause
diff --git a/src/backend/Dot.ml b/src/backend/Dot.ml
index 93981958..559b3fa0 100644
--- a/src/backend/Dot.ml
+++ b/src/backend/Dot.ml
@@ -4,6 +4,8 @@ Copyright 2014 Guillaume Bury
 Copyright 2014 Simon Cruanes
 *)
 
+open Msat
+
 (** Output interface for the backend *)
 module type S = Backend_intf.S
 
diff --git a/src/backend/Dot.mli b/src/backend/Dot.mli
index 59412b47..84cf048b 100644
--- a/src/backend/Dot.mli
+++ b/src/backend/Dot.mli
@@ -9,6 +9,7 @@ Copyright 2014 Simon Cruanes
     This module provides functions to export proofs into the dot graph format.
     Graphs in dot format can be used to generates images using the graphviz tool.
 *)
+open Msat
 
 module type S = Backend_intf.S
 (** Interface for exporting proofs. *)
diff --git a/src/backend/jbuild b/src/backend/jbuild
new file mode 100644
index 00000000..aa2609ff
--- /dev/null
+++ b/src/backend/jbuild
@@ -0,0 +1,13 @@
+; vim:ft=lisp:
+
+; main binary
+(library
+  ((name msat_backend)
+   (public_name msat.backend)
+   (synopsis "proof backends for msat")
+   (libraries (msat))
+   (flags (:standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string))
+   (ocamlopt_flags (:standard -O3 -bin-annot
+                    -unbox-closures -unbox-closures-factor 20))
+  ))
+
diff --git a/src/core/External.ml b/src/core/External.ml
index fb5e03d1..e14e03a7 100644
--- a/src/core/External.ml
+++ b/src/core/External.ml
@@ -31,6 +31,11 @@ type ('clause, 'proof) unsat_state = ('clause, 'proof) Solver_intf.unsat_state =
   (** returns a persistent proof of the empty clause from the Unsat result. *)
 }
 
+type 'clause export = 'clause Solver_intf.export = {
+  hyps: 'clause Vec.t;
+  history: 'clause Vec.t;
+  local: 'clause Vec.t;
+}
 
 module Make
     (St : Solver_types.S)
@@ -56,8 +61,9 @@ module Make
 
   let pp_all lvl status =
     Log.debugf lvl
-      "@[<v>%s - Full resume:@,@[<hov 2>Trail:@\n%a@]@,@[<hov 2>Temp:@\n%a@]@,@[<hov 2>Hyps:@\n%a@]@,@[<hov 2>Lemmas:@\n%a@]@,@]@."
-      (fun k -> k status
+      (fun k -> k
+        "@[<v>%s - Full resume:@,@[<hov 2>Trail:@\n%a@]@,@[<hov 2>Temp:@\n%a@]@,@[<hov 2>Hyps:@\n%a@]@,@[<hov 2>Lemmas:@\n%a@]@,@]@."
+          status
           (Vec.print ~sep:"" St.pp) (S.trail ())
           (Vec.print ~sep:"" St.pp_clause) (S.temp ())
           (Vec.print ~sep:"" St.pp_clause) (S.hyps ())
@@ -98,7 +104,7 @@ module Make
 
   let solve ?(assumptions=[]) () =
     try
-      S.pop ();
+      S.pop (); (* FIXME: what?! *)
       S.push ();
       S.local assumptions;
       S.solve ();
@@ -119,19 +125,9 @@ module Make
   let new_lit = S.new_lit
   let new_atom = S.new_atom
 
-  (* Dimacs & iCNF export *)
-  module D = Dimacs.Make(St)(struct end)
-
-  let export_dimacs fmt () =
+  let export () : St.clause export =
     let hyps = S.hyps () in
     let history = S.history () in
     let local = S.temp () in
-    D.export fmt ~hyps ~history ~local
-
-  let export_icnf fmt () =
-    let hyps = S.hyps () in
-    let history = S.history () in
-    let local = S.temp () in
-    D.export_icnf fmt ~hyps ~history ~local
-
+    {hyps; history; local}
 end
diff --git a/src/core/Heap.ml b/src/core/Heap.ml
new file mode 100644
index 00000000..a8f78d08
--- /dev/null
+++ b/src/core/Heap.ml
@@ -0,0 +1,155 @@
+(**************************************************************************)
+(*                                                                        *)
+(*                                  Cubicle                               *)
+(*             Combining model checking algorithms and SMT solvers        *)
+(*                                                                        *)
+(*                  Mohamed Iguernelala                                   *)
+(*                  Universite Paris-Sud 11                               *)
+(*                                                                        *)
+(*  Copyright 2011. This file is distributed under the terms of the       *)
+(*  Apache Software License version 2.0                                   *)
+(*                                                                        *)
+(**************************************************************************)
+
+module type RANKED = Heap_intf.RANKED
+
+module type S = Heap_intf.S
+
+module Make(Elt : RANKED) = struct
+  type elt = Elt.t
+
+  type t = {
+    heap : elt Vec.t;
+  }
+
+  let _absent_index = -1
+
+  let create () =
+    { heap = Vec.make_empty Elt.dummy; }
+
+  let[@inline] left i = (i lsl 1) + 1 (* i*2 + 1 *)
+  let[@inline] right i = (i + 1) lsl 1 (* (i+1)*2 *)
+  let[@inline] parent i = (i - 1) asr 1 (* (i-1) / 2 *)
+
+  (*
+  let rec heap_property cmp ({heap=heap} as s) i =
+    i >= (Vec.size heap)  ||
+      ((i = 0 || not(cmp (Vec. get heap i) (Vec.get heap (parent i))))
+       && heap_property cmp s (left i) && heap_property cmp s (right i))
+
+  let heap_property cmp s = heap_property cmp s 1
+  *)
+
+  (* [elt] is above or at its expected position. Move it up the heap
+     (towards high indices) to restore the heap property *)
+  let percolate_up {heap} (elt:Elt.t) : unit =
+    let pi = ref (parent (Elt.idx elt)) in
+    let i = ref (Elt.idx elt) in
+    while !i <> 0 && Elt.cmp elt (Vec.get heap !pi) do
+      Vec.set heap !i (Vec.get heap !pi);
+      Elt.set_idx (Vec.get heap !i) !i;
+      i  := !pi;
+      pi := parent !i
+    done;
+    Vec.set heap !i elt;
+    Elt.set_idx elt !i
+
+  let percolate_down {heap} (elt:Elt.t): unit =
+    let sz = Vec.size heap in
+    let li = ref (left (Elt.idx elt)) in
+    let ri = ref (right (Elt.idx elt)) in
+    let i = ref (Elt.idx elt) in
+    begin
+      try
+        while !li < sz do
+          let child =
+            if !ri < sz && Elt.cmp (Vec.get heap !ri) (Vec.get heap !li)
+            then !ri
+            else !li
+          in
+          if not (Elt.cmp (Vec.get heap child) elt) then raise Exit;
+          Vec.set heap !i (Vec.get heap child);
+          Elt.set_idx (Vec.get heap !i) !i;
+          i  := child;
+          li := left !i;
+          ri := right !i
+        done;
+      with Exit -> ()
+    end;
+    Vec.set heap !i elt;
+    Elt.set_idx elt !i
+
+  let[@inline] in_heap x = Elt.idx x >= 0
+
+  let[@inline] decrease s x = assert (in_heap x); percolate_up s x
+
+  (*
+  let increase cmp s n =
+    assert (in_heap s n); percolate_down cmp s (V.get s.indices n)
+  *)
+
+  let filter s filt =
+    let j = ref 0 in
+    let lim = Vec.size s.heap in
+    for i = 0 to lim - 1 do
+      if filt (Vec.get s.heap i) then (
+        Vec.set s.heap !j (Vec.get s.heap i);
+        Elt.set_idx (Vec.get s.heap i) !j;
+        incr j;
+      ) else (
+        Elt.set_idx (Vec.get s.heap i) _absent_index;
+      );
+    done;
+    Vec.shrink s.heap (lim - !j);
+    for i = (lim / 2) - 1 downto 0 do
+      percolate_down s (Vec.get s.heap i)
+    done
+
+  let size s = Vec.size s.heap
+
+  let is_empty s = Vec.is_empty s.heap
+
+  let clear {heap} =
+    Vec.iter (fun e -> Elt.set_idx e _absent_index) heap;
+    Vec.clear heap;
+    ()
+
+  let insert s elt =
+    if not (in_heap elt) then (
+      Elt.set_idx elt (Vec.size s.heap);
+      Vec.push s.heap elt;
+      percolate_up s elt;
+    )
+
+  let[@inline] grow_to_at_least s sz =
+    Vec.grow_to_at_least s.heap sz
+
+  (*
+  let update cmp s n =
+    assert (heap_property cmp s);
+    begin
+      if in_heap s n then
+        begin
+          percolate_up cmp s (Vec.get s.indices n);
+          percolate_down cmp s (Vec.get s.indices n)
+        end
+      else insert cmp s n
+    end;
+    assert (heap_property cmp s)
+  *)
+
+  let remove_min ({heap} as s) =
+    if Vec.size heap=0 then raise Not_found;
+    let x = Vec.get heap 0 in
+    Elt.set_idx x _absent_index;
+    let new_hd = Vec.last heap in (* heap.last() *)
+    Vec.set heap 0 new_hd;
+    Elt.set_idx new_hd 0;
+    Vec.pop heap; (* remove last *)
+    (* enforce heap property again *)
+    if Vec.size heap > 1 then (
+      percolate_down s new_hd;
+    );
+    x
+
+end
diff --git a/src/core/Heap.mli b/src/core/Heap.mli
new file mode 100644
index 00000000..24c47bd6
--- /dev/null
+++ b/src/core/Heap.mli
@@ -0,0 +1,18 @@
+(**************************************************************************)
+(*                                                                        *)
+(*                                  Cubicle                               *)
+(*             Combining model checking algorithms and SMT solvers        *)
+(*                                                                        *)
+(*                  Mohamed Iguernelala                                   *)
+(*                  Universite Paris-Sud 11                               *)
+(*                                                                        *)
+(*  Copyright 2011. This file is distributed under the terms of the       *)
+(*  Apache Software License version 2.0                                   *)
+(*                                                                        *)
+(**************************************************************************)
+
+module type RANKED = Heap_intf.RANKED
+
+module type S = Heap_intf.S
+
+module Make(X : RANKED) : S with type elt = X.t
diff --git a/src/core/Heap_intf.ml b/src/core/Heap_intf.ml
new file mode 100644
index 00000000..a5d11100
--- /dev/null
+++ b/src/core/Heap_intf.ml
@@ -0,0 +1,51 @@
+
+module type RANKED = sig
+  type t
+  val idx: t -> int (** Index in heap. return -1 if never set *)
+  val set_idx : t -> int -> unit (** Update index in heap *)
+  val dummy : t
+  val cmp : t -> t -> bool
+end
+
+module type S = sig
+  type elt
+  (** Type of elements *)
+
+  type t
+  (** Heap of {!elt}, whose priority is increased or decreased
+      incrementally (see {!decrease} for instance) *)
+
+  val create : unit -> t
+  (** Create a heap *)
+
+  val decrease : t -> elt -> unit
+  (** [decrease h x] decreases the value associated to [x] within [h] *)
+
+  val in_heap : elt -> bool
+
+  (*val increase : (int -> int -> bool) -> t -> int -> unit*)
+
+  val size : t -> int
+  (** Number of integers within the heap *)
+
+  val is_empty : t -> bool
+
+  val clear : t -> unit
+  (** Clear the content of the heap *)
+
+  val insert : t -> elt -> unit
+  (** Insert a new element into the heap *)
+
+  val grow_to_at_least: t -> int -> unit
+  (** Hint: augment the internal capacity of the heap until it reaches at
+      least the given integer *)
+
+  (*val update : (int -> int -> bool) -> t -> int -> unit*)
+
+  val remove_min : t -> elt
+  (** Remove and return the integer that has the lowest value from the heap
+      @raise Not_found if the heap is empty *)
+
+  val filter : t -> (elt -> bool) -> unit
+  (** Filter out values that don't satisfy the predicate *)
+end
diff --git a/src/core/Internal.ml b/src/core/Internal.ml
index 2583c301..f2227514 100644
--- a/src/core/Internal.ml
+++ b/src/core/Internal.ml
@@ -11,11 +11,18 @@ module Make
                              and type proof = St.proof)
     (Dummy: sig end)
 = struct
-
   module Proof = Res.Make(St)
 
   open St
 
+  module H = Heap.Make(struct
+    type t = St.elt
+    let[@inline] cmp i j = get_elt_weight j < get_elt_weight i (* comparison by weight *)
+    let dummy = elt_of_var St.dummy_var
+    let idx = get_elt_idx
+    let set_idx = set_elt_idx
+  end)
+
   exception Sat
   exception Unsat
   exception UndecidedLit
@@ -89,7 +96,7 @@ module Make
     (* number of toplevel assignments since last call to [simplify ()] *)
 
 
-    order : Iheap.t;
+    order : H.t;
     (* Heap ordered by variable activity *)
 
     var_decay : float;
@@ -147,7 +154,7 @@ module Make
     th_levels = Vec.make 100 Plugin.dummy;
     user_levels = Vec.make 10 (-1);
 
-    order = Iheap.init 0;
+    order = H.create();
 
     var_incr = 1.;
     clause_incr = 1.;
@@ -183,9 +190,6 @@ module Make
   let decision_level () = Vec.size env.elt_levels
   let base_level () = Vec.size env.user_levels
 
-  let f_weight i j =
-    get_elt_weight (St.get_elt j) < get_elt_weight (St.get_elt i)
-
   (* Are the assumptions currently unsat ? *)
   let is_unsat () =
     match env.unsat_conflict with
@@ -226,14 +230,14 @@ module Make
      When we add a variable (which wraps a formula), we also need to add all
      its subterms.
   *)
-  let rec insert_var_order = function
-    | E_lit l ->
-      Iheap.insert f_weight env.order l.lid
-    | E_var v ->
-      Iheap.insert f_weight env.order v.vid;
-      insert_subterms_order v
+  let rec insert_var_order (elt:elt) : unit =
+    H.insert env.order elt;
+    begin match elt with
+      | E_lit _ -> ()
+      | E_var v -> insert_subterms_order v
+    end
 
-  and insert_subterms_order v =
+  and insert_subterms_order (v:St.var) : unit =
     iter_sub (fun t -> insert_var_order (elt_of_lit t)) v
 
   (* Add new litterals/atoms on which to decide on, even if there is no
@@ -269,8 +273,10 @@ module Make
       done;
       env.var_incr <- env.var_incr *. 1e-100;
     end;
-    if Iheap.in_heap env.order v.vid then
-      Iheap.decrease f_weight env.order v.vid
+    let elt = elt_of_var v in
+    if H.in_heap elt then (
+      H.decrease env.order elt
+    )
 
   (* increase activity of literal [l] *)
   let lit_bump_activity_aux (l:lit): unit =
@@ -281,8 +287,10 @@ module Make
       done;
       env.var_incr <- env.var_incr *. 1e-100;
     end;
-    if Iheap.in_heap env.order l.lid then
-      Iheap.decrease f_weight env.order l.lid
+    let elt = elt_of_lit l in
+    if H.in_heap elt then (
+      H.decrease env.order elt
+    )
 
   (* increase activity of var [v] *)
   let var_bump_activity (v:var): unit =
@@ -408,7 +416,7 @@ module Make
   *)
   let attach_clause c =
     assert (not c.attached);
-    Log.debugf debug "Attaching %a" (fun k -> k St.pp_clause c);
+    Log.debugf debug (fun k -> k "Attaching %a" St.pp_clause c);
     Array.iter (fun a -> a.var.used <- a.var.used + 1) c.atoms;
     Vec.push c.atoms.(0).neg.watched c;
     Vec.push c.atoms.(1).neg.watched c;
@@ -423,9 +431,9 @@ module Make
     assert (lvl >= base_level ());
     (* Nothing to do if we try to backtrack to a non-existent level. *)
     if decision_level () <= lvl then
-      Log.debugf debug "Already at level <= %d" (fun k -> k lvl)
+      Log.debugf debug (fun k -> k "Already at level <= %d" lvl)
     else begin
-      Log.debugf info "Backtracking to lvl %d" (fun k -> k lvl);
+      Log.debugf info (fun k -> k "Backtracking to lvl %d" lvl);
       (* We set the head of the solver and theory queue to what it was. *)
       let head = ref (Vec.get env.elt_levels lvl) in
       env.elt_head <- !head;
@@ -468,17 +476,17 @@ module Make
       (* Recover the right theory state. *)
       Plugin.backtrack (Vec.get env.th_levels lvl);
       (* Resize the vectors according to their new size. *)
-      Vec.shrink env.elt_queue ((Vec.size env.elt_queue) - !head);
-      Vec.shrink env.elt_levels ((Vec.size env.elt_levels) - lvl);
-      Vec.shrink env.th_levels ((Vec.size env.th_levels) - lvl);
+      Vec.shrink env.elt_queue !head;
+      Vec.shrink env.elt_levels lvl;
+      Vec.shrink env.th_levels lvl;
     end;
     assert (Vec.size env.elt_levels = Vec.size env.th_levels);
     ()
 
   (* Unsatisfiability is signaled through an exception, since it can happen
      in multiple places (adding new clauses, or solving for instance). *)
-  let report_unsat ({atoms=atoms} as confl) : _ =
-    Log.debugf info "@[Unsat conflict: %a@]" (fun k -> k St.pp_clause confl);
+  let report_unsat confl : _ =
+    Log.debugf info (fun k -> k "@[Unsat conflict: %a@]" St.pp_clause confl);
     env.unsat_conflict <- Some confl;
     raise Unsat
 
@@ -492,25 +500,27 @@ module Make
     | (Bcp cl) as r ->
       let l, history = partition cl.atoms in
       begin match l with
-        | [ a ] ->
-          if history = [] then r
-          (* no simplification has been done, so [cl] is actually a clause with only
-             [a], so it is a valid reason for propagating [a]. *)
-          else begin
+        | [_] ->
+          if history = [] then (
+            (* no simplification has been done, so [cl] is actually a clause with only
+               [a], so it is a valid reason for propagating [a]. *)
+            r
+          ) else (
             (* Clauses in [history] have been used to simplify [cl] into a clause [tmp_cl]
                with only one formula (which is [a]). So we explicitly create that clause
                and set it as the cause for the propagation of [a], that way we can
                rebuild the whole resolution tree when we want to prove [a]. *)
             let c' = make_clause (fresh_lname ()) l (History (cl :: history)) in
-            Log.debugf debug "Simplified reason: @[<v>%a@,%a@]"
-              (fun k -> k St.pp_clause cl St.pp_clause c');
+            Log.debugf debug
+              (fun k -> k "Simplified reason: @[<v>%a@,%a@]" St.pp_clause cl St.pp_clause c');
             Bcp c'
-          end
+          )
         | _ ->
-          Log.debugf error "@[<v 2>Failed at reason simplification:@,%a@,%a@]"
+          Log.debugf error
             (fun k ->
-               k (Vec.print ~sep:"" St.pp_atom)
-                 (Vec.from_list l (List.length l) St.dummy_atom)
+               k "@[<v 2>Failed at reason simplification:@,%a@,%a@]"
+                 (Vec.print ~sep:"" St.pp_atom)
+                 (Vec.from_list l St.dummy_atom)
                  St.pp_clause cl);
           assert false
       end
@@ -520,7 +530,7 @@ module Make
      Wrapper function for adding a new propagated formula. *)
   let enqueue_bool a ~level:lvl reason : unit =
     if a.neg.is_true then begin
-      Log.debugf error "Trying to enqueue a false literal: %a" (fun k->k St.pp_atom a);
+      Log.debugf error (fun k->k "Trying to enqueue a false literal: %a" St.pp_atom a);
       assert false
     end;
     assert (not a.is_true && a.var.v_level < 0 &&
@@ -533,8 +543,8 @@ module Make
     a.var.v_level <- lvl;
     a.var.reason <- Some reason;
     Vec.push env.elt_queue (of_atom a);
-    Log.debugf debug "Enqueue (%d): %a"
-      (fun k->k (Vec.size env.elt_queue) pp_atom a)
+    Log.debugf debug
+      (fun k->k "Enqueue (%d): %a" (Vec.size env.elt_queue) pp_atom a)
 
   let enqueue_semantic a terms =
     if a.is_true then ()
@@ -542,24 +552,24 @@ module Make
       let l = List.map St.add_term terms in
       let lvl = List.fold_left (fun acc {l_level; _} ->
           assert (l_level > 0); max acc l_level) 0 l in
-      Iheap.grow_to_at_least env.order (St.nb_elt ());
-      enqueue_bool a lvl Semantic
+      H.grow_to_at_least env.order (St.nb_elt ());
+      enqueue_bool a ~level:lvl Semantic
     end
 
   (* MCsat semantic assignment *)
   let enqueue_assign l value lvl =
     match l.assigned with
     | Some _ ->
-      Log.debugf error "Trying to assign an already assigned literal: %a"
-        (fun k -> k St.pp_lit l);
+      Log.debugf error
+        (fun k -> k "Trying to assign an already assigned literal: %a" St.pp_lit l);
       assert false
     | None ->
       assert (l.l_level < 0);
       l.assigned <- Some value;
       l.l_level <- lvl;
       Vec.push env.elt_queue (of_lit l);
-      Log.debugf debug "Enqueue (%d): %a"
-        (fun k -> k (Vec.size env.elt_queue) pp_lit l)
+      Log.debugf debug
+        (fun k -> k "Enqueue (%d): %a" (Vec.size env.elt_queue) pp_lit l)
 
   (* evaluate an atom for MCsat, if it's not assigned
      by boolean propagation/decision *)
@@ -583,16 +593,16 @@ module Make
   let backtrack_lvl : atom list -> int * bool = function
     | [] | [_] ->
       0, true
-    | a :: b :: r ->
+    | a :: b :: _ ->
       assert(a.var.v_level > base_level ());
-      if a.var.v_level > b.var.v_level then begin
+      if a.var.v_level > b.var.v_level then (
         (* backtrack below [a], so we can propagate [not a] *)
         b.var.v_level, true
-      end else begin
+      ) else (
         assert (a.var.v_level = b.var.v_level);
         assert (a.var.v_level >= base_level ());
         max (a.var.v_level - 1) (base_level ()), false
-      end
+      )
 
   (* result of conflict analysis, containing the learnt clause and some
      additional info.
@@ -628,14 +638,14 @@ module Make
     let conflict_level =
       Array.fold_left (fun acc p -> max acc p.var.v_level) 0 c_clause.atoms
     in
-    Log.debugf debug "Analyzing conflict (%d): %a"
-      (fun k -> k conflict_level St.pp_clause c_clause);
+    Log.debugf debug
+      (fun k -> k "Analyzing conflict (%d): %a" conflict_level St.pp_clause c_clause);
     while !cond do
       begin match !c with
         | None ->
-          Log.debugf debug "  skipping resolution for semantic propagation" (fun k->k)
+          Log.debug debug "  skipping resolution for semantic propagation"
         | Some clause ->
-          Log.debugf debug "  Resolving clause: %a" (fun k->k St.pp_clause clause);
+          Log.debugf debug (fun k->k"  Resolving clause: %a"  St.pp_clause clause);
           begin match clause.cpremise with
             | History _ -> clause_bump_activity clause
             | Hyp | Local | Lemma _ -> ()
@@ -670,7 +680,7 @@ module Make
       (* look for the next node to expand *)
       while
         let a = Vec.get env.elt_queue !tr_ind in
-        Log.debugf debug "  looking at: %a" (fun k -> k St.pp a);
+        Log.debugf debug (fun k -> k "  looking at: %a" St.pp a);
         match a with
         | Atom q ->
           (not (q.var.seen = Both)) ||
@@ -694,7 +704,7 @@ module Make
         assert (n > 0);
         assert (p.var.v_level >= conflict_level);
         c := Some cl
-      | n, _ -> assert false
+      | _ -> assert false
     done;
     List.iter (fun q -> clear q.var) !seen;
     let l = List.fast_sort (fun p q -> compare q.var.v_level p.var.v_level) !learnt in
@@ -749,12 +759,12 @@ module Make
      - report unsat if conflict at level 0
   *)
   let add_boolean_conflict (confl:clause): unit =
-    Log.debugf info "Boolean conflict: %a" (fun k -> k St.pp_clause confl);
+    Log.debugf info (fun k -> k "Boolean conflict: %a" St.pp_clause confl);
     env.next_decision <- None;
     env.conflicts <- env.conflicts + 1;
     assert (decision_level() >= base_level ());
     if decision_level() = base_level ()
-    || Array_util.for_all (fun a -> a.var.v_level <= base_level ()) confl.atoms then
+    || Array.for_all (fun a -> a.var.v_level <= base_level ()) confl.atoms then
       report_unsat confl; (* Top-level conflict *)
     let cr = analyze confl in
     cancel_until (max cr.cr_backtrack_lvl (base_level ()));
@@ -770,14 +780,14 @@ module Make
   (* Add a new clause, simplifying, propagating, and backtracking if
      the clause is false in the current trail *)
   let add_clause (init:clause) : unit =
-    Log.debugf debug "Adding clause: @[<hov>%a@]" (fun k -> k St.pp_clause init);
+    Log.debugf debug (fun k -> k "Adding clause: @[<hov>%a@]" St.pp_clause init);
     (* Insertion of new lits is done before simplification. Indeed, else a lit in a
        trivial clause could end up being not decided on, which is a bug. *)
     Array.iter (fun x -> insert_var_order (elt_of_var x.var)) init.atoms;
     let vec = clause_vector init in
     try
       let c = eliminate_doublons init in
-      Log.debugf debug "Doublons eliminated: %a" (fun k -> k St.pp_clause c);
+      Log.debugf debug (fun k -> k "Doublons eliminated: %a" St.pp_clause c);
       let atoms, history = partition c.atoms in
       let clause =
         if history = []
@@ -788,7 +798,7 @@ module Make
         )
         else make_clause (fresh_name ()) atoms (History (c :: history))
       in
-      Log.debugf info "New clause: @[<hov>%a@]" (fun k->k St.pp_clause clause);
+      Log.debugf info (fun k->k "New clause: @[<hov>%a@]" St.pp_clause clause);
       match atoms with
       | [] ->
         (* Report_unsat will raise, and the current clause will be lost if we do not
@@ -802,7 +812,7 @@ module Make
           (* Since we cannot propagate the atom [a], in order to not lose
              the information that [a] must be true, we add clause to the list
              of clauses to add, so that it will be e-examined later. *)
-          Log.debugf debug "Unit clause, adding to clauses to add" (fun k -> k);
+          Log.debug debug "Unit clause, adding to clauses to add";
           Stack.push clause env.clauses_to_add;
           report_unsat clause
         end else if a.is_true then begin
@@ -810,12 +820,12 @@ module Make
              However it means we can't propagate it at level 0. In order to not lose
              that information, we store the clause in a stack of clauses that we will
              add to the solver at the next pop. *)
-          Log.debugf debug "Unit clause, adding to root clauses" (fun k -> k);
+          Log.debug debug "Unit clause, adding to root clauses";
           assert (0 < a.var.v_level && a.var.v_level <= base_level ());
           Stack.push clause env.clauses_root;
           ()
         end else begin
-          Log.debugf debug "Unit clause, propagating: %a" (fun k->k St.pp_atom a);
+          Log.debugf debug (fun k->k "Unit clause, propagating: %a" St.pp_atom a);
           Vec.push vec clause;
           enqueue_bool a ~level:0 (Bcp clause)
         end
@@ -834,18 +844,18 @@ module Make
           if b.neg.is_true && not a.is_true && not a.neg.is_true then begin
             let lvl = List.fold_left (fun m a -> max m a.var.v_level) 0 atoms in
             cancel_until (max lvl (base_level ()));
-            enqueue_bool a lvl (Bcp clause)
+            enqueue_bool a ~level:lvl (Bcp clause)
           end
         end
     with Trivial ->
       Vec.push vec init;
-      Log.debugf info "Trivial clause ignored : @[%a@]" (fun k->k St.pp_clause init)
+      Log.debugf info (fun k->k "Trivial clause ignored : @[%a@]" St.pp_clause init)
 
   let flush_clauses () =
     if not (Stack.is_empty env.clauses_to_add) then begin
       let nbv = St.nb_elt () in
       let nbc = env.nb_init_clauses + Stack.length env.clauses_to_add in
-      Iheap.grow_to_at_least env.order nbv;
+      H.grow_to_at_least env.order nbv;
       Vec.grow_to_at_least env.clauses_hyps nbc;
       Vec.grow_to_at_least env.clauses_learnt nbc;
       env.nb_init_clauses <- nbc;
@@ -898,7 +908,7 @@ module Make
         end else begin
           match th_eval first with
           | None -> (* clause is unit, keep the same watches, but propagate *)
-            enqueue_bool first (decision_level ()) (Bcp c)
+            enqueue_bool first ~level:(decision_level ()) (Bcp c)
           | Some true -> ()
           | Some false ->
             env.elt_head <- Vec.size env.elt_queue;
@@ -946,14 +956,14 @@ module Make
     match Vec.get env.elt_queue i with
     | Atom a ->
       Plugin_intf.Lit a.lit
-    | Lit {term; assigned = Some v} ->
+    | Lit {term; assigned = Some v; _} ->
       Plugin_intf.Assign (term, v)
     | Lit _ -> assert false
 
   let slice_push (l:formula list) (lemma:proof): unit =
     let atoms = List.rev_map create_atom l in
     let c = make_clause (fresh_tname ()) atoms (Lemma lemma) in
-    Log.debugf info "Pushing clause %a" (fun k->k St.pp_clause c);
+    Log.debugf info (fun k->k "Pushing clause %a" St.pp_clause c);
     Stack.push c env.clauses_to_add
 
   let slice_propagate f = function
@@ -970,10 +980,10 @@ module Make
         else if p.neg.is_true then
           Stack.push c env.clauses_to_add
         else begin
-          Iheap.grow_to_at_least env.order (St.nb_elt ());
+          H.grow_to_at_least env.order (St.nb_elt ());
           insert_subterms_order p.var;
           let lvl = List.fold_left (fun acc a -> max acc a.var.v_level) 0 l in
-          enqueue_bool p lvl (Bcp c)
+          enqueue_bool p ~level:lvl (Bcp c)
         end
       else
         raise (Invalid_argument "Msat.Internal.slice_propagate")
@@ -1013,10 +1023,11 @@ module Make
         (* conflict *)
         let l = List.rev_map create_atom l in
         (* Assert that the conflcit is indeeed a conflict *)
-        if not @@ List.for_all (fun a -> a.neg.is_true) l then
+        if not @@ List.for_all (fun a -> a.neg.is_true) l then (
           raise (Invalid_argument "msat:core/internal: invalid conflict");
+        );
         (* Insert elements for decision (and ensure the heap is big enough) *)
-        Iheap.grow_to_at_least env.order (St.nb_elt ());
+        H.grow_to_at_least env.order (St.nb_elt ());
         List.iter (fun a -> insert_var_order (elt_of_var a.var)) l;
         (* Create the clause and return it. *)
         let c = St.make_clause (St.fresh_tname ()) l (Lemma p) in
@@ -1067,7 +1078,7 @@ module Make
         env.decisions <- env.decisions + 1;
         new_decision_level();
         let current_level = decision_level () in
-        enqueue_bool atom current_level Decision
+        enqueue_bool atom ~level:current_level Decision
       | Plugin_intf.Valued (b, l) ->
         let a = if b then atom else atom.neg in
         enqueue_semantic a l
@@ -1079,7 +1090,7 @@ module Make
       pick_branch_aux atom
     | None ->
       begin try
-          begin match St.get_elt (Iheap.remove_min f_weight env.order) with
+          begin match H.remove_min env.order with
             | E_lit l ->
               if l.l_level >= 0 then
                 pick_branch_lit ()
@@ -1120,7 +1131,7 @@ module Make
         if Vec.size env.elt_queue = St.nb_elt ()
         then raise Sat;
         if n_of_conflicts > 0 && !conflictC >= n_of_conflicts then begin
-          Log.debugf info "Restarting..." (fun k -> k);
+          Log.debug info "Restarting...";
           cancel_until (base_level ());
           raise Restart
         end;
@@ -1179,7 +1190,7 @@ module Make
               | Plugin_intf.Unsat (l, p) ->
                 let atoms = List.rev_map create_atom l in
                 let c = make_clause (fresh_tname ()) atoms (Lemma p) in
-                Log.debugf info "Theory conflict clause: %a" (fun k -> k St.pp_clause c);
+                Log.debugf info (fun k -> k "Theory conflict clause: %a" St.pp_clause c);
                 Stack.push c env.clauses_to_add
             end;
             if Stack.is_empty env.clauses_to_add then raise Sat
@@ -1192,26 +1203,27 @@ module Make
       (fun l ->
          let atoms = List.rev_map atom l in
          let c = make_clause ?tag (fresh_hname ()) atoms Hyp in
-         Log.debugf debug "Assuming clause: @[<hov 2>%a@]" (fun k -> k pp_clause c);
+         Log.debugf debug (fun k -> k "Assuming clause: @[<hov 2>%a@]" pp_clause c);
          Stack.push c env.clauses_to_add)
       cnf
 
   (* create a factice decision level for local assumptions *)
   let push (): unit =
-    Log.debugf debug "Pushing a new user level" (fun k -> k);
+    Log.debug debug "Pushing a new user level";
     match env.unsat_conflict with
-    | Some confl -> raise Unsat
+    | Some _ -> raise Unsat
     | None ->
       cancel_until (base_level ());
-      Log.debugf debug "@[<v>Status:@,@[<hov 2>trail: %d - %d@]@,%a@]"
-        (fun k -> k env.elt_head env.th_head (Vec.print ~sep:"" St.pp) env.elt_queue);
+      Log.debugf debug
+        (fun k -> k "@[<v>Status:@,@[<hov 2>trail: %d - %d@,%a@]"
+            env.elt_head env.th_head (Vec.print ~sep:"" St.pp) env.elt_queue);
       begin match propagate () with
         | Some confl ->
           report_unsat confl
         | None ->
-          Log.debugf debug "@[<v>Current trail:@,@[<hov>%a@]@]"
-            (fun k -> k (Vec.print ~sep:"" St.pp) env.elt_queue);
-          Log.debugf info "Creating new user level" (fun k -> k);
+          Log.debugf debug
+            (fun k -> k "@[<v>Current trail:@,@[<hov>%a@]@]" (Vec.print ~sep:"" St.pp) env.elt_queue);
+          Log.debug info "Creating new user level";
           new_decision_level ();
           Vec.push env.user_levels (Vec.size env.clauses_temp);
           assert (decision_level () = base_level ())
@@ -1220,9 +1232,9 @@ module Make
   (* pop the last factice decision level *)
   let pop (): unit =
     if base_level () = 0 then
-      Log.debugf warn "Cannot pop (already at user level 0)" (fun k -> k)
-    else begin
-      Log.debugf info "Popping user level" (fun k -> k);
+      Log.debug warn "Cannot pop (already at level 0)"
+    else (
+      Log.debug info "Popping user level";
       assert (base_level () > 0);
       env.unsat_conflict <- None;
       let n = Vec.last env.user_levels in
@@ -1231,22 +1243,22 @@ module Make
       Stack.iter (fun c -> Stack.push c env.clauses_to_add) env.clauses_root;
       Stack.clear env.clauses_root;
       (* remove from env.clauses_temp the now invalid caluses. *)
-      Vec.shrink env.clauses_temp (Vec.size env.clauses_temp - n);
+      Vec.shrink env.clauses_temp n;
       assert (Vec.for_all (fun c -> Array.length c.atoms = 1) env.clauses_temp);
       assert (Vec.for_all (fun c -> c.atoms.(0).var.v_level <= base_level ()) env.clauses_temp);
       cancel_until (base_level ())
-    end
+    )
 
   (* Add local hyps to the current decision level *)
   let local l =
     let aux lit =
       let a = atom lit in
-      Log.debugf info "Local assumption: @[%a@]" (fun k-> k pp_atom a);
+      Log.debugf info (fun k-> k "Local assumption: @[%a@]" pp_atom a);
       assert (decision_level () = base_level ());
       if a.is_true then ()
       else
         let c = make_clause (fresh_hname ()) [a] Local in
-        Log.debugf debug "Temp clause: @[%a@]" (fun k -> k pp_clause c);
+        Log.debugf debug (fun k -> k "Temp clause: @[%a@]" pp_clause c);
         Vec.push env.clauses_temp c;
         if a.neg.is_true then begin
           (* conflict between assumptions: UNSAT *)
@@ -1254,7 +1266,7 @@ module Make
         end else begin
           (* Grow the heap, because when the lit is backtracked,
              it will be added to the heap. *)
-          Iheap.grow_to_at_least env.order (St.nb_elt ());
+          H.grow_to_at_least env.order (St.nb_elt ());
           (* make a decision, propagate *)
           let level = decision_level() in
           enqueue_bool a ~level (Bcp c);
@@ -1263,11 +1275,11 @@ module Make
     assert (base_level () > 0);
     match env.unsat_conflict with
     | None ->
-      Log.debugf info "Adding local assumption" (fun k -> k);
+      Log.debug info "Adding local assumption";
       cancel_until (base_level ());
       List.iter aux l
     | Some _ ->
-      Log.debugf warn "Cannot add local assumption (already unsat)" (fun k -> k)
+      Log.debug warn "Cannot add local assumption (already unsat)"
 
   (* Check satisfiability *)
   let check_clause c =
@@ -1275,10 +1287,10 @@ module Make
         if a.is_true then true
         else if a.neg.is_true then false
         else raise UndecidedLit) c.atoms in
-    let res = Array_util.exists (fun x -> x) tmp in
+    let res = Array.exists (fun x -> x) tmp in
     if not res then begin
-      Log.debugf debug "Clause not satisfied: @[<hov>%a@]"
-        (fun k -> k St.pp_clause c);
+      Log.debugf debug
+        (fun k -> k "Clause not satisfied: @[<hov>%a@]" St.pp_clause c);
       false
     end else
       true
diff --git a/src/core/Res.ml b/src/core/Res.ml
index d0fa44e4..f29dc568 100644
--- a/src/core/Res.ml
+++ b/src/core/Res.ml
@@ -117,31 +117,30 @@ module Make(St : Solver_types.S) = struct
     assert St.(a.var.v_level >= 0);
     match St.(a.var.reason) with
     | Some St.Bcp c ->
-      Log.debugf debug "Analysing: @[%a@ %a@]"
-        (fun k -> k St.pp_atom a St.pp_clause c);
+      Log.debugf debug (fun k->k "Analysing: @[%a@ %a@]" St.pp_atom a St.pp_clause c);
       if Array.length c.St.atoms = 1 then begin
-        Log.debugf debug "Old reason: @[%a@]" (fun k -> k St.pp_atom a);
+        Log.debugf debug (fun k -> k "Old reason: @[%a@]" St.pp_atom a);
         c
       end else begin
         assert (a.St.neg.St.is_true);
         let r = St.History (c :: (Array.fold_left aux [] c.St.atoms)) in
         let c' = St.make_clause (fresh_pcl_name ()) [a.St.neg] r in
         a.St.var.St.reason <- Some St.(Bcp c');
-        Log.debugf debug "New reason: @[%a@ %a@]"
-          (fun k -> k St.pp_atom a St.pp_clause c');
+        Log.debugf debug
+          (fun k -> k "New reason: @[%a@ %a@]" St.pp_atom a St.pp_clause c');
         c'
       end
     | _ ->
-      Log.debugf error "Error while proving atom %a" (fun k -> k St.pp_atom a);
+      Log.debugf error (fun k -> k "Error while proving atom %a" St.pp_atom a);
       raise (Resolution_error "Cannot prove atom")
 
   let prove_unsat conflict =
     if Array.length conflict.St.atoms = 0 then conflict
     else begin
-      Log.debugf info "Proving unsat from: @[%a@]" (fun k -> k St.pp_clause conflict);
+      Log.debugf info (fun k -> k "Proving unsat from: @[%a@]" St.pp_clause conflict);
       let l = Array.fold_left (fun acc a -> set_atom_proof a :: acc) [] conflict.St.atoms in
       let res = St.make_clause (fresh_pcl_name ()) [] (St.History (conflict :: l)) in
-      Log.debugf info "Proof found: @[%a@]" (fun k -> k St.pp_clause res);
+      Log.debugf info (fun k -> k "Proof found: @[%a@]" St.pp_clause res);
       res
     end
 
@@ -166,8 +165,8 @@ module Make(St : Solver_types.S) = struct
 
   let rec chain_res (c, cl) = function
     | d :: r ->
-      Log.debugf debug "  Resolving clauses : @[%a@\n%a@]"
-        (fun k -> k St.pp_clause c St.pp_clause d);
+      Log.debugf debug
+        (fun k -> k "  Resolving clauses : @[%a@\n%a@]" St.pp_clause c St.pp_clause d);
       let dl = to_list d in
       begin match resolve (merge cl dl) with
         | [ a ], l ->
@@ -179,15 +178,15 @@ module Make(St : Solver_types.S) = struct
               chain_res (new_clause, l) r
           end
         | _ ->
-          Log.debugf error "While resolving clauses:@[<hov>%a@\n%a@]"
-            (fun k -> k St.pp_clause c St.pp_clause d);
+          Log.debugf error
+            (fun k -> k "While resolving clauses:@[<hov>%a@\n%a@]" St.pp_clause c St.pp_clause d);
           raise (Resolution_error "Clause mismatch")
       end
     | _ ->
       raise (Resolution_error "Bad history")
 
   let expand conclusion =
-    Log.debugf debug "Expanding : @[%a@]" (fun k -> k St.pp_clause conclusion);
+    Log.debugf debug (fun k -> k "Expanding : @[%a@]" St.pp_clause conclusion);
     match conclusion.St.cpremise with
     | St.Lemma l ->
       {conclusion; step = Lemma l; }
@@ -196,7 +195,7 @@ module Make(St : Solver_types.S) = struct
     | St.Local ->
       { conclusion; step = Assumption; }
     | St.History [] ->
-      Log.debugf error "Empty history for clause: %a" (fun k -> k St.pp_clause conclusion);
+      Log.debugf error (fun k -> k "Empty history for clause: %a" St.pp_clause conclusion);
       raise (Resolution_error "Empty history")
     | St.History [ c ] ->
       let duplicates, res = analyze (list c) in
diff --git a/src/core/Solver_intf.ml b/src/core/Solver_intf.ml
index 2852aadc..39e47ef9 100644
--- a/src/core/Solver_intf.ml
+++ b/src/core/Solver_intf.ml
@@ -38,14 +38,22 @@ type ('clause, 'proof) unsat_state = {
 }
 (** The type of values returned when the solver reaches an UNSAT state. *)
 
+type 'clause export = {
+  hyps: 'clause Vec.t;
+  history: 'clause Vec.t;
+  local: 'clause Vec.t;
+}
+(** Export internal state *)
+
 (** The external interface implemented by safe solvers, such as the one
     created by the {!Solver.Make} and {!Mcsolver.Make} functors. *)
 module type S = sig
-
   (** {2 Internal modules}
       These are the internal modules used, you should probably not use them
       if you're not familiar with the internals of mSAT. *)
 
+  (* TODO: replace {!St} with explicit modules (Expr, Var, Lit, Elt,...)
+     with carefully picked interfaces *)
   module St : Solver_types.S
   (** WARNING: Very dangerous module that expose the internal representation used
       by the solver. *)
@@ -96,14 +104,6 @@ module type S = sig
   val get_tag : St.clause -> int option
   (** Recover tag from a clause, if any *)
 
-  val export_dimacs : Format.formatter -> unit -> unit
-  (** Prints the entire set of clauses in the input problem
-      (including hypothesis, lemmas and local assumptions),
-      in the dimacs format. *)
-
-  val export_icnf : Format.formatter -> unit -> unit
-  (** Export the current problem contents to iCNF format.
-      This function is meant to be used icnrementally, i.e.
-      called for each return value of the solve function. *)
+  val export : unit -> St.clause export
 end
 
diff --git a/src/core/Solver_types.ml b/src/core/Solver_types.ml
index 1edbfbd3..1fd4b7b7 100644
--- a/src/core/Solver_types.ml
+++ b/src/core/Solver_types.ml
@@ -40,6 +40,7 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct
     lid : int;
     term : term;
     mutable l_level : int;
+    mutable l_idx: int;
     mutable l_weight : float;
     mutable assigned : term option;
   }
@@ -51,7 +52,8 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct
     mutable used : int;
     mutable seen : seen;
     mutable v_level : int;
-    mutable v_weight : float;
+    mutable v_idx: int; (** position in heap *)
+    mutable v_weight : float; (** Weight (for the heap), tracking activity *)
     mutable v_assignable: lit list option;
     mutable reason : reason option;
   }
@@ -101,6 +103,7 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct
       seen = Nope;
       v_level = -1;
       v_weight = -1.;
+      v_idx= -1;
       v_assignable = None;
       reason = None;
     }
@@ -146,6 +149,7 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct
         lid = !cpt_mk_var;
         term = t;
         l_weight = 1.;
+        l_idx= -1;
         l_level = -1;
         assigned = None;
       } in
@@ -168,6 +172,7 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct
             used = 0;
             seen = Nope;
             v_level = -1;
+            v_idx= -1;
             v_weight = 0.;
             v_assignable = None;
             reason = None;
@@ -244,18 +249,22 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct
   let of_atom a = Atom a
 
   (* Elements *)
-  let elt_of_lit l = E_lit l
-  let elt_of_var v = E_var v
+  let[@inline] elt_of_lit l = E_lit l
+  let[@inline] elt_of_var v = E_var v
 
   let get_elt_id = function
     | E_lit l -> l.lid | E_var v ->  v.vid
   let get_elt_level = function
     | E_lit l -> l.l_level | E_var v ->  v.v_level
+  let get_elt_idx = function
+    | E_lit l -> l.l_idx | E_var v ->  v.v_idx
   let get_elt_weight = function
     | E_lit l -> l.l_weight | E_var v ->  v.v_weight
 
   let set_elt_level e lvl = match e with
     | E_lit l -> l.l_level <- lvl | E_var v ->  v.v_level <- lvl
+  let set_elt_idx e i = match e with
+    | E_lit l -> l.l_idx <- i | E_var v ->  v.v_idx <- i
   let set_elt_weight e w = match e with
     | E_lit l -> l.l_weight <- w | E_var v ->  v.v_weight <- w
 
@@ -346,11 +355,11 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct
   let pp_atoms_vec out vec =
     Array.iter (fun a -> Format.fprintf out "%a@ " pp_atom a) vec
 
-  let pp_clause out {name=name; atoms=arr; cpremise=cp; } =
+  let pp_clause out {name=name; atoms=arr; cpremise=cp;_} =
     Format.fprintf out "%s@[<hov>{@[<hov>%a@]}@ cpremise={@[<hov>%a@]}@]"
       name pp_atoms_vec arr pp_premise cp
 
-  let pp_dimacs fmt { atoms; } =
+  let pp_dimacs fmt {atoms;_} =
     let aux fmt a =
       Array.iter (fun p ->
           Format.fprintf fmt "%s%d "
diff --git a/src/core/Solver_types_intf.ml b/src/core/Solver_types_intf.ml
index e9832e14..24022f7d 100644
--- a/src/core/Solver_types_intf.ml
+++ b/src/core/Solver_types_intf.ml
@@ -45,6 +45,7 @@ module type S = sig
     lid : int;                      (** Unique identifier *)
     term : term;                    (** Wrapped term *)
     mutable l_level : int;          (** Decision level of the assignment *)
+    mutable l_idx: int;             (** index in heap *)
     mutable l_weight : float;       (** Weight (for the heap) *)
     mutable assigned : term option; (** Assignment *)
   }
@@ -57,6 +58,7 @@ module type S = sig
     mutable used : int;         (** Number of attached clause that contain the var *)
     mutable seen : seen;        (** Boolean used during propagation *)
     mutable v_level : int;      (** Level of decision/propagation *)
+    mutable v_idx: int;         (** rank in variable heap *)
     mutable v_weight : float;   (** Variable weight (for the heap) *)
     mutable v_assignable: lit list option;
     (** In mcsat, the list of lits that wraps subterms of the formula wrapped. *)
@@ -144,8 +146,10 @@ module type S = sig
 
   val get_elt_id : elt -> int
   val get_elt_level : elt -> int
+  val get_elt_idx : elt -> int
   val get_elt_weight : elt -> float
   val set_elt_level : elt -> int -> unit
+  val set_elt_idx : elt -> int -> unit
   val set_elt_weight : elt -> float -> unit
   (** Accessors for elements *)
 
diff --git a/src/util/vec.ml b/src/core/Vec.ml
similarity index 77%
rename from src/util/vec.ml
rename to src/core/Vec.ml
index 8a3c82b5..c8c68f84 100644
--- a/src/util/vec.ml
+++ b/src/core/Vec.ml
@@ -11,7 +11,11 @@
 (*                                                                        *)
 (**************************************************************************)
 
-type 'a t = { mutable dummy: 'a; mutable data : 'a array; mutable sz : int }
+type 'a t = {
+  mutable dummy: 'a;
+  mutable data : 'a array;
+  mutable sz : int;
+}
 
 let _size_too_big()=
   failwith "Vec: capacity exceeds maximum array size"
@@ -20,7 +24,7 @@ let make capa d =
   if capa > Sys.max_array_length then _size_too_big();
   {data = Array.make capa d; sz = 0; dummy = d}
 
-let make_empty d = {data = [||]; sz=0; dummy=d }
+let[@inline] make_empty d = {data = [||]; sz=0; dummy=d }
 
 let init capa f d =
   if capa > Sys.max_array_length then _size_too_big();
@@ -30,10 +34,9 @@ let from_array data sz d =
   assert (sz <= Array.length data);
   {data = data; sz = sz; dummy = d}
 
-let from_list l sz d =
-  let l = ref l in
-  let f_init i = match !l with [] -> assert false | e::r -> l := r; e in
-  {data = Array.init sz f_init; sz = sz; dummy = d}
+let from_list l d =
+  let a = Array.of_list l in
+  from_array a (Array.length a) d
 
 let to_list s =
   let l = ref [] in
@@ -42,20 +45,20 @@ let to_list s =
   done;
   List.rev !l
 
-let clear s = s.sz <- 0
+let[@inline] clear s = s.sz <- 0
 
-let shrink t i =
+let[@inline] shrink t i =
   assert (i >= 0);
   assert (i<=t.sz);
-  t.sz <- t.sz - i
+  t.sz <- i
 
-let pop t =
+let[@inline] pop t =
   if t.sz = 0 then invalid_arg "vec.pop";
   t.sz <- t.sz - 1
 
-let size t = t.sz
+let[@inline] size t = t.sz
 
-let is_empty t = t.sz = 0
+let[@inline] is_empty t = t.sz = 0
 
 let grow_to_exact t new_capa =
   assert (new_capa > Array.length t.data);
@@ -81,33 +84,39 @@ let grow_to_at_least t new_capa =
     grow_to_exact t !capa
   )
 
-let is_full t = Array.length t.data = t.sz
+let[@inline] is_full t = Array.length t.data = t.sz
 
-let push t e =
+let[@inline] push t e =
   if is_full t then grow_to_double_size t;
   t.data.(t.sz) <- e;
   t.sz <- t.sz + 1
 
-let last t =
+let[@inline] last t =
   if t.sz = 0 then invalid_arg "vec.last";
   t.data.(t.sz - 1)
 
-let get t i =
+let[@inline] pop_last t =
+  if t.sz = 0 then invalid_arg "vec.pop_last";
+  let x = t.data.(t.sz - 1) in
+  t.sz <- t.sz - 1;
+  x
+
+let[@inline] get t i =
   if i < 0 || i >= t.sz then invalid_arg "vec.get";
   Array.unsafe_get t.data i
 
-let set t i v =
+let[@inline] set t i v =
   if i < 0 || i > t.sz then invalid_arg "vec.set";
   if i = t.sz then
     push t v
   else
     Array.unsafe_set t.data i v
 
-let copy t =
+let[@inline] copy t =
   let data = Array.copy t.data in
   {t with data; }
 
-let move_to t t' =
+let[@inline] move_to t t' =
   t'.data <- Array.copy t.data;
   t'.sz <- t.sz
 
@@ -118,11 +127,17 @@ let remove t e =
   for i = !j to t.sz - 2 do t.data.(i) <- t.data.(i+1) done;
   pop t
 
-let fast_remove t i =
+let[@inline] fast_remove t i =
   assert (i < t.sz);
   t.data.(i) <- t.data.(t.sz - 1);
   t.sz <- t.sz - 1
 
+let filter_in_place f vec =
+  let i = ref 0 in
+  while !i < size vec do
+    if f (get vec !i) then incr i else fast_remove vec !i
+  done
+
 let sort t f =
   let sub_arr = Array.sub t.data 0 t.sz in
   Array.fast_sort f sub_arr;
@@ -130,16 +145,21 @@ let sort t f =
 
 let iter f t =
   for i = 0 to size t - 1 do
-    f t.data.(i)
+    f (Array.unsafe_get t.data i)
   done
 
+let append a b =
+  grow_to_at_least a (size a + size b);
+  iter (push a) b
+
 let fold f acc t =
   let rec _fold f acc t i =
     if i=t.sz
     then acc
-    else
-      let acc' = f acc (Array.get t.data i) in
+    else (
+      let acc' = f acc (Array.unsafe_get t.data i) in
       _fold f acc' t (i+1)
+    )
   in _fold f acc t 0
 
 exception ExitVec
@@ -147,7 +167,7 @@ exception ExitVec
 let exists p t =
   try
     for i = 0 to t.sz - 1 do
-      if p (Array.get t.data i) then raise ExitVec
+      if p (Array.unsafe_get t.data i) then raise ExitVec
     done;
     false
   with ExitVec -> true
@@ -155,7 +175,7 @@ let exists p t =
 let for_all p t =
   try
     for i = 0 to t.sz - 1 do
-      if not (p (Array.get t.data i)) then raise ExitVec
+      if not (p (Array.unsafe_get t.data i)) then raise ExitVec
     done;
     true
   with ExitVec -> false
diff --git a/src/util/vec.mli b/src/core/Vec.mli
similarity index 88%
rename from src/util/vec.mli
rename to src/core/Vec.mli
index d57b9cc3..914d4eba 100644
--- a/src/util/vec.mli
+++ b/src/core/Vec.mli
@@ -30,8 +30,7 @@ val from_array : 'a array -> int -> 'a -> 'a t
     to create a vector. [size] is the length of the slice of [data] that is
     used ([size <= Array.length data] must hold) *)
 
-val from_list : 'a list -> int -> 'a -> 'a t
-(** [from_list l n] takes the [n] first elements of list [l] to make a new vector *)
+val from_list : 'a list -> 'a -> 'a t
 
 val to_list : 'a t -> 'a list
 (** Returns the list of elements of the vector *)
@@ -40,6 +39,8 @@ val clear : 'a t -> unit
 (** Set size to 0, doesn't free elements *)
 
 val shrink : 'a t -> int -> unit
+(** [shrink vec sz] resets size of [vec] to [sz].
+    Assumes [sz >=0 && sz <= size vec] *)
 
 val pop : 'a t -> unit
 (** Pop last element
@@ -62,10 +63,17 @@ val is_full : 'a t -> bool
 
 val push : 'a t -> 'a -> unit
 
+val append : 'a t -> 'a t -> unit
+(** [append v1 v2] pushes all elements of [v2] into [v1] *)
+
 val last : 'a t -> 'a
 (** Last element, or
     @raise Invalid_argument if the vector is empty *)
 
+val pop_last : 'a t -> 'a
+(** Combine {!last} and {!pop}: remove last element and return it
+    @raise Invalid_argument if empty *)
+
 val get : 'a t -> int -> 'a
 (** get the element at the given index, or
     @raise Invalid_argument if the index is not valid *)
@@ -88,6 +96,10 @@ val fast_remove : 'a t -> int -> unit
 (** Remove element at index [i] without preserving order
     (swap with last element) *)
 
+val filter_in_place : ('a -> bool) -> 'a t -> unit
+(** [filter_in_place f v] removes from [v] the elements that do
+    not satisfy [f] *)
+
 val sort : 'a t -> ('a -> 'a -> int) -> unit
 (** Sort in place the array *)
 
diff --git a/src/core/jbuild b/src/core/jbuild
index 777d98f1..22ef52fb 100644
--- a/src/core/jbuild
+++ b/src/core/jbuild
@@ -1,8 +1,5 @@
 ; vim:ft=lisp:
 
-(jbuild_version 1)
-
-; main binary
 (library
   ((name msat)
    (public_name msat)
@@ -12,4 +9,3 @@
    (ocamlopt_flags (:standard -O3 -bin-annot
                     -unbox-closures -unbox-closures-factor 20))
   ))
-
diff --git a/src/doc.txt b/src/core/msat.mld
similarity index 100%
rename from src/doc.txt
rename to src/core/msat.mld
diff --git a/src/main/jbuild b/src/main/jbuild
new file mode 100644
index 00000000..08a42162
--- /dev/null
+++ b/src/main/jbuild
@@ -0,0 +1,13 @@
+
+; vim:ft=lisp:
+
+; main binary
+(executable
+  ((name main)
+   (public_name msat_solver)
+   (package msat_solver)
+   (libraries (msat msat.backend msat.sat msat.smt msat.mcsat dolmen))
+   (flags (:standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string))
+   (ocamlopt_flags (:standard -O3 -color always
+                    -unbox-closures -unbox-closures-factor 20))
+  ))
diff --git a/src/main.ml b/src/main/main.ml
similarity index 89%
rename from src/main.ml
rename to src/main/main.ml
index 952a69e1..30611d77 100644
--- a/src/main.ml
+++ b/src/main/main.ml
@@ -4,6 +4,8 @@ Copyright 2014 Guillaume Bury
 Copyright 2014 Simon Cruanes
 *)
 
+open Msat
+
 exception Incorrect_model
 exception Out_of_time
 exception Out_of_space
@@ -26,20 +28,20 @@ end
 
 module Make
     (S : External.S)
-    (T : Type.S with type atom := S.atom)
+    (T : Msat_solver.Type.S with type atom := S.atom)
   : sig
     val do_task : Dolmen.Statement.t -> unit
   end = struct
 
-  module D = Dot.Make(S.Proof)(Dot.Default(S.Proof))
+  module D = Msat_backend.Dot.Make(S.Proof)(Msat_backend.Dot.Default(S.Proof))
 
   let hyps = ref []
 
   let check_model state =
     let check_clause c =
       let l = List.map (function a ->
-          Log.debugf 99 "Checking value of %a"
-            (fun k -> k S.St.pp_atom (S.St.add_atom a));
+          Log.debugf 99
+            (fun k -> k "Checking value of %a" S.St.pp_atom (S.St.add_atom a));
           state.Solver_intf.eval a) c in
       List.exists (fun x -> x) l
     in
@@ -47,7 +49,7 @@ module Make
     List.for_all (fun x -> x) l
 
   let prove ~assumptions =
-    let res = S.solve () in
+    let res = S.solve ~assumptions () in
     let t = Sys.time () in
     begin match res with
       | S.Sat state ->
@@ -86,10 +88,10 @@ module Make
       hyps := cnf @ !hyps;
       S.assume cnf
     | Dolmen.Statement.Pack [
-        { Dolmen.Statement.descr = Dolmen.Statement.Push 1; };
-        { Dolmen.Statement.descr = Dolmen.Statement.Antecedent f; };
+        { Dolmen.Statement.descr = Dolmen.Statement.Push 1;_ };
+        { Dolmen.Statement.descr = Dolmen.Statement.Antecedent f;_ };
         { Dolmen.Statement.descr = Dolmen.Statement.Prove []; };
-        { Dolmen.Statement.descr = Dolmen.Statement.Pop 1; };
+        { Dolmen.Statement.descr = Dolmen.Statement.Pop 1;_ };
       ] ->
       let assumptions = T.assumptions f in
       prove ~assumptions
@@ -104,9 +106,9 @@ module Make
         Dolmen.Statement.print s
 end
 
-module Sat = Make(Sat.Make(struct end))(Type_sat)
-module Smt = Make(Smt.Make(struct end))(Type_smt)
-module Mcsat = Make(Mcsat.Make(struct end))(Type_smt)
+module Sat = Make(Msat_sat.Sat.Make(struct end))(Msat_sat.Type_sat)
+module Smt = Make(Msat_smt.Smt.Make(struct end))(Msat_smt.Type_smt)
+module Mcsat = Make(Msat_mcsat.Mcsat.Make(struct end))(Msat_smt.Type_smt)
 
 let solver = ref (module Sat : S)
 let solver_list = [
@@ -225,8 +227,8 @@ let () =
   | Incorrect_model ->
     Format.printf "Internal error : incorrect *sat* model@.";
     exit 4
-  | Type_sat.Typing_error (msg, t)
-  | Type_smt.Typing_error (msg, t) ->
+  | Msat_sat.Type_sat.Typing_error (msg, t)
+  | Msat_smt.Type_smt.Typing_error (msg, t) ->
     let b = Printexc.get_backtrace () in
     let loc = match t.Dolmen.Term.loc with
       | Some l -> l | None -> Dolmen.ParseLocation.mk "<>" 0 0 0 0
diff --git a/src/util/backtrack.ml b/src/mcsat/backtrack.ml
similarity index 100%
rename from src/util/backtrack.ml
rename to src/mcsat/backtrack.ml
diff --git a/src/util/backtrack.mli b/src/mcsat/backtrack.mli
similarity index 100%
rename from src/util/backtrack.mli
rename to src/mcsat/backtrack.mli
diff --git a/src/mcsat/eclosure.ml b/src/mcsat/eclosure.ml
index 2fbbedb4..fb53655d 100644
--- a/src/mcsat/eclosure.ml
+++ b/src/mcsat/eclosure.ml
@@ -106,8 +106,9 @@ module Make(T : Key) = struct
       tag = (match mx.tag, my.tag with
           | Some (z, t1), Some (w, t2) ->
             if not (T.equal t1 t2) then begin
-              Log.debugf 3 "Tag shenanigan : %a (%a) <> %a (%a)" (fun k ->
-                  k T.print t1 T.print z T.print t2 T.print w);
+              Log.debugf 3
+                (fun k -> k "Tag shenanigan : %a (%a) <> %a (%a)" 
+                     T.print t1 T.print z T.print t2 T.print w);
               raise (Equal (z, w))
             end else Some (z, t1)
           | Some t, None | None, Some t -> Some t
@@ -223,7 +224,7 @@ module Make(T : Key) = struct
     | () -> ()
     | exception Equal (a, b) ->
       raise (Unsat (a, b, expl t a b))
-    | exception Same_tag (x, y) ->
+    | exception Same_tag (_, _) ->
       add_eq_aux t i j;
       let res = expl t i j in
       raise (Unsat (i, j, res))
diff --git a/src/mcsat/jbuild b/src/mcsat/jbuild
new file mode 100644
index 00000000..5c4061d3
--- /dev/null
+++ b/src/mcsat/jbuild
@@ -0,0 +1,13 @@
+; vim:ft=lisp:
+
+(library
+  ((name msat_mcsat)
+   (public_name msat.mcsat)
+   (libraries (msat msat.solver msat.smt))
+   (synopsis "mcsat interface")
+   (flags (:standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string -open Msat))
+   (ocamlopt_flags (:standard -O3 -bin-annot
+                    -unbox-closures -unbox-closures-factor 20))
+  ))
+
+
diff --git a/src/mcsat/mcsat.ml b/src/mcsat/mcsat.ml
index 40d35e49..10ad9720 100644
--- a/src/mcsat/mcsat.ml
+++ b/src/mcsat/mcsat.ml
@@ -5,9 +5,9 @@ Copyright 2014 Simon Cruanes
 *)
 
 module Make(Dummy:sig end) =
-  Mcsolver.Make(struct
+  Msat_solver.Mcsolver.Make(struct
     type proof = unit
-    module Term = Expr_smt.Term
-    module Formula = Expr_smt.Atom
+    module Term = Msat_smt.Expr_smt.Term
+    module Formula = Msat_smt.Expr_smt.Atom
   end)(Plugin_mcsat)(struct end)
 
diff --git a/src/mcsat/mcsat.mli b/src/mcsat/mcsat.mli
index edb13401..ddd06949 100644
--- a/src/mcsat/mcsat.mli
+++ b/src/mcsat/mcsat.mli
@@ -4,5 +4,5 @@ Copyright 2014 Guillaume Bury
 Copyright 2014 Simon Cruanes
 *)
 
-module Make(Dummy: sig end) : Solver.S with type St.formula = Expr_smt.atom
+module Make(Dummy: sig end) : Msat_solver.Solver.S with type St.formula = Msat_smt.Expr_smt.atom
 
diff --git a/src/mcsat/plugin_mcsat.ml b/src/mcsat/plugin_mcsat.ml
index 06c09c2e..610d7fc2 100644
--- a/src/mcsat/plugin_mcsat.ml
+++ b/src/mcsat/plugin_mcsat.ml
@@ -1,6 +1,8 @@
 
 (* Module initialization *)
 
+open Msat_smt
+
 module E = Eclosure.Make(Expr_smt.Term)
 module H = Backtrack.Hashtbl(Expr_smt.Term)
 module M = Hashtbl.Make(Expr_smt.Term)
@@ -63,7 +65,7 @@ let update_job x ((t, watchees) as job) =
   with Not_found ->
     add_job job x;
     begin match t with
-      | { Expr_smt.term = Expr_smt.App (f, tys, l) } ->
+      | { Expr_smt.term = Expr_smt.App (f, tys, l);_ } ->
         let is_prop = Expr_smt.(Ty.equal t.t_type Ty.prop) in
         let t_v = H.find map t in
         let l' = List.map (H.find map) l in
@@ -72,7 +74,7 @@ let update_job x ((t, watchees) as job) =
             let t', u_v = H.find interpretation u in
             if not (Expr_smt.Term.equal t_v u_v) then begin
               match t' with
-              | { Expr_smt.term = Expr_smt.App (_, _, r) } when is_prop ->
+              | { Expr_smt.term = Expr_smt.App (_, _, r); _ } when is_prop ->
                 let eqs = List.map2 (fun a b -> Expr_smt.Atom.neg (Expr_smt.Atom.eq a b)) l r in
                 if Expr_smt.(Term.equal u_v true_) then begin
                   let res = Expr_smt.Atom.pred t ::
@@ -83,7 +85,7 @@ let update_job x ((t, watchees) as job) =
                             Expr_smt.Atom.neg (Expr_smt.Atom.pred t) :: eqs in
                   raise (Absurd res)
                 end
-              | { Expr_smt.term = Expr_smt.App (_, _, r) } ->
+              | { Expr_smt.term = Expr_smt.App (_, _, r); _ } ->
                 let eqs = List.map2 (fun a b -> Expr_smt.Atom.neg (Expr_smt.Atom.eq a b)) l r in
                 let res = Expr_smt.Atom.eq t t' :: eqs in
                 raise (Absurd res)
@@ -117,25 +119,25 @@ let add_assign t v =
 (* Assignemnts *)
 
 let rec iter_aux f = function
-  | { Expr_smt.term = Expr_smt.Var _ } as t ->
-    Log.debugf 10 "Adding %a as assignable" (fun k -> k Expr_smt.Term.print t);
+  | { Expr_smt.term = Expr_smt.Var _; _ } as t ->
+    Log.debugf 10 (fun k -> k "Adding %a as assignable" Expr_smt.Term.print t);
     f t
-  | { Expr_smt.term = Expr_smt.App (_, _, l) } as t ->
+  | { Expr_smt.term = Expr_smt.App (_, _, l); _ } as t ->
     if l <> [] then add_watch t (t :: l);
     List.iter (iter_aux f) l;
-    Log.debugf 10 "Adding %a as assignable" (fun k -> k Expr_smt.Term.print t);
+    Log.debugf 10 (fun k -> k "Adding %a as assignable" Expr_smt.Term.print t);
     f t
 
 let iter_assignable f = function
-  | { Expr_smt.atom = Expr_smt.Pred { Expr_smt.term = Expr_smt.Var _ } } -> ()
-  | { Expr_smt.atom = Expr_smt.Pred ({ Expr_smt.term = Expr_smt.App (_, _, l) } as t) } ->
+  | { Expr_smt.atom = Expr_smt.Pred { Expr_smt.term = Expr_smt.Var _;_ }; _ } -> ()
+  | { Expr_smt.atom = Expr_smt.Pred ({ Expr_smt.term = Expr_smt.App (_, _, l);_} as t); _ } ->
     if l <> [] then add_watch t (t :: l);
     List.iter (iter_aux f) l;
-  | { Expr_smt.atom = Expr_smt.Equal (a, b) } ->
+  | { Expr_smt.atom = Expr_smt.Equal (a, b);_ } ->
     iter_aux f a; iter_aux f b
 
 let eval = function
-  | { Expr_smt.atom = Expr_smt.Pred t } ->
+  | { Expr_smt.atom = Expr_smt.Pred t; _ } ->
     begin try
         let v = H.find map t in
         if Expr_smt.Term.equal v true_ then
@@ -147,7 +149,7 @@ let eval = function
       with Not_found ->
         Plugin_intf.Unknown
     end
-  | { Expr_smt.atom = Expr_smt.Equal (a, b); sign } ->
+  | { Expr_smt.atom = Expr_smt.Equal (a, b); sign; _ } ->
     begin try
         let v_a = H.find map a in
         let v_b = H.find map b in
@@ -164,7 +166,7 @@ let eval = function
 
 let rec chain_eq = function
   | [] | [_] -> []
-  | a :: ((b :: r) as l) -> (Expr_smt.Atom.eq a b) :: chain_eq l
+  | a :: ((b :: _) as l) -> (Expr_smt.Atom.eq a b) :: chain_eq l
 
 let assume s =
   let open Plugin_intf in
@@ -176,11 +178,11 @@ let assume s =
         E.add_tag uf t v
       | Lit f ->
         begin match f with
-          | { Expr_smt.atom = Expr_smt.Equal (u, v); sign = true } ->
+          | { Expr_smt.atom = Expr_smt.Equal (u, v); sign = true;_ } ->
             E.add_eq uf u v
-          | { Expr_smt.atom = Expr_smt.Equal (u, v); sign = false } ->
+          | { Expr_smt.atom = Expr_smt.Equal (u, v); sign = false;_ } ->
             E.add_neq uf u v
-          | { Expr_smt.atom = Expr_smt.Pred p; sign } ->
+          | { Expr_smt.atom = Expr_smt.Pred p; sign;_ } ->
             let v = if sign then true_ else false_ in
             add_assign p v
         end
diff --git a/src/msat.mlpack b/src/msat.mlpack
deleted file mode 100644
index 088df142..00000000
--- a/src/msat.mlpack
+++ /dev/null
@@ -1,34 +0,0 @@
-# Debug
-Log
-
-# Interface definitions
-Formula_intf
-Theory_intf
-Plugin_intf
-Expr_intf
-Tseitin_intf
-Res_intf
-Solver_intf
-Solver_types_intf
-
-# Solver Modules
-Internal
-External
-Solver
-Mcsolver
-Solver_types
-
-# Proofs & Backends
-Res
-Backend_intf
-Dot
-Coq
-Dimacs
-Dedukti
-
-# Auxiliary modules
-Tseitin
-
-# Pure Sat solver
-Sat
-
diff --git a/src/msat.odocl b/src/msat.odocl
deleted file mode 100644
index 4e17798f..00000000
--- a/src/msat.odocl
+++ /dev/null
@@ -1,43 +0,0 @@
-# Log utilities
-util/Log
-
-# Interfaces
-core/Formula_intf
-core/Theory_intf
-core/Plugin_intf
-core/Expr_intf
-core/Res_intf
-core/Solver_types_intf
-core/Solver_intf
-solver/Tseitin_intf
-
-# Main modules
-core/Res
-core/Internal
-core/External
-core/Solver_types
-
-solver/Solver
-solver/Mcsolver
-solver/Tseitin
-
-# Backends
-backend/Dot
-backend/Coq
-backend/Dedukti
-backend/Backend_intf
-
-# SAT solver frontend
-sat/Sat
-#sat/Type_sat
-
-# SMT solver frontend
-#smt/Smt
-#smt/Expr_smt
-#smt/Type_smt
-#smt/Unionfind
-
-# MCsat solver frontend
-#mcsat/Mcsat
-#mcsat/Eclosure
-#mcsat/Plugin_mcsat
diff --git a/src/msat_sat.mlpack b/src/msat_sat.mlpack
deleted file mode 100644
index dc169686..00000000
--- a/src/msat_sat.mlpack
+++ /dev/null
@@ -1 +0,0 @@
-Sat
diff --git a/src/msat_smt.mlpack b/src/msat_smt.mlpack
deleted file mode 100644
index 1bba977f..00000000
--- a/src/msat_smt.mlpack
+++ /dev/null
@@ -1,3 +0,0 @@
-Smt
-Cc
-Explanation
diff --git a/src/sat/jbuild b/src/sat/jbuild
new file mode 100644
index 00000000..7ee505a7
--- /dev/null
+++ b/src/sat/jbuild
@@ -0,0 +1,13 @@
+; vim:ft=lisp:
+
+(library
+  ((name msat_sat)
+   (public_name msat.sat)
+   (libraries (msat msat.solver))
+   (synopsis "sat interface")
+   (flags (:standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string -open Msat))
+   (ocamlopt_flags (:standard -O3 -bin-annot
+                    -unbox-closures -unbox-closures-factor 20))
+  ))
+
+
diff --git a/src/sat/sat.ml b/src/sat/sat.ml
index 83de3bc9..5da9cebd 100644
--- a/src/sat/sat.ml
+++ b/src/sat/sat.ml
@@ -78,5 +78,5 @@ module Expr = struct
 end
 
 module Make(Dummy : sig end) =
-  Solver.Make(Expr)(Solver.DummyTheory(Expr))(struct end)
+  Msat_solver.Solver.Make(Expr)(Msat_solver.Solver.DummyTheory(Expr))(struct end)
 
diff --git a/src/sat/sat.mli b/src/sat/sat.mli
index ac49b6d4..500f740f 100644
--- a/src/sat/sat.mli
+++ b/src/sat/sat.mli
@@ -42,6 +42,6 @@ module Expr : sig
 end
 (** The module defining formulas *)
 
-module Make(Dummy : sig end) : Solver.S with type St.formula = Expr.t
+module Make(Dummy : sig end) : Msat_solver.Solver.S with type St.formula = Expr.t
 (** A functor that can generate as many solvers as needed. *)
 
diff --git a/src/sat/type_sat.ml b/src/sat/type_sat.ml
index 3c45b9cb..1b846e44 100644
--- a/src/sat/type_sat.ml
+++ b/src/sat/type_sat.ml
@@ -10,7 +10,7 @@ Copyright 2014 Simon Cruanes
 module Id = Dolmen.Id
 module Ast = Dolmen.Term
 module H = Hashtbl.Make(Id)
-module Formula = Tseitin.Make(Sat.Expr)
+module Formula = Msat_solver.Tseitin.Make(Sat.Expr)
 
 (* Exceptions *)
 (* ************************************************************************ *)
@@ -33,6 +33,8 @@ let find_id id =
 (* Actual parsing *)
 (* ************************************************************************ *)
 
+[@@@ocaml.warning "-9"]
+
 let rec parse = function
   | { Ast.term = Ast.Builtin Ast.True } ->
     Formula.f_true
@@ -59,6 +61,8 @@ let rec parse = function
   | t ->
     raise (Typing_error ("Term is not a pure proposition", t))
 
+[@@@ocaml.warning "+9"]
+
 (* Exported functions *)
 (* ************************************************************************ *)
 
diff --git a/src/sat/type_sat.mli b/src/sat/type_sat.mli
index 56fced24..512d358b 100644
--- a/src/sat/type_sat.mli
+++ b/src/sat/type_sat.mli
@@ -8,5 +8,5 @@ Copyright 2014 Simon Cruanes
     This module provides functions to parse terms from the untyped syntax tree
     defined in Dolmen, and generate formulas as defined in the Expr_sat module. *)
 
-include Type.S with type atom := Sat.Expr.t
+include Msat_solver.Type.S with type atom := Sat.Expr.t
 
diff --git a/src/smt/expr_smt.ml b/src/smt/expr_smt.ml
index 53beee62..51d87cd2 100644
--- a/src/smt/expr_smt.ml
+++ b/src/smt/expr_smt.ml
@@ -85,7 +85,7 @@ module Print = struct
   let rec list f sep fmt = function
     | [] -> ()
     | [x] -> f fmt x
-    | x :: ((y :: _) as r) ->
+    | x :: ((_ :: _) as r) ->
       Format.fprintf fmt "%a%s" f x sep;
       list f sep fmt r
 
@@ -521,5 +521,5 @@ module Atom = struct
 
 end
 
-module Formula = Tseitin.Make(Atom)
+module Formula = Msat_solver.Tseitin.Make(Atom)
 
diff --git a/src/smt/expr_smt.mli b/src/smt/expr_smt.mli
index 229cf51b..7e410e8d 100644
--- a/src/smt/expr_smt.mli
+++ b/src/smt/expr_smt.mli
@@ -322,5 +322,5 @@ module Atom : sig
 
 end
 
-module Formula : Tseitin.S with type atom = atom
+module Formula : Msat_solver.Tseitin.S with type atom = atom
 
diff --git a/src/smt/jbuild b/src/smt/jbuild
new file mode 100644
index 00000000..f8d694fe
--- /dev/null
+++ b/src/smt/jbuild
@@ -0,0 +1,13 @@
+; vim:ft=lisp:
+
+(library
+  ((name msat_smt)
+   (public_name msat.smt)
+   (libraries (msat msat.solver dolmen))
+   (synopsis "smt interface")
+   (flags (:standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string -open Msat))
+   (ocamlopt_flags (:standard -O3 -bin-annot
+                    -unbox-closures -unbox-closures-factor 20))
+  ))
+
+
diff --git a/src/smt/smt.ml b/src/smt/smt.ml
index 5acf092d..1321f5bd 100644
--- a/src/smt/smt.ml
+++ b/src/smt/smt.ml
@@ -4,8 +4,8 @@ Copyright 2014 Guillaume Bury
 Copyright 2014 Simon Cruanes
 *)
 
-module Th = Solver.DummyTheory(Expr_smt.Atom)
+module Th = Msat_solver.Solver.DummyTheory(Expr_smt.Atom)
 
 module Make(Dummy:sig end) =
-  Solver.Make(Expr_smt.Atom)(Th)(struct end)
+  Msat_solver.Solver.Make(Expr_smt.Atom)(Th)(struct end)
 
diff --git a/src/smt/smt.mli b/src/smt/smt.mli
index edb13401..5cec2966 100644
--- a/src/smt/smt.mli
+++ b/src/smt/smt.mli
@@ -4,5 +4,5 @@ Copyright 2014 Guillaume Bury
 Copyright 2014 Simon Cruanes
 *)
 
-module Make(Dummy: sig end) : Solver.S with type St.formula = Expr_smt.atom
+module Make(Dummy: sig end) : Msat_solver.Solver.S with type St.formula = Expr_smt.atom
 
diff --git a/src/smt/type_smt.ml b/src/smt/type_smt.ml
index a3f55125..5dbe3837 100644
--- a/src/smt/type_smt.ml
+++ b/src/smt/type_smt.ml
@@ -73,29 +73,29 @@ let find_global name =
 (* Symbol declarations *)
 let decl_ty_cstr id c =
   if H.mem global_env id then
-    Log.debugf 0 "Symbol '%a' has already been defined, overwriting previous definition"
-      (fun k -> k Id.print id);
+    Log.debugf 0
+      (fun k -> k "Symbol '%a' has already been defined, overwriting previous definition" Id.print id);
   H.add global_env id (`Ty c);
-  Log.debugf 1 "New type constructor : %a" (fun k -> k Expr.Print.const_ttype c)
+  Log.debugf 1 (fun k -> k "New type constructor : %a" Expr.Print.const_ttype c)
 
 let decl_term id c =
   if H.mem global_env id then
-    Log.debugf 0 "Symbol '%a' has already been defined, overwriting previous definition"
-      (fun k -> k Id.print id);
+    Log.debugf 0
+      (fun k -> k "Symbol '%a' has already been defined, overwriting previous definition" Id.print id);
   H.add global_env id (`Term c);
-  Log.debugf 1 "New constant : %a" (fun k -> k Expr.Print.const_ty c)
+  Log.debugf 1 (fun k -> k "New constant : %a" Expr.Print.const_ty c)
 
 (* Symbol definitions *)
 let def_ty id args body =
   if H.mem global_env id then
-    Log.debugf 0 "Symbol '%a' has already been defined, overwriting previous definition"
-      (fun k -> k Id.print id);
+    Log.debugf 0
+      (fun k -> k "Symbol '%a' has already been defined, overwriting previous definition" Id.print id);
   H.add global_env id (`Ty_alias (args, body))
 
 let def_term id ty_args args body =
   if H.mem global_env id then
-    Log.debugf 0 "Symbol '%a' has already been defined, overwriting previous definition"
-      (fun k -> k Id.print id);
+    Log.debugf 0
+      (fun k -> k "Symbol '%a' has already been defined, overwriting previous definition" Id.print id);
   H.add global_env id (`Term_alias (ty_args, args, body))
 
 (* Local Environment *)
@@ -126,8 +126,8 @@ let add_type_var env id v =
     else
       v
   in
-  Log.debugf 1 "New binding : %a -> %a"
-    (fun k -> k Id.print id Expr.Print.id_ttype v');
+  Log.debugf 1
+    (fun k -> k "New binding : %a -> %a" Id.print id Expr.Print.id_ttype v');
   v', { env with type_vars = M.add id v' env.type_vars }
 
 let add_type_vars env l =
@@ -143,8 +143,8 @@ let add_term_var env id v =
     else
       v
   in
-  Log.debugf 1 "New binding : %a -> %a"
-    (fun k -> k Id.print id Expr.Print.id_ty v');
+  Log.debugf 1
+    (fun k -> k "New binding : %a -> %a" Id.print id Expr.Print.id_ty v');
   v', { env with term_vars = M.add id v' env.term_vars }
 
 let find_var env name =
@@ -159,13 +159,13 @@ let find_var env name =
 
 (* Add local bound variables to env *)
 let add_let_term env id t =
-  Log.debugf 1 "New let-binding : %s -> %a"
-    (fun k -> k id.Id.name Expr.Print.term t);
+  Log.debugf 1
+    (fun k -> k "New let-binding : %s -> %a" id.Id.name Expr.Print.term t);
   { env with term_lets = M.add id t env.term_lets }
 
 let add_let_prop env id t =
-  Log.debugf 1 "New let-binding : %s -> %a"
-    (fun k -> k id.Id.name Expr.Formula.print t);
+  Log.debugf 1
+    (fun k -> k "New let-binding : %s -> %a" id.Id.name Expr.Formula.print t);
   { env with prop_lets = M.add id t env.prop_lets }
 
 let find_let env name =
@@ -207,13 +207,13 @@ let arity f =
   List.length Expr.(f.id_type.fun_vars) +
   List.length Expr.(f.id_type.fun_args)
 
-let ty_apply env ast f args =
+let ty_apply _env ast f args =
   try
     Expr.Ty.apply f args
   with Expr.Bad_ty_arity _ ->
     _bad_arity Expr.(f.id_name) (arity f) ast
 
-let term_apply env ast f ty_args t_args =
+let term_apply _env ast f ty_args t_args =
   try
     Expr.Term.apply f ty_args t_args
   with
@@ -277,6 +277,8 @@ let infer env s args =
 (* Expression parsing *)
 (* ************************************************************************ *)
 
+[@@@ocaml.warning "-9"]
+
 let rec parse_expr (env : env) t =
   match t with
   (* Base Types *)
@@ -582,13 +584,15 @@ let rec parse_fun ty_args t_args env = function
       | Formula _ -> _expected "type or term" ast
     end
 
+[@@@ocaml.warning "+9"]
+
 (* High-level parsing functions *)
 (* ************************************************************************ *)
 
 let decl id t =
   let env = empty_env () in
-  Log.debugf 5 "Typing declaration: %s : %a"
-    (fun k -> k id.Id.name Ast.print t);
+  Log.debugf 5
+    (fun k -> k "Typing declaration: %s : %a" id.Id.name Ast.print t);
   begin match parse_sig env t with
     | `Ty_cstr n -> decl_ty_cstr id (Expr.Id.ty_fun id.Id.name n)
     | `Fun_ty (vars, args, ret) ->
@@ -597,8 +601,8 @@ let decl id t =
 
 let def id t =
   let env = empty_env () in
-  Log.debugf 5 "Typing definition: %s = %a"
-    (fun k -> k id.Id.name Ast.print t);
+  Log.debugf 5
+    (fun k -> k "Typing definition: %s = %a" id.Id.name Ast.print t);
   begin match parse_fun [] [] env t with
     | `Ty (ty_args, body) -> def_ty id ty_args body
     | `Term (ty_args, t_args, body) -> def_term id ty_args t_args body
@@ -606,7 +610,7 @@ let def id t =
 
 let formula t =
   let env = empty_env () in
-  Log.debugf 5 "Typing top-level formula: %a" (fun k -> k Ast.print t);
+  Log.debugf 5 (fun k -> k "Typing top-level formula: %a" Ast.print t);
   parse_formula env t
 
 let assumptions t =
diff --git a/src/smt/type_smt.mli b/src/smt/type_smt.mli
index 51957bc8..7593432b 100644
--- a/src/smt/type_smt.mli
+++ b/src/smt/type_smt.mli
@@ -3,5 +3,5 @@
     This module provides functions to parse terms from the untyped syntax tree
     defined in Dolmen, and generate formulas as defined in the Expr_smt module. *)
 
-include Type.S with type atom := Expr_smt.Atom.t
+include Msat_solver.Type.S with type atom := Expr_smt.Atom.t
 
diff --git a/src/solver/jbuild b/src/solver/jbuild
new file mode 100644
index 00000000..f9e40772
--- /dev/null
+++ b/src/solver/jbuild
@@ -0,0 +1,12 @@
+; vim:ft=lisp:
+
+(library
+  ((name msat_solver)
+   (public_name msat.solver)
+   (libraries (msat dolmen))
+   (synopsis "mcsat solver util")
+   (flags (:standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string -open Msat))
+   (ocamlopt_flags (:standard -O3 -bin-annot
+                    -unbox-closures -unbox-closures-factor 20))
+  ))
+
diff --git a/src/solver/tseitin.ml b/src/solver/tseitin.ml
index f5dacd21..e1901aa1 100644
--- a/src/solver/tseitin.ml
+++ b/src/solver/tseitin.ml
@@ -242,7 +242,7 @@ module Make (F : Tseitin_intf.Arg) = struct
         (fun (_, acc) f ->
            match cnf f with
            | _, [] -> assert false
-           | cmb, [a] -> Some And, a :: acc
+           | _cmb, [a] -> Some And, a :: acc
            | Some And, l ->
              Some And, l @@ acc
            (* let proxy = mk_proxy () in *)
@@ -261,7 +261,7 @@ module Make (F : Tseitin_intf.Arg) = struct
         (fun (_, acc) f ->
            match cnf f with
            | _, [] -> assert false
-           | cmb, [a] -> Some Or, a :: acc
+           | _cmb, [a] -> Some Or, a :: acc
            | Some Or, l ->
              Some Or, l @@ acc
            (* let proxy = mk_proxy () in *)
diff --git a/src/util/type.ml b/src/solver/type.ml
similarity index 100%
rename from src/util/type.ml
rename to src/solver/type.ml
diff --git a/src/util/iheap.ml b/src/util/iheap.ml
deleted file mode 100644
index 25bbbb18..00000000
--- a/src/util/iheap.ml
+++ /dev/null
@@ -1,143 +0,0 @@
-(**************************************************************************)
-(*                                                                        *)
-(*                                  Cubicle                               *)
-(*             Combining model checking algorithms and SMT solvers        *)
-(*                                                                        *)
-(*                  Mohamed Iguernelala                                   *)
-(*                  Universite Paris-Sud 11                               *)
-(*                                                                        *)
-(*  Copyright 2011. This file is distributed under the terms of the       *)
-(*  Apache Software License version 2.0                                   *)
-(*                                                                        *)
-(**************************************************************************)
-
-module V = Sparse_vec
-
-type t = {heap : int Vec.t; indices : int V.t }
-
-let _absent_index = -1
-
-let init sz =
-  { heap    =  Vec.init sz (fun i -> i) 0;
-    indices =  V.init sz (fun i -> i) _absent_index}
-
-let left i   = (i lsl 1) + 1 (* i*2 + 1 *)
-let right i  = (i + 1) lsl 1 (* (i+1)*2 *)
-let parent i = (i - 1) asr 1 (* (i-1) / 2 *)
-
-(*
-let rec heap_property cmp ({heap=heap} as s) i =
-  i >= (Vec.size heap)  ||
-    ((i = 0 || not(cmp (Vec. get heap i) (Vec.get heap (parent i))))
-     && heap_property cmp s (left i) && heap_property cmp s (right i))
-
-let heap_property cmp s = heap_property cmp s 1
-*)
-
-let percolate_up cmp {heap=heap;indices=indices} i =
-  let x = Vec.get heap i in
-  let pi = ref (parent i) in
-  let i = ref i in
-  while !i <> 0 && cmp x (Vec.get heap !pi) do
-    Vec.set heap !i (Vec.get heap !pi);
-    V.set indices (Vec.get heap !i) !i;
-    i  := !pi;
-    pi := parent !i
-  done;
-  Vec.set heap !i x;
-  V.set indices x !i
-
-let percolate_down cmp {heap=heap;indices=indices} i =
-  let x = Vec.get heap i in
-  let sz = Vec.size heap in
-  let li = ref (left i) in
-  let ri = ref (right i) in
-  let i = ref i in
-  (try
-     while !li < sz do
-       let child =
-         if !ri < sz && cmp (Vec.get heap !ri) (Vec.get heap !li) then !ri
-         else !li
-       in
-       if not (cmp (Vec.get heap child) x) then raise Exit;
-       Vec.set heap !i (Vec.get heap child);
-       V.set indices (Vec.get heap !i) !i;
-       i  := child;
-       li := left !i;
-       ri := right !i
-     done;
-   with Exit -> ());
-  Vec.set heap !i x;
-  V.set indices x !i
-
-let in_heap s n = n < V.length s.indices && V.get s.indices n >= 0
-
-let decrease cmp s n =
-  assert (in_heap s n); percolate_up cmp s (V.get s.indices n)
-
-(*
-let increase cmp s n =
-  assert (in_heap s n); percolate_down cmp s (V.get s.indices n)
-*)
-
-let filter s filt cmp =
-  let j = ref 0 in
-  let lim = Vec.size s.heap in
-  for i = 0 to lim - 1 do
-    if filt (Vec.get s.heap i) then begin
-      Vec.set s.heap !j (Vec.get s.heap i);
-      V.set s.indices (Vec.get s.heap i) !j;
-      incr j;
-    end
-    else V.set s.indices (Vec.get s.heap i) _absent_index;
-  done;
-  Vec.shrink s.heap (lim - !j);
-  for i = (lim / 2) - 1 downto 0 do
-    percolate_down cmp s i
-  done
-
-let size s = Vec.size s.heap
-
-let is_empty s = Vec.is_empty s.heap
-
-let clear {heap; indices} =
-  Vec.clear heap;
-  V.clear indices;
-  ()
-
-let insert cmp s n =
-  if not (in_heap s n) then
-    begin
-      V.set s.indices n (Vec.size s.heap);
-      Vec.push s.heap n;
-      percolate_up cmp s (V.get s.indices n)
-    end
-
-let grow_to_at_least s sz =
-  V.resize s.indices sz;
-  Vec.grow_to_at_least s.heap sz
-
-(*
-let update cmp s n =
-  assert (heap_property cmp s);
-  begin
-    if in_heap s n then
-      begin
-        percolate_up cmp s (Vec.get s.indices n);
-        percolate_down cmp s (Vec.get s.indices n)
-      end
-    else insert cmp s n
-  end;
-  assert (heap_property cmp s)
-*)
-
-let remove_min cmp ({heap=heap; indices=indices} as s) =
-  if Vec.size heap=0 then raise Not_found;
-  let x = Vec.get heap 0 in
-  Vec.set heap 0 (Vec.last heap); (*heap.last()*)
-  V.set indices (Vec.get heap 0) 0;
-  V.set indices x (-1);
-  Vec.pop s.heap;
-  if Vec.size s.heap > 1 then percolate_down cmp s 0;
-  x
-
diff --git a/src/util/iheap.mli b/src/util/iheap.mli
deleted file mode 100644
index 6c1004a5..00000000
--- a/src/util/iheap.mli
+++ /dev/null
@@ -1,55 +0,0 @@
-(**************************************************************************)
-(*                                                                        *)
-(*                                  Cubicle                               *)
-(*             Combining model checking algorithms and SMT solvers        *)
-(*                                                                        *)
-(*                  Mohamed Iguernelala                                   *)
-(*                  Universite Paris-Sud 11                               *)
-(*                                                                        *)
-(*  Copyright 2011. This file is distributed under the terms of the       *)
-(*  Apache Software License version 2.0                                   *)
-(*                                                                        *)
-(**************************************************************************)
-
-type t
-(** Heap of integers, whose priority is increased or decreased
-    incrementally (see {!decrease} for instance) *)
-
-val init : int -> t
-(** Create a heap with the given number of values inside.
-    [init len] contains integers from [0] to [len-1]. *)
-
-val in_heap : t -> int -> bool
-(** [in_heap h x] returns [true] iff [x] is among the integers that belong to
-    the heap. *)
-
-val decrease : (int -> int -> bool) -> t -> int -> unit
-(** [decrease cmp h x] decreases the value associated to [x] within [h],
-    according to the comparison function [cmp] *)
-
-(*val increase : (int -> int -> bool) -> t -> int -> unit*)
-
-val size : t -> int
-(** Number of integers within the heap *)
-
-val is_empty : t -> bool
-
-val clear : t -> unit
-(** Clear the content of the heap *)
-
-val insert : (int -> int -> bool) -> t -> int -> unit
-(** Insert a new integer into the heap, according to the given comparison *)
-
-val grow_to_at_least: t -> int -> unit
-(** Hint: augment the internal capacity of the heap until it reaches at
-    least the given integer *)
-
-(*val update : (int -> int -> bool) -> t -> int -> unit*)
-
-val remove_min : (int -> int -> bool) -> t -> int
-(** Remove and return the integer that has the lowest value from the heap
-    @raise Not_found if the heap is empty *)
-
-val filter : t -> (int -> bool) -> (int -> int -> bool) -> unit
-(** Filter out values that don't satisfy the predicate. A comparison
-    function is used to re-order the heap *)
diff --git a/tests/jbuild b/tests/jbuild
new file mode 100644
index 00000000..988fae01
--- /dev/null
+++ b/tests/jbuild
@@ -0,0 +1,16 @@
+; vim:ft=lisp:
+
+(executable
+  ((name test_api)
+   (libraries (msat msat.backend msat.sat msat.smt msat.mcsat dolmen))
+   (flags (:standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string))
+   (ocamlopt_flags (:standard -O3 -color always
+                    -unbox-closures -unbox-closures-factor 20))
+  ))
+
+(alias
+ ((name    runtest)
+  (deps    (test_api.exe))
+  (action  (run ${<}))))
+
+
diff --git a/tests/run b/tests/run
index 4d90b8a3..463ab373 100755
--- a/tests/run
+++ b/tests/run
@@ -1,7 +1,7 @@
 #!/bin/bash
 
 CURDIR=`dirname $0`
-SOLVER="$CURDIR/../msat"
+SOLVER="$CURDIR/../msat.exe"
 
 solvertest () {
     for f in `find -L $1 -type f -name '*.cnf' -o -name '*.smt2'`
diff --git a/tests/test_api.ml b/tests/test_api.ml
index e575758e..158dc30b 100644
--- a/tests/test_api.ml
+++ b/tests/test_api.ml
@@ -6,8 +6,11 @@ Copyright 2014 Simon Cruanes
 
 (* Tests that require the API *)
 
+open Msat
+open Msat_sat
+
 module F = Sat.Expr
-module T = Tseitin.Make(F)
+module T = Msat_solver.Tseitin.Make(F)
 
 let (|>) x f = f x