Initial import of SMTCoq v1.2

11 files changed, 2755 insertions, 0 deletions

diff --git a/src/trace/coqTerms.ml b/src/trace/coqTerms.ml
new file mode 100644
index 0000000..1ee6448
--- /dev/null
+++ b/src/trace/coqTerms.ml
@@ -0,0 +1,187 @@
+(**************************************************************************)
+(*                                                                        *)
+(*     SMTCoq                                                             *)
+(*     Copyright (C) 2011 - 2015                                          *)
+(*                                                                        *)
+(*     Michaël Armand                                                     *)
+(*     Benjamin Grégoire                                                  *)
+(*     Chantal Keller                                                     *)
+(*                                                                        *)
+(*     Inria - École Polytechnique - MSR-Inria Joint Lab                  *)
+(*                                                                        *)
+(*   This file is distributed under the terms of the CeCILL-C licence     *)
+(*                                                                        *)
+(**************************************************************************)
+
+open Coqlib
+
+let gen_constant modules constant = lazy (gen_constant_in_modules "SMT" modules constant)
+
+(* Int63 *)
+let int63_modules = [["Coq";"Numbers";"Cyclic";"Int63";"Int63Native"]]
+
+let cint = gen_constant int63_modules "int"
+let ceq63 = gen_constant int63_modules "eqb"
+
+(* PArray *)
+let parray_modules = [["Coq";"Array";"PArray"]]
+
+let carray = gen_constant parray_modules "array"
+
+(* Positive *)
+let positive_modules = [["Coq";"Numbers";"BinNums"];
+                        ["Coq";"PArith";"BinPosDef";"Pos"]]
+
+let cpositive = gen_constant positive_modules "positive"
+let cxI = gen_constant positive_modules "xI"
+let cxO = gen_constant positive_modules "xO"
+let cxH = gen_constant positive_modules "xH"
+let ceqbP = gen_constant positive_modules "eqb"
+
+(* Z *)
+let z_modules = [["Coq";"Numbers";"BinNums"];
+                 ["Coq";"ZArith";"BinInt"];
+                 ["Coq";"ZArith";"BinInt";"Z"]]
+
+let cZ = gen_constant z_modules "Z"
+let cZ0 = gen_constant z_modules "Z0"
+let cZpos = gen_constant z_modules "Zpos"
+let cZneg = gen_constant z_modules "Zneg"
+let copp = gen_constant z_modules "opp"
+let cadd = gen_constant z_modules "add"
+let csub = gen_constant z_modules "sub"
+let cmul = gen_constant z_modules "mul"
+let cltb = gen_constant z_modules "ltb"
+let cleb = gen_constant z_modules "leb"
+let cgeb = gen_constant z_modules "geb"
+let cgtb = gen_constant z_modules "gtb"
+(* Je ne comprends pas pourquoi ça fonctionne avec Zeq_bool et pas avec
+   Z.eqb *)
+(* let ceqbZ = gen_constant z_modules "eqb" *)
+let ceqbZ = gen_constant [["Coq";"ZArith";"Zbool"]] "Zeq_bool"
+
+(* Booleans *)
+let bool_modules = [["Coq";"Bool";"Bool"]]
+
+let cbool = gen_constant init_modules "bool"
+let ctrue = gen_constant init_modules "true"
+let cfalse = gen_constant init_modules "false"
+let candb = gen_constant init_modules "andb"
+let corb = gen_constant init_modules "orb"
+let cxorb = gen_constant init_modules "xorb"
+let cnegb = gen_constant init_modules "negb"
+let cimplb = gen_constant init_modules "implb"
+let ceqb = gen_constant  bool_modules "eqb"
+let cifb = gen_constant bool_modules "ifb"
+let creflect = gen_constant bool_modules "reflect"
+
+(* Lists *)
+let clist = gen_constant init_modules "list"
+let cnil = gen_constant init_modules "nil"
+let ccons = gen_constant init_modules "cons"
+
+
+(* Option *)
+let coption = gen_constant init_modules "option"
+let cSome = gen_constant init_modules "Some"
+let cNone = gen_constant init_modules "None"
+
+(* Pairs *)
+let cpair = gen_constant init_modules "pair"
+
+(* Logical Operators *)
+let cnot = gen_constant init_modules "not"
+let ceq = gen_constant init_modules "eq"
+let crefl_equal = gen_constant init_modules "eq_refl"
+
+(* SMT_terms *)
+
+let smt_modules = [ ["SMTCoq";"Misc"];
+		    ["SMTCoq";"State"];
+		    ["SMTCoq";"SMT_terms"];
+		    ["SMTCoq";"SMT_terms";"Typ"];
+		    ["SMTCoq";"SMT_terms";"Form"];
+		    ["SMTCoq";"SMT_terms";"Atom"]
+		  ]
+
+let cdistinct = gen_constant smt_modules "distinct"
+
+let ctype = gen_constant smt_modules "type"
+let cTZ = gen_constant smt_modules "TZ"
+let cTbool = gen_constant smt_modules "Tbool"
+let cTpositive = gen_constant smt_modules "Tpositive"
+let cTindex = gen_constant smt_modules "Tindex"
+
+let ctyp_eqb = gen_constant smt_modules "typ_eqb"
+let cTyp_eqb = gen_constant smt_modules "Typ_eqb"
+let cte_carrier = gen_constant smt_modules "te_carrier"
+let cte_eqb = gen_constant smt_modules "te_eqb"
+let cunit_typ_eqb = gen_constant smt_modules "unit_typ_eqb"
+
+let ctval =  gen_constant smt_modules "tval"
+let cTval =  gen_constant smt_modules "Tval"
+
+let cCO_xH = gen_constant smt_modules "CO_xH"
+let cCO_Z0 = gen_constant smt_modules "CO_Z0"
+
+let cUO_xO = gen_constant smt_modules "UO_xO"
+let cUO_xI = gen_constant smt_modules "UO_xI"
+let cUO_Zpos = gen_constant smt_modules "UO_Zpos"
+let cUO_Zneg = gen_constant smt_modules "UO_Zneg"
+let cUO_Zopp = gen_constant smt_modules "UO_Zopp"
+
+let cBO_Zplus = gen_constant smt_modules "BO_Zplus"
+let cBO_Zminus = gen_constant smt_modules "BO_Zminus"
+let cBO_Zmult = gen_constant smt_modules "BO_Zmult"
+let cBO_Zlt = gen_constant smt_modules "BO_Zlt"
+let cBO_Zle = gen_constant smt_modules "BO_Zle"
+let cBO_Zge = gen_constant smt_modules "BO_Zge"
+let cBO_Zgt = gen_constant smt_modules "BO_Zgt"
+let cBO_eq = gen_constant smt_modules "BO_eq"
+
+let cNO_distinct = gen_constant smt_modules "NO_distinct"
+
+let catom = gen_constant smt_modules "atom"
+let cAcop = gen_constant smt_modules "Acop"
+let cAuop = gen_constant smt_modules "Auop"
+let cAbop = gen_constant smt_modules "Abop"
+let cAnop = gen_constant smt_modules "Anop"
+let cAapp = gen_constant smt_modules "Aapp"
+
+let cform  = gen_constant smt_modules "form"
+let cFatom = gen_constant smt_modules "Fatom"
+let cFtrue = gen_constant smt_modules "Ftrue"
+let cFfalse = gen_constant smt_modules "Ffalse"
+let cFnot2 = gen_constant smt_modules "Fnot2"
+let cFand = gen_constant smt_modules "Fand"
+let cFor = gen_constant smt_modules "For"
+let cFxor = gen_constant smt_modules "Fxor"
+let cFimp = gen_constant smt_modules "Fimp"
+let cFiff = gen_constant smt_modules "Fiff"
+let cFite = gen_constant smt_modules "Fite"
+
+let cis_true = gen_constant smt_modules "is_true"
+
+let make_certif_ops modules = 
+ (gen_constant modules "step", 
+  gen_constant modules "Res", gen_constant modules "ImmFlatten", 
+  gen_constant modules "CTrue", gen_constant modules "CFalse", 
+  gen_constant modules "BuildDef", gen_constant modules "BuildDef2", 
+  gen_constant modules "BuildProj", 
+  gen_constant modules "ImmBuildProj", gen_constant modules"ImmBuildDef", 
+  gen_constant modules"ImmBuildDef2",
+  gen_constant modules "EqTr", gen_constant modules "EqCgr", gen_constant modules "EqCgrP", 
+  gen_constant modules "LiaMicromega", gen_constant modules "LiaDiseq", gen_constant modules "SplArith", gen_constant modules "SplDistinctElim")
+  
+
+(** Usefull construction *)
+
+let ceq_refl_true = 
+  lazy (SmtMisc.mklApp crefl_equal [|Lazy.force cbool;Lazy.force ctrue|])
+
+let eq_refl_true () = Lazy.force ceq_refl_true
+
+let vm_cast_true t = 
+  Term.mkCast(eq_refl_true (),
+	      Term.VMcast, 
+	      SmtMisc.mklApp ceq [|Lazy.force cbool; t; Lazy.force ctrue|])
diff --git a/src/trace/satAtom.ml b/src/trace/satAtom.ml
new file mode 100644
index 0000000..ca72504
--- /dev/null
+++ b/src/trace/satAtom.ml
@@ -0,0 +1,65 @@
+(**************************************************************************)
+(*                                                                        *)
+(*     SMTCoq                                                             *)
+(*     Copyright (C) 2011 - 2015                                          *)
+(*                                                                        *)
+(*     Michaël Armand                                                     *)
+(*     Benjamin Grégoire                                                  *)
+(*     Chantal Keller                                                     *)
+(*                                                                        *)
+(*     Inria - École Polytechnique - MSR-Inria Joint Lab                  *)
+(*                                                                        *)
+(*   This file is distributed under the terms of the CeCILL-C licence     *)
+(*                                                                        *)
+(**************************************************************************)
+
+open SmtMisc
+open CoqTerms
+
+module Atom = 
+  struct 
+
+    type t = int 
+
+    let index a = a
+
+    let equal a1 a2 = a1 == a2
+
+    let is_bool_type a = true
+
+    type reify_tbl =
+        { mutable count : int;
+	          tbl : (Term.constr, int) Hashtbl.t 
+	}
+
+    let create () = 
+      { count = 0;
+	tbl =  Hashtbl.create 17 }
+
+    let declare reify a = 
+      let res = reify.count in
+      Hashtbl.add reify.tbl a res;
+      reify.count <- res + 1;
+      res
+
+    let get reify a =
+      try Hashtbl.find reify.tbl a 
+      with Not_found -> declare reify a
+
+    let atom_tbl reify =
+      let t = Array.make (reify.count + 1) (Lazy.force ctrue) in
+      let set c i = t.(i) <- c in
+      Hashtbl.iter set reify.tbl;
+      t
+
+    let interp_tbl reify =
+      Term.mkArray (Lazy.force cbool, atom_tbl reify)
+
+  end
+
+module Form = SmtForm.Make(Atom)
+module Trace = SmtTrace.MakeOpt(Form)
+module Cnf = SmtCnf.MakeCnf(Form)
+
+      
+
diff --git a/src/trace/smtAtom.ml b/src/trace/smtAtom.ml
new file mode 100644
index 0000000..3164692
--- /dev/null
+++ b/src/trace/smtAtom.ml
@@ -0,0 +1,748 @@
+(**************************************************************************)
+(*                                                                        *)
+(*     SMTCoq                                                             *)
+(*     Copyright (C) 2011 - 2015                                          *)
+(*                                                                        *)
+(*     Michaël Armand                                                     *)
+(*     Benjamin Grégoire                                                  *)
+(*     Chantal Keller                                                     *)
+(*                                                                        *)
+(*     Inria - École Polytechnique - MSR-Inria Joint Lab                  *)
+(*                                                                        *)
+(*   This file is distributed under the terms of the CeCILL-C licence     *)
+(*                                                                        *)
+(**************************************************************************)
+
+open SmtMisc
+open CoqTerms
+
+(** Syntaxified version of Coq type *)
+type indexed_type = Term.constr gen_hashed
+
+let dummy_indexed_type i = {index = i; hval = Term.mkProp}
+let indexed_type_index i = i.index
+
+type btype =
+  | TZ
+  | Tbool
+  | Tpositive
+  | Tindex of indexed_type
+
+module Btype = 
+  struct 
+
+    let index_tbl = Hashtbl.create 17 
+
+    let index_to_coq i =
+      let i = i.index in 
+      try Hashtbl.find index_tbl i
+      with Not_found ->
+	let interp = mklApp cTindex [|mkInt i|] in
+	Hashtbl.add index_tbl i interp;
+	interp
+
+    let equal t1 t2 =
+      match t1,t2 with
+        | Tindex i, Tindex j -> i.index == j.index
+        | _ -> t1 == t2
+
+    let to_coq = function 
+      | TZ -> Lazy.force cTZ
+      | Tbool -> Lazy.force cTbool
+      | Tpositive -> Lazy.force cTpositive
+      | Tindex i -> index_to_coq i
+
+    let to_smt fmt = function
+      | TZ -> Format.fprintf fmt "Int"
+      | Tbool -> Format.fprintf fmt "Bool"
+      | Tpositive -> Format.fprintf fmt "Int"
+      | Tindex i -> Format.fprintf fmt "Tindex_%i" i.index
+
+    (* reify table *)
+    type reify_tbl = 
+        { mutable count : int;
+	          tbl : (Term.constr, btype) Hashtbl.t
+	}
+
+    let create () = 
+      let htbl = Hashtbl.create 17 in  
+      Hashtbl.add htbl (Lazy.force cZ) TZ;
+      Hashtbl.add htbl (Lazy.force cbool) Tbool;
+      (* Hashtbl.add htbl (Lazy.force cpositive) Tpositive; *)
+      { count = 0;
+	tbl = htbl }
+
+    let declare reify t typ_eqb =
+      (* TODO: allows to have only typ_eqb *)
+      assert (not (Hashtbl.mem reify.tbl t));
+      let res = Tindex {index = reify.count; hval = typ_eqb} in
+      Hashtbl.add reify.tbl t res;
+      reify.count <- reify.count + 1;
+      res
+
+    let of_coq reify t =
+      try
+        Hashtbl.find reify.tbl t
+      with | Not_found ->
+        let eq_t = declare_new_variable (Names.id_of_string "eq") (Term.mkArrow t (Term.mkArrow t (Lazy.force cbool))) in
+        let x = mkName "x" in
+        let y = mkName "y" in
+        let rx = Term.mkRel 2 in
+        let ry = Term.mkRel 1 in
+        let eq_refl = Term.mkProd (x,t,Term.mkProd (y,t,mklApp creflect [|mklApp ceq [|t;rx;ry|];mklApp (lazy eq_t) [|rx;ry|]|])) in
+        let eq_refl_v = declare_new_variable (Names.id_of_string ("eq_refl")) eq_refl in
+        let ce = mklApp cTyp_eqb [|t;eq_t;eq_refl_v|] in
+        declare reify t ce
+
+    let interp_tbl reify =
+      let t = Array.make (reify.count + 1) (Lazy.force cunit_typ_eqb) in
+      let set _ = function 
+	| Tindex it -> t.(it.index) <- it.hval
+	| _ -> () in
+      Hashtbl.iter set reify.tbl;
+      Term.mkArray (Lazy.force ctyp_eqb, t)
+
+    let to_list reify =
+      let set _ t acc = match t with
+	| Tindex it -> (it.index,it)::acc
+	| _ -> acc in
+      Hashtbl.fold set reify.tbl []
+
+    let interp_to_coq reify = function
+      | TZ -> Lazy.force cZ
+      | Tbool -> Lazy.force cbool
+      | Tpositive -> Lazy.force cpositive
+      | Tindex c -> mklApp cte_carrier [|c.hval|]
+
+  end
+
+(** Operators *)
+
+type cop = 
+   | CO_xH
+   | CO_Z0
+
+type uop =
+   | UO_xO
+   | UO_xI
+   | UO_Zpos 
+   | UO_Zneg
+   | UO_Zopp
+
+type bop = 
+   | BO_Zplus
+   | BO_Zminus
+   | BO_Zmult
+   | BO_Zlt
+   | BO_Zle
+   | BO_Zge
+   | BO_Zgt
+   | BO_eq of btype
+
+type nop =
+  | NO_distinct of btype
+
+type op_def = { 
+    tparams : btype array; 
+    tres : btype; 
+    op_val : Term.constr }
+
+type indexed_op = op_def gen_hashed 
+
+let dummy_indexed_op i dom codom = {index = i; hval = {tparams = dom; tres = codom; op_val = Term.mkProp}}
+let indexed_op_index op = op.index
+
+type op = 
+  | Cop of cop
+  | Uop of uop
+  | Bop of bop
+  | Nop of nop
+  | Iop of indexed_op
+
+module Op =
+  struct 
+    let c_to_coq = function
+      | CO_xH -> Lazy.force cCO_xH
+      | CO_Z0 -> Lazy.force cCO_Z0
+
+    let c_type_of = function
+      | CO_xH -> Tpositive
+      | CO_Z0 -> TZ
+
+    let interp_cop = function
+      | CO_xH -> Lazy.force cxH
+      | CO_Z0 -> Lazy.force cZ0
+
+    let u_to_coq = function 
+      | UO_xO -> Lazy.force cUO_xO
+      | UO_xI -> Lazy.force cUO_xI
+      | UO_Zpos -> Lazy.force cUO_Zpos 
+      | UO_Zneg -> Lazy.force cUO_Zneg
+      | UO_Zopp -> Lazy.force cUO_Zopp
+
+    let u_type_of = function 
+      | UO_xO | UO_xI -> Tpositive
+      | UO_Zpos | UO_Zneg | UO_Zopp -> TZ
+
+    let u_type_arg = function 
+      | UO_xO | UO_xI | UO_Zpos | UO_Zneg -> Tpositive
+      | UO_Zopp -> TZ
+
+    let interp_uop = function
+      | UO_xO -> Lazy.force cxO
+      | UO_xI -> Lazy.force cxI
+      | UO_Zpos -> Lazy.force cZpos
+      | UO_Zneg -> Lazy.force cZneg
+      | UO_Zopp -> Lazy.force copp
+
+    let eq_tbl = Hashtbl.create 17 
+
+    let eq_to_coq t =
+      try Hashtbl.find eq_tbl t 
+      with Not_found ->
+	let op = mklApp cBO_eq [|Btype.to_coq t|] in
+	Hashtbl.add eq_tbl t op;
+	op
+     
+    let b_to_coq = function
+      | BO_Zplus -> Lazy.force cBO_Zplus
+      | BO_Zminus -> Lazy.force cBO_Zminus
+      | BO_Zmult -> Lazy.force cBO_Zmult
+      | BO_Zlt -> Lazy.force cBO_Zlt
+      | BO_Zle -> Lazy.force cBO_Zle
+      | BO_Zge -> Lazy.force cBO_Zge
+      | BO_Zgt -> Lazy.force cBO_Zgt
+      | BO_eq t -> eq_to_coq t
+
+    let b_type_of = function
+      | BO_Zplus | BO_Zminus | BO_Zmult -> TZ
+      | BO_Zlt | BO_Zle | BO_Zge | BO_Zgt | BO_eq _ -> Tbool
+
+    let b_type_args = function
+      | BO_Zplus | BO_Zminus | BO_Zmult 
+      | BO_Zlt | BO_Zle | BO_Zge | BO_Zgt -> (TZ,TZ)
+      | BO_eq t -> (t,t)
+
+    let interp_eq = function
+      | TZ -> Lazy.force ceqbZ
+      | Tbool -> Lazy.force ceqb
+      | Tpositive -> Lazy.force ceqbP
+      | Tindex i -> mklApp cte_eqb [|i.hval|]
+
+    let interp_bop = function
+      | BO_Zplus -> Lazy.force cadd
+      | BO_Zminus -> Lazy.force csub
+      | BO_Zmult -> Lazy.force cmul
+      | BO_Zlt -> Lazy.force cltb
+      | BO_Zle -> Lazy.force cleb
+      | BO_Zge -> Lazy.force cgeb
+      | BO_Zgt -> Lazy.force cgtb
+      | BO_eq t -> interp_eq t
+
+    let n_to_coq = function
+      | NO_distinct t -> mklApp cNO_distinct [|Btype.to_coq t|]
+
+    let n_type_of = function
+      | NO_distinct _ -> Tbool
+
+    let n_type_args = function
+      | NO_distinct ty -> ty
+
+    let interp_distinct = function
+      | TZ -> Lazy.force cZ
+      | Tbool -> Lazy.force cbool
+      | Tpositive -> Lazy.force cpositive
+      | Tindex i -> mklApp cte_carrier [|i.hval|]
+
+    let interp_nop = function
+      | NO_distinct ty -> mklApp cdistinct [|interp_distinct ty;interp_eq ty|]
+
+    let i_to_coq i = mkInt i.index
+
+    let i_type_of i = i.hval.tres
+
+    let i_type_args i = i.hval.tparams
+	  
+    (* reify table *)
+    type reify_tbl =
+        { mutable count : int;
+	          tbl : (Term.constr, indexed_op) Hashtbl.t
+	}
+
+    let create () = 
+      { count = 0;
+	tbl =  Hashtbl.create 17 }
+
+    let declare reify op tparams tres =
+      assert (not (Hashtbl.mem reify.tbl op));
+      let v = { tparams = tparams; tres = tres; op_val = op } in
+      let res = {index = reify.count; hval = v } in
+      Hashtbl.add reify.tbl op res;
+      reify.count <- reify.count + 1;
+      res
+
+    let of_coq reify op =
+      Hashtbl.find reify.tbl op
+
+
+    let interp_tbl tval mk_Tval reify =
+      let t = Array.make (reify.count + 1) 
+	  (mk_Tval [||] Tbool (Lazy.force ctrue))  in
+      let set _ v = 
+	t.(v.index) <- mk_Tval v.hval.tparams v.hval.tres v.hval.op_val in
+      Hashtbl.iter set reify.tbl;
+      Term.mkArray (tval, t)
+
+    let to_list reify =
+      let set _ op acc =
+        let value = op.hval in
+        (op.index,value.tparams,value.tres,op)::acc in
+      Hashtbl.fold set reify.tbl []
+
+    let c_equal op1 op2 = op1 == op2
+
+    let u_equal op1 op2 = op1 == op2
+
+    let b_equal op1 op2 =
+      match op1,op2 with
+        | BO_eq t1, BO_eq t2 -> Btype.equal t1 t2
+        | _ -> op1 == op2
+
+    let n_equal op1 op2 =
+      match op1,op2 with
+        | NO_distinct t1, NO_distinct t2 -> Btype.equal t1 t2
+
+    let i_equal op1 op2 = op1.index == op2.index
+
+  end
+
+
+(** Definition of atoms *)
+
+type atom = 
+  | Acop of cop
+  | Auop of uop * hatom 
+  | Abop of bop * hatom * hatom 
+  | Anop of nop * hatom array
+  | Aapp of indexed_op * hatom array
+
+and hatom = atom gen_hashed
+
+(* let pp_acop = function *)
+(*   | CO_xH -> "CO_xH" *)
+(*   | CO_Z0 -> "CO_Z0" *)
+
+(* let pp_auop = function *)
+(*   | UO_xO -> "UO_xO" *)
+(*   | UO_xI -> "UO_xI" *)
+(*   | UO_Zpos -> "UO_Zpos" *)
+(*   | UO_Zneg -> "UO_Zneg" *)
+(*   | UO_Zopp -> "UO_Zopp" *)
+
+(* let pp_abop = function *)
+(*   | BO_Zplus -> "BO_Zplus" *)
+(*   | BO_Zminus -> "BO_Zminus" *)
+(*   | BO_Zmult -> "BO_Zmult" *)
+(*   | BO_Zlt -> "BO_Zlt" *)
+(*   | BO_Zle -> "BO_Zle" *)
+(*   | BO_Zge -> "BO_Zge" *)
+(*   | BO_Zgt -> "BO_Zgt" *)
+(*   | BO_eq _ -> "(BO_eq ??)" *)
+
+(* let rec pp_atom = function *)
+(*   | Acop c -> "(Acop "^(pp_acop c)^")" *)
+(*   | Auop (u,b) -> "(Auop "^(pp_auop u)^" "^(pp_atom b.hval)^")" *)
+(*   | Abop (b,c,d) -> "(Abop "^(pp_abop b)^" "^(pp_atom c.hval)^" "^(pp_atom d.hval)^")" *)
+(*   | Aapp (op,a) -> "(Aapp "^(string_of_int op.index)^" ("^(Array.fold_left (fun acc h -> acc^" "^(pp_atom h.hval)) "" a)^"))" *)
+
+module HashedAtom =
+  struct 
+    type t = atom
+
+    let equal a b =
+      match a, b with
+      | Acop opa, Acop opb -> Op.c_equal opa opb
+      | Auop(opa,ha), Auop(opb,hb) -> Op.u_equal opa opb && ha.index == hb.index
+      | Abop(opa,ha1,ha2), Abop(opb,hb1,hb2) ->
+	  Op.b_equal opa opb && ha1.index == hb1.index && ha2.index == hb2.index
+      | Anop (opa,ha), Anop (opb,hb) ->
+        let na = Array.length ha in
+        let nb = Array.length hb in
+        let i = ref (-1) in
+        Op.n_equal opa opb && na == nb && Array.fold_left (fun b h -> incr i; b && h.index == hb.(!i).index) true ha
+      | Aapp (va,ha), Aapp (vb,hb) ->
+        let na = Array.length ha in
+        let nb = Array.length hb in
+        let i = ref (-1) in
+        Op.i_equal va vb && na == nb && Array.fold_left (fun b h -> incr i; b && h.index == hb.(!i).index) true ha
+      | _, _ -> false
+
+    let hash = function
+      |	Acop op -> ((Hashtbl.hash op) lsl 3) lxor 1
+      | Auop (op,h) ->
+          (( (h.index lsl 3) + (Hashtbl.hash op)) lsl 3) lxor 2
+      | Abop (op,h1,h2) ->
+          (((( (h1.index lsl 2) + h2.index) lsl 3) + Hashtbl.hash op) lsl 3) lxor 3
+      | Anop (op, args) ->
+          let hash_args =
+            match Array.length args with
+            | 0 -> 0
+            | 1 -> args.(0).index
+            | 2 -> args.(1).index lsl 2 + args.(0).index
+            | _ -> args.(2).index lsl 4 + args.(1).index lsl 2 + args.(0).index in
+          (hash_args lsl 5 + (Hashtbl.hash op) lsl 3) lxor 4
+      | Aapp (op, args) ->
+          let hash_args =
+            match Array.length args with
+            | 0 -> 0
+            | 1 -> args.(0).index
+            | 2 -> args.(1).index lsl 2 + args.(0).index
+            | _ -> args.(2).index lsl 4 + args.(1).index lsl 2 + args.(0).index in
+          (hash_args lsl 5 + op.index lsl 3) lxor 4
+
+  end
+
+module HashAtom = Hashtbl.Make(HashedAtom)
+
+module Atom = 
+  struct 
+
+    type t = hatom
+
+    let atom h = h.hval
+    let index h = h.index 
+
+    let equal h1 h2 = h1.index == h2.index
+
+    let type_of h =
+      match h.hval with
+      | Acop op -> Op.c_type_of op
+      | Auop (op,_) -> Op.u_type_of op
+      | Abop (op,_,_) -> Op.b_type_of op
+      | Anop (op,_) -> Op.n_type_of op
+      | Aapp (op,_) -> Op.i_type_of op
+
+    let is_bool_type h = Btype.equal (type_of h) Tbool
+
+
+    let rec compute_int = function
+      | Acop c ->
+        (match c with
+          | CO_xH -> 1
+          | CO_Z0 -> 0)
+      | Auop (op,h) ->
+        (match op with
+          | UO_xO -> 2*(compute_hint h)
+          | UO_xI -> 2*(compute_hint h) + 1
+          | UO_Zpos -> compute_hint h
+          | UO_Zneg -> - (compute_hint h)
+          | UO_Zopp -> assert false)
+      | _ -> assert false
+
+    and compute_hint h = compute_int (atom h)
+
+    let to_smt_int fmt i =
+      let s1 = if i < 0 then "(- " else "" in
+      let s2 = if i < 0 then ")" else "" in
+      let j = if i < 0 then -i else i in
+      Format.fprintf fmt "%s%i%s" s1 j s2
+
+    let rec to_smt fmt h = to_smt_atom fmt (atom h)
+
+    and to_smt_atom fmt = function
+      | Acop _ as a -> to_smt_int fmt (compute_int a)
+      | Auop (UO_Zopp,h) ->
+        Format.fprintf fmt "(- ";
+        to_smt fmt h;
+        Format.fprintf fmt ")"
+      | Auop _ as a -> to_smt_int fmt (compute_int a)
+      | Abop (op,h1,h2) -> to_smt_bop fmt op h1 h2
+      | Anop (op,a) -> to_smt_nop fmt op a
+      | Aapp (op,a) ->
+        if Array.length a = 0 then (
+          Format.fprintf fmt "op_%i" op.index;
+        ) else (
+          Format.fprintf fmt "(op_%i" op.index;
+          Array.iter (fun h -> Format.fprintf fmt " "; to_smt fmt h) a;
+          Format.fprintf fmt ")"
+        )
+
+    and to_smt_bop fmt op h1 h2 =
+      let s = match op with
+        | BO_Zplus -> "+"
+        | BO_Zminus -> "-"
+        | BO_Zmult -> "*"
+        | BO_Zlt -> "<"
+        | BO_Zle -> "<="
+        | BO_Zge -> ">="
+        | BO_Zgt -> ">"
+        | BO_eq _ -> "=" in
+      Format.fprintf fmt "(%s " s;
+      to_smt fmt h1;
+      Format.fprintf fmt " ";
+      to_smt fmt h2;
+      Format.fprintf fmt ")"
+
+    and to_smt_nop fmt op a =
+      let s = match op with
+        | NO_distinct _ -> "distinct" in
+      Format.fprintf fmt "(%s" s;
+      Array.iter (fun h -> Format.fprintf fmt " "; to_smt fmt h) a;
+      Format.fprintf fmt ")"
+
+
+
+    exception NotWellTyped of atom
+
+    let check a =
+      match a with
+      | Acop _ -> ()
+      | Auop(op,h) -> 
+	  if not (Btype.equal (Op.u_type_arg op) (type_of h)) then
+	    raise (NotWellTyped a)
+      | Abop(op,h1,h2) ->
+	  let (t1,t2) = Op.b_type_args op in
+	  if not (Btype.equal t1 (type_of h1) && Btype.equal t2 (type_of h2))
+	  then raise (NotWellTyped a)
+      | Anop(op,ha) ->
+        let ty = Op.n_type_args op in
+        Array.iter (fun h -> if not (Btype.equal ty (type_of h)) then raise (NotWellTyped a)) ha
+      | Aapp(op,args) ->
+	  let tparams = Op.i_type_args op in
+	  Array.iteri (fun i t -> 
+	    if not (Btype.equal t (type_of args.(i))) then
+		raise (NotWellTyped a)) tparams
+
+    type reify_tbl =
+        { mutable count : int;
+	          tbl : hatom HashAtom.t 
+	}
+
+    let create () = 
+      { count = 0;
+	tbl =  HashAtom.create 17 }
+
+    let clear reify =
+      reify.count <- 0;
+      HashAtom.clear reify.tbl
+
+    let declare reify a = 
+      check a;
+      let res = {index = reify.count; hval = a} in
+      HashAtom.add reify.tbl a res;
+      reify.count <- reify.count + 1;
+      res
+
+    let get reify a =
+      try HashAtom.find reify.tbl a 
+      with Not_found -> declare reify a
+
+
+    (** Given a coq term, build the corresponding atom *)
+    type coq_cst =
+      | CCxH
+      | CCZ0
+      | CCxO
+      | CCxI
+      | CCZpos
+      | CCZneg
+      | CCZopp
+      | CCZplus
+      | CCZminus
+      | CCZmult
+      | CCZlt
+      | CCZle
+      | CCZge
+      | CCZgt
+      | CCeqb
+      | CCeqbP
+      | CCeqbZ
+      | CCunknown
+
+    let op_tbl () =
+      let tbl = Hashtbl.create 29 in
+      let add (c1,c2) = Hashtbl.add tbl (Lazy.force c1) c2 in
+      List.iter add
+	[ cxH,CCxH; cZ0,CCZ0;
+          cxO,CCxO; cxI,CCxI; cZpos,CCZpos; cZneg,CCZneg; copp,CCZopp;
+          cadd,CCZplus; csub,CCZminus; cmul,CCZmult; cltb,CCZlt;
+          cleb,CCZle; cgeb,CCZge; cgtb,CCZgt; ceqb,CCeqb; ceqbP,CCeqbP;
+          ceqbZ, CCeqbZ
+        ];
+      tbl
+
+    let op_tbl = lazy (op_tbl ())
+
+    let of_coq rt ro reify env sigma c =
+      let op_tbl = Lazy.force op_tbl in
+      let get_cst c =
+	try Hashtbl.find op_tbl c with Not_found -> CCunknown in
+      let mk_cop op = get reify (Acop op) in
+      let rec mk_hatom h =
+	let c, args = Term.decompose_app h in
+	match get_cst c with
+          | CCxH -> mk_cop CO_xH
+          | CCZ0 -> mk_cop CO_Z0
+          | CCxO -> mk_uop UO_xO args
+          | CCxI -> mk_uop UO_xI args
+          | CCZpos -> mk_uop UO_Zpos args
+          | CCZneg -> mk_uop UO_Zneg args
+          | CCZopp -> mk_uop UO_Zopp args
+          | CCZplus -> mk_bop BO_Zplus args
+          | CCZminus -> mk_bop BO_Zminus args
+          | CCZmult -> mk_bop BO_Zmult args
+          | CCZlt -> mk_bop BO_Zlt args
+          | CCZle -> mk_bop BO_Zle args
+          | CCZge -> mk_bop BO_Zge args
+          | CCZgt -> mk_bop BO_Zgt args
+          | CCeqb -> mk_bop (BO_eq Tbool) args
+          | CCeqbP -> mk_bop (BO_eq Tpositive) args
+          | CCeqbZ -> mk_bop (BO_eq TZ) args
+	  | CCunknown -> mk_unknown c args (Retyping.get_type_of env sigma h)
+
+      and mk_uop op = function
+        | [a] -> let h = mk_hatom a in get reify (Auop (op,h))
+        | _ -> assert false
+
+      and mk_bop op = function
+        | [a1;a2] ->
+          let h1 = mk_hatom a1 in
+          let h2 = mk_hatom a2 in
+          get reify (Abop (op,h1,h2))
+        | _ -> assert false
+
+      and mk_unknown c args ty =
+        let hargs = Array.of_list (List.map mk_hatom args) in
+        let op =
+          try Op.of_coq ro c
+          with | Not_found ->
+            let targs = Array.map type_of hargs in
+            let tres = Btype.of_coq rt ty in
+            Op.declare ro c targs tres in
+        get reify (Aapp (op,hargs)) in
+
+       mk_hatom c
+
+
+    let to_coq h = mkInt h.index
+
+    let a_to_coq a =
+      match a with
+      | Acop op -> mklApp cAcop [|Op.c_to_coq op|]
+      | Auop (op,h) -> mklApp cAuop [|Op.u_to_coq op; to_coq h|]
+      | Abop (op,h1,h2) -> 
+	  mklApp cAbop [|Op.b_to_coq op;to_coq h1; to_coq h2|]
+      | Anop (op,ha) ->
+        let cop = Op.n_to_coq op in
+        let cargs = Array.fold_right (fun h l -> mklApp ccons [|Lazy.force cint; to_coq h; l|]) ha (mklApp cnil [|Lazy.force cint|]) in
+        mklApp cAnop [|cop; cargs|]
+      | Aapp (op,args) ->
+        let cop = Op.i_to_coq op in
+        let cargs = Array.fold_right (fun h l -> mklApp ccons [|Lazy.force cint; to_coq h; l|]) args (mklApp cnil [|Lazy.force cint|]) in
+        mklApp cAapp [|cop; cargs|]
+
+    let dft_atom = lazy (mklApp cAcop [| Lazy.force cCO_xH |])
+
+    let to_array reify dft f =
+      let t = Array.make (reify.count + 1) dft in
+      let set _ h = t.(h.index) <- f h.hval in
+      HashAtom.iter set reify.tbl;
+      t
+
+    let interp_tbl reify =
+      let t = to_array reify (Lazy.force dft_atom) a_to_coq in
+      Term.mkArray (Lazy.force catom, t)
+
+
+    (** Producing a Coq term corresponding to the interpretation of an atom *)
+    let interp_to_coq atom_tbl a =
+      let rec interp_atom a =
+	let l = index a in
+	try Hashtbl.find atom_tbl l
+	with Not_found ->
+	  let pc =
+	    match atom a with
+              | Acop c -> Op.interp_cop c
+              | Auop (op,h) -> Term.mkApp (Op.interp_uop op, [|interp_atom h|])
+              | Abop (op,h1,h2) -> Term.mkApp (Op.interp_bop op, [|interp_atom h1; interp_atom h2|])
+              | Anop (NO_distinct ty as op,ha) ->
+                let cop = Op.interp_nop op in
+                let typ = Op.interp_distinct ty in
+                let cargs = Array.fold_right (fun h l -> mklApp ccons [|typ; interp_atom h; l|]) ha (mklApp cnil [|typ|]) in
+                Term.mkApp (cop,[|cargs|])
+              | Aapp (op,t) -> Term.mkApp (op.hval.op_val, Array.map interp_atom t) in
+	  Hashtbl.add atom_tbl l pc;
+	  pc in
+      interp_atom a
+
+
+    (* Generation of atoms *)
+
+    let mk_nop op reify a = get reify (Anop (op,a))
+
+    let mk_binop op reify h1 h2 = get reify (Abop (op, h1, h2))
+
+    let mk_unop op reify h = get reify (Auop (op, h))
+
+    let rec hatom_pos_of_int reify i =
+      if i <= 1 then
+        get reify (Acop CO_xH)
+      else
+        if i land 1 = 0
+        then mk_unop UO_xO reify (hatom_pos_of_int reify (i lsr 1))
+        else mk_unop UO_xI reify (hatom_pos_of_int reify (i lsr 1))
+
+    let hatom_Z_of_int reify i =
+      if i = 0 then
+        get reify (Acop CO_Z0)
+      else
+        if i > 0
+        then mk_unop UO_Zpos reify (hatom_pos_of_int reify i)
+        else mk_unop UO_Zneg reify (hatom_pos_of_int reify (-i))
+
+    let rec hatom_pos_of_bigint reify i =
+      if Big_int.le_big_int i Big_int.unit_big_int then
+        get reify (Acop CO_xH)
+      else
+        let (q,r) = Big_int.quomod_big_int i (Big_int.big_int_of_int 2) in
+        if Big_int.eq_big_int r Big_int.zero_big_int then
+          mk_unop UO_xO reify (hatom_pos_of_bigint reify q)
+        else
+          mk_unop UO_xI reify (hatom_pos_of_bigint reify q)
+
+    let hatom_Z_of_bigint reify i =
+      if Big_int.eq_big_int i Big_int.zero_big_int then
+        get reify (Acop CO_Z0)
+      else
+        if Big_int.gt_big_int i Big_int.zero_big_int then
+          mk_unop UO_Zpos reify (hatom_pos_of_bigint reify i)
+        else
+          mk_unop UO_Zneg reify (hatom_pos_of_bigint reify (Big_int.minus_big_int i))
+
+    let mk_eq reify ty h1 h2 =
+      let op = BO_eq ty in
+      try
+        HashAtom.find reify.tbl (Abop (op, h1, h2))
+      with
+        | Not_found ->
+          try
+            HashAtom.find reify.tbl (Abop (op, h2, h1))
+          with
+            | Not_found ->
+              declare reify (Abop (op, h1, h2))
+
+    let mk_lt = mk_binop BO_Zlt
+    let mk_le = mk_binop BO_Zle
+    let mk_gt = mk_binop BO_Zgt
+    let mk_ge = mk_binop BO_Zge
+    let mk_plus = mk_binop BO_Zplus
+    let mk_minus = mk_binop BO_Zminus
+    let mk_mult = mk_binop BO_Zmult
+    let mk_opp = mk_unop UO_Zopp
+    let mk_distinct reify ty = mk_nop (NO_distinct ty) reify
+
+  end
+
+
+module Form = SmtForm.Make(Atom)
+module Trace = SmtTrace.MakeOpt(Form)
diff --git a/src/trace/smtAtom.mli b/src/trace/smtAtom.mli
new file mode 100644
index 0000000..8eadb49
--- /dev/null
+++ b/src/trace/smtAtom.mli
@@ -0,0 +1,175 @@
+(**************************************************************************)
+(*                                                                        *)
+(*     SMTCoq                                                             *)
+(*     Copyright (C) 2011 - 2015                                          *)
+(*                                                                        *)
+(*     Michaël Armand                                                     *)
+(*     Benjamin Grégoire                                                  *)
+(*     Chantal Keller                                                     *)
+(*                                                                        *)
+(*     Inria - École Polytechnique - MSR-Inria Joint Lab                  *)
+(*                                                                        *)
+(*   This file is distributed under the terms of the CeCILL-C licence     *)
+(*                                                                        *)
+(**************************************************************************)
+
+
+type indexed_type
+
+val dummy_indexed_type: int -> indexed_type
+val indexed_type_index : indexed_type -> int
+
+type btype =
+  | TZ
+  | Tbool
+  | Tpositive
+  | Tindex of indexed_type
+
+module Btype : 
+    sig
+      
+      val equal : btype -> btype -> bool
+	  
+      val to_coq : btype -> Term.constr
+
+      val to_smt : Format.formatter -> btype -> unit
+
+      type reify_tbl
+	  
+      val create : unit -> reify_tbl
+
+      val declare : reify_tbl -> Term.constr -> Term.constr -> btype
+
+      val of_coq : reify_tbl -> Term.constr -> btype
+
+      val interp_tbl : reify_tbl -> Term.constr
+
+      val to_list : reify_tbl -> (int * indexed_type) list
+
+      val interp_to_coq : reify_tbl -> btype -> Term.constr
+
+    end
+
+(** Operators *)
+
+type cop = 
+   | CO_xH
+   | CO_Z0
+
+type uop =
+   | UO_xO
+   | UO_xI
+   | UO_Zpos 
+   | UO_Zneg
+   | UO_Zopp
+
+type bop = 
+   | BO_Zplus
+   | BO_Zminus
+   | BO_Zmult
+   | BO_Zlt
+   | BO_Zle
+   | BO_Zge
+   | BO_Zgt
+   | BO_eq of btype
+
+type nop =
+  | NO_distinct of btype
+
+type indexed_op
+
+val dummy_indexed_op: int -> btype array -> btype -> indexed_op
+val indexed_op_index : indexed_op -> int
+
+module Op :
+  sig
+	  
+    type reify_tbl
+
+    val create : unit -> reify_tbl
+
+    val declare : reify_tbl -> Term.constr -> btype array -> btype -> indexed_op
+
+    val of_coq : reify_tbl -> Term.constr -> indexed_op
+
+    val interp_tbl : Term.constr -> 
+      (btype array -> btype -> Term.constr -> Term.constr) -> 
+      reify_tbl -> Term.constr 
+
+    val to_list : reify_tbl -> (int * (btype array) * btype * indexed_op) list
+
+  end
+
+
+(** Definition of atoms *)
+
+type hatom 
+
+type atom = 
+  | Acop of cop
+  | Auop of uop * hatom 
+  | Abop of bop * hatom * hatom 
+  | Anop of nop * hatom array
+  | Aapp of indexed_op * hatom array
+
+
+
+module Atom : 
+    sig 
+
+      type t = hatom
+
+      val equal : hatom -> hatom -> bool
+
+      val index : hatom -> int
+
+      val atom : hatom -> atom
+ 
+      val type_of : hatom -> btype
+
+      val to_smt : Format.formatter -> t -> unit
+
+      exception NotWellTyped of atom
+
+      type reify_tbl 
+
+      val create : unit -> reify_tbl
+
+      val clear : reify_tbl -> unit
+
+      val get : reify_tbl -> atom -> hatom
+
+      (** Given a coq term, build the corresponding atom *)
+      val of_coq : Btype.reify_tbl -> Op.reify_tbl -> reify_tbl ->
+        Environ.env -> Evd.evar_map -> Term.constr -> t
+
+      val to_coq : hatom -> Term.constr
+
+      val to_array : reify_tbl -> 'a -> (atom -> 'a) -> 'a array
+
+      val interp_tbl : reify_tbl -> Term.constr
+
+      val interp_to_coq : (int, Term.constr) Hashtbl.t ->
+	t -> Term.constr
+
+      (* Generation of atoms *)
+      val hatom_Z_of_int : reify_tbl -> int -> hatom
+      val hatom_Z_of_bigint : reify_tbl -> Big_int.big_int -> hatom
+      val mk_eq : reify_tbl -> btype -> hatom -> hatom -> hatom
+      val mk_lt : reify_tbl -> hatom -> hatom -> hatom
+      val mk_le : reify_tbl -> hatom -> hatom -> hatom
+      val mk_gt : reify_tbl -> hatom -> hatom -> hatom
+      val mk_ge : reify_tbl -> hatom -> hatom -> hatom
+      val mk_plus : reify_tbl -> hatom -> hatom -> hatom
+      val mk_minus : reify_tbl -> hatom -> hatom -> hatom
+      val mk_mult : reify_tbl -> hatom -> hatom -> hatom
+      val mk_opp : reify_tbl -> hatom -> hatom
+      val mk_distinct : reify_tbl -> btype -> hatom array -> hatom
+
+    end
+
+
+module Form : SmtForm.FORM with type hatom = hatom
+module Trace : sig
+  val share_prefix : Form.t SmtCertif.clause -> int -> unit
+end
diff --git a/src/trace/smtCertif.ml b/src/trace/smtCertif.ml
new file mode 100644
index 0000000..76036a5
--- /dev/null
+++ b/src/trace/smtCertif.ml
@@ -0,0 +1,140 @@
+(**************************************************************************)
+(*                                                                        *)
+(*     SMTCoq                                                             *)
+(*     Copyright (C) 2011 - 2015                                          *)
+(*                                                                        *)
+(*     Michaël Armand                                                     *)
+(*     Benjamin Grégoire                                                  *)
+(*     Chantal Keller                                                     *)
+(*                                                                        *)
+(*     Inria - École Polytechnique - MSR-Inria Joint Lab                  *)
+(*                                                                        *)
+(*   This file is distributed under the terms of the CeCILL-C licence     *)
+(*                                                                        *)
+(**************************************************************************)
+
+
+open SmtForm
+
+type used = int
+
+type clause_id  = int
+
+type 'hform rule =
+  | ImmFlatten of 'hform clause * 'hform 
+
+  (* CNF Transformations *)
+  | True       
+     (*  * true             : {true} 
+     *)
+  | False 
+     (* * false             : {(not false)} 
+     *)
+  | BuildDef of 'hform (* the first literal of the clause *)       
+     (*  * and_neg          : {(and a_1 ... a_n) (not a_1) ... (not a_n)}
+         * or_pos           : {(not (or a_1 ... a_n)) a_1 ... a_n} 
+         * implies_pos      : {(not (implies a b)) (not a) b}
+         * xor_pos1         : {(not (xor a b)) a b}
+         * xor_neg1         : {(xor a b) a (not b)}
+         * equiv_pos1       : {(not (iff a b)) a (not b)}
+         * equiv_neg1       : {(iff a b) (not a) (not b)}
+         * ite_pos1         : {(not (if_then_else a b c)) a c}
+         * ite_neg1         : {(if_then_else a b c) a (not c)}
+     *)
+  | BuildDef2 of 'hform (* the first literal of the clause *) 
+     (* * xor_pos2          : {(not (xor a b)) (not a) (not b)}
+        * xor_neg2          : {(xor a b) (not a) b}
+        * equiv_pos2        : {(not (iff a b)) (not a) b}
+        * equiv_neg2        : {(iff a b) a b}
+        * ite_pos2          : {(not (if_then_else a b c)) (not a) b}
+        * ite_neg2          : {(if_then_else a b c) (not a) (not b)}
+
+     *)
+  | BuildProj of 'hform * int 
+     (*  * or_neg           : {(or a_1 ... a_n) (not a_i)}
+         * and_pos          : {(not (and a_1 ... a_n)) a_i} 
+         * implies_neg1     : {(implies a b) a}
+         * implies_neg2     : {(implies a b) (not b)}
+     *)
+
+  (* Immediate CNF transformation : CNF transformation + Reso *)
+  | ImmBuildDef of 'hform clause 
+     (* * not_and           : {(not (and a_1 ... a_n))} --> {(not a_1) ... (not a_n)}
+        * or                : {(or a_1 ... a_n)} --> {a_1 ... a_n}
+        * implies           : {(implies a b)} --> {(not a) b}
+        * xor1              : {(xor a b)} --> {a b}
+        * not_xor1          : {(not (xor a b))} --> {a (not b)}
+        * equiv2            : {(iff a b)} --> {a (not b)}
+        * not_equiv2        : {(not (iff a b))} --> {(not a) (not b)}
+        * ite1              : {(if_then_else a b c)} --> {a c}
+        * not_ite1          : {(not (if_then_else a b c))} --> {a (not c)}
+     *)
+  | ImmBuildDef2 of 'hform clause
+     (* * xor2              : {(xor a b)} --> {(not a) (not b)}
+        * not_xor2          : {(not (xor a b))} --> {(not a) b}
+        * equiv1            : {(iff a b)} --> {(not a) b}
+        * not_equiv1        : {(not (iff a b))} --> {a b}
+        * ite2              : {(if_then_else a b c)} --> {(not a) b}
+        * not_ite2          : {(not (if_then_else a b c))} --> {(not a) (not b)}
+     *)
+  | ImmBuildProj of 'hform clause * int
+     (*  * and               : {(and a_1 ... a_n)} --> {a_i} 
+         * not_or            : {(not (or a_1 ... a_n))} --> {(not a_i)}
+         * not_implies1      : {(not (implies a b))} --> {a}
+         * not_implies2      : {(not (implies a b))} --> {(not b)}
+     *)
+
+  (* Equality *)
+  | EqTr of 'hform * 'hform list
+    (*  * eq_reflexive     : {(= x x)}
+        * eq_transitive    : {(not (= x_1 x_2)) ... (not (= x_{n-1} x_n)) (= x_1 x_n)}
+    *)
+  | EqCgr of 'hform * ('hform option) list
+    (*  * eq_congruent     : {(not (= x_1 y_1)) ... (not (= x_n y_n)) 
+                                   (= (f x_1 ... x_n) (f y_1 ... y_n))}
+    *)
+  | EqCgrP of 'hform * 'hform * ('hform option) list
+    (*  * eq_congruent_pred : {(not (= x_1 y_1)) ... (not (= x_n y_n)) 
+                                   (not (p x_1 ... x_n)) (p y_1 ... y_n)}
+    *)
+
+  (* Linear arithmetic *)
+  | LiaMicromega of 'hform list * Certificate.Mc.zArithProof list
+  | LiaDiseq of 'hform
+
+  (* Arithmetic simplifications *)
+  | SplArith of 'hform clause * 'hform * Certificate.Mc.zArithProof list
+
+  (* Elimination of operators *)
+  | SplDistinctElim of 'hform clause * 'hform
+
+and 'hform clause = {
+            id    : clause_id;
+    mutable kind  : 'hform clause_kind;
+    mutable pos   : int option;
+    mutable used  : used;
+    mutable prev  : 'hform clause option;
+    mutable next  : 'hform clause option;
+            value : 'hform list option
+              (* This field should be defined for rules which can create atoms :
+                 EqTr, EqCgr, EqCgrP, Lia, Dlde, Lra *)
+}
+
+and 'hform clause_kind =
+  | Root
+  | Same of 'hform clause
+  | Res of 'hform resolution
+  | Other of 'hform rule
+
+and 'hform resolution = {
+  mutable rc1   : 'hform clause;
+  mutable rc2   : 'hform clause;
+  mutable rtail : 'hform clause list}
+
+let used_clauses r =
+  match r with
+  | ImmBuildProj (c, _) | ImmBuildDef c | ImmBuildDef2 c
+  | ImmFlatten (c,_)  | SplArith (c,_,_) | SplDistinctElim (c,_) -> [c]
+  | True | False | BuildDef _ | BuildDef2 _ | BuildProj _
+  | EqTr _ | EqCgr _ | EqCgrP _
+  | LiaMicromega _ | LiaDiseq _ -> []
diff --git a/src/trace/smtCnf.ml b/src/trace/smtCnf.ml
new file mode 100644
index 0000000..d159db0
--- /dev/null
+++ b/src/trace/smtCnf.ml
@@ -0,0 +1,264 @@
+(**************************************************************************)
+(*                                                                        *)
+(*     SMTCoq                                                             *)
+(*     Copyright (C) 2011 - 2015                                          *)
+(*                                                                        *)
+(*     Michaël Armand                                                     *)
+(*     Benjamin Grégoire                                                  *)
+(*     Chantal Keller                                                     *)
+(*                                                                        *)
+(*     Inria - École Polytechnique - MSR-Inria Joint Lab                  *)
+(*                                                                        *)
+(*   This file is distributed under the terms of the CeCILL-C licence     *)
+(*                                                                        *)
+(**************************************************************************)
+
+
+open SmtForm
+open SmtCertif
+open SmtTrace
+
+module MakeCnf (Form:FORM) =
+  struct 
+
+    type form_info = 
+      | Immediate of bool (* true if the positive literal is set *) 
+      | Done (* means that the equivalence clauses have been generated *)
+      | Todo (* nothing has been done, process the cnf transformation *)
+
+    let info = Hashtbl.create 17 
+
+    let init_last = 
+      let last = SmtTrace.mk_scertif Root None in
+      SmtTrace.clear ();
+      last
+
+    let last = ref init_last
+
+    let cnf_todo = ref [] 
+
+    let clear () = 
+      Hashtbl.clear info;
+      last := init_last;
+      cnf_todo := []
+
+    let push_cnf args = cnf_todo := args :: !cnf_todo
+
+    let get_info l =
+      try Hashtbl.find info (Form.index l)
+      with Not_found -> Todo 
+
+    let set_done l =
+      Hashtbl.add info (Form.index l) Done
+
+    let set_immediate l = 
+      Hashtbl.add info (Form.index l) (Immediate (Form.is_pos l))
+
+    let test_immediate l = 
+      match get_info l with
+      | Immediate b -> b = Form.is_pos l 
+      | _ -> false
+
+    let check_trivial cl =
+      List.exists test_immediate cl 
+
+    let link_Other other cl =
+      if not (check_trivial cl) then 
+	let c = mkOther other (Some cl) in
+	link !last c;
+	last := c
+
+    let both_lit l = if Form.is_pos l then Form.neg l,l else l, Form.neg l 
+
+    let or_of_imp args =  
+      Array.mapi (fun i l -> 
+	if i = Array.length args - 1 then l else Form.neg l) args 
+
+    let rec cnf l =
+      match get_info l with
+      | Immediate _ | Done -> ()
+      | Todo -> 
+	  match Form.pform l with
+	  | Fatom _ -> ()
+
+	  | Fapp (op,args) ->
+	      match op with
+	      | Ftrue | Ffalse -> () 
+
+	      | Fand ->
+		  let nl,pl = both_lit l in
+		  let nargs = Array.map Form.neg args in
+		  link_Other (BuildDef pl) (pl::Array.to_list nargs);
+		  Array.iteri (fun i l' -> 
+		    link_Other (BuildProj (nl,i)) [nl;l']) args;
+		  set_done l;
+		  Array.iter cnf args
+
+	      | For ->
+		  let nl,pl = both_lit l in
+		  link_Other (BuildDef nl) (nl::Array.to_list args);
+		  Array.iteri (fun i l' -> 
+		    link_Other (BuildProj(pl,i)) [pl;Form.neg l']) args;
+		  set_done l;
+		  Array.iter cnf args
+
+	      | Fimp ->
+		  let args = or_of_imp args in
+		  let nl,pl = both_lit l in
+		  link_Other (BuildDef nl) (nl::Array.to_list args);
+		  Array.iteri (fun i l' -> 
+		    link_Other (BuildProj(pl,i)) [pl;Form.neg l']) args;
+		  set_done l;
+		  Array.iter cnf args
+	
+	      | Fxor -> 
+		  let nl,pl = both_lit l in
+		  let a, b = args.(0), args.(1) in
+		  let na, nb = Form.neg a, Form.neg b in
+		  link_Other (BuildDef nl) [nl;a;b];
+		  link_Other (BuildDef pl) [pl;a;nb];
+		  link_Other (BuildDef2 nl) [nl;na;nb];
+		  link_Other (BuildDef2 pl) [pl;na;b];
+		  set_done l;
+		  cnf a;
+		  cnf b
+		
+	      | Fiff ->
+		  let nl,pl = both_lit l in
+		  let a, b = args.(0), args.(1) in
+		  let na, nb = Form.neg a, Form.neg b in
+		  link_Other (BuildDef nl) [nl;a;nb];
+		  link_Other (BuildDef pl) [pl;na;nb];
+		  link_Other (BuildDef2 nl) [pl;na;b];
+		  link_Other (BuildDef2 pl) [pl;a;b];
+		  set_done l;
+		  cnf a;
+		  cnf b
+
+	      | Fite ->
+		  let nl,pl = both_lit l in
+		  let a, b, c = args.(0), args.(1), args.(2) in
+		  let na, nb, nc = Form.neg a, Form.neg b, Form.neg c in
+		  link_Other (BuildDef nl) [nl;a;c];
+		  link_Other (BuildDef pl) [pl;a;nc];
+		  link_Other (BuildDef2 nl) [nl;na;b];
+		  link_Other (BuildDef2 pl) [pl;na;nb];
+		  set_done l;
+		  cnf a;
+		  cnf b;
+		  cnf c
+
+	      | Fnot2 _ -> cnf args.(0)
+ 
+    exception Cnf_done
+
+    let rec imm_link_Other other l =
+      if not (test_immediate l) then
+	let c = mkOther other (Some [l]) in
+	link !last c;
+	last := c;
+	imm_cnf c
+
+    and imm_cnf c =
+      let l = 
+	match c.value with
+	| Some [l] -> 
+	    begin match Form.pform l with
+	    | Fapp (Fnot2 _, args) -> 
+		let l' = args.(0) in
+		if Form.is_pos l then l'
+		else Form.neg l'
+	    | _ -> l
+	    end
+	| _ -> assert false in
+      match get_info l with
+      | Immediate b -> if b = Form.is_neg l then raise Cnf_done
+      | Done -> assert false
+      | Todo ->
+	  set_immediate l;
+
+	  match Form.pform l with
+	  | Fatom _ -> ()
+
+	  | Fapp (op,args) ->
+	      match op with
+	      | Ftrue | Ffalse -> ()
+
+	      | Fand ->
+		  if Form.is_pos l then 
+		    Array.iteri (fun i l' -> 
+		      imm_link_Other (ImmBuildProj(c,i)) l') args
+		  else begin
+		    let nargs = Array.map Form.neg args in
+		    link_Other (ImmBuildDef c) (Array.to_list nargs);
+		    push_cnf args
+		  end
+
+	      | For ->
+		  if Form.is_pos l then begin
+		    link_Other (ImmBuildDef c) (Array.to_list args);
+		    push_cnf args
+		  end else 
+		    Array.iteri (fun i l' ->
+		      imm_link_Other (ImmBuildProj(c,i)) (Form.neg l')) args
+
+	      | Fimp ->
+		  let args = or_of_imp args in
+		  if Form.is_pos l then begin
+		    link_Other (ImmBuildDef c) (Array.to_list args);
+		    push_cnf args
+		  end else 
+		    Array.iteri (fun i l' ->
+		      imm_link_Other (ImmBuildProj(c,i)) (Form.neg l')) args
+
+	      | Fxor -> 
+		  let args1 = 
+		    if Form.is_pos l then [args.(0);args.(1)]
+		    else [args.(0);Form.neg args.(1)] in
+		  let args2 =
+		    if Form.is_pos l then [Form.neg args.(0);Form.neg args.(1)] 
+		    else  [Form.neg args.(0); args.(1)] in
+		  link_Other (ImmBuildDef c) args1;
+		  link_Other (ImmBuildDef2 c) args2;
+		  push_cnf args
+		
+	      | Fiff ->
+		  let args1 = 
+		    if Form.is_pos l then [args.(0);Form.neg args.(1)]
+		    else [Form.neg args.(0);Form.neg args.(1)] in
+		  let args2 =
+		    if Form.is_pos l then [Form.neg args.(0);args.(1)] 
+		    else  [args.(0); args.(1)] in
+		  link_Other (ImmBuildDef c) args1;
+		  link_Other (ImmBuildDef2 c) args2;
+		  push_cnf args
+
+	      | Fite ->
+		  let args1 = 
+		    if Form.is_pos l then [args.(0);Form.neg args.(2)]
+		    else [args.(0);Form.neg args.(2)] in
+		  let args2 =
+		    if Form.is_pos l then [Form.neg args.(0);args.(1)] 
+		    else  [Form.neg args.(0); Form.neg args.(1)] in
+		  link_Other (ImmBuildDef c) args1;
+		  link_Other (ImmBuildDef2 c) args2;
+		  push_cnf args
+
+              | Fnot2 _ -> assert false
+
+    let make_cnf reify c =
+      let ftrue = Form.get reify (Fapp(Ftrue, [||])) in
+      let ffalse = Form.get reify (Fapp(Ffalse, [||])) in
+      last := c;
+      link_Other True [ftrue];
+      link_Other False [Form.neg ffalse];
+      (try 
+	imm_cnf c;
+	List.iter (Array.iter cnf) !cnf_todo
+      with Cnf_done -> ());
+      let res = !last in
+      clear ();
+      res
+
+  end
+
diff --git a/src/trace/smtForm.ml b/src/trace/smtForm.ml
new file mode 100644
index 0000000..6075b3f
--- /dev/null
+++ b/src/trace/smtForm.ml
@@ -0,0 +1,510 @@
+(**************************************************************************)
+(*                                                                        *)
+(*     SMTCoq                                                             *)
+(*     Copyright (C) 2011 - 2015                                          *)
+(*                                                                        *)
+(*     Michaël Armand                                                     *)
+(*     Benjamin Grégoire                                                  *)
+(*     Chantal Keller                                                     *)
+(*                                                                        *)
+(*     Inria - École Polytechnique - MSR-Inria Joint Lab                  *)
+(*                                                                        *)
+(*   This file is distributed under the terms of the CeCILL-C licence     *)
+(*                                                                        *)
+(**************************************************************************)
+open Util
+open SmtMisc
+open CoqTerms
+open Errors
+
+module type ATOM = 
+  sig 
+
+    type t 
+    val index : t -> int
+
+    val equal : t -> t -> bool
+
+    val is_bool_type : t -> bool
+
+  end 
+
+
+type fop =
+  | Ftrue
+  | Ffalse
+  | Fand
+  | For
+  | Fxor
+  | Fimp
+  | Fiff
+  | Fite
+  | Fnot2 of int
+
+type ('a,'f) gen_pform = 
+  | Fatom of 'a
+  | Fapp of fop * 'f array
+
+
+module type FORM =
+  sig 
+    type hatom 
+    type t
+    type pform = (hatom, t) gen_pform
+
+      val pform_true : pform
+      val pform_false : pform
+
+      val equal : t -> t -> bool
+
+      val to_lit : t -> int
+      val index : t -> int
+      val pform : t -> pform
+
+      val neg : t -> t
+      val is_pos : t -> bool
+      val is_neg : t -> bool
+
+      val to_smt : (Format.formatter -> hatom -> unit) -> Format.formatter -> t -> unit
+
+      (* Building formula from positive formula *)
+      exception NotWellTyped of pform
+      type reify 
+      val create : unit -> reify 
+      val clear : reify -> unit
+      val get : reify -> pform -> t
+      
+      (** Give a coq term, build the corresponding formula *)  
+      val of_coq : (Term.constr -> hatom) -> reify -> Term.constr -> t
+   
+      (** Flattening of [Fand] and [For], removing of [Fnot2]  *)
+      val flatten : reify -> t -> t
+
+      (** Producing Coq terms *) 
+
+      val to_coq : t -> Term.constr
+
+      val pform_tbl : reify -> pform array
+
+      val to_array : reify -> 'a -> (pform -> 'a) -> int * 'a array
+      val interp_tbl : reify -> Term.constr * Term.constr
+      val nvars : reify -> int 
+      (** Producing a Coq term corresponding to the interpretation 
+          of a formula *)
+      (** [interp_atom] map [hatom] to coq term, it is better if it produce
+          shared terms. *)
+      val interp_to_coq : 
+	  (hatom -> Term.constr) -> (int, Term.constr) Hashtbl.t -> 
+	    t -> Term.constr
+  end
+
+module Make (Atom:ATOM) =
+  struct 
+
+    type hatom = Atom.t 
+
+    type pform = (Atom.t, t) gen_pform
+ 
+    and hpform = pform gen_hashed
+	  
+    and t = 
+      | Pos of hpform
+      | Neg of hpform 
+
+    let pform_true = Fapp (Ftrue,[||])
+    let pform_false = Fapp (Ffalse,[||])
+
+    let equal h1 h2 = 
+      match h1, h2 with
+      | Pos hp1, Pos hp2 -> hp1.index == hp2.index
+      | Neg hp1, Neg hp2 -> hp1.index == hp2.index
+      | _, _ -> false
+
+    let index = function
+      | Pos hp -> hp.index
+      | Neg hp -> hp.index
+
+    let to_lit = function
+      | Pos hp -> hp.index * 2
+      | Neg hp -> hp.index * 2 + 1
+
+    let neg = function
+      | Pos hp -> Neg hp
+      | Neg hp -> Pos hp
+	    
+    let is_pos = function
+      | Pos _ -> true
+      | _ -> false
+	    
+    let is_neg = function
+      | Neg _ -> true
+      | _ -> false
+
+    let pform = function
+      | Pos hp -> hp.hval
+      | Neg hp -> hp.hval
+
+
+    let rec to_smt atom_to_smt fmt = function
+      | Pos hp -> to_smt_pform atom_to_smt fmt hp.hval
+      | Neg hp ->
+        Format.fprintf fmt "(not ";
+        to_smt_pform atom_to_smt fmt hp.hval;
+        Format.fprintf fmt ")"
+
+    and to_smt_pform atom_to_smt fmt = function
+      | Fatom a -> atom_to_smt fmt a
+      | Fapp (op,args) -> to_smt_op atom_to_smt fmt op args
+
+    and to_smt_op atom_to_smt fmt op args =
+      let s = match op with
+        | Ftrue -> "true"
+        | Ffalse -> "false"
+        | Fand -> "and"
+        | For -> "or"
+        | Fxor -> "xor"
+        | Fimp -> "=>"
+        | Fiff -> "="
+        | Fite -> "ite"
+        | Fnot2 _ -> "" in
+      let (s1,s2) = if Array.length args = 0 then ("","") else ("(",")") in
+      Format.fprintf fmt "%s%s" s1 s;
+      Array.iter (fun h -> Format.fprintf fmt " "; to_smt atom_to_smt fmt h) args;
+      Format.fprintf fmt "%s" s2
+
+
+    module HashedForm =
+      struct 
+	
+	type t = pform
+	      
+	let equal pf1 pf2 = 
+	  match pf1, pf2 with
+	  | Fatom ha1, Fatom ha2 -> Atom.equal ha1 ha2
+	  | Fapp(op1,args1), Fapp(op2,args2) ->
+	      op1 = op2 && 
+	      Array.length args1 == Array.length args2 &&
+	      (try 
+		for i = 0 to Array.length args1 - 1 do
+		  if not (equal args1.(i) args2.(i)) then raise Not_found 
+		done;
+		true
+	      with Not_found -> false)
+	  | _, _ -> false
+
+	let hash pf = 
+	  match pf with
+	  | Fatom ha1 -> Atom.index ha1 * 2 
+	  | Fapp(op, args) -> 
+	      let hash_args =
+		match Array.length args with
+		| 0 -> 0
+		| 1 -> to_lit args.(0)
+		| 2 -> (to_lit args.(1)) lsl 2 + to_lit args.(0)
+		| _ -> 
+		    (to_lit args.(2)) lsl 4 + (to_lit args.(1)) lsl 2 +
+		      to_lit args.(0) in
+	      (hash_args * 10 + Hashtbl.hash op) * 2 + 1
+		
+      end
+
+    module HashForm = Hashtbl.Make (HashedForm)
+
+    type reify = {
+	mutable count : int;
+                tbl : t HashForm.t 
+      }  
+
+    exception NotWellTyped of pform
+   	
+    let check pf = 
+      match pf with
+      | Fatom ha ->  if not (Atom.is_bool_type ha) then raise (NotWellTyped pf)
+      | Fapp (op, args) ->
+	  match op with
+	  | Ftrue | Ffalse -> 
+	      if Array.length args <> 0 then raise (NotWellTyped pf)
+	  | Fnot2 _ -> 
+	      if Array.length args <> 1 then raise (NotWellTyped pf)
+	  | Fand | For -> ()
+	  | Fxor | Fimp | Fiff ->
+	      if Array.length args <> 2 then raise (NotWellTyped pf)
+	  | Fite ->
+	      if Array.length args <> 3 then raise (NotWellTyped pf)
+
+    let declare reify pf =
+      check pf;
+      let res = Pos {index = reify.count; hval = pf} in
+      HashForm.add reify.tbl pf res;
+      reify.count <- reify.count + 1;
+      res
+
+    let create () =
+      let reify = 
+	{ count = 0; 
+	  tbl =  HashForm.create 17 } in
+      let _ = declare reify pform_true in
+      let _ = declare reify pform_false in
+      reify
+
+    let clear r =
+      r.count <- 0;
+      HashForm.clear r.tbl;
+      let _ = declare r pform_true in
+      let _ = declare r pform_false in
+      ()
+
+    let get reify pf =
+      try HashForm.find reify.tbl pf 
+      with Not_found -> declare reify pf
+
+
+    (** Given a coq term, build the corresponding formula *)  
+    type coq_cst = 
+      | CCtrue
+      | CCfalse
+      | CCnot
+      | CCand
+      | CCor
+      | CCxor
+      | CCimp
+      | CCiff
+      | CCifb
+      | CCunknown
+
+    let op_tbl () =
+      let tbl = Hashtbl.create 29 in
+      let add (c1,c2) = Hashtbl.add tbl (Lazy.force c1) c2 in
+      List.iter add 
+	[
+	 ctrue,CCtrue; cfalse,CCfalse;
+	 candb,CCand; corb,CCor; cxorb,CCxor; cimplb,CCimp; cnegb,CCnot;
+         ceqb,CCiff; cifb,CCifb ];
+      tbl
+
+    let op_tbl = lazy (op_tbl ())
+
+    let empty_args = [||]
+
+    let of_coq atom_of_coq reify c =
+      let op_tbl = Lazy.force op_tbl in
+      let get_cst c = 
+	try Hashtbl.find op_tbl c with Not_found -> CCunknown in
+      let rec mk_hform h =
+	let c, args = Term.decompose_app h in
+	match get_cst c with
+	| CCtrue  -> get reify (Fapp(Ftrue,empty_args))
+	| CCfalse -> get reify (Fapp(Ffalse,empty_args))
+	| CCnot -> mk_fnot 1 args
+	| CCand -> mk_fand [] args
+	| CCor  -> mk_for [] args
+	| CCxor -> op2 (fun l -> Fapp(Fxor,l)) args
+	| CCiff -> op2 (fun l -> Fapp(Fiff,l)) args
+	| CCimp ->
+          (match args with
+            | [b1;b2] ->
+              let l1 = mk_hform b1 in
+              let l2 = mk_hform b2 in
+              get reify (Fapp (Fimp, [|l1;l2|]))
+            | _ -> error "SmtForm.Form.of_coq: wrong number of arguments for implb")
+	| CCifb ->
+	    (* We should also be able to syntaxify if then else *)
+	    begin match args with
+	    | [b1;b2;b3] ->
+		let l1 = mk_hform b1 in
+		let l2 = mk_hform b2 in
+		let l3 = mk_hform b3 in
+		get reify (Fapp(Fite, [|l1;l2;l3|]))
+	    | _ -> error "SmtForm.Form.of_coq: wrong number of arguments for ifb"
+	    end
+	| _ -> 
+	    let a = atom_of_coq  h in
+            get reify (Fatom a)
+
+      and op2 f args =
+	match args with
+	| [b1;b2] ->
+	    let l1 = mk_hform b1 in
+            let l2 = mk_hform b2 in
+            get reify (f [|l1; l2|])
+	| _ ->  error "SmtForm.Form.of_coq: wrong number of arguments"
+	  
+      and mk_fnot i args =
+	match args with
+	| [t] -> 
+	    let c,args = Term.decompose_app t in
+	    if c = Lazy.force cnegb then
+              mk_fnot (i+1) args
+	    else 
+              let q,r = i lsr 1 , i land 1 in
+              let l = mk_hform t in
+              let l = if r = 0 then l else neg l in
+	      if q = 0 then l
+	      else get reify (Fapp(Fnot2 q, [|l|]))
+	| _ -> error "SmtForm.Form.mk_hform: wrong number of arguments for negb"
+	  
+      and mk_fand acc args = 
+	match args with
+	| [t1;t2] -> 
+	    let l2 = mk_hform t2 in
+	    let c, args = Term.decompose_app t1 in
+	    if c = Lazy.force candb then
+              mk_fand (l2::acc) args
+	    else 
+	      let l1 = mk_hform t1 in
+	      get reify (Fapp(Fand, Array.of_list  (l1::l2::acc)))
+	| _ -> error "SmtForm.Form.mk_hform: wrong number of arguments for andb" 
+
+      and mk_for acc args = 
+	match args with
+	| [t1;t2] -> 
+	    let l2 = mk_hform t2 in
+	    let c, args = Term.decompose_app t1 in
+	    if c = Lazy.force corb then
+              mk_for (l2::acc) args
+	    else 
+	      let l1 = mk_hform t1 in
+	      get reify (Fapp(For, Array.of_list (l1::l2::acc)))
+	| _ -> error "SmtForm.Form.mk_hform: wrong number of arguments for orb" in
+
+      let l = mk_hform c in
+      l
+
+    (** Flattening of Fand and For, removing of Fnot2 *)
+    let set_sign f f' =
+      if is_pos f then f' else neg f'
+
+    let rec flatten reify f = 
+      match pform f with
+      | Fatom _ -> f
+      | Fapp(Fnot2 _,args) -> set_sign f (flatten reify args.(0))
+      | Fapp(Fand, args) -> set_sign f (flatten_and reify [] (Array.to_list args))
+      | Fapp(For,args) -> set_sign f (flatten_or reify [] (Array.to_list args))
+      | Fapp(op,args) ->
+          (* TODO change Fimp into For ? *)
+	  set_sign f (get reify (Fapp(op, Array.map (flatten reify) args)))
+
+    and flatten_and reify acc args =
+      match args with
+      | [] -> get reify (Fapp(Fand, Array.of_list (List.rev acc)))
+      | a::args ->
+	  (* TODO change (not For) and (not Fimp) into Fand *)
+	  match pform a with
+	  | Fapp(Fand, args') when is_pos a ->
+	      let args = Array.fold_right (fun a args -> a::args) args' args in
+	      flatten_and reify acc args
+	  | _ -> flatten_and reify (flatten reify a :: acc) args
+
+    and flatten_or reify acc args =
+      (* TODO change Fimp and (not Fand) into For *)
+      match args with
+      | [] -> get reify (Fapp(For, Array.of_list (List.rev acc)))
+      | a::args ->
+	  match pform a with
+	  | Fapp(For, args') when is_pos a ->
+	      let args = Array.fold_right (fun a args -> a::args) args' args in
+	      flatten_or reify acc args
+	  | _ -> flatten_or reify (flatten reify a :: acc) args
+
+    (** Producing Coq terms *) 
+
+    let to_coq hf = mkInt (to_lit hf)
+
+    let args_to_coq args =
+      let cargs = Array.make (Array.length args + 1) (mkInt 0) in
+      Array.iteri (fun i hf -> cargs.(i) <- to_coq hf) args;
+      Term.mkArray (Lazy.force cint, cargs)
+	
+    let pf_to_coq = function
+      | Fatom a -> mklApp cFatom [|mkInt (Atom.index a)|]	
+      | Fapp(op,args) ->
+        match op with
+	| Ftrue -> Lazy.force cFtrue
+	| Ffalse -> Lazy.force cFfalse
+	| Fand -> mklApp cFand [| args_to_coq args|]
+	| For  -> mklApp cFor [| args_to_coq args|]
+	| Fimp -> mklApp cFimp [| args_to_coq args|]
+	| Fxor -> mklApp cFxor (Array.map to_coq args)
+	| Fiff -> mklApp cFiff (Array.map to_coq args)
+	| Fite -> mklApp cFite (Array.map to_coq args)
+	| Fnot2 i -> mklApp cFnot2 [|mkInt i; to_coq args.(0)|]
+
+    let pform_tbl reify =
+      let t = Array.make reify.count pform_true in
+      let set _ h =
+	match h with
+	| Pos hp -> t.(hp.index) <- hp.hval
+	| _ -> assert false in
+      HashForm.iter set reify.tbl;
+      t
+
+    let to_array reify dft f =
+      let t = Array.make (reify.count + 1) dft in
+      let set _ h =
+	match h with
+	| Pos hp -> t.(hp.index) <- f hp.hval
+	| _ -> assert false in
+      HashForm.iter set reify.tbl;
+      (reify.count, t)
+
+    let interp_tbl reify =
+      let (i,t) = to_array reify (Lazy.force cFtrue) pf_to_coq in
+      (mkInt i, Term.mkArray (Lazy.force cform, t))
+
+    let nvars reify = reify.count
+    (** Producing a Coq term corresponding to the interpretation of a formula *)
+    (** [interp_atom] map [Atom.t] to coq term, it is better if it produce
+	shared terms. *)
+    let interp_to_coq interp_atom form_tbl f =
+      let rec interp_form f = 
+	let l = to_lit f in
+	try Hashtbl.find form_tbl l 
+	with Not_found ->
+	  if is_neg f then 
+	    let pc = interp_form (neg f) in
+	    let nc = mklApp cnegb [|pc|] in
+	    Hashtbl.add form_tbl l nc;
+	    nc
+	  else
+	    let pc = 
+	      match pform f with
+	      | Fatom a -> interp_atom a
+	      | Fapp(op, args) ->
+		  match op with
+		  | Ftrue -> Lazy.force ctrue
+		  | Ffalse -> Lazy.force cfalse
+		  | Fand -> interp_args candb args
+		  | For -> interp_args corb args
+		  | Fxor -> interp_args cxorb args
+		  | Fimp -> 
+		      let r = ref (interp_form args.(Array.length args - 1)) in
+		      for i = Array.length args - 2 downto 0 do
+			r := mklApp cimplb [|interp_form args.(i); !r|]
+		      done;
+		      !r
+		  | Fiff -> interp_args ceqb args
+		  | Fite -> 
+		      (* TODO with if here *)
+		      mklApp cifb (Array.map interp_form args)
+		  | Fnot2 n -> 
+		      let r = ref (interp_form args.(0)) in
+		      for i = 1 to n do	r := mklApp cnegb [|!r|] done;
+		      !r in 
+	    Hashtbl.add form_tbl l pc;
+	    pc
+      and interp_args op args =
+	let r = ref (interp_form args.(0)) in
+	for i = 1 to Array.length args - 1 do
+	  r := mklApp op [|!r;interp_form args.(i)|] 
+	done;
+	!r in
+      interp_form f
+
+  end
+	
+
+	  
+
+    
+
+  
diff --git a/src/trace/smtForm.mli b/src/trace/smtForm.mli
new file mode 100644
index 0000000..118ecf5
--- /dev/null
+++ b/src/trace/smtForm.mli
@@ -0,0 +1,99 @@
+(**************************************************************************)
+(*                                                                        *)
+(*     SMTCoq                                                             *)
+(*     Copyright (C) 2011 - 2015                                          *)
+(*                                                                        *)
+(*     Michaël Armand                                                     *)
+(*     Benjamin Grégoire                                                  *)
+(*     Chantal Keller                                                     *)
+(*                                                                        *)
+(*     Inria - École Polytechnique - MSR-Inria Joint Lab                  *)
+(*                                                                        *)
+(*   This file is distributed under the terms of the CeCILL-C licence     *)
+(*                                                                        *)
+(**************************************************************************)
+
+module type ATOM = 
+  sig 
+
+    type t 
+    val index : t -> int
+
+    val equal : t -> t -> bool
+
+    val is_bool_type : t -> bool
+
+  end 
+
+
+type fop =
+  | Ftrue
+  | Ffalse
+  | Fand
+  | For
+  | Fxor
+  | Fimp
+  | Fiff
+  | Fite
+  | Fnot2 of int
+
+ 
+type ('a,'f) gen_pform = 
+  | Fatom of 'a
+  | Fapp of fop * 'f array
+
+module type FORM =
+  sig 
+    type hatom 
+    type t
+    type pform = (hatom, t) gen_pform
+
+      val pform_true : pform
+      val pform_false : pform
+
+      val equal : t -> t -> bool
+
+      val to_lit : t -> int
+      val index : t -> int
+      val pform : t -> pform
+
+      val neg : t -> t
+      val is_pos : t -> bool
+      val is_neg : t -> bool
+
+      val to_smt : (Format.formatter -> hatom -> unit) -> Format.formatter -> t -> unit
+
+      (* Building formula from positive formula *)
+      exception NotWellTyped of pform
+      type reify 
+      val create : unit -> reify
+      val clear : reify -> unit
+      val get : reify -> pform -> t
+      
+      (** Given a coq term, build the corresponding formula *)  
+      val of_coq : (Term.constr -> hatom) -> reify -> Term.constr -> t
+   
+      (** Flattening of [Fand] and [For], removing of [Fnot2]  *)
+      val flatten : reify -> t -> t
+
+      (** Producing Coq terms *) 
+
+      val to_coq : t -> Term.constr
+
+      val pform_tbl : reify -> pform array
+
+      val to_array : reify -> 'a -> (pform -> 'a) -> int * 'a array
+      val interp_tbl : reify -> Term.constr * Term.constr
+      val nvars : reify -> int 
+      (** Producing a Coq term corresponding to the interpretation 
+          of a formula *)
+      (** [interp_atom] map [hatom] to coq term, it is better if it produce
+          shared terms. *)
+      val interp_to_coq : 
+	  (hatom -> Term.constr) -> (int, Term.constr) Hashtbl.t -> 
+	    t -> Term.constr
+  end
+
+module Make (Atom:ATOM) : FORM with type hatom = Atom.t
+
+	
diff --git a/src/trace/smtMisc.ml b/src/trace/smtMisc.ml
new file mode 100644
index 0000000..02e5f26
--- /dev/null
+++ b/src/trace/smtMisc.ml
@@ -0,0 +1,47 @@
+(**************************************************************************)
+(*                                                                        *)
+(*     SMTCoq                                                             *)
+(*     Copyright (C) 2011 - 2015                                          *)
+(*                                                                        *)
+(*     Michaël Armand                                                     *)
+(*     Benjamin Grégoire                                                  *)
+(*     Chantal Keller                                                     *)
+(*                                                                        *)
+(*     Inria - École Polytechnique - MSR-Inria Joint Lab                  *)
+(*                                                                        *)
+(*   This file is distributed under the terms of the CeCILL-C licence     *)
+(*                                                                        *)
+(**************************************************************************)
+
+
+(** Sharing of coq Int *)
+let cInt_tbl = Hashtbl.create 17 
+
+let mkInt i = 
+  try Hashtbl.find cInt_tbl i 
+  with Not_found ->
+    let ci = Term.mkInt (Uint63.of_int i) in
+    Hashtbl.add cInt_tbl i ci;
+    ci
+
+(** Generic representation of shared object *)
+type 'a gen_hashed = { index : int; hval : 'a }
+
+(** Functions over constr *)
+
+let mklApp f args = Term.mkApp (Lazy.force f, args)
+
+(* TODO : Set -> Type *)
+let coqtype = lazy Term.mkSet
+
+let declare_new_type t =
+  Command.declare_assumption false (Decl_kinds.Local,Decl_kinds.Definitional) (Lazy.force coqtype) [] false None (Pp.dummy_loc,t);
+  Term.mkVar t
+
+let declare_new_variable v constr_t =
+  Command.declare_assumption false (Decl_kinds.Local,Decl_kinds.Definitional) constr_t [] false None (Pp.dummy_loc,v);
+  Term.mkVar v
+
+let mkName s =
+  let id = Names.id_of_string s in
+  Names.Name id
diff --git a/src/trace/smtTrace.ml b/src/trace/smtTrace.ml
new file mode 100644
index 0000000..8420ca1
--- /dev/null
+++ b/src/trace/smtTrace.ml
@@ -0,0 +1,465 @@
+(**************************************************************************)
+(*                                                                        *)
+(*     SMTCoq                                                             *)
+(*     Copyright (C) 2011 - 2015                                          *)
+(*                                                                        *)
+(*     Michaël Armand                                                     *)
+(*     Benjamin Grégoire                                                  *)
+(*     Chantal Keller                                                     *)
+(*                                                                        *)
+(*     Inria - École Polytechnique - MSR-Inria Joint Lab                  *)
+(*                                                                        *)
+(*   This file is distributed under the terms of the CeCILL-C licence     *)
+(*                                                                        *)
+(**************************************************************************)
+open SmtMisc
+open CoqTerms
+open SmtCertif
+
+let notUsed = 0
+
+let next_id = ref 0 
+
+let clear () = next_id := 0
+
+let next_id () =
+  let id = !next_id in
+  incr next_id;
+  id
+
+(** Basic functions over small certificates *)
+
+let mk_scertif kind ov = 
+  {
+   id   = next_id ();
+   kind = kind;
+   pos  = None;
+   used = notUsed;
+   prev = None;
+   next = None;
+   value = ov 
+ }
+  
+(** Roots *)
+
+
+let mkRootGen ov = 
+  let pos = next_id () in
+  {
+   id   = pos;
+   kind = Root;
+   pos  = Some pos;
+   used = notUsed;
+   prev = None;
+   next = None;
+   value = ov 
+ }
+
+(* let mkRoot = mkRootGen None *)
+let mkRootV v = mkRootGen (Some v)
+ 
+let isRoot k = k == Root 
+
+(** Resolutions *)
+
+let mkRes c1 c2 tl = 
+  mk_scertif (Res { rc1 = c1; rc2 = c2; rtail = tl }) None
+
+let isRes k =
+  match k with
+    | Res _ -> true
+    | _ -> false
+
+
+(** Other *)
+
+let mkOther r ov = mk_scertif (Other r) ov
+
+
+(** Moving into the trace *)
+let next c =
+  match c.next with
+  | Some c1 -> c1
+  | None -> assert false
+
+let has_prev c =
+  match c.prev with
+    | Some _ -> true
+    | None -> false
+
+let prev c =
+  match c.prev with
+  | Some c1 -> c1
+  | None -> Printf.printf "prev %i\n" c.id;flush stdout;assert false
+
+let link c1 c2 =
+  c1.next <- Some c2;
+  c2.prev <- Some c1
+
+let clear_links c =
+  c.prev <- None;
+  c.next <- None
+
+let skip c =
+  link (prev c) (next c);
+  clear_links c
+
+let insert_before c cprev =
+  link (prev c) cprev;
+  link cprev c
+
+let get_res c s =
+  match c.kind with
+  | Res res -> res
+  | _ -> Printf.printf "get_res %s\n" s; assert false
+
+let get_other c s =
+  match c.kind with
+  | Other res -> res
+  | _ -> Printf.printf "get_other %s\n" s; assert false
+
+let get_val c =
+  match c.value with
+  | None -> assert false
+  | Some cl -> cl
+
+let rec repr c =
+  match c.kind with
+  | Root | Res _ | Other _ -> c
+  | Same c -> repr c
+
+let set_same c nc =
+  c.kind <- Same (repr nc);
+  skip c
+
+let rec get_pos c =
+  match c.kind with
+  | Root | Res _ | Other _ ->
+      begin match c.pos with
+      | Some n -> n
+      | _ -> assert false
+      end
+  | Same c -> get_pos c 
+
+let eq_clause c1 c2 = (repr c1).id = (repr c2).id
+
+(* Selection of useful rules *)
+let select c =
+  let mark c =
+    if not (isRoot c.kind) then c.used <- 1 in
+  mark c;
+  let r = ref c in
+  while not (isRoot !r.kind) do
+    let p = prev !r in
+    (match !r.kind with
+      | Res res ->
+      if !r.used == 1 then begin
+        !r.used <- notUsed;
+        (* let res = get_res !r "select" in *)
+        mark res.rc1; mark res.rc2;
+        List.iter mark res.rtail
+      end else
+        skip !r;
+      | Same _ ->
+        skip !r
+      | _ ->
+      if !r.used == 1 then 
+	begin
+          !r.used <- notUsed;
+          let rl = get_other !r "select" in
+          List.iter mark (used_clauses rl)
+	end 
+      else skip !r;
+    );
+    r := p
+  done
+
+ 
+
+
+(* Compute the number of occurence of each_clause *)
+
+let rec occur c =
+  match c.kind with
+  | Root -> c.used <- c.used + 1
+  | Res res ->
+      if c.used == notUsed then 
+	begin occur res.rc1; occur res.rc2; List.iter occur res.rtail end;
+      c.used <- c.used + 1
+  | Other res ->
+      if c.used == notUsed then List.iter occur (used_clauses res);
+      c.used <- c.used + 1;
+  | Same c' ->
+    occur c';
+    c.used <- c.used + 1
+
+(* Allocate clause *)
+
+let alloc c =
+  let free_pos = ref [] in
+
+  (* free the unused roots *)
+
+  let r = ref c in
+  while isRoot !r.kind do
+    if !r.used == notUsed then begin
+      free_pos := get_pos !r :: !free_pos;
+    end;
+    r := next !r;
+  done;
+
+  (* r is the first clause defined by resolution or another rule,
+     normaly the first used *)
+  let last_set = ref (get_pos (prev !r)) in
+
+  let decr_clause c =
+    let rc = repr c in
+      assert (rc.used > notUsed);
+    rc.used <- rc.used - 1;
+    if rc.used = notUsed then
+      free_pos := get_pos rc :: !free_pos in
+
+  let decr_res res =
+    decr_clause res.rc1;
+    decr_clause res.rc2;
+    List.iter decr_clause res.rtail in
+
+  let decr_other o =
+    List.iter decr_clause (used_clauses o) in
+
+  while !r.next <> None do
+    let n = next !r in
+      assert (!r.used <> notUsed);
+    if isRes !r.kind then
+      decr_res (get_res !r "alloc")
+    else
+      decr_other (get_other !r "alloc");
+    begin match !free_pos with
+    | p::free -> free_pos := free; !r.pos <- Some p
+    | _ -> incr last_set; !r.pos <- Some !last_set
+    end;
+    r := n
+  done;
+  begin match !free_pos with
+  | p::free -> free_pos := free; !r.pos <- Some p
+  | _ -> incr last_set; !r.pos <- Some !last_set
+  end;
+  !last_set
+
+
+(* A naive allocation for debugging *)
+
+let naive_alloc c =
+  let r = ref c in
+  while isRoot !r.kind do
+    r := next !r
+  done;
+  let last_set = ref (get_pos (prev !r)) in
+  while !r.next <> None do
+    let n = next !r in
+    incr last_set; !r.pos <- Some !last_set;
+    r := n
+  done;
+  incr last_set; !r.pos <- Some !last_set;
+  !last_set
+
+
+(* This function is currently inlined in verit/verit.ml and zchaff/zchaff.ml *)
+
+let build_certif first_root confl =
+  select confl;
+  occur confl;
+  alloc first_root
+
+
+let to_coq to_lit (cstep,
+    cRes, cImmFlatten,
+    cTrue, cFalse, cBuildDef, cBuildDef2, cBuildProj,
+    cImmBuildProj,cImmBuildDef,cImmBuildDef2,  
+    cEqTr, cEqCgr, cEqCgrP, 
+    cLiaMicromega, cLiaDiseq, cSplArith, cSplDistinctElim) confl =
+  let out_f f = to_lit f in
+  let out_c c = mkInt (get_pos c) in
+  let step_to_coq c =
+    match c.kind with
+    | Res res -> 
+	let size = List.length res.rtail + 3 in
+	let args = Array.make size (mkInt 0) in
+	args.(0) <- mkInt (get_pos res.rc1);
+	args.(1) <- mkInt (get_pos res.rc2);
+	let l = ref res.rtail in
+	for i = 2 to size - 2 do
+	  match !l with
+	  | c::tl -> 
+	      args.(i) <- mkInt (get_pos c);
+	      l := tl
+	  | _ -> assert false 
+	done;
+	mklApp cRes [|mkInt (get_pos c); Term.mkArray (Lazy.force cint, args)|]
+    | Other other ->
+	begin match other with
+	| ImmFlatten (c',f) -> mklApp cImmFlatten [|out_c c;out_c c'; out_f f|]
+        | True -> mklApp cTrue [|out_c c|]
+	| False -> mklApp cFalse [|out_c c|]
+	| BuildDef f -> mklApp cBuildDef [|out_c c; out_f f|]
+	| BuildDef2 f -> mklApp cBuildDef2 [|out_c c;out_f f|]
+	| BuildProj (f, i) -> mklApp cBuildProj [|out_c c; out_f f;mkInt i|]
+	| ImmBuildDef c' -> mklApp cImmBuildDef [|out_c c; out_c c'|]
+	| ImmBuildDef2 c' -> mklApp cImmBuildDef2 [|out_c c;out_c c'|]
+	| ImmBuildProj(c', i) -> mklApp cImmBuildProj [|out_c c; out_c c';mkInt i|]
+        | EqTr (f, fl) ->
+          let res = List.fold_right (fun f l -> mklApp ccons [|Lazy.force cint; out_f f; l|]) fl (mklApp cnil [|Lazy.force cint|]) in
+          mklApp cEqTr [|out_c c; out_f f; res|]
+        | EqCgr (f, fl) ->
+          let res = List.fold_right (fun f l -> mklApp ccons [|mklApp coption [|Lazy.force cint|]; (match f with | Some f -> mklApp cSome [|Lazy.force cint; out_f f|] | None -> mklApp cNone [|Lazy.force cint|]); l|]) fl (mklApp cnil [|mklApp coption [|Lazy.force cint|]|]) in
+          mklApp cEqCgr [|out_c c; out_f f; res|]
+        | EqCgrP (f1, f2, fl) ->
+          let res = List.fold_right (fun f l -> mklApp ccons [|mklApp coption [|Lazy.force cint|]; (match f with | Some f -> mklApp cSome [|Lazy.force cint; out_f f|] | None -> mklApp cNone [|Lazy.force cint|]); l|]) fl (mklApp cnil [|mklApp coption [|Lazy.force cint|]|]) in
+          mklApp cEqCgrP [|out_c c; out_f f1; out_f f2; res|]
+	| LiaMicromega (cl,d) ->
+          let cl' = List.fold_right (fun f l -> mklApp ccons [|Lazy.force cint; out_f f; l|]) cl (mklApp cnil [|Lazy.force cint|]) in
+          let c' = List.fold_right (fun f l -> mklApp ccons [|Lazy.force Coq_micromega.M.coq_proofTerm; Coq_micromega.dump_proof_term f; l|]) d (mklApp cnil [|Lazy.force Coq_micromega.M.coq_proofTerm|]) in
+          mklApp cLiaMicromega [|out_c c; cl'; c'|]
+        | LiaDiseq l -> mklApp cLiaDiseq [|out_c c; out_f l|]
+        | SplArith (orig,res,l) ->
+          let res' = out_f res in
+          let l' = List.fold_right (fun f l -> mklApp ccons [|Lazy.force Coq_micromega.M.coq_proofTerm; Coq_micromega.dump_proof_term f; l|]) l (mklApp cnil [|Lazy.force Coq_micromega.M.coq_proofTerm|]) in
+          mklApp cSplArith [|out_c c; out_c orig; res'; l'|]
+	| SplDistinctElim (c',f) -> mklApp cSplDistinctElim [|out_c c;out_c c'; out_f f|]
+	end
+    | _ -> assert false in
+  let step = Lazy.force cstep in
+  let def_step = 
+    mklApp cRes [|mkInt 0; Term.mkArray (Lazy.force cint, [|mkInt 0|]) |] in
+  let r = ref confl in
+  let nc = ref 0 in
+  while not (isRoot !r.kind) do r := prev !r; incr nc done;
+  let last_root = !r in
+  let size = !nc in
+  let max = (Parray.trunc_size (Uint63.of_int 4194303)) - 1 in
+  let q,r1 = size / max, size mod max in
+
+  let trace = 
+    let len = if r1 = 0 then q + 1 else q + 2 in
+    Array.make len (Term.mkArray (step, [|def_step|])) in
+  for j = 0 to q - 1 do
+    let tracej = Array.make (Parray.trunc_size (Uint63.of_int 4194303)) def_step in
+    for i = 0 to max - 1 do
+      r := next !r;
+      tracej.(i) <- step_to_coq !r; 
+    done;
+    trace.(j) <- Term.mkArray (step, tracej)
+  done;
+  if r1 <> 0 then begin
+    let traceq = Array.make (r1 + 1) def_step in
+    for i = 0 to r1-1 do 
+    r := next !r; 
+    traceq.(i) <- step_to_coq !r; 
+    done;
+    trace.(q) <- Term.mkArray (step, traceq)
+  end;
+
+  (Term.mkArray (mklApp carray [|step|], trace), last_root)
+
+
+
+(** Optimization of the trace *)
+
+module MakeOpt (Form:SmtForm.FORM) = 
+  struct 
+    (* Share the certificate building a common clause *)
+    let share_value c =
+      let tbl = Hashtbl.create 17 in
+      let to_lits v = List.map (Form.to_lit) v in
+      let process c = 
+	match c.value with
+	| None -> ()
+	| Some v ->
+	    let lits = to_lits v in
+	    try
+	      let c' = Hashtbl.find tbl lits in
+	      set_same c c'
+	    with Not_found  -> Hashtbl.add tbl lits c in
+      let r = ref c in
+      while !r.next <> None do
+	let next = next !r in
+	process !r;
+	r := next 
+      done;
+      process !r
+
+   (* Sharing of the common prefix *)
+
+    module HashedHeadRes =
+      struct
+
+	type t = Form.t resolution
+
+	let equal r1 r2 =
+	  eq_clause r1.rc1 r2.rc1 && eq_clause r1.rc2 r2.rc2
+
+	let hash r = (repr r.rc1).id * 19 + (repr r.rc2).id
+
+      end
+
+    module HRtbl = Hashtbl.Make (HashedHeadRes)
+
+    let common_head tl1 tl2 =
+      let rec aux rhd tl1 tl2 =
+	match tl1, tl2 with
+	| [], _ -> List.rev rhd, tl1, tl2
+	| _, [] -> List.rev rhd, tl1, tl2
+	| c1::tl1', c2::tl2' ->
+	    if eq_clause c1 c2 then aux (repr c1 :: rhd) tl1' tl2'
+	    else List.rev rhd, tl1, tl2
+      in aux [] tl1 tl2
+	
+    let share_prefix first_c n =
+      let tbl = HRtbl.create (min n Sys.max_array_length) in
+      let rec share c2 =
+	if isRes c2.kind then (
+	  let res2 = get_res c2 "share_prefix1" in
+	  try
+            let c1 = HRtbl.find tbl res2 in
+            let res1 = get_res c1 "share_prefix2" in
+	    (* res1 and res2 have the same head *)
+            let head, tl1, tl2 = common_head res1.rtail res2.rtail in
+            match tl1, tl2 with
+            | [], [] ->
+		set_same c2 c1;
+            | [], c2'::tl2' ->
+		res2.rc1 <- c1;
+		res2.rc2 <- c2';
+		res2.rtail <- tl2';
+		share c2
+            | c1'::tl1', [] ->
+		skip c2;
+		HRtbl.remove tbl res1;
+		insert_before c1 c2;
+		res1.rc1 <- c2;
+		res1.rc2 <- c1';
+		res1.rtail <- tl1';
+		share c1
+            | c1'::tl1', c2'::tl2' ->
+		let c = mkRes res1.rc1 res1.rc2 head in
+		HRtbl.remove tbl res1;
+		insert_before c1 c;
+		res1.rc1 <- c;
+		res1.rc2 <- c1';
+		res1.rtail <- tl1';
+		res2.rc1 <- c;
+		res2.rc2 <- c2';
+		res2.rtail <- tl2';
+		share c;
+		share c1;
+		share c2
+	  with Not_found -> HRtbl.add tbl res2 c2
+	 ) in
+      let r = ref first_c in
+      while !r.next <> None do
+	let n = next !r in
+	share !r;
+	r := n
+      done
+
+  end
diff --git a/src/trace/smt_tactic.ml4 b/src/trace/smt_tactic.ml4
new file mode 100644
index 0000000..219810d
--- /dev/null
+++ b/src/trace/smt_tactic.ml4
@@ -0,0 +1,55 @@
+(**************************************************************************)
+(*                                                                        *)
+(*     SMTCoq                                                             *)
+(*     Copyright (C) 2011 - 2015                                          *)
+(*                                                                        *)
+(*     Michaël Armand                                                     *)
+(*     Benjamin Grégoire                                                  *)
+(*     Chantal Keller                                                     *)
+(*                                                                        *)
+(*     Inria - École Polytechnique - MSR-Inria Joint Lab                  *)
+(*                                                                        *)
+(*   This file is distributed under the terms of the CeCILL-C licence     *)
+(*                                                                        *)
+(**************************************************************************)
+
+
+VERNAC COMMAND EXTEND Parse_certif_zchaff
+| [ "Parse_certif_zchaff" 
+    ident(dimacs) ident(trace) string(fdimacs) string(fproof) ] ->
+  [
+    Zchaff.parse_certif dimacs trace fdimacs fproof
+  ]
+| [ "Zchaff_Checker" string(fdimacs) string(fproof) ] ->
+  [
+    Zchaff.checker fdimacs fproof
+  ]
+| [ "Zchaff_Theorem" ident(name) string(fdimacs) string(fproof) ] ->
+  [
+    Zchaff.theorem name fdimacs fproof
+  ] 
+END
+
+VERNAC COMMAND EXTEND Parse_certif_verit
+| [ "Parse_certif_verit"
+    ident(t_i) ident(t_func) ident(t_atom) ident(t_form) ident(root) ident(used_roots) ident(trace) string(fsmt) string(fproof) ] ->
+  [
+    Verit.parse_certif t_i t_func t_atom t_form root used_roots trace fsmt fproof
+  ]
+| [ "Verit_Checker" string(fsmt) string(fproof) ] ->
+  [
+    Verit.checker fsmt fproof
+  ]
+| [ "Verit_Theorem" ident(name) string(fsmt) string(fproof) ] ->
+  [
+    Verit.theorem name fsmt fproof
+  ]
+END
+
+TACTIC EXTEND zchaff
+| [ "zchaff" ] -> [ Zchaff.tactic ]
+END
+
+TACTIC EXTEND verit
+| [ "verit" ] -> [ Verit.tactic ]
+END