diff --git a/.header b/.header
deleted file mode 100644
index fe8863b5..00000000
--- a/.header
+++ /dev/null
@@ -1,5 +0,0 @@
-(*
-MSAT is free software, using the Apache license, see file LICENSE
-Copyright 2014 Guillaume Bury
-Copyright 2014 Simon Cruanes
-*)
diff --git a/src/sat/.gitignore b/src/sat/.gitignore
new file mode 100644
index 00000000..f07c6d70
--- /dev/null
+++ b/src/sat/.gitignore
@@ -0,0 +1,13 @@
+_build/
+*.annot
+*.native
+*.log
+*.status
+.*.swp
+.session
+*.docdir
+src/util/log.ml
+doc/index.html
+*.exe
+.merlin
+*.install
diff --git a/src/sat/CHANGELOG.md b/src/sat/CHANGELOG.md
new file mode 100644
index 00000000..0efb4bb4
--- /dev/null
+++ b/src/sat/CHANGELOG.md
@@ -0,0 +1,118 @@
+# CHANGES
+
+## 0.9.1
+
+- add `on_conflit` callback
+- fix termination issue when using `push_decision_lit` from plugin
+
+## 0.9
+
+- feat: allow the theory to ask for some literals to be decided on
+- feat: allow to set the default polarity of variables at creation time
+
+## 0.8.3
+
+- support containers 3.0
+
+## 0.8.2
+
+- fix opam file
+- fix: allow conflicts below decision level in `Make_cdcl_t`
+
+## 0.8.1
+
+- fixes in `Heap`
+- package for `msat-bin`
+- use `iter` instead of `sequence` in dune and opam files
+- more docs
+
+## 0.8
+
+big refactoring, change of API with fewer functions, etc.
+see `git log` for more details.
+
+## 0.6.1
+
+- add simple functor for DOT backend
+- various bugfixes
+
+## 0.6
+
+### Feature
+
+- An already instantiated sat solver in the Sat module
+- A `full_slice` function for running possibly expensive satisfiability
+  tests (in SMT) when a propositional model has been found
+- Forgetful propagations: propagations whose reason (i.e clause) is not watched
+
+## 0.5.1
+
+### Bug
+
+- Removed some needless allocations
+
+### Breaking
+
+- Better interface for mcsat propagations
+
+### Feature
+
+- Allow level 0 semantic propagations
+
+## 0.5
+
+### Bug
+
+- Grow heap when adding local hyps
+- Avoid forgetting some one atom clauses
+- Fixed a bug for propagations at level 0
+- Late propagations need to be re-propagated
+- Fixed conflict at level 0
+- Avoid forgetting some theory conflict clauses
+
+### Breaking
+
+- Changed `if_sat` interface
+
+## 0.4.1
+
+### Bug
+
+- fix bug in `add_clause`
+
+## 0.4
+
+- performance improvements
+- many bugfixes
+- more tests
+
+### Breaking
+
+- remove push/pop (source of many bugs)
+- replaced by solve : assumptions:lit list -> unit -> result
+
+### Features
+
+- Accept late conflict clauses
+- cleaner API, moving some types outside the client-required interface
+
+## 0.3
+
+### Features
+
+- Proofs for atoms at level 0
+- Compatibility with ocaml >= 4.00
+- Released some restrictions on dummy sat theories
+
+## 0.2
+
+### Breaking
+
+- Log argument has been removed from functors
+- All the functors now take a dummy last argument to ensure the solver modules are unique
+
+### Features
+
+- push/pop operations
+- access to decision level when evaluating literals
+
diff --git a/src/sat/README.md b/src/sat/README.md
new file mode 100644
index 00000000..8cf81dcc
--- /dev/null
+++ b/src/sat/README.md
@@ -0,0 +1,188 @@
+# MSAT  [![Build Status](https://travis-ci.org/Gbury/mSAT.svg?branch=master)](https://travis-ci.org/Gbury/mSAT)
+
+MSAT is an OCaml library that features a modular SAT-solver and some
+extensions (including SMT), derived from [Alt-Ergo Zero](http://cubicle.lri.fr/alt-ergo-zero).
+
+It was presented at [ICFP 2017](https://icfp17.sigplan.org/event/ocaml-2017-papers-msat-an-ocaml-sat-solver),
+using a [poster](https://github.com/Gbury/mSAT/blob/master/articles/icfp_2017.pdf)
+
+
+## COPYRIGHT
+
+This program is distributed under the Apache Software License version
+2.0. See the enclosed file `LICENSE`.
+
+## Documentation
+
+See https://gbury.github.io/mSAT/
+
+## INSTALLATION
+
+### Via opam
+
+Once the package is on [opam](http://opam.ocaml.org), just `opam install msat`.
+For the development version, use:
+
+```
+opam pin add msat https://github.com/Gbury/mSAT.git
+```
+
+### Manual installation
+
+You will need `dune` and `iter`. The command is:
+
+```
+$ make install
+```
+
+## USAGE
+
+### Generic SAT/SMT Solver
+
+A modular implementation of the SMT algorithm can be found in the `Msat.Solver` module,
+as a functor which takes two modules :
+
+  - A representation of formulas (which implements the `Formula_intf.S` signature)
+
+  - A theory (which implements the `Theory_intf.S` signature) to check consistence of assertions.
+
+  - A dummy empty module to ensure generativity of the solver (solver modules heavily relies on
+  side effects to their internal state)
+
+### Sat Solver
+
+A ready-to-use SAT solver is available in the `Msat_sat` module
+using the `msat.sat` library. It can be loaded
+as shown in the following code :
+
+```ocaml
+# #require "msat";;
+# #require "msat.sat";;
+# #print_depth 0;; (* do not print details *)
+```
+
+Then we can create a solver and create some boolean variables:
+
+```ocaml
+module Sat = Msat_sat
+module E = Sat.Int_lit (* expressions *)
+
+let solver = Sat.create()
+
+(* We create here two distinct atoms *)
+let a = E.fresh ()    (* A 'new_atom' is always distinct from any other atom *)
+let b = E.make 1      (* Atoms can be created from integers *)
+```
+
+We can try and check the satisfiability of some clauses — here, the clause `a or b`.
+`Sat.assume` adds a list of clauses to the solver. Calling `Sat.solve`
+will check the satisfiability of the current set of clauses, here "Sat".
+
+```ocaml
+# a <> b;;
+- : bool = true
+# Sat.assume solver [[a; b]] ();;
+- : unit = ()
+# let res = Sat.solve solver;;
+val res : Sat.res = Sat.Sat ...
+```
+
+The Sat solver has an incremental mutable state, so we still have
+the clause `a or b` in our assumptions.
+We add `not a` and `not b` to the state, and get "Unsat".
+
+```ocaml
+# Sat.assume solver [[E.neg a]; [E.neg b]] () ;;
+- : unit = ()
+# let res = Sat.solve solver ;;
+val res : Sat.res = Sat.Unsat ...
+```
+
+#### Formulas API
+
+Writing clauses by hand can be tedious and error-prone.
+The functor `Msat_tseitin.Make` in the library `msat.tseitin`
+proposes a formula AST (parametrized by
+atoms) and a function to convert these formulas into clauses:
+
+```ocaml
+# #require "msat.tseitin";;
+```
+
+```ocaml
+(* Module initialization *)
+module F = Msat_tseitin.Make(E)
+
+let solver = Sat.create ()
+
+(* We create here two distinct atoms *)
+let a = E.fresh ()    (* A fresh atom is always distinct from any other atom *)
+let b = E.make 1      (* Atoms can be created from integers *)
+
+(* Let's create some formulas *)
+let p = F.make_atom a
+let q = F.make_atom b
+let r = F.make_and [p; q]
+let s = F.make_or [F.make_not p; F.make_not q]
+```
+
+We can try and check the satisfiability of the given formulas, by turning
+it into clauses using `make_cnf`:
+
+```ocaml
+# Sat.assume solver (F.make_cnf r) ();;
+- : unit = ()
+# Sat.solve solver;;
+- : Sat.res = Sat.Sat ...
+```
+
+```ocaml
+# Sat.assume solver (F.make_cnf s) ();;
+- : unit = ()
+# Sat.solve solver ;;
+- : Sat.res = Sat.Unsat ...
+```
+
+### CDCL(T): a Sudoku solver as an example
+
+The directory `src/sudoku/` contains a simple Sudoku solver that
+uses the interface `Msat.Make_cdcl_t`.
+In essence, it implements the logical theory `CDCL(Sudoku)`.
+The script `sudoku_solve.sh` compiles and runs the solver,
+as does `dune exec src/sudoku/sudoku_solve.exe`.
+
+It's able to parse sudoku grids denoted as 81 integers
+(see `tests/sudoku/sudoku.txt` for example).
+
+Here is a sample grid and the output from the solver (in roughly .5s):
+
+```sh non-deterministic=command
+$ echo '..............3.85..1.2.......5.7.....4...1...9.......5......73..2.1........4...9' > sudoku.txt
+$ dune exec src/sudoku/sudoku_solve.exe -- sudoku.txt
+...
+#########################
+solve grid:
+  .........
+  .....3.85
+  ..1.2....
+  ...5.7...
+  ..4...1..
+  .9.......
+  5......73
+  ..2.1....
+  ....4...9
+  
+...
+  987654321
+  246173985
+  351928746
+  128537694
+  634892157
+  795461832
+  519286473
+  472319568
+  863745219
+  
+###################
+...
+```
diff --git a/src/sat/dune b/src/sat/dune
new file mode 100644
index 00000000..8b682629
--- /dev/null
+++ b/src/sat/dune
@@ -0,0 +1,10 @@
+
+(alias
+ (name runtest)
+ (deps README.md src/core/msat.cma src/sat/msat_sat.cma (source_tree src))
+ (locks test)
+ (package msat)
+ (action (progn
+          (run mdx test README.md)
+          (diff? README.md README.md.corrected))))
+
diff --git a/src/sat/src/backend/Backend_intf.ml b/src/sat/src/backend/Backend_intf.ml
new file mode 100644
index 00000000..29900a0c
--- /dev/null
+++ b/src/sat/src/backend/Backend_intf.ml
@@ -0,0 +1,27 @@
+(*
+MSAT is free software, using the Apache license, see file LICENSE
+Copyright 2014 Guillaume Bury
+Copyright 2014 Simon Cruanes
+*)
+
+(** Backend interface
+
+    This modules defines the interface of the modules providing
+    export of proofs.
+*)
+
+module type S = sig
+  (** Proof exporting
+
+      Currently, exporting a proof means printing it into a file
+      according to the conventions of a given format.
+  *)
+
+  type t
+  (** The type of proofs. *)
+
+  val pp : Format.formatter -> t -> unit
+  (** A function for printing proofs in the desired format. *)
+
+end
+
diff --git a/src/sat/src/backend/Coq.ml b/src/sat/src/backend/Coq.ml
new file mode 100644
index 00000000..ffb736fd
--- /dev/null
+++ b/src/sat/src/backend/Coq.ml
@@ -0,0 +1,193 @@
+(*
+MSAT is free software, using the Apache license, see file LICENSE
+Copyright 2015 Guillaume Bury
+*)
+
+module type S = Backend_intf.S
+
+module type Arg = sig
+
+  type hyp
+  type lemma
+  type assumption
+
+  val prove_hyp : Format.formatter -> string -> hyp -> unit
+  val prove_lemma : Format.formatter -> string -> lemma -> unit
+  val prove_assumption : Format.formatter -> string -> assumption -> unit
+
+end
+
+module Make(S : Msat.S)(A : Arg with type hyp := S.clause
+                                and type lemma := S.clause
+                                and type assumption := S.clause) = struct
+
+  module Atom = S.Atom
+  module Clause = S.Clause
+  module M = Map.Make(S.Atom)
+  module C_tbl = S.Clause.Tbl
+  module P = S.Proof
+
+  let name = Clause.name
+
+  let clause_map c =
+    let rec aux acc a i =
+      if i >= Array.length a then acc
+      else begin
+        let name = Format.sprintf "A%d" i in
+        aux (M.add a.(i) name acc) a (i + 1)
+      end
+    in
+    aux M.empty (Clause.atoms c) 0
+
+  let clause_iter m format fmt clause =
+    let aux atom = Format.fprintf fmt format (M.find atom m) in
+    Array.iter aux (Clause.atoms clause)
+
+  let elim_duplicate fmt goal hyp _ =
+    (** Printing info comment in coq *)
+    Format.fprintf fmt
+      "(* Eliminating doublons. Goal : %s ; Hyp : %s *)@\n"
+      (name goal) (name hyp);
+    (** Prove the goal: intro the atoms, then use them with the hyp *)
+    let m = clause_map goal in
+    Format.fprintf fmt "pose proof @[<hov>(fun %a=>@ %s%a) as %s@].@\n"
+      (clause_iter m "%s@ ") goal (name hyp)
+      (clause_iter m "@ %s") hyp (name goal)
+
+  let resolution_aux m a h1 h2 fmt () =
+    Format.fprintf fmt "%s%a" (name h1)
+      (fun fmt -> Array.iter (fun b ->
+           if b == a then begin
+             Format.fprintf fmt "@ (fun p =>@ %s%a)"
+               (name h2) (fun fmt -> (Array.iter (fun c ->
+                   if Atom.equal c (Atom.neg a) then
+                     Format.fprintf fmt "@ (fun np => np p)"
+                   else
+                     Format.fprintf fmt "@ %s" (M.find c m)))
+                 ) (Clause.atoms h2)
+           end else
+             Format.fprintf fmt "@ %s" (M.find b m)
+         )) (Clause.atoms h1)
+
+  let resolution fmt goal hyp1 hyp2 atom =
+    let a = Atom.abs atom in
+    let h1, h2 =
+      if Array.exists (Atom.equal a) (Clause.atoms hyp1) then hyp1, hyp2
+      else (
+        assert (Array.exists (Atom.equal a) (Clause.atoms hyp2));
+        hyp2, hyp1
+      )
+    in
+    (** Print some debug info *)
+    Format.fprintf fmt
+      "(* Clausal resolution. Goal : %s ; Hyps : %s, %s *)@\n"
+      (name goal) (name h1) (name h2);
+    (** Prove the goal: intro the axioms, then perform resolution *)
+    if Array.length (Clause.atoms goal) = 0 then (
+      let m = M.empty in
+      Format.fprintf fmt "exact @[<hov 1>(%a)@].@\n" (resolution_aux m a h1 h2) ();
+      false
+    ) else (
+      let m = clause_map goal in
+      Format.fprintf fmt "pose proof @[<hov>(fun %a=>@ %a)@ as %s.@]@\n"
+        (clause_iter m "%s@ ") goal (resolution_aux m a h1 h2) () (name goal);
+      true
+    )
+
+  (* Count uses of hypotheses *)
+  let incr_use h c =
+    let i = try C_tbl.find h c with Not_found -> 0 in
+    C_tbl.add h c (i + 1)
+
+  let decr_use h c =
+    let i = C_tbl.find h c - 1 in
+    assert (i >= 0);
+    let () = C_tbl.add h c i in
+    i <= 0
+
+  let clear fmt c =
+    Format.fprintf fmt "clear %s." (name c)
+
+  let rec clean_aux fmt = function
+    | [] -> ()
+    | [x] ->
+      Format.fprintf fmt "%a@\n" clear x
+    | x :: ((_ :: _) as r) ->
+      Format.fprintf fmt "%a@ %a" clear x clean_aux r
+
+  let clean h fmt l =
+    match List.filter (decr_use h) l with
+    | [] -> ()
+    | l' ->
+      Format.fprintf fmt "(* Clearing unused clauses *)@\n%a" clean_aux l'
+
+  let prove_node t fmt node =
+    let clause = node.P.conclusion in
+    match node.P.step with
+    | P.Hypothesis _ ->
+      A.prove_hyp fmt (name clause) clause
+    | P.Assumption ->
+      A.prove_assumption fmt (name clause) clause
+    | P.Lemma _ ->
+      A.prove_lemma fmt (name clause) clause
+    | P.Duplicate (p, l) ->
+      let c = P.conclusion p in
+      let () = elim_duplicate fmt clause c l in
+      clean t fmt [c]
+    | P.Hyper_res hr ->
+      let (p1, p2, a) = P.res_of_hyper_res hr in
+      let c1 = P.conclusion p1 in
+      let c2 = P.conclusion p2 in
+      if resolution fmt clause c1 c2 a then clean t fmt [c1; c2]
+
+  let count_uses p =
+    let h = C_tbl.create 128 in
+    let aux () node =
+      List.iter (fun p' -> incr_use h P.(conclusion p')) (P.parents node.P.step)
+    in
+    let () = P.fold aux () p in
+    h
+
+  (* Here the main idea is to always try and have exactly
+     one goal to prove, i.e False. So each  *)
+  let pp fmt p =
+    let h = count_uses p in
+    let aux () node =
+      Format.fprintf fmt "%a" (prove_node h) node
+    in
+    Format.fprintf fmt "(* Coq proof generated by mSAT*)@\n";
+    P.fold aux () p
+end
+
+
+module Simple(S : Msat.S)
+    (A : Arg with type hyp = S.formula list
+              and type lemma := S.lemma
+              and type assumption := S.formula) =
+  Make(S)(struct
+    module P = S.Proof
+
+    (* Some helpers *)
+    let lit = S.Atom.formula
+
+    let get_assumption c =
+      match S.Clause.atoms_l c with
+      | [ x ] -> x
+      | _ -> assert false
+
+    let get_lemma c =
+      match P.expand (P.prove c) with
+      | {P.step=P.Lemma p; _} -> p
+      | _ -> assert false
+
+    let prove_hyp fmt name c =
+      A.prove_hyp fmt name (List.map lit (S.Clause.atoms_l c))
+
+    let prove_lemma fmt name c =
+      A.prove_lemma fmt name (get_lemma c)
+
+    let prove_assumption fmt name c =
+      A.prove_assumption fmt name (lit (get_assumption c))
+
+  end)
+
diff --git a/src/sat/src/backend/Coq.mli b/src/sat/src/backend/Coq.mli
new file mode 100644
index 00000000..3d34f549
--- /dev/null
+++ b/src/sat/src/backend/Coq.mli
@@ -0,0 +1,46 @@
+(*
+MSAT is free software, using the Apache license, see file LICENSE
+Copyright 2015 Guillaume Bury
+*)
+
+(** Coq Backend
+
+    This module provides an easy way to produce coq scripts
+    corresponding to the resolution proofs output by the
+    sat solver. *)
+
+module type S = Backend_intf.S
+(** Interface for exporting proofs. *)
+
+module type Arg = sig
+  (** Term printing for Coq *)
+
+  type hyp
+  type lemma
+  type assumption
+  (** The types of hypotheses, lemmas, and assumptions *)
+
+  val prove_hyp : Format.formatter -> string -> hyp -> unit
+  val prove_lemma : Format.formatter -> string -> lemma -> unit
+  val prove_assumption : Format.formatter -> string -> assumption -> unit
+  (** Proving function for hypotheses, lemmas and assumptions.
+      [prove_x fmt name x] should prove [x], and be such that after
+      executing it, [x] is among the coq hypotheses under the name [name].
+      The hypothesis should be the encoding of the given clause, i.e
+      for a clause [a \/ not b \/ c], the proved hypothesis should be:
+      [ ~ a -> ~ ~ b -> ~ c -> False ], keeping the same order as the
+      one in the atoms array of the clause. *)
+
+end
+
+module Make(S : Msat.S)(A : Arg with type hyp := S.clause
+                                and type lemma := S.clause
+                                and type assumption := S.clause) : S with type t := S.proof
+(** Base functor to output Coq proofs *)
+
+
+module Simple(S : Msat.S)(A : Arg with type hyp = S.formula list
+                                  and type lemma := S.lemma
+                                  and type assumption := S.formula) : S with type t := S.proof
+(** Simple functor to output Coq proofs *)
+
diff --git a/src/sat/src/backend/Dedukti.ml b/src/sat/src/backend/Dedukti.ml
new file mode 100644
index 00000000..7f8526eb
--- /dev/null
+++ b/src/sat/src/backend/Dedukti.ml
@@ -0,0 +1,62 @@
+(*
+MSAT is free software, using the Apache license, see file LICENSE
+Copyright 2015 Guillaume Bury
+*)
+
+module type S = Backend_intf.S
+
+module type Arg = sig
+
+  type proof
+  type lemma
+  type formula
+
+  val pp : Format.formatter -> formula -> unit
+  val prove : Format.formatter -> lemma -> unit
+  val context : Format.formatter -> proof -> unit
+end
+
+module Make(S : Msat.S)(A : Arg with type formula := S.formula
+                                and type lemma := S.lemma
+                                and type proof := S.proof) = struct
+  module P = S.Proof
+
+  let pp_nl fmt = Format.fprintf fmt "@\n"
+  let fprintf fmt format = Format.kfprintf pp_nl fmt format
+
+  let _clause_name = S.Clause.name
+
+  let _pp_clause fmt c =
+    let rec aux fmt = function
+      | [] -> ()
+      | a :: r ->
+        let f, pos =
+          if S.Atom.sign a then
+            S.Atom.formula a, true
+          else
+            S.Atom.formula (S.Atom.neg a), false
+        in
+        fprintf fmt "%s _b %a ->@ %a"
+          (if pos then "_pos" else "_neg") A.pp f aux r
+    in
+    fprintf fmt "_b : Prop ->@ %a ->@ _proof _b" aux (S.Clause.atoms_l c)
+
+  let context fmt p =
+    fprintf fmt "(; Embedding ;)";
+    fprintf fmt "Prop : Type.";
+    fprintf fmt "_proof : Prop -> Type.";
+    fprintf fmt "(; Notations for clauses ;)";
+    fprintf fmt "_pos : Prop -> Prop -> Type.";
+    fprintf fmt "_neg : Prop -> Prop -> Type.";
+    fprintf fmt "[b: Prop, p: Prop] _pos b p --> _proof p -> _proof b.";
+    fprintf fmt "[b: Prop, p: Prop] _neg b p --> _pos b p -> _proof b.";
+    A.context fmt p
+
+  let pp fmt p =
+    fprintf fmt "#NAME Proof.";
+    fprintf fmt "(; Dedukti file automatically generated by mSAT ;)";
+    context fmt p;
+    ()
+
+end
+
diff --git a/src/sat/src/backend/Dedukti.mli b/src/sat/src/backend/Dedukti.mli
new file mode 100644
index 00000000..ef7cc88e
--- /dev/null
+++ b/src/sat/src/backend/Dedukti.mli
@@ -0,0 +1,32 @@
+(*
+MSAT is free software, using the Apache license, see file LICENSE
+Copyright 2014 Guillaume Bury
+Copyright 2014 Simon Cruanes
+*)
+
+(** Deduki backend for proofs
+
+    Work in progress...
+*)
+
+module type S = Backend_intf.S
+
+module type Arg = sig
+
+  type lemma
+  type proof
+  type formula
+
+  val pp : Format.formatter -> formula -> unit
+  val prove : Format.formatter -> lemma -> unit
+  val context : Format.formatter -> proof -> unit
+end
+
+module Make :
+  functor(S : Msat.S) ->
+  functor(A : Arg
+          with type formula := S.formula
+           and type lemma := S.lemma
+           and type proof := S.proof) ->
+    S with type t := S.proof
+(** Functor to generate a backend to output proofs for the dedukti type checker. *)
diff --git a/src/sat/src/backend/Dot.ml b/src/sat/src/backend/Dot.ml
new file mode 100644
index 00000000..9097cc45
--- /dev/null
+++ b/src/sat/src/backend/Dot.ml
@@ -0,0 +1,191 @@
+(*
+MSAT is free software, using the Apache license, see file LICENSE
+Copyright 2014 Guillaume Bury
+Copyright 2014 Simon Cruanes
+*)
+
+(** Output interface for the backend *)
+module type S = Backend_intf.S
+
+(** Input module for the backend *)
+module type Arg = sig
+
+  type atom
+  (* Type of atoms *)
+
+  type hyp
+  type lemma
+  type assumption
+  (** Types for hypotheses, lemmas, and assumptions. *)
+
+  val print_atom : Format.formatter -> atom -> unit
+  (** Printing function for atoms *)
+
+  val hyp_info : hyp -> string * string option * (Format.formatter -> unit -> unit) list
+  val lemma_info : lemma -> string * string option * (Format.formatter -> unit -> unit) list
+  val assumption_info : assumption -> string * string option * (Format.formatter -> unit -> unit) list
+  (** Functions to return information about hypotheses and lemmas *)
+
+end
+
+module Default(S : Msat.S) = struct
+  module Atom = S.Atom
+  module Clause = S.Clause
+
+  let print_atom = Atom.pp
+
+  let hyp_info c =
+    "hypothesis", Some "LIGHTBLUE",
+    [ fun fmt () -> Format.fprintf fmt "%s" @@ Clause.name c]
+
+  let lemma_info c =
+    "lemma", Some "BLUE",
+    [ fun fmt () -> Format.fprintf fmt "%s" @@ Clause.name c]
+
+  let assumption_info c =
+    "assumption", Some "PURPLE",
+    [ fun fmt () -> Format.fprintf fmt "%s" @@ Clause.name c]
+
+end
+
+(** Functor to provide dot printing *)
+module Make(S : Msat.S)(A : Arg with type atom := S.atom
+                                and type hyp := S.clause
+                                and type lemma := S.clause
+                                and type assumption := S.clause) = struct
+  module Atom = S.Atom
+  module Clause = S.Clause
+  module P = S.Proof
+
+  let node_id n = Clause.name n.P.conclusion
+  let proof_id p = node_id (P.expand p)
+  let res_nn_id n1 n2 = node_id n1 ^ "_" ^ node_id n2 ^ "_res"
+  let res_np_id n1 n2 = node_id n1 ^ "_" ^ proof_id n2 ^ "_res"
+
+  let print_clause fmt c =
+    let v = Clause.atoms c in
+    if Array.length v = 0 then
+      Format.fprintf fmt "⊥"
+    else
+      let n = Array.length v in
+      for i = 0 to n - 1 do
+        Format.fprintf fmt "%a" A.print_atom v.(i);
+        if i < n - 1 then
+          Format.fprintf fmt ", "
+      done
+
+  let print_edge fmt i j =
+    Format.fprintf fmt "%s -> %s;@\n" j i
+
+  let print_edges fmt n =
+    match P.(n.step) with
+    | P.Hyper_res {P.hr_steps=[];_} -> assert false (* NOTE: should never happen *)
+    | P.Hyper_res {P.hr_init; hr_steps=((_,p0)::_) as l} ->
+      print_edge fmt (res_np_id n p0) (proof_id hr_init);
+      List.iter
+        (fun (_,p2) -> print_edge fmt (res_np_id n p2) (proof_id p2))
+        l;
+    | _ -> ()
+
+  let table_options fmt color =
+    Format.fprintf fmt "BORDER=\"0\" CELLBORDER=\"1\" CELLSPACING=\"0\" BGCOLOR=\"%s\"" color
+
+  let table fmt (c, rule, color, l) =
+    Format.fprintf fmt "<TR><TD colspan=\"2\">%a</TD></TR>" print_clause c;
+    match l with
+    | [] ->
+      Format.fprintf fmt "<TR><TD BGCOLOR=\"%s\" colspan=\"2\">%s</TD></TR>" color rule
+    | f :: r ->
+      Format.fprintf fmt "<TR><TD BGCOLOR=\"%s\" rowspan=\"%d\">%s</TD><TD>%a</TD></TR>"
+        color (List.length l) rule f ();
+      List.iter (fun f -> Format.fprintf fmt "<TR><TD>%a</TD></TR>" f ()) r
+
+  let print_dot_node fmt id color c rule rule_color l =
+    Format.fprintf fmt "%s [shape=plaintext, label=<<TABLE %a>%a</TABLE>>];@\n"
+      id table_options color table (c, rule, rule_color, l)
+
+  let print_dot_res_node fmt id a =
+    Format.fprintf fmt "%s [label=<%a>];@\n" id A.print_atom a
+
+  let ttify f c = fun fmt () -> f fmt c
+
+  let print_contents fmt n =
+    match P.(n.step) with
+    (* Leafs of the proof tree *)
+    | P.Hypothesis _ ->
+      let rule, color, l = A.hyp_info P.(n.conclusion) in
+      let color = match color with None -> "LIGHTBLUE" | Some c -> c in
+      print_dot_node fmt (node_id n) "LIGHTBLUE" P.(n.conclusion) rule color l
+    | P.Assumption ->
+      let rule, color, l = A.assumption_info P.(n.conclusion) in
+      let color = match color with None -> "LIGHTBLUE" | Some c -> c in
+      print_dot_node fmt (node_id n) "LIGHTBLUE" P.(n.conclusion) rule color l
+    | P.Lemma _ ->
+      let rule, color, l = A.lemma_info P.(n.conclusion) in
+      let color = match color with None -> "YELLOW" | Some c -> c in
+      print_dot_node fmt (node_id n) "LIGHTBLUE" P.(n.conclusion) rule color l
+
+    (* Tree nodes *)
+    | P.Duplicate (p, l) ->
+      print_dot_node fmt (node_id n) "GREY" P.(n.conclusion) "Duplicate" "GREY"
+        ((fun fmt () -> (Format.fprintf fmt "%s" (node_id n))) ::
+         List.map (ttify A.print_atom) l);
+      print_edge fmt (node_id n) (node_id (P.expand p))
+    | P.Hyper_res {P.hr_steps=l; _} ->
+      print_dot_node fmt (node_id n) "GREY" P.(n.conclusion) "Resolution" "GREY"
+        [(fun fmt () -> (Format.fprintf fmt "%s" (node_id n)))];
+      List.iter
+        (fun (a,p2) ->
+          print_dot_res_node fmt (res_np_id n p2) a;
+          print_edge fmt (node_id n) (res_np_id n p2))
+        l
+
+  let print_node fmt n =
+    print_contents fmt n;
+    print_edges fmt n
+
+  let pp fmt p =
+    Format.fprintf fmt "digraph proof {@\n";
+    P.fold (fun () -> print_node fmt) () p;
+    Format.fprintf fmt "}@."
+
+end
+
+module Simple(S : Msat.S)
+    (A : Arg with type atom := S.formula
+              and type hyp = S.formula list
+              and type lemma := S.lemma
+              and type assumption = S.formula) =
+  Make(S)(struct
+    module Atom = S.Atom
+    module Clause = S.Clause
+    module P = S.Proof
+
+    (* Some helpers *)
+    let lit = Atom.formula
+
+    let get_assumption c =
+      match S.Clause.atoms_l c with
+      | [ x ] -> x
+      | _ -> assert false
+
+    let get_lemma c =
+      match P.expand (P.prove c) with
+      | {P.step=P.Lemma p;_} -> p
+      | _ -> assert false
+
+    (* Actual functions *)
+    let print_atom fmt a =
+      A.print_atom fmt (lit a)
+
+    let hyp_info c =
+      A.hyp_info (List.map lit (S.Clause.atoms_l c))
+
+    let lemma_info c =
+      A.lemma_info (get_lemma c)
+
+    let assumption_info c =
+      A.assumption_info (lit (get_assumption c))
+
+  end)
+
diff --git a/src/sat/src/backend/Dot.mli b/src/sat/src/backend/Dot.mli
new file mode 100644
index 00000000..70adffa1
--- /dev/null
+++ b/src/sat/src/backend/Dot.mli
@@ -0,0 +1,70 @@
+(*
+MSAT is free software, using the Apache license, see file LICENSE
+Copyright 2014 Guillaume Bury
+Copyright 2014 Simon Cruanes
+*)
+
+(** Dot backend for proofs
+
+    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.
+*)
+
+module type S = Backend_intf.S
+(** Interface for exporting proofs. *)
+
+module type Arg = sig
+  (** Term printing for DOT
+
+      This module defines what functions are required in order to export
+      a proof to the DOT format.
+  *)
+
+  type atom
+  (** The type of atomic formuals *)
+
+  type hyp
+  type lemma
+  type assumption
+  (** The type of theory-specifi proofs (also called lemmas). *)
+
+  val print_atom : Format.formatter -> atom -> unit
+  (** Print the contents of the given atomic formulas.
+      WARNING: this function should take care to escape and/or not output special
+      reserved characters for the dot format (such as quotes and so on). *)
+
+  val hyp_info : hyp -> string * string option * (Format.formatter -> unit -> unit) list
+  val lemma_info : lemma -> string * string option * (Format.formatter -> unit -> unit) list
+  val assumption_info : assumption -> string * string option * (Format.formatter -> unit -> unit) list
+  (** Generate some information about the leafs of the proof tree. Currently this backend
+      print each lemma/assumption/hypothesis as a single leaf of the proof tree.
+      These function should return a triplet [(rule, color, l)], such that:
+      - [rule] is a name for the proof (arbitrary, does not need to be unique, but
+        should rather be descriptive)
+      - [color] is a color name (optional) understood by DOT
+      - [l] is a list of printers that will be called to print some additional information
+  *)
+
+end
+
+module Default(S : Msat.S) : Arg with type atom := S.atom
+                                 and type hyp := S.clause
+                                 and type lemma := S.clause
+                                 and type assumption := S.clause
+(** Provides a reasonnable default to instantiate the [Make] functor, assuming
+    the original printing functions are compatible with DOT html labels. *)
+
+module Make(S : Msat.S)(A : Arg with type atom := S.atom
+                                and type hyp := S.clause
+                                and type lemma := S.clause
+                                and type assumption := S.clause) : S with type t := S.proof
+(** Functor for making a module to export proofs to the DOT format. *)
+
+module Simple(S : Msat.S)(A : Arg with type atom := S.formula
+                                  and type hyp = S.formula list
+                                  and type lemma := S.lemma
+                                  and type assumption = S.formula) : S with type t := S.proof
+(** Functor for making a module to export proofs to the DOT format.
+    The substitution of the hyp type is non-destructive due to a restriction
+    of destructive substitutions on earlier versions of ocaml. *)
+
diff --git a/src/sat/src/backend/dune b/src/sat/src/backend/dune
new file mode 100644
index 00000000..7febb3bc
--- /dev/null
+++ b/src/sat/src/backend/dune
@@ -0,0 +1,10 @@
+(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 -warn-error -27 -color always -safe-string)
+  (ocamlopt_flags :standard -O3 -bin-annot
+                  -unbox-closures -unbox-closures-factor 20)
+  )
+
diff --git a/src/sat/src/backtrack/Backtrackable_ref.ml b/src/sat/src/backtrack/Backtrackable_ref.ml
new file mode 100644
index 00000000..bc91cfd5
--- /dev/null
+++ b/src/sat/src/backtrack/Backtrackable_ref.ml
@@ -0,0 +1,29 @@
+
+type 'a t = {
+  mutable cur: 'a;
+  stack: 'a Vec.t;
+  copy: ('a -> 'a) option;
+}
+
+let create ?copy x: _ t =
+  {cur=x; stack=Vec.create(); copy}
+
+let[@inline] get self = self.cur
+let[@inline] set self x = self.cur <- x
+let[@inline] update self f = self.cur <- f self.cur
+
+let[@inline] n_levels self = Vec.size self.stack
+
+let[@inline] push_level self : unit =
+  let x = self.cur in
+  let x = match self.copy with None -> x | Some f -> f x in
+  Vec.push self.stack x
+
+let pop_levels self n : unit =
+  assert (n>=0);
+  if n > Vec.size self.stack then invalid_arg "Backtrackable_ref.pop_levels";
+  let i = Vec.size self.stack-n in
+  let x = Vec.get self.stack i in
+  self.cur <- x;
+  Vec.shrink self.stack i;
+  ()
diff --git a/src/sat/src/backtrack/Backtrackable_ref.mli b/src/sat/src/backtrack/Backtrackable_ref.mli
new file mode 100644
index 00000000..a1755115
--- /dev/null
+++ b/src/sat/src/backtrack/Backtrackable_ref.mli
@@ -0,0 +1,30 @@
+
+(** {1 Backtrackable ref} *)
+
+type 'a t
+
+val create : ?copy:('a -> 'a) -> 'a -> 'a t
+(** Create a backtrackable reference holding the given value initially.
+    @param copy if provided, will be used to copy the value when [push_level]
+    is called. *)
+
+val set : 'a t -> 'a -> unit
+(** Set the reference's current content *)
+
+val get : 'a t -> 'a
+(** Get the reference's current content *)
+
+val update : 'a t -> ('a -> 'a) -> unit
+(** Update the reference's current content *)
+  
+val push_level : _ t -> unit
+(** Push a backtracking level, copying the current value on top of some
+    stack. The [copy] function will be used if it was provided in {!create}. *)
+
+val n_levels : _ t -> int
+(** Number of saved values *)
+
+val pop_levels : _ t -> int -> unit
+(** Pop [n] levels, restoring to the value the reference was storing [n] calls
+    to [push_level] earlier.
+    @raise Invalid_argument if [n] is bigger than [n_levels]. *)
diff --git a/src/sat/src/backtrack/Msat_backtrack.ml b/src/sat/src/backtrack/Msat_backtrack.ml
new file mode 100644
index 00000000..14857855
--- /dev/null
+++ b/src/sat/src/backtrack/Msat_backtrack.ml
@@ -0,0 +1,2 @@
+
+module Ref = Backtrackable_ref
diff --git a/src/sat/src/backtrack/dune b/src/sat/src/backtrack/dune
new file mode 100644
index 00000000..48740ab9
--- /dev/null
+++ b/src/sat/src/backtrack/dune
@@ -0,0 +1,11 @@
+
+(library
+  (name msat_backtrack)
+  (public_name msat.backtrack)
+  (libraries msat)
+  (synopsis "backtrackable data structures for msat")
+  (flags :standard -warn-error -3 -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/src/core/Heap.ml b/src/sat/src/core/Heap.ml
new file mode 100644
index 00000000..ed9884bb
--- /dev/null
+++ b/src/sat/src/core/Heap.ml
@@ -0,0 +1,145 @@
+
+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;
+  } [@@unboxed]
+
+  let _absent_index = -1
+
+  let create () =
+    { heap = Vec.create(); }
+
+  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 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) =
+    match Vec.size heap with
+    | 0 -> raise Not_found
+    | 1 ->
+      let x = Vec.pop heap in
+      Elt.set_idx x _absent_index;
+      x
+    | _ ->
+      let x = Vec.get heap 0 in
+      let new_hd = Vec.pop heap in (* heap.last() *)
+      Vec.set heap 0 new_hd;
+      Elt.set_idx x _absent_index;
+      Elt.set_idx new_hd 0;
+      (* enforce heap property again *)
+      if Vec.size heap > 1 then (
+        percolate_down s new_hd;
+      );
+      x
+
+end [@@inline]
diff --git a/src/sat/src/core/Heap.mli b/src/sat/src/core/Heap.mli
new file mode 100644
index 00000000..a621885c
--- /dev/null
+++ b/src/sat/src/core/Heap.mli
@@ -0,0 +1,5 @@
+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/sat/src/core/Heap_intf.ml b/src/sat/src/core/Heap_intf.ml
new file mode 100644
index 00000000..bee623e6
--- /dev/null
+++ b/src/sat/src/core/Heap_intf.ml
@@ -0,0 +1,46 @@
+
+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 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 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/sat/src/core/Internal.ml b/src/sat/src/core/Internal.ml
new file mode 100644
index 00000000..7e704403
--- /dev/null
+++ b/src/sat/src/core/Internal.ml
@@ -0,0 +1,2275 @@
+(*
+MSAT is free software, using the Apache license, see file LICENSE
+Copyright 2014 Guillaume Bury
+Copyright 2014 Simon Cruanes
+*)
+
+module type PLUGIN = sig
+  val mcsat : bool
+  (** Is this a mcsat plugin? *)
+
+  val has_theory : bool
+  (** Is this a CDCL(T) plugin or mcsat plugin?
+      i.e does it have theories *)
+
+  include Solver_intf.PLUGIN_MCSAT
+end
+
+let invalid_argf fmt =
+  Format.kasprintf (fun msg -> invalid_arg ("msat: " ^ msg)) fmt
+
+module Make(Plugin : PLUGIN)
+= struct
+  module Term = Plugin.Term
+  module Formula = Plugin.Formula
+  module Value = Plugin.Value
+
+  type term = Term.t
+  type formula = Formula.t
+  type theory = Plugin.t
+  type lemma = Plugin.proof
+  type value = Value.t
+
+  (* MCSAT literal *)
+  type lit = {
+    lid : int;
+    term : term;
+    mutable l_level : int;
+    mutable l_idx: int;
+    mutable l_weight : float;
+    mutable assigned : value option;
+  }
+
+  type var = {
+    vid : int;
+    pa : atom;
+    na : atom;
+    mutable v_fields : int;
+    mutable v_level : int;
+    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;
+  }
+
+  and atom = {
+    aid : int;
+    var : var;
+    neg : atom;
+    lit : formula;
+    mutable is_true : bool;
+    watched : clause Vec.t;
+  }
+
+  and clause = {
+    cid: int;
+    atoms : atom array;
+    mutable cpremise : premise;
+    mutable activity : float;
+    mutable flags: int; (* bitfield *)
+  }
+
+  and reason =
+    | Decision
+    | Bcp of clause
+    | Bcp_lazy of clause lazy_t
+    | Semantic
+
+  (* TODO: remove, replace with user-provided proof trackng device?
+     for pure SAT, [reason] is sufficient *)
+  and premise =
+    | Hyp of lemma
+    | Local
+    | Lemma of lemma
+    | History of clause list
+    | Empty_premise
+
+  type elt =
+    | E_lit of lit
+    | E_var of var
+
+  type trail_elt =
+    | Lit of lit
+    | Atom of atom
+
+  (* Constructors *)
+  module MF = Hashtbl.Make(Formula)
+  module MT = Hashtbl.Make(Term)
+
+  type st = {
+    t_map: lit MT.t;
+    f_map: var MF.t;
+    vars: elt Vec.t;
+    mutable cpt_mk_var: int;
+    mutable cpt_mk_clause: int;
+  }
+
+  let create_st ?(size=`Big) () : st =
+    let size_map = match size with
+      | `Tiny -> 8
+      | `Small -> 16
+      | `Big -> 4096
+    in
+    { f_map = MF.create size_map;
+      t_map = MT.create size_map;
+      vars = Vec.create();
+      cpt_mk_var = 0;
+      cpt_mk_clause = 0;
+    }
+
+  let nb_elt st = Vec.size st.vars
+  let get_elt st i = Vec.get st.vars i
+  let iter_elt st f = Vec.iter f st.vars
+
+  let name_of_clause c = match c.cpremise with
+    | Hyp _ -> "H" ^ string_of_int c.cid
+    | Lemma _ -> "T" ^ string_of_int c.cid
+    | Local -> "L" ^ string_of_int c.cid
+    | History _ -> "C" ^ string_of_int c.cid
+    | Empty_premise -> string_of_int c.cid
+
+  module Lit = struct
+    type t = lit
+    let[@inline] term l = l.term
+    let[@inline] level l = l.l_level
+    let[@inline] assigned l = l.assigned
+    let[@inline] weight l = l.l_weight
+
+    let make (st:st) (t:term) : t =
+      try MT.find st.t_map t
+      with Not_found ->
+        let res = {
+          lid = st.cpt_mk_var;
+          term = t;
+          l_weight = 1.;
+          l_idx= -1;
+          l_level = -1;
+          assigned = None;
+        } in
+        st.cpt_mk_var <- st.cpt_mk_var + 1;
+        MT.add st.t_map t res;
+        Vec.push st.vars (E_lit res);
+        res
+
+    let debug_assign fmt v =
+      match v.assigned with
+      | None ->
+        Format.fprintf fmt ""
+      | Some t ->
+        Format.fprintf fmt "@[<hov>@@%d->@ %a@]" v.l_level Value.pp t
+
+    let pp out v = Term.pp out v.term
+    let debug out v =
+      Format.fprintf out "%d[%a][lit:@[<hov>%a@]]"
+        (v.lid+1) debug_assign v Term.pp v.term
+  end
+
+  (* some boolean flags for variables, used as masks *)
+  let seen_var = 0b1
+  let seen_pos = 0b10
+  let seen_neg = 0b100
+  let default_pol_true = 0b1000
+
+  module Var = struct
+    type t = var
+    let[@inline] level v = v.v_level
+    let[@inline] pos v = v.pa
+    let[@inline] neg v = v.na
+    let[@inline] reason v = v.reason
+    let[@inline] assignable v = v.v_assignable
+    let[@inline] weight v = v.v_weight
+    let[@inline] mark v = v.v_fields <- v.v_fields lor seen_var
+    let[@inline] unmark v = v.v_fields <- v.v_fields land (lnot seen_var)
+    let[@inline] marked v = (v.v_fields land seen_var) <> 0
+    let[@inline] set_default_pol_true v = v.v_fields <- v.v_fields lor default_pol_true
+    let[@inline] set_default_pol_false v = v.v_fields <- v.v_fields land (lnot default_pol_true)
+    let[@inline] default_pol v = (v.v_fields land default_pol_true) <> 0
+
+    let make ?(default_pol=true) (st:st) (t:formula) : var * Solver_intf.negated =
+      let lit, negated = Formula.norm t in
+      try
+        MF.find st.f_map lit, negated
+      with Not_found ->
+        let cpt_double = st.cpt_mk_var lsl 1 in
+        let rec var  =
+          { vid = st.cpt_mk_var;
+            pa = pa;
+            na = na;
+            v_fields = 0;
+            v_level = -1;
+            v_idx= -1;
+            v_weight = 0.;
+            v_assignable = None;
+            reason = None;
+          }
+        and pa =
+          { var = var;
+            lit = lit;
+            watched = Vec.create();
+            neg = na;
+            is_true = false;
+            aid = cpt_double (* aid = vid*2 *) }
+        and na =
+          { var = var;
+            lit = Formula.neg lit;
+            watched = Vec.create();
+            neg = pa;
+            is_true = false;
+            aid = cpt_double + 1 (* aid = vid*2+1 *) } in
+        MF.add st.f_map lit var;
+        st.cpt_mk_var <- st.cpt_mk_var + 1;
+        if default_pol then set_default_pol_true var;
+        Vec.push st.vars (E_var var);
+        var, negated
+
+    (* Marking helpers *)
+    let[@inline] clear v =
+      v.v_fields <- 0
+
+    let[@inline] seen_both v =
+      (seen_pos land v.v_fields <> 0) &&
+      (seen_neg land v.v_fields <> 0)
+  end
+
+  module Atom = struct
+    type t = atom
+    let[@inline] level a = a.var.v_level
+    let[@inline] var a = a.var
+    let[@inline] neg a = a.neg
+    let[@inline] abs a = a.var.pa
+    let[@inline] formula a = a.lit
+    let[@inline] equal a b = a == b
+    let[@inline] sign a = a == abs a
+    let[@inline] hash a = Hashtbl.hash a.aid
+    let[@inline] compare a b = compare a.aid b.aid
+    let[@inline] reason a = Var.reason a.var
+    let[@inline] id a = a.aid
+    let[@inline] is_true a = a.is_true
+    let[@inline] is_false a = a.neg.is_true
+    let has_value a = is_true a || is_false a
+
+    let[@inline] seen a =
+      if sign a
+      then (seen_pos land a.var.v_fields <> 0)
+      else (seen_neg land a.var.v_fields <> 0)
+
+    let[@inline] mark a =
+      let pos = equal a (abs a) in
+      if pos then (
+        a.var.v_fields <- seen_pos lor a.var.v_fields
+      ) else (
+        a.var.v_fields <- seen_neg lor a.var.v_fields
+      )
+
+    let[@inline] make ?default_pol st lit =
+      let var, negated = Var.make ?default_pol st lit in
+      match negated with
+      | Solver_intf.Negated -> var.na
+      | Solver_intf.Same_sign -> var.pa
+
+    let pp fmt a = Formula.pp fmt a.lit
+
+    let pp_a fmt v =
+      if Array.length v = 0 then (
+        Format.fprintf fmt "∅"
+      ) else (
+        pp fmt v.(0);
+        if (Array.length v) > 1 then begin
+          for i = 1 to (Array.length v) - 1 do
+            Format.fprintf fmt " ∨ %a" pp v.(i)
+          done
+        end
+      )
+
+    (* Complete debug printing *)
+    let pp_sign a = if a == a.var.pa then "+" else "-"
+
+    let debug_reason fmt = function
+      | n, _ when n < 0 ->
+        Format.fprintf fmt "%%"
+      | n, None ->
+        Format.fprintf fmt "%d" n
+      | n, Some Decision ->
+        Format.fprintf fmt "@@%d" n
+      | n, Some Bcp c ->
+        Format.fprintf fmt "->%d/%s" n (name_of_clause c)
+      | n, Some (Bcp_lazy _) ->
+        Format.fprintf fmt "->%d/<lazy>" n
+      | n, Some Semantic ->
+        Format.fprintf fmt "::%d" n
+
+    let pp_level fmt a =
+      debug_reason fmt (a.var.v_level, a.var.reason)
+
+    let debug_value fmt a =
+      if a.is_true then
+        Format.fprintf fmt "T%a" pp_level a
+      else if a.neg.is_true then
+        Format.fprintf fmt "F%a" pp_level a
+      else
+        Format.fprintf fmt ""
+
+    let debug out a =
+      Format.fprintf out "%s%d[%a][atom:@[<hov>%a@]]"
+        (pp_sign a) (a.var.vid+1) debug_value a Formula.pp a.lit
+
+    let debug_a out vec =
+      Array.iter (fun a -> Format.fprintf out "%a@ " debug a) vec
+    let debug_l out l =
+      List.iter (fun a -> Format.fprintf out "%a@ " debug a) l
+
+    module Set = Set.Make(struct type t=atom let compare=compare end)
+  end
+
+  (* Elements *)
+  module Elt = struct
+    type t = elt
+    let[@inline] of_lit l = E_lit l
+    let[@inline] of_var v = E_var v
+
+    let[@inline] id = function
+      | E_lit l -> l.lid | E_var v ->  v.vid
+    let[@inline] level = function
+      | E_lit l -> l.l_level | E_var v ->  v.v_level
+    let[@inline] idx = function
+      | E_lit l -> l.l_idx | E_var v ->  v.v_idx
+    let[@inline] weight = function
+      | E_lit l -> l.l_weight | E_var v ->  v.v_weight
+
+    let[@inline] set_level e lvl = match e with
+      | E_lit l -> l.l_level <- lvl | E_var v ->  v.v_level <- lvl
+    let[@inline] set_idx e i = match e with
+      | E_lit l -> l.l_idx <- i | E_var v ->  v.v_idx <- i
+    let[@inline] set_weight e w = match e with
+      | E_lit l -> l.l_weight <- w | E_var v ->  v.v_weight <- w
+  end
+
+  module Trail_elt = struct
+    type t = trail_elt
+    let[@inline] of_lit l = Lit l
+    let[@inline] of_atom a = Atom a
+
+    let debug fmt = function
+      | Lit l -> Lit.debug fmt l
+      | Atom a -> Atom.debug fmt a
+  end
+
+  module Clause = struct
+    type t = clause
+
+    let make_a =
+      let n = ref 0 in
+      fun ~flags atoms premise ->
+        let cid = !n in
+        incr n;
+        { cid;
+          atoms = atoms;
+          flags;
+          activity = 0.;
+          cpremise = premise}
+
+    let make ~flags l premise = make_a ~flags (Array.of_list l) premise
+
+    let empty = make [] (History [])
+    let name = name_of_clause
+    let[@inline] equal c1 c2 = c1.cid = c2.cid
+    let[@inline] hash c = Hashtbl.hash c.cid
+    let[@inline] atoms c = c.atoms
+    let[@inline] atoms_seq c = Iter.of_array c.atoms
+    let[@inline] atoms_l c = Array.to_list c.atoms
+
+    let flag_attached = 0b1
+    let flag_visited = 0b10
+    let flag_removable = 0b100
+    let flag_dead = 0b1000
+
+    let[@inline] make_removable l premise = make ~flags:flag_removable l premise
+    let[@inline] make_removable_a l premise = make_a ~flags:flag_removable l premise
+    let[@inline] make_permanent l premise = make ~flags:0 l premise
+
+    let[@inline] visited c = (c.flags land flag_visited) <> 0
+    let[@inline] set_visited c b =
+      if b then c.flags <- c.flags lor flag_visited
+      else c.flags <- c.flags land lnot flag_visited
+
+    let[@inline] attached c = (c.flags land flag_attached) <> 0
+    let[@inline] set_attached c b =
+      if b then c.flags <- c.flags lor flag_attached
+      else c.flags <- c.flags land lnot flag_attached
+
+    let[@inline] removable c = (c.flags land flag_removable) <> 0
+    let[@inline] set_removable c b =
+      if b then c.flags <- c.flags lor flag_removable
+      else c.flags <- c.flags land lnot flag_removable
+
+    let[@inline] dead c = (c.flags land flag_dead) <> 0
+    let[@inline] set_dead c = c.flags <- c.flags lor flag_dead
+
+    let[@inline] activity c = c.activity
+    let[@inline] set_activity c w = c.activity <- w
+
+    module Tbl = Hashtbl.Make(struct
+        type t = clause
+        let hash = hash
+        let equal = equal
+      end)
+
+    let pp fmt c =
+      Format.fprintf fmt "%s : %a" (name c) Atom.pp_a c.atoms
+
+    let debug_premise out = function
+      | Hyp _ -> Format.fprintf out "hyp"
+      | Lemma _ -> Format.fprintf out "th_lemma"
+      | Local -> Format.fprintf out "local"
+      | History v ->
+        List.iter (fun c -> Format.fprintf out "%s,@ " (name_of_clause c)) v
+      | Empty_premise -> Format.fprintf out "<no premise>"
+
+    let debug out ({atoms=arr; cpremise=cp;_}as c) =
+      Format.fprintf out "%s@[<hov>{@[<hov>%a@]}@ cpremise={@[<hov>%a@]}@]"
+        (name c) Atom.debug_a arr debug_premise cp
+  end
+
+  module Proof =  struct
+    exception Resolution_error of string
+
+    type atom = Atom.t
+    type clause = Clause.t
+    type formula = Formula.t
+    type lemma = Plugin.proof
+
+    let error_res_f msg = Format.kasprintf (fun s -> raise (Resolution_error s)) msg
+
+    let[@inline] clear_var_of_ (a:atom) = Var.clear a.var
+
+    (* Compute resolution of 2 clauses.
+       returns [pivots, resulting_atoms] *)
+    let resolve (c1:clause) (c2:clause) : atom list * atom list =
+      (* invariants: only atoms in [c2] are marked, and the pivot is
+         cleared when traversing [c1] *)
+      Array.iter Atom.mark c2.atoms;
+      let pivots = ref [] in
+      let l =
+        Array.fold_left
+          (fun l a ->
+             if Atom.seen a then l
+             else if Atom.seen a.neg then (
+               pivots := a.var.pa :: !pivots;
+               clear_var_of_ a;
+               l
+             ) else a::l)
+          [] c1.atoms
+      in
+      let l =
+        Array.fold_left (fun l a -> if Atom.seen a then a::l else l) l c2.atoms
+      in
+      Array.iter clear_var_of_ c2.atoms;
+      !pivots, l
+
+    (* [find_dups c] returns a list of duplicate atoms, and the deduplicated list *)
+    let find_dups (c:clause) : atom list * atom list =
+      let res =
+        Array.fold_left
+          (fun (dups,l) a ->
+             if Atom.seen a then (
+               a::dups, l
+             ) else (
+               Atom.mark a;
+               dups, a::l
+             ))
+          ([], []) c.atoms
+      in
+      Array.iter clear_var_of_ c.atoms;
+      res
+
+    (* do [c1] and [c2] have the same lits, modulo reordering and duplicates? *)
+    let same_lits (c1:atom Iter.t) (c2:atom Iter.t): bool =
+      let subset a b =
+        Iter.iter Atom.mark b;
+        let res = Iter.for_all Atom.seen a in
+        Iter.iter clear_var_of_ b;
+        res
+      in
+      subset c1 c2 && subset c2 c1
+
+    let prove conclusion =
+      match conclusion.cpremise with
+      | History [] -> assert false
+      | Empty_premise -> raise Solver_intf.No_proof
+      | _ -> conclusion
+
+    let rec set_atom_proof a =
+      let aux acc b =
+        if Atom.equal a.neg b then acc
+        else set_atom_proof b :: acc
+      in
+      assert (a.var.v_level >= 0);
+      match (a.var.reason) with
+      | Some (Bcp c | Bcp_lazy (lazy c)) ->
+        Log.debugf 5 (fun k->k "(@[proof.analyze.clause@ :atom %a@ :c %a@])" Atom.debug a Clause.debug c);
+        if Array.length c.atoms = 1 then (
+          Log.debugf 5 (fun k -> k "(@[proof.analyze.old-reason@ %a@])" Atom.debug a);
+          c
+        ) else (
+          assert (a.neg.is_true);
+          let r = History (c :: (Array.fold_left aux [] c.atoms)) in
+          let c' = Clause.make_permanent [a.neg] r in
+          a.var.reason <- Some (Bcp c');
+          Log.debugf 5
+            (fun k -> k "(@[proof.analyze.new-reason@ :atom %a@ :c %a@])" Atom.debug a Clause.debug c');
+          c'
+        )
+      | _ ->
+        error_res_f "cannot prove atom %a" Atom.debug a
+
+    let prove_unsat conflict =
+      if Array.length conflict.atoms = 0 then (
+        conflict
+      ) else (
+        Log.debugf 1 (fun k -> k "(@[sat.prove-unsat@ :from %a@])" Clause.debug conflict);
+        let l = Array.fold_left (fun acc a -> set_atom_proof a :: acc) [] conflict.atoms in
+        let res = Clause.make_permanent [] (History (conflict :: l)) in
+        Log.debugf 1 (fun k -> k "(@[sat.proof-found@ %a@])" Clause.debug res);
+        res
+      )
+
+    let prove_atom a =
+      if a.is_true && a.var.v_level = 0 then
+        Some (set_atom_proof a)
+      else
+        None
+
+    type t = clause
+    and proof_node = {
+      conclusion : clause;
+      step : step;
+    }
+    and step =
+      | Hypothesis of lemma
+      | Assumption
+      | Lemma of lemma
+      | Duplicate of t * atom list
+      | Hyper_res of hyper_res_step
+
+    and hyper_res_step = {
+      hr_init: t;
+      hr_steps: (atom * t) list; (* list of pivot+clause to resolve against [init] *)
+    }
+
+    let[@inline] conclusion (p:t) : clause = p
+
+    type res_step = {
+      rs_res: atom list;
+      rs_c1: clause;
+      rs_c2: clause;
+      rs_pivot: atom;
+    }
+
+    (* find pivots for resolving [l] with [init], and also return
+       the atoms of the conclusion *)
+    let find_pivots (init:clause) (l:clause list) : _ * (atom * t) list =
+      Log.debugf 15
+        (fun k->k "(@[proof.find-pivots@ :init %a@ :l %a@])"
+            Clause.debug init (Format.pp_print_list Clause.debug) l);
+      Array.iter Atom.mark init.atoms;
+      let steps =
+        List.map
+          (fun c ->
+             let pivot =
+               match
+                 Iter.of_array c.atoms
+                 |> Iter.filter (fun a -> Atom.seen (Atom.neg a))
+                 |> Iter.to_list
+               with
+                 | [a] -> a
+                 | [] ->
+                   error_res_f "(@[proof.expand.pivot_missing@ %a@])" Clause.debug c
+                 | pivots ->
+                   error_res_f "(@[proof.expand.multiple_pivots@ %a@ :pivots %a@])"
+                     Clause.debug c Atom.debug_l pivots
+             in
+             Array.iter Atom.mark c.atoms; (* add atoms to result *)
+             clear_var_of_ pivot;
+             Atom.abs pivot, c)
+          l
+      in
+      (* cleanup *)
+      let res = ref [] in
+      let cleanup_a_ a =
+        if Atom.seen a then (
+          res := a :: !res;
+          clear_var_of_ a
+        )
+      in
+      Array.iter cleanup_a_ init.atoms;
+      List.iter (fun c -> Array.iter cleanup_a_ c.atoms) l;
+      !res, steps
+
+    let expand conclusion =
+      Log.debugf 5 (fun k -> k "(@[sat.proof.expand@ @[%a@]@])" Clause.debug conclusion);
+      match conclusion.cpremise with
+      | Lemma l ->
+        { conclusion; step = Lemma l; }
+      | Local ->
+        { conclusion; step = Assumption; }
+      | Hyp l ->
+        { conclusion; step = Hypothesis l; }
+      | History [] ->
+        error_res_f "@[empty history for clause@ %a@]" Clause.debug conclusion
+      | History [c] ->
+        let duplicates, res = find_dups c in
+        assert (same_lits (Iter.of_list res) (Clause.atoms_seq conclusion));
+        { conclusion; step = Duplicate (c, duplicates) }
+      | History (c :: r) ->
+        let res, steps = find_pivots c r in
+        assert (same_lits (Iter.of_list res) (Clause.atoms_seq conclusion));
+        { conclusion; step = Hyper_res {hr_init=c; hr_steps=steps};  }
+      | Empty_premise -> raise Solver_intf.No_proof
+
+    let rec res_of_hyper_res (hr: hyper_res_step) : _ * _ * atom =
+      let {hr_init=c1; hr_steps=l} = hr in
+      match l with
+      | [] -> assert false
+      | [a, c2] -> c1, c2, a (* done *)
+      | (a,c2) :: steps' ->
+        (* resolve [c1] with [c2], then resolve that against [steps] *)
+        let pivots, l = resolve c1 c2 in
+        assert (match pivots with [a'] -> Atom.equal a a' | _ -> false);
+        let c_1_2 = Clause.make_removable l (History [c1; c2]) in
+        res_of_hyper_res {hr_init=c_1_2; hr_steps=steps'}
+
+    (* Proof nodes manipulation *)
+    let is_leaf = function
+      | Hypothesis _
+      | Assumption
+      | Lemma _ -> true
+      | Duplicate _
+      | Hyper_res _ -> false
+
+    let parents = function
+      | Hypothesis _
+      | Assumption
+      | Lemma _ -> []
+      | Duplicate (p, _) -> [p]
+      | Hyper_res {hr_init; hr_steps} -> hr_init :: List.map snd hr_steps
+
+    let expl = function
+      | Hypothesis _ -> "hypothesis"
+      | Assumption -> "assumption"
+      | Lemma _ -> "lemma"
+      | Duplicate _ -> "duplicate"
+      | Hyper_res _ -> "hyper-resolution"
+
+    (* Compute unsat-core by accumulating the leaves *)
+    let unsat_core proof =
+      let rec aux res acc = function
+        | [] -> res, acc
+        | c :: r ->
+          if not @@ Clause.visited c then (
+            Clause.set_visited c true;
+            match c.cpremise with
+            | Empty_premise -> raise Solver_intf.No_proof
+            | Hyp _ | Lemma _ | Local -> aux (c :: res) acc r
+            | History h ->
+              let l = List.fold_left (fun acc c ->
+                  if not @@ Clause.visited c then c :: acc else acc) r h in
+              aux res (c :: acc) l
+          ) else (
+            aux res acc r
+          )
+      in
+      let res, tmp = aux [] [] [proof] in
+      List.iter (fun c -> Clause.set_visited c false) res;
+      List.iter (fun c -> Clause.set_visited c false) tmp;
+      res
+
+    module Tbl = Clause.Tbl
+
+    type task =
+      | Enter of t
+      | Leaving of t
+
+    let spop s = try Some (Stack.pop s) with Stack.Empty -> None
+
+    let rec fold_aux s h f acc =
+      match spop s with
+      | None -> acc
+      | Some (Leaving c) ->
+        Tbl.add h c true;
+        fold_aux s h f (f acc (expand c))
+      | Some (Enter c) ->
+        if not (Tbl.mem h c) then begin
+          Stack.push (Leaving c) s;
+          let node = expand c in
+          begin match node.step with
+            | Duplicate (p1, _) ->
+              Stack.push (Enter p1) s
+            | Hyper_res {hr_init=p1; hr_steps=l} ->
+              List.iter (fun (_,p2) -> Stack.push (Enter p2) s) l;
+              Stack.push (Enter p1) s;
+            | Hypothesis _ | Assumption | Lemma _ -> ()
+          end
+        end;
+        fold_aux s h f acc
+
+    let fold f acc p =
+      let h = Tbl.create 42 in
+      let s = Stack.create () in
+      Stack.push (Enter p) s;
+      fold_aux s h f acc
+
+    let check_empty_conclusion (p:t) =
+      if Array.length p.atoms > 0 then (
+        error_res_f "@[<2>Proof.check: non empty conclusion for clause@ %a@]" Clause.debug p;
+      )
+
+    let check (p:t) = fold (fun () _ -> ()) () p
+  end
+  type proof = Proof.t
+
+  module H = (Heap.Make [@specialise]) (struct
+    type t = Elt.t
+    let[@inline] cmp i j = Elt.weight j < Elt.weight i (* comparison by weight *)
+    let idx = Elt.idx
+    let set_idx = Elt.set_idx
+  end)
+
+  (* cause of "unsat", possibly conditional to local assumptions *)
+  type unsat_cause =
+    | US_local of {
+        first: atom; (* assumption which was found to be proved false *)
+        core: atom list; (* the set of assumptions *)
+      }
+    | US_false of clause (* true unsat *)
+
+  exception E_sat
+  exception E_unsat of unsat_cause
+  exception UndecidedLit
+  exception Restart
+  exception Conflict of clause
+
+  (* Log levels *)
+  let error = 1
+  let warn = 3
+  let info = 5
+  let debug = 50
+
+  let var_decay : float = 1. /. 0.95
+  (* inverse of the activity factor for variables. Default 1/0.95 *)
+
+  let clause_decay : float = 1. /. 0.999
+  (* inverse of the activity factor for clauses. Default 1/0.999 *)
+
+  let restart_inc : float = 1.5
+  (* multiplicative factor for restart limit, default 1.5 *)
+
+  let learntsize_inc : float = 1.1
+  (* multiplicative factor for [learntsize_factor] at each restart, default 1.1 *)
+
+  (* Singleton type containing the current state *)
+  type t = {
+    st : st;
+    th: theory;
+
+    store_proof: bool; (* do we store proofs? *)
+
+    (* Clauses are simplified for eficiency purposes. In the following
+       vectors, the comments actually refer to the original non-simplified
+       clause. *)
+
+    clauses_hyps : clause Vec.t;
+    (* clauses added by the user *)
+    clauses_learnt : clause Vec.t;
+    (* learnt clauses (tautologies true at any time, whatever the user level) *)
+
+    clauses_to_add : clause Vec.t;
+    (* Clauses either assumed or pushed by the theory, waiting to be added. *)
+
+    mutable unsat_at_0: clause option;
+    (* conflict at level 0, if any *)
+
+    mutable next_decisions : atom list;
+    (* When the last conflict was a semantic one (mcsat),
+       this stores the next decision to make;
+       if some theory wants atoms to be decided on (for theory combination),
+       store them here. *)
+
+    trail : trail_elt Vec.t;
+    (* decision stack + propagated elements (atoms or assignments). *)
+
+    elt_levels : int Vec.t;
+    (* decision levels in [trail]  *)
+
+    mutable assumptions: atom Vec.t;
+    (* current assumptions *)
+
+    mutable th_head : int;
+    (* Start offset in the queue {!trail} of
+       unit facts not yet seen by the theory. *)
+    mutable elt_head : int;
+    (* Start offset in the queue {!trail} of
+       unit facts to propagate, within the trail *)
+
+    (* invariant:
+       - during propagation, th_head <= elt_head
+       - then, once elt_head reaches length trail, Th.assume is
+         called so that th_head can catch up with elt_head
+       - this is repeated until a fixpoint is reached;
+       - before a decision (and after the fixpoint),
+         th_head = elt_head = length trail
+    *)
+
+    order : H.t;
+    (* Heap ordered by variable activity *)
+
+    to_clear: var Vec.t;
+    (* variables to unmark *)
+
+    mutable var_incr : float;
+    (* increment for variables' activity *)
+
+    mutable clause_incr : float;
+    (* increment for clauses' activity *)
+
+    mutable on_conflict : (atom array -> unit) option;
+    mutable on_decision : (atom -> unit) option;
+    mutable on_new_atom: (atom -> unit) option;
+  }
+  type solver = t
+
+  (* intial restart limit *)
+  let restart_first = 100
+
+  (* initial limit for the number of learnt clauses, 1/3 of initial
+      number of clauses by default *)
+  let learntsize_factor = 1. /. 3.
+
+  let _nop_on_conflict (_:atom array) = ()
+
+  (* Starting environment. *)
+  let create_ ~st ~store_proof (th:theory) : t = {
+    st; th;
+    unsat_at_0=None;
+    next_decisions = [];
+
+    clauses_hyps = Vec.create();
+    clauses_learnt = Vec.create();
+
+    clauses_to_add = Vec.create ();
+    to_clear=Vec.create();
+
+    th_head = 0;
+    elt_head = 0;
+
+    trail = Vec.create ();
+    elt_levels = Vec.create();
+    assumptions= Vec.create();
+
+    order = H.create();
+
+    var_incr = 1.;
+    clause_incr = 1.;
+    store_proof;
+    on_conflict = None;
+    on_decision= None;
+    on_new_atom = None;
+  }
+
+  let create
+      ?on_conflict ?on_decision ?on_new_atom
+      ?(store_proof=true) ?(size=`Big) (th:theory) : t =
+    let st = create_st ~size () in
+    let st = create_ ~st ~store_proof th in
+    st.on_new_atom <- on_new_atom;
+    st.on_decision <- on_decision;
+    st.on_conflict <- on_conflict;
+    st
+
+  let[@inline] st t = t.st
+  let[@inline] nb_clauses st = Vec.size st.clauses_hyps
+  let[@inline] decision_level st = Vec.size st.elt_levels
+
+  (* Do we have a level-0 empty clause? *)
+  let[@inline] check_unsat_ st =
+    match st.unsat_at_0 with
+    | Some c -> raise (E_unsat (US_false c))
+    | None -> ()
+
+  (* Iteration over subterms.
+     When incrementing activity, we want to be able to iterate over
+     all subterms of a formula. However, the function provided by the theory
+     may be costly (if it walks a tree-like structure, and does some processing
+     to ignore some subterms for instance), so we want to 'cache' the list
+     of subterms of each formula, so we have a field [v_assignable]
+     directly in variables to do so.  *)
+  let iter_sub f v =
+    if Plugin.mcsat then (
+      match v.v_assignable with
+      | Some l -> List.iter f l
+      | None -> assert false
+    )
+
+  let mk_atom_mcsat_ st a =
+    match a.var.v_assignable with
+    | Some _ -> ()
+    | None ->
+      let l = ref [] in
+      Plugin.iter_assignable st.th
+        (fun t -> l := Lit.make st.st t :: !l)
+        a.var.pa.lit;
+      a.var.v_assignable <- Some !l;
+      ()
+
+  (* When we have a new literal,
+     we need to first create the list of its subterms. *)
+  let mk_atom ?default_pol st (f:formula) : atom =
+    let res = Atom.make ?default_pol st.st f in
+    if Plugin.mcsat then (
+      mk_atom_mcsat_ st res;
+    );
+    res
+
+  (* Variable and literal activity.
+     Activity is used to decide on which variable to decide when propagation
+     is done. Uses a heap (implemented in Iheap), to keep track of variable activity.
+     To be more general, the heap only stores the variable/literal id (i.e an int).
+     When we add a variable (which wraps a formula), we also need to add all
+     its subterms.
+  *)
+  let rec insert_elt_order st (elt:elt) : unit =
+    H.insert st.order elt;
+    if Plugin.mcsat then (
+      match elt with
+      | E_lit _ -> ()
+      | E_var v -> insert_subterms_order st v
+    )
+
+  and insert_var_order st (v:var) : unit =
+    insert_elt_order st (E_var v)
+
+  and insert_subterms_order st (v:var) : unit =
+    iter_sub (fun t -> insert_elt_order st (Elt.of_lit t)) v
+
+  (* Add new litterals/atoms on which to decide on, even if there is no
+     clause that constrains it.
+     We could maybe check if they have already has been decided before
+     inserting them into the heap, if it appears that it helps performance. *)
+  let make_term st t =
+    let l = Lit.make st.st t in
+    if l.l_level < 0 then (
+      insert_elt_order st (E_lit l);
+    )
+
+  let make_atom st (p:formula) : atom =
+    let a = mk_atom st p in
+    if a.var.v_level < 0 then (
+      insert_elt_order st (E_var a.var);
+      (match st.on_new_atom with Some f -> f a | None -> ());
+    ) else (
+      assert (a.is_true || a.neg.is_true);
+    );
+    a
+
+  (* Rather than iterate over all the heap when we want to decrease all the
+     variables/literals activity, we instead increase the value by which
+     we increase the activity of 'interesting' var/lits. *)
+  let[@inline] var_decay_activity st =
+    st.var_incr <- st.var_incr *. var_decay
+
+  let[@inline] clause_decay_activity st =
+    st.clause_incr <- st.clause_incr *. clause_decay
+
+  (* increase activity of [v] *)
+  let var_bump_activity_aux st v =
+    v.v_weight <- v.v_weight +. st.var_incr;
+    if v.v_weight > 1e100 then (
+      for i = 0 to nb_elt st.st - 1 do
+        Elt.set_weight (get_elt st.st i) ((Elt.weight (get_elt st.st i)) *. 1e-100)
+      done;
+      st.var_incr <- st.var_incr *. 1e-100;
+    );
+    let elt = Elt.of_var v in
+    if H.in_heap elt then (
+      H.decrease st.order elt
+    )
+
+  (* increase activity of literal [l] *)
+  let lit_bump_activity_aux (st:t) (l:lit): unit =
+    l.l_weight <- l.l_weight +. st.var_incr;
+    if l.l_weight > 1e100 then (
+      iter_elt st.st (fun e -> Elt.set_weight e (Elt.weight e *. 1e-100));
+      st.var_incr <- st.var_incr *. 1e-100;
+    );
+    let elt = Elt.of_lit l in
+    if H.in_heap elt then (
+      H.decrease st.order elt
+    )
+
+  (* increase activity of var [v] *)
+  let var_bump_activity st (v:var): unit =
+    var_bump_activity_aux st v;
+    iter_sub (lit_bump_activity_aux st) v
+
+  (* increase activity of clause [c] *)
+  let clause_bump_activity st (c:clause) : unit =
+    c.activity <- c.activity +. st.clause_incr;
+    if c.activity > 1e20 then (
+      Vec.iter (fun c -> c.activity <- c.activity *. 1e-20) st.clauses_learnt;
+      st.clause_incr <- st.clause_incr *. 1e-20
+    )
+
+  (* Simplification of clauses.
+
+     When adding new clauses, it is desirable to 'simplify' them, i.e
+     minimize the amount of literals in it, because it greatly reduces
+     the search space for new watched literals during propagation.
+     Additionally, we have to partition the lits, to ensure the watched
+     literals (which are the first two lits of the clause) are appropriate.
+     Indeed, it is better to watch true literals, and then unassigned literals.
+     Watching false literals should be a last resort, and come with constraints
+     (see {!add_clause}).
+  *)
+  exception Trivial
+
+  (* [arr_to_list a i] converts [a.(i), ... a.(length a-1)] into a list *)
+  let arr_to_list arr i : _ list =
+    if i >= Array.length arr then []
+    else Array.to_list (Array.sub arr i (Array.length arr - i))
+
+  (* Eliminates atom duplicates in clauses *)
+  let eliminate_duplicates clause : clause =
+    let trivial = ref false in
+    let duplicates = ref [] in
+    let res = ref [] in
+    Array.iter (fun a ->
+        if Atom.seen a then duplicates := a :: !duplicates
+        else (
+          Atom.mark a;
+          res := a :: !res
+        ))
+      clause.atoms;
+    List.iter
+      (fun a ->
+         if Var.seen_both a.var then trivial := true;
+         Var.clear a.var)
+      !res;
+    if !trivial then (
+      raise Trivial
+    ) else if !duplicates = [] then (
+      clause
+    ) else (
+      Clause.make ~flags:clause.flags !res (History [clause])
+    )
+
+  (* Partition literals for new clauses, into:
+     - true literals (maybe makes the clause trivial if the lit is proved true at level 0)
+     - unassigned literals, yet to be decided
+     - false literals (not suitable to watch, those at level 0 can be removed from the clause)
+
+     Clauses that propagated false lits are remembered to reconstruct resolution proofs.
+  *)
+  let partition atoms : atom list * clause list =
+    let rec partition_aux trues unassigned falses history i =
+      if i >= Array.length atoms then (
+        trues @ unassigned @ falses, history
+      ) else (
+        let a = atoms.(i) in
+        if a.is_true then (
+          let l = a.var.v_level in
+          if l = 0 then
+            raise Trivial (* A var true at level 0 gives a trivially true clause *)
+          else
+            (a :: trues) @ unassigned @ falses @
+            (arr_to_list atoms (i + 1)), history
+        ) else if a.neg.is_true then (
+          let l = a.var.v_level in
+          if l = 0 then (
+            match a.var.reason with
+            | Some (Bcp cl | Bcp_lazy (lazy cl)) ->
+              partition_aux trues unassigned falses (cl :: history) (i + 1)
+            (* A var false at level 0 can be eliminated from the clause,
+               but we need to kepp in mind that we used another clause to simplify it. *)
+            | Some Semantic ->
+              partition_aux trues unassigned falses history (i + 1)
+            (* Semantic propagations at level 0 are, well not easy to deal with,
+               this shouldn't really happen actually (because semantic propagations
+               at level 0 should come with a proof). *)
+            (* TODO: get a proof of the propagation. *)
+            | None | Some Decision -> assert false
+            (* The var must have a reason, and it cannot be a decision/assumption,
+               since its level is 0. *)
+          ) else (
+            partition_aux trues unassigned (a::falses) history (i + 1)
+          )
+        ) else (
+          partition_aux trues (a::unassigned) falses history (i + 1)
+        )
+      )
+    in
+    partition_aux [] [] [] [] 0
+
+
+  (* Making a decision.
+     Before actually creatig a new decision level, we check that
+     all propagations have been done and propagated to the theory,
+     i.e that the theoriy state indeed takes into account the whole
+     stack of literals
+     i.e we have indeed reached a propagation fixpoint before making
+     a new decision *)
+  let new_decision_level st =
+    assert (st.th_head = Vec.size st.trail);
+    assert (st.elt_head = Vec.size st.trail);
+    Vec.push st.elt_levels (Vec.size st.trail);
+    Plugin.push_level st.th;
+    ()
+
+  (* Attach/Detach a clause.
+
+     A clause is attached (to its watching lits) when it is first added,
+     either because it is assumed or learnt.
+
+  *)
+  let attach_clause c =
+    assert (not @@ Clause.attached c);
+    Log.debugf debug (fun k -> k "(@[sat.attach-clause@ %a@])" Clause.debug c);
+    Vec.push c.atoms.(0).neg.watched c;
+    Vec.push c.atoms.(1).neg.watched c;
+    Clause.set_attached c true;
+    ()
+
+  (* Backtracking.
+     Used to backtrack, i.e cancel down to [lvl] excluded,
+     i.e we want to go back to the state the solver was in
+         when decision level [lvl] was created. *)
+  let cancel_until st lvl =
+    assert (lvl >= 0);
+    (* Nothing to do if we try to backtrack to a non-existent level. *)
+    if decision_level st <= lvl then (
+      Log.debugf debug (fun k -> k "(@[sat.cancel-until.nop@ :already-at-level <= %d@])" lvl)
+    ) else (
+      Log.debugf info (fun k -> k "(@[sat.cancel-until %d@])" lvl);
+      (* We set the head of the solver and theory queue to what it was. *)
+      let head = ref (Vec.get st.elt_levels lvl) in
+      st.elt_head <- !head;
+      st.th_head <- !head;
+      (* Now we need to cleanup the vars that are not valid anymore
+         (i.e to the right of elt_head in the queue. *)
+      for c = st.elt_head to Vec.size st.trail - 1 do
+        match (Vec.get st.trail c) with
+        (* A literal is unassigned, we nedd to add it back to
+           the heap of potentially assignable literals, unless it has
+           a level lower than [lvl], in which case we just move it back. *)
+        | Lit l ->
+          if l.l_level <= lvl then (
+            Vec.set st.trail !head (Trail_elt.of_lit l);
+            head := !head + 1
+          ) else (
+            l.assigned <- None;
+            l.l_level <- -1;
+            insert_elt_order st (Elt.of_lit l)
+          )
+        (* A variable is not true/false anymore, one of two things can happen: *)
+        | Atom a ->
+          if a.var.v_level <= lvl then (
+            (* It is a late propagation, which has a level
+               lower than where we backtrack, so we just move it to the head
+               of the queue, to be propagated again. *)
+            Vec.set st.trail !head (Trail_elt.of_atom a);
+            head := !head + 1
+          ) else (
+            (* it is a result of bolean propagation, or a semantic propagation
+               with a level higher than the level to which we backtrack,
+               in that case, we simply unset its value and reinsert it into the heap. *)
+            a.is_true <- false;
+            a.neg.is_true <- false;
+            a.var.v_level <- -1;
+            a.var.reason <- None;
+            insert_elt_order st (Elt.of_var a.var)
+          )
+      done;
+      (* Recover the right theory state. *)
+      let n = decision_level st - lvl in
+      assert (n>0);
+      (* Resize the vectors according to their new size. *)
+      Vec.shrink st.trail !head;
+      Vec.shrink st.elt_levels lvl;
+      Plugin.pop_levels st.th n;
+      st.next_decisions <- [];
+    );
+    ()
+
+  let pp_unsat_cause out = function
+    | US_local {first=_; core} ->
+      Format.fprintf out "(@[unsat-cause@ :false-assumptions %a@])"
+        (Format.pp_print_list Atom.pp) core
+    | US_false c ->
+      Format.fprintf out "(@[unsat-cause@ :false %a@])" Clause.debug c
+
+  (* Unsatisfiability is signaled through an exception, since it can happen
+     in multiple places (adding new clauses, or solving for instance). *)
+  let report_unsat st (us:unsat_cause) : _ =
+    Log.debugf info (fun k -> k "(@[sat.unsat-conflict@ %a@])" pp_unsat_cause us);
+    let us = match us with
+      | US_false c ->
+        let c = if st.store_proof then Proof.prove_unsat c else c in
+        st.unsat_at_0 <- Some c;
+        US_false c
+      | _ -> us
+    in
+    raise (E_unsat us)
+
+  (* Simplification of boolean propagation reasons.
+     When doing boolean propagation *at level 0*, it can happen
+     that the clause cl, which propagates a formula, also contains
+     other formulas, but has been simplified. in which case, we
+     need to rebuild a clause with correct history, in order to
+     be able to build a correct proof at the end of proof search. *)
+  let simpl_reason : reason -> reason = function
+    | (Bcp cl | Bcp_lazy (lazy cl)) as r ->
+      let l, history = partition cl.atoms in
+      begin match l with
+        | [_] ->
+          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' = Clause.make ~flags:cl.flags l (History (cl :: history)) in
+            Log.debugf debug
+              (fun k -> k "(@[<hv>sat.simplified-reason@ %a@ %a@])" Clause.debug cl Clause.debug c');
+            Bcp c'
+          )
+        | _ ->
+          Log.debugf error
+            (fun k ->
+               k "(@[<v2>sat.simplify-reason.failed@ :at %a@ %a@]"
+                 (Vec.pp ~sep:"" Atom.debug) (Vec.of_list l)
+                 Clause.debug cl);
+          assert false
+      end
+    | (Decision | Semantic) as r -> r
+
+  (* Boolean propagation.
+     Wrapper function for adding a new propagated formula. *)
+  let enqueue_bool st a ~level:lvl reason : unit =
+    if a.neg.is_true then (
+      Log.debugf error
+        (fun k->k "(@[sat.error.trying to enqueue a false literal %a@])" Atom.debug a);
+      assert false
+    );
+    assert (not a.is_true && a.var.v_level < 0 &&
+            a.var.reason = None && lvl >= 0);
+    let reason =
+      if lvl > 0 then reason
+      else simpl_reason reason
+    in
+    a.is_true <- true;
+    a.var.v_level <- lvl;
+    a.var.reason <- Some reason;
+    Vec.push st.trail (Trail_elt.of_atom a);
+    Log.debugf debug
+      (fun k->k "(@[sat.enqueue[%d]@ %a@])" (Vec.size st.trail) Atom.debug a);
+    ()
+
+  let enqueue_semantic st a terms =
+    if not a.is_true then (
+      let l = List.map (Lit.make st.st) terms in
+      let lvl = List.fold_left (fun acc {l_level; _} ->
+          assert (l_level > 0); max acc l_level) 0 l in
+      enqueue_bool st a ~level:lvl Semantic
+    )
+
+  (* MCsat semantic assignment *)
+  let enqueue_assign st (l:lit) (value:value) lvl =
+    match l.assigned with
+    | Some _ ->
+      Log.debugf error
+        (fun k -> k "(@[sat.error: Trying to assign an already assigned literal:@ %a@])" Lit.debug l);
+      assert false
+    | None ->
+      assert (l.l_level < 0);
+      l.assigned <- Some value;
+      l.l_level <- lvl;
+      Vec.push st.trail (Trail_elt.of_lit l);
+      Log.debugf debug
+        (fun k -> k "(@[sat.enqueue-semantic[%d]@ %a@])" (Vec.size st.trail) Lit.debug l);
+      ()
+
+  (* swap elements of array *)
+  let[@inline] swap_arr a i j =
+    if i<>j then (
+      let tmp = a.(i) in
+      a.(i) <- a.(j);
+      a.(j) <- tmp;
+    )
+
+  (* move atoms assigned at high levels first *)
+  let put_high_level_atoms_first (arr:atom array) : unit =
+    Array.iteri
+      (fun i a ->
+         if i>0 && Atom.level a > Atom.level arr.(0) then (
+           (* move first to second, [i]-th to first, second to [i] *)
+           if i=1 then (
+             swap_arr arr 0 1;
+           ) else (
+             let tmp = arr.(1) in
+             arr.(1) <- arr.(0);
+             arr.(0) <- arr.(i);
+             arr.(i) <- tmp;
+           );
+         ) else if i>1 && Atom.level a > Atom.level arr.(1) then (
+           swap_arr arr 1 i;
+         ))
+      arr
+
+  (* evaluate an atom for MCsat, if it's not assigned
+     by boolean propagation/decision *)
+  let th_eval st a : bool option =
+    if a.is_true || a.neg.is_true then None
+    else match Plugin.eval st.th a.lit with
+      | Solver_intf.Unknown -> None
+      | Solver_intf.Valued (b, l) ->
+        if l = [] then (
+          invalid_argf "semantic propagation at level 0 currently forbidden: %a" Atom.pp a;
+        );
+        let atom = if b then a else a.neg in
+        enqueue_semantic st atom l;
+        Some b
+
+  (* find which level to backtrack to, given a conflict clause
+     and a boolean stating whether it is
+     a UIP ("Unique Implication Point")
+     precond: the atom list is sorted by decreasing decision level *)
+  let backtrack_lvl _st (arr: atom array) : int * bool =
+    if Array.length arr <= 1 then (
+      0, true
+    ) else (
+      let a = arr.(0) in
+      let b = arr.(1) in
+      assert(a.var.v_level > 0);
+      if a.var.v_level > b.var.v_level then (
+        (* backtrack below [a], so we can propagate [not a] *)
+        b.var.v_level, true
+      ) else (
+        assert (a.var.v_level = b.var.v_level);
+        assert (a.var.v_level >= 0);
+        max (a.var.v_level - 1) 0, false
+      )
+    )
+
+  (* result of conflict analysis, containing the learnt clause and some
+     additional info.
+
+     invariant: cr_history's order matters, as its head is later used
+     during pop operations to determine the origin of a clause/conflict
+     (boolean conflict i.e hypothesis, or theory lemma) *)
+  type conflict_res = {
+    cr_backtrack_lvl : int; (* level to backtrack to *)
+    cr_learnt: atom array; (* lemma learnt from conflict *)
+    cr_history: clause list; (* justification *)
+    cr_is_uip: bool; (* conflict is UIP? *)
+  }
+
+  let[@inline] get_atom st i =
+    match Vec.get st.trail i with
+    | Atom x -> x
+    | Lit _ -> assert false
+
+  (* conflict analysis for SAT
+     Same idea as the mcsat analyze function (without semantic propagations),
+     except we look the the Last UIP (TODO: check ?), and do it in an imperative
+     and efficient manner. *)
+  let analyze st c_clause : conflict_res =
+    let pathC  = ref 0 in
+    let learnt = ref [] in
+    let cond   = ref true in
+    let blevel = ref 0 in
+    let to_unmark = st.to_clear in (* for cleanup *)
+    let c      = ref (Some c_clause) in
+    let tr_ind = ref (Vec.size st.trail - 1) in
+    let history = ref [] in
+    assert (decision_level st > 0);
+    Vec.clear to_unmark;
+    let conflict_level =
+      if Plugin.mcsat || Plugin.has_theory
+      then Array.fold_left (fun acc p -> max acc p.var.v_level) 0 c_clause.atoms
+      else decision_level st
+    in
+    Log.debugf debug
+      (fun k -> k "(@[sat.analyze-conflict@ :c-level %d@ :clause %a@])" conflict_level Clause.debug c_clause);
+    while !cond do
+      begin match !c with
+        | None ->
+          Log.debug debug "(@[sat.analyze-conflict: skipping resolution for semantic propagation@])"
+        | Some clause ->
+          Log.debugf debug (fun k->k"(@[sat.analyze-conflict.resolve@ %a@])"  Clause.debug clause);
+          if Clause.removable clause then (
+            clause_bump_activity st clause;
+          );
+          history := clause :: !history;
+          (* visit the current predecessors *)
+          for j = 0 to Array.length clause.atoms - 1 do
+            let q = clause.atoms.(j) in
+            assert (q.is_true || q.neg.is_true && q.var.v_level >= 0); (* unsure? *)
+            if q.var.v_level <= 0 then (
+              assert (q.neg.is_true);
+              match q.var.reason with
+              | Some (Bcp cl | Bcp_lazy (lazy cl)) -> history := cl :: !history
+              | Some (Decision | Semantic) | None -> assert false
+            );
+            if not (Var.marked q.var) then (
+              Var.mark q.var;
+              Vec.push to_unmark q.var;
+              if q.var.v_level > 0 then (
+                var_bump_activity st q.var;
+                if q.var.v_level >= conflict_level then (
+                  incr pathC;
+                ) else (
+                  learnt := q :: !learnt;
+                  blevel := max !blevel q.var.v_level
+                )
+              )
+            )
+          done
+      end;
+
+      (* look for the next node to expand *)
+      while
+        let a = Vec.get st.trail !tr_ind in
+        Log.debugf debug
+          (fun k -> k "(@[sat.analyze-conflict.at-trail-elt@ %a@])" Trail_elt.debug a);
+        match a with
+        | Atom q ->
+          (not (Var.marked q.var)) ||
+          (q.var.v_level < conflict_level)
+        | Lit _ -> true
+      do
+        decr tr_ind;
+      done;
+      let p = get_atom st !tr_ind in
+      decr pathC;
+      decr tr_ind;
+      match !pathC, p.var.reason with
+      | 0, _ ->
+        cond := false;
+        learnt := p.neg :: List.rev !learnt
+      | n, Some Semantic ->
+        assert (n > 0);
+        learnt := p.neg :: !learnt;
+        c := None
+      | n, Some (Bcp cl | Bcp_lazy (lazy cl)) ->
+        assert (n > 0);
+        assert (p.var.v_level >= conflict_level);
+        c := Some cl
+      | _, (None | Some Decision) -> assert false
+    done;
+    Vec.iter Var.clear to_unmark;
+    Vec.clear to_unmark;
+    (* put high-level literals first, so that:
+       - they make adequate watch lits
+       - the first literal is the UIP, if any *)
+    let a = Array.of_list !learnt in
+    Array.fast_sort (fun p q -> compare q.var.v_level p.var.v_level) a;
+    (* put_high_level_atoms_first a; *)
+    let level, is_uip = backtrack_lvl st a in
+    { cr_backtrack_lvl = level;
+      cr_learnt = a;
+      cr_history = List.rev !history;
+      cr_is_uip = is_uip;
+    }
+
+  (* add the learnt clause to the clause database, propagate, etc. *)
+  let record_learnt_clause st (confl:clause) (cr:conflict_res): unit =
+    let proof = if st.store_proof then History cr.cr_history else Empty_premise in
+    begin match cr.cr_learnt with
+      | [| |] -> assert false
+      | [|fuip|] ->
+        assert (cr.cr_backtrack_lvl = 0 && decision_level st = 0);
+        if fuip.neg.is_true then (
+          (* incompatible at level 0 *)
+          report_unsat st (US_false confl)
+        ) else (
+          let uclause = Clause.make_removable_a cr.cr_learnt proof  in
+          (* no need to attach [uclause], it is true at level 0 *)
+          enqueue_bool st fuip ~level:0 (Bcp uclause)
+        )
+      | _ ->
+        let fuip = cr.cr_learnt.(0) in
+        let lclause = Clause.make_removable_a cr.cr_learnt proof in
+        if Array.length lclause.atoms > 2 then (
+          Vec.push st.clauses_learnt lclause; (* potentially gc'able *)
+        );
+        attach_clause lclause;
+        clause_bump_activity st lclause;
+        if cr.cr_is_uip then (
+          enqueue_bool st fuip ~level:cr.cr_backtrack_lvl (Bcp lclause)
+        ) else (
+          assert Plugin.mcsat;
+          assert (st.next_decisions = []);
+          st.next_decisions <- [fuip.neg];
+        )
+    end;
+    var_decay_activity st;
+    clause_decay_activity st
+
+  (* process a conflict:
+     - learn clause
+     - backtrack
+     - report unsat if conflict at level 0
+  *)
+  let add_boolean_conflict st (confl:clause): unit =
+    Log.debugf info (fun k -> k "(@[sat.add-bool-conflict@ %a@])" Clause.debug confl);
+    st.next_decisions <- [];
+    assert (decision_level st >= 0);
+    if decision_level st = 0 ||
+       Array.for_all (fun a -> a.var.v_level <= 0) confl.atoms then (
+      (* Top-level conflict *)
+      report_unsat st (US_false confl);
+    );
+    let cr = analyze st confl in
+    cancel_until st (max cr.cr_backtrack_lvl 0);
+    record_learnt_clause st confl cr
+
+  (* Get the correct vector to insert a clause in. *)
+  let[@inline] add_clause_to_vec st c =
+    if Clause.removable c then (
+      Vec.push st.clauses_learnt c
+    ) else (
+      Vec.push st.clauses_hyps c
+    )
+
+  (* Add a new clause, simplifying, propagating, and backtracking if
+     the clause is false in the current trail *)
+  let add_clause_ st (init:clause) : unit =
+    Log.debugf debug (fun k -> k "(@[sat.add-clause@ @[<hov>%a@]@])" Clause.debug 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_elt_order st (Elt.of_var x.var)) init.atoms;
+    try
+      let c = eliminate_duplicates init in
+      assert (c.flags = init.flags);
+      Log.debugf debug (fun k -> k "(@[sat.dups-removed@ %a@])" Clause.debug c);
+      let atoms, history = partition c.atoms in
+      let clause =
+        if history = [] then (
+          (* just update order of atoms *)
+          List.iteri (fun i a -> c.atoms.(i) <- a) atoms;
+          c
+        ) else (
+          let proof = if st.store_proof then History (c::history) else Empty_premise in
+          Clause.make ~flags:c.flags atoms proof
+        )
+      in
+      assert (clause.flags = init.flags);
+      Log.debugf info (fun k->k "(@[sat.new-clause@ @[<hov>%a@]@])" Clause.debug clause);
+      match atoms with
+      | [] ->
+        report_unsat st @@ US_false clause
+      | [a]   ->
+        cancel_until st 0;
+        if a.neg.is_true then (
+          (* cannot recover from this *)
+          report_unsat st @@ US_false clause
+        ) else if a.is_true then (
+          () (* atom is already true, nothing to do *)
+        ) else (
+          Log.debugf debug
+            (fun k->k "(@[sat.add-clause.unit-clause@ :propagating %a@])" Atom.debug a);
+          add_clause_to_vec st clause;
+          enqueue_bool st a ~level:0 (Bcp clause)
+        )
+      | a::b::_ ->
+        add_clause_to_vec st clause;
+        if a.neg.is_true then (
+          (* Atoms need to be sorted in decreasing order of decision level,
+             or we might watch the wrong literals. *)
+          put_high_level_atoms_first clause.atoms;
+          attach_clause clause;
+          add_boolean_conflict st clause
+        ) else (
+          attach_clause clause;
+          if b.neg.is_true && not a.is_true && not a.neg.is_true then (
+            let lvl = List.fold_left (fun m a -> max m a.var.v_level) 0 atoms in
+            cancel_until st lvl;
+            enqueue_bool st a ~level:lvl (Bcp clause)
+          )
+        )
+    with Trivial ->
+      Log.debugf info
+        (fun k->k "(@[sat.add-clause@ :ignore-trivial @[%a@]@])" Clause.debug init)
+
+  let[@inline never] flush_clauses_ st =
+    while not @@ Vec.is_empty st.clauses_to_add do
+      let c = Vec.pop st.clauses_to_add in
+      add_clause_ st c
+    done
+
+  let[@inline] flush_clauses st =
+    if not @@ Vec.is_empty st.clauses_to_add then flush_clauses_ st
+
+  type watch_res =
+    | Watch_kept
+    | Watch_removed
+
+  (* boolean propagation.
+     [a] is the false atom, one of [c]'s two watch literals
+     [i] is the index of [c] in [a.watched]
+     @return whether [c] was removed from [a.watched]
+  *)
+  let propagate_in_clause st (a:atom) (c:clause) (i:int): watch_res =
+    let atoms = c.atoms in
+    let first = atoms.(0) in
+    if first == a.neg then (
+      (* false lit must be at index 1 *)
+      atoms.(0) <- atoms.(1);
+      atoms.(1) <- first
+    ) else (
+      assert (a.neg == atoms.(1))
+    );
+    let first = atoms.(0) in
+    if first.is_true
+    then Watch_kept (* true clause, keep it in watched *)
+    else (
+      try (* look for another watch lit *)
+        for k = 2 to Array.length atoms - 1 do
+          let ak = atoms.(k) in
+          if not (ak.neg.is_true) then (
+            (* watch lit found: update and exit *)
+            atoms.(1) <- ak;
+            atoms.(k) <- a.neg;
+            (* remove [c] from [a.watched], add it to [ak.neg.watched] *)
+            Vec.push ak.neg.watched c;
+            assert (Vec.get a.watched i == c);
+            Vec.fast_remove a.watched i;
+            raise_notrace Exit
+          )
+        done;
+        (* no watch lit found *)
+        if first.neg.is_true then (
+          (* clause is false *)
+          st.elt_head <- Vec.size st.trail;
+          raise_notrace (Conflict c)
+        ) else (
+          match th_eval st first with
+          | None -> (* clause is unit, keep the same watches, but propagate *)
+            enqueue_bool st first ~level:(decision_level st) (Bcp c)
+          | Some true -> ()
+          | Some false ->
+            st.elt_head <- Vec.size st.trail;
+            raise_notrace (Conflict c)
+        );
+        Watch_kept
+      with Exit ->
+        Watch_removed
+    )
+
+  (* propagate atom [a], which was just decided. This checks every
+     clause watching [a] to see if the clause is false, unit, or has
+     other possible watches
+     @param res the optional conflict clause that the propagation might trigger *)
+  let propagate_atom st a : unit =
+    let watched = a.watched in
+    let rec aux i =
+      if i >= Vec.size watched then ()
+      else (
+        let c = Vec.get watched i in
+        assert (Clause.attached c);
+        let j =
+          if Clause.dead c then (
+            Vec.fast_remove watched i;
+            i
+          ) else (
+            match propagate_in_clause st a c i with
+            | Watch_kept -> i+1
+            | Watch_removed -> i (* clause at this index changed *)
+          )
+        in
+        aux j
+      )
+    in
+    aux 0
+
+  (* Propagation (boolean and theory) *)
+  let create_atom ?default_pol st f =
+    let a = mk_atom ?default_pol st f in
+    ignore (th_eval st a);
+    a
+
+  exception Th_conflict of Clause.t
+
+  let slice_get st i =
+    match Vec.get st.trail i with
+    | Atom a ->
+      Solver_intf.Lit a.lit
+    | Lit {term; assigned = Some v; _} ->
+      Solver_intf.Assign (term, v)
+    | Lit _ -> assert false
+
+  let acts_add_clause st ?(keep=false) (l:formula list) (lemma:lemma): unit =
+    let atoms = List.rev_map (create_atom st) l in
+    let flags = if keep then 0 else Clause.flag_removable in
+    let c = Clause.make ~flags atoms (Lemma lemma) in
+    Log.debugf info (fun k->k "(@[sat.th.add-clause@ %a@])" Clause.debug c);
+    Vec.push st.clauses_to_add c
+
+  let acts_add_decision_lit (st:t) (f:formula) (sign:bool) : unit =
+    let a = create_atom st f in
+    let a = if sign then a else Atom.neg a in
+    if not (Atom.has_value a) then (
+      Log.debugf 10 (fun k->k "(@[sat.th.add-decision-lit@ %a@])" Atom.debug a);
+      st.next_decisions <- a :: st.next_decisions
+    )
+
+  let acts_raise st (l:formula list) proof : 'a =
+    let atoms = List.rev_map (create_atom st) l in
+    (* conflicts can be removed *)
+    let c = Clause.make_removable atoms (Lemma proof) in
+    Log.debugf 5 (fun k->k "(@[@{<yellow>sat.th.raise-conflict@}@ %a@])" Clause.debug c);
+    raise_notrace (Th_conflict c)
+
+  let check_consequence_lits_false_ l : unit =
+    match List.find Atom.is_true l with
+    | a ->
+      invalid_argf
+        "slice.acts_propagate:@ Consequence should contain only true literals, but %a isn't"
+        Atom.debug (Atom.neg a)
+    | exception Not_found -> ()
+
+  let acts_propagate (st:t) f = function
+    | Solver_intf.Eval l ->
+      let a = mk_atom st f in
+      enqueue_semantic st a l
+    | Solver_intf.Consequence mk_expl ->
+      let p = mk_atom st f in
+      if Atom.is_true p then ()
+      else if Atom.is_false p then (
+        let lits, proof = mk_expl() in
+        let l = List.rev_map (fun f -> Atom.neg @@ mk_atom st f) lits in
+        check_consequence_lits_false_ l;
+        let c = Clause.make_removable (p :: l) (Lemma proof) in
+        raise_notrace (Th_conflict c)
+      ) else (
+        insert_var_order st p.var;
+        let c = lazy (
+          let lits, proof = mk_expl () in
+          let l = List.rev_map (fun f -> Atom.neg @@ mk_atom st f) lits in
+          (* note: we can check that invariant here in the [lazy] block,
+             as conflict analysis will run in an environment where
+             the literals should be true anyway, since it's an extension of the
+             current trail
+             (otherwise the propagated lit would have been backtracked and
+             discarded already.) *)
+          check_consequence_lits_false_ l;
+          Clause.make_removable (p :: l) (Lemma proof)
+        ) in
+        let level = decision_level st in
+        enqueue_bool st p ~level (Bcp_lazy c)
+      )
+
+  let[@specialise] acts_iter st ~full head f : unit =
+    for i = (if full then 0 else head) to Vec.size st.trail-1 do
+      let e = match Vec.get st.trail i with
+        | Atom a ->
+          Solver_intf.Lit a.lit
+        | Lit {term; assigned = Some v; _} ->
+          Solver_intf.Assign (term, v)
+        | Lit _ -> assert false
+      in
+      f e
+    done
+
+  let eval_atom_ a =
+    if Atom.is_true a then Solver_intf.L_true
+    else if Atom.is_false a then Solver_intf.L_false
+    else Solver_intf.L_undefined
+
+  let[@inline] acts_eval_lit st (f:formula) : Solver_intf.lbool =
+    let a = create_atom st f in
+    eval_atom_ a
+
+  let[@inline] acts_mk_lit st ?default_pol f : unit =
+    ignore (create_atom ?default_pol st f : atom)
+
+  let[@inline] acts_mk_term st t : unit = make_term st t
+
+  let[@inline] current_slice st : _ Solver_intf.acts = {
+    Solver_intf.
+    acts_iter_assumptions=acts_iter st ~full:false st.th_head;
+    acts_eval_lit= acts_eval_lit st;
+    acts_mk_lit=acts_mk_lit st;
+    acts_mk_term=acts_mk_term st;
+    acts_add_clause = acts_add_clause st;
+    acts_propagate = acts_propagate st;
+    acts_raise_conflict=acts_raise st;
+    acts_add_decision_lit=acts_add_decision_lit st;
+  }
+
+  (* full slice, for [if_sat] final check *)
+  let[@inline] full_slice st : _ Solver_intf.acts = {
+    Solver_intf.
+    acts_iter_assumptions=acts_iter st ~full:true st.th_head;
+    acts_eval_lit= acts_eval_lit st;
+    acts_mk_lit=acts_mk_lit st;
+    acts_mk_term=acts_mk_term st;
+    acts_add_clause = acts_add_clause st;
+    acts_propagate = acts_propagate st;
+    acts_raise_conflict=acts_raise st;
+    acts_add_decision_lit=acts_add_decision_lit st;
+  }
+
+  (* Assert that the conflict is indeeed a conflict *)
+  let check_is_conflict_ (c:Clause.t) : unit =
+    if not @@ Array.for_all (Atom.is_false) c.atoms then (
+      invalid_argf "conflict should be false: %a" Clause.debug c
+    )
+
+  (* some boolean literals were decided/propagated within Msat. Now we
+     need to inform the theory of those assumptions, so it can do its job.
+     @return the conflict clause, if the theory detects unsatisfiability *)
+  let rec theory_propagate st : clause option =
+    assert (st.elt_head = Vec.size st.trail);
+    assert (st.th_head <= st.elt_head);
+    if st.th_head = st.elt_head then (
+      None (* fixpoint/no propagation *)
+    ) else (
+      let slice = current_slice st in
+      st.th_head <- st.elt_head; (* catch up *)
+      match Plugin.partial_check st.th slice with
+      | () ->
+        flush_clauses st;
+        propagate st
+      | exception Th_conflict c ->
+        check_is_conflict_ c;
+        Array.iter (fun a -> insert_elt_order st (Elt.of_var a.var)) c.atoms;
+        Some c
+    )
+
+  (* fixpoint between boolean propagation and theory propagation
+     @return a conflict clause, if any *)
+  and propagate (st:t) : clause option =
+    (* First, treat the stack of lemmas added by the theory, if any *)
+    flush_clauses st;
+    (* Now, check that the situation is sane *)
+    assert (st.elt_head <= Vec.size st.trail);
+    if st.elt_head = Vec.size st.trail then (
+      theory_propagate st
+    ) else (
+      match
+        while st.elt_head < Vec.size st.trail do
+          begin match Vec.get st.trail st.elt_head with
+            | Lit _ -> ()
+            | Atom a -> propagate_atom st a
+          end;
+          st.elt_head <- st.elt_head + 1;
+        done;
+      with
+      | () -> theory_propagate st
+      | exception Conflict c -> Some c
+    )
+
+  (* compute unsat core from assumption [a] *)
+  let analyze_final (self:t) (a:atom) : atom list =
+    Log.debugf 5 (fun k->k "(@[sat.analyze-final@ :lit %a@])" Atom.debug a);
+    assert (Atom.is_false a);
+    let core = ref [a] in
+    let idx = ref (Vec.size self.trail - 1) in
+    Var.mark a.var;
+    let seen = ref [a.var] in
+    while !idx >= 0 do
+      begin match Vec.get self.trail !idx with
+        | Lit _ -> () (* semantic decision, ignore *)
+        | Atom a' ->
+          if Var.marked a'.var then (
+            match Atom.reason a' with
+            | Some Semantic -> ()
+            | Some Decision -> core := a' :: !core
+            | Some (Bcp c | Bcp_lazy (lazy c)) ->
+              Array.iter
+                (fun a ->
+                   let v = a.var in
+                   if not @@ Var.marked v then (
+                     seen := v :: !seen;
+                     Var.mark v;
+                   ))
+                c.atoms
+            | None -> ()
+          );
+      end;
+      decr idx
+    done;
+    List.iter Var.unmark !seen;
+    Log.debugf 5 (fun k->k "(@[sat.analyze-final.done@ :core %a@])" (Format.pp_print_list Atom.debug) !core);
+    !core
+
+  (* remove some learnt clauses. *)
+  let reduce_db (st:t) (n_of_learnts: int) : unit =
+    let v = st.clauses_learnt in
+    Log.debugf 3 (fun k->k "(@[sat.gc.start :keep %d :out-of %d@])" n_of_learnts (Vec.size v));
+    assert (Vec.size v > n_of_learnts);
+    (* sort by decreasing activity *)
+    Vec.sort v (fun c1 c2 -> compare c2.activity c1.activity);
+    let n_collected = ref 0 in
+    while Vec.size v > n_of_learnts do
+      let c = Vec.pop v in
+      assert (Clause.removable c);
+      Clause.set_dead c;
+      assert (Clause.dead c);
+      incr n_collected;
+    done;
+    Log.debugf 3 (fun k->k "(@[sat.gc.done :collected %d@])" !n_collected);
+    ()
+
+  (* Decide on a new literal, and enqueue it into the trail *)
+  let rec pick_branch_aux st atom : unit =
+    let v = atom.var in
+    if v.v_level >= 0 then (
+      assert (v.pa.is_true || v.na.is_true);
+      pick_branch_lit st
+    ) else if Plugin.mcsat then (
+      match Plugin.eval st.th atom.lit with
+      | Solver_intf.Unknown ->
+        new_decision_level st;
+        let current_level = decision_level st in
+        enqueue_bool st atom ~level:current_level Decision;
+        (match st.on_decision with Some f -> f atom | None -> ());
+      | Solver_intf.Valued (b, l) ->
+        let a = if b then atom else atom.neg in
+        enqueue_semantic st a l
+    ) else (
+      new_decision_level st;
+      let current_level = decision_level st in
+      enqueue_bool st atom ~level:current_level Decision;
+      (match st.on_decision with Some f -> f atom | None -> ());
+    )
+
+  and pick_branch_lit st =
+    match st.next_decisions with
+    | atom :: tl ->
+      st.next_decisions <- tl;
+      pick_branch_aux st atom
+    | [] when decision_level st < Vec.size st.assumptions ->
+      (* use an assumption *)
+      let a = Vec.get st.assumptions (decision_level st) in
+      if Atom.is_true a then (
+        new_decision_level st; (* pseudo decision level, [a] is already true *)
+        pick_branch_lit st
+      ) else if Atom.is_false a then (
+        (* root conflict, find unsat core *)
+        let core = analyze_final st a in
+        raise (E_unsat (US_local {first=a; core}))
+      ) else (
+        pick_branch_aux st a
+      )
+    | [] ->
+      begin match H.remove_min st.order with
+        | E_lit l ->
+          if Lit.level l >= 0 then (
+            pick_branch_lit st
+          ) else (
+            let value = Plugin.assign st.th l.term in
+            new_decision_level st;
+            let current_level = decision_level st in
+            enqueue_assign st l value current_level
+          )
+        | E_var v ->
+          pick_branch_aux st (if Var.default_pol v then v.pa else v.na)
+        | exception Not_found -> raise_notrace E_sat
+      end
+
+  (* do some amount of search, until the number of conflicts or clause learnt
+     reaches the given parameters *)
+  let search (st:t) n_of_conflicts n_of_learnts : unit =
+    Log.debugf 3
+      (fun k->k "(@[sat.search@ :n-conflicts %d@ :n-learnt %d@])" n_of_conflicts n_of_learnts);
+    let conflictC = ref 0 in
+    while true do
+      match propagate st with
+      | Some confl -> (* Conflict *)
+        incr conflictC;
+        (* When the theory has raised Unsat, add_boolean_conflict
+           might 'forget' the initial conflict clause, and only add the
+           analyzed backtrack clause. So in those case, we use add_clause
+           to make sure the initial conflict clause is also added. *)
+        if Clause.attached confl then (
+          add_boolean_conflict st confl
+        ) else (
+          add_clause_ st confl
+        );
+        (match st.on_conflict with Some f -> f confl.atoms | None -> ());
+
+      | None -> (* No Conflict *)
+        assert (st.elt_head = Vec.size st.trail);
+        assert (st.elt_head = st.th_head);
+        if n_of_conflicts > 0 && !conflictC >= n_of_conflicts then (
+          Log.debug info "(sat.restarting)";
+          cancel_until st 0;
+          raise_notrace Restart
+        );
+        (* if decision_level() = 0 then simplify (); *)
+
+        if n_of_learnts > 0 &&
+           Vec.size st.clauses_learnt - Vec.size st.trail > n_of_learnts then (
+          reduce_db st n_of_learnts;
+        );
+
+        pick_branch_lit st
+    done
+
+  let eval_level (_st:t) (a:atom) =
+    let lvl = a.var.v_level in
+    if Atom.is_true a then (
+      assert (lvl >= 0);
+      true, lvl
+    ) else if Atom.is_false a then (
+      false, lvl
+    ) else (
+      raise UndecidedLit
+    )
+
+  let[@inline] eval st lit = fst @@ eval_level st lit
+
+  let[@inline] unsat_conflict st = st.unsat_at_0
+
+  let model (st:t) : (term * value) list =
+    let opt = function Some a -> a | None -> assert false in
+    Vec.fold
+      (fun acc e -> match e with
+         | Lit v -> (v.term, opt v.assigned)  :: acc
+         | Atom _ -> acc)
+      [] st.trail
+
+  (* fixpoint of propagation and decisions until a model is found, or a
+     conflict is reached *)
+  let solve_ (st:t) : unit =
+    Log.debugf 5 (fun k->k "(@[sat.solve :assms %d@])" (Vec.size st.assumptions));
+    check_unsat_ st;
+    try
+      flush_clauses st; (* add initial clauses *)
+      let n_of_conflicts = ref (float_of_int restart_first) in
+      let n_of_learnts = ref ((float_of_int (nb_clauses st)) *. learntsize_factor) in
+      while true do
+        begin try
+            search st (int_of_float !n_of_conflicts) (int_of_float !n_of_learnts)
+          with
+          | Restart ->
+            n_of_conflicts := !n_of_conflicts *. restart_inc;
+            n_of_learnts   := !n_of_learnts *. learntsize_inc
+          | E_sat ->
+            assert (st.elt_head = Vec.size st.trail &&
+                    Vec.is_empty st.clauses_to_add &&
+                    st.next_decisions=[]);
+            begin match Plugin.final_check st.th (full_slice st) with
+              | () ->
+                if st.elt_head = Vec.size st.trail &&
+                   Vec.is_empty st.clauses_to_add &&
+                   st.next_decisions = []
+                then (
+                  raise_notrace E_sat
+                );
+                (* otherwise, keep on *)
+                flush_clauses st;
+              | exception Th_conflict c ->
+                check_is_conflict_ c;
+                Array.iter (fun a -> insert_elt_order st (Elt.of_var a.var)) c.atoms;
+                Log.debugf info (fun k -> k "(@[sat.theory-conflict-clause@ %a@])" Clause.debug c);
+                (match st.on_conflict with Some f -> f c.atoms | None -> ());
+                Vec.push st.clauses_to_add c;
+                flush_clauses st;
+            end;
+        end
+      done
+    with E_sat -> ()
+
+  let assume st cnf lemma =
+    List.iter
+      (fun l ->
+         let atoms = List.rev_map (mk_atom st) l in
+         let c = Clause.make_permanent atoms (Hyp lemma) in
+         Log.debugf debug (fun k -> k "(@[sat.assume-clause@ @[<hov 2>%a@]@])" Clause.debug c);
+         Vec.push st.clauses_to_add c)
+      cnf
+
+  (* Check satisfiability *)
+  let check_clause c =
+    let res = Array.exists (fun a -> a.is_true) c.atoms in
+    if not res then (
+      Log.debugf debug
+        (fun k -> k "(@[sat.check-clause@ :not-satisfied @[<hov>%a@]@])" Clause.debug c);
+      false
+    ) else
+      true
+
+  let check_vec v = Vec.for_all check_clause v
+  let check st : bool =
+    Vec.is_empty st.clauses_to_add &&
+    check_vec st.clauses_hyps &&
+    check_vec st.clauses_learnt
+
+  let[@inline] theory st = st.th
+
+  (* Unsafe access to internal data *)
+
+  let hyps env = env.clauses_hyps
+
+  let history env = env.clauses_learnt
+
+  let trail env = env.trail
+
+  (* Result type *)
+  type res =
+    | Sat of (term,Formula.t,value) Solver_intf.sat_state
+    | Unsat of (atom,clause,Proof.t) Solver_intf.unsat_state
+
+  let pp_all st lvl status =
+    Log.debugf lvl
+      (fun k -> k
+          "(@[<v>sat.full-state :res %s - Full summary:@,@[<hov 2>Trail:@\n%a@]@,\
+           @[<hov 2>Hyps:@\n%a@]@,@[<hov 2>Lemmas:@\n%a@]@,@]@."
+          status
+          (Vec.pp ~sep:"" Trail_elt.debug) (trail st)
+          (Vec.pp ~sep:"" Clause.debug) (hyps st)
+          (Vec.pp ~sep:"" Clause.debug) (history st)
+      )
+
+  let mk_sat (st:t) : (Term.t, Formula.t, _) Solver_intf.sat_state =
+    pp_all st 99 "SAT";
+    let t = trail st in
+    let iter_trail f f' =
+      Vec.iter (function
+          | Atom a -> f (Atom.formula a)
+          | Lit l -> f' l.term)
+        t
+    in
+    let[@inline] eval f = eval st (mk_atom st f) in
+    let[@inline] eval_level f = eval_level st (mk_atom st f) in
+    { Solver_intf.
+      eval; eval_level; iter_trail;
+      model = (fun () -> model st);
+    }
+
+  let mk_unsat (st:t) (us: unsat_cause) : _ Solver_intf.unsat_state =
+    pp_all st 99 "UNSAT";
+    let unsat_assumptions () = match us with
+      | US_local {first=_; core} -> core
+      | _ -> []
+    in
+    let unsat_conflict = match us with
+      | US_false c -> fun() -> c
+      | US_local {core=[]; _} -> assert false
+      | US_local {first; core} ->
+        let c = lazy (
+          let core = List.rev core in (* increasing trail order *)
+          assert (Atom.equal first @@ List.hd core);
+          let proof_of (a:atom) = match Atom.reason a with
+            | Some (Decision | Semantic) -> Clause.make_removable [a] Local
+            | Some (Bcp c | Bcp_lazy (lazy c)) -> c
+            | None -> assert false
+          in
+          let other_lits = List.filter (fun a -> not (Atom.equal a first)) core in
+          let hist =
+            Clause.make_permanent [first] Local ::
+            proof_of first ::
+            List.map proof_of other_lits in
+          Clause.make_permanent [] (History hist)
+        ) in
+        fun () -> Lazy.force c
+    in
+    let get_proof () =
+      let c = unsat_conflict () in
+      Proof.prove c
+    in
+    { Solver_intf.unsat_conflict; get_proof; unsat_assumptions; }
+
+  let add_clause_a st c lemma : unit =
+    try
+      let c = Clause.make_a ~flags:0 c (Hyp lemma) in
+      add_clause_ st c
+    with
+    | E_unsat (US_false c) ->
+      st.unsat_at_0 <- Some c
+
+  let add_clause st c lemma : unit =
+    try
+      let c = Clause.make_permanent c (Hyp lemma) in
+      add_clause_ st c
+    with
+    | E_unsat (US_false c) ->
+      st.unsat_at_0 <- Some c
+
+  let solve ?(assumptions=[]) (st:t) : res =
+    cancel_until st 0;
+    Vec.clear st.assumptions;
+    List.iter (Vec.push st.assumptions) assumptions;
+    try
+      solve_ st;
+      Sat (mk_sat st)
+    with E_unsat us ->
+      Unsat (mk_unsat st us)
+
+  let true_at_level0 st a =
+    try
+      let b, lev = eval_level st a in
+      b && lev = 0
+    with UndecidedLit -> false
+
+  let[@inline] eval_atom _st a : Solver_intf.lbool = eval_atom_ a
+
+  let export (st:t) : clause Solver_intf.export =
+    let hyps = hyps st in
+    let history = history st in
+    {Solver_intf.hyps; history; }
+end
+[@@inline][@@specialise]
+
+  module Void_ = struct
+    type t = Solver_intf.void
+    let equal _ _ = assert false
+    let hash _ =  assert false
+    let pp _ _ = assert false
+  end
+
+module Make_cdcl_t(Plugin : Solver_intf.PLUGIN_CDCL_T) =
+  Make(struct
+    include Plugin
+    module Term = Void_
+    module Value = Void_
+    let eval _ _ = Solver_intf.Unknown
+    let assign _ t = t
+    let mcsat = false
+    let has_theory = true
+    let iter_assignable _ _ _ = ()
+  end)
+[@@inline][@@specialise]
+
+module Make_mcsat(Plugin : Solver_intf.PLUGIN_MCSAT) =
+  Make(struct
+    include Plugin
+    let mcsat = true
+    let has_theory = false
+  end)
+[@@inline][@@specialise]
+
+module Make_pure_sat(Plugin : Solver_intf.PLUGIN_SAT) =
+  Make(struct
+  module Formula = Plugin.Formula
+  module Term = Void_
+  module Value = Void_
+  type t = unit
+  type proof = Plugin.proof
+  let push_level () = ()
+  let pop_levels _ _ = ()
+  let partial_check () _ = ()
+  let final_check () _ = ()
+  let eval () _ = Solver_intf.Unknown
+  let assign () t = t
+  let mcsat = false
+  let has_theory = false
+  let iter_assignable () _ _ = ()
+  let mcsat = false
+end)
+[@@inline][@@specialise]
+
diff --git a/src/sat/src/core/Log.ml b/src/sat/src/core/Log.ml
new file mode 100644
index 00000000..f60603ea
--- /dev/null
+++ b/src/sat/src/core/Log.ml
@@ -0,0 +1,33 @@
+(*
+MSAT is free software, using the Apache license, see file LICENSE
+Copyright 2014 Guillaume Bury
+Copyright 2014 Simon Cruanes
+*)
+
+(** {1 Logging functions, real version} *)
+
+let enabled = true (* NOTE: change here for 0-overhead *)
+
+let debug_level_ = ref 0
+let set_debug l = debug_level_ := l
+let get_debug () = !debug_level_
+
+let debug_fmt_ = ref Format.err_formatter
+
+let set_debug_out f = debug_fmt_ := f
+
+(* does the printing, inconditionally *)
+let debug_real_ l k =
+  k (fun fmt ->
+    Format.fprintf !debug_fmt_ "@[<2>@{<Blue>[%d|%.3f]@}@ "
+      l (Sys.time());
+    Format.kfprintf
+      (fun fmt -> Format.fprintf fmt "@]@.")
+      !debug_fmt_ fmt)
+
+let[@inline] debugf l k =
+  if enabled && l <= !debug_level_ then (
+    debug_real_ l k;
+  )
+
+let[@inline] debug l msg = debugf l (fun k->k "%s" msg)
diff --git a/src/sat/src/core/Log.mli b/src/sat/src/core/Log.mli
new file mode 100644
index 00000000..8923f8e3
--- /dev/null
+++ b/src/sat/src/core/Log.mli
@@ -0,0 +1,26 @@
+(*
+MSAT is free software, using the Apache license, see file LICENSE
+Copyright 2014 Guillaume Bury
+Copyright 2014 Simon Cruanes
+*)
+
+(** {1 Logging function, for debugging} *)
+
+val enabled : bool
+
+val set_debug : int -> unit (** Set debug level *)
+val get_debug : unit -> int (** Current debug level *)
+
+val debugf :
+  int ->
+  ((('a, Format.formatter, unit, unit) format4 -> 'a) -> unit) ->
+  unit
+(** Emit a debug message at the given level. If the level is lower
+    than [get_debug ()], the message will indeed be emitted *)
+
+val debug : int -> string -> unit
+(** Simpler version of {!debug}, without formatting *)
+
+val set_debug_out : Format.formatter -> unit
+(** Change the output formatter. *)
+
diff --git a/src/sat/src/core/Msat.ml b/src/sat/src/core/Msat.ml
new file mode 100644
index 00000000..fb049615
--- /dev/null
+++ b/src/sat/src/core/Msat.ml
@@ -0,0 +1,76 @@
+(** Main API *)
+
+
+module Solver_intf = Solver_intf
+
+module type S = Solver_intf.S
+module type FORMULA = Solver_intf.FORMULA
+module type EXPR = Solver_intf.EXPR
+module type PLUGIN_CDCL_T = Solver_intf.PLUGIN_CDCL_T
+module type PLUGIN_MCSAT = Solver_intf.PLUGIN_MCSAT
+module type PROOF = Solver_intf.PROOF
+
+(** Empty type *)
+type void = (unit,bool) Solver_intf.gadt_eq
+
+type lbool = Solver_intf.lbool = L_true | L_false | L_undefined
+
+type ('term, 'form, 'value) sat_state = ('term, 'form, 'value) Solver_intf.sat_state = {
+  eval : 'form -> bool;
+  eval_level : 'form -> bool * int;
+  iter_trail : ('form -> unit) -> ('term -> unit) -> unit;
+  model : unit -> ('term * 'value) list;
+}
+
+type ('atom,'clause, 'proof) unsat_state = ('atom,'clause, 'proof) Solver_intf.unsat_state = {
+  unsat_conflict : unit -> 'clause;
+  get_proof : unit -> 'proof;
+  unsat_assumptions: unit -> 'atom list;
+}
+type 'clause export = 'clause Solver_intf.export = {
+  hyps : 'clause Vec.t;
+  history : 'clause Vec.t;
+}
+
+type ('term, 'formula, 'value) assumption = ('term, 'formula, 'value) Solver_intf.assumption =
+  | Lit of 'formula  (** The given formula is asserted true by the solver *)
+  | Assign of 'term * 'value (** The term is assigned to the value *)
+
+type ('term, 'formula, 'proof) reason = ('term, 'formula, 'proof) Solver_intf.reason =
+  | Eval of 'term list
+  | Consequence of (unit -> 'formula list * 'proof)
+
+type ('term, 'formula, 'value, 'proof) acts = ('term, 'formula, 'value, 'proof) Solver_intf.acts = {
+  acts_iter_assumptions: (('term,'formula,'value) assumption -> unit) -> unit;
+  acts_eval_lit: 'formula -> lbool;
+  acts_mk_lit: ?default_pol:bool -> 'formula -> unit;
+  acts_mk_term: 'term -> unit;
+  acts_add_clause : ?keep:bool -> 'formula list -> 'proof -> unit;
+  acts_raise_conflict: 'b. 'formula list -> 'proof -> 'b;
+  acts_propagate : 'formula -> ('term, 'formula, 'proof) reason -> unit;
+  acts_add_decision_lit: 'formula -> bool -> unit;
+}
+
+type negated = Solver_intf.negated = Negated | Same_sign
+
+(** Print {!negated} values *)
+let pp_negated out = function
+  | Negated -> Format.fprintf out "negated"
+  | Same_sign -> Format.fprintf out "same-sign"
+
+(** Print {!lbool} values *)
+let pp_lbool out = function
+  | L_true -> Format.fprintf out "true"
+  | L_false -> Format.fprintf out "false"
+  | L_undefined -> Format.fprintf out "undefined"
+
+exception No_proof = Solver_intf.No_proof
+
+module Make_mcsat = Solver.Make_mcsat
+module Make_cdcl_t = Solver.Make_cdcl_t
+module Make_pure_sat = Solver.Make_pure_sat
+
+(**/**)
+module Vec = Vec
+module Log = Log
+(**/**)
diff --git a/src/sat/src/core/Solver.ml b/src/sat/src/core/Solver.ml
new file mode 100644
index 00000000..5863de2a
--- /dev/null
+++ b/src/sat/src/core/Solver.ml
@@ -0,0 +1,12 @@
+(*
+MSAT is free software, using the Apache license, see file LICENSE
+Copyright 2016 Guillaume Bury
+Copyright 2016 Simon Cruanes
+*)
+
+module type S = Solver_intf.S
+
+module Make_cdcl_t = Internal.Make_cdcl_t
+module Make_mcsat = Internal.Make_mcsat
+module Make_pure_sat = Internal.Make_pure_sat
+
diff --git a/src/sat/src/core/Solver.mli b/src/sat/src/core/Solver.mli
new file mode 100644
index 00000000..b256a4a8
--- /dev/null
+++ b/src/sat/src/core/Solver.mli
@@ -0,0 +1,34 @@
+(*
+MSAT is free software, using the Apache license, see file LICENSE
+Copyright 2014 Guillaume Bury
+Copyright 2014 Simon Cruanes
+*)
+
+(** mSAT safe interface
+
+    This module defines a safe interface for the core solver.
+    It is the basis of the {!module:Solver} and {!module:Mcsolver} modules.
+*)
+
+module type S = Solver_intf.S
+(** Safe external interface of solvers. *)
+
+module Make_cdcl_t(Th : Solver_intf.PLUGIN_CDCL_T)
+  : S with type Term.t = Solver_intf.void
+       and module Formula = Th.Formula
+       and type lemma = Th.proof
+       and type theory = Th.t
+
+module Make_mcsat(Th : Solver_intf.PLUGIN_MCSAT)
+  : S with module Term = Th.Term
+       and module Formula = Th.Formula
+       and type lemma = Th.proof
+       and type theory = Th.t
+
+module Make_pure_sat(Th: Solver_intf.PLUGIN_SAT)
+  : S with type Term.t = Solver_intf.void
+       and module Formula = Th.Formula
+       and type lemma = Th.proof
+       and type theory = unit
+
+
diff --git a/src/sat/src/core/Solver_intf.ml b/src/sat/src/core/Solver_intf.ml
new file mode 100644
index 00000000..ab375a4d
--- /dev/null
+++ b/src/sat/src/core/Solver_intf.ml
@@ -0,0 +1,514 @@
+(*
+MSAT is free software, using the Apache license, see file LICENSE
+Copyright 2016 Guillaume Bury
+Copyright 2016 Simon Cruanes
+*)
+
+(** Interface for Solvers
+
+    This modules defines the safe external interface for solvers.
+    Solvers that implements this interface can be obtained using the [Make]
+    functor in {!Solver} or {!Mcsolver}.
+*)
+
+type 'a printer = Format.formatter -> 'a -> unit
+
+type ('term, 'form, 'value) sat_state = {
+  eval: 'form -> bool;
+  (** Returns the valuation of a formula in the current state
+      of the sat solver.
+      @raise UndecidedLit if the literal is not decided *)
+  eval_level: 'form -> bool * int;
+  (** Return the current assignement of the literals, as well as its
+      decision level. If the level is 0, then it is necessary for
+      the atom to have this value; otherwise it is due to choices
+      that can potentially be backtracked.
+      @raise UndecidedLit if the literal is not decided *)
+  iter_trail : ('form -> unit) -> ('term -> unit) -> unit;
+  (** Iter thorugh the formulas and terms in order of decision/propagation
+      (starting from the first propagation, to the last propagation). *)
+  model: unit -> ('term * 'value) list;
+  (** Returns the model found if the formula is satisfiable. *)
+}
+(** The type of values returned when the solver reaches a SAT state. *)
+
+type ('atom, 'clause, 'proof) unsat_state = {
+  unsat_conflict : unit -> 'clause;
+  (** Returns the unsat clause found at the toplevel *)
+  get_proof : unit -> 'proof;
+  (** returns a persistent proof of the empty clause from the Unsat result. *)
+  unsat_assumptions: unit -> 'atom list;
+  (** Subset of assumptions responsible for "unsat" *)
+}
+(** The type of values returned when the solver reaches an UNSAT state. *)
+
+type 'clause export = {
+  hyps: 'clause Vec.t;
+  history: 'clause Vec.t;
+}
+(** Export internal state *)
+
+type negated =
+  | Negated     (** changed sign *)
+  | Same_sign   (** kept sign *)
+(** This type is used during the normalisation of formulas.
+    See {!val:Expr_intf.S.norm} for more details. *)
+
+type 'term eval_res =
+  | Unknown                       (** The given formula does not have an evaluation *)
+  | Valued of bool * ('term list) (** The given formula can be evaluated to the given bool.
+                                      The list of terms to give is the list of terms that
+                                      were effectively used for the evaluation. *)
+(** The type of evaluation results for a given formula.
+    For instance, let's suppose we want to evaluate the formula [x * y = 0], the
+    following result are correct:
+    - [Unknown] if neither [x] nor [y] are assigned to a value
+    - [Valued (true, [x])] if [x] is assigned to [0]
+    - [Valued (true, [y])] if [y] is assigned to [0]
+    - [Valued (false, [x; y])] if [x] and [y] are assigned to 1 (or any non-zero number)
+*)
+
+type ('term, 'formula, 'value) assumption =
+  | Lit of 'formula  (** The given formula is asserted true by the solver *)
+  | Assign of 'term * 'value (** The term is assigned to the value *)
+(** Asusmptions made by the core SAT solver. *)
+
+type ('term, 'formula, 'proof) reason =
+  | Eval of 'term list
+  (** The formula can be evalutaed using the terms in the list *)
+  | Consequence of (unit -> 'formula list * 'proof)
+  (** [Consequence (l, p)] means that the formulas in [l] imply the propagated
+      formula [f]. The proof should be a proof of the clause "[l] implies [f]".
+
+      invariant: in [Consequence (fun () -> l,p)], all elements of [l] must be true in
+      the current trail.
+
+      {b note} on lazyiness: the justification is suspended (using [unit -> …])
+      to avoid potentially costly computations that might never be used
+      if this literal is backtracked without participating in a conflict.
+      Therefore the function that produces [(l,p)] needs only be safe in
+      trails (partial models) that are conservative extensions of the current
+      trail.
+      If the theory isn't robust w.r.t. extensions of the trail (e.g. if
+      its internal state undergoes significant changes),
+      it can be easier to produce the explanation eagerly when
+      propagating, and then use [Consequence (fun () -> expl, proof)] with
+      the already produced [(expl,proof)] tuple.
+  *)
+(** The type of reasons for propagations of a formula [f]. *)
+
+type lbool = L_true | L_false | L_undefined
+(** Valuation of an atom *)
+
+(* TODO: find a way to use atoms instead of formulas here *)
+type ('term, 'formula, 'value, 'proof) acts = {
+  acts_iter_assumptions: (('term,'formula,'value) assumption -> unit) -> unit;
+  (** Traverse the new assumptions on the boolean trail. *)
+
+  acts_eval_lit: 'formula -> lbool;
+  (** Obtain current value of the given literal *)
+
+  acts_mk_lit: ?default_pol:bool -> 'formula -> unit;
+  (** Map the given formula to a literal, which will be decided by the
+      SAT solver. *)
+
+  acts_mk_term: 'term -> unit;
+  (** Map the given term (and its subterms) to decision variables,
+      for the MCSAT solver to decide. *)
+
+  acts_add_clause: ?keep:bool -> 'formula list -> 'proof -> unit;
+  (** Add a clause to the solver.
+      @param keep if true, the clause will be kept by the solver.
+        Otherwise the solver is allowed to GC the clause and propose this
+        partial model again.
+  *)
+
+  acts_raise_conflict: 'b. 'formula list -> 'proof -> 'b;
+  (** Raise a conflict, yielding control back to the solver.
+      The list of atoms must be a valid theory lemma that is false in the
+      current trail. *)
+
+  acts_propagate: 'formula -> ('term, 'formula, 'proof) reason -> unit;
+  (** Propagate a formula, i.e. the theory can evaluate the formula to be true
+      (see the definition of {!type:eval_res} *)
+
+  acts_add_decision_lit: 'formula -> bool -> unit;
+  (** Ask the SAT solver to decide on the given formula with given sign
+      before it can answer [SAT]. The order of decisions is still unspecified.
+      Useful for theory combination. This will be undone on backtracking. *)
+}
+(** The type for a slice of assertions to assume/propagate in the theory. *)
+
+type ('a, 'b) gadt_eq = GADT_EQ : ('a, 'a) gadt_eq
+
+type void = (unit,bool) gadt_eq
+(** A provably empty type *)
+
+exception No_proof
+
+module type FORMULA = sig
+  (** formulas *)
+
+  type t
+  (** The type of atomic formulas over terms. *)
+
+  val equal : t -> t -> bool
+  (** Equality over formulas. *)
+
+  val hash : t -> int
+  (** Hashing function for formulas. Should be such that two formulas equal according
+      to {!val:Expr_intf.S.equal} have the same hash. *)
+
+  val pp : t printer
+  (** Printing function used among other thing for debugging.  *)
+
+  val neg : t -> t
+  (** Formula negation *)
+
+  val norm : t -> t * negated
+  (** Returns a 'normalized' form of the formula, possibly negated
+      (in which case return [Negated]).
+      [norm] must be so that [a] and [neg a] normalise to the same formula,
+      but one returns [Negated] and the other [Same_sign]. *)
+end
+
+(** Formulas and Terms required for mcSAT *)
+module type EXPR = sig
+  type proof
+  (** An abstract type for proofs *)
+
+  module Term : sig
+    type t
+    (** The type of terms *)
+
+    val equal : t -> t -> bool
+    (** Equality over terms. *)
+
+    val hash : t -> int
+    (** Hashing function for terms. Should be such that two terms equal according
+        to {!equal} have the same hash. *)
+
+    val pp : t printer
+    (** Printing function used among other for debugging. *)
+  end
+
+  module Value : sig
+    type t
+    (** The type of semantic values (domain elements) *)
+
+    val pp : t printer
+    (** Printing function used among other for debugging. *)
+  end
+
+  module Formula : FORMULA
+end
+
+(** Signature for theories to be given to the CDCL(T) solver *)
+module type PLUGIN_CDCL_T = sig
+  type t
+  (** The plugin state itself *)
+
+  module Formula : FORMULA
+
+  type proof
+
+  val push_level : t -> unit
+  (** Create a new backtrack level *)
+
+  val pop_levels : t -> int -> unit
+  (** Pop [n] levels of the theory *)
+
+  val partial_check : t -> (void, Formula.t, void, proof) acts -> unit
+  (** Assume the formulas in the slice, possibly using the [slice]
+      to push new formulas to be propagated or to raising a conflict or to add
+      new lemmas. *)
+
+  val final_check : t -> (void, Formula.t, void, proof) acts -> unit
+  (** Called at the end of the search in case a model has been found.
+      If no new clause is pushed, then proof search ends and "sat" is returned;
+      if lemmas are added, search is resumed;
+      if a conflict clause is added, search backtracks and then resumes. *)
+end
+
+(** Signature for theories to be given to the Model Constructing Solver. *)
+module type PLUGIN_MCSAT = sig
+  type t
+  (** The plugin state itself *)
+
+  include EXPR
+
+  val push_level : t -> unit
+  (** Create a new backtrack level *)
+
+  val pop_levels : t -> int -> unit
+  (** Pop [n] levels of the theory *)
+
+  val partial_check : t -> (Term.t, Formula.t, Value.t, proof) acts -> unit
+  (** Assume the formulas in the slice, possibly using the [slice]
+      to push new formulas to be propagated or to raising a conflict or to add
+      new lemmas. *)
+
+  val final_check : t -> (Term.t, Formula.t, Value.t, proof) acts -> unit
+  (** Called at the end of the search in case a model has been found.
+      If no new clause is pushed, then proof search ends and "sat" is returned;
+      if lemmas are added, search is resumed;
+      if a conflict clause is added, search backtracks and then resumes. *)
+
+  val assign : t -> Term.t -> Value.t
+  (** Returns an assignment value for the given term. *)
+
+  val iter_assignable : t -> (Term.t -> unit) -> Formula.t -> unit
+  (** An iterator over the subTerm.ts of a Formula.t that should be assigned a value (usually the poure subTerm.ts) *)
+
+  val eval : t -> Formula.t -> Term.t eval_res
+  (** Returns the evaluation of the Formula.t in the current assignment *)
+end
+
+(** Signature for pure SAT solvers *)
+module type PLUGIN_SAT = sig
+  module Formula : FORMULA
+
+  type proof
+end
+
+module type PROOF = sig
+  (** Signature for a module handling proof by resolution from sat solving traces *)
+
+  (** {3 Type declarations} *)
+
+  exception Resolution_error of string
+  (** Raised when resolution failed. *)
+
+  type formula
+  type atom
+  type lemma
+  type clause
+  (** Abstract types for atoms, clauses and theory-specific lemmas *)
+
+  type t
+  (** Lazy type for proof trees. Proofs are persistent objects, and can be
+      extended to proof nodes using functions defined later. *)
+
+  and proof_node = {
+    conclusion : clause;  (** The conclusion of the proof *)
+    step : step;          (** The reasoning step used to prove the conclusion *)
+  }
+  (** A proof can be expanded into a proof node, which show the first step of the proof. *)
+
+  (** The type of reasoning steps allowed in a proof. *)
+  and step =
+    | Hypothesis of lemma
+    (** The conclusion is a user-provided hypothesis *)
+    | Assumption
+    (** The conclusion has been locally assumed by the user *)
+    | Lemma of lemma
+    (** The conclusion is a tautology provided by the theory, with associated proof *)
+    | Duplicate of t * atom list
+    (** The conclusion is obtained by eliminating multiple occurences of the atom in
+        the conclusion of the provided proof. *)
+    | Hyper_res of hyper_res_step
+
+  and hyper_res_step = {
+    hr_init: t;
+    hr_steps: (atom * t) list; (* list of pivot+clause to resolve against [init] *)
+  }
+
+  (** {3 Proof building functions} *)
+
+  val prove : clause -> t
+  (** Given a clause, return a proof of that clause.
+      @raise Resolution_error if it does not succeed. *)
+
+  val prove_unsat : clause -> t
+  (** Given a conflict clause [c], returns a proof of the empty clause.
+      @raise Resolution_error if it does not succeed. *)
+
+  val prove_atom : atom -> t option
+  (** Given an atom [a], returns a proof of the clause [[a]] if [a] is true at level 0 *)
+
+  val res_of_hyper_res : hyper_res_step -> t * t * atom
+  (** Turn an hyper resolution step into a resolution step.
+      The conclusion can be deduced by performing a resolution between the conclusions
+      of the two given proofs.
+      The atom on which to perform the resolution is also given. *)
+
+  (** {3 Proof Nodes} *)
+
+  val parents : step -> t list
+  (** Returns the parents of a proof node. *)
+
+  val is_leaf : step -> bool
+  (** Returns wether the the proof node is a leaf, i.e. an hypothesis,
+      an assumption, or a lemma.
+      [true] if and only if {!parents} returns the empty list. *)
+
+  val expl : step -> string
+  (** Returns a short string description for the proof step; for instance
+      ["hypothesis"] for a [Hypothesis]
+      (it currently returns the variant name in lowercase). *)
+
+
+  (** {3 Proof Manipulation} *)
+
+  val expand : t -> proof_node
+  (** Return the proof step at the root of a given proof. *)
+
+  val conclusion : t -> clause
+  (** What is proved at the root of the clause *)
+
+  val fold : ('a -> proof_node -> 'a) -> 'a -> t -> 'a
+  (** [fold f acc p], fold [f] over the proof [p] and all its node. It is guaranteed that
+      [f] is executed exactly once on each proof node in the tree, and that the execution of
+      [f] on a proof node happens after the execution on the parents of the nodes. *)
+
+  val unsat_core : t -> clause list
+  (** Returns the unsat_core of the given proof, i.e the lists of conclusions
+      of all leafs of the proof.
+      More efficient than using the [fold] function since it has
+      access to the internal representation of proofs *)
+
+  (** {3 Misc} *)
+
+  val check_empty_conclusion : t -> unit
+  (** Check that the proof's conclusion is the empty clause,
+      @raise Resolution_error otherwise *)
+
+  val check : t -> unit
+  (** Check the contents of a proof. Mainly for internal use. *)
+
+  module Tbl : Hashtbl.S with type key = t
+end
+
+(** 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. *)
+
+  include EXPR
+
+  type term = Term.t (** user terms *)
+
+  type formula = Formula.t (** user formulas *)
+
+  type atom
+  (** The type of atoms given by the module argument for formulas.
+      An atom is a user-defined atomic formula whose truth value is
+      picked by Msat. *)
+
+  type clause
+
+  type theory
+
+  type lemma
+  (** A theory lemma or an input axiom *)
+
+  type solver
+
+  module Atom : sig
+    type t = atom
+
+    val equal : t -> t -> bool
+    val compare : t -> t -> int
+    val hash : t -> int
+    val neg : t -> t
+    val sign : t -> bool
+    val abs : t -> t
+    val formula : t -> formula
+    val pp : t printer
+  end
+
+  module Clause : sig
+    type t = clause
+
+    val atoms : t -> atom array
+    val atoms_l : t -> atom list
+    val equal : t -> t -> bool
+    val name : t -> string
+
+    val pp : t printer
+
+    module Tbl : Hashtbl.S with type key = t
+  end
+
+  module Proof : PROOF
+    with type clause = clause
+     and type atom = atom
+     and type formula = formula
+     and type lemma = lemma
+     and type t = proof
+  (** A module to manipulate proofs. *)
+
+  type t = solver
+  (** Main solver type, containing all state for solving. *)
+
+  val create :
+    ?on_conflict:(atom array -> unit) ->
+    ?on_decision:(atom -> unit) ->
+    ?on_new_atom:(atom -> unit) ->
+    ?store_proof:bool ->
+    ?size:[`Tiny|`Small|`Big] ->
+    theory ->
+    t
+  (** Create new solver
+      @param theory the theory
+      @param store_proof if true, stores proof (default [true]). Otherwise
+        the functions that return proofs will fail with [No_proof]
+      @param size the initial size of internal data structures. The bigger,
+        the faster, but also the more RAM it uses. *)
+
+  val theory : t -> theory
+  (** Access the theory state *)
+
+  (** {2 Types} *)
+
+  (** Result type for the solver *)
+  type res =
+    | Sat of (term,formula,Value.t) sat_state (** Returned when the solver reaches SAT, with a model *)
+    | Unsat of (atom,clause,Proof.t) unsat_state (** Returned when the solver reaches UNSAT, with a proof *)
+
+  exception UndecidedLit
+  (** Exception raised by the evaluating functions when a literal
+      has not yet been assigned a value. *)
+
+  (** {2 Base operations} *)
+
+  val assume : t -> formula list list -> lemma -> unit
+  (** Add the list of clauses to the current set of assumptions.
+      Modifies the sat solver state in place. *)
+
+  val add_clause : t -> atom list -> lemma -> unit
+  (** Lower level addition of clauses *)
+
+  val add_clause_a : t -> atom array -> lemma -> unit
+  (** Lower level addition of clauses *)
+
+  val solve :
+    ?assumptions:atom list ->
+    t -> res
+  (** Try and solves the current set of clauses.
+      @param assumptions additional atomic assumptions to be temporarily added.
+        The assumptions are just used for this call to [solve], they are
+        not saved in the solver's state. *)
+
+  val make_term : t -> term -> unit
+  (** Add a new term (i.e. decision variable) to the solver. This term will
+      be decided on at some point during solving, wether it appears
+      in clauses or not. *)
+
+  val make_atom : t -> formula -> atom
+  (** Add a new atom (i.e propositional formula) to the solver.
+      This formula will be decided on at some point during solving,
+      wether it appears in clauses or not. *)
+
+  val true_at_level0 : t -> atom -> bool
+  (** [true_at_level0 a] returns [true] if [a] was proved at level0, i.e.
+      it must hold in all models *)
+
+  val eval_atom : t -> atom -> lbool
+  (** Evaluate atom in current state *)
+
+  val export : t -> clause export
+end
+
diff --git a/src/sat/src/core/Vec.ml b/src/sat/src/core/Vec.ml
new file mode 100644
index 00000000..782a8b6a
--- /dev/null
+++ b/src/sat/src/core/Vec.ml
@@ -0,0 +1,113 @@
+
+type 'a t = {
+  mutable data : 'a array;
+  mutable sz : int;
+}
+
+let make n x = {data=Array.make n x; sz=0}
+
+let[@inline] create () = {data = [||]; sz = 0}
+
+let[@inline] clear s = s.sz <- 0
+
+let[@inline] shrink t i =
+  assert (i >= 0);
+  assert (i<=t.sz);
+  t.sz <- i
+
+let[@inline] pop t =
+  if t.sz = 0 then invalid_arg "vec.pop";
+  let x = Array.unsafe_get t.data (t.sz - 1) in
+  t.sz <- t.sz - 1;
+  x
+
+let[@inline] size t = t.sz
+
+let[@inline] is_empty t = t.sz = 0
+
+let[@inline] is_full t = Array.length t.data = t.sz
+
+let[@inline] copy t : _ t =
+  let data = Array.copy t.data in
+  {t with data}
+
+(* grow the array *)
+let[@inline never] grow_to_double_size t x : unit =
+  if Array.length t.data = Sys.max_array_length then (
+    failwith "vec: cannot resize";
+  );
+  let size =
+    min Sys.max_array_length (max 4 (2 * Array.length t.data))
+  in
+  let arr' = Array.make size x in
+  Array.blit t.data 0 arr' 0 (Array.length t.data);
+  t.data <- arr';
+  assert (Array.length t.data > t.sz);
+  ()
+
+let[@inline] push t x : unit =
+  if is_full t then grow_to_double_size t x;
+  Array.unsafe_set t.data t.sz x;
+  t.sz <- t.sz + 1
+
+let[@inline] get t i =
+  if i < 0 || i >= t.sz then invalid_arg "vec.get";
+  Array.unsafe_get t.data i
+
+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[@inline] fast_remove t i =
+  assert (i>= 0 && i < t.sz);
+  Array.unsafe_set t.data i @@ Array.unsafe_get 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 (Array.unsafe_get vec.data !i) then incr i else fast_remove vec !i
+  done
+
+let sort t f : unit =
+  let sub_arr = if is_full t then t.data else Array.sub t.data 0 t.sz in
+  Array.fast_sort f sub_arr;
+  t.data <- sub_arr
+
+let[@inline] iter f t =
+  for i = 0 to size t - 1 do
+    f (Array.unsafe_get t.data i)
+  done
+
+let[@inline] iteri f t =
+  for i = 0 to size t - 1 do
+    f i (Array.unsafe_get t.data i)
+  done
+
+let[@inline] to_seq a k = iter k a
+
+let exists p t = Iter.exists p @@ to_seq t
+let for_all p t = Iter.for_all p @@ to_seq t
+let fold f acc a = Iter.fold f acc @@ to_seq a
+let to_list a = Iter.to_list @@ to_seq a
+let to_array a = Array.sub a.data 0 a.sz
+
+let of_list l : _ t =
+  match l with
+  | [] -> create()
+  | x :: tl ->
+    let v = make (List.length tl+1) x in
+    List.iter (push v) l;
+    v
+
+let pp ?(sep=", ") pp out v =
+  let first = ref true in
+  iter
+    (fun x ->
+       if !first then first := false else Format.fprintf out "%s@," sep;
+       pp out x)
+    v
diff --git a/src/sat/src/core/Vec.mli b/src/sat/src/core/Vec.mli
new file mode 100644
index 00000000..d51a2b69
--- /dev/null
+++ b/src/sat/src/core/Vec.mli
@@ -0,0 +1,83 @@
+
+type 'a t
+(** Abstract type of vectors of 'a *)
+
+val make : int -> 'a -> 'a t
+(** [make cap dummy] creates a new vector filled with [dummy]. The vector
+    is initially empty but its underlying array has capacity [cap].
+    [dummy] will stay alive as long as the vector *)
+
+val create : unit -> 'a t
+
+val to_list : 'a t -> 'a list
+(** Returns the list of elements of the vector *)
+
+val to_array : 'a t -> 'a array
+
+val of_list : 'a list -> 'a t
+
+val to_seq : 'a t -> 'a Iter.t
+
+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 -> 'a
+(** Pop last element and return it.
+    @raise Invalid_argument if the vector is empty *)
+
+val size : 'a t -> int
+
+val is_empty : 'a t -> bool
+
+val is_full : 'a t -> bool
+(** Is the capacity of the vector equal to the number of its elements? *)
+
+val push : 'a t -> 'a -> unit
+(** Push element into the vector *)
+
+val get : 'a t -> int -> 'a
+(** get the element at the given index, or
+    @raise Invalid_argument if the index is not valid *)
+
+val set : 'a t -> int -> 'a -> unit
+(** set the element at the given index, either already set or the first
+    free slot if [not (is_full vec)], or
+    @raise Invalid_argument if the index is not valid *)
+
+val copy : 'a t -> 'a t
+(** Fresh copy *)
+
+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 *)
+
+val iter : ('a -> unit) -> 'a t -> unit
+(** Iterate on elements *)
+
+val iteri : (int -> 'a -> unit) -> 'a t -> unit
+(** Iterate on elements with their index *)
+
+val fold : ('b -> 'a -> 'b) -> 'b -> 'a t -> 'b
+(** Fold over elements *)
+
+val exists : ('a -> bool) -> 'a t -> bool
+(** Does there exist an element that satisfies the predicate? *)
+
+val for_all : ('a -> bool) -> 'a t -> bool
+(** Do all elements satisfy the predicate? *)
+
+val pp :
+  ?sep:string ->
+  (Format.formatter -> 'a -> unit) ->
+  Format.formatter -> 'a t -> unit
diff --git a/src/sat/src/core/dune b/src/sat/src/core/dune
new file mode 100644
index 00000000..85a23d9a
--- /dev/null
+++ b/src/sat/src/core/dune
@@ -0,0 +1,10 @@
+
+(library
+  (name msat)
+  (public_name msat)
+  (libraries iter)
+  (synopsis "core data structures and algorithms for msat")
+  (flags :standard -warn-error -3 -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/sat/src/core/msat.mld b/src/sat/src/core/msat.mld
new file mode 100644
index 00000000..50973961
--- /dev/null
+++ b/src/sat/src/core/msat.mld
@@ -0,0 +1,92 @@
+{1 mSAT}
+
+{2 License}
+
+This code is free, under the {{:https://github.com/Gbury/mSAT/blob/master/LICENSE}Apache 2.0 license}.
+
+{2 Contents}
+
+mSAT is an ocaml library providing SAT/SMT/McSat solvers. More precisely,
+what mSAT provides are functors to easily create such solvers. Indeed, the core
+of a sat solver does not need much information about either the exact representation
+of terms or the inner workings of a theory.
+
+Most modules in mSAT actually define functors. These functors usually take one
+or two arguments, usually an implementation of Terms and formulas used, and an implementation
+of the theory used during solving.
+
+{4 Solver creation}
+
+The following modules allow to easily create a SAT or SMT solver (remark: a SAT solver is
+simply an SMT solver with an empty theory).
+
+{!modules:
+Msat
+}
+
+The following modules allow the creation of a McSat solver (Model Constructing solver):
+
+{!modules:
+Msat_mcsolver
+}
+
+{4 Useful tools}
+
+An instanciation of a pure sat solver is also provided:
+
+{!modules:
+Msat_sat
+}
+
+Lastly, mSAT also provides an implementation of Tseitin's CNF conversion:
+
+{!modules:
+Msat_tseitin
+}
+
+{4 Proof Management}
+
+mSAT solvers are able to provide detailed proofs when an unsat state is reached. To do
+so, it require the provided theory to give proofs of the tautologies it gives the solver.
+These proofs will be called lemmas. The type of lemmas is defined by the theory and can
+very well be [unit].
+
+In this context a proof is a resolution tree, whose conclusion (i.e. root) is the
+empty clause, effectively allowing to deduce [false] from the hypotheses.
+A resolution tree is a binary tree whose nodes are clauses. Inner nodes' clauses are
+obtained by performing resolution between the two clauses of the children nodes, while
+leafs of the tree are either hypotheses, or tautologies (i.e. conflicts returned by
+the theory).
+
+{!modules:
+Msat__Res
+Msat__Res_intf
+}
+
+Backends for exporting proofs to different formats:
+
+{!modules:
+Dot
+Coq
+Dedukti
+Backend_intf
+}
+
+{4 Internal modules}
+
+WARNING: for advanced users only ! These modules expose a lot of unsafe functions
+that must be used with care to not break the required invariants. Additionally, these
+interfaces are not part of the main API and so are subject to a lot more breaking changes
+than the safe modules above.
+
+{!modules:
+Dimacs
+Internal
+External
+Solver_types
+Solver_types_intf
+}
+
+{2 Index}
+
+{!indexlist}
diff --git a/src/sat/src/dune b/src/sat/src/dune
new file mode 100644
index 00000000..05c64298
--- /dev/null
+++ b/src/sat/src/dune
@@ -0,0 +1,4 @@
+
+(documentation
+  (package msat)
+  (mld_files :standard))
diff --git a/src/sat/src/index.mld b/src/sat/src/index.mld
new file mode 100644
index 00000000..38b0a9cc
--- /dev/null
+++ b/src/sat/src/index.mld
@@ -0,0 +1,121 @@
+
+
+{1 mSAT: a Modular SAT Solver}
+
+(The entry point of this library is the module: {!module-Msat}.)
+
+A modular implementation of the SMT algorithm can be found in the {!Msat.Solver} module,
+as a functor which takes two modules :
+
+- A representation of formulas (which implements the `Formula_intf.S` signature)
+
+- A theory (which implements the `Theory_intf.S` signature) to check consistence of assertions.
+
+- A dummy empty module to ensure generativity of the solver (solver modules heavily relies on
+side effects to their internal state)
+
+{3 Sat Solver}
+
+A ready-to-use SAT solver is available in the {!Msat_sat} module
+using the [msat.sat] library (see {!module-Msat_sat}). It can be loaded
+as shown in the following code :
+
+{[
+# #require "msat";;
+# #require "msat.sat";;
+# #print_depth 0;; (* do not print details *)
+]}
+
+Then we can create a solver and create some boolean variables:
+
+{[
+module Sat = Msat_sat
+module E = Sat.Int_lit (* expressions *)
+
+let solver = Sat.create()
+
+(* We create here two distinct atoms *)
+let a = E.fresh ()    (* A 'new_atom' is always distinct from any other atom *)
+let b = E.make 1      (* Atoms can be created from integers *)
+]}
+
+We can try and check the satisfiability of some clauses — here, the clause [a or b].
+[Sat.assume] adds a list of clauses to the solver. Calling [Sat.solve]
+will check the satisfiability of the current set of clauses, here "Sat".
+
+{[
+# a <> b;;
+- : bool = true
+# Sat.assume solver [[a; b]] ();;
+- : unit = ()
+# let res = Sat.solve solver;;
+val res : Sat.res = Sat.Sat ...
+]}
+
+The Sat solver has an incremental mutable state, so we still have
+the clause `a or b` in our assumptions.
+We add `not a` and `not b` to the state, and get "Unsat".
+
+{[
+# Sat.assume solver [[E.neg a]; [E.neg b]] () ;;
+- : unit = ()
+# let res = Sat.solve solver ;;
+val res : Sat.res = Sat.Unsat ...
+]}
+
+{3 Formulas API}
+
+Writing clauses by hand can be tedious and error-prone.
+The functor {!Msat_tseitin.Make} in the library [msat.tseitin] (see {!module-Msat_tseitin}).
+proposes a formula AST (parametrized by
+atoms) and a function to convert these formulas into clauses:
+
+{[
+# #require "msat.tseitin";;
+]}
+
+{[
+(* Module initialization *)
+module F = Msat_tseitin.Make(E)
+
+let solver = Sat.create ()
+
+(* We create here two distinct atoms *)
+let a = E.fresh ()    (* A fresh atom is always distinct from any other atom *)
+let b = E.make 1      (* Atoms can be created from integers *)
+
+(* Let's create some formulas *)
+let p = F.make_atom a
+let q = F.make_atom b
+let r = F.make_and [p; q]
+let s = F.make_or [F.make_not p; F.make_not q]
+]}
+
+We can try and check the satisfiability of the given formulas, by turning
+it into clauses using `make_cnf`:
+
+{[
+# Sat.assume solver (F.make_cnf r) ();;
+- : unit = ()
+# Sat.solve solver;;
+- : Sat.res = Sat.Sat ...
+]}
+
+{[
+# Sat.assume solver (F.make_cnf s) ();;
+- : unit = ()
+# Sat.solve solver ;;
+- : Sat.res = Sat.Unsat ...
+]}
+
+{3 Backtracking utils}
+
+The library {!module-Msat_backtrack} contains some backtrackable
+data structures that are useful for implementing theories.
+
+{3 Library msat.backend}
+
+This is used for proof backends:
+
+The entry point of this library is the module:
+{!module-Msat_backend}.
diff --git a/src/sat/src/main/Dimacs_lex.mll b/src/sat/src/main/Dimacs_lex.mll
new file mode 100644
index 00000000..67850c1f
--- /dev/null
+++ b/src/sat/src/main/Dimacs_lex.mll
@@ -0,0 +1,20 @@
+{
+  open Dimacs_parse
+}
+
+let number = ['1' - '9'] ['0' - '9']*
+
+rule token = parse
+  | eof                     { EOF }
+  | "c"                     { comment lexbuf }
+  | [' ' '\t' '\r']         { token lexbuf }
+  | 'p'                     { P }
+  | "cnf"                   { CNF }
+  | '\n'                    { Lexing.new_line lexbuf; token lexbuf }
+  | '0'                     { ZERO }
+  | '-'? number             { LIT (int_of_string (Lexing.lexeme lexbuf)) }
+  | _                       { failwith @@ Printf.sprintf "dimacs.lexer: unexpected char `%s`" (Lexing.lexeme lexbuf) }
+
+and comment = parse
+  | '\n'                    { Lexing.new_line lexbuf; token lexbuf }
+  | [^'\n']                 { comment lexbuf }
diff --git a/src/sat/src/main/Dimacs_parse.mly b/src/sat/src/main/Dimacs_parse.mly
new file mode 100644
index 00000000..408b8db9
--- /dev/null
+++ b/src/sat/src/main/Dimacs_parse.mly
@@ -0,0 +1,34 @@
+/*  Copyright 2005 INRIA  */
+
+%{
+  let lnum pos = pos.Lexing.pos_lnum
+  let cnum pos = pos.Lexing.pos_cnum - pos.Lexing.pos_bol
+  let pp_pos out (start,stop) =
+    Format.fprintf out "(at %d:%d - %d:%d)"
+      (lnum start) (cnum start) (lnum stop) (cnum stop)
+%}
+
+%token <int> LIT
+%token ZERO
+%token P CNF EOF
+
+%start file
+%type <int list list> file
+
+%%
+
+/* DIMACS syntax */
+
+prelude:
+  | P CNF LIT LIT { () }
+
+clauses:
+  | { [] }
+  | clause clauses { $1 :: $2 }
+
+file:
+  | prelude clauses EOF { $2 }
+
+clause:
+  | ZERO { [] }
+  | LIT clause { $1 :: $2 }
diff --git a/src/sat/src/main/dune b/src/sat/src/main/dune
new file mode 100644
index 00000000..073ec30f
--- /dev/null
+++ b/src/sat/src/main/dune
@@ -0,0 +1,14 @@
+
+; main binary
+(executable
+  (name main)
+  (public_name msat)
+  (package msat-bin)
+  (libraries containers camlzip msat msat.sat msat.backend)
+  (flags :standard -warn-error -3 -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string -open Msat)
+  (ocamlopt_flags :standard -O3 -color always
+                  -unbox-closures -unbox-closures-factor 20)
+  )
+
+(ocamlyacc (modules Dimacs_parse))
+(ocamllex (modules Dimacs_lex))
diff --git a/src/sat/src/main/main.ml b/src/sat/src/main/main.ml
new file mode 100644
index 00000000..ddc1d856
--- /dev/null
+++ b/src/sat/src/main/main.ml
@@ -0,0 +1,186 @@
+(*
+MSAT is free software, using the Apache license, see file LICENSE
+Copyright 2014 Guillaume Bury
+Copyright 2014 Simon Cruanes
+*)
+
+exception Incorrect_model
+exception Out_of_time
+exception Out_of_space
+
+let file = ref ""
+let p_cnf = ref false
+let p_check = ref false
+let p_dot_proof = ref ""
+let p_proof_print = ref false
+let time_limit = ref 300.
+let size_limit = ref 1000_000_000.
+let no_proof = ref false
+
+module S = Msat_sat
+
+module Process() = struct
+  module D = Msat_backend.Dot.Make(S)(Msat_backend.Dot.Default(S))
+
+  let hyps = ref []
+
+  let st = S.create ~store_proof:(not !no_proof) ~size:`Big ()
+
+  let check_model sat =
+    let check_clause c =
+      let l = List.map (function a ->
+          Log.debugf 99
+            (fun k -> k "Checking value of %a" S.Formula.pp a);
+          sat.Msat.eval a) c in
+      List.exists (fun x -> x) l
+    in
+    let l = List.map check_clause !hyps in
+    List.for_all (fun x -> x) l
+
+  let prove ~assumptions () =
+    let res = S.solve ~assumptions st in
+    let t = Sys.time () in
+    begin match res with
+      | S.Sat state ->
+        if !p_check then
+          if not (check_model state) then
+            raise Incorrect_model;
+        let t' = Sys.time () -. t in
+        Format.printf "Sat (%f/%f)@." t t'
+      | S.Unsat state ->
+        if !p_check then (
+          let p = state.Msat.get_proof () in
+          S.Proof.check_empty_conclusion p;
+          S.Proof.check p;
+          if !p_dot_proof <> "" then (
+            let oc = open_out !p_dot_proof in
+            let fmt = Format.formatter_of_out_channel oc in
+            Format.fprintf fmt "%a@?" D.pp p;
+            flush oc; close_out_noerr oc;
+          )
+        );
+        let t' = Sys.time () -. t in
+        Format.printf "Unsat (%f/%f)@." t t'
+    end
+
+  let conv_c c = List.rev_map S.Int_lit.make c
+
+  let add_clauses cs =
+    S.assume st (CCList.map conv_c cs) ()
+end[@@inline]
+
+let parse_file f =
+  let module L = Lexing in
+  CCIO.with_in f
+    (fun ic ->
+       let buf =
+         if CCString.suffix ~suf:".gz" f
+         then (
+           let gic = Gzip.open_in_chan ic in
+           L.from_function (fun bytes len -> Gzip.input gic bytes 0 len)
+         ) else L.from_channel ic
+       in
+       buf.L.lex_curr_p <- {buf.L.lex_curr_p with L.pos_fname=f;};
+       Dimacs_parse.file Dimacs_lex.token buf)
+
+let error_msg opt arg l =
+  Format.fprintf Format.str_formatter "'%s' is not a valid argument for '%s', valid arguments are : %a"
+    arg opt (fun fmt -> List.iter (fun (s, _) -> Format.fprintf fmt "%s, " s)) l;
+  Format.flush_str_formatter ()
+
+(* Arguments parsing *)
+let int_arg r arg =
+  let l = String.length arg in
+  let multiplier m =
+    let arg1 = String.sub arg 0 (l-1) in
+    r := m *. (float_of_string arg1)
+  in
+  if l = 0 then raise (Arg.Bad "bad numeric argument")
+  else
+    try
+      match arg.[l-1] with
+      | 'k' -> multiplier 1e3
+      | 'M' -> multiplier 1e6
+      | 'G' -> multiplier 1e9
+      | 'T' -> multiplier 1e12
+      | 's' -> multiplier 1.
+      | 'm' -> multiplier 60.
+      | 'h' -> multiplier 3600.
+      | 'd' -> multiplier 86400.
+      | '0'..'9' -> r := float_of_string arg
+      | _ -> raise (Arg.Bad "bad numeric argument")
+    with Failure _ -> raise (Arg.Bad "bad numeric argument")
+
+let setup_gc_stat () =
+  at_exit (fun () ->
+      Gc.print_stat stdout;
+    )
+
+let input_file = fun s -> file := s
+
+let usage = "Usage : main [options] <file>"
+let argspec = Arg.align [
+    "-bt", Arg.Unit (fun () -> Printexc.record_backtrace true),
+    " Enable stack traces";
+    "-cnf", Arg.Set p_cnf,
+    " Prints the cnf used.";
+    "-check", Arg.Set p_check,
+    " Build, check and print the proof (if output is set), if unsat";
+    "-dot", Arg.Set_string p_dot_proof,
+    " If provided, print the dot proof in the given file";
+    "-gc", Arg.Unit setup_gc_stat,
+    " Outputs statistics about the GC";
+    "-size", Arg.String (int_arg size_limit),
+    "<s>[kMGT] Sets the size limit for the sat solver";
+    "-time", Arg.String (int_arg time_limit),
+    "<t>[smhd] Sets the time limit for the sat solver";
+    "-v", Arg.Int (fun i -> Log.set_debug i),
+    "<lvl> Sets the debug verbose level";
+    "-no-proof", Arg.Set no_proof, " disable proof logging";
+  ]
+
+(* Limits alarm *)
+let check () =
+  let t = Sys.time () in
+  let heap_size = (Gc.quick_stat ()).Gc.heap_words in
+  let s = float heap_size *. float Sys.word_size /. 8. in
+  if t > !time_limit then
+    raise Out_of_time
+  else if s > !size_limit then
+    raise Out_of_space
+
+let main () =
+  (* Administrative duties *)
+  Arg.parse argspec input_file usage;
+  if !file = "" then (
+    Arg.usage argspec usage;
+    exit 2
+  );
+  let al = Gc.create_alarm check in
+
+  let module P = Process() in
+
+  (* Interesting stuff happening *)
+  let clauses = parse_file !file in
+  P.add_clauses clauses;
+  P.prove ~assumptions:[] ();
+  Gc.delete_alarm al;
+  ()
+
+let () =
+  try
+    main ()
+  with
+  | Out_of_time ->
+    Format.printf "Timeout@.";
+    exit 2
+  | Out_of_space ->
+    Format.printf "Spaceout@.";
+    exit 3
+  | Incorrect_model ->
+    Format.printf "Internal error : incorrect *sat* model@.";
+    exit 4
+  | S.Proof.Resolution_error msg  ->
+    Format.printf "Internal error: incorrect *unsat* proof:\n%s@." msg;
+    exit 5
+
diff --git a/src/sat/src/sat/Int_lit.ml b/src/sat/src/sat/Int_lit.ml
new file mode 100644
index 00000000..9f01aaeb
--- /dev/null
+++ b/src/sat/src/sat/Int_lit.ml
@@ -0,0 +1,66 @@
+
+exception Bad_atom
+(** Exception raised if an atom cannot be created *)
+
+type t = int
+(** Atoms are represented as integers. [-i] begin the negation of [i].
+    Additionally, since we nee dot be able to create fresh atoms, we
+    use even integers for user-created atoms, and odd integers for the
+    fresh atoms. *)
+
+let max_lit = max_int
+
+(* Counters *)
+let max_index = ref 0
+let max_fresh = ref (-1)
+
+(** Internal function for creating atoms.
+    Updates the internal counters *)
+let _make i =
+  if i <> 0 && (abs i) < max_lit then begin
+    max_index := max !max_index (abs i);
+    i
+  end else
+    raise Bad_atom
+
+let to_int i = i
+
+(** *)
+let neg a = - a
+
+let norm a =
+  abs a, if a < 0 then
+    Solver_intf.Negated
+  else
+    Solver_intf.Same_sign
+
+let abs = abs
+
+let sign i = i > 0
+
+let apply_sign b i = if b then i else neg i
+
+let set_sign b i = if b then abs i else neg (abs i)
+
+let hash (a:int) = a land max_int
+let equal (a:int) b = a=b
+let compare (a:int) b = compare a b
+
+let make i = _make (2 * i)
+
+let fresh () =
+  incr max_fresh;
+  _make (2 * !max_fresh + 1)
+
+(*
+let iter: (t -> unit) -> unit = fun f ->
+  for j = 1 to !max_index do
+    f j
+  done
+*)
+
+let pp fmt a =
+  Format.fprintf fmt "%s%s%d"
+    (if a < 0 then "~" else "")
+    (if a mod 2 = 0 then "v" else "f")
+    ((abs a) / 2)
diff --git a/src/sat/src/sat/Int_lit.mli b/src/sat/src/sat/Int_lit.mli
new file mode 100644
index 00000000..6845d161
--- /dev/null
+++ b/src/sat/src/sat/Int_lit.mli
@@ -0,0 +1,33 @@
+
+(** {1 The module defining formulas} *)
+
+(** SAT Formulas
+
+    This modules implements formuals adequate for use in a pure SAT Solver.
+    Atomic formuals are represented using integers, that should allow
+    near optimal efficiency (both in terms of space and time).
+*)
+
+include Solver_intf.FORMULA
+(** This modules implements the requirements for implementing an SAT Solver. *)
+
+val make : int -> t
+(** Make a proposition from an integer. *)
+
+val to_int : t -> int
+
+val fresh : unit -> t
+(** Make a fresh atom *)
+
+val compare : t -> t -> int
+(** Compare atoms *)
+
+val sign : t -> bool
+(** Is the given atom positive ? *)
+
+val apply_sign : bool -> t -> t
+(** [apply_sign b] is the identity if [b] is [true], and the negation
+    function if [b] is [false]. *)
+
+val set_sign : bool -> t -> t
+(** Return the atom with the sign set. *)
diff --git a/src/sat/src/sat/Msat_sat.ml b/src/sat/src/sat/Msat_sat.ml
new file mode 100644
index 00000000..91cc70c6
--- /dev/null
+++ b/src/sat/src/sat/Msat_sat.ml
@@ -0,0 +1,11 @@
+(*
+MSAT is free software, using the Apache license, see file LICENSE
+Copyright 2016 Guillaume Bury
+*)
+
+module Int_lit = Int_lit
+include Msat.Make_pure_sat(struct
+    module Formula = Int_lit
+    type proof = unit
+  end)
+
diff --git a/src/sat/src/sat/Msat_sat.mli b/src/sat/src/sat/Msat_sat.mli
new file mode 100644
index 00000000..0517e913
--- /dev/null
+++ b/src/sat/src/sat/Msat_sat.mli
@@ -0,0 +1,19 @@
+(*
+MSAT is free software, using the Apache license, see file LICENSE
+Copyright 2016 Guillaume Bury
+*)
+
+(** Sat solver
+
+    This modules instanciates a pure sat solver using integers to represent
+    atomic propositions.
+*)
+
+module Int_lit = Int_lit
+
+include Msat.S
+  with type Formula.t = Int_lit.t
+   and type theory = unit
+   and type lemma = unit
+(** A functor that can generate as many solvers as needed. *)
+
diff --git a/src/sat/src/sat/dune b/src/sat/src/sat/dune
new file mode 100644
index 00000000..624b2a57
--- /dev/null
+++ b/src/sat/src/sat/dune
@@ -0,0 +1,11 @@
+
+(library
+  (name msat_sat)
+  (public_name msat.sat)
+  (synopsis "purely boolean interface to Msat")
+  (libraries msat)
+  (flags :standard -warn-error -3 -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string -open Msat)
+  (ocamlopt_flags :standard -O3 -color always
+                  -unbox-closures -unbox-closures-factor 20)
+  )
+
diff --git a/src/sat/src/sudoku/dune b/src/sat/src/sudoku/dune
new file mode 100644
index 00000000..000c407f
--- /dev/null
+++ b/src/sat/src/sudoku/dune
@@ -0,0 +1,9 @@
+
+(executable
+  (name sudoku_solve)
+  (modes native)
+  (libraries msat msat.backtrack iter containers)
+  (flags :standard -warn-error -a -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/sat/src/sudoku/sudoku_solve.ml b/src/sat/src/sudoku/sudoku_solve.ml
new file mode 100644
index 00000000..a75ace03
--- /dev/null
+++ b/src/sat/src/sudoku/sudoku_solve.ml
@@ -0,0 +1,331 @@
+
+(** {1 simple sudoku solver} *)
+
+module Fmt = CCFormat
+module Log = Msat.Log
+module Vec = Msat.Vec
+
+let errorf msg = CCFormat.kasprintf failwith msg
+
+module Cell : sig
+  type t = private int
+  val equal : t -> t -> bool
+  val neq : t -> t -> bool
+  val hash : t -> int
+  val empty : t
+  val is_empty : t -> bool
+  val is_full : t -> bool
+  val make : int -> t
+  val pp : t Fmt.printer
+end = struct
+  type t = int
+  let empty = 0
+  let[@inline] make i = assert (i >= 0 && i <= 9); i
+  let[@inline] is_empty x = x = 0
+  let[@inline] is_full x = x > 0
+  let hash = CCHash.int
+  let[@inline] equal (a:t) b = a=b
+  let[@inline] neq (a:t) b = a<>b
+  let pp out i = if i=0 then Fmt.char out '.' else Fmt.int out i
+end
+
+module Grid : sig
+  type t
+
+  val get : t -> int -> int -> Cell.t
+  val set : t -> int -> int -> Cell.t -> t
+
+  (** A set of related cells *)
+  type set = (int*int*Cell.t) Iter.t
+
+  val rows : t -> set Iter.t
+  val cols : t -> set Iter.t
+  val squares : t -> set Iter.t
+
+  val all_cells : t -> (int*int*Cell.t) Iter.t
+
+  val parse : string -> t
+  val is_full : t -> bool
+  val is_valid : t -> bool
+  val matches : pat:t -> t -> bool
+  val pp : t Fmt.printer
+end = struct
+  type t = Cell.t array
+
+  let[@inline] get (s:t) i j = s.(i*9 + j)
+
+  let[@inline] set (s:t) i j n =
+    let s' = Array.copy s in
+    s'.(i*9 + j) <- n;
+    s'
+
+  (** A set of related cells *)
+  type set = (int*int*Cell.t) Iter.t
+
+  open Iter.Infix
+
+  let all_cells (g:t) =
+    0 -- 8 >>= fun i ->
+    0 -- 8 >|= fun j -> (i,j,get g i j)
+
+  let rows (g:t) =
+    0 -- 8 >|= fun i ->
+    ( 0 -- 8 >|= fun j -> (i,j,get g i j))
+
+  let cols g =
+    0 -- 8 >|= fun j ->
+    ( 0 -- 8 >|= fun i -> (i,j,get g i j))
+
+  let squares g =
+    0 -- 2 >>= fun sq_i ->
+    0 -- 2 >|= fun sq_j ->
+    ( 0 -- 2 >>= fun off_i ->
+      0 -- 2 >|= fun off_j ->
+      let i = 3*sq_i + off_i in
+      let j = 3*sq_j + off_j in
+      (i,j,get g i j))
+
+  let is_full g = Array.for_all Cell.is_full g
+
+  let is_valid g =
+    let all_distinct (s:set) =
+      (s >|= fun (_,_,c) -> c)
+      |> Iter.diagonal
+      |> Iter.for_all (fun (c1,c2) -> Cell.neq c1 c2)
+    in
+    Iter.for_all all_distinct @@ rows g &&
+    Iter.for_all all_distinct @@ cols g &&
+    Iter.for_all all_distinct @@ squares g
+
+  let matches ~pat:g1 g2 : bool =
+    all_cells g1
+    |> Iter.filter (fun (_,_,c) -> Cell.is_full c)
+    |> Iter.for_all (fun (x,y,c) -> Cell.equal c @@ get g2 x y)
+
+  let pp out g =
+    Fmt.fprintf out "@[<v>";
+    Array.iteri
+      (fun i n ->
+         Cell.pp out n;
+         if i mod 9 = 8 then Fmt.fprintf out "@,")
+      g;
+    Fmt.fprintf out "@]"
+
+  let parse (s:string) : t =
+    if String.length s < 81 then (
+      errorf "line is too short, expected 81 chars, not %d" (String.length s);
+    );
+    let a = Array.make 81 Cell.empty in
+    for i = 0 to 80 do
+      let c = String.get s i in
+      let n = if c = '.' then 0 else Char.code c - Char.code '0' in
+      if n < 0 || n > 9 then errorf "invalid char %c" c;
+      a.(i) <- Cell.make n
+    done;
+    a
+end
+
+module B_ref = Msat_backtrack.Ref
+
+module Solver : sig
+  type t
+  val create : Grid.t -> t
+  val solve : t -> Grid.t option
+end = struct
+  open Msat.Solver_intf
+
+  (* formulas *)
+  module F = struct
+    type t = bool*int*int*Cell.t
+    let equal (sign1,x1,y1,c1)(sign2,x2,y2,c2) =
+      sign1=sign2 && x1=x2 && y1=y2 && Cell.equal c1 c2
+    let hash (sign,x,y,c) = CCHash.(combine4 (bool sign)(int x)(int y)(Cell.hash c))
+    let pp out (sign,x,y,c) =
+      Fmt.fprintf out "[@[(%d,%d) %s %a@]]" x y (if sign then "=" else "!=") Cell.pp c
+    let neg (sign,x,y,c) = (not sign,x,y,c)
+    let norm ((sign,_,_,_) as f) =
+      if sign then f, Same_sign else neg f, Negated
+
+    let make sign x y (c:Cell.t) : t = (sign,x,y,c)
+  end
+
+  module Theory = struct
+    type proof = unit
+    module Formula = F
+    type t = {
+      grid: Grid.t B_ref.t;
+    }
+
+    let create g : t = {grid=B_ref.create g}
+    let[@inline] grid self : Grid.t = B_ref.get self.grid
+    let[@inline] set_grid self g : unit = B_ref.set self.grid g
+
+    let push_level self = B_ref.push_level self.grid
+    let pop_levels self n = B_ref.pop_levels self.grid n
+
+    let pp_c_ = Fmt.(list ~sep:(return "@ ∨ ")) F.pp
+    let[@inline] logs_conflict kind c : unit =
+      Log.debugf 4 (fun k->k "(@[conflict.%s@ %a@])" kind pp_c_ c)
+
+    (* check that all cells are full *)
+    let check_full_ (self:t) acts : unit =
+      Grid.all_cells (grid self)
+        (fun (x,y,c) ->
+           if Cell.is_empty c then (
+             let c =
+               CCList.init 9
+                 (fun c -> F.make true x y (Cell.make (c+1)))
+             in
+             Log.debugf 4 (fun k->k "(@[add-clause@ %a@])" pp_c_ c);
+             acts.acts_add_clause ~keep:true c ();
+           ))
+
+    (* check constraints *)
+    let check_ (self:t) acts : unit =
+      Log.debugf 4 (fun k->k "(@[sudoku.check@ @[:g %a@]@])" Grid.pp (B_ref.get self.grid));
+      let[@inline] all_diff kind f =
+        let pairs =
+          f (grid self)
+          |> Iter.flat_map
+            (fun set ->
+               set
+               |> Iter.filter (fun (_,_,c) -> Cell.is_full c)
+               |> Iter.diagonal)
+        in
+        pairs
+          (fun ((x1,y1,c1),(x2,y2,c2)) ->
+             if Cell.equal c1 c2 then (
+               assert (x1<>x2 || y1<>y2);
+               let c = [F.make false x1 y1 c1; F.make false x2 y2 c2] in
+               logs_conflict ("all-diff." ^ kind) c;
+               acts.acts_raise_conflict c ()
+             ))
+      in
+      all_diff "rows" Grid.rows;
+      all_diff "cols" Grid.cols;
+      all_diff "squares" Grid.squares;
+      ()
+
+    let trail_ (acts:_ Msat.acts) =
+      acts.acts_iter_assumptions
+      |> Iter.map
+        (function
+          | Assign _ -> assert false
+          | Lit f -> f)
+
+    (* update current grid with the given slice *)
+    let add_slice (self:t) acts : unit =
+      trail_ acts
+        (function
+          | false,_,_,_ -> ()
+          | true,x,y,c ->
+            assert (Cell.is_full c);
+            let grid = grid self in
+            let c' = Grid.get grid x y in
+            if Cell.is_empty c' then (
+              set_grid self (Grid.set grid x y c);
+            ) else if Cell.neq c c' then (
+              (* conflict: at most one value *)
+              let c = [F.make false x y c; F.make false x y c'] in
+              logs_conflict "at-most-one" c;
+              acts.acts_raise_conflict c ()
+            )
+        )
+
+    let partial_check (self:t) acts : unit =
+      Log.debugf 4
+        (fun k->k "(@[sudoku.partial-check@ :trail [@[%a@]]@])"
+            (Fmt.list F.pp) (trail_ acts |> Iter.to_list));
+      add_slice self acts;
+      check_ self acts
+
+    let final_check (self:t) acts : unit =
+      Log.debugf 4 (fun k->k "(@[sudoku.final-check@])");
+      check_full_ self acts;
+      check_ self acts
+
+  end
+
+  module S = Msat.Make_cdcl_t(Theory)
+
+  type t = {
+    grid0: Grid.t;
+    solver: S.t;
+  }
+
+  let solve (self:t) : _ option =
+    let assumptions =
+      Grid.all_cells self.grid0
+      |> Iter.filter (fun (_,_,c) -> Cell.is_full c)
+      |> Iter.map (fun (x,y,c) -> F.make true x y c)
+      |> Iter.map (S.make_atom self.solver)
+      |> Iter.to_rev_list
+    in
+    Log.debugf 2
+      (fun k->k "(@[sudoku.solve@ :assumptions %a@])" (Fmt.Dump.list S.Atom.pp) assumptions);
+    let r =
+      match S.solve self.solver ~assumptions with
+      | S.Sat _ -> Some (Theory.grid (S.theory self.solver))
+      | S.Unsat _ -> None
+    in
+    (* TODO: print some stats *)
+    r
+
+  let create g : t =
+    { solver=S.create ~store_proof:false (Theory.create g); grid0=g }
+end
+
+let solve_grid (g:Grid.t) : Grid.t option =
+  let s = Solver.create g in
+  Solver.solve s
+
+let solve_file file =
+  Format.printf "solve grids in file %S@." file;
+  let start = Sys.time() in
+  let grids =
+    CCIO.with_in file CCIO.read_lines_l
+    |> CCList.filter_map
+      (fun s ->
+         let s = String.trim s in
+         if s="" then None
+         else match Grid.parse s with
+           | g -> Some g
+           | exception e ->
+             errorf "cannot parse sudoku %S: %s@." s (Printexc.to_string e))
+  in
+  Format.printf "parsed %d grids (in %.3fs)@." (List.length grids) (Sys.time()-.start);
+  List.iter
+    (fun g ->
+       Format.printf "@[<v>@,#########################@,@[<2>solve grid:@ %a@]@]@." Grid.pp g;
+       let start=Sys.time() in
+       match solve_grid g with
+       | None -> Format.printf "no solution (in %.3fs)@." (Sys.time()-.start)
+       | Some g' when not @@ Grid.is_full g' ->
+         errorf "grid %a@ is not full" Grid.pp g'
+       | Some g' when not @@ Grid.is_valid g' ->
+         errorf "grid %a@ is not valid" Grid.pp g'
+       | Some g' when not @@ Grid.matches ~pat:g g' ->
+         errorf "grid %a@ @[<2>does not match original@ %a@]" Grid.pp g' Grid.pp g
+       | Some g' ->
+         Format.printf "@[<v>@[<2>solution (in %.3fs):@ %a@]@,###################@]@."
+           (Sys.time()-.start) Grid.pp g')
+    grids;
+  Format.printf "@.solved %d grids (in %.3fs)@." (List.length grids) (Sys.time()-.start);
+  ()
+
+let () =
+  Fmt.set_color_default true;
+  let files = ref [] in
+  let debug = ref 0 in
+  let opts = [
+    "--debug", Arg.Set_int debug, " debug";
+    "-d", Arg.Set_int debug, " debug";
+  ] |> Arg.align in
+  Arg.parse opts (fun f -> files := f :: !files) "sudoku_solve [options] <file>";
+  Msat.Log.set_debug !debug;
+  try
+    List.iter (fun f -> solve_file f) !files;
+  with
+  | Failure msg | Invalid_argument msg ->
+    Format.printf "@{<Red>Error@}:@.%s@." msg;
+    exit 1
diff --git a/src/sat/src/tseitin/Msat_tseitin.ml b/src/sat/src/tseitin/Msat_tseitin.ml
new file mode 100644
index 00000000..3f162c8d
--- /dev/null
+++ b/src/sat/src/tseitin/Msat_tseitin.ml
@@ -0,0 +1,326 @@
+(**************************************************************************)
+(*                                                                        *)
+(*                          Alt-Ergo Zero                                 *)
+(*                                                                        *)
+(*                  Sylvain Conchon and Alain Mebsout                     *)
+(*                      Universite Paris-Sud 11                           *)
+(*                                                                        *)
+(*  Copyright 2011. This file is distributed under the terms of the       *)
+(*  Apache Software License version 2.0                                   *)
+(*                                                                        *)
+(**************************************************************************)
+
+module type Arg = Tseitin_intf.Arg
+
+module type S = Tseitin_intf.S
+
+module Make (F : Tseitin_intf.Arg) = struct
+
+  exception Empty_Or
+  type combinator = And | Or | Imp | Not
+
+  type atom = F.t
+  type t =
+    | True
+    | Lit of atom
+    | Comb of combinator * t list
+
+  let rec pp fmt phi =
+    match phi with
+    | True -> Format.fprintf fmt "true"
+    | Lit a -> F.pp fmt a
+    | Comb (Not, [f]) ->
+      Format.fprintf fmt "not (%a)" pp f
+    | Comb (And, l) -> Format.fprintf fmt "(%a)" (pp_list "and") l
+    | Comb (Or, l) ->  Format.fprintf fmt "(%a)" (pp_list "or") l
+    | Comb (Imp, [f1; f2]) ->
+      Format.fprintf fmt "(%a => %a)" pp f1 pp f2
+    | _ -> assert false
+  and pp_list sep fmt = function
+    | [] -> ()
+    | [f] -> pp fmt f
+    | f::l -> Format.fprintf fmt "%a %s %a" pp f sep (pp_list sep) l
+
+  let make comb l = Comb (comb, l)
+
+  let make_atom p = Lit p
+
+  let f_true = True
+  let f_false = Comb(Not, [True])
+
+  let rec flatten comb acc = function
+    | [] -> acc
+    | (Comb (c, l)) :: r when c = comb ->
+      flatten comb (List.rev_append l acc) r
+    | a :: r ->
+      flatten comb (a :: acc) r
+
+  let rec opt_rev_map f acc = function
+    | [] -> acc
+    | a :: r -> begin match f a with
+        | None -> opt_rev_map f acc r
+        | Some b -> opt_rev_map f (b :: acc) r
+      end
+
+  let remove_true l =
+    let aux = function
+      | True -> None
+      | f -> Some f
+    in
+    opt_rev_map aux [] l
+
+  let remove_false l =
+    let aux = function
+      | Comb(Not, [True]) -> None
+      | f -> Some f
+    in
+    opt_rev_map aux [] l
+
+
+  let make_not f = make Not [f]
+
+  let make_and l =
+    let l' = remove_true (flatten And [] l) in
+    if List.exists ((=) f_false) l' then
+      f_false
+    else
+      make And l'
+
+  let make_or l =
+    let l' = remove_false (flatten Or [] l) in
+    if List.exists ((=) f_true) l' then
+      f_true
+    else match l' with
+      | [] -> raise Empty_Or
+      | [a] -> a
+      | _ -> Comb (Or, l')
+
+  let make_imply f1 f2 = make Imp [f1; f2]
+  let make_equiv f1 f2 = make_and [ make_imply f1 f2; make_imply f2 f1]
+  let make_xor f1 f2 = make_or [ make_and [ make_not f1; f2 ];
+                                 make_and [ f1; make_not f2 ] ]
+
+  (* simplify formula *)
+  let (%%) f g x = f (g x)
+
+  let rec sform f k = match f with
+    | True | Comb (Not, [True]) -> k f
+    | Comb (Not, [Lit a]) -> k (Lit (F.neg a))
+    | Comb (Not, [Comb (Not, [f])]) -> sform f k
+    | Comb (Not, [Comb (Or, l)]) -> sform_list_not [] l (k %% make_and)
+    | Comb (Not, [Comb (And, l)]) -> sform_list_not [] l (k %% make_or)
+    | Comb (And, l) -> sform_list [] l (k %% make_and)
+    | Comb (Or, l) -> sform_list [] l (k %% make_or)
+    | Comb (Imp, [f1; f2]) ->
+      sform (make_not f1) (fun f1' -> sform f2 (fun f2' -> k (make_or [f1'; f2'])))
+    | Comb (Not, [Comb (Imp, [f1; f2])]) ->
+      sform f1 (fun f1' -> sform (make_not f2) (fun f2' -> k (make_and [f1';f2'])))
+    | Comb ((Imp | Not), _) -> assert false
+    | Lit _ -> k f
+  and sform_list acc l k = match l with
+    | [] -> k acc
+    | f :: tail ->
+      sform f (fun f' -> sform_list (f'::acc) tail k)
+  and sform_list_not acc l k = match l with
+    | [] -> k acc
+    | f :: tail ->
+      sform (make_not f) (fun f' -> sform_list_not (f'::acc) tail k)
+
+  let ( @@ ) l1 l2 = List.rev_append l1 l2
+  (* let ( @ ) = `Use_rev_append_instead   (* prevent use of non-tailrec append *) *)
+
+  (*
+  let distrib l_and l_or =
+    let l =
+      if l_or = [] then l_and
+      else
+        List.rev_map
+          (fun x ->
+             match x with
+             | Lit _ -> Comb (Or, x::l_or)
+             | Comb (Or, l) -> Comb (Or, l @@ l_or)
+             | _ -> assert false
+          ) l_and
+    in
+    Comb (And, l)
+
+  let rec flatten_or = function
+    | [] -> []
+    | Comb (Or, l)::r -> l @@ (flatten_or r)
+    | Lit a :: r -> (Lit a)::(flatten_or r)
+    | _ -> assert false
+
+  let rec flatten_and = function
+    | [] -> []
+    | Comb (And, l)::r -> l @@ (flatten_and r)
+    | a :: r -> a::(flatten_and r)
+
+
+  let rec cnf f =
+    match f with
+    | Comb (Or, l) ->
+      begin
+        let l = List.rev_map cnf l in
+        let l_and, l_or =
+          List.partition (function Comb(And,_) -> true | _ -> false) l in
+        match l_and with
+        | [ Comb(And, l_conj) ] ->
+          let u = flatten_or l_or in
+          distrib l_conj u
+
+        | Comb(And, l_conj) :: r ->
+          let u = flatten_or l_or in
+          cnf (Comb(Or, (distrib l_conj u)::r))
+
+        | _ ->
+          begin
+            match flatten_or l_or with
+            | [] -> assert false
+            | [r] -> r
+            | v -> Comb (Or, v)
+          end
+      end
+    | Comb (And, l) ->
+      Comb (And, List.rev_map cnf l)
+    | f -> f
+
+  let rec mk_cnf = function
+    | Comb (And, l) ->
+      List.fold_left (fun acc f ->  (mk_cnf f) @@ acc) [] l
+
+    | Comb (Or, [f1;f2]) ->
+      let ll1 = mk_cnf f1 in
+      let ll2 = mk_cnf f2 in
+      List.fold_left
+        (fun acc l1 -> (List.rev_map (fun l2 -> l1 @@ l2)ll2) @@ acc) [] ll1
+
+    | Comb (Or, f1 :: l) ->
+      let ll1 = mk_cnf f1 in
+      let ll2 = mk_cnf (Comb (Or, l)) in
+      List.fold_left
+        (fun acc l1 -> (List.rev_map (fun l2 -> l1 @@ l2)ll2) @@ acc) [] ll1
+
+    | Lit a -> [[a]]
+    | Comb (Not, [Lit a]) -> [[F.neg a]]
+    | _ -> assert false
+
+
+  let rec unfold mono f =
+    match f with
+    | Lit a -> a::mono
+    | Comb (Not, [Lit a]) ->
+      (F.neg a)::mono
+    | Comb (Or, l) ->
+      List.fold_left unfold mono l
+    | _ -> assert false
+
+  let rec init monos f =
+    match f with
+    | Comb (And, l) ->
+      List.fold_left init monos l
+    | f -> (unfold [] f)::monos
+
+  let make_cnf f =
+    let sfnc = cnf (sform f) in
+    init [] sfnc
+  *)
+
+  let mk_proxy = F.fresh
+
+  let acc_or = ref []
+  let acc_and = ref []
+
+  (* build a clause by flattening (if sub-formulas have the
+     same combinator) and proxy-ing sub-formulas that have the
+     opposite operator. *)
+  let rec cnf f = match f with
+    | Lit a -> None, [a]
+    | Comb (Not, [Lit a]) -> None, [F.neg a]
+
+    | Comb (And, l) ->
+      List.fold_left
+        (fun (_, acc) f ->
+           match cnf f with
+           | _, [] -> assert false
+           | _cmb, [a] -> Some And, a :: acc
+           | Some And, l ->
+             Some And, l @@ acc
+           (* let proxy = mk_proxy () in *)
+           (* acc_and := (proxy, l) :: !acc_and; *)
+           (* proxy :: acc *)
+           | Some Or, l ->
+             let proxy = mk_proxy () in
+             acc_or := (proxy, l) :: !acc_or;
+             Some And, proxy :: acc
+           | None, l -> Some And, l @@ acc
+           | _ -> assert false
+        ) (None, []) l
+
+    | Comb (Or, l) ->
+      List.fold_left
+        (fun (_, acc) f ->
+           match cnf f with
+           | _, [] -> assert false
+           | _cmb, [a] -> Some Or, a :: acc
+           | Some Or, l ->
+             Some Or, l @@ acc
+           (* let proxy = mk_proxy () in *)
+           (* acc_or := (proxy, l) :: !acc_or; *)
+           (* proxy :: acc *)
+           | Some And, l ->
+             let proxy = mk_proxy () in
+             acc_and := (proxy, l) :: !acc_and;
+             Some Or, proxy :: acc
+           | None, l -> Some Or, l @@ acc
+           | _ -> assert false
+        ) (None, []) l
+    | _ -> assert false
+
+  let cnf f =
+    let acc = match f with
+      | True -> []
+      | Comb(Not, [True]) -> [[]]
+      | Comb (And, l) -> List.rev_map (fun f -> snd(cnf f)) l
+      | _ -> [snd (cnf f)]
+    in
+    let proxies = ref [] in
+    (* encore clauses that make proxies in !acc_and equivalent to
+       their clause *)
+    let acc =
+      List.fold_left
+        (fun acc (p,l) ->
+           proxies := p :: !proxies;
+           let np = F.neg p in
+           (* build clause [cl = l1 & l2 & ... & ln => p] where [l = [l1;l2;..]]
+              also add clauses [p => l1], [p => l2], etc. *)
+           let cl, acc =
+             List.fold_left
+               (fun (cl,acc) a -> (F.neg a :: cl), [np; a] :: acc)
+               ([p],acc) l in
+           cl :: acc
+        ) acc !acc_and
+    in
+    (* encore clauses that make proxies in !acc_or equivalent to
+       their clause *)
+    let acc =
+      List.fold_left
+        (fun acc (p,l) ->
+           proxies := p :: !proxies;
+           (* add clause [p => l1 | l2 | ... | ln], and add clauses
+              [l1 => p], [l2 => p], etc. *)
+           let acc = List.fold_left (fun acc a -> [p; F.neg a]::acc)
+               acc l in
+           (F.neg p :: l) :: acc
+        ) acc !acc_or
+    in
+    acc
+
+  let make_cnf f =
+    acc_or := [];
+    acc_and := [];
+    cnf (sform f (fun f' -> f'))
+
+  (* Naive CNF XXX remove???
+     let make_cnf f = mk_cnf (sform f)
+  *)
+end
diff --git a/src/sat/src/tseitin/Msat_tseitin.mli b/src/sat/src/tseitin/Msat_tseitin.mli
new file mode 100644
index 00000000..498667c5
--- /dev/null
+++ b/src/sat/src/tseitin/Msat_tseitin.mli
@@ -0,0 +1,22 @@
+(*
+MSAT is free software, using the Apache license, see file LICENSE
+Copyright 2014 Guillaume Bury
+Copyright 2014 Simon Cruanes
+*)
+
+(** Tseitin CNF conversion
+
+    This modules implements Tseitin's Conjunctive Normal Form conversion, i.e.
+    the ability to transform an arbitrary boolean formula into an equi-satisfiable
+    CNF, that can then be fed to a SAT/SMT/McSat solver.
+*)
+
+module type Arg = Tseitin_intf.Arg
+(** The implementation of formulas required to implement Tseitin's CNF conversion. *)
+
+module type S = Tseitin_intf.S
+(** The exposed interface of Tseitin's CNF conversion. *)
+
+module Make : functor (F : Arg) -> S with type atom = F.t
+(** This functor provides an implementation of Tseitin's CNF conversion. *)
+
diff --git a/src/sat/src/tseitin/Tseitin_intf.ml b/src/sat/src/tseitin/Tseitin_intf.ml
new file mode 100644
index 00000000..99805c35
--- /dev/null
+++ b/src/sat/src/tseitin/Tseitin_intf.ml
@@ -0,0 +1,85 @@
+(**************************************************************************)
+(*                                                                        *)
+(*                          Alt-Ergo Zero                                 *)
+(*                                                                        *)
+(*                  Sylvain Conchon and Alain Mebsout                     *)
+(*                      Universite Paris-Sud 11                           *)
+(*                                                                        *)
+(*  Copyright 2011. This file is distributed under the terms of the       *)
+(*  Apache Software License version 2.0                                   *)
+(*                                                                        *)
+(**************************************************************************)
+
+(** Interfaces for Tseitin's CNF conversion *)
+
+module type Arg = sig
+  (** Formulas
+
+      This defines what is needed of formulas in order to implement
+      Tseitin's CNF conversion.
+  *)
+
+  type t
+  (** Type of atomic formulas. *)
+
+  val neg : t -> t
+  (** Negation of atomic formulas. *)
+
+  val fresh : unit -> t
+  (** Generate fresh formulas (that are different from any other). *)
+
+  val pp : Format.formatter -> t -> unit
+  (** Print the given formula. *)
+
+end
+
+module type S = sig
+  (** CNF conversion
+
+      This modules converts arbitrary boolean formulas into CNF.
+  *)
+
+  type atom
+  (** The type of atomic formulas. *)
+
+  type t
+  (** The type of arbitrary boolean formulas. Arbitrary boolean formulas
+      can be built using functions in this module, and then converted
+      to a CNF, which is a list of clauses that only use atomic formulas. *)
+
+  val f_true : t
+  (** The [true] formula, i.e a formula that is always satisfied. *)
+
+  val f_false : t
+  (** The [false] formula, i.e a formula that cannot be satisfied. *)
+
+  val make_atom : atom -> t
+  (** [make_atom p] builds the boolean formula equivalent to the atomic formula [p]. *)
+
+  val make_not : t -> t
+  (** Creates the negation of a boolean formula. *)
+
+  val make_and : t list -> t
+  (** Creates the conjunction of a list of formulas. An empty conjunction is always satisfied. *)
+
+  val make_or : t list -> t
+  (** Creates the disjunction of a list of formulas. An empty disjunction is never satisfied. *)
+
+  val make_xor : t -> t -> t
+  (** [make_xor p q] creates the boolean formula "[p] xor [q]". *)
+
+  val make_imply : t -> t -> t
+  (** [make_imply p q] creates the boolean formula "[p] implies [q]". *)
+
+  val make_equiv : t -> t -> t
+  (** [make_equiv p q] creates the boolena formula "[p] is equivalent to [q]". *)
+
+  val make_cnf : t -> atom list list
+  (** [make_cnf f] returns a conjunctive normal form of [f] under the form: a
+      list (which is a conjunction) of lists (which are disjunctions) of
+      atomic formulas. *)
+
+  val pp : Format.formatter -> t -> unit
+  (** [print fmt f] prints the formula on the formatter [fmt].*)
+
+end
diff --git a/src/sat/src/tseitin/dune b/src/sat/src/tseitin/dune
new file mode 100644
index 00000000..0a35225d
--- /dev/null
+++ b/src/sat/src/tseitin/dune
@@ -0,0 +1,11 @@
+
+(library
+  (name msat_tseitin)
+  (public_name msat.tseitin)
+  (synopsis "Tseitin transformation 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)
+  )
+