diff --git a/README.md b/README.md
index c89dd631..6dbcca2d 100644
--- a/README.md
+++ b/README.md
@@ -6,11 +6,6 @@ extensions (including SMT). This is *work in progress*.
 
 It derives from [Alt-Ergo Zero](http://cubicle.lri.fr/alt-ergo-zero).
 
-The following theories should be supported:
-
-- Equality and uninterpreted functions
-- Arithmetic (linear, non-linear, integer, real)
-- Enumerated data-types
 
 ## COPYRIGHT
 
@@ -18,6 +13,32 @@ This program is distributed under the Apache Software License version
 2.0. See the enclosed file `LICENSE`.
 
 
+## USAGE
+
+A ready-to-use SAT solver is available in the Sat module. It can be used
+as shown in the following code :
+
+    (* Module initialization *)
+    module F = Msat.Sat.Tseitin
+    module Sat = Msat.Sat.Make(Msat.Log)
+
+    (* We create here two distinct atoms *)
+    let a = Sat.new_atom () (* A 'new_atom' is always distinct from any other atom *)
+    let b = Sat.make 1      (* Atoms can be creted from integers *)
+
+    (* Let's create some formulas *)
+    let p = F.make_and [a; b]
+    let q = F.make_or [F.make_not a; F.make_not b]
+
+    (* We can try and check the satisfiability of the given formulas *)
+    Sat.assume (F.make_cnf p)
+    let _ = Sat.solve ()        (* Should return Sat.Sat *)
+
+    (* The Sat solver has an incremental mutable state, so we still have
+     * the formula 'p' in our assumptions *)
+    Sat.assume (F.make_cnf q)
+    let _ = Sat.solve ()        (* Should return Sat.Unsat *)
+
 ## INSTALLATION
 
 ### Via opam
diff --git a/msat.odocl b/msat.odocl
index 72538d43..08fe2c1f 100644
--- a/msat.odocl
+++ b/msat.odocl
@@ -18,6 +18,7 @@ solver/Mcsolver_types_intf
 solver/Theory_intf
 solver/Plugin_intf
 
-#sat/Sat
-#smt/Smt
-#smt/Mcsat
+solver/Tseitin
+solver/Tseitin_intf
+
+sat/Sat
diff --git a/smt/smt.mli b/smt/smt.mli
index a089b513..bbc9a05b 100644
--- a/smt/smt.mli
+++ b/smt/smt.mli
@@ -5,7 +5,7 @@ Copyright 2014 Simon Cruanes
 *)
 
 module Make(Dummy: sig end) : sig
-  (** Fonctor to make a pure SAT Solver module with built-in literals. *)
+  (** Fonctor to make a SMT Solver module with built-in literals. *)
 
   type atom = Expr.Formula.t
   (** Type for atoms, i.e boolean literals. *)
diff --git a/solver/formula_intf.ml b/solver/formula_intf.ml
index 712b9566..044f1ac2 100644
--- a/solver/formula_intf.ml
+++ b/solver/formula_intf.ml
@@ -5,7 +5,7 @@ Copyright 2014 Simon Cruanes
 *)
 
 module type S = sig
-  (** Signature of formulas that parametrises the SMT Solver Module. *)
+  (** Signature of formulas that parametrises the SAT/SMT Solver Module. *)
 
   type t
   (** The type of atomic formulas. *)