Adding support for lemmas in the command verit

38 files changed, 1107 insertions, 358 deletions

diff --git a/src/SMTCoq.v b/src/SMTCoq.v
index c7588af..a17c840 100644
--- a/src/SMTCoq.v
+++ b/src/SMTCoq.v
@@ -20,3 +20,64 @@ Require Export Conversion_tactics.
 Export Atom Form Sat_Checker Cnf_Checker Euf_Checker.
 
 Declare ML Module "smtcoq_plugin".
+
+Require Import Bool.
+Open Scope Z_scope.
+
+(* verit silently transforms an <implb a b> into a <or (not a) b> when
+ instantiating a quantified theorem with <implb> *)
+Lemma impl_split a b:
+  implb a b = true -> orb (negb a) b = true.
+Proof.
+  intro H.
+  destruct a; destruct b; trivial.
+(* alternatively we could do <now verit_base H.> but it forces us to have veriT
+   installed when we compile SMTCoq. *)
+Qed.
+
+Hint Resolve impl_split.
+
+(* verit silently transforms an <implb (a || b) c> into a <or (not a) c>
+   or into a <or (not b) c> when instantiating such a quantified theorem *)
+Lemma impl_or_split_right a b c:
+  implb (a || b) c -> negb b || c.
+Proof.
+  intro H.
+  destruct a; destruct c; intuition.
+Qed.
+
+Lemma impl_or_split_left a b c:
+  implb (a || b) c -> negb a || c.
+Proof.
+  intro H.
+  destruct a; destruct c; intuition.
+Qed.
+
+(* verit considers equality modulo its symmetry, so we have to recover the
+   right direction in the instances of the theorems *)
+Definition hidden_eq a b := a =? b.
+Ltac all_rew :=
+  repeat match goal with
+         | [ |- context [ ?A =? ?B]] =>
+           change (A =? B) with (hidden_eq A B)
+         end;
+  repeat match goal with
+         | [ |- context [ hidden_eq ?A ?B] ] =>
+           replace (hidden_eq A B) with (B =? A);
+           [ | now rewrite Z.eqb_sym]
+         end.
+
+(* An automatic tactic that takes into account all those transformations *)
+Ltac vauto :=
+  try (let H := fresh "H" in
+       intro H; try (all_rew; apply H);
+       match goal with
+       | [ |- is_true (negb ?A || ?B) ] =>
+         try (eapply impl_or_split_right; apply H);
+         eapply impl_or_split_left; apply H
+       end;
+       apply H);
+  auto.
+
+Ltac verit :=
+  verit_base; vauto.
diff --git a/src/Trace.v b/src/Trace.v
index 5b1be7a..d01ccbe 100644
--- a/src/Trace.v
+++ b/src/Trace.v
@@ -180,9 +180,11 @@ Qed.
  Lemma theorem_checker :
    forall d c,
      checker d c = true ->
-     forall rho, ~ valid (interp_var rho) d.
+     forall rho, negb (valid (interp_var rho) d).
  Proof.
-  intros d c H rho; apply checker_correct with c;trivial.
+  intros d c H rho.
+  apply negb_true_iff. apply neg_eq_true_eq_false.
+  apply checker_correct with c;trivial.
   split;compute;trivial;discriminate.
  Qed.
 
@@ -339,6 +341,8 @@ Inductive step :=
      WARNING: this breaks extraction. *)
   | Hole (pos:int) (prem_id:list clause_id) (prem:list C.t) (concl:C.t)
     (p:interp_conseq_uf (Form.interp_state_var (Atom.interp_form_hatom t_i t_func t_atom) t_form) prem concl)
+  | ForallInst (pos:int) (lemma:Prop) (plemma:lemma) (concl:C.t)
+    (p: lemma -> interp_conseq_uf (Form.interp_state_var (Atom.interp_form_hatom t_i t_func t_atom) t_form) nil concl)
   .
 
   Local Open Scope list_scope.
@@ -365,6 +369,7 @@ Inductive step :=
       | SplArith pos orig res l => S.set_clause s pos (check_spl_arith t_form t_atom (S.get s orig) res l)
       | SplDistinctElim pos orig res => S.set_clause s pos (check_distinct_elim t_form t_atom (S.get s orig) res)
       | @Hole pos prem_id prem concl _ => S.set_clause s pos (check_hole s prem_id prem concl)
+      | @ForallInst pos lemma _ concl  _ => S.set_clause s pos concl
     end.
 
   Lemma step_checker_correct :
@@ -374,7 +379,7 @@ Inductive step :=
       forall s, S.valid rho s ->
         forall st : step, S.valid rho (step_checker s st).
   Proof.
-    intros rho H1 H2 H10 s Hs. destruct (Form.check_form_correct (Atom.interp_form_hatom t_i t_func t_atom) _ H1) as [[Ht1 Ht2] Ht3]. destruct (Atom.check_atom_correct _ H2) as [Ha1 Ha2]. intros [pos res|pos cid lf|pos|pos|pos l|pos l|pos l i|pos cid|pos cid|pos cid i|pos l fl|pos l fl|pos l1 l2 fl|pos cl c|pos l|pos orig res l|pos orig res|pos prem_id prem concl p]; simpl; try apply S.valid_set_clause; auto.
+    intros rho H1 H2 H10 s Hs. destruct (Form.check_form_correct (Atom.interp_form_hatom t_i t_func t_atom) _ H1) as [[Ht1 Ht2] Ht3]. destruct (Atom.check_atom_correct _ H2) as [Ha1 Ha2]. intros [pos res|pos cid lf|pos|pos|pos l|pos l|pos l i|pos cid|pos cid|pos cid i|pos l fl|pos l fl|pos l1 l2 fl|pos cl c|pos l|pos orig res l|pos orig res|pos prem_id prem concl p | pos lemma plemma concl p]; simpl; try apply S.valid_set_clause; auto.
     apply S.valid_set_resolve; auto.
     apply valid_check_flatten; auto; intros h1 h2 H.
     rewrite (Syntactic.check_hatom_correct_bool _ _ _ Ha1 Ha2 _ _ H); auto.
@@ -395,6 +400,7 @@ Inductive step :=
     apply valid_check_spl_arith; auto.
     apply valid_check_distinct_elim; auto.
     apply valid_check_hole; auto.
+    apply valid_check_forall_inst with lemma; auto.
   Qed.
 
   Definition euf_checker (* t_atom t_form *) s t :=
@@ -451,9 +457,12 @@ Inductive step :=
 
   Lemma checker_correct : forall (* t_i t_func t_atom t_form *) d used_roots c,
     checker (* t_i t_func t_atom t_form *) d used_roots c = true ->
-    ~ valid t_func t_atom t_form d.
+    negb (valid t_func t_atom t_form d).
   Proof.
-    unfold checker; intros (* t_i t_func t_atom t_form *) d used_roots (nclauses, t, confl); rewrite !andb_true_iff; intros [[[H1 H2] H10] H3] H; eelim euf_checker_correct; try eassumption; apply add_roots_correct; try eassumption; apply S.valid_make; destruct (Form.check_form_correct (Atom.interp_form_hatom t_i t_func t_atom) _ H1) as [_ H4]; auto.
+    unfold checker; intros (* t_i t_func t_atom t_form *) d used_roots (nclauses, t, confl); rewrite !andb_true_iff.  intros [[[H1 H2] H10] H3].
+    apply Is_true_eq_true. apply negb_prop_intro. intro H.
+    apply Is_true_eq_true in H.
+    eelim euf_checker_correct; try eassumption; apply add_roots_correct; try eassumption; apply S.valid_make; destruct (Form.check_form_correct (Atom.interp_form_hatom t_i t_func t_atom) _ H1) as [_ H4]; auto.
   Qed.
 
   Definition checker_b (* t_i t_func t_atom t_form *) l (b:bool) (c:certif) :=
@@ -465,7 +474,10 @@ Inductive step :=
     checker_b (* t_func t_atom t_form *) l b c = true ->
     Lit.interp (Form.interp_state_var (Atom.interp_form_hatom t_i t_func t_atom) t_form) l = b.
   Proof.
-    unfold checker_b; intros (* t_i t_func t_atom t_form *) l b (nclauses, t, confl); case b; intros H2; case_eq (Lit.interp (Form.interp_state_var (Atom.interp_form_hatom t_i t_func t_atom) t_form) l); auto; intros H1; elim (checker_correct H2); auto; unfold valid; apply afold_left_andb_true; intros i Hi; rewrite get_make; auto; rewrite Lit.interp_neg, H1; auto.
+    unfold checker_b; intros (* t_i t_func t_atom t_form *) l b (nclauses, t, confl); case b; intros H2; case_eq (Lit.interp (Form.interp_state_var (Atom.interp_form_hatom t_i t_func t_atom) t_form) l); auto; intros H1;
+    assert (G:= checker_correct H2);
+    apply negb_true_iff in G; apply neg_eq_true_eq_false in G;
+    elim G; auto; unfold valid; apply afold_left_andb_true; intros i Hi; rewrite get_make; auto; rewrite Lit.interp_neg, H1; auto.
  Qed.
 
   Definition checker_eq (* t_i t_func t_atom t_form *) l1 l2 l (c:certif) :=
@@ -484,7 +496,10 @@ Inductive step :=
   Proof.
    unfold checker_eq; intros (* t_i t_func t_atom t_form *) l1 l2 l (nclauses, t, confl); rewrite !andb_true_iff; case_eq (t_form .[ Lit.blit l]); [intros _ _|intros _|intros _|intros _ _ _|intros _ _|intros _ _|intros _ _|intros _ _ _|intros l1' l2' Heq|intros _ _ _ _]; intros [[H1 H2] H3]; try discriminate; rewrite andb_true_iff in H2; rewrite !Int63Properties.eqb_spec in H2; destruct H2 as [H2 H4]; subst l1' l2'; case_eq (Lit.is_pos l); intro Heq'; rewrite Heq' in H1; try discriminate; clear H1; assert (H:PArray.default t_form = Form.Ftrue /\ Form.wf t_form).
    unfold checker in H3; rewrite !andb_true_iff in H3; destruct H3 as [[[H3 _] _] _]; destruct (Form.check_form_correct (Atom.interp_form_hatom t_i t_func t_atom) _ H3) as [[Ht1 Ht2] Ht3]; split; auto.
-   destruct H as [H1 H2]; case_eq (Lit.interp (Form.interp_state_var (Atom.interp_form_hatom t_i t_func t_atom) t_form) l1); intro Heq1; case_eq (Lit.interp (Form.interp_state_var (Atom.interp_form_hatom t_i t_func t_atom) t_form) l2); intro Heq2; auto; elim (checker_correct H3); unfold valid; apply afold_left_andb_true; intros i Hi; rewrite get_make; unfold Lit.interp; rewrite Heq'; unfold Var.interp; rewrite Form.wf_interp_form; auto; rewrite Heq; simpl; rewrite Heq1, Heq2; auto.
+   destruct H as [H1 H2]; case_eq (Lit.interp (Form.interp_state_var (Atom.interp_form_hatom t_i t_func t_atom) t_form) l1); intro Heq1; case_eq (Lit.interp (Form.interp_state_var (Atom.interp_form_hatom t_i t_func t_atom) t_form) l2); intro Heq2; auto;
+     assert (G:= checker_correct H3);
+    apply negb_true_iff in G; apply neg_eq_true_eq_false in G;
+   elim G; unfold valid; apply afold_left_andb_true; intros i Hi; rewrite get_make; unfold Lit.interp; rewrite Heq'; unfold Var.interp; rewrite Form.wf_interp_form; auto; rewrite Heq; simpl; rewrite Heq1, Heq2; auto.
  Qed.
 
 
diff --git a/src/lia/lia.ml b/src/lia/lia.ml
index 589d59a..e5f2fe9 100644
--- a/src/lia/lia.ml
+++ b/src/lia/lia.ml
@@ -160,6 +160,7 @@ let rec smt_Form_to_coq_micromega_formula tbl l =
           failwith "Lia.smt_Form_to_coq_micromega_formula: wrong number of arguments for Fnot2"
         else
           smt_Form_to_coq_micromega_formula tbl l.(0)
+      | Fapp (Fforall _, _) -> assert false
   in
   if Form.is_pos l then v
   else N(v)
diff --git a/src/smtlib2/smtlib2_genConstr.ml b/src/smtlib2/smtlib2_genConstr.ml
index 27ac8d3..76dde25 100644
--- a/src/smtlib2/smtlib2_genConstr.ml
+++ b/src/smtlib2/smtlib2_genConstr.ml
@@ -93,7 +93,7 @@ let declare_fun rt ro sym arg cod =
   let coqTy = List.fold_right (fun typ c -> Term.mkArrow (interp_to_coq rt (fst typ)) c) tyl (interp_to_coq rt (fst ty)) in
   let cons_v = declare_new_variable (Names.id_of_string ("Smt_var_"^s)) coqTy in
 
-  let op = Op.declare ro cons_v (Array.of_list (List.map fst tyl)) (fst ty) in
+  let op = Op.declare ro cons_v (Array.of_list (List.map fst tyl)) (fst ty) None in
   VeritSyntax.add_fun s op;
   op
 
@@ -147,35 +147,35 @@ let make_root ra rf t =
           | Atom a', Atom b' ->
             (match Atom.type_of a' with
               | Tbool -> Form (Form.get rf (Fapp (Fiff, [|Form.get rf (Fatom a'); Form.get rf (Fatom b')|])))
-              | ty -> Atom (Atom.mk_eq ra ty a' b'))
+              | ty -> Atom (Atom.mk_eq ra true ty a' b'))
           | _, _ -> assert false)
       | "<", [a;b] ->
         (match make_root_term a, make_root_term b with
-          | Atom a', Atom b' -> Atom (Atom.mk_lt ra a' b')
+          | Atom a', Atom b' -> Atom (Atom.mk_lt ra true a' b')
           | _, _ -> assert false)
       | "<=", [a;b] ->
         (match make_root_term a, make_root_term b with
-          | Atom a', Atom b' -> Atom (Atom.mk_le ra a' b')
+          | Atom a', Atom b' -> Atom (Atom.mk_le ra true a' b')
           | _, _ -> assert false)
       | ">", [a;b] ->
         (match make_root_term a, make_root_term b with
-          | Atom a', Atom b' -> Atom (Atom.mk_gt ra a' b')
+          | Atom a', Atom b' -> Atom (Atom.mk_gt ra true a' b')
           | _, _ -> assert false)
       | ">=", [a;b] ->
         (match make_root_term a, make_root_term b with
-          | Atom a', Atom b' -> Atom (Atom.mk_ge ra a' b')
+          | Atom a', Atom b' -> Atom (Atom.mk_ge ra true a' b')
           | _, _ -> assert false)
       | "+", [a;b] ->
         (match make_root_term a, make_root_term b with
-          | Atom a', Atom b' -> Atom (Atom.mk_plus ra a' b')
+          | Atom a', Atom b' -> Atom (Atom.mk_plus ra true a' b')
           | _, _ -> assert false)
       | "-", [a;b] ->
         (match make_root_term a, make_root_term b with
-          | Atom a', Atom b' -> Atom (Atom.mk_minus ra a' b')
+          | Atom a', Atom b' -> Atom (Atom.mk_minus ra true a' b')
           | _, _ -> assert false)
       | "*", [a;b] ->
         (match make_root_term a, make_root_term b with
-          | Atom a', Atom b' -> Atom (Atom.mk_mult ra a' b')
+          | Atom a', Atom b' -> Atom (Atom.mk_mult ra true a' b')
           | _, _ -> assert false)
       | "-", [a] ->
         (match make_root_term a with
diff --git a/src/spl/Assumptions.v b/src/spl/Assumptions.v
index 1f2bb93..b3dee4b 100644
--- a/src/spl/Assumptions.v
+++ b/src/spl/Assumptions.v
@@ -68,7 +68,7 @@ Section Checker.
 
   End Forallb2.
 
-  Definition check_hole (s:S.t) (prem_id:list clause_id) (prem:list C.t) (concl:C.t) :=
+  Definition check_hole (s:S.t) (prem_id:list clause_id) (prem:list C.t) (concl:C.t) : C.t :=
     if forallb2 (fun id c => forallb2 (fun i j => i == j) (S.get s id) (S.sort_uniq c)) prem_id prem
     then concl
     else C._true.
@@ -107,6 +107,18 @@ Section Checker_correct.
     rewrite <- (interp_check_clause _ _ H). now apply Hs.
   Qed.
 
+  Lemma valid_check_forall_inst (lemma : Prop) :
+    lemma ->
+    forall concl,
+    (lemma -> interp_uf rho concl) ->
+    C.valid rho concl.
+
+  Proof.
+    intros pl concl applemma.
+    unfold C.valid. rewrite interp_equiv.
+    now apply applemma.
+  Qed.
+
   Variable prem_id : list int.
   Variable prem : list C.t.
   Variable concl : C.t.
@@ -123,10 +135,7 @@ Section Checker_correct.
     - now apply C.interp_true.
     - case_eq (forallb2 (fun i j => i == j) (S.get s pid) (S.sort_uniq p));
       simpl; intro Heq; [ |now apply C.interp_true].
-      case_eq (forallb2 (fun id c => forallb2 (fun i j => i == j) (S.get s id) (S.sort_uniq c)) pids ps);
-      simpl; intro Heq2; [ |now apply C.interp_true].
-      assert (IH:=IHpids _ (H (valid_check_clause _ _ Heq))).
-      now rewrite Heq2 in IH.
+      apply IHpids. apply H. apply (valid_check_clause _ _ Heq).
   Qed.
 
 End Checker_correct.
diff --git a/src/trace/coqTerms.ml b/src/trace/coqTerms.ml
index 1874d5f..96d5a69 100644
--- a/src/trace/coqTerms.ml
+++ b/src/trace/coqTerms.ml
@@ -90,6 +90,8 @@ let csigT = gen_constant init_modules "sigT"
 let cnot = gen_constant init_modules "not"
 let ceq = gen_constant init_modules "eq"
 let crefl_equal = gen_constant init_modules "eq_refl"
+let cconj = gen_constant init_modules "conj"
+let cand = gen_constant init_modules "and"
 
 (* SMT_terms *)
 
@@ -179,7 +181,7 @@ let make_certif_ops modules args =
   gen_constant"ImmBuildDef2",
   gen_constant "EqTr", gen_constant "EqCgr", gen_constant "EqCgrP", 
   gen_constant "LiaMicromega", gen_constant "LiaDiseq", gen_constant "SplArith", gen_constant "SplDistinctElim",
-  gen_constant "Hole")
+  gen_constant "Hole", gen_constant "ForallInst")
   
 
 (** Useful construction *)
diff --git a/src/trace/coqTerms.mli b/src/trace/coqTerms.mli
index 8fd166e..7d7fe6a 100644
--- a/src/trace/coqTerms.mli
+++ b/src/trace/coqTerms.mli
@@ -45,6 +45,8 @@ val csigT : Term.constr lazy_t
 val cnot : Term.constr lazy_t
 val ceq : Term.constr lazy_t
 val crefl_equal : Term.constr lazy_t
+val cconj : Term.constr lazy_t
+val cand : Term.constr lazy_t
 val smt_modules : string list list
 val cState_C_t : Term.constr lazy_t
 val cdistinct : Term.constr lazy_t
@@ -106,7 +108,7 @@ val make_certif_ops :
   Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
   Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
   Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
-  Term.constr lazy_t
+  Term.constr lazy_t * Term.constr lazy_t 
 val ceq_refl_true : Term.constr lazy_t
 val eq_refl_true : unit -> Term.constr
 val vm_cast_true : Term.constr -> Term.constr
diff --git a/src/trace/satAtom.mli b/src/trace/satAtom.mli
index 5d4201b..4577d42 100644
--- a/src/trace/satAtom.mli
+++ b/src/trace/satAtom.mli
@@ -28,14 +28,15 @@ module Form :
     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
+    val to_string : ?pi:bool -> (hatom -> string) -> t -> string
+    val to_smt : (hatom -> string) -> Format.formatter -> t -> unit
     exception NotWellTyped of pform
     type reify = SmtForm.Make(Atom).reify
     val create : unit -> reify
     val clear : reify -> unit
-    val get : reify -> pform -> t
+    val get : ?declare:bool -> reify -> pform -> t
     val of_coq : (Term.constr -> hatom) -> reify -> Term.constr -> t
+    val hash_hform : (hatom -> hatom) -> reify -> t -> t
     val flatten : reify -> t -> t
     val to_coq : t -> Term.constr
     val pform_tbl : reify -> pform array
diff --git a/src/trace/smtAtom.ml b/src/trace/smtAtom.ml
index ed0402c..7ccaa95 100644
--- a/src/trace/smtAtom.ml
+++ b/src/trace/smtAtom.ml
@@ -49,17 +49,18 @@ type op_def = {
     tres : btype;
     op_val : Term.constr }
 
-type indexed_op = op_def gen_hashed 
+type index = Index of int
+           | Rel_name of string
 
-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 indexed_op = index * op_def
 
-type op = 
-  | Cop of cop
-  | Uop of uop
-  | Bop of bop
-  | Nop of nop
-  | Iop of indexed_op
+let destruct s (i, hval) = match i with
+  | Index index -> index, hval
+  | Rel_name _ -> failwith s
+
+let dummy_indexed_op i dom codom = i, {tparams = dom; tres = codom; op_val = Term.mkProp}
+let indexed_op_index i = let index, _ = destruct "destruct on a Rel: called by indexed_op_index" i in
+                         index
 
 module Op =
   struct
@@ -159,11 +160,12 @@ module Op =
     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_to_coq i = let index, _ = destruct "destruct on a Rel: called by i_to_coq" i in
+                     mkInt index
 
-    let i_type_of i = i.hval.tres
+    let i_type_of (_, hval) = hval.tres
 
-    let i_type_args i = i.hval.tparams
+    let i_type_args (_, hval) = hval.tparams
 
     (* reify table *)
     type reify_tbl =
@@ -175,13 +177,15 @@ module Op =
       { count = 0;
 	tbl =  Hashtbl.create 17 }
 
-    let declare reify op tparams tres =
+    let declare reify op tparams tres os =
       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 opa = { tparams = tparams; tres = tres; op_val = op } in
+      match os with
+      | None ->  let res = Index reify.count, opa in
+                 Hashtbl.add reify.tbl op res;
+                 reify.count <- reify.count + 1;
+                 res
+      | Some name -> Rel_name name, opa
 
     let of_coq reify op =
       Hashtbl.find reify.tbl op
@@ -190,15 +194,16 @@ module 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
+      let set _ op =
+        let index, hval = destruct "destruct on a Rel: called by set in interp_tbl" op in
+        t.(index) <- mk_Tval hval.tparams hval.tres hval.op_val in
       Hashtbl.iter set reify.tbl;
       Structures.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
+        let index, hval = destruct "destruct on a Rel: called by set in to_list" op in
+        (index, hval.tparams, hval.tres, op)::acc in
       Hashtbl.fold set reify.tbl []
 
     let c_equal op1 op2 = op1 == op2
@@ -214,7 +219,7 @@ module Op =
       match op1,op2 with
       | NO_distinct t1, NO_distinct t2 -> SmtBtype.equal t1 t2
 
-    let i_equal op1 op2 = op1.index == op2.index
+    let i_equal (i1, _) (i2, _) = i1 = i2
 
   end
 
@@ -294,13 +299,14 @@ module HashedAtom =
            | _ -> 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 op_index = try fst (destruct "destruct on a Rel: called by hash" op) with _ -> 0 in
          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
+         (hash_args lsl 5 + op_index lsl 3) lxor 4
 
   end
 
@@ -343,33 +349,44 @@ module Atom =
 
     and compute_hint h = compute_int (atom h)
 
-    let to_smt_int fmt i =
+    let to_string_int 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 =
+      s1 ^ string_of_int j ^ s2
+
+    let to_string ?pi:(pi=false) h =
+      let rec to_string h = 
+        (if pi then string_of_int (index h) ^":" else "")
+        ^ to_string_atom (atom h)
+
+      and to_string_atom = function
+        | Acop _ as a -> to_string_int (compute_int a)
+        | Auop (UO_Zopp,h) -> 
+           "(- " ^
+             to_string h ^
+               ")"
+        | Auop _ as a -> to_string_int (compute_int a)
+        | Abop (op,h1,h2) -> to_string_bop op h1 h2
+        | Anop (op,a) -> to_string_nop op a
+        | Aapp ((i, op), a) ->
+           let op_string = begin match i with
+                           | Index index -> "op_" ^ string_of_int index
+                           | Rel_name name -> name end
+                           ^ if pi then to_string_op op else "" in
+           if Array.length a = 0 then (
+             op_string
+           ) else (
+             "(" ^ op_string ^
+               Array.fold_left (fun acc h -> acc ^ " " ^ to_string h) "" a ^
+                 ")"
+           )
+      and to_string_op {tparams=bta; tres=bt; op_val=t} =
+        "[(" ^ Array.fold_left (fun acc bt -> acc ^ SmtBtype.to_string bt ^ " ")
+                 " " bta ^ ") ( " ^ SmtBtype.to_string bt ^ " ) ( " ^
+          Pp.string_of_ppcmds (Printer.pr_constr t) ^ " )]"
+
+      and to_string_bop op h1 h2 =
         let s = match op with
           | BO_Zplus -> "+"
           | BO_Zminus -> "-"
@@ -379,19 +396,21 @@ module Atom =
           | 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 ")"
+        "(" ^ s ^ " " ^
+          to_string h1 ^
+            " " ^
+              to_string h2 ^
+                ")"
 
-      and to_smt_nop fmt op a =
+      and to_string_nop 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 ")"
+        "(" ^ s ^
+          Array.fold_left (fun acc h -> acc ^ " " ^ to_string h) "" a ^
+            ")" in
+      to_string h
 
+    let to_smt fmt t = Format.fprintf fmt "%s@." (to_string t)
 
 
     exception NotWellTyped of atom
@@ -436,9 +455,58 @@ module Atom =
       reify.count <- reify.count + 1;
       res
 
-    let get reify a =
-      try HashAtom.find reify.tbl a
-      with Not_found -> declare reify a
+    let get ?declare:(decl=true) reify a =
+      if decl
+      then try HashAtom.find reify.tbl a
+           with Not_found -> declare reify a
+      else {index = -1; hval = a}
+
+    let mk_eq reify decl 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 ->
+          get ~declare:decl reify (Abop (op, h1, h2))
+
+    let mk_neg reify ({index = i; hval = a} as ha) =
+      try HashAtom.find reify.tbl (Auop (UO_Zopp, ha))
+      with Not_found -> 
+        let na = match a with
+          | Auop (UO_Zpos, x) -> Auop (UO_Zneg, x)
+          | Auop (UO_Zneg, x) -> Auop (UO_Zpos, x)
+          | _ -> failwith "opp not on Z" in
+        get reify na
+
+    let rec hash_hatom ra' {index = _; hval = a} =
+      match a with 
+      | Acop cop -> get ra' a
+      | Auop (uop, ha) -> get ra' (Auop (uop, hash_hatom ra' ha))
+      | Abop (bop, ha1, ha2) ->
+         let new_ha1 = hash_hatom ra' ha1 in
+         let new_ha2 = hash_hatom ra' ha2 in
+         begin match bop with
+         | BO_eq ty -> mk_eq ra' true ty new_ha1 new_ha2
+         | _ -> get ra' (Abop (bop, new_ha1, new_ha2)) end
+      | Anop _ -> assert false
+      | Aapp (op, arr) -> get ra' (Aapp (op, Array.map (hash_hatom ra') arr))
+              
+    let copy {count=c; tbl=t} = {count = c; tbl = HashAtom.copy t}
+             
+    let print_atoms reify where =
+      let oc = open_out where in
+      let fmt = Format.formatter_of_out_channel oc in
+      let accumulate _ ha acc = ha :: acc in
+      let list = HashAtom.fold accumulate reify.tbl [] in
+      let compare ha1 ha2 = compare ha1.index ha2.index in
+      let slist = List.sort compare list in
+      let print ha = Format.fprintf fmt "%i: " ha.index;
+                     to_smt fmt ha; Format.fprintf fmt "\n" in
+      List.iter print slist;
+      Format.fprintf fmt "@.";
+      close_out oc
 
 
     (** Given a coq term, build the corresponding atom *)
@@ -476,11 +544,10 @@ module Atom =
 
     let op_tbl = lazy (op_tbl ())
 
-    let of_coq rt ro reify env sigma c =
+    let of_coq ?hash:(h=false) 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
@@ -498,21 +565,32 @@ module Atom =
         | 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)
+        | CCeqb -> mk_teq Tbool args
+        | CCeqbP -> mk_teq Tpositive args
+        | CCeqbZ -> mk_teq TZ args
+	| CCunknown -> let ty = Retyping.get_type_of env sigma h in
+                       mk_unknown c args ty
+
+      and mk_cop op = get reify (Acop op)
 
       and mk_uop op = function
         | [a] -> let h = mk_hatom a in get reify (Auop (op,h))
-        | _ -> assert false
+        | _ -> failwith "unexpected number of arguments for mk_uop"
+
+      and mk_teq ty args = 
+        if h then match args with    
+        | [a1; a2] -> let h1 = mk_hatom a1 in
+                      let h2 = mk_hatom a2 in
+                      mk_eq reify true ty h1 h2
+        | _ -> failwith "unexpected number of arguments for mk_teq"
+        else mk_bop (BO_eq ty) args
 
       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
+        | _ -> failwith "unexpected number of arguments for mk_bop"
 
       and mk_unknown c args ty =
         let hargs = Array.of_list (List.map mk_hatom args) in
@@ -520,7 +598,12 @@ module Atom =
                  with Not_found ->
                    let targs = Array.map type_of hargs in
                    let tres = SmtBtype.of_coq rt ty in
-                   Op.declare ro c targs tres in
+                   let os = if Term.isRel c
+                            then let i = Term.destRel c in
+                                 let n, _ = Structures.destruct_rel_decl (Environ.lookup_rel i env) in
+                                 Some (string_of_name n)
+                            else None in
+                   Op.declare ro c targs tres os in
         get reify (Aapp (op,hargs)) in
 
       mk_hatom c
@@ -572,7 +655,7 @@ module Atom =
                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
+            | Aapp ((_, hval),t) -> Term.mkApp (hval.op_val, Array.map interp_atom t) in
 	  Hashtbl.add atom_tbl l pc;
 	  pc in
       interp_atom a
@@ -580,11 +663,11 @@ module Atom =
 
     (* Generation of atoms *)
 
-    let mk_nop op reify a = get reify (Anop (op,a))
+    let mk_nop op reify ?declare:(decl=true) a = get ~declare:decl reify (Anop (op,a))
 
-    let mk_binop op reify h1 h2 = get reify (Abop (op, h1, h2))
+    let mk_binop op reify decl h1 h2 = get ~declare:decl reify (Abop (op, h1, h2))
 
-    let mk_unop op reify h = get reify (Auop (op, h))
+    let mk_unop op reify ?declare:(decl=true) h = get ~declare:decl reify (Auop (op, h))
 
     let rec hatom_pos_of_int reify i =
       if i <= 1 then
@@ -621,17 +704,7 @@ module Atom =
         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_unop op reify ?declare:(decl=true) h = get ~declare:decl reify (Auop (op, h))
 
     let mk_lt = mk_binop BO_Zlt
     let mk_le = mk_binop BO_Zle
diff --git a/src/trace/smtAtom.mli b/src/trace/smtAtom.mli
index 8e69265..47734fb 100644
--- a/src/trace/smtAtom.mli
+++ b/src/trace/smtAtom.mli
@@ -43,7 +43,10 @@ type nop =
 
 type indexed_op
 
-val dummy_indexed_op: int -> btype array -> btype -> indexed_op
+type index = Index of int
+           | Rel_name of string
+
+val dummy_indexed_op: index -> btype array -> btype -> indexed_op
 val indexed_op_index : indexed_op -> int
 
 module Op :
@@ -53,7 +56,8 @@ module Op :
 
     val create : unit -> reify_tbl
 
-    val declare : reify_tbl -> Term.constr -> btype array -> btype -> indexed_op
+    val declare : reify_tbl -> Term.constr -> btype array ->
+                  btype -> string option -> indexed_op
 
     val of_coq : reify_tbl -> Term.constr -> indexed_op
 
@@ -92,6 +96,8 @@ module Atom :
  
       val type_of : hatom -> btype
 
+      val to_string : ?pi:bool -> hatom -> string
+                               
       val to_smt : Format.formatter -> t -> unit
 
       exception NotWellTyped of atom
@@ -102,10 +108,22 @@ module Atom :
 
       val clear : reify_tbl -> unit
 
-      val get : reify_tbl -> atom -> hatom
+      val get : ?declare:bool -> reify_tbl -> atom -> hatom
+
+      val mk_eq : reify_tbl -> bool -> btype -> hatom -> hatom -> hatom
+
+      val mk_neg : reify_tbl -> hatom -> hatom
+                                                                    
+      val hash_hatom : reify_tbl -> hatom -> hatom
+
+      (** for debugging purposes **)
 
+      val copy : reify_tbl -> reify_tbl
+                                                        
+      val print_atoms : reify_tbl -> string -> unit
+                                       
       (** Given a coq term, build the corresponding atom *)
-      val of_coq : SmtBtype.reify_tbl -> Op.reify_tbl ->
+      val of_coq : ?hash:bool -> SmtBtype.reify_tbl -> Op.reify_tbl ->
         reify_tbl -> Environ.env -> Evd.evar_map -> Term.constr -> t
 
       val to_coq : hatom -> Term.constr
@@ -121,16 +139,15 @@ module Atom :
       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
+      val mk_lt : reify_tbl -> bool -> hatom -> hatom -> hatom
+      val mk_le : reify_tbl -> bool -> hatom -> hatom -> hatom
+      val mk_gt : reify_tbl -> bool -> hatom -> hatom -> hatom
+      val mk_ge : reify_tbl -> bool -> hatom -> hatom -> hatom
+      val mk_plus : reify_tbl -> bool -> hatom -> hatom -> hatom
+      val mk_minus : reify_tbl -> bool -> hatom -> hatom -> hatom
+      val mk_mult : reify_tbl -> bool -> hatom -> hatom -> hatom
+      val mk_opp : reify_tbl -> ?declare:bool -> hatom -> hatom
+      val mk_distinct : reify_tbl -> btype -> ?declare:bool -> hatom array -> hatom
 
     end
 
diff --git a/src/trace/smtBtype.ml b/src/trace/smtBtype.ml
index 92b8ad7..f3245ea 100644
--- a/src/trace/smtBtype.ml
+++ b/src/trace/smtBtype.ml
@@ -18,13 +18,15 @@ type btype =
 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 indexed_type_of_int i =
+  {index = i; hval = index_to_coq i }
+      
 let equal t1 t2 =
   match t1,t2 with
   | Tindex i, Tindex j -> i.index == j.index
@@ -34,13 +36,15 @@ let to_coq = function
   | TZ -> Lazy.force cTZ
   | Tbool -> Lazy.force cTbool
   | Tpositive -> Lazy.force cTpositive
-  | Tindex i -> index_to_coq i
+  | Tindex i -> index_to_coq i.index
 
-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
+let to_string = function
+  | TZ -> "Int"
+  | Tbool -> "Bool"
+  | Tpositive -> "Int"
+  | Tindex i -> "Tindex_" ^ string_of_int i.index
+
+let to_smt fmt b = Format.fprintf fmt "%s" (to_string b)
 
 (* reify table *)
 type reify_tbl =
diff --git a/src/trace/smtBtype.mli b/src/trace/smtBtype.mli
index 11d596f..29e91bf 100644
--- a/src/trace/smtBtype.mli
+++ b/src/trace/smtBtype.mli
@@ -3,14 +3,16 @@ val dummy_indexed_type : int -> indexed_type
 val indexed_type_index : indexed_type -> int
 val indexed_type_hval : indexed_type -> Term.constr
 type btype = TZ | Tbool | Tpositive | Tindex of indexed_type
+val indexed_type_of_int : int -> indexed_type
 val equal : btype -> btype -> bool
 val to_coq : btype -> Term.constr
+val to_string : btype -> string
 val to_smt : Format.formatter -> btype -> unit
 type reify_tbl
 val create : unit -> reify_tbl
+val get_cuts : reify_tbl -> (Structures.names_id_t * Term.types) list
 val declare : reify_tbl -> Term.constr -> Term.constr -> btype
-val of_coq : reify_tbl -> Term.constr -> btype
+val of_coq : reify_tbl -> Term.types -> 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
-val get_cuts : reify_tbl -> (Structures.names_id_t * Term.types) list
+val interp_to_coq : 'a -> btype -> Term.constr
diff --git a/src/trace/smtCertif.ml b/src/trace/smtCertif.ml
index a0972d4..a0af59d 100644
--- a/src/trace/smtCertif.ml
+++ b/src/trace/smtCertif.ml
@@ -110,15 +110,17 @@ type 'hform rule =
 
   (* Possibility to introduce "holes" in proofs (that should be filled in Coq) *)
   | Hole of ('hform clause) list * 'hform list
+  | Forall_inst of 'hform clause * 'hform
+  | Qf_lemma of 'hform clause * 'hform
 
 and 'hform clause = {
-            id    : clause_id;
+    mutable 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
+    mutable value : 'hform list option
               (* This field should be defined for rules which can create atoms :
                  EqTr, EqCgr, EqCgrP, Lia, Dlde, Lra *)
 }
@@ -137,8 +139,45 @@ and 'hform resolution = {
 let used_clauses r =
   match r with
   | ImmBuildProj (c, _) | ImmBuildDef c | ImmBuildDef2 c
-  | ImmFlatten (c,_)  | SplArith (c,_,_) | SplDistinctElim (c,_) -> [c]
+  | ImmFlatten (c,_)  | SplArith (c,_,_) | SplDistinctElim (c,_)
+  | Forall_inst (c, _) | Qf_lemma (c, _) -> [c]
   | Hole (cs, _) -> cs
   | True | False | BuildDef _ | BuildDef2 _ | BuildProj _
   | EqTr _ | EqCgr _ | EqCgrP _
   | LiaMicromega _ | LiaDiseq _ -> []
+
+(* for debugging *)                                       
+let to_string r =
+  match r with
+            Root -> "Root"
+          | Same c -> "Same(" ^ string_of_int (c.id) ^ ")"
+          | Res r ->
+             let id1 = string_of_int r.rc1.id in
+             let id2 = string_of_int r.rc2.id in
+             let rest_ids = List.fold_left (fun str rc -> str ^ "; " ^ string_of_int rc.id) "" r.rtail in
+             "Res [" ^ id1 ^ "; " ^ id2 ^ rest_ids ^"]"
+          | Other x -> "Other(" ^
+                         begin match x with
+                         | True -> "True"
+                         | False -> "False"
+                         | BuildDef _ -> "BuildDef"
+                         | BuildDef2 _ -> "BuildDef2"
+                         | BuildProj _ -> "BuildProj"
+                         | EqTr _ -> "EqTr"
+                         | EqCgr _ -> "EqCgr"
+                         | EqCgrP _ -> "EqCgrP"
+                         | LiaMicromega _ -> "LiaMicromega"
+                         | LiaDiseq _ -> "LiaDiseq"
+                         | Qf_lemma _ -> "Qf_lemma"
+                                         
+                         | Hole _ -> "Hole"
+
+                         | ImmFlatten _ -> "ImmFlatten"
+                         | ImmBuildDef _ -> "ImmBuildDef"
+                         | ImmBuildDef2 _ -> "ImmBuildDef2"
+                         | ImmBuildProj _ -> "ImmBuildProj"
+                         | SplArith _ -> "SplArith"
+                         | SplDistinctElim _ -> "SplDistinctElim"
+                         | Forall_inst _ -> "Forall_inst"  end ^ ")"
+
+
diff --git a/src/trace/smtCertif.mli b/src/trace/smtCertif.mli
index 767dc8b..942262c 100644
--- a/src/trace/smtCertif.mli
+++ b/src/trace/smtCertif.mli
@@ -20,15 +20,17 @@ type 'hform rule =
       Structures.Micromega_plugin_Certificate.Mc.zArithProof list
   | SplDistinctElim of 'hform clause * 'hform
   | Hole of 'hform clause list * 'hform list
+  | Forall_inst of 'hform clause * 'hform
+  | Qf_lemma of 'hform clause * 'hform
 
 and 'hform clause = {
-            id    : clause_id;
+    mutable 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;
+    mutable value : 'hform list option;
 }
 and 'hform clause_kind =
     Root
@@ -41,3 +43,4 @@ and 'hform resolution = {
   mutable rtail : 'hform clause list;
 }
 val used_clauses : 'a rule -> 'a clause list
+val to_string : 'a clause_kind -> string
diff --git a/src/trace/smtCnf.ml b/src/trace/smtCnf.ml
index bf3d0d1..62a040d 100644
--- a/src/trace/smtCnf.ml
+++ b/src/trace/smtCnf.ml
@@ -149,7 +149,8 @@ module MakeCnf (Form:FORM) =
 		  cnf c
 
 	      | Fnot2 _ -> cnf args.(0)
- 
+              | Fforall _ -> assert false
+
     exception Cnf_done
 
     let rec imm_link_Other other l =
@@ -245,6 +246,7 @@ module MakeCnf (Form:FORM) =
 		  push_cnf args
 
               | Fnot2 _ -> assert false
+              | Fforall _ -> assert false
 
     let make_cnf reify c =
       let ftrue = Form.get reify (Fapp(Ftrue, [||])) in
diff --git a/src/trace/smtCommands.ml b/src/trace/smtCommands.ml
index ba86a5b..27b8210 100644
--- a/src/trace/smtCommands.ml
+++ b/src/trace/smtCommands.ml
@@ -38,6 +38,7 @@ let cchecker_b = gen_constant euf_checker_modules "checker_b"
 let cchecker_eq_correct =
   gen_constant euf_checker_modules "checker_eq_correct"
 let cchecker_eq = gen_constant euf_checker_modules "checker_eq"
+let cZeqbsym = gen_constant z_modules "eqb_sym"
 
 (* Given an SMT-LIB2 file and a certif, build the corresponding objects *)
 
@@ -105,7 +106,8 @@ let parse_certif t_i t_func t_atom t_form root used_root trace (rt, ro, ra, rf,
   let ce2 = Structures.mkUConst t_form' in
   let ct_form = Term.mkConst (declare_constant t_form (DefinitionEntry ce2, IsDefinition Definition)) in
 
-  let (tres, last_root, cuts) = SmtTrace.to_coq (fun i -> mkInt (Form.to_lit i)) interp_conseq_uf (certif_ops (Some [|ct_i; ct_func; ct_atom; ct_form|])) confl in
+  (* EMPTY LEMMA LIST *)
+  let (tres, last_root, cuts) = SmtTrace.to_coq (fun i -> mkInt (Form.to_lit i)) interp_conseq_uf (certif_ops (Some [|ct_i; ct_func; ct_atom; ct_form|])) confl None in
   List.iter (fun (v,ty) ->
     let _ = Structures.declare_new_variable v ty in
     print_assm ty
@@ -160,7 +162,8 @@ let theorem name (rt, ro, ra, rf, roots, max_id, confl) =
   let t_atom = Atom.interp_tbl ra in
   let t_form = snd (Form.interp_tbl rf) in
 
-  let (tres,last_root,cuts) = SmtTrace.to_coq (fun i -> mkInt (Form.to_lit i)) interp_conseq_uf (certif_ops (Some [|v 4(*t_i*); v 3(*t_func*); v 2(*t_atom*); v 1(* t_form *)|])) confl in
+  (* EMPTY LEMMA LIST *)
+  let (tres,last_root,cuts) = SmtTrace.to_coq (fun i -> mkInt (Form.to_lit i)) interp_conseq_uf (certif_ops (Some [|v 4(*t_i*); v 3(*t_func*); v 2(*t_atom*); v 1(* t_form *)|])) confl None in
   List.iter (fun (v,ty) ->
     let _ = Structures.declare_new_variable v ty in
     print_assm ty
@@ -182,7 +185,7 @@ let theorem name (rt, ro, ra, rf, roots, max_id, confl) =
     List.iter (fun j -> res.(!i) <- mkInt (Form.to_lit j); incr i) roots;
     Structures.mkArray (Lazy.force cint, res) in
 
-  let theorem_concl = mklApp cnot [|mklApp cis_true [|interp_roots roots|]|] in
+  let theorem_concl = mklApp cis_true [|mklApp cnegb [|interp_roots roots|]|] in
   let theorem_proof_cast =
     Term.mkCast (
         Term.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_eqb|],
@@ -234,7 +237,8 @@ let checker (rt, ro, ra, rf, roots, max_id, confl) =
   let t_atom = Atom.interp_tbl ra in
   let t_form = snd (Form.interp_tbl rf) in
 
-  let (tres,last_root,cuts) = SmtTrace.to_coq (fun i -> mkInt (Form.to_lit i)) interp_conseq_uf (certif_ops (Some [|v 4(*t_i*); v 3(*t_func*); v 2(*t_atom*); v 1(* t_form *)|])) confl in
+  (* EMPTY LEMMA LIST *)
+  let (tres,last_root,cuts) = SmtTrace.to_coq (fun i -> mkInt (Form.to_lit i)) interp_conseq_uf (certif_ops (Some [|v 4(*t_i*); v 3(*t_func*); v 2(*t_atom*); v 1(* t_form *)|])) confl None in
   List.iter (fun (v,ty) ->
     let _ = Structures.declare_new_variable v ty in
     print_assm ty
@@ -274,7 +278,7 @@ let checker (rt, ro, ra, rf, roots, max_id, confl) =
 
 (* Tactic *)
 
-let build_body rt ro ra rf l b (max_id, confl) =
+let build_body rt ro ra rf l b (max_id, confl) find =
   let nti = mkName "t_i" in
   let ntfunc = mkName "t_func" in
   let ntatom = mkName "t_atom" in
@@ -287,7 +291,7 @@ let build_body rt ro ra rf l b (max_id, confl) =
   let t_func = Structures.lift 1 (make_t_func ro (v 0 (*t_i - 1*))) in
   let t_atom = Atom.interp_tbl ra in
   let t_form = snd (Form.interp_tbl rf) in
-  let (tres,_,cuts) = SmtTrace.to_coq Form.to_coq interp_conseq_uf (certif_ops (Some [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|])) confl in
+  let (tres,_,cuts) = SmtTrace.to_coq Form.to_coq interp_conseq_uf (certif_ops (Some [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|])) confl find in
   let certif =
     mklApp cCertif [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*); mkInt (max_id + 1); tres;mkInt (get_pos confl)|] in
 
@@ -314,7 +318,7 @@ let build_body rt ro ra rf l b (max_id, confl) =
   (proof_cast, proof_nocast, cuts)
 
 
-let build_body_eq rt ro ra rf l1 l2 l (max_id, confl) =
+let build_body_eq rt ro ra rf l1 l2 l (max_id, confl) find =
   let nti = mkName "t_i" in
   let ntfunc = mkName "t_func" in
   let ntatom = mkName "t_atom" in
@@ -327,7 +331,7 @@ let build_body_eq rt ro ra rf l1 l2 l (max_id, confl) =
   let t_func = Structures.lift 1 (make_t_func ro (v 0 (*t_i*))) in
   let t_atom = Atom.interp_tbl ra in
   let t_form = snd (Form.interp_tbl rf) in
-  let (tres,_,cuts) = SmtTrace.to_coq Form.to_coq interp_conseq_uf (certif_ops (Some [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|])) confl in
+  let (tres,_,cuts) = SmtTrace.to_coq Form.to_coq interp_conseq_uf (certif_ops (Some [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|])) confl find in
   let certif =
     mklApp cCertif [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*); mkInt (max_id + 1); tres;mkInt (get_pos confl)|] in
 
@@ -362,26 +366,89 @@ let get_arguments concl =
   | _ -> failwith ("Verit.tactic: can only deal with equality over bool")
 
 
-let make_proof call_solver rt ro rf l =
-  let fl = Form.flatten rf l in
-  let root = SmtTrace.mkRootV [l] in
-  call_solver rt ro fl (root,l)
-
-
-let core_tactic call_solver rt ro ra rf env sigma concl =
+let make_proof call_solver rt ro rf ra' rf' l' ls_smtc=
+  let fl' = Form.flatten rf' l' in
+  let root = SmtTrace.mkRootV [l'] in
+  call_solver rt ro ra' rf' (Some (root, l')) (fl'::ls_smtc)
+
+(* <of_coq_lemma> reifies the coq lemma given, we can then easily print it in a
+ .smt2 file. We need the reify tables to correctly recognize unbound variables
+ of the lemma. We also need to make sure to leave unchanged the tables because
+ the new objects may contain bound (by forall of the lemma) variables. *)
+exception Axiom_form_unsupported
+              
+let of_coq_lemma rt ro ra' rf' env sigma clemma =
+  let rel_context, qf_lemma = Term.decompose_prod_assum clemma in
+  let env_lemma = List.fold_right Environ.push_rel rel_context env in
+  let forall_args =
+    let fmap r = let n, t = Structures.destruct_rel_decl r in
+                 string_of_name n, SmtBtype.of_coq rt t in
+    List.map fmap rel_context in
+  let f, args = Term.decompose_app qf_lemma in
+  let core_f =
+    if Term.eq_constr f (Lazy.force cis_true) then
+      match args with
+      | [a] -> a
+      | _ -> raise Axiom_form_unsupported
+    else if Term.eq_constr f (Lazy.force ceq) then
+      match args with
+      | [ty; arg1; arg2] when Term.eq_constr ty (Lazy.force cbool) &&
+                                Term.eq_constr arg2 (Lazy.force ctrue) ->
+         arg1
+      | _ -> raise Axiom_form_unsupported
+    else raise Axiom_form_unsupported in
+  let core_smt = Form.of_coq (Atom.of_coq ~hash:true rt ro ra' env_lemma sigma)
+                   rf' core_f in
+  match forall_args with
+    [] -> core_smt
+  | _ -> Form.get rf' (Fapp (Fforall forall_args, [|core_smt|]))
+
+let core_tactic call_solver rt ro ra rf ra' rf' lcpl lcepl env sigma concl =
   let a, b = get_arguments concl in
+  let tlcepl = List.map (Structures.interp_constr env sigma) lcepl in
+  let lcpl = lcpl @ tlcepl in
+  let lcl = List.map (Retyping.get_type_of env sigma) lcpl in
+
+  let lsmt  = List.map (of_coq_lemma rt ro ra' rf' env sigma) lcl in
+  let l_pl_ls = List.combine (List.combine lcl lcpl) lsmt in
+
+  let lem_tbl : (int, Term.constr * Term.constr) Hashtbl.t =
+    Hashtbl.create 100 in
+  let new_ref ((l, pl), ls) =
+    Hashtbl.add lem_tbl (Form.index ls) (l, pl) in
+
+  List.iter new_ref l_pl_ls;
+  
+  let find_lemma cl =
+    let re_hash hf = Form.hash_hform (Atom.hash_hatom ra') rf' hf in
+    match cl.value with
+    | Some [l] ->
+       let hl = re_hash l in
+       begin try Hashtbl.find lem_tbl (Form.index hl)
+             with Not_found ->
+               let oc = open_out "/tmp/find_lemma.log" in
+               List.iter (fun u -> Printf.fprintf oc "%s\n"
+                                     (VeritSyntax.string_hform u)) lsmt;
+               Printf.fprintf oc "\n%s\n" (VeritSyntax.string_hform hl);
+               flush oc; close_out oc; failwith "find_lemma" end
+      | _ -> failwith "unexpected form of root" in
+  
   let (body_cast, body_nocast, cuts) =
     if ((Term.eq_constr b (Lazy.force ctrue)) || (Term.eq_constr b (Lazy.force cfalse))) then
       let l = Form.of_coq (Atom.of_coq rt ro ra env sigma) rf a in
-      let l' = if (Term.eq_constr b (Lazy.force ctrue)) then Form.neg l else l in
-      let max_id_confl = make_proof call_solver rt ro rf l' in
-      build_body rt ro ra rf (Form.to_coq l) b max_id_confl
+      let l' = Form.of_coq (Atom.of_coq ~hash:true rt ro ra' env sigma) rf' a in
+      let l' = if (Term.eq_constr b (Lazy.force ctrue)) then Form.neg l' else l' in
+      let max_id_confl = make_proof call_solver rt ro rf ra' rf' l' lsmt in
+      build_body rt ro ra rf (Form.to_coq l) b max_id_confl (Some find_lemma)
     else
       let l1 = Form.of_coq (Atom.of_coq rt ro ra env sigma) rf a in
       let l2 = Form.of_coq (Atom.of_coq rt ro ra env sigma) rf b in
       let l = Form.neg (Form.get rf (Fapp(Fiff,[|l1;l2|]))) in
-      let max_id_confl = make_proof call_solver rt ro rf l in
-      build_body_eq rt ro ra rf (Form.to_coq l1) (Form.to_coq l2) (Form.to_coq l) max_id_confl in
+      let l1' = Form.of_coq (Atom.of_coq ~hash:true rt ro ra' env sigma) rf' a in
+      let l2' = Form.of_coq (Atom.of_coq ~hash:true rt ro ra' env sigma) rf' b in
+      let l' = Form.neg (Form.get rf' (Fapp(Fiff,[|l1';l2'|]))) in
+      let max_id_confl = make_proof call_solver rt ro rf ra' rf' l' lsmt in
+      build_body_eq rt ro ra rf (Form.to_coq l1) (Form.to_coq l2) (Form.to_coq l) max_id_confl (Some find_lemma) in
 
   let cuts = SmtBtype.get_cuts rt @ cuts in
 
@@ -392,7 +459,7 @@ let core_tactic call_solver rt ro ra rf env sigma concl =
        (Structures.set_evars_tac body_nocast)
        (Structures.vm_cast_no_check body_cast))
 
-let tactic call_solver rt ro ra rf =
+let tactic call_solver rt ro ra rf ra' rf' lcpl lcepl =
   Structures.tclTHEN
     Tactics.intros
-    (Structures.mk_tactic (core_tactic call_solver rt ro ra rf))
+    (Structures.mk_tactic (core_tactic call_solver rt ro ra rf ra' rf' lcpl lcepl))
diff --git a/src/trace/smtCommands.mli b/src/trace/smtCommands.mli
index 3cac245..6248270 100644
--- a/src/trace/smtCommands.mli
+++ b/src/trace/smtCommands.mli
@@ -7,7 +7,7 @@ val certif_ops :
   Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
   Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
   Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
-  Term.constr lazy_t
+  Term.constr lazy_t * Term.constr lazy_t
 val cCertif : Term.constr lazy_t
 val ccertif : Term.constr lazy_t
 val cchecker : Term.constr lazy_t
@@ -53,6 +53,7 @@ val build_body :
   Term.constr ->
   Term.constr ->
   int * SmtAtom.Form.t SmtCertif.clause ->
+  (SmtAtom.Form.t SmtCertif.clause  -> Term.constr * Term.constr) option ->
   Term.constr * Term.constr * (Names.identifier * Term.types) list
 val build_body_eq :
   SmtBtype.reify_tbl ->
@@ -63,30 +64,35 @@ val build_body_eq :
   Term.constr ->
   Term.constr ->
   int * SmtAtom.Form.t SmtCertif.clause ->
+  (SmtAtom.Form.t SmtCertif.clause  -> Term.constr * Term.constr) option ->
   Term.constr * Term.constr * (Names.identifier * Term.types) list
 val get_arguments : Term.constr -> Term.constr * Term.constr
 val make_proof :
-  ('a ->
-   'b ->
-   SmtAtom.Form.t -> SmtAtom.Form.t SmtCertif.clause * SmtAtom.Form.t -> 'c) ->
-  'a -> 'b -> SmtAtom.Form.reify -> SmtAtom.Form.t -> 'c
-val core_tactic :
-  (SmtBtype.reify_tbl ->
-   SmtAtom.Op.reify_tbl ->
-   SmtAtom.Form.t ->
-   SmtAtom.Form.t SmtCertif.clause * SmtAtom.Form.t ->
-   int * SmtAtom.Form.t SmtCertif.clause) ->
-  SmtBtype.reify_tbl ->
-  SmtAtom.Op.reify_tbl ->
-  SmtAtom.Atom.reify_tbl ->
+  (SmtBtype.reify_tbl -> SmtAtom.Op.reify_tbl ->
+   SmtAtom.Atom.reify_tbl -> SmtAtom.Form.reify ->
+   (SmtAtom.Form.t SmtCertif.clause * SmtAtom.Form.t) option ->
+   SmtAtom.Form.t list -> int * SmtAtom.Form.t SmtCertif.clause) ->
+  SmtBtype.reify_tbl -> SmtAtom.Op.reify_tbl ->
   SmtAtom.Form.reify ->
+  SmtAtom.Atom.reify_tbl -> SmtAtom.Form.reify ->
+  SmtAtom.Form.t -> SmtAtom.Form.t list -> int * SmtAtom.Form.t SmtCertif.clause
+val core_tactic :
+  (SmtBtype.reify_tbl -> SmtAtom.Op.reify_tbl ->
+   SmtAtom.Atom.reify_tbl -> SmtAtom.Form.reify ->
+   (SmtAtom.Form.t SmtCertif.clause * SmtAtom.Form.t) option ->
+   SmtAtom.Form.t list -> int * SmtAtom.Form.t SmtCertif.clause) ->
+  SmtBtype.reify_tbl -> SmtAtom.Op.reify_tbl ->
+  SmtAtom.Atom.reify_tbl -> SmtAtom.Form.reify ->
+  SmtAtom.Atom.reify_tbl -> SmtAtom.Form.reify ->
+  Term.constr list -> Structures.constr_expr list -> 
   Environ.env -> Evd.evar_map -> Term.constr -> Structures.tactic
 val tactic :
-  (SmtBtype.reify_tbl ->
-   SmtAtom.Op.reify_tbl ->
-   SmtAtom.Form.t ->
-   SmtAtom.Form.t SmtCertif.clause * SmtAtom.Form.t ->
-   int * SmtAtom.Form.t SmtCertif.clause) ->
+  (SmtBtype.reify_tbl -> SmtAtom.Op.reify_tbl ->
+   SmtAtom.Atom.reify_tbl -> SmtAtom.Form.reify ->
+   (SmtAtom.Form.t SmtCertif.clause * SmtAtom.Form.t) option ->
+   SmtAtom.Form.t list -> int * SmtAtom.Form.t SmtCertif.clause) ->
   SmtBtype.reify_tbl ->
   SmtAtom.Op.reify_tbl ->
-  SmtAtom.Atom.reify_tbl -> SmtAtom.Form.reify -> Structures.tactic
+  SmtAtom.Atom.reify_tbl -> SmtAtom.Form.reify ->
+  SmtAtom.Atom.reify_tbl -> SmtAtom.Form.reify ->
+  Term.constr list -> Structures.constr_expr list -> Structures.tactic
diff --git a/src/trace/smtForm.ml b/src/trace/smtForm.ml
index 069f2ec..c408343 100644
--- a/src/trace/smtForm.ml
+++ b/src/trace/smtForm.ml
@@ -17,6 +17,7 @@
 open Util
 open SmtMisc
 open CoqTerms
+open SmtBtype
 
 module type ATOM =
   sig
@@ -41,6 +42,7 @@ type fop =
   | Fiff
   | Fite
   | Fnot2 of int
+  | Fforall of (string * btype) list
 
 type ('a,'f) gen_pform =
   | Fatom of 'a
@@ -66,18 +68,21 @@ module type FORM =
     val is_pos : t -> bool
     val is_neg : t -> bool
 
-      val to_smt : (Format.formatter -> hatom -> unit) -> Format.formatter -> t -> unit
+    val to_string : ?pi:bool -> (hatom -> string) -> t -> string
+    val to_smt : (hatom -> string) -> 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
+    val get : ?declare:bool -> reify -> pform -> t
 
     (** Give a coq term, build the corresponding formula *)
     val of_coq : (Term.constr -> hatom) -> reify -> Term.constr -> t
 
+    val hash_hform : (hatom -> hatom) -> reify -> t -> t
     (** Flattening of [Fand] and [For], removing of [Fnot2]  *)
     val flatten : reify -> t -> t
 
@@ -145,20 +150,22 @@ module Make (Atom:ATOM) =
       | Pos hp -> hp.hval
       | Neg hp -> hp.hval
 
+    let rec to_string ?pi:(pi=false) atom_to_string = function
+      | Pos hp -> (if pi then string_of_int hp.index ^ ":" else "")
+                  ^ to_string_pform atom_to_string hp.hval
+      | Neg hp -> (if pi then string_of_int hp.index ^ ":" else "") ^ "(not "
+                  ^ to_string_pform atom_to_string 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_string_pform atom_to_string = function
+      | Fatom a -> atom_to_string a
+      | Fapp (op,args) -> to_string_op_args atom_to_string op args
 
-    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_string_op_args atom_to_string op args =
+      let (s1,s2) = if Array.length args = 0 then ("","") else ("(",")") in
+      s1 ^ to_string_op op ^
+        Array.fold_left (fun acc h -> acc ^ " " ^ to_string atom_to_string h) "" args ^ s2
 
-    and to_smt_op atom_to_smt fmt op args =
-      let s = match op with
+    and to_string_op = function
         | Ftrue -> "true"
         | Ffalse -> "false"
         | Fand -> "and"
@@ -167,12 +174,26 @@ module Make (Atom:ATOM) =
         | 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
-
+        | Fnot2 _ -> ""
+        | Fforall l -> "forall (" ^
+                       to_string_args l ^
+                       ")"
+                                                                                
+    and to_string_args = function
+      | [] -> " "
+      | (s, t)::rest -> " (" ^ s ^ " " ^ SmtBtype.to_string t ^ ")"
+                        ^ to_string_args rest
+
+    let dumbed_down op =
+      let dumbed_down_bt = function
+        | Tindex it -> Tindex (dummy_indexed_type (indexed_type_index it))
+        | x -> x in
+      match op with
+      | Fforall l -> Fforall (List.map (fun (x, bt) -> x, dumbed_down_bt bt) l)
+      | x -> x
+
+    let to_smt atom_to_string fmt f =
+      Format.fprintf fmt "%s" (to_string atom_to_string f)
 
     module HashedForm =
       struct
@@ -182,8 +203,8 @@ module Make (Atom:ATOM) =
 	let equal pf1 pf2 =
 	  match pf1, pf2 with
 	  | Fatom ha1, Fatom ha2 -> Atom.equal ha1 ha2
-	  | Fapp(op1,args1), Fapp(op2,args2) ->
-	      op1 = op2 && 
+	  | Fapp(op1,args1), Fapp(op2,args2) -> 
+	     dumbed_down op1 = dumbed_down op2 && 
 	       Array.length args1 == Array.length args2 &&
 	         (try
 		    for i = 0 to Array.length args1 - 1 do
@@ -205,7 +226,7 @@ module Make (Atom:ATOM) =
 	       | _ ->
 		  (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
+	     (hash_args * 10 + Hashtbl.hash (dumbed_down op)) * 2 + 1
 
       end
 
@@ -232,6 +253,7 @@ module Make (Atom:ATOM) =
 	    if Array.length args <> 2 then raise (NotWellTyped pf)
 	 | Fite ->
 	    if Array.length args <> 3 then raise (NotWellTyped pf)
+         | Fforall l -> ()
 
     let declare reify pf =
       check pf;
@@ -255,9 +277,11 @@ module Make (Atom:ATOM) =
       let _ = declare r pform_false in
       ()
 
-    let get reify pf =
-      try HashForm.find reify.tbl pf
-      with Not_found -> declare reify pf
+    let get ?declare:(decl=true) reify pf =
+      if decl then 
+        try HashForm.find reify.tbl pf
+        with Not_found -> declare reify pf
+      else Pos {index = -1; hval = pf}
 
     (** Given a coq term, build the corresponding formula *)
     type coq_cst =
@@ -376,6 +400,17 @@ module Make (Atom:ATOM) =
 
       mk_hform c
 
+    let hash_hform hash_hatom rf' hf =
+      let rec mk_hform = function
+        | Pos hp -> Pos (mk_hpform hp)
+        | Neg hp -> Neg (mk_hpform hp)
+      and mk_hpform {index = _; hval = hv} =
+        let new_hv = match hv with
+          | Fatom a -> Fatom (hash_hatom a)
+          | Fapp (fop, arr) -> Fapp (fop, Array.map mk_hform arr) in
+        match get rf' new_hv with Pos x | Neg x -> x in
+      mk_hform hf
+
     (** Flattening of Fand and For, removing of Fnot2 *)
     let set_sign f f' =
       if is_pos f then f' else neg f'
@@ -434,6 +469,7 @@ module Make (Atom:ATOM) =
 	 | 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)|]
+         | Fforall _ -> failwith "pf_to_coq on forall"
 
     let pform_tbl reify =
       let t = Array.make reify.count pform_true in
@@ -497,7 +533,8 @@ module Make (Atom:ATOM) =
 		        for i = 1 to n do
                           r := mklApp cnegb [|!r|]
                         done;
-                        !r in
+                        !r
+                     |Fforall _ -> failwith "interp_to_coq on forall" in
 	        Hashtbl.add form_tbl l pc;
 	        pc
       and interp_args op args =
diff --git a/src/trace/smtForm.mli b/src/trace/smtForm.mli
index c372bf5..4ee86e2 100644
--- a/src/trace/smtForm.mli
+++ b/src/trace/smtForm.mli
@@ -37,6 +37,7 @@ type fop =
   | Fiff
   | Fite
   | Fnot2 of int
+  | Fforall of (string * SmtBtype.btype) list 
  
 type ('a,'f) gen_pform = 
   | Fatom of 'a
@@ -61,18 +62,21 @@ module type FORM =
       val is_pos : t -> bool
       val is_neg : t -> bool
 
-      val to_smt : (Format.formatter -> hatom -> unit) -> Format.formatter -> t -> unit
+      val to_string : ?pi:bool -> (hatom -> string) -> t -> string
+      val to_smt : (hatom -> string) -> 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
+      val get : ?declare:bool -> reify -> pform -> t
       
       (** Given a coq term, build the corresponding formula *)  
       val of_coq : (Term.constr -> hatom) -> reify -> Term.constr -> t
 
+      val hash_hform : (hatom -> hatom) -> reify -> t -> t
+                                             
       (** Flattening of [Fand] and [For], removing of [Fnot2]  *)
       val flatten : reify -> t -> t
 
diff --git a/src/trace/smtMisc.ml b/src/trace/smtMisc.ml
index 1ad92ac..58de402 100644
--- a/src/trace/smtMisc.ml
+++ b/src/trace/smtMisc.ml
@@ -38,3 +38,7 @@ let declare_new_variable = Structures.declare_new_variable
 let mkName s =
   let id = Names.id_of_string s in
   Names.Name id
+
+let string_of_name = function
+    Names.Name id -> Names.string_of_id id
+  | _ -> failwith "unnamed rel"
diff --git a/src/trace/smtMisc.mli b/src/trace/smtMisc.mli
index d6aa792..e5cf69f 100644
--- a/src/trace/smtMisc.mli
+++ b/src/trace/smtMisc.mli
@@ -5,3 +5,4 @@ val mklApp : Term.constr Lazy.t -> Term.constr array -> Term.constr
 val declare_new_type : Names.variable -> Term.constr
 val declare_new_variable : Names.variable -> Term.types -> Term.constr
 val mkName : string -> Names.name
+val string_of_name : Names.name -> string
diff --git a/src/trace/smtTrace.ml b/src/trace/smtTrace.ml
index 96d5f0f..9042b8b 100644
--- a/src/trace/smtTrace.ml
+++ b/src/trace/smtTrace.ml
@@ -118,7 +118,9 @@ let get_res c s =
 let get_other c s =
   match c.kind with
   | Other res -> res
-  | _ -> Printf.printf "get_other %s\n" s; assert false
+  | Same _ -> failwith "get_other on a Same"
+  | Res _ -> failwith "get_other on a Res"
+  | Root -> failwith "get_other on a Root"
 
 let get_val c =
   match c.value with
@@ -145,7 +147,86 @@ let rec get_pos c =
 
 let eq_clause c1 c2 = (repr c1).id = (repr c2).id
 
+
+(* Reorders the roots according to the order they were given in initially. *)
+let order_roots init_index first =
+  let r = ref first in
+  let acc = ref [] in
+  while isRoot !r.kind do
+    begin match !r.value with
+    | Some [f] -> let n = next !r in
+                  clear_links !r; 
+                  acc := (init_index f, !r) :: !acc;
+                  r := n
+    | _ -> failwith "root value has unexpected form" end
+  done;
+  let _, lr = List.sort (fun (i1, _) (i2, _) -> Pervasives.compare i1 i2) !acc
+             |> List.split in
+  let link_to c1 c2 =
+    let curr_id = c2.id -1 in
+    c1.id <- curr_id;
+    c1.pos <- Some curr_id;
+    link c1 c2; c1 in
+  List.fold_right link_to lr !r, lr
+
+
+(* <add_scertifs> adds the clauses <to_add> after the roots and makes sure that 
+the following clauses reference those clauses instead of the roots *)
+let add_scertifs to_add c =
+  let r = ref c in
+  clear (); ignore (next_id ());
+  while isRoot !r.kind do
+    ignore (next_id ());
+    r := next !r;
+  done;
+  let after_roots = !r in
+  r := prev !r;
+  let tbl : (int, 'a SmtCertif.clause) Hashtbl.t =
+    Hashtbl.create 17 in
+  let rec push_all = function
+    | [] -> ()
+    | (kind, ov, t_cl)::t -> let cl = mk_scertif kind ov in
+                             Hashtbl.add tbl t_cl.id cl;
+                             link !r cl;
+                             r := next !r;
+                             push_all t in
+  push_all to_add; link !r after_roots; r:= after_roots;
+  let uc c = try Hashtbl.find tbl c.id
+             with Not_found -> c in
+  let update_kind = function
+    | Root -> Root
+    | Same c -> Same (uc c)
+    | Res {rc1 = r1; rc2 = r2; rtail = rt} ->
+       Res {rc1 = uc r1;
+            rc2 = uc r2;
+            rtail = List.map uc rt}
+    | Other u ->
+       Other begin match u with
+         | ImmBuildProj (c, x) -> ImmBuildProj (uc c, x)
+         | ImmBuildDef c -> ImmBuildDef (uc c)
+         | ImmBuildDef2 c -> ImmBuildDef2 (uc c)
+         | Forall_inst (c, x) -> Forall_inst (uc c, x) 
+         | ImmFlatten (c, x) -> ImmFlatten (uc c, x) 
+         | SplArith (c, x, y) -> SplArith (uc c, x, y) 
+         | SplDistinctElim (c, x) -> SplDistinctElim (uc c, x) 
+
+         | Hole (cs, x) -> Hole (List.map uc cs, x)
+
+         | x -> x end in
+  let continue = ref true in
+  while !continue do
+    !r.kind <- update_kind !r.kind;
+    !r.id <- next_id ();
+    match !r.next with 
+    | None -> continue := false
+    | Some n -> r := n
+  done;
+  !r
+
 (* Selection of useful rules *)
+(* For <select>, <occur> and <alloc> we assume that the roots and only the 
+roots are at the beginning of the smtcoq certif *)
+(* After <select> no selected clauses are used so that <occur> works properly*)
 let select c =
   let mark c =
     if not (isRoot c.kind) then c.used <- 1 in
@@ -162,7 +243,8 @@ let select c =
             List.iter mark res.rtail
           end else
           skip !r;
-     | Same _ ->
+     | Same c ->
+        mark c;
         skip !r
      | _ ->
         if !r.used == 1 then
@@ -176,9 +258,8 @@ let select c =
     r := p
   done
 
-
-
-(* Compute the number of occurence of each_clause *)
+(* Compute the number of occurence of each clause so that <alloc> works 
+properly *)
 let rec occur c =
   match c.kind with
   | Root -> c.used <- c.used + 1
@@ -226,23 +307,22 @@ let alloc c =
   let decr_other o =
     List.iter decr_clause (used_clauses o) in
 
-  while !r.next <> None do
-    let n = next !r in
+  let continue = ref true in
+  while !continue do
     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
+    begin try match !free_pos with
+              | p::free -> free_pos := free; !r.pos <- Some p
+              | _ -> incr last_set; !r.pos <- Some !last_set
+          with _ -> failwith (to_string !r.kind)
     end;
-    r := n
+    match !r.next with
+    | None -> continue := false
+    | Some n -> 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
 
 
@@ -277,12 +357,13 @@ let to_coq to_lit interp (cstep,
     cImmBuildProj,cImmBuildDef,cImmBuildDef2,
     cEqTr, cEqCgr, cEqCgrP,
     cLiaMicromega, cLiaDiseq, cSplArith, cSplDistinctElim,
-    cHole) confl =
+    cHole, cForallInst) confl sf =
 
   let cuts = ref [] in
 
   let out_f f = to_lit f in
   let out_c c = mkInt (get_pos c) in
+  let out_cl cl = List.fold_right (fun f l -> mklApp ccons [|Lazy.force cint; out_f f; l|]) cl (mklApp cnil [|Lazy.force cint|]) in
   let step_to_coq c =
     match c.kind with
     | Res res ->
@@ -335,11 +416,20 @@ let to_coq to_lit interp (cstep,
            let ass_ty = interp (prem, concl) in
            cuts := (ass_name, ass_ty)::!cuts;
            let ass_var = Term.mkVar ass_name in
-           let out_cl cl = List.fold_right (fun f l -> mklApp ccons [|Lazy.force cint; out_f f; l|]) cl (mklApp cnil [|Lazy.force cint|]) in
            let prem_id' = List.fold_right (fun c l -> mklApp ccons [|Lazy.force cint; out_c c; l|]) prem_id (mklApp cnil [|Lazy.force cint|]) in
            let prem' = List.fold_right (fun cl l -> mklApp ccons [|Lazy.force cState_C_t; out_cl cl; l|]) prem (mklApp cnil [|Lazy.force cState_C_t|]) in
            let concl' = out_cl concl in
            mklApp cHole [|out_c c; prem_id'; prem'; concl'; ass_var|]
+        | Forall_inst (cl, concl) | Qf_lemma (cl, concl) ->
+           let clemma, cplemma = match sf with
+             | Some find -> find cl
+             | None -> assert false in
+           let concl' = out_cl [concl] in
+           let app_name = Names.id_of_string ("app" ^ (string_of_int (Hashtbl.hash concl))) in
+           let app_var = Term.mkVar app_name in
+           let app_ty = Term.mkArrow clemma (interp ([], [concl])) in
+           cuts := (app_name, app_ty)::!cuts;
+           mklApp cForallInst [|out_c c; clemma; cplemma; concl'; app_var|]
 	end
     | _ -> assert false in
   let step = Lazy.force cstep in
@@ -373,7 +463,8 @@ let to_coq to_lit interp (cstep,
   (*   trace.(q) <- Structures.mkArray (step, traceq) *)
   (* end; *)
   (* (Structures.mkArray (mklApp carray [|step|], trace), last_root, !cuts) *)
-  (Structures.mkTrace step_to_coq next carray clist cnil ccons cpair !nc step def_step r, last_root, !cuts)
+  let tres = Structures.mkTrace step_to_coq next carray clist cnil ccons cpair !nc step def_step r in
+  (tres, last_root, !cuts)
 
 
 
diff --git a/src/trace/smtTrace.mli b/src/trace/smtTrace.mli
index 533725b..57d0d42 100644
--- a/src/trace/smtTrace.mli
+++ b/src/trace/smtTrace.mli
@@ -25,6 +25,10 @@ val repr : 'a SmtCertif.clause -> 'a SmtCertif.clause
 val set_same : 'a SmtCertif.clause -> 'a SmtCertif.clause -> unit
 val get_pos : 'a SmtCertif.clause -> int
 val eq_clause : 'a SmtCertif.clause -> 'b SmtCertif.clause -> bool
+val order_roots : ('a -> int) -> 'a SmtCertif.clause ->
+                  'a SmtCertif.clause * 'a SmtCertif.clause list
+val add_scertifs : ('a SmtCertif.clause_kind * 'a list option * 'a SmtCertif.clause) list -> 
+                   'a SmtCertif.clause -> 'a SmtCertif.clause
 val select : 'a SmtCertif.clause -> unit
 val occur : 'a SmtCertif.clause -> unit
 val alloc : 'a SmtCertif.clause -> int
@@ -32,16 +36,16 @@ val naive_alloc : 'a SmtCertif.clause -> int
 val build_certif : 'a SmtCertif.clause -> 'b SmtCertif.clause -> int
 val to_coq :
   ('a -> Term.constr) ->
-  ('a list list * 'a list -> 'b) ->
+  ('a list list * 'a list -> Term.types) ->
   Term.types Lazy.t * Term.constr Lazy.t * Term.constr Lazy.t *
   Term.constr Lazy.t * Term.constr Lazy.t * Term.constr Lazy.t *
   Term.constr Lazy.t * Term.constr Lazy.t * Term.constr Lazy.t *
   Term.constr Lazy.t * Term.constr Lazy.t * Term.constr Lazy.t *
   Term.constr Lazy.t * Term.constr Lazy.t * Term.constr Lazy.t *
   Term.constr Lazy.t * Term.constr Lazy.t * Term.constr Lazy.t *
-  Term.constr Lazy.t ->
-  'a SmtCertif.clause ->
-  Term.constr * 'a SmtCertif.clause * (Names.identifier * 'b) list
+  Term.constr Lazy.t * Term.constr Lazy.t -> 'a SmtCertif.clause ->
+  ('a SmtCertif.clause -> Term.constr * Term.constr) option ->
+  Term.constr * 'a SmtCertif.clause * (Names.identifier * Term.types) list
 module MakeOpt :
   functor (Form : SmtForm.FORM) ->
     sig
diff --git a/src/verit/verit.ml b/src/verit/verit.ml
index 88d0769..8eb1b60 100644
--- a/src/verit/verit.ml
+++ b/src/verit/verit.ml
@@ -21,9 +21,10 @@ open Decl_kinds
 open SmtMisc
 open CoqTerms
 open SmtForm
-open SmtCertif
 open SmtTrace
 open SmtAtom
+open SmtBtype
+open SmtCertif
 
 
 let debug = false
@@ -32,8 +33,38 @@ let debug = false
 (******************************************************************************)
 (* Given a verit trace build the corresponding certif and theorem             *)
 (******************************************************************************)
+exception Import_trace of int
+
+let get_val = function
+    Some a -> a
+  | None -> assert false
 
-let import_trace filename first =
+(* For debugging certif processing : <add_scertif> <select> <occur> <alloc> *)
+let print_certif c where=
+  let r = ref c in
+  let out_channel = open_out where in
+  let fmt = Format.formatter_of_out_channel out_channel in
+  let continue = ref true in
+  while !continue do
+    let kind = to_string (!r.kind) in
+    let id = !r.id in
+    let pos = match !r.pos with
+      | None -> "None"
+      | Some p -> string_of_int p in
+    let used = !r.used in
+    Format.fprintf fmt "id:%i kind:%s pos:%s used:%i value:" id kind pos used;
+    begin match !r.value with
+    | None -> Format.fprintf fmt "None"
+    | Some l -> List.iter (fun f -> Form.to_smt Atom.to_string fmt f;
+                                    Format.fprintf fmt " ") l end;
+    Format.fprintf fmt "\n";
+    match !r.next with
+    | None -> continue := false
+    | Some n -> r := n 
+  done;
+  Format.fprintf fmt "@."; close_out out_channel
+                            
+let import_trace ra' rf' filename first lsmt =
   let chan = open_in filename in
   let lexbuf = Lexing.from_channel chan in
   let confl_num = ref (-1) in
@@ -54,23 +85,29 @@ let import_trace filename first =
   with
     | VeritLexer.Eof ->
        close_in chan;
-       let first =
-         let aux = VeritSyntax.get_clause !first_num in
-          match first, aux.value with
-          | Some (root,l), Some (fl::nil) ->
-            if Form.equal l fl then
-              aux
-            else (
-              aux.kind <- Other (ImmFlatten(root,fl));
-              SmtTrace.link root aux;
-              root
-            )
-          | _,_ -> aux in
-      let confl = VeritSyntax.get_clause !confl_num in
-      SmtTrace.select confl;
-      (* Trace.share_prefix first (2 * last.id); *)
-      occur confl;
-      (alloc first, confl)
+       let cfirst = ref (VeritSyntax.get_clause !first_num) in
+       let confl = ref (VeritSyntax.get_clause !confl_num) in
+       let re_hash = Form.hash_hform (Atom.hash_hatom ra') rf' in
+       begin match first with
+       | None -> ()
+       | Some _ ->
+          let cf, lr = order_roots (VeritSyntax.init_index lsmt re_hash)
+                         !cfirst in
+          cfirst := cf;
+          let to_add = VeritSyntax.qf_to_add (List.tl lr) in
+          let to_add =
+            (match first, !cfirst.value with
+             | Some (root, l), Some [fl] when not (Form.equal l (re_hash fl)) ->
+                let cfirst_value = !cfirst.value in
+                !cfirst.value <- root.value;
+                [Other (ImmFlatten (root, fl)), cfirst_value, !cfirst]
+             | _ -> []) @ to_add in
+       match to_add with
+       | [] -> ()
+       | _  -> confl := add_scertifs to_add !cfirst end;
+       select !confl;
+       occur !confl;
+       (alloc !cfirst, !confl)
     | Parsing.Parse_error -> failwith ("Verit.import_trace: parsing error line "^(string_of_int !line))
 
 
@@ -85,8 +122,10 @@ let import_all fsmt fproof =
   let ro = Op.create () in
   let ra = VeritSyntax.ra in
   let rf = VeritSyntax.rf in
+  let ra' = VeritSyntax.ra' in
+  let rf' = VeritSyntax.rf' in
   let roots = Smtlib2_genConstr.import_smtlib2 rt ro ra rf fsmt in
-  let (max_id, confl) = import_trace fproof None in
+  let (max_id, confl) = import_trace ra' rf' fproof None [] in
   (rt, ro, ra, rf, roots, max_id, confl)
 
 
@@ -101,9 +140,9 @@ let checker fsmt fproof = SmtCommands.checker (import_all fsmt fproof)
 (** Given a Coq formula build the proof                                       *)
 (******************************************************************************)
 
-let export out_channel rt ro l =
+let export out_channel rt ro lsmt =
   let fmt = Format.formatter_of_out_channel out_channel in
-  Format.fprintf fmt "(set-logic QF_UFLIA)@.";
+  Format.fprintf fmt "(set-logic UFLIA)@.";
 
   List.iter (fun (i,t) ->
     let s = "Tindex_"^(string_of_int i) in
@@ -111,47 +150,60 @@ let export out_channel rt ro l =
     Format.fprintf fmt "(declare-sort %s 0)@." s
   ) (SmtBtype.to_list rt);
 
-  List.iter (fun (i,cod,dom,op) ->
+  List.iter (fun (i,dom,cod,op) ->
     let s = "op_"^(string_of_int i) in
     VeritSyntax.add_fun s op;
     Format.fprintf fmt "(declare-fun %s (" s;
     let is_first = ref true in
-    Array.iter (fun t -> if !is_first then is_first := false else Format.fprintf fmt " "; SmtBtype.to_smt fmt t) cod;
+    Array.iter (fun t -> if !is_first then is_first := false else Format.fprintf fmt " "; SmtBtype.to_smt fmt t) dom;
     Format.fprintf fmt ") ";
-    SmtBtype.to_smt fmt dom;
+    SmtBtype.to_smt fmt cod;
     Format.fprintf fmt ")@."
   ) (Op.to_list ro);
 
-  Format.fprintf fmt "(assert ";
-  Form.to_smt Atom.to_smt fmt l;
-  Format.fprintf fmt ")@\n(check-sat)@\n(exit)@."
+  List.iter (fun u -> Format.fprintf fmt "(assert ";
+                      Form.to_smt Atom.to_string fmt u;
+                      Format.fprintf fmt ")\n") lsmt;
+
+  Format.fprintf fmt "(check-sat)\n(exit)@."
 
 
 (* val call_verit : Btype.reify_tbl -> Op.reify_tbl -> Form.t -> (Form.t clause * Form.t) -> (int * Form.t clause) *)
-let call_verit rt ro fl root =
-  let (filename, outchan) = Filename.open_temp_file "verit_coq" ".smt2" in
-  export outchan rt ro fl;
+let call_verit rt ro ra' rf' first lsmt =
+  let filename, outchan = Filename.open_temp_file "verit_coq" ".smt2" in
+  export outchan rt ro lsmt;
   close_out outchan;
   let logfilename = Filename.chop_extension filename ^ ".vtlog" in
-  let command = "veriT --proof-prune --proof-merge --proof-with-sharing --cnf-definitional --disable-ackermann --input=smtlib2 --proof=" ^ logfilename ^ " " ^ filename in
+  let wname, woc = Filename.open_temp_file "warnings_verit" ".log" in
+  close_out woc;
+  let command = "veriT --proof-prune --proof-merge --proof-with-sharing --cnf-definitional --disable-ackermann --input=smtlib2 --proof=" ^ logfilename ^ " " ^ filename ^ " 2> " ^ wname in
   Format.eprintf "%s@." command;
   let t0 = Sys.time () in
   let exit_code = Sys.command command in
   let t1 = Sys.time () in
   Format.eprintf "Verit = %.5f@." (t1-.t0);
-  if exit_code <> 0 then
-    failwith ("Verit.call_verit: command " ^ command ^
-	        " exited with code " ^ string_of_int exit_code);
-  try
-    import_trace logfilename (Some root)
-  with
-    | VeritSyntax.Sat -> Structures.error "veriT can't prove this"
-
-
-let tactic () =
+  let win = open_in wname in
+  try 
+    if exit_code <> 0 then
+      failwith ("Verit.call_verit: command " ^ command ^
+	          " exited with code " ^ string_of_int exit_code);
+
+    try let _ = input_line win in
+        Structures.error "veriT returns 'unknown'"
+    with End_of_file ->
+          try
+            let res = import_trace ra' rf' logfilename first lsmt in
+            close_in win; Sys.remove wname; res
+          with
+          | VeritSyntax.Sat -> Structures.error "veriT found a counter-example"
+  with x -> close_in win; Sys.remove wname; raise x
+
+let tactic lcpl lcepl =
   clear_all ();
   let rt = SmtBtype.create () in
   let ro = Op.create () in
   let ra = VeritSyntax.ra in
   let rf = VeritSyntax.rf in
-  SmtCommands.tactic call_verit rt ro ra rf
+  let ra' = VeritSyntax.ra' in
+  let rf' = VeritSyntax.rf' in
+  SmtCommands.tactic call_verit rt ro ra rf ra' rf' lcpl lcepl
diff --git a/src/verit/verit.mli b/src/verit/verit.mli
index 68ee317..95959da 100644
--- a/src/verit/verit.mli
+++ b/src/verit/verit.mli
@@ -1,8 +1,8 @@
 val debug : bool
 val import_trace :
-  string ->
+  SmtAtom.Atom.reify_tbl -> SmtAtom.Form.reify -> string ->
   (SmtAtom.Form.t SmtCertif.clause * SmtAtom.Form.t) option ->
-  int * SmtAtom.Form.t SmtCertif.clause
+  SmtAtom.Form.t list -> int * SmtAtom.Form.t SmtCertif.clause
 val clear_all : unit -> unit
 val import_all :
   string ->
@@ -22,11 +22,13 @@ val checker : string -> string -> unit
 val export :
   out_channel ->
   SmtBtype.reify_tbl -> SmtAtom.Op.reify_tbl ->
-  SmtAtom.Form.t -> unit
+  SmtAtom.Form.t list -> unit
 val call_verit :
   SmtBtype.reify_tbl ->
   SmtAtom.Op.reify_tbl ->
-  SmtAtom.Form.t ->
-  SmtAtom.Form.t SmtCertif.clause * SmtAtom.Form.t ->
+  SmtAtom.Atom.reify_tbl ->
+  SmtAtom.Form.reify ->
+  (SmtAtom.Form.t SmtCertif.clause * SmtAtom.Form.t) option ->
+  SmtAtom.Form.t list ->
   int * SmtAtom.Form.t SmtCertif.clause
-val tactic : unit -> Structures.tactic
+val tactic : Term.constr list -> Structures.constr_expr list -> Structures.tactic
diff --git a/src/verit/veritLexer.mll b/src/verit/veritLexer.mll
index 2a51a02..80fcc39 100644
--- a/src/verit/veritLexer.mll
+++ b/src/verit/veritLexer.mll
@@ -55,6 +55,7 @@
         "dl_disequality", DLDE;
         "la_disequality", LADE;
         "forall_inst", FINS;
+	"forall", FORALL;
         "exists_inst", EINS;
         "skolem_ex_ax", SKEA;
         "skolem_all_ax", SKAA;
@@ -105,6 +106,7 @@ let alpha = [ 'a'-'z' 'A' - 'Z' ]
 let blank = [' ' '\t']
 let newline = ['\n' '\r']
 let var = alpha (alpha|digit|'_')*
+let atvar = '@' var
 let bindvar = '?' var+
 let int = '-'? digit+
 
@@ -136,7 +138,9 @@ rule token = parse
   | "distinct"                 { DIST }
 
   | "Formula is Satisfiable"   { SAT }
-
+  | "Tindex_" (int as i)       { TINDEX (int_of_string i) }
+  | "Int"     	      	       { TINT }
+  | "Bool"		       { TBOOL }
   | int                        { try INT (int_of_string (Lexing.lexeme lexbuf))
 	                         with _ -> 
                                    BIGINT 
@@ -147,4 +151,6 @@ rule token = parse
                                    | Not_found -> VAR v }
   | bindvar                    { BINDVAR (Lexing.lexeme lexbuf) }
 
+  | atvar 		       { ATVAR (Lexing.lexeme lexbuf) }
+
   | eof                        { raise Eof }
diff --git a/src/verit/veritParser.mly b/src/verit/veritParser.mly
index 799c32d..4ea6cd6 100644
--- a/src/verit/veritParser.mly
+++ b/src/verit/veritParser.mly
@@ -15,6 +15,7 @@
 
 
 %{
+  open SmtBtype 
   open SmtAtom
   open SmtForm
   open VeritSyntax
@@ -29,13 +30,20 @@
 %token COLON SHARP
 %token LPAR RPAR
 %token NOT XOR ITE EQ LT LEQ GT GEQ PLUS MINUS MULT OPP LET DIST
-%token INPU DEEP TRUE FALS ANDP ANDN ORP ORN XORP1 XORP2 XORN1 XORN2 IMPP IMPN1 IMPN2 EQUP1 EQUP2 EQUN1 EQUN2 ITEP1 ITEP2 ITEN1 ITEN2 EQRE EQTR EQCO EQCP DLGE LAGE LATA DLDE LADE FINS EINS SKEA SKAA QNTS QNTM RESO AND NOR OR NAND XOR1 XOR2 NXOR1 NXOR2 IMP NIMP1 NIMP2 EQU1 EQU2 NEQU1 NEQU2 ITE1 ITE2 NITE1 NITE2 TPAL TLAP TPLE TPNE TPDE TPSA TPIE TPMA TPBR TPBE TPSC TPPP TPQT TPQS TPSK SUBP HOLE
+%token TBOOL TINT
+%token<int> TINDEX
+%token INPU DEEP TRUE FALS ANDP ANDN ORP ORN XORP1 XORP2 XORN1 XORN2 IMPP IMPN1 IMPN2 EQUP1 EQUP2 EQUN1 EQUN2 ITEP1 ITEP2 ITEN1 ITEN2 EQRE EQTR EQCO EQCP DLGE LAGE LATA DLDE LADE FINS EINS SKEA SKAA QNTS QNTM RESO AND NOR OR NAND XOR1 XOR2 NXOR1 NXOR2 IMP NIMP1 NIMP2 EQU1 EQU2 NEQU1 NEQU2 ITE1 ITE2 NITE1 NITE2 TPAL TLAP TPLE TPNE TPDE TPSA TPIE TPMA TPBR TPBE TPSC TPPP TPQT TPQS TPSK SUBP HOLE FORALL
 %token <int> INT
 %token <Big_int.big_int> BIGINT
-%token <string> VAR BINDVAR
+%token <string> VAR BINDVAR ATVAR
+
 
 /* type de "retour" du parseur : une clause */
 %type <int> line
+/*
+%type <VeritSyntax.atom_form_lit> term
+%start term
+*/
 %start line
 
 
@@ -45,9 +53,13 @@ line:
   | SAT                                                    { raise Sat }
   | INT COLON LPAR typ clause                   RPAR EOL   { mk_clause ($1,$4,$5,[]) }
   | INT COLON LPAR typ clause clause_ids_params RPAR EOL   { mk_clause ($1,$4,$5,$6) }
+  | INT COLON LPAR TPQT LPAR SHARP INT COLON LPAR forall_decl RPAR RPAR INT RPAR EOL { add_solver $7 $10; add_ref $7 $1; mk_clause ($1, Tpqt, [], [$13]) }
+  | INT COLON LPAR FINS LPAR SHARP INT COLON LPAR OR LPAR NOT SHARP INT RPAR lit RPAR RPAR RPAR EOL
+  { mk_clause ($1, Fins, [snd $16], [get_ref $14]) }
 ;
 
 typ:
+  | TPBR                                                   { Tpbr  }
   | INPU                                                   { Inpu  }
   | DEEP                                                   { Deep  }
   | TRUE                                                   { True  }
@@ -80,7 +92,6 @@ typ:
   | LATA                                                   { Lata  }
   | DLDE                                                   { Dlde  }
   | LADE                                                   { Lade  }
-  | FINS                                                   { Fins  }
   | EINS                                                   { Eins  }
   | SKEA                                                   { Skea  }
   | SKAA                                                   { Skaa  }
@@ -114,11 +125,9 @@ typ:
   | TPSA                                                   { Tpsa  }
   | TPIE                                                   { Tpie  }
   | TPMA                                                   { Tpma  }
-  | TPBR                                                   { Tpbr  }
   | TPBE                                                   { Tpbe  }
   | TPSC                                                   { Tpsc  }
   | TPPP                                                   { Tppp  }
-  | TPQT                                                   { Tpqt  }
   | TPQS                                                   { Tpqs  }
   | TPSK                                                   { Tpsk  }
   | SUBP                                                   { Subp  }
@@ -127,7 +136,7 @@ typ:
 
 clause:
   | LPAR          RPAR                                     { [] }
-  | LPAR lit_list RPAR                                     { $2 }
+  | LPAR lit_list RPAR                                     { let _, l = list_dec $2 in l }
 ;
 
 lit_list:
@@ -135,67 +144,105 @@ lit_list:
   | lit lit_list                                           { $1::$2 }
 ;
 
-lit:   /* returns a SmtAtom.Form.t */
-  | name_term                                              { lit_of_atom_form_lit rf $1 }
-  | LPAR NOT lit RPAR                                      { Form.neg $3 }
+lit:   /* returns a SmtAtom.Form.t option */
+  | name_term                                              { let decl, t = $1 in decl, lit_of_atom_form_lit rf (decl, t) }
+  | LPAR NOT lit RPAR                                      { apply_dec Form.neg $3 }
+;
+
+nlit:   
+  | LPAR NOT lit RPAR                                      { apply_dec Form.neg $3 }
+;
+
+var_atvar:   
+  | VAR			                                   { $1 }
+  | ATVAR			                           { $1 }
 ;
 
-name_term:   /* returns a SmtAtom.Form.pform or a SmtAtom.hatom */
+name_term:   /* returns a bool * (SmtAtom.Form.pform or SmtAtom.hatom), the boolean indicates if we should declare the term or not */
   | SHARP INT                                              { get_solver $2 }
-  | SHARP INT COLON LPAR term RPAR                         { let res = $5 in add_solver $2 res; res }
-  | TRUE                                                   { Form Form.pform_true }
-  | FALS                                                   { Form Form.pform_false }
-  | VAR                                                    { Atom (Atom.get ra (Aapp (get_fun $1,[||]))) }
-  | BINDVAR                                                { Hashtbl.find hlets $1 }
-  | INT                                                    { Atom (Atom.hatom_Z_of_int ra $1) }
-  | BIGINT                                                 { Atom (Atom.hatom_Z_of_bigint ra $1) }
+  | SHARP INT COLON LPAR term RPAR                         { let u = $5 in add_solver $2 u; u }
+  | TRUE                                                   { true, Form Form.pform_true }
+  | FALS                                                   { true, Form Form.pform_false }
+  | var_atvar						   { let x = $1 in match find_opt_qvar x with
+    					                   | Some bt -> false, Atom (Atom.get ~declare:false ra (Aapp (dummy_indexed_op (Rel_name x) [||] bt, [||])))
+							   | None -> true, Atom (Atom.get ra (Aapp (get_fun $1, [||]))) }
+  | BINDVAR                                                { true, Hashtbl.find hlets $1 }
+  | INT                                                    { true, Atom (Atom.hatom_Z_of_int ra $1) }
+  | BIGINT                                                 { true, Atom (Atom.hatom_Z_of_bigint ra $1) }
+;
+
+tvar:
+  | TINT						   { TZ }
+  | TBOOL						   { Tbool }
+  | TINDEX						   { Tindex (indexed_type_of_int $1) }
+
+var_decl_list:
+  | LPAR var_atvar tvar RPAR				   { add_qvar $2 $3; [$2, $3] }
+  | LPAR var_atvar tvar RPAR var_decl_list		   { add_qvar $2 $3; ($2, $3)::$5 }
 ;
 
-term:   /* returns a SmtAtom.Form.pform or a SmtAtom.hatom */
+forall_decl:
+  | FORALL LPAR var_decl_list RPAR name_term		   { clear_qvar (); false, Form (Fapp (Fforall $3, [|lit_of_atom_form_lit rf $5|])) }
+; 
+
+term:   /* returns a bool * (SmtAtom.Form.pform or SmtAtom.hatom), the boolean indicates if we should declare the term or not */
   | LPAR term RPAR                                         { $2 }
 
   /* Formulae */
-  | TRUE                                                   { Form Form.pform_true }
-  | FALS                                                   { Form Form.pform_false }
-  | AND lit_list                                           { Form (Fapp (Fand, Array.of_list $2)) }
-  | OR lit_list                                            { Form (Fapp (For, Array.of_list $2)) }
-  | IMP lit_list                                           { Form (Fapp (Fimp, Array.of_list $2)) }
-  | XOR lit_list                                           { Form (Fapp (Fxor, Array.of_list $2)) }
-  | ITE lit_list                                           { Form (Fapp (Fite, Array.of_list $2)) }
+  | TRUE                                                   { true, Form Form.pform_true }
+  | FALS                                                   { true, Form Form.pform_false }
+  | AND lit_list                                           { apply_dec (fun x -> Form (Fapp (Fand, Array.of_list x))) (list_dec $2) }
+  | OR lit_list                                            { apply_dec (fun x -> Form (Fapp (For, Array.of_list x))) (list_dec $2) }
+  | IMP lit_list                                           { apply_dec (fun x -> Form (Fapp (Fimp, Array.of_list x))) (list_dec $2) }
+  | XOR lit_list                                           { apply_dec (fun x -> Form (Fapp (Fxor, Array.of_list x))) (list_dec $2) }
+  | ITE lit_list                                           { apply_dec (fun x -> Form (Fapp (Fite, Array.of_list x))) (list_dec $2) }
+  | forall_decl                                            { $1 }
 
   /* Atoms */
-  | INT                                                    { Atom (Atom.hatom_Z_of_int ra $1) }
-  | BIGINT                                                 { Atom (Atom.hatom_Z_of_bigint ra $1) }
-  | LT name_term name_term                                 { match $2,$3 with |Atom h1, Atom h2 -> Atom (Atom.mk_lt ra h1 h2) | _,_ -> assert false }
-  | LEQ name_term name_term                                { match $2,$3 with |Atom h1, Atom h2 -> Atom (Atom.mk_le ra h1 h2) | _,_ -> assert false }
-  | GT name_term name_term                                 { match $2,$3 with |Atom h1, Atom h2 -> Atom (Atom.mk_gt ra h1 h2) | _,_ -> assert false }
-  | GEQ name_term name_term                                { match $2,$3 with |Atom h1, Atom h2 -> Atom (Atom.mk_ge ra h1 h2) | _,_ -> assert false }
-  | PLUS name_term name_term                               { match $2,$3 with |Atom h1, Atom h2 -> Atom (Atom.mk_plus ra h1 h2) | _,_ -> assert false }
-  | MULT name_term name_term                               { match $2,$3 with |Atom h1, Atom h2 -> Atom (Atom.mk_mult ra h1 h2) | _,_ -> assert false }
-  | MINUS name_term name_term                              { match $2,$3 with |Atom h1, Atom h2 -> Atom (Atom.mk_minus ra h1 h2) | _,_ -> assert false }
-  | MINUS name_term                                        { match $2 with | Atom h -> Atom (Atom.mk_opp ra h) | _ -> assert false }
-  | OPP name_term                                          { match $2 with | Atom h -> Atom (Atom.mk_opp ra h) | _ -> assert false }
-  | DIST args                                              { let a = Array.of_list $2 in Atom (Atom.mk_distinct ra (Atom.type_of a.(0)) a) }
-  | VAR                                                    { Atom (Atom.get ra (Aapp (get_fun $1, [||]))) }
-  | VAR args                                               { Atom (Atom.get ra (Aapp (get_fun $1, Array.of_list $2))) }
+  | INT                                                    { true, Atom (Atom.hatom_Z_of_int ra $1) }
+  | BIGINT                                                 { true, Atom (Atom.hatom_Z_of_bigint ra $1) }
+  | LT name_term name_term                                 { apply_bdec_atom (Atom.mk_lt ra) $2 $3 }
+  | LEQ name_term name_term                                { apply_bdec_atom (Atom.mk_le ra) $2 $3 }
+  | GT name_term name_term                                 { apply_bdec_atom (Atom.mk_gt ra) $2 $3 }
+  | GEQ name_term name_term                                { apply_bdec_atom (Atom.mk_ge ra) $2 $3 }
+  | PLUS name_term name_term                               { apply_bdec_atom (Atom.mk_plus ra) $2 $3 }
+  | MULT name_term name_term                               { apply_bdec_atom (Atom.mk_mult ra) $2 $3 }
+  | MINUS name_term name_term                              { apply_bdec_atom (Atom.mk_minus ra) $2 $3}
+  | MINUS name_term                                        { apply_dec_atom (fun d a -> Atom.mk_neg ra a) $2 }
+  | OPP name_term                                          { apply_dec_atom (fun d a -> Atom.mk_opp ra ~declare:d a) $2 }
+  | DIST args                                              { let da, la = list_dec $2 in
+    	 						     let a = Array.of_list la in
+							     da, Atom (Atom.mk_distinct ra (Atom.type_of a.(0)) ~declare:da a) }
+  | VAR                                                    {let x = $1 in match find_opt_qvar x with
+    							     | Some bt -> false, Atom (Atom.get ~declare:false ra (Aapp (dummy_indexed_op (Rel_name x) [||] bt, [||])))
+							     | None -> true, Atom (Atom.get ra (Aapp (get_fun $1, [||])))}
+  | VAR args                                               { let f = $1 in let a = $2 in match find_opt_qvar f with
+    							     | Some bt -> let op = dummy_indexed_op (Rel_name f) [||] bt in
+							       	       	  false, Atom (Atom.get ~declare:false ra (Aapp (op, Array.of_list (snd (list_dec a)))))
+      							     | None -> let dl, l = list_dec $2 in
+							       	       dl, Atom (Atom.get ra ~declare:dl (Aapp (get_fun f, Array.of_list l))) }
+
 
   /* Both */
-  | EQ name_term name_term                                 { let t1 = $2 in let t2 = $3 in match t1,t2 with | Atom h1, Atom h2 when (match Atom.type_of h1 with | Tbool -> false | _ -> true) -> Atom (Atom.mk_eq ra (Atom.type_of h1) h1 h2) | _, _ -> Form (Fapp (Fiff, [|lit_of_atom_form_lit rf t1; lit_of_atom_form_lit rf t2|])) }
-  /* This rule introduces lots of shift/reduce conflicts */
-  | EQ lit lit                                             { let t1 = $2 in let t2 = $3 in Form (Fapp (Fiff, [|t1; t2|])) }
+  | EQ name_term name_term                                 { let t1 = $2 in let t2 = $3 in match t1,t2 with | (decl1, Atom h1), (decl2, Atom h2) when (match Atom.type_of h1 with | SmtBtype.Tbool -> false | _ -> true) -> let decl = decl1 && decl2 in decl, Atom (Atom.mk_eq ra decl (Atom.type_of h1) h1 h2) | (decl1, t1), (decl2, t2) -> decl1 && decl2, Form (Fapp (Fiff, [|lit_of_atom_form_lit rf (decl1, t1); lit_of_atom_form_lit rf (decl2, t2)|])) }
+  | EQ nlit lit                                            { match $2, $3 with (decl1, t1), (decl2, t2) -> decl1 && decl2, Form (Fapp (Fiff, [|t1; t2|])) }
+  | EQ name_term nlit                                      { match $2, $3 with (decl1, t1), (decl2, t2) -> decl1 && decl2, Form (Fapp (Fiff, [|lit_of_atom_form_lit rf (decl1, t1); t2|])) }
   | LET LPAR bindlist RPAR name_term                       { $3; $5 }
-  | BINDVAR                                                { Hashtbl.find hlets $1 }
+  | BINDVAR                                                { true, Hashtbl.find hlets $1 }
+;
+
+blit:   
+  | name_term                                              { $1 } 
+  | LPAR NOT lit RPAR                                      { apply_dec (fun l -> Lit (Form.neg l)) $3 }
 ;
 
 bindlist:
-  | LPAR BINDVAR name_term RPAR                            { Hashtbl.add hlets $2 $3 }
-  | LPAR BINDVAR lit RPAR                                  { Hashtbl.add hlets $2 (Lit $3) }
-  | LPAR BINDVAR name_term RPAR bindlist                   { Hashtbl.add hlets $2 $3; $5 }
-  | LPAR BINDVAR lit RPAR bindlist                         { Hashtbl.add hlets $2 (Lit $3); $5 }
+  | LPAR BINDVAR blit RPAR	                           { Hashtbl.add hlets $2 (snd $3) }
+  | LPAR BINDVAR blit RPAR bindlist                        { Hashtbl.add hlets $2 (snd $3); $5 }
 
 args:
-  | name_term                                              { match $1 with Atom h -> [h] | _ -> assert false }
-  | name_term args                                         { match $1 with Atom h -> h::$2 | _ -> assert false }
+  | name_term                                              { match $1 with decl, Atom h -> [decl, h] | _ -> assert false }
+  | name_term args                                         { match $1 with decl, Atom h -> (decl, h)::$2 | _ -> assert false }
 ;
 
 clause_ids_params:
diff --git a/src/verit/veritSyntax.ml b/src/verit/veritSyntax.ml
index b598e2c..5d79016 100644
--- a/src/verit/veritSyntax.ml
+++ b/src/verit/veritSyntax.ml
@@ -203,16 +203,76 @@ let get_clause id =
 let add_clause id cl = Hashtbl.add clauses id cl
 let clear_clauses () = Hashtbl.clear clauses
 
-let mk_clause (id,typ,value,ids_params) =
+
+(* <ref_cl> maps solver integers to id integers. *)
+let ref_cl : (int, int) Hashtbl.t = Hashtbl.create 17
+let get_ref i = Hashtbl.find ref_cl i
+let add_ref i j = Hashtbl.add ref_cl i j
+let clear_ref () = Hashtbl.clear ref_cl
+
+(* Recognizing and modifying clauses depending on a forall_inst clause. *)
+                                 
+let rec fins_lemma ids_params =
+  match ids_params with
+    [] -> raise Not_found
+  | h :: t -> let cl_target = repr (get_clause h) in
+              match cl_target.kind with
+                Other (Forall_inst (lemma, _)) -> lemma
+              | _ -> fins_lemma t
+
+let rec find_remove_lemma lemma ids_params =
+  let eq_lemma h = eq_clause lemma (get_clause h) in
+  list_find_remove eq_lemma ids_params 
+
+(* Removes the lemma in a list of ids containing an instance of this lemma *)                   
+let rec merge ids_params =
+  let rest_opt = try let lemma = fins_lemma ids_params in
+                     let _, rest = find_remove_lemma lemma ids_params in
+                     Some rest
+                 with Not_found -> None in
+  match rest_opt with
+    None -> ids_params
+  | Some r -> merge r
+
+let to_add = ref []
+                     
+let rec mk_clause (id,typ,value,ids_params) =
   let kind =
     match typ with
+    | Tpbr ->
+       begin match ids_params with
+       | [id] ->
+          Same (get_clause id)
+       | _ -> failwith "unexpected form of tmp_betared" end
+    | Tpqt ->
+       begin match ids_params with
+       | [id] ->
+          Same (get_clause id)
+       | _ -> failwith "unexpected form of tmp_qnt_tidy" end
+    | Fins ->
+       begin match value, ids_params with
+        | [inst], [ref_th] when Form.is_pos inst ->
+           let cl_th = get_clause ref_th in
+           Other (Forall_inst (repr cl_th, inst))
+        | _ -> failwith "unexpected form of forall_inst" end
+    | Or ->
+       (match ids_params with
+        | [id_target] ->
+           let cl_target = get_clause id_target in
+           begin match cl_target.kind with
+           | Other (Forall_inst _) -> Same cl_target
+           | _ -> Other (ImmBuildDef cl_target) end
+        | _ -> assert false)
     (* Resolution *)
     | Reso ->
+       let ids_params = merge ids_params in
        (match ids_params with
         | cl1::cl2::q ->
            let res = {rc1 = get_clause cl1; rc2 = get_clause cl2; rtail = List.map get_clause q} in
            Res res
-        | _ -> assert false)
+        | [fins_id] -> Same (get_clause fins_id)
+        | [] -> assert false)
+
     (* Roots *)
     | Inpu -> Root
     (* Cnf conversion *)
@@ -238,7 +298,7 @@ let mk_clause (id,typ,value,ids_params) =
        (match value with
         | l::_ -> Other (BuildProj (l,1))
         | _ -> assert false)
-    | Nand | Or | Imp | Xor1 | Nxor1 | Equ2 | Nequ2 | Ite1 | Nite1 ->
+    | Nand | Imp | Xor1 | Nxor1 | Equ2 | Nequ2 | Ite1 | Nite1 ->
        (match ids_params with
         | [id] -> Other (ImmBuildDef (get_clause id))
         | _ -> assert false)
@@ -291,7 +351,6 @@ let mk_clause (id,typ,value,ids_params) =
     | Hole -> Other (SmtCertif.Hole (List.map get_clause ids_params, value))
     (* Not implemented *)
     | Deep -> failwith "VeritSyntax.ml: rule deep_res not implemented yet"
-    | Fins -> failwith "VeritSyntax.ml: rule forall_inst not implemented yet"
     | Eins -> failwith "VeritSyntax.ml: rule exists_inst not implemented yet"
     | Skea -> failwith "VeritSyntax.ml: rule skolem_ex_ax not implemented yet"
     | Skaa -> failwith "VeritSyntax.ml: rule skolem_all_ax not implemented yet"
@@ -300,11 +359,9 @@ let mk_clause (id,typ,value,ids_params) =
     | Tpne -> failwith "VeritSyntax.ml: rule tmp_nary_elim not implemented yet"
     | Tpie -> failwith "VeritSyntax.ml: rule tmp_ite_elim not implemented yet"
     | Tpma -> failwith "VeritSyntax.ml: rule tmp_macrosubst not implemented yet"
-    | Tpbr -> failwith "VeritSyntax.ml: rule tmp_betared not implemented yet"
     | Tpbe -> failwith "VeritSyntax.ml: rule tmp_bfun_elim not implemented yet"
     | Tpsc -> failwith "VeritSyntax.ml: rule tmp_sk_connector not implemented yet"
     | Tppp -> failwith "VeritSyntax.ml: rule tmp_pm_process not implemented yet"
-    | Tpqt -> failwith "VeritSyntax.ml: rule tmp_qnt_tidy not implemented yet"
     | Tpqs -> failwith "VeritSyntax.ml: rule tmp_qnt_simplify not implemented yet"
     | Tpsk -> failwith "VeritSyntax.ml: rule tmp_skolemize not implemented yet"
     | Subp -> failwith "VeritSyntax.ml: rule subproof not implemented yet"
@@ -323,12 +380,36 @@ type atom_form_lit =
   | Form of SmtAtom.Form.pform
   | Lit of SmtAtom.Form.t
 
+(* functions for applying on a pair with a boolean when the boolean indicates
+   if the entire term should be declared in the tables *)
 let lit_of_atom_form_lit rf = function
-  | Atom a -> Form.get rf (Fatom a)
-  | Form f -> Form.get rf f
-  | Lit l -> l
-
-let solver : (int,atom_form_lit) Hashtbl.t = Hashtbl.create 17
+  | decl, Atom a -> Form.get ~declare:decl rf (Fatom a)
+  | decl, Form f -> begin match f with
+                    | Fapp (Fforall _, _) when decl -> failwith "decl is true on a forall"
+                    | _ -> Form.get ~declare:decl rf f end
+  | decl, Lit l -> l
+
+let apply_dec f (decl, a) = decl, f a
+
+let rec list_dec = function
+  | [] -> true, []
+  | (decl_h, h) :: t ->
+     let decl_t, l_t = list_dec t in
+     decl_h && decl_t, h :: l_t
+    
+let apply_dec_atom f = function
+  | decl, Atom h -> decl, Atom (f decl h)
+  | _ -> assert false
+
+let apply_bdec_atom f o1 o2 =
+  match o1, o2 with
+  | (decl1, Atom h1), (decl2, Atom h2) ->
+     let decl = decl1 && decl2 in
+     decl, Atom (f decl h1 h2)
+  | _ -> assert false
+
+
+let solver : (int, (bool * atom_form_lit)) Hashtbl.t = Hashtbl.create 17
 let get_solver id =
   try Hashtbl.find solver id
   with | Not_found -> failwith ("VeritSyntax.get_solver : solver variable number "^(string_of_int id)^" not found\n")
@@ -349,18 +430,66 @@ let get_fun id =
 let add_fun id cl = Hashtbl.add funs id cl
 let clear_funs () = Hashtbl.clear funs
 
-
+let qvar_tbl : (string, SmtBtype.btype) Hashtbl.t = Hashtbl.create 10
+let find_opt_qvar s = try Some (Hashtbl.find qvar_tbl s)
+                      with Not_found -> None
+let add_qvar s bt = Hashtbl.add qvar_tbl s bt
+let clear_qvar () = Hashtbl.clear qvar_tbl
+
+let string_hform = Form.to_string ~pi:true (Atom.to_string ~pi:true )
+
+(* Finding the index of a root in <lsmt> modulo the <re_hash> function. 
+   This function is used by SmtTrace.order_roots *)
+let init_index lsmt re_hash =
+  let form_index_init_rank : (int, int) Hashtbl.t = Hashtbl.create 20 in
+  let add = Hashtbl.add form_index_init_rank in
+  let find = Hashtbl.find form_index_init_rank in
+  let rec walk rank = function
+    | [] -> ()
+    | h::t -> add (Form.to_lit h) rank;
+              walk (rank+1) t in
+  walk 1 lsmt;
+  fun hf -> let re_hf = re_hash hf in
+            try find (Form.to_lit re_hf)
+            with Not_found ->
+              let oc = open_out "/tmp/input_not_found.log" in
+              (List.map string_hform lsmt)
+              |> List.iter (Printf.fprintf oc "%s\n");
+              Printf.fprintf oc "\n%s\n" (string_hform re_hf);
+              flush oc; close_out oc;
+              failwith "not found: log available"
+
+let qf_to_add lr =
+  let is_forall l = match Form.pform l with
+    | Fapp (Fforall _, _) -> true
+    | _ -> false in
+  let rec qf_lemmas = function
+    | [] -> []
+    | ({value = Some [l]} as r)::t when not (is_forall l) ->
+       (Other (Qf_lemma (r, l)), r.value, r) :: qf_lemmas t
+    | _::t -> qf_lemmas t in
+  qf_lemmas lr
+                       
 let ra = Atom.create ()
 let rf = Form.create ()
+let ra' = Atom.create ()
+let rf' = Form.create ()
 
 let hlets : (string, atom_form_lit) Hashtbl.t = Hashtbl.create 17
 
+let clear_mk_clause () = 
+  to_add := [];
+  clear_ref ()
 
 let clear () =
+  clear_qvar ();
+  clear_mk_clause ();
   clear_clauses ();
   clear_solver ();
   clear_btypes ();
   clear_funs ();
   Atom.clear ra;
   Form.clear rf;
+  Atom.clear ra';
+  Form.clear rf';
   Hashtbl.clear hlets
diff --git a/src/verit/veritSyntax.mli b/src/verit/veritSyntax.mli
index c7bf659..27a7ee3 100644
--- a/src/verit/veritSyntax.mli
+++ b/src/verit/veritSyntax.mli
@@ -21,15 +21,30 @@ type typ = | Inpu | Deep | True | Fals | Andp | Andn | Orp | Orn | Xorp1 | Xorp2
 val get_clause : int -> SmtAtom.Form.t SmtCertif.clause
 val add_clause : int -> SmtAtom.Form.t SmtCertif.clause -> unit
 
+val add_ref : int -> int -> unit
+val get_ref : int -> int
+val to_add : (int * SmtAtom.Form.t list) list ref
+
 val mk_clause : SmtCertif.clause_id * typ * SmtAtom.Form.t list * SmtCertif.clause_id list -> SmtCertif.clause_id
 
 type atom_form_lit =
   | Atom of SmtAtom.Atom.t
   | Form of SmtAtom.Form.pform
   | Lit of SmtAtom.Form.t
-val lit_of_atom_form_lit : SmtAtom.Form.reify -> atom_form_lit -> SmtAtom.Form.t
-val get_solver : int -> atom_form_lit
-val add_solver : int -> atom_form_lit -> unit
+val lit_of_atom_form_lit : SmtAtom.Form.reify -> bool * atom_form_lit -> SmtAtom.Form.t
+
+val apply_dec_atom : (bool -> SmtAtom.hatom -> SmtAtom.hatom) ->
+                     bool * atom_form_lit -> bool * atom_form_lit
+val apply_bdec_atom :
+  (bool -> SmtAtom.Atom.t -> SmtAtom.Atom.t -> SmtAtom.Atom.t) ->
+  bool * atom_form_lit -> bool * atom_form_lit -> bool * atom_form_lit
+
+val apply_dec : ('a -> 'b) -> bool * 'a -> bool * 'b
+val list_dec : (bool * 'a) list -> bool * 'a list
+
+
+val get_solver : int -> bool * atom_form_lit
+val add_solver : int -> bool * atom_form_lit -> unit
 
 val get_btype : string -> SmtBtype.btype
 val add_btype : string -> SmtBtype.btype -> unit
@@ -37,8 +52,21 @@ val add_btype : string -> SmtBtype.btype -> unit
 val get_fun : string -> SmtAtom.indexed_op
 val add_fun : string -> SmtAtom.indexed_op -> unit
 
+val find_opt_qvar : string -> SmtBtype.btype option 
+val add_qvar : string -> SmtBtype.btype -> unit
+val clear_qvar : unit -> unit
+
+val string_hform : SmtAtom.Form.t -> string
+
+val init_index : SmtAtom.Form.t list -> (SmtAtom.Form.t -> SmtAtom.Form.t) ->
+                 SmtAtom.Form.t -> int
+
+val qf_to_add : SmtAtom.Form.t SmtCertif.clause list -> (SmtAtom.Form.t SmtCertif.clause_kind * SmtAtom.Form.t list option * SmtAtom.Form.t SmtCertif.clause) list
+                                     
 val ra : SmtAtom.Atom.reify_tbl
 val rf : SmtAtom.Form.reify
+val ra' : SmtAtom.Atom.reify_tbl
+val rf' : SmtAtom.Form.reify
 
 val hlets : (string, atom_form_lit) Hashtbl.t
 
diff --git a/src/versions/native/smtcoq_plugin_native.ml4 b/src/versions/native/smtcoq_plugin_native.ml4
index da0671e..f3c571c 100644
--- a/src/versions/native/smtcoq_plugin_native.ml4
+++ b/src/versions/native/smtcoq_plugin_native.ml4
@@ -58,6 +58,14 @@ TACTIC EXTEND Tactic_zchaff
 | [ "zchaff" ] -> [ Zchaff.tactic () ]
 END
 
+let lemmas_list = ref []
+
+VERNAC COMMAND EXTEND Add_lemma
+| [ "Add_lemmas" constr_list(lems) ] -> [ lemmas_list := lems @ !lemmas_list ]
+| [ "Clear_lemmas" ] -> [ lemmas_list := [] ]
+END
+
+
 TACTIC EXTEND Tactic_verit
-| [ "verit" ] -> [ Verit.tactic () ]
+| [ "verit_base" constr_list(lpl) ] -> [ Verit.tactic lpl !lemmas_list ]
 END
diff --git a/src/versions/native/structures.ml b/src/versions/native/structures.ml
index 8db91fd..06ca01c 100644
--- a/src/versions/native/structures.ml
+++ b/src/versions/native/structures.ml
@@ -108,6 +108,12 @@ let pr_constr_env = Printer.pr_constr_env
 
 let lift = Term.lift
 
+let destruct_rel_decl (n, _, t) = n, t
+
+let interp_constr env sigma = Constrintern.interp_constr sigma env
+
+type constr_expr = Topconstr.constr_expr
+                            
 let tclTHEN = Tacticals.tclTHEN
 let tclTHENLAST = Tacticals.tclTHENLAST
 let assert_before = Tactics.assert_tac
diff --git a/src/versions/native/structures.mli b/src/versions/native/structures.mli
index ba095c8..7c5edfd 100644
--- a/src/versions/native/structures.mli
+++ b/src/versions/native/structures.mli
@@ -23,6 +23,9 @@ val extern_constr : Term.constr -> Topconstr.constr_expr
 val vernacentries_interp : Topconstr.constr_expr -> unit
 val pr_constr_env : Environ.env -> Term.constr -> Pp.std_ppcmds
 val lift : int -> Term.constr -> Term.constr
+val destruct_rel_decl : Term.rel_declaration -> Names.name * Term.constr
+val interp_constr : Environ.env -> Evd.evar_map -> Topconstr.constr_expr -> Term.constr
+type constr_expr = Topconstr.constr_expr
 val tclTHEN : Proof_type.tactic -> Proof_type.tactic -> Proof_type.tactic
 val tclTHENLAST : Proof_type.tactic -> Proof_type.tactic -> Proof_type.tactic
 val assert_before : Names.name -> Term.types -> Proof_type.tactic
diff --git a/src/versions/standard/g_smtcoq_standard.ml4 b/src/versions/standard/g_smtcoq_standard.ml4
index ab097a1..b8ea279 100644
--- a/src/versions/standard/g_smtcoq_standard.ml4
+++ b/src/versions/standard/g_smtcoq_standard.ml4
@@ -57,6 +57,14 @@ TACTIC EXTEND Tactic_zchaff
 | [ "zchaff" ] -> [ Zchaff.tactic () ]
 END
 
+let lemmas_list = ref []
+
+VERNAC COMMAND EXTEND Add_lemma CLASSIFIED AS SIDEFF
+| [ "Add_lemmas" constr_list(lems) ] -> [ lemmas_list := lems @ !lemmas_list ]
+| [ "Clear_lemmas" ] -> [ lemmas_list := [] ]
+END
+
+
 TACTIC EXTEND Tactic_verit
-| [ "verit" ] -> [ Verit.tactic () ]
+| [ "verit_base" constr_list(lpl) ] -> [ Verit.tactic lpl !lemmas_list ]
 END
diff --git a/src/versions/standard/structures.ml b/src/versions/standard/structures.ml
index ec899d8..be63a80 100644
--- a/src/versions/standard/structures.ml
+++ b/src/versions/standard/structures.ml
@@ -135,6 +135,15 @@ let pr_constr_env env = Printer.pr_constr_env env Evd.empty
 
 let lift = Vars.lift
 
+type rel_decl = Context.Rel.Declaration.t
+
+let destruct_rel_decl r = Context.Rel.Declaration.get_name r,
+                          Context.Rel.Declaration.get_type r
+
+type constr_expr = Constrexpr.constr_expr
+                        
+let interp_constr env sigma t = Constrintern.interp_constr env sigma t |> fst
+                        
 let tclTHEN = Tacticals.New.tclTHEN
 let tclTHENLAST = Tacticals.New.tclTHENLAST
 let assert_before = Tactics.assert_before
diff --git a/src/versions/standard/structures.mli b/src/versions/standard/structures.mli
index 86ceb3e..600503d 100644
--- a/src/versions/standard/structures.mli
+++ b/src/versions/standard/structures.mli
@@ -37,6 +37,10 @@ val extern_constr : Term.constr -> Constrexpr.constr_expr
 val vernacentries_interp : Constrexpr.constr_expr -> unit
 val pr_constr_env : Environ.env -> Term.constr -> Pp.std_ppcmds
 val lift : int -> Constr.constr -> Constr.constr
+type rel_decl = Context.Rel.Declaration.t                                     
+val destruct_rel_decl : rel_decl -> Names.Name.t * Constr.t
+type constr_expr = Constrexpr.constr_expr
+val interp_constr : Environ.env -> Evd.evar_map -> Constrexpr.constr_expr -> Term.constr
 val tclTHEN :
   unit Proofview.tactic -> unit Proofview.tactic -> unit Proofview.tactic
 val tclTHENLAST :
diff --git a/src/zchaff/satParser.ml b/src/zchaff/satParser.ml
index 79d0b14..9e624ed 100644
--- a/src/zchaff/satParser.ml
+++ b/src/zchaff/satParser.ml
@@ -26,7 +26,7 @@ let buff_length = 1024
 let open_file s name =
   try
     let in_channel = open_in name in
-    let buff = String.create buff_length in
+    let buff = Bytes.create buff_length in
     let buff_end = input in_channel buff 0 buff_length in
     { buff = buff; curr_char = 0; buff_end = buff_end; in_ch = in_channel }
   with _ ->
@@ -83,7 +83,7 @@ let skip_string lb s =
 let match_string lb s =
   if not (skip_string lb s) then raise (Invalid_argument ("match_string "^s))
 
-let aux_buff = String.create buff_length
+let aux_buff = Bytes.create buff_length
 let aux_be = ref 0
 let aux_pi = ref 0
 let aux_cc = ref 0
diff --git a/src/zchaff/zchaff.ml b/src/zchaff/zchaff.ml
index bfa1949..928dd8d 100644
--- a/src/zchaff/zchaff.ml
+++ b/src/zchaff/zchaff.ml
@@ -49,6 +49,7 @@ let string_of_op = function
   | Fiff -> "iff"
   | Fite -> "ite"
   | Fnot2 i -> "!"^string_of_int i
+  | Fforall _ -> assert false
 
 let rec pp_form fmt l =
   Format.fprintf fmt "(#%i %a %a)" (Form.to_lit l)pp_sign l pp_pform (Form.pform l)
@@ -204,7 +205,7 @@ let parse_certif dimacs trace fdimacs ftrace =
   let _ = declare_constant dimacs (DefinitionEntry ce1, IsDefinition Definition) in
 
   let max_id, confl = import_cnf_trace reloc ftrace first last in
-  let (tres,_,_) = SmtTrace.to_coq (fun _ -> assert false) (fun _ -> assert false) certif_ops confl in
+  let (tres,_,_) = SmtTrace.to_coq (fun _ -> assert false) (fun _ -> assert false) certif_ops confl None in
   let certif =
    mklApp cCertif [|mkInt (max_id + 1); tres;mkInt (get_pos confl)|] in
   let ce2 = Structures.mkUConst certif in
@@ -223,11 +224,11 @@ let theorems interp name fdimacs ftrace =
 
   let max_id, confl = import_cnf_trace reloc ftrace first last in
   let (tres,_,_) =
-    SmtTrace.to_coq (fun _ -> assert false) (fun _ -> assert false) certif_ops confl in
+    SmtTrace.to_coq (fun _ -> assert false) (fun _ -> assert false) certif_ops confl None in
   let certif =
    mklApp cCertif [|mkInt (max_id + 1);tres;mkInt (get_pos confl)|] in
 
-  let theorem_concl = mklApp cnot [|mklApp cis_true [|interp d first last|] |] in
+  let theorem_concl = mklApp cis_true [|mklApp cnegb [|interp d first last|] |] in
   let vtype = Term.mkProd(Names.Anonymous, Lazy.force cint, Lazy.force cbool) in
   let theorem_type =
     Term.mkProd (mkName "v", vtype, theorem_concl) in
@@ -267,7 +268,7 @@ let checker fdimacs ftrace =
 
   let max_id, confl = import_cnf_trace reloc ftrace first last in
   let (tres,_,_) =
-    SmtTrace.to_coq (fun _ -> assert false) (fun _ -> assert false) certif_ops confl in
+    SmtTrace.to_coq (fun _ -> assert false) (fun _ -> assert false) certif_ops confl None in
   let certif =
     mklApp cCertif [|mkInt (max_id + 1);tres;mkInt (get_pos confl)|] in
 
@@ -340,7 +341,8 @@ let call_zchaff nvars root =
   let exit_code2 = Sys.command command2 in
   if exit_code2 <> 0 then
       failwith ("Zchaff.call_zchaff: command " ^ command2 ^
-                  " exited with code " ^ (string_of_int exit_code2));
+                  " exited with code " ^ (string_of_int exit_code2) ^
+        "\nDid you forget to turn on Zchaff proof production?" );
   (* import_cnf_trace reloc logfilename root last  *)
   (reloc, resfilename, logfilename, last)
 
@@ -366,7 +368,7 @@ let build_body reify_atom reify_form l b (max_id, confl) =
   let tvar = Atom.interp_tbl reify_atom in
   let _, tform = Form.interp_tbl reify_form in
   let (tres,_,_) =
-    SmtTrace.to_coq Form.to_coq (fun _ -> assert false) certif_ops confl in
+    SmtTrace.to_coq Form.to_coq (fun _ -> assert false) certif_ops confl None in
   let certif =
     mklApp cCertif [|mkInt (max_id + 1);tres;mkInt (get_pos confl)|] in
   let vtvar = Term.mkRel 3 in
@@ -397,7 +399,7 @@ let build_body_eq reify_atom reify_form l1 l2 l (max_id, confl) =
   let tvar = Atom.interp_tbl reify_atom in
   let _, tform = Form.interp_tbl reify_form in
   let (tres,_,_) =
-    SmtTrace.to_coq Form.to_coq (fun _ -> assert false) certif_ops confl in
+    SmtTrace.to_coq Form.to_coq (fun _ -> assert false) certif_ops confl None in
   let certif =
     mklApp cCertif [|mkInt (max_id + 1);tres;mkInt (get_pos confl)|] in
   let vtvar = Term.mkRel 3 in
diff --git a/src/zchaff/zchaff.mli b/src/zchaff/zchaff.mli
index 7fbaabd..6a873ec 100644
--- a/src/zchaff/zchaff.mli
+++ b/src/zchaff/zchaff.mli
@@ -53,7 +53,7 @@ val certif_ops :
   Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
   Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
   Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
-  Term.constr lazy_t
+  Term.constr lazy_t * Term.constr lazy_t
 val ccertif : Term.constr lazy_t
 val cCertif : Term.constr lazy_t
 val cchecker_b_correct : Term.constr lazy_t