diff --git a/README.md b/README.md
index 754f1b84..0991d8b9 100644
--- a/README.md
+++ b/README.md
@@ -45,7 +45,14 @@ as shown in the following code :
 
 ### Generic SAT/SMT Solver
 
-A modular implementation of the SMT algorithm can be found in the `Msat.`
+A modular implementation of the SMT algorithm can be found in the `Msat.Solver` module,
+as a functor which takes three modules :
+
+  - A log module for debug output
+
+  - 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.
 
 ## INSTALLATION