diff --git a/.merlin b/.merlin
index 6457aa65..cfd63256 100644
--- a/.merlin
+++ b/.merlin
@@ -2,6 +2,7 @@ S src/core
 S src/solver
 S src/sat
 S src/smt
+S src/mcsat
 S src/backend
 S src/util
 S tests
@@ -11,6 +12,7 @@ B _build/src/core
 B _build/src/solver
 B _build/src/sat
 B _build/src/smt
+B _build/src/mcsat
 B _build/src/util
 B _build/src/backend
 B _build/tests
diff --git a/_tags b/_tags
index e737cd45..3714ec07 100644
--- a/_tags
+++ b/_tags
@@ -23,6 +23,8 @@ true: inline(100), optimize(3), unbox_closures, unbox_closures_factor(20)
 # Testing dependencies
 <src/main.*>: package(dolmen)
 <src/util/type.*>: package(dolmen)
+<src/sat/type_sat.*>: package(dolmen)
+<src/smt/type_smt.*>: package(dolmen)
 
 # more warnings
 <src/**/*.ml>: warn_K, warn_Y, warn_X
diff --git a/src/main.ml b/src/main.ml
index 3ce4dd3f..0dbc9031 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -4,28 +4,77 @@ Copyright 2014 Guillaume Bury
 Copyright 2014 Simon Cruanes
 *)
 
-module Sat = Sat.Make(struct end)
-module Smt = Smt.Make(struct end)
-module Mcsat = Mcsat.Make(struct end)
+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_proof_print = ref false
+let p_unsat_core = ref false
+let time_limit = ref 300.
+let size_limit = ref 1000_000_000.
 
 module P =
   Dolmen.Logic.Make(Dolmen.ParseLocation)
     (Dolmen.Id)(Dolmen.Term)(Dolmen.Statement)
 
-exception Incorrect_model
-exception Out_of_time
-exception Out_of_space
+module type S = sig
+  val do_task : Dolmen.Statement.t -> unit
+end
 
-type solver =
-  | Sat
-  | Smt
-  | Mcsat
+module Make
+    (S : External.S)
+    (T : Type.S with type atom := S.atom)
+= struct
 
-let solver = ref Smt
+  let hyps = ref []
+
+  let do_task s =
+    match s.Dolmen.Statement.descr with
+    | Dolmen.Statement.Def (id, t) -> T.def id t
+    | Dolmen.Statement.Decl (id, t) -> T.decl id t
+    | Dolmen.Statement.Consequent t ->
+      let cnf = T.consequent t in
+      hyps := cnf @ !hyps;
+      S.assume cnf
+    | Dolmen.Statement.Antecedent t ->
+      let cnf = T.antecedent t in
+      hyps := cnf @ !hyps;
+      S.assume cnf
+    | Dolmen.Statement.Prove ->
+      let res = S.solve () in
+      let t = Sys.time () in
+      begin match res with
+        | S.Sat state ->
+          if !p_check then
+            if not (List.for_all (List.exists state.Solver_intf.eval) !hyps) then
+              raise Incorrect_model;
+          let t' = Sys.time () -. t in
+          Format.printf "Sat (%f/%f)@." t t'
+        | S.Unsat state ->
+          if !p_check then begin
+            let p = state.Solver_intf.get_proof () in
+            S.Proof.check p;
+          end;
+          let t' = Sys.time () -. t in
+          Format.printf "Unsat (%f/%f)@." t t'
+      end
+    | _ ->
+      Format.printf "Command not supported:@\n%a@."
+        Dolmen.Statement.print s
+end
+
+module Sat = Make(Sat.Make(struct end))(Type_sat)
+module Smt = Make(Smt.Make(struct end))(Type_smt)
+module Mcsat = Make(Mcsat.Make(struct end))(Type_smt)
+
+let solver = ref (module Sat : S)
 let solver_list = [
-  "sat", Sat;
-  "smt", Smt;
-  "mcsat", Mcsat;
+  "sat", (module Sat : S);
+  "smt", (module Smt : S);
+  "mcsat", (module Mcsat : S);
 ]
 
 let error_msg opt arg l =
@@ -42,14 +91,6 @@ let set_flag opt arg flag l =
 let set_solver s = set_flag "Solver" s solver solver_list
 
 (* Arguments parsing *)
-let file = ref ""
-let p_cnf = ref false
-let p_check = ref false
-let p_proof_print = ref false
-let p_unsat_core = ref false
-let time_limit = ref 300.
-let size_limit = ref 1000_000_000.
-
 let int_arg r arg =
   let l = String.length arg in
   let multiplier m =
@@ -111,30 +152,6 @@ let check () =
   else if s > !size_limit then
     raise Out_of_space
 
-module Make
-    (T : Type.S)
-    (S : External.S with type St.formula = T.atom) = struct
-
-  let do_task s =
-    match s.Dolmen.Statement.descr with
-    | Dolmen.Statement.Def (id, t) -> T.def id t
-    | Dolmen.Statement.Decl (id, t) -> T.decl id t
-    | Dolmen.Statement.Consequent t ->
-      let cnf = T.consequent t in
-      S.assume cnf
-    | Dolmen.Statement.Antecedent t ->
-      let cnf = T.antecedent t in
-      S.assume cnf
-    | Dolmen.Statement.Prove ->
-      begin match S.solve () with
-        | S.Sat _ -> ()
-        | S.Unsat _ -> ()
-      end
-    | _ ->
-      Format.printf "Command not supported:@\n%a@."
-        Dolmen.Statement.print s
-end
-
 
 let main () =
   (* Administrative duties *)
@@ -146,73 +163,35 @@ let main () =
   let al = Gc.create_alarm check in
 
   (* Interesting stuff happening *)
-  let _, _input = P.parse_file !file in
+  let lang, input = P.parse_file !file in
+  let module S = (val !solver : S) in
+  List.iter S.do_task input;
+  (* Small hack for dimacs, which do not output a "Prove" statement *)
+  begin match lang with
+    | P.Dimacs -> S.do_task @@ Dolmen.Statement.check_sat ()
+    | _ -> ()
+  end;
   Gc.delete_alarm al;
   ()
 
-(* Old code ...
-
-   let cnf = get_cnf () in
-   if !p_cnf then
-   print_cnf cnf;
-   match !solver with
-   | Smt ->
-   Smt.assume cnf;
-   let res = Smt.solve () in
-   Gc.delete_alarm al;
-   begin match res with
-    | Smt.Sat sat ->
-      let t = Sys.time () in
-      if !p_check then
-        if not (List.for_all (List.exists sat.Solver_intf.eval) cnf) then
-          raise Incorrect_model;
-      print "Sat (%f/%f)" t (Sys.time () -. t)
-    | Smt.Unsat us ->
-      let t = Sys.time () in
-      if !p_check then begin
-        let p = us.Solver_intf.get_proof () in
-        Smt.Proof.check p;
-        print_proof p;
-        if !p_unsat_core then
-          print_unsat_core (Smt.unsat_core p)
-      end;
-      print "Unsat (%f/%f)" t (Sys.time () -. t)
-   end
-   | Mcsat ->
-   Mcsat.assume cnf;
-   let res = Mcsat.solve () in
-   begin match res with
-    | Mcsat.Sat sat ->
-      let t = Sys.time () in
-      if !p_check then
-        if not (List.for_all (List.exists sat.Solver_intf.eval) cnf) then
-          raise Incorrect_model;
-      print "Sat (%f/%f)" t (Sys.time () -. t)
-    | Mcsat.Unsat us ->
-      let t = Sys.time () in
-      if !p_check then begin
-        let p = us.Solver_intf.get_proof () in
-        Mcsat.Proof.check p;
-        print_mcproof p;
-        if !p_unsat_core then
-          print_mc_unsat_core (Mcsat.unsat_core p)
-      end;
-      print "Unsat (%f/%f)" t (Sys.time () -. t)
-   end
-
-*)
-
 let () =
   try
     main ()
   with
-  | Incorrect_model ->
-    Format.printf "Internal error : incorrect *sat* model@.";
-    exit 4
   | 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
+  | Type_sat.Typing_error (msg, t)
+  | Type_smt.Typing_error (msg, t) ->
+    let loc = match t.Dolmen.Term.loc with
+      | Some l -> l | None -> Dolmen.ParseLocation.mk "<>" 0 0 0 0
+    in
+    Format.fprintf Format.std_formatter "While typing:@\n%a@\n%a: typing error\n%s@."
+      Dolmen.Term.print t Dolmen.ParseLocation.fmt loc msg
 
diff --git a/src/sat/expr_sat.mli b/src/sat/expr_sat.mli
index f4b72e48..4e1b70ab 100644
--- a/src/sat/expr_sat.mli
+++ b/src/sat/expr_sat.mli
@@ -6,3 +6,6 @@ Copyright 2016 Simon Cruanes
 
 include Formula_intf.S
 
+val make : int -> t
+(** Make a proposition from an integer. *)
+
diff --git a/src/sat/type_sat.ml b/src/sat/type_sat.ml
new file mode 100644
index 00000000..6689f7f6
--- /dev/null
+++ b/src/sat/type_sat.ml
@@ -0,0 +1,73 @@
+
+(* Log&Module Init *)
+(* ************************************************************************ *)
+
+module Id = Dolmen.Id
+module Ast = Dolmen.Term
+module H = Hashtbl.Make(Id)
+module Formula = Tseitin.Make(Expr_sat)
+
+(* Exceptions *)
+(* ************************************************************************ *)
+
+exception Typing_error of string * Dolmen.Term.t
+
+(* Identifiers *)
+(* ************************************************************************ *)
+
+let symbols = H.create 42
+
+let find_id id =
+  try
+    H.find symbols id
+  with Not_found ->
+    let res = Expr_sat.fresh () in
+    H.add symbols id res;
+    res
+
+(* Actual parsing *)
+(* ************************************************************************ *)
+
+let rec parse = function
+  | { Ast.term = Ast.Builtin Ast.True } ->
+    Formula.f_true
+  | { Ast.term = Ast.Builtin Ast.False } ->
+    Formula.f_false
+  | { Ast.term = Ast.Symbol id } ->
+    let s = find_id id in
+    Formula.make_atom s
+  | { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Not }, [p]) }
+  | { Ast.term = Ast.App ({Ast.term = Ast.Symbol { Id.name = "not" } }, [p]) } ->
+    Formula.make_not (parse p)
+  | { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.And }, l) }
+  | { Ast.term = Ast.App ({Ast.term = Ast.Symbol { Id.name = "and" } }, l) } ->
+    Formula.make_and (List.map parse l)
+  | { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Or }, l) }
+  | { Ast.term = Ast.App ({Ast.term = Ast.Symbol { Id.name = "or" } }, l) } ->
+    Formula.make_or (List.map parse l)
+  | { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Imply }, [p; q]) } ->
+    Formula.make_imply (parse p) (parse q)
+  | { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Equiv }, [p; q]) } ->
+    Formula.make_equiv (parse p) (parse q)
+  | { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Xor }, [p; q]) } ->
+    Formula.make_xor (parse p) (parse q)
+  | t ->
+    raise (Typing_error ("Term is not a pure proposition", t))
+
+(* Exported functions *)
+(* ************************************************************************ *)
+
+let decl _ t =
+  raise (Typing_error ("Declarations are not allowed in pure sat", t))
+
+let def _ t =
+  raise (Typing_error ("Definitions are not allowed in pure sat", t))
+
+let antecedent t =
+  let f = parse t in
+  Formula.make_cnf f
+
+let consequent t =
+  let f = parse t in
+  Formula.make_cnf @@ Formula.make_not f
+
diff --git a/src/sat/type_sat.mli b/src/sat/type_sat.mli
new file mode 100644
index 00000000..6d295a52
--- /dev/null
+++ b/src/sat/type_sat.mli
@@ -0,0 +1,7 @@
+
+(** Typechecking of terms from Dolmen.Term.t
+    This module provides functions to parse terms from the untyped syntax tree
+    defined in Dolmen, and generate formulas as defined in the Expr_sat module. *)
+
+include Type.S with type atom := Expr_sat.t
+
diff --git a/src/smt/expr_smt.ml b/src/smt/expr_smt.ml
index 9270d741..5fb8acfe 100644
--- a/src/smt/expr_smt.ml
+++ b/src/smt/expr_smt.ml
@@ -133,8 +133,11 @@ module Print = struct
 
   let atom_aux fmt f =
     match f.atom with
-    | Equal (a, b) -> Format.fprintf fmt "%a = %a" term a term b
-    | Pred t -> Format.fprintf fmt "%a" term t
+    | Equal (a, b) ->
+      Format.fprintf fmt "%a %s %a"
+        term a (if f.sign then "=" else "<>") term b
+    | Pred t ->
+      Format.fprintf fmt "%s%a" (if f.sign then "" else "¬ ") term t
 
   let atom fmt f = Format.fprintf fmt "⟦%a⟧" atom_aux f
 
diff --git a/src/smt/type_smt.ml b/src/smt/type_smt.ml
index 65127dcf..529cff89 100644
--- a/src/smt/type_smt.ml
+++ b/src/smt/type_smt.ml
@@ -6,6 +6,7 @@ module Ast = Dolmen.Term
 module Id = Dolmen.Id
 module M = Map.Make(Id)
 module H = Hashtbl.Make(Id)
+module Expr = Expr_smt
 
 (* Types *)
 (* ************************************************************************ *)
@@ -287,6 +288,9 @@ let infer env s args =
 
 let rec parse_expr (env : env) t =
   match t with
+  (* Base Type *)
+  | { Ast.term = Ast.Symbol { Id.name = "Bool" } } ->
+    Ty (Expr_smt.Ty.prop)
 
   (* Basic formulas *)
   | { Ast.term = Ast.App ({ Ast.term = Ast.Builtin Ast.True }, []) }
@@ -297,10 +301,12 @@ let rec parse_expr (env : env) t =
   | { Ast.term = Ast.Builtin Ast.False } ->
     Formula Expr.Formula.f_false
 
-  | { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.And}, l) } ->
+  | { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.And}, l) }
+  | { Ast.term = Ast.App ({Ast.term = Ast.Symbol { Id.name = "and" }}, l) } ->
     Formula (Expr.Formula.make_and (List.map (parse_formula env) l))
 
-  | { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Or}, l) } ->
+  | { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Or}, l) }
+  | { Ast.term = Ast.App ({Ast.term = Ast.Symbol { Id.name = "or" }}, l) } ->
     Formula (Expr.Formula.make_or (List.map (parse_formula env) l))
 
   | { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Xor}, l) } as t ->
@@ -330,7 +336,8 @@ let rec parse_expr (env : env) t =
       | _ -> _bad_arity "<=>" 2 t
     end
 
-  | { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Not}, l) } as t ->
+  | ({ Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Not}, l) } as t)
+  | ({ Ast.term = Ast.App ({Ast.term = Ast.Symbol { Id.name = "not" }}, l) } as t) ->
     begin match l with
       | [p] ->
         Formula (Expr.Formula.make_not (parse_formula env p))
@@ -338,7 +345,8 @@ let rec parse_expr (env : env) t =
     end
 
   (* (Dis)Equality *)
-  | { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Eq}, l) } as t ->
+  | ({ Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Eq}, l) } as t)
+  | ({ Ast.term = Ast.App ({Ast.term = Ast.Symbol { Id.name = "=" }}, l) } as t) ->
     begin match l with
       | [a; b] ->
         Formula (
@@ -607,9 +615,9 @@ let formula t =
   Log.debugf 5 "Typing top-level formula: %a" (fun k -> k Ast.print t);
   parse_formula env t
 
-let consequent t =
+let antecedent t =
   Expr.Formula.make_cnf (formula t)
 
-let antecedent t =
+let consequent t =
   Expr.Formula.make_cnf (Expr.Formula.make_not (formula t))
 
diff --git a/src/smt/type_smt.mli b/src/smt/type_smt.mli
index 3a2429c4..51957bc8 100644
--- a/src/smt/type_smt.mli
+++ b/src/smt/type_smt.mli
@@ -1,7 +1,7 @@
 
 (** Typechecking of terms from Dolmen.Term.t
     This module provides functions to parse terms from the untyped syntax tree
-    defined in Dolmen, and generate formulas as defined in the Expr module. *)
+    defined in Dolmen, and generate formulas as defined in the Expr_smt module. *)
 
-include Type.S with type atom = Expr.atom
+include Type.S with type atom := Expr_smt.Atom.t
 
diff --git a/tests/test_api.ml b/tests/test_api.ml
index 74f36e37..75ae7fd2 100644
--- a/tests/test_api.ml
+++ b/tests/test_api.ml
@@ -6,18 +6,11 @@ Copyright 2014 Simon Cruanes
 
 (* Tests that require the API *)
 
-module F = Expr
-module T = Cnf.S
+module F = Expr_sat
+module T = Tseitin.Make(F)
 
 let (|>) x f = f x
 
-type solver = Smt | Mcsat
-let solver_list = [
-  "smt", Smt;
-  "mcsat", Mcsat;
-]
-
-let solver = ref Smt
 let p_check = ref false
 let time_limit = ref 300.
 let size_limit = ref 1000_000_000.
@@ -32,59 +25,38 @@ let set_flag opt arg flag l =
     flag := List.assoc arg l
   with Not_found ->
     invalid_arg (error_msg opt arg l)
-let set_solver s = set_flag "Solver" s solver solver_list
 
 let usage = "Usage : test_api [options]"
 let argspec = Arg.align [
     "-check", Arg.Set p_check,
     " Build, check and print the proof (if output is set), if unsat";
-    "-s", Arg.String set_solver,
-    "{smt,mcsat} Sets the solver to use (default smt)";
     "-v", Arg.Int (fun i -> Log.set_debug i),
     "<lvl> Sets the debug verbose level";
   ]
 
-let string_of_solver = function
-  | Mcsat -> "mcsat"
-  | Smt -> "smt"
-
 type solver_res =
   | R_sat
   | R_unsat
 
+exception Incorrect_model
+
 module type BASIC_SOLVER = sig
   val solve : ?assumptions:F.t list -> unit -> solver_res
   val assume : ?tag:int -> F.t list list -> unit
 end
 
-exception Incorrect_model
-
-let mk_solver (s:solver): (module BASIC_SOLVER) =
-  match s with
-    | Smt ->
-      let module S = struct
-        include Smt.Make(struct end)
-        let solve ?assumptions ()= match solve ?assumptions() with
-          | Sat _ ->
-            R_sat
-          | Unsat us ->
-            let p = us.Solver_intf.get_proof () in
-            Proof.check p;
-            R_unsat
-      end
-      in (module S)
-    | Mcsat ->
-      let module S = struct
-        include Mcsat.Make(struct end)
-        let solve ?assumptions ()= match solve ?assumptions() with
-          | Sat _ ->
-            R_sat
-          | Unsat us ->
-            let p = us.Solver_intf.get_proof () in
-            Proof.check p;
-            R_unsat
-      end
-      in (module S)
+let mk_solver (): (module BASIC_SOLVER) =
+  let module S = struct
+    include Sat.Make(struct end)
+    let solve ?assumptions ()= match solve ?assumptions() with
+      | Sat _ ->
+        R_sat
+      | Unsat us ->
+        let p = us.Solver_intf.get_proof () in
+        Proof.check p;
+        R_unsat
+  end
+  in (module S)
 
 exception Error of string
 
@@ -102,19 +74,19 @@ module Test = struct
   }
 
   let mk_test name l = {name; actions=l}
-  let assume l = A_assume (List.map (List.map F.mk_prop) l)
+  let assume l = A_assume (List.map (List.map F.make) l)
   let assume1 c = assume [c]
   let solve ?(assumptions=[]) e =
-    let assumptions = List.map F.mk_prop assumptions in
+    let assumptions = List.map F.make assumptions in
     A_solve (assumptions, e)
 
   type result =
     | Pass
     | Fail of string
 
-  let run (solver:solver) (t:t): result =
+  let run (t:t): result =
   (* Interesting stuff happening *)
-    let (module S: BASIC_SOLVER) = mk_solver solver in
+    let (module S: BASIC_SOLVER) = mk_solver () in
     try
       List.iter
         (function
@@ -190,17 +162,14 @@ let main () =
   Arg.parse argspec (fun _ -> ()) usage;
   let failed = ref false in
   List.iter
-    (fun solver ->
-       List.iter
-         (fun test ->
-            Printf.printf "(%-6s) %-10s... %!" (string_of_solver solver) test.Test.name;
-            match Test.run solver test with
-              | Test.Pass -> Printf.printf "ok\n%!"
-              | Test.Fail msg ->
-                failed := true;
-                Printf.printf "fail (%s)\n%!" msg)
-         Test.suite)
-    [Smt; Mcsat];
+    (fun test ->
+       Printf.printf "%-10s... %!" test.Test.name;
+       match Test.run test with
+       | Test.Pass -> Printf.printf "ok\n%!"
+       | Test.Fail msg ->
+         failed := true;
+         Printf.printf "fail (%s)\n%!" msg)
+    Test.suite;
   if !failed then exit 1
 
 let () = main()