Made SmtCommands independent from VeritSyntax

Made lfsc/* mostly independent from VeritSyntax

21 files changed, 240 insertions, 298 deletions

diff --git a/src/lfsc/lfsc.ml b/src/lfsc/lfsc.ml
index a11139d..7938885 100644
--- a/src/lfsc/lfsc.ml
+++ b/src/lfsc/lfsc.ml
@@ -134,7 +134,9 @@ let import_trace_from_file first filename =
 
 let clear_all () =
   SmtTrace.clear ();
+  SmtMaps.clear ();
   VeritSyntax.clear ();
+  Tosmtcoq.clear ();
   C.clear ()
 
 
@@ -142,8 +144,8 @@ let import_all fsmt fproof =
   clear_all ();
   let rt = SmtBtype.create () in
   let ro = Op.create () in
-  let ra = VeritSyntax.ra in
-  let rf = VeritSyntax.rf in
+  let ra = Tosmtcoq.ra in
+  let rf = Tosmtcoq.rf in
   let roots = Smtlib2_genConstr.import_smtlib2 rt ro ra rf fsmt in
   let (max_id, confl) = import_trace_from_file None fproof in
   (rt, ro, ra, rf, roots, max_id, confl)
@@ -362,13 +364,13 @@ let call_cvc4 env rt ro ra rf root _ =
 
   List.iter (fun (i,t) ->
     let s = "Tindex_"^(string_of_int i) in
-    VeritSyntax.add_btype s (SmtBtype.Tindex t);
+    SmtMaps.add_btype s (SmtBtype.Tindex t);
     declare_sort cvc4 s 0;
   ) (SmtBtype.to_list rt);
   
   List.iter (fun (i,cod,dom,op) ->
     let s = "op_"^(string_of_int i) in
-    VeritSyntax.add_fun s op;
+    SmtMaps.add_fun s op;
     let args =
       Array.fold_right
         (fun t acc -> asprintf "%a" SmtBtype.to_smt t :: acc) cod [] in
@@ -376,7 +378,7 @@ let call_cvc4 env rt ro ra rf root _ =
     declare_fun cvc4 s args ret
   ) (Op.to_list ro);
 
-  assume cvc4 (asprintf "%a" (Form.to_smt Atom.to_smt) fl);
+  assume cvc4 (asprintf "%a" (Form.to_smt ~debug:false) fl);
 
   let proof =
     match check_sat cvc4 with
@@ -407,13 +409,13 @@ let export out_channel rt ro l =
 
   List.iter (fun (i,t) ->
     let s = "Tindex_"^(string_of_int i) in
-    VeritSyntax.add_btype s (SmtBtype.Tindex t);
+    SmtMaps.add_btype s (SmtBtype.Tindex t);
     fprintf fmt "(declare-sort %s 0)@." s
   ) (SmtBtype.to_list rt);
 
   List.iter (fun (i,cod,dom,op) ->
     let s = "op_"^(string_of_int i) in
-    VeritSyntax.add_fun s op;
+    SmtMaps.add_fun s op;
     fprintf fmt "(declare-fun %s (" s;
     let is_first = ref true in
     Array.iter (fun t ->
@@ -424,7 +426,7 @@ let export out_channel rt ro l =
   ) (Op.to_list ro);
 
   fprintf fmt "(assert %a)@\n(check-sat)@\n(exit)@."
-    (Form.to_smt Atom.to_smt) l
+    (Form.to_smt ~debug:false) l
 
 
 
@@ -488,14 +490,12 @@ let tactic_gen vm_cast =
   clear_all ();
   let rt = SmtBtype.create () in
   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 ra = Tosmtcoq.ra in
+  let rf = Tosmtcoq.rf in
+  let ra' = Tosmtcoq.ra in
+  let rf' = Tosmtcoq.rf in
   SmtCommands.tactic call_cvc4 cvc4_logic rt ro ra rf ra' rf' vm_cast [] []
-  (* let ra = VeritSyntax.ra in
-   * let rf = VeritSyntax.rf in
-   * (\* Currently, quantifiers are not handled by the cvc4 tactic: we pass
+  (* (\* Currently, quantifiers are not handled by the cvc4 tactic: we pass
    *    the same ra and rf twice to have everything reifed *\)
    * SmtCommands.tactic call_cvc4 cvc4_logic rt ro ra rf ra rf vm_cast [] [] *)
 let tactic () = tactic_gen vm_cast_true
diff --git a/src/lfsc/tosmtcoq.ml b/src/lfsc/tosmtcoq.ml
index f520ba7..6382e9e 100644
--- a/src/lfsc/tosmtcoq.ml
+++ b/src/lfsc/tosmtcoq.ml
@@ -12,18 +12,20 @@
 
 open SmtAtom
 open SmtForm
-open VeritSyntax
 open Ast
 open Builtin
 open Format
 open Translator_sig
 open SmtBtype
 
+let ra = Atom.create ()
+let rf = Form.create ()
+
 type lit = SmtAtom.Form.t
 
 type clause = lit list
 
-let lit_of_atom_form_lit rf af = lit_of_atom_form_lit rf (true, af)
+let lit_of_atom_form_lit rf af = Form.lit_of_atom_form_lit rf (true, af)
 
 let show_veritproof =
   try ignore (Sys.getenv "DONTSHOWVERIT"); false
@@ -213,44 +215,44 @@ let rec const_bv_aux acc t = match name t with
 
 let const_bv t =
   let bv_list = const_bv_aux [] t in
-  Atom (Atom.mk_bvconst ra bv_list)
+  Form.Atom (Atom.mk_bvconst ra bv_list)
 
 
 let rec term_smtcoq_old t =
   match value t with
-  | Const {sname=Name n} when n == H.ttrue -> Form Form.pform_true
-  | Const {sname=Name n} when n == H.tfalse -> Form Form.pform_false
+  | Const {sname=Name n} when n == H.ttrue -> Form.Form Form.pform_true
+  | Const {sname=Name n} when n == H.tfalse -> Form.Form Form.pform_false
   | Const {sname=Name n} when n == H.bvn -> const_bv t
   | Const {sname=Name n} ->
     begin
       try
         term_smtcoq  (HS.find alias_tbl n)
       with Not_found ->
-        Atom (Atom.get ra (Aapp (get_fun (Hstring.view n),[||])))
+        Form.Atom (Atom.get ra (Aapp (SmtMaps.get_fun (Hstring.view n),[||])))
     end
-  | Int bi -> Atom (Atom.hatom_Z_of_bigint ra bi)
+  | Int bi -> Form.Atom (Atom.hatom_Z_of_bigint ra bi)
   | App _ ->
     begin match app_name t with
       | Some (n, [f]) when n == H.not_ ->
-        Lit (Form.neg (lit_of_atom_form_lit rf (term_smtcoq f)))
-      | Some (n, args) when n == H.and_ -> Form (Fapp (Fand, args_smtcoq args))
-      | Some (n, args) when n == H.or_ -> Form (Fapp (For, args_smtcoq args))
-      | Some (n, args) when n == H.impl_ -> Form (Fapp (Fimp, args_smtcoq args))
-      | Some (n, args) when n == H.xor_ -> Form (Fapp (Fxor, args_smtcoq args))
+        Form.Lit (Form.neg (lit_of_atom_form_lit rf (term_smtcoq f)))
+      | Some (n, args) when n == H.and_ -> Form.Form (Fapp (Fand, args_smtcoq args))
+      | Some (n, args) when n == H.or_ -> Form.Form (Fapp (For, args_smtcoq args))
+      | Some (n, args) when n == H.impl_ -> Form.Form (Fapp (Fimp, args_smtcoq args))
+      | Some (n, args) when n == H.xor_ -> Form.Form (Fapp (Fxor, args_smtcoq args))
       | Some (n, args) when n == H.ite || n == H.ifte_ ->
-        Form (Fapp (Fite, args_smtcoq args))
-      | Some (n, args) when n == H.iff -> Form (Fapp (Fiff, args_smtcoq args))
+        Form.Form (Fapp (Fite, args_smtcoq args))
+      | Some (n, args) when n == H.iff -> Form.Form (Fapp (Fiff, args_smtcoq args))
       | Some (n, [_; a; b]) when n == H.eq ->
         let h1, h2 = term_smtcoq_atom a, term_smtcoq_atom b in
-        Atom (Atom.mk_eq ra (Atom.type_of h1) h1 h2)
+        Form.Atom (Atom.mk_eq ra (Atom.type_of h1) h1 h2)
       | Some (n, _) when n == H.apply -> uncurry [] t
       | Some (n, [p]) when n == H.p_app -> term_smtcoq p
       | Some (n, [{value = Int bi}]) when n == H.a_int ->
-        Atom (Atom.hatom_Z_of_bigint ra bi)
+        Form.Atom (Atom.hatom_Z_of_bigint ra bi)
       | Some (n, [ni]) when n == H.a_int ->
         begin match app_name ni with
           | Some (n, [{value = Int bi}]) when n == H.uminus ->
-            Atom (Atom.hatom_Z_of_bigint ra (Big_int.minus_big_int bi))
+            Form.Atom (Atom.hatom_Z_of_bigint ra (Big_int.minus_big_int bi))
           | _ -> assert false
         end
       | Some (n, [_; v]) when n == H.a_var_bv -> term_smtcoq v
@@ -259,83 +261,83 @@ let rec term_smtcoq_old t =
       | Some (b, [a; {value = Int n}]) when b == H.bitof ->
          (let ha = term_smtcoq_atom a in
           match Atom.type_of ha with
-            | TBV s -> Atom (Atom.mk_bitof ra s (Big_int.int_of_big_int n) ha)
+            | TBV s -> Form.Atom (Atom.mk_bitof ra s (Big_int.int_of_big_int n) ha)
             | _ -> assert false)
       | Some (n, [_; a; bb]) when n == H.bblast_term ->
-        Form (FbbT ((term_smtcoq_atom a), bblt_lits [] bb))
+        Form.Form (FbbT ((term_smtcoq_atom a), bblt_lits [] bb))
       | Some (n, [_; a]) when n == H.bvnot ->
          (let ha = term_smtcoq_atom a in
           match Atom.type_of ha with
-            | TBV s -> Atom (Atom.mk_bvnot ra s ha)
+            | TBV s -> Form.Atom (Atom.mk_bvnot ra s ha)
             | _ -> assert false)
       | Some (n, [_; a]) when n == H.bvneg ->
          (let ha = term_smtcoq_atom a in
           match Atom.type_of ha with
-            | TBV s -> Atom (Atom.mk_bvneg ra s ha)
+            | TBV s -> Form.Atom (Atom.mk_bvneg ra s ha)
             | _ -> assert false)
       | Some (n, [_; a; b]) when n == H.bvand ->
          (let ha = term_smtcoq_atom a in
           let hb = term_smtcoq_atom b in
           match Atom.type_of ha with
-            | TBV s -> Atom (Atom.mk_bvand ra s ha hb)
+            | TBV s -> Form.Atom (Atom.mk_bvand ra s ha hb)
             | _ -> assert false)
       | Some (n, [_; a; b]) when n == H.bvor ->
          (let ha = term_smtcoq_atom a in
           let hb = term_smtcoq_atom b in
           match Atom.type_of ha with
-            | TBV s -> Atom (Atom.mk_bvor ra s ha hb)
+            | TBV s -> Form.Atom (Atom.mk_bvor ra s ha hb)
             | _ -> assert false)
       | Some (n, [_; a; b]) when n == H.bvxor ->
          (let ha = term_smtcoq_atom a in
           let hb = term_smtcoq_atom b in
           match Atom.type_of ha with
-            | TBV s -> Atom (Atom.mk_bvxor ra s ha hb)
+            | TBV s -> Form.Atom (Atom.mk_bvxor ra s ha hb)
             | _ -> assert false)
       | Some (n, [_; a; b]) when n == H.bvadd ->
          (let ha = term_smtcoq_atom a in
           let hb = term_smtcoq_atom b in
           match Atom.type_of ha with
-            | TBV s -> Atom (Atom.mk_bvadd ra s ha hb)
+            | TBV s -> Form.Atom (Atom.mk_bvadd ra s ha hb)
             | _ -> assert false)
       | Some (n, [_; a; b]) when n == H.bvmul ->
          (let ha = term_smtcoq_atom a in
           let hb = term_smtcoq_atom b in
           match Atom.type_of ha with
-            | TBV s -> Atom (Atom.mk_bvmult ra s ha hb)
+            | TBV s -> Form.Atom (Atom.mk_bvmult ra s ha hb)
             | _ -> assert false)
       | Some (n, [_; a; b]) when n == H.bvult ->
          (let ha = term_smtcoq_atom a in
           let hb = term_smtcoq_atom b in
           match Atom.type_of ha with
-            | TBV s -> Atom (Atom.mk_bvult ra s ha hb)
+            | TBV s -> Form.Atom (Atom.mk_bvult ra s ha hb)
             | _ -> assert false)
       | Some (n, [_; a; b]) when n == H.bvslt ->
          (let ha = term_smtcoq_atom a in
           let hb = term_smtcoq_atom b in
           match Atom.type_of ha with
-            | TBV s -> Atom (Atom.mk_bvslt ra s ha hb)
+            | TBV s -> Form.Atom (Atom.mk_bvslt ra s ha hb)
             | _ -> assert false)
       | Some (n, [_; a; b]) when n == H.bvule ->
         (let ha = term_smtcoq_atom a in
          let hb = term_smtcoq_atom b in
          match Atom.type_of ha with
          | TBV s ->
-           let a = Atom (Atom.mk_bvult ra s hb ha) in
-           Lit (Form.neg (lit_of_atom_form_lit rf a))
+           let a = Form.Atom (Atom.mk_bvult ra s hb ha) in
+           Form.Lit (Form.neg (lit_of_atom_form_lit rf a))
          | _ -> assert false)
       | Some (n, [_; a; b]) when n == H.bvsle ->
         (let ha = term_smtcoq_atom a in
          let hb = term_smtcoq_atom b in
          match Atom.type_of ha with
          | TBV s ->
-           let a = Atom (Atom.mk_bvslt ra s hb ha) in
-           Lit (Form.neg (lit_of_atom_form_lit rf a))
+           let a = Form.Atom (Atom.mk_bvslt ra s hb ha) in
+           Form.Lit (Form.neg (lit_of_atom_form_lit rf a))
          | _ -> assert false)         
       | Some (n, [_; _; _; a; b]) when n == H.concat ->
          (let ha = term_smtcoq_atom a in
           let hb = term_smtcoq_atom b in
           match Atom.type_of ha, Atom.type_of hb with
-            | TBV s1, TBV s2 -> Atom (Atom.mk_bvconcat ra s1 s2 ha hb)
+            | TBV s1, TBV s2 -> Form.Atom (Atom.mk_bvconcat ra s1 s2 ha hb)
             | _ -> assert false)
       | Some (n, [_; {value = Int bj}; {value = Int bi}; _; a])
         when n == H.extract ->
@@ -343,51 +345,51 @@ let rec term_smtcoq_old t =
          let i = Big_int.int_of_big_int bi in
          let j = Big_int.int_of_big_int bj in
           match Atom.type_of ha with
-            | TBV s -> Atom (Atom.mk_bvextr ra ~s ~i ~n:(j-i+1) ha)
+            | TBV s -> Form.Atom (Atom.mk_bvextr ra ~s ~i ~n:(j-i+1) ha)
             | _ -> assert false)
       | Some (n, [_; {value = Int bi}; _; a])
         when n == H.zero_extend ->
         (let ha = term_smtcoq_atom a in
          let n = Big_int.int_of_big_int bi in
           match Atom.type_of ha with
-            | TBV s -> Atom (Atom.mk_bvzextn ra ~s ~n ha)
+            | TBV s -> Form.Atom (Atom.mk_bvzextn ra ~s ~n ha)
             | _ -> assert false)
       | Some (n, [_; {value = Int bi}; _; a])
         when n == H.sign_extend ->
         (let ha = term_smtcoq_atom a in
          let n = Big_int.int_of_big_int bi in
           match Atom.type_of ha with
-            | TBV s -> Atom (Atom.mk_bvsextn ra ~s ~n ha)
+            | TBV s -> Form.Atom (Atom.mk_bvsextn ra ~s ~n ha)
             | _ -> assert false)
       | Some (n, [_; a; b]) when n == H.bvshl ->
          (let ha = term_smtcoq_atom a in
           let hb = term_smtcoq_atom b in
           match Atom.type_of ha with
-            | TBV s -> Atom (Atom.mk_bvshl ra s ha hb)
+            | TBV s -> Form.Atom (Atom.mk_bvshl ra s ha hb)
             | _ -> assert false)
       | Some (n, [_; a; b]) when n == H.bvlshr ->
          (let ha = term_smtcoq_atom a in
           let hb = term_smtcoq_atom b in
           match Atom.type_of ha with
-            | TBV s -> Atom (Atom.mk_bvshr ra s ha hb)
+            | TBV s -> Form.Atom (Atom.mk_bvshr ra s ha hb)
             | _ -> assert false)
 
       | Some (n, [a; b]) when n == H.lt_Int ->
-        Atom (Atom.mk_lt ra (term_smtcoq_atom a) (term_smtcoq_atom b))
+        Form.Atom (Atom.mk_lt ra (term_smtcoq_atom a) (term_smtcoq_atom b))
       | Some (n, [a; b]) when n == H.le_Int ->
-        Atom (Atom.mk_le ra (term_smtcoq_atom a) (term_smtcoq_atom b))
+        Form.Atom (Atom.mk_le ra (term_smtcoq_atom a) (term_smtcoq_atom b))
       | Some (n, [a; b]) when n == H.gt_Int ->
-        Atom (Atom.mk_gt ra (term_smtcoq_atom a) (term_smtcoq_atom b))
+        Form.Atom (Atom.mk_gt ra (term_smtcoq_atom a) (term_smtcoq_atom b))
       | Some (n, [a; b]) when n == H.ge_Int ->
-        Atom (Atom.mk_ge ra (term_smtcoq_atom a) (term_smtcoq_atom b))
+        Form.Atom (Atom.mk_ge ra (term_smtcoq_atom a) (term_smtcoq_atom b))
       | Some (n, [a; b]) when n == H.plus_Int ->
-        Atom (Atom.mk_plus ra (term_smtcoq_atom a) (term_smtcoq_atom b))
+        Form.Atom (Atom.mk_plus ra (term_smtcoq_atom a) (term_smtcoq_atom b))
       | Some (n, [a; b]) when n == H.minus_Int ->
-        Atom (Atom.mk_minus ra (term_smtcoq_atom a) (term_smtcoq_atom b))
+        Form.Atom (Atom.mk_minus ra (term_smtcoq_atom a) (term_smtcoq_atom b))
       | Some (n, [a; b]) when n == H.times_Int ->
-        Atom (Atom.mk_mult ra (term_smtcoq_atom a) (term_smtcoq_atom b))
+        Form.Atom (Atom.mk_mult ra (term_smtcoq_atom a) (term_smtcoq_atom b))
       | Some (n, [a]) when n == H.uminus_Int ->
-        Atom (Atom.mk_opp ra (term_smtcoq_atom a))
+        Form.Atom (Atom.mk_opp ra (term_smtcoq_atom a))
       | Some (n, _) ->
         Format.eprintf "\nTerm: %a\n@." print_term t;
         failwith ("LFSC function symbol "^Hstring.view n^" not supported.")
@@ -416,7 +418,7 @@ and term_smtcoq t =
 
 
 and term_smtcoq_atom a = match term_smtcoq a with
-  | Atom h -> h
+  | Form.Atom h -> h
   | _ ->  assert false
 
 and args_smtcoq args =
@@ -428,21 +430,21 @@ and uncurry acc t = match app_name t, acc with
     uncurry (term_smtcoq_atom a :: acc) f
   | Some (n, [_; _]) , [h1; h2] when n == H.read ->
     (match Atom.type_of h1 with
-     | TFArray (ti,te) -> Atom (Atom.mk_select ra ti te h1 h2)
+     | TFArray (ti,te) -> Form.Atom (Atom.mk_select ra ti te h1 h2)
      | _ -> assert false)
   | Some (n, [_; _]) , [h1; h2; h3] when n == H.write ->
     (match Atom.type_of h1 with
-     | TFArray (ti,te) -> Atom (Atom.mk_store ra ti te h1 h2 h3)
+     | TFArray (ti,te) -> Form.Atom (Atom.mk_store ra ti te h1 h2 h3)
      | _ -> assert false)
   | Some (n, [_; _]) , [h1; h2] when n == H.diff ->
     (match Atom.type_of h1 with
-     | TFArray (ti,te) -> Atom (Atom.mk_diffarray ra ti te h1 h2)
+     | TFArray (ti,te) -> Form.Atom (Atom.mk_diffarray ra ti te h1 h2)
      | _ -> assert false)
   | None, _ ->
     (match name t with
      | Some n ->
        let args = Array.of_list acc in
-       Atom (Atom.get ra (Aapp (get_fun (Hstring.view n), args)))
+       Form.Atom (Atom.get ra (Aapp (SmtMaps.get_fun (Hstring.view n), args)))
      | _ -> assert false)
   | _ ->
     eprintf "uncurry fail: %a@." Ast.print_term t;
@@ -484,7 +486,7 @@ let to_clause = clause_smtcoq []
 
 let print_clause fmt cl =
   fprintf fmt "(";
-  List.iter (fprintf fmt "%a " (Form.to_smt Atom.to_smt)) cl;
+  List.iter (fprintf fmt "%a " (Form.to_smt ~debug:false)) cl;
   fprintf fmt ")"
 
 
@@ -581,6 +583,8 @@ let register_decl_id name id =
 
 
 let clear () =
+  Atom.clear ra;
+  Form.clear rf;
   HCl.clear clauses_ids;
   Hashtbl.clear ids_clauses;
   HT.clear propvars;
diff --git a/src/lfsc/tosmtcoq.mli b/src/lfsc/tosmtcoq.mli
index b0d980b..34d3119 100644
--- a/src/lfsc/tosmtcoq.mli
+++ b/src/lfsc/tosmtcoq.mli
@@ -11,3 +11,6 @@
 
 
 include Translator_sig.S
+
+val ra : SmtAtom.Atom.reify_tbl
+val rf : SmtAtom.Form.reify
diff --git a/src/lfsc/translator_sig.mli b/src/lfsc/translator_sig.mli
index 66005f3..0937aef 100644
--- a/src/lfsc/translator_sig.mli
+++ b/src/lfsc/translator_sig.mli
@@ -19,7 +19,7 @@ open Ast
 open Format
 
 
-(** The type of destination rules that are currently supported byt the
+(** The type of destination rules that are currently supported by the
     converter *)
 type rule =
   | Reso
diff --git a/src/smtlib2/smtlib2_genConstr.ml b/src/smtlib2/smtlib2_genConstr.ml
index 64f0b20..f938671 100644
--- a/src/smtlib2/smtlib2_genConstr.ml
+++ b/src/smtlib2/smtlib2_genConstr.ml
@@ -45,7 +45,7 @@ let string_type s =
   | "Array" -> (function [ti;te] -> TFArray (ti, te) | _ -> assert false)
   | _ ->
     try Scanf.sscanf s "BitVec_%d%!" (fun size -> fun _ -> TBV size)
-    with _ -> fun _ -> VeritSyntax.get_btype s
+    with _ -> fun _ -> SmtMaps.get_btype s
 
 let sort_of_string s = string_type s
 
@@ -96,30 +96,33 @@ let rec sort_of_sort = function
     sort_of_string (string_of_identifier id) (List.map sort_of_sort l)
 
 
-let declare_sort rt sym =
-  let s = string_of_symbol sym in
+let declare_sort_from_name rt s =
   let cons_t = Structures.declare_new_type (Structures.mkId ("Smt_sort_"^s)) in
   let compdec_type = mklApp cCompDec [| cons_t |] in
   let compdec_var =
     Structures.declare_new_variable (Structures.mkId ("CompDec_"^s)) compdec_type in
   let ce = mklApp cTyp_compdec [|cons_t; compdec_var|] in
   let res = SmtBtype.declare rt cons_t ce in
-  VeritSyntax.add_btype s res;
+  SmtMaps.add_btype s res;
   res
 
+let declare_sort rt sym = declare_sort_from_name rt (string_of_symbol sym)
 
-let declare_fun rt ro sym arg cod =
-  let s = string_of_symbol sym in
-  let tyl = List.map sort_of_sort arg in
-  let ty = sort_of_sort cod in
+
+let declare_fun_from_name rt ro s tyl ty =
   let coqTy = List.fold_right (fun typ c ->
       Term.mkArrow (interp_to_coq rt typ) c)
       tyl (interp_to_coq rt ty) in
   let cons_v = Structures.declare_new_variable (Structures.mkId ("Smt_var_"^s)) coqTy in
   let op = Op.declare ro cons_v (Array.of_list tyl) ty None in
-  VeritSyntax.add_fun s op;
+  SmtMaps.add_fun s op;
   op
 
+let declare_fun rt ro sym arg cod =
+  let tyl = List.map sort_of_sort arg in
+  let ty = sort_of_sort cod in
+  declare_fun_from_name rt ro (string_of_symbol sym) tyl ty
+
 
 
 let parse_smt2bv s =
@@ -405,7 +408,7 @@ let make_root ra rf t =
          with _ -> assert false)
 
       | _, _ ->
-        let op = VeritSyntax.get_fun v in
+        let op = SmtMaps.get_fun v in
         let l' = List.map (fun t ->
             match make_root_term t with
             | Atom h -> h | Form _ -> assert false) l in
diff --git a/src/smtlib2/smtlib2_genConstr.mli b/src/smtlib2/smtlib2_genConstr.mli
index dabd99b..7868839 100644
--- a/src/smtlib2/smtlib2_genConstr.mli
+++ b/src/smtlib2/smtlib2_genConstr.mli
@@ -13,8 +13,16 @@
 val pp_symbol : Smtlib2_ast.symbol -> string
 val parse_smt2bv : string -> bool list
 val bigint_bv : Big_int.big_int -> int -> string
+
+(* Import from an SMTLIB2 file *)
 val import_smtlib2 :
   SmtBtype.reify_tbl ->
   SmtAtom.Op.reify_tbl ->
   SmtAtom.Atom.reify_tbl ->
   SmtAtom.Form.reify -> string -> SmtAtom.Form.t list
+
+(* Lower level functions, to build types and terms *)
+val declare_sort_from_name : SmtBtype.reify_tbl -> string -> SmtBtype.btype
+val declare_fun_from_name :
+  SmtBtype.reify_tbl -> SmtAtom.Op.reify_tbl -> string ->
+  SmtBtype.btype list -> SmtBtype.btype -> SmtAtom.indexed_op
diff --git a/src/trace/satAtom.ml b/src/trace/satAtom.ml
index c91cee1..0c5bf83 100644
--- a/src/trace/satAtom.ml
+++ b/src/trace/satAtom.ml
@@ -62,6 +62,3 @@ module Atom =
 module Form = SmtForm.Make(Atom)
 module Trace = SmtTrace.MakeOpt(Form)
 module Cnf = SmtCnf.MakeCnf(Form)
-
-      
-
diff --git a/src/trace/satAtom.mli b/src/trace/satAtom.mli
index 49bc590..92f9bc7 100644
--- a/src/trace/satAtom.mli
+++ b/src/trace/satAtom.mli
@@ -38,38 +38,6 @@ module Form : SmtForm.FORM with type hatom = Atom.t
 
 module Trace :
   sig
-    val share_value : Form.t SmtCertif.clause -> unit
-    module HashedHeadRes :
-      sig
-        type t = Form.t SmtCertif.resolution
-        val equal :
-          'a SmtCertif.resolution -> 'b SmtCertif.resolution -> bool
-        val hash : 'a SmtCertif.resolution -> int
-      end
-    module HRtbl :
-      sig
-        type key = HashedHeadRes.t
-        type 'a t = 'a Hashtbl.Make(HashedHeadRes).t
-        val create : int -> 'a t
-        val clear : 'a t -> unit
-        val reset : 'a t -> unit
-        val copy : 'a t -> 'a t
-        val add : 'a t -> key -> 'a -> unit
-        val remove : 'a t -> key -> unit
-        val find : 'a t -> key -> 'a
-        val find_all : 'a t -> key -> 'a list
-        val replace : 'a t -> key -> 'a -> unit
-        val mem : 'a t -> key -> bool
-        val iter : (key -> 'a -> unit) -> 'a t -> unit
-        val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
-        val length : 'a t -> int
-        val stats : 'a t -> Hashtbl.statistics
-      end
-    val common_head :
-      'a SmtCertif.clause list ->
-      'b SmtCertif.clause list ->
-      'a SmtCertif.clause list * 'a SmtCertif.clause list *
-      'b SmtCertif.clause list
     val share_prefix : Form.t SmtCertif.clause -> int -> unit
   end
 module Cnf :
diff --git a/src/trace/smtCommands.ml b/src/trace/smtCommands.ml
index 78c07b9..e64a131 100644
--- a/src/trace/smtCommands.ml
+++ b/src/trace/smtCommands.ml
@@ -735,8 +735,8 @@ let core_tactic call_solver solver_logic rt ro ra rf ra' rf' vm_cast lcpl lcepl
              with Not_found ->
                let oc = open_out "/tmp/find_lemma.log" in
                let fmt = Format.formatter_of_out_channel oc in
-               List.iter (fun u -> Format.fprintf fmt "%a\n" VeritSyntax.hform_to_smt u) lsmt;
-               Format.fprintf fmt "\n%a\n" VeritSyntax.hform_to_smt hl;
+               List.iter (fun u -> Format.fprintf fmt "%a\n" (Form.to_smt ~debug:true) u) lsmt;
+               Format.fprintf fmt "\n%a\n" (Form.to_smt ~debug:true) hl;
                flush oc; close_out oc; failwith "find_lemma" end
       | _ -> failwith "unexpected form of root" in
 
diff --git a/src/trace/smtForm.ml b/src/trace/smtForm.ml
index 20b99ac..12aef5a 100644
--- a/src/trace/smtForm.ml
+++ b/src/trace/smtForm.ml
@@ -68,8 +68,7 @@ module type FORM =
     val is_pos : t -> bool
     val is_neg : t -> bool
 
-    val to_smt : ?pi:bool ->
-                 (Format.formatter -> hatom -> unit) ->
+    val to_smt : ?debug:bool ->
                  Format.formatter -> t -> unit
 
     val logic : t -> logic
@@ -108,6 +107,13 @@ module type FORM =
     val interp_to_coq :
       (hatom -> Structures.constr) -> (int, Structures.constr) Hashtbl.t ->
       t -> Structures.constr
+
+    (* Unstratified terms *)
+    type atom_form_lit =
+      | Atom of hatom
+      | Form of pform
+      | Lit of t
+    val lit_of_atom_form_lit : reify -> bool * atom_form_lit -> t
   end
 
 module Make (Atom:ATOM) =
@@ -157,29 +163,29 @@ module Make (Atom:ATOM) =
       | Neg hp -> hp.hval
 
 
-    let rec to_smt ?pi:(pi=false) atom_to_smt fmt = function
+    let rec to_smt ?debug:(debug=false) fmt = function
       | Pos hp ->
-         if pi then Format.fprintf fmt "%s" (string_of_int hp.index ^ ":");
-         to_smt_pform atom_to_smt fmt hp.hval
+         if debug then Format.fprintf fmt "%s" (string_of_int hp.index ^ ":");
+         to_smt_pform fmt hp.hval
       | Neg hp ->
-         if pi then Format.fprintf fmt "%s" (string_of_int hp.index ^ ":");
+         if debug then Format.fprintf fmt "%s" (string_of_int hp.index ^ ":");
          Format.fprintf fmt "(not ";
-         to_smt_pform atom_to_smt fmt hp.hval;
+         to_smt_pform fmt hp.hval;
          Format.fprintf fmt ")"
 
-    and to_smt_pform atom_to_smt fmt = function
-      | Fatom a -> atom_to_smt fmt a
-      | Fapp (op,args) -> to_smt_op atom_to_smt fmt op args
+    and to_smt_pform fmt = function
+      | Fatom a -> Atom.to_smt fmt a
+      | Fapp (op,args) -> to_smt_op fmt op args
       (* This is an intermediate object of proofs, it correspond to nothing in SMT *)
       | FbbT (a, l) ->
-        Format.fprintf fmt "(bbT %a [" atom_to_smt a;
+        Format.fprintf fmt "(bbT %a [" Atom.to_smt a;
         let fi = ref true in
         List.iter (fun f -> Format.fprintf fmt "%s%a"
                       (if !fi then "" else "; ")
-                      (to_smt atom_to_smt) f; fi := false) l;
+                      (to_smt ~debug:false) f; fi := false) l;
         Format.fprintf fmt "])"
 
-    and to_smt_op atom_to_smt fmt op args =
+    and to_smt_op fmt op args =
       let (s1,s2) = if ((Array.length args = 0) || (match op with Fnot2 _ -> true | _ -> false)) then ("","") else ("(",")") in
       Format.fprintf fmt "%s" s1;
       (match op with
@@ -198,7 +204,7 @@ module Make (Atom:ATOM) =
              Format.fprintf fmt  ")")
       );
 
-      Array.iter (fun h -> Format.fprintf fmt " "; to_smt atom_to_smt fmt h) args;
+      Array.iter (fun h -> Format.fprintf fmt " "; to_smt fmt h) args;
       Format.fprintf fmt "%s" s2
 
     and to_smt_args fmt = function
@@ -275,6 +281,7 @@ module Make (Atom:ATOM) =
 		| a0::a1::a2::_ ->
                    (to_lit a2) lsl 4 + (to_lit a1) lsl 2 + to_lit a0 in
               (hash_args * 10 + Atom.index ha) * 2 + 1
+
       end
 
     module HashForm = Hashtbl.Make (HashedForm)
@@ -289,34 +296,34 @@ module Make (Atom:ATOM) =
     let check pf =
       match pf with
       | Fatom ha ->  if not (Atom.is_bool_type ha) then
-          raise (Format.eprintf "nwt: %a" (to_smt_pform Atom.to_smt) pf;
+          raise (Format.eprintf "nwt: %a" to_smt_pform pf;
                  NotWellTyped pf)
       | Fapp (op, args) ->
 	(match op with
 	 | Ftrue | Ffalse ->
            if Array.length args <> 0 then
-             raise (Format.eprintf "nwt: %a" (to_smt_pform Atom.to_smt) pf;
+             raise (Format.eprintf "nwt: %a" to_smt_pform pf;
                     NotWellTyped pf)
 	 | Fnot2 _ ->
            if Array.length args <> 1 then
-             raise (Format.eprintf "nwt: %a" (to_smt_pform Atom.to_smt) pf;
+             raise (Format.eprintf "nwt: %a" to_smt_pform pf;
                     NotWellTyped pf)
 	 | Fand | For -> ()
 	 | Fxor | Fimp | Fiff ->
            if Array.length args <> 2 then
-             raise (Format.eprintf "nwt: %a" (to_smt_pform Atom.to_smt) pf;
+             raise (Format.eprintf "nwt: %a" to_smt_pform pf;
                     NotWellTyped pf)
 
           | Fite ->
             if Array.length args <> 3 then
-              raise (Format.eprintf "nwt: %a" (to_smt_pform Atom.to_smt) pf;
+              raise (Format.eprintf "nwt: %a" to_smt_pform pf;
                      NotWellTyped pf)
 
          | Fforall l -> ()
        )
 
       | FbbT (ha, l) -> if not (Atom.is_bv_type ha) then
-          raise (Format.eprintf "nwt: %a" (to_smt_pform Atom.to_smt) pf;
+          raise (Format.eprintf "nwt: %a" to_smt_pform pf;
                  NotWellTyped pf)
 
     let declare reify pf =
@@ -639,4 +646,17 @@ module Make (Atom:ATOM) =
 	  done;
 	  !r in
         interp_form f
+
+    (* Unstratified terms *)
+    type atom_form_lit =
+      | Atom of hatom
+      | Form of pform
+      | Lit of t
+
+    let lit_of_atom_form_lit rf = function
+      | decl, Atom a -> get ~declare:decl rf (Fatom a)
+      | decl, Form f -> begin match f with
+                          | Fapp (Fforall _, _) when decl -> failwith "decl is true on a forall"
+                          | _ -> get ~declare:decl rf f end
+      | decl, Lit l -> l
 end
diff --git a/src/trace/smtForm.mli b/src/trace/smtForm.mli
index ba8c066..ad7d2ca 100644
--- a/src/trace/smtForm.mli
+++ b/src/trace/smtForm.mli
@@ -64,8 +64,7 @@ module type FORM =
       val is_pos : t -> bool
       val is_neg : t -> bool
 
-      val to_smt : ?pi:bool ->
-                   (Format.formatter -> hatom -> unit) ->
+      val to_smt : ?debug:bool ->
                    Format.formatter -> t -> unit
 
       val logic : t -> logic
@@ -105,6 +104,13 @@ module type FORM =
       val interp_to_coq :
 	  (hatom -> Structures.constr) -> (int, Structures.constr) Hashtbl.t ->
 	    t -> Structures.constr
+
+      (* Unstratified terms *)
+      type atom_form_lit =
+        | Atom of hatom
+        | Form of pform
+        | Lit of t
+      val lit_of_atom_form_lit : reify -> bool * atom_form_lit -> t
   end
 
 module Make (Atom:ATOM) : FORM with type hatom = Atom.t
diff --git a/src/trace/smtTrace.ml b/src/trace/smtTrace.ml
index 5d9d82d..f397826 100644
--- a/src/trace/smtTrace.ml
+++ b/src/trace/smtTrace.ml
@@ -14,11 +14,14 @@ open SmtMisc
 open CoqTerms
 open SmtCertif
 
+
+(** Steps identifiers **)
+
 let notUsed = 0
 
 let next_id = ref 0
 
-let clear () = next_id := 0
+let clear_id () = next_id := 0
 
 let next_id () =
   let id = !next_id in
@@ -170,7 +173,7 @@ let order_roots init_index first =
 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 ());
+  clear_id (); ignore (next_id ());
   while isRoot !r.kind do
     ignore (next_id ());
     r := next !r;
@@ -498,25 +501,25 @@ let to_coq to_lit interp (cstep,
 module MakeOpt (Form:SmtForm.FORM) =
   struct
     (* Share the certificate building a common clause *)
-    let share_value c =
-      let tbl = Hashtbl.create 17 in
-      let to_lits v = List.map (Form.to_lit) v in
-      let process c =
-	match c.value with
-	| None -> ()
-	| Some v ->
-	    let lits = to_lits v in
-	    try
-	      let c' = Hashtbl.find tbl lits in
-	      set_same c c'
-	    with Not_found  -> Hashtbl.add tbl lits c in
-      let r = ref c in
-      while !r.next <> None do
-	let next = next !r in
-	process !r;
-	r := next
-      done;
-      process !r
+    (* let share_value c =
+     *   let tbl = Hashtbl.create 17 in
+     *   let to_lits v = List.map (Form.to_lit) v in
+     *   let process c =
+     *     match c.value with
+     *     | None -> ()
+     *     | Some v ->
+     *         let lits = to_lits v in
+     *         try
+     *           let c' = Hashtbl.find tbl lits in
+     *           set_same c c'
+     *         with Not_found  -> Hashtbl.add tbl lits c in
+     *   let r = ref c in
+     *   while !r.next <> None do
+     *     let next = next !r in
+     *     process !r;
+     *     r := next
+     *   done;
+     *   process !r *)
 
    (* Sharing of the common prefix *)
 
@@ -593,3 +596,6 @@ module MakeOpt (Form:SmtForm.FORM) =
       done
 
   end
+
+
+let clear () = clear_id ()
diff --git a/src/trace/smtTrace.mli b/src/trace/smtTrace.mli
index 5ded32a..a12e2e7 100644
--- a/src/trace/smtTrace.mli
+++ b/src/trace/smtTrace.mli
@@ -10,6 +10,7 @@
 (**************************************************************************)
 
 
+(* Traces *)
 val notUsed : int
 val clear : unit -> unit
 val next_id : unit -> SmtCertif.clause_id
@@ -67,40 +68,10 @@ val to_coq :
   ('a SmtCertif.clause -> Structures.types * Structures.constr) option ->
   Structures.constr * 'a SmtCertif.clause *
     (Structures.id * Structures.types) list
+
+
 module MakeOpt :
   functor (Form : SmtForm.FORM) ->
     sig
-      val share_value : Form.t SmtCertif.clause -> unit
-      module HashedHeadRes :
-        sig
-          type t = Form.t SmtCertif.resolution
-          val equal :
-            'a SmtCertif.resolution -> 'b SmtCertif.resolution -> bool
-          val hash : 'a SmtCertif.resolution -> int
-        end
-      module HRtbl :
-        sig
-          type key = HashedHeadRes.t
-          type 'a t = 'a Hashtbl.Make(HashedHeadRes).t
-          val create : int -> 'a t
-          val clear : 'a t -> unit
-          val reset : 'a t -> unit
-          val copy : 'a t -> 'a t
-          val add : 'a t -> key -> 'a -> unit
-          val remove : 'a t -> key -> unit
-          val find : 'a t -> key -> 'a
-          val find_all : 'a t -> key -> 'a list
-          val replace : 'a t -> key -> 'a -> unit
-          val mem : 'a t -> key -> bool
-          val iter : (key -> 'a -> unit) -> 'a t -> unit
-          val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
-          val length : 'a t -> int
-          val stats : 'a t -> Hashtbl.statistics
-        end
-      val common_head :
-        'a SmtCertif.clause list ->
-        'b SmtCertif.clause list ->
-        'a SmtCertif.clause list * 'a SmtCertif.clause list *
-        'b SmtCertif.clause list
       val share_prefix : Form.t SmtCertif.clause -> int -> unit
     end
diff --git a/src/verit/verit.ml b/src/verit/verit.ml
index 57fd0cc..17a230f 100644
--- a/src/verit/verit.ml
+++ b/src/verit/verit.ml
@@ -104,6 +104,7 @@ let import_trace ra' rf' filename first lsmt =
 
 let clear_all () =
   SmtTrace.clear ();
+  SmtMaps.clear ();
   VeritSyntax.clear ()
 
 
@@ -145,13 +146,13 @@ let export out_channel rt ro lsmt =
 
   List.iter (fun (i,t) ->
     let s = "Tindex_"^(string_of_int i) in
-    VeritSyntax.add_btype s (Tindex t);
+    SmtMaps.add_btype s (Tindex t);
     Format.fprintf fmt "(declare-sort %s 0)@." s
   ) (SmtBtype.to_list rt);
 
   List.iter (fun (i,dom,cod,op) ->
     let s = "op_"^(string_of_int i) in
-    VeritSyntax.add_fun s op;
+    SmtMaps.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) dom;
@@ -161,7 +162,7 @@ let export out_channel rt ro lsmt =
   ) (Op.to_list ro);
 
   List.iter (fun u -> Format.fprintf fmt "(assert ";
-                      Form.to_smt Atom.to_smt fmt u;
+                      Form.to_smt fmt u;
                       Format.fprintf fmt ")\n") lsmt;
 
   Format.fprintf fmt "(check-sat)\n(exit)@."
diff --git a/src/verit/veritParser.mly b/src/verit/veritParser.mly
index 65eb6b7..08c5cb3 100644
--- a/src/verit/veritParser.mly
+++ b/src/verit/veritParser.mly
@@ -175,7 +175,7 @@ lit_list:
 ;
 
 lit:   /* returns a SmtAtom.Form.t option */
-  | name_term                                              { let decl, t = $1 in decl, lit_of_atom_form_lit rf (decl, t) }
+  | name_term                                              { let decl, t = $1 in decl, Form.lit_of_atom_form_lit rf (decl, t) }
   | LPAR NOT lit RPAR                                      { apply_dec Form.neg $3 }
 ;
 
@@ -191,15 +191,15 @@ var_atvar:
 name_term:   /* returns a bool * (SmtAtom.Form.pform or a SmtAtom.hatom), the boolean indicates if we should declare the term or not */
   | SHARPINT                                              { get_solver $1 }
   | SHARPINT COLON LPAR term RPAR                         { let res = $4 in add_solver $1 res; res }
-  | BITV                                                   { true, Atom (Atom.mk_bvconst ra (parse_bv $1)) }
-  | TRUE                                                   { true, Form Form.pform_true }
-  | FALS                                                   { true, Form Form.pform_false }
+  | BITV                                                   { true, Form.Atom (Atom.mk_bvconst ra (parse_bv $1)) }
+  | TRUE                                                   { true, Form.Form Form.pform_true }
+  | FALS                                                   { true, Form.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, [||]))) }
+    					                   | Some bt -> false, Form.Atom (Atom.get ~declare:false ra (Aapp (dummy_indexed_op (Rel_name x) [||] bt, [||])))
+							   | None -> true, Form.Atom (Atom.get ra (Aapp (SmtMaps.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) }
+  | INT                                                    { true, Form.Atom (Atom.hatom_Z_of_int ra $1) }
+  | BIGINT                                                 { true, Form.Atom (Atom.hatom_Z_of_bigint ra $1) }
 ;
 
 tvar:
@@ -214,27 +214,27 @@ var_decl_list:
 ;
 
 forall_decl:
-  | FORALL LPAR var_decl_list RPAR blit		   { clear_qvar (); false, Form (Fapp (Fforall $3, [|lit_of_atom_form_lit rf $5|])) }
+  | FORALL LPAR var_decl_list RPAR blit		   { clear_qvar (); false, Form.Form (Fapp (Fforall $3, [|Form.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                                                   { 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) }
+  | TRUE                                                   { true, Form.Form Form.pform_true }
+  | FALS                                                   { true, Form.Form Form.pform_false }
+  | AND lit_list                                           { apply_dec (fun x -> Form.Form (Fapp (Fand, Array.of_list x))) (list_dec $2) }
+  | OR lit_list                                            { apply_dec (fun x -> Form.Form (Fapp (For, Array.of_list x))) (list_dec $2) }
+  | IMP lit_list                                           { apply_dec (fun x -> Form.Form (Fapp (Fimp, Array.of_list x))) (list_dec $2) }
+  | XOR lit_list                                           { apply_dec (fun x -> Form.Form (Fapp (Fxor, Array.of_list x))) (list_dec $2) }
+  | ITE lit_list                                           { apply_dec (fun x -> Form.Form (Fapp (Fite, Array.of_list x))) (list_dec $2) }
   | forall_decl                                            { $1 }
-  | BBT name_term LBRACKET lit_list RBRACKET               { let (decl, t) = $2 in let (decll, l) = list_dec $4 in (decl && decll, match t with | Atom a -> Form (FbbT (a, l)) | _ -> assert false) }
+  | BBT name_term LBRACKET lit_list RBRACKET               { let (decl, t) = $2 in let (decll, l) = list_dec $4 in (decl && decll, match t with | Form.Atom a -> Form.Form (FbbT (a, l)) | _ -> assert false) }
 
   /* Atoms */
-  | INT                                                    { true, Atom (Atom.hatom_Z_of_int ra $1) }
-  | BIGINT                                                 { true, Atom (Atom.hatom_Z_of_bigint ra $1) }
-  | BITV                                                   { true, Atom (Atom.mk_bvconst ra (parse_bv $1)) }
+  | INT                                                    { true, Form.Atom (Atom.hatom_Z_of_int ra $1) }
+  | BIGINT                                                 { true, Form.Atom (Atom.hatom_Z_of_bigint ra $1) }
+  | BITV                                                   { true, Form.Atom (Atom.mk_bvconst ra (parse_bv $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 }
@@ -246,7 +246,7 @@ term:   /* returns a bool * (SmtAtom.Form.pform or SmtAtom.hatom), the boolean i
   | OPP name_term                                          { apply_dec_atom (Atom.mk_opp ra) $2 }
   | DIST args                                              { let da, la = list_dec $2 in
     	 						     let a = Array.of_list la in
-                                                             da, Atom (Atom.mk_distinct ra ~declare:da (Atom.type_of a.(0)) a) }
+                                                             da, Form.Atom (Atom.mk_distinct ra ~declare:da (Atom.type_of a.(0)) a) }
   | BITOF INT name_term                                    { apply_dec_atom (fun ?declare:(d=true) h -> match Atom.type_of h with TBV s -> Atom.mk_bitof ra ~declare:d s $2 h | _ -> assert false) $3 }
   | BVNOT name_term                                        { apply_dec_atom (fun ?declare:(d=true) h -> match Atom.type_of h with TBV s -> Atom.mk_bvnot ra ~declare:d s h | _ -> assert false) $2 }
   | BVAND name_term name_term                              { apply_bdec_atom (fun ?declare:(d=true) h1 h2 -> match Atom.type_of h1 with TBV s -> Atom.mk_bvand ra ~declare:d s h1 h2 | _ -> assert false) $2 $3 }
@@ -257,8 +257,8 @@ term:   /* returns a bool * (SmtAtom.Form.pform or SmtAtom.hatom), the boolean i
   | BVMUL name_term name_term                              { apply_bdec_atom (fun ?declare:(d=true) h1 h2 -> match Atom.type_of h1 with TBV s -> Atom.mk_bvmult ra ~declare:d s h1 h2 | _ -> assert false) $2 $3 }
   | BVULT name_term name_term                              { apply_bdec_atom (fun ?declare:(d=true) h1 h2 -> match Atom.type_of h1 with TBV s -> Atom.mk_bvult ra ~declare:d s h1 h2 | _ -> assert false) $2 $3 }
   | BVSLT name_term name_term                              { apply_bdec_atom (fun ?declare:(d=true) h1 h2 -> match Atom.type_of h1 with TBV s -> Atom.mk_bvslt ra ~declare:d s h1 h2 | _ -> assert false) $2 $3 }
-  | BVULE name_term name_term                              { let (decl,_) as a = apply_bdec_atom (fun ?declare:(d=true) h1 h2 -> match Atom.type_of h1 with TBV s -> Atom.mk_bvult ra ~declare:d s h1 h2 | _ -> assert false) $2 $3 in (decl, Lit (Form.neg (lit_of_atom_form_lit rf a))) }
-  | BVSLE name_term name_term                              { let (decl,_) as a = apply_bdec_atom (fun ?declare:(d=true) h1 h2 -> match Atom.type_of h1 with TBV s -> Atom.mk_bvslt ra ~declare:d s h1 h2 | _ -> assert false) $2 $3 in (decl, Lit (Form.neg (lit_of_atom_form_lit rf a))) }
+  | BVULE name_term name_term                              { let (decl,_) as a = apply_bdec_atom (fun ?declare:(d=true) h1 h2 -> match Atom.type_of h1 with TBV s -> Atom.mk_bvult ra ~declare:d s h1 h2 | _ -> assert false) $2 $3 in (decl, Form.Lit (Form.neg (Form.lit_of_atom_form_lit rf a))) }
+  | BVSLE name_term name_term                              { let (decl,_) as a = apply_bdec_atom (fun ?declare:(d=true) h1 h2 -> match Atom.type_of h1 with TBV s -> Atom.mk_bvslt ra ~declare:d s h1 h2 | _ -> assert false) $2 $3 in (decl, Form.Lit (Form.neg (Form.lit_of_atom_form_lit rf a))) }
   | BVSHL name_term name_term                              { apply_bdec_atom (fun ?declare:(d=true) h1 h2 -> match Atom.type_of h1 with TBV s -> Atom.mk_bvshl ra ~declare:d s h1 h2 | _ -> assert false) $2 $3 }
   | BVSHR name_term name_term                              { apply_bdec_atom (fun ?declare:(d=true) h1 h2 -> match Atom.type_of h1 with TBV s -> Atom.mk_bvshr ra ~declare:d s h1 h2 | _ -> assert false) $2 $3 }
   | BVCONC name_term name_term                             { apply_bdec_atom (fun ?declare:(d=true) h1 h2 -> match Atom.type_of h1, Atom.type_of h2 with TBV s1, TBV s2 -> Atom.mk_bvconcat ra ~declare:d s1 s2 h1 h2 | _, _ -> assert false) $2 $3 }
@@ -268,26 +268,20 @@ term:   /* returns a bool * (SmtAtom.Form.pform or SmtAtom.hatom), the boolean i
   | SELECT name_term name_term                             { apply_bdec_atom (fun ?declare:(d=true) h1 h2 -> match Atom.type_of h1 with TFArray (ti, te) -> Atom.mk_select ra ~declare:d ti te h1 h2 | _ -> assert false) $2 $3 }
   | DIFF name_term name_term                               { apply_bdec_atom (fun ?declare:(d=true) h1 h2 -> match Atom.type_of h1 with TFArray (ti, te) -> Atom.mk_diffarray ra ~declare:d ti te h1 h2 | _ -> assert false) $2 $3 }
   | STORE name_term name_term name_term                    { apply_tdec_atom (fun ?declare:(d=true) h1 h2 h3 -> match Atom.type_of h1 with TFArray (ti, te) -> Atom.mk_store ra ~declare:d ti te h1 h2 h3 | _ -> assert false) $2 $3 $4 }
-  | 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))) }
+  | VAR                                                    { let x = $1 in match find_opt_qvar x with | Some bt -> false, Form.Atom (Atom.get ~declare:false ra (Aapp (dummy_indexed_op (Rel_name x) [||] bt, [||]))) | None -> true, Form.Atom (Atom.get ra (Aapp (SmtMaps.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, Form.Atom (Atom.get ~declare:false ra (Aapp (op, Array.of_list (snd (list_dec a))))) | None -> let dl, l = list_dec $2 in dl, Form.Atom (Atom.get ra ~declare:dl (Aapp (SmtMaps.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 | (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 ~declare: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|])) }
+  | EQ name_term name_term                                 { let t1 = $2 in let t2 = $3 in match t1,t2 with | (decl1, Form.Atom h1), (decl2, Form.Atom h2) when (match Atom.type_of h1 with | SmtBtype.Tbool -> false | _ -> true) -> let decl = decl1 && decl2 in decl, Form.Atom (Atom.mk_eq ra ~declare:decl (Atom.type_of h1) h1 h2) | (decl1, t1), (decl2, t2) -> decl1 && decl2, Form.Form (Fapp (Fiff, [|Form.lit_of_atom_form_lit rf (decl1, t1); Form.lit_of_atom_form_lit rf (decl2, t2)|])) }
+  | EQ nlit lit                                            { match $2, $3 with (decl1, t1), (decl2, t2) -> decl1 && decl2, Form.Form (Fapp (Fiff, [|t1; t2|])) }
+  | EQ name_term nlit                                      { match $2, $3 with (decl1, t1), (decl2, t2) -> decl1 && decl2, Form.Form (Fapp (Fiff, [|Form.lit_of_atom_form_lit rf (decl1, t1); t2|])) }
   | LET LPAR bindlist RPAR name_term                       { $3; $5 }
   | BINDVAR                                                { true, Hashtbl.find hlets $1 }
 ;
 
 blit:
   | name_term                                              { $1 }
-  | LPAR NOT lit RPAR                                      { apply_dec (fun l -> Lit (Form.neg l)) $3 }
+  | LPAR NOT lit RPAR                                      { apply_dec (fun l -> Form.Lit (Form.neg l)) $3 }
 ;
 
 bindlist:
@@ -295,8 +289,8 @@ bindlist:
   | LPAR BINDVAR blit RPAR bindlist                        { Hashtbl.add hlets $2 (snd $3); $5 }
 
 args:
-  | 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 }
+  | name_term                                              { match $1 with decl, Form.Atom h -> [decl, h] | _ -> assert false }
+  | name_term args                                         { match $1 with decl, Form.Atom h -> (decl, h)::$2 | _ -> assert false }
 ;
 
 clause_ids_params:
diff --git a/src/verit/veritSyntax.ml b/src/verit/veritSyntax.ml
index 6b26f65..b1a6304 100644
--- a/src/verit/veritSyntax.ml
+++ b/src/verit/veritSyntax.ml
@@ -496,20 +496,6 @@ let mk_clause cl =
     Structures.error ("SMTCoq was not able to check the certificate \
                        for the following reason.\n"^f)
 
-type atom_form_lit =
-  | Atom of SmtAtom.Atom.t
-  | 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
-  | 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
@@ -519,54 +505,37 @@ let rec list_dec = function
      decl_h && decl_t, h :: l_t
 
 let apply_dec_atom (f:?declare:bool -> SmtAtom.hatom -> SmtAtom.hatom) = function
-  | decl, Atom h -> decl, Atom (f ~declare:decl h)
+  | decl, Form.Atom h -> decl, Form.Atom (f ~declare:decl h)
   | _ -> assert false
 
 let apply_bdec_atom (f:?declare:bool -> SmtAtom.Atom.t -> SmtAtom.Atom.t -> SmtAtom.Atom.t) o1 o2 =
   match o1, o2 with
-  | (decl1, Atom h1), (decl2, Atom h2) ->
+  | (decl1, Form.Atom h1), (decl2, Form.Atom h2) ->
      let decl = decl1 && decl2 in
-     decl, Atom (f ~declare:decl h1 h2)
+     decl, Form.Atom (f ~declare:decl h1 h2)
   | _ -> assert false
 
 let apply_tdec_atom (f:?declare:bool -> SmtAtom.Atom.t -> SmtAtom.Atom.t -> SmtAtom.Atom.t -> SmtAtom.Atom.t) o1 o2 o3 =
   match o1, o2, o3 with
-  | (decl1, Atom h1), (decl2, Atom h2), (decl3, Atom h3) ->
+  | (decl1, Form.Atom h1), (decl2, Form.Atom h2), (decl3, Form.Atom h3) ->
      let decl = decl1 && decl2 && decl3 in
-     decl, Atom (f ~declare:decl h1 h2 h3)
+     decl, Form.Atom (f ~declare:decl h1 h2 h3)
   | _ -> assert false
 
 
-let solver : (int, (bool * atom_form_lit)) Hashtbl.t = Hashtbl.create 17
+let solver : (int, (bool * Form.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")
 let add_solver id cl = Hashtbl.add solver id cl
 let clear_solver () = Hashtbl.clear solver
 
-let btypes : (string, SmtBtype.btype) Hashtbl.t = Hashtbl.create 17
-let get_btype id =
-  try Hashtbl.find btypes id
-  with | Not_found -> failwith ("VeritSyntax.get_btype : sort symbol \""^id^"\" not found\n")
-let add_btype id cl = Hashtbl.add btypes id cl
-let clear_btypes () = Hashtbl.clear btypes
-
-let funs : (string,indexed_op) Hashtbl.t = Hashtbl.create 17
-let get_fun id =
-  try Hashtbl.find funs id
-  with | Not_found -> failwith ("VeritSyntax.get_fun : function symbol \""^id^"\" not found\n")
-let add_fun id cl = Hashtbl.add funs id cl
-let remove_fun id = Hashtbl.remove funs id
-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 hform_to_smt = Form.to_smt ~pi:true Atom.to_smt
-
 (* 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 =
@@ -583,8 +552,8 @@ let init_index lsmt re_hash =
             with Not_found ->
               let oc = open_out "/tmp/input_not_found.log" in
               let fmt = Format.formatter_of_out_channel oc in
-              List.iter (fun h -> Format.fprintf fmt "%a\n" hform_to_smt (re_hash h)) lsmt;
-              Format.fprintf fmt "\n%a\n@." hform_to_smt re_hf;
+              List.iter (fun h -> Format.fprintf fmt "%a\n" (Form.to_smt ~debug:true) (re_hash h)) lsmt;
+              Format.fprintf fmt "\n%a\n@." (Form.to_smt ~debug:true) re_hf;
               flush oc; close_out oc;
               failwith "not found: log available"
 
@@ -604,7 +573,7 @@ let rf = Form.create ()
 let ra' = Atom.create ()
 let rf' = Form.create ()
 
-let hlets : (string, atom_form_lit) Hashtbl.t = Hashtbl.create 17
+let hlets : (string, Form.atom_form_lit) Hashtbl.t = Hashtbl.create 17
 
 let clear_mk_clause () =
   to_add := [];
@@ -615,8 +584,6 @@ let clear () =
   clear_mk_clause ();
   clear_clauses ();
   clear_solver ();
-  clear_btypes ();
-  clear_funs ();
   Atom.clear ra;
   Form.clear rf;
   Atom.clear ra';
diff --git a/src/verit/veritSyntax.mli b/src/verit/veritSyntax.mli
index fd39052..7a325a6 100644
--- a/src/verit/veritSyntax.mli
+++ b/src/verit/veritSyntax.mli
@@ -10,6 +10,8 @@
 (**************************************************************************)
 
 
+open SmtAtom
+
 exception Sat
 
 type typ = | 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 | Weak | 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 | Flat | Hole | Bbva | Bbconst | Bbeq | Bbdis | Bbop | Bbadd | Bbmul | Bbult | Bbslt | Bbnot | Bbneg | Bbconc | Bbextr | Bbzext | Bbsext | Bbshl | Bbshr | Row1 | Row2 | Exte
@@ -23,51 +25,36 @@ 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 -> bool * atom_form_lit -> SmtAtom.Form.t
-
 val apply_dec_atom : (?declare:bool -> SmtAtom.hatom -> SmtAtom.hatom) ->
-                     bool * atom_form_lit -> bool * atom_form_lit
+                     bool * Form.atom_form_lit -> bool * Form.atom_form_lit
 val apply_bdec_atom :
   (?declare:bool -> SmtAtom.Atom.t -> SmtAtom.Atom.t -> SmtAtom.Atom.t) ->
-  bool * atom_form_lit -> bool * atom_form_lit -> bool * atom_form_lit
+  bool * Form.atom_form_lit -> bool * Form.atom_form_lit -> bool * Form.atom_form_lit
 val apply_tdec_atom :
   (?declare:bool -> SmtAtom.Atom.t -> SmtAtom.Atom.t -> SmtAtom.Atom.t -> SmtAtom.Atom.t) ->
-  bool * atom_form_lit -> bool * atom_form_lit -> bool * atom_form_lit -> bool * atom_form_lit
+  bool * Form.atom_form_lit -> bool * Form.atom_form_lit -> bool * Form.atom_form_lit -> bool * Form.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
-
-val get_fun : string -> SmtAtom.indexed_op
-val add_fun : string -> SmtAtom.indexed_op -> unit
-val remove_fun : string -> unit
+val get_solver : int -> bool * Form.atom_form_lit
+val add_solver : int -> bool * Form.atom_form_lit -> unit
 
 val find_opt_qvar : string -> SmtBtype.btype option 
 val add_qvar : string -> SmtBtype.btype -> unit
 val clear_qvar : unit -> unit
 
-val hform_to_smt : Format.formatter -> SmtAtom.Form.t -> unit
-
 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
+val hlets : (string, Form.atom_form_lit) Hashtbl.t
 
 val clear : unit -> unit
diff --git a/src/versions/native/Make b/src/versions/native/Make
index f28d1c9..e278c82 100644
--- a/src/versions/native/Make
+++ b/src/versions/native/Make
@@ -46,7 +46,7 @@
 -custom "$(CAMLYACC) $<" "%.mly" "%.ml %.mli"
 -custom "" "verit/veritParser.ml verit/veritLexer.ml ../3rdparty/alt-ergo/smtlib2_parse.ml ../3rdparty/alt-ergo/smtlib2_lex.ml smtlib2/sExprParser.ml smtlib2/sExprLexer.ml lfsc/lfscParser.ml lfsc/lfscLexer.ml" "ml"
 
--custom "$(CAMLOPTLINK) $(ZFLAGS) -a -o $@ $^" "versions/native/structures.cmx trace/smtMisc.cmx trace/coqTerms.cmx trace/smtBtype.cmx trace/smtForm.cmx trace/smtCertif.cmx trace/smtTrace.cmx trace/smtCnf.cmx trace/satAtom.cmx trace/smtAtom.cmx zchaff/satParser.cmx zchaff/zchaffParser.cmx zchaff/cnfParser.cmx zchaff/zchaff.cmx ../3rdparty/alt-ergo/smtlib2_util.cmx ../3rdparty/alt-ergo/smtlib2_ast.cmx ../3rdparty/alt-ergo/smtlib2_parse.cmx ../3rdparty/alt-ergo/smtlib2_lex.cmx smtlib2/sExpr.cmx smtlib2/sExprParser.cmx smtlib2/sExprLexer.cmx smtlib2/smtlib2_solver.cmx lia/lia.cmx verit/veritSyntax.cmx verit/veritParser.cmx verit/veritLexer.cmx lfsc/shashcons.cmx lfsc/hstring.cmx lfsc/type.cmx lfsc/ast.cmx lfsc/builtin.cmx lfsc/tosmtcoq.cmx lfsc/converter.cmx lfsc/lfscParser.cmx lfsc/lfscLexer.cmx smtlib2/smtlib2_genConstr.cmx trace/smtCommands.cmx verit/verit.cmx lfsc/lfsc.cmx smtcoq_plugin.cmx" "$(CMXA)"
+-custom "$(CAMLOPTLINK) $(ZFLAGS) -a -o $@ $^" "versions/native/structures.cmx trace/smtMisc.cmx trace/coqTerms.cmx trace/smtBtype.cmx trace/smtForm.cmx trace/smtCertif.cmx trace/smtTrace.cmx trace/smtCnf.cmx trace/satAtom.cmx trace/smtAtom.cmx trace/smtMaps.cmx zchaff/satParser.cmx zchaff/zchaffParser.cmx zchaff/cnfParser.cmx zchaff/zchaff.cmx ../3rdparty/alt-ergo/smtlib2_util.cmx ../3rdparty/alt-ergo/smtlib2_ast.cmx ../3rdparty/alt-ergo/smtlib2_parse.cmx ../3rdparty/alt-ergo/smtlib2_lex.cmx smtlib2/sExpr.cmx smtlib2/sExprParser.cmx smtlib2/sExprLexer.cmx smtlib2/smtlib2_solver.cmx lia/lia.cmx verit/veritSyntax.cmx verit/veritParser.cmx verit/veritLexer.cmx lfsc/shashcons.cmx lfsc/hstring.cmx lfsc/type.cmx lfsc/ast.cmx lfsc/builtin.cmx lfsc/tosmtcoq.cmx lfsc/converter.cmx lfsc/lfscParser.cmx lfsc/lfscLexer.cmx smtlib2/smtlib2_genConstr.cmx trace/smtCommands.cmx verit/verit.cmx lfsc/lfsc.cmx smtcoq_plugin.cmx" "$(CMXA)"
 -custom "$(CAMLOPTLINK) $(ZFLAGS) -o $@ -linkall -shared $^" "$(CMXA)" "$(CMXS)"
 
 CMXA = smtcoq.cmxa
@@ -84,6 +84,8 @@ trace/smtCommands.ml
 trace/smtCommands.mli
 trace/smtForm.ml
 trace/smtForm.mli
+trace/smtMaps.ml
+trace/smtMaps.mli
 trace/smtMisc.ml
 trace/smtMisc.mli
 trace/smtTrace.ml
diff --git a/src/versions/native/Makefile b/src/versions/native/Makefile
index 3f0d0f6..aaaab9e 100644
--- a/src/versions/native/Makefile
+++ b/src/versions/native/Makefile
@@ -215,6 +215,7 @@ MLFILES:=lia/lia.ml\
   ../3rdparty/alt-ergo/smtlib2_parse.ml\
   trace/smtTrace.ml\
   trace/smtMisc.ml\
+  trace/smtMaps.ml\
   trace/smtForm.ml\
   trace/smtCommands.ml\
   trace/smtCnf.ml\
@@ -252,6 +253,7 @@ MLIFILES:=lia/lia.mli\
   ../3rdparty/alt-ergo/smtlib2_parse.mli\
   trace/smtTrace.mli\
   trace/smtMisc.mli\
+  trace/smtMaps.mli\
   trace/smtForm.mli\
   trace/smtCommands.mli\
   trace/smtCnf.mli\
@@ -329,7 +331,7 @@ beautify: $(VFILES:=.beautified)
 $(CMXS): $(CMXA)
 	$(CAMLOPTLINK) $(ZFLAGS) -o $@ -linkall -shared $^
 
-$(CMXA): versions/native/structures.cmx trace/smtMisc.cmx trace/coqTerms.cmx trace/smtBtype.cmx trace/smtForm.cmx trace/smtCertif.cmx trace/smtTrace.cmx trace/smtCnf.cmx trace/satAtom.cmx trace/smtAtom.cmx zchaff/satParser.cmx zchaff/zchaffParser.cmx zchaff/cnfParser.cmx zchaff/zchaff.cmx ../3rdparty/alt-ergo/smtlib2_util.cmx ../3rdparty/alt-ergo/smtlib2_ast.cmx ../3rdparty/alt-ergo/smtlib2_parse.cmx ../3rdparty/alt-ergo/smtlib2_lex.cmx smtlib2/sExpr.cmx smtlib2/sExprParser.cmx smtlib2/sExprLexer.cmx smtlib2/smtlib2_solver.cmx lia/lia.cmx verit/veritSyntax.cmx verit/veritParser.cmx verit/veritLexer.cmx lfsc/shashcons.cmx lfsc/hstring.cmx lfsc/type.cmx lfsc/ast.cmx lfsc/builtin.cmx lfsc/tosmtcoq.cmx lfsc/converter.cmx lfsc/lfscParser.cmx lfsc/lfscLexer.cmx smtlib2/smtlib2_genConstr.cmx trace/smtCommands.cmx verit/verit.cmx lfsc/lfsc.cmx smtcoq_plugin.cmx
+$(CMXA): versions/native/structures.cmx trace/smtMisc.cmx trace/coqTerms.cmx trace/smtBtype.cmx trace/smtForm.cmx trace/smtCertif.cmx trace/smtTrace.cmx trace/smtCnf.cmx trace/satAtom.cmx trace/smtAtom.cmx trace/smtMaps.cmx zchaff/satParser.cmx zchaff/zchaffParser.cmx zchaff/cnfParser.cmx zchaff/zchaff.cmx ../3rdparty/alt-ergo/smtlib2_util.cmx ../3rdparty/alt-ergo/smtlib2_ast.cmx ../3rdparty/alt-ergo/smtlib2_parse.cmx ../3rdparty/alt-ergo/smtlib2_lex.cmx smtlib2/sExpr.cmx smtlib2/sExprParser.cmx smtlib2/sExprLexer.cmx smtlib2/smtlib2_solver.cmx lia/lia.cmx verit/veritSyntax.cmx verit/veritParser.cmx verit/veritLexer.cmx lfsc/shashcons.cmx lfsc/hstring.cmx lfsc/type.cmx lfsc/ast.cmx lfsc/builtin.cmx lfsc/tosmtcoq.cmx lfsc/converter.cmx lfsc/lfscParser.cmx lfsc/lfscLexer.cmx smtlib2/smtlib2_genConstr.cmx trace/smtCommands.cmx verit/verit.cmx lfsc/lfsc.cmx smtcoq_plugin.cmx
 	$(CAMLOPTLINK) $(ZFLAGS) -a -o $@ $^
 
 ml: verit/veritParser.ml verit/veritLexer.ml ../3rdparty/alt-ergo/smtlib2_parse.ml ../3rdparty/alt-ergo/smtlib2_lex.ml smtlib2/sExprParser.ml smtlib2/sExprLexer.ml lfsc/lfscParser.ml lfsc/lfscLexer.ml
@@ -370,11 +372,11 @@ install-natdynlink:
 	 install -d `dirname $(DSTROOT)$(COQLIBINSTALL)/SMTCoq/$$i`; \
 	 install -m 0644 $$i $(DSTROOT)$(COQLIBINSTALL)/SMTCoq/$$i; \
 	done
-	for i in $(VCMXS); do \
+	for i in $(CMXA); do \
 	 install -d `dirname $(DSTROOT)$(COQLIBINSTALL)/SMTCoq/$$i`; \
 	 install -m 0644 $$i $(DSTROOT)$(COQLIBINSTALL)/SMTCoq/$$i; \
 	done
-	for i in $(CMXA); do \
+	for i in $(VCMXS); do \
 	 install -d `dirname $(DSTROOT)$(COQLIBINSTALL)/SMTCoq/$$i`; \
 	 install -m 0644 $$i $(DSTROOT)$(COQLIBINSTALL)/SMTCoq/$$i; \
 	done
diff --git a/src/versions/standard/_CoqProject b/src/versions/standard/_CoqProject
index 8b88cb5..e067da8 100644
--- a/src/versions/standard/_CoqProject
+++ b/src/versions/standard/_CoqProject
@@ -70,6 +70,8 @@ trace/smtCommands.ml
 trace/smtCommands.mli
 trace/smtForm.ml
 trace/smtForm.mli
+trace/smtMaps.ml
+trace/smtMaps.mli
 trace/smtMisc.ml
 trace/smtMisc.mli
 trace/smtTrace.ml
diff --git a/src/versions/standard/smtcoq_plugin_standard.mlpack b/src/versions/standard/smtcoq_plugin_standard.mlpack
index 0101147..81ac24b 100644
--- a/src/versions/standard/smtcoq_plugin_standard.mlpack
+++ b/src/versions/standard/smtcoq_plugin_standard.mlpack
@@ -11,6 +11,7 @@ SmtTrace
 SmtCnf
 SatAtom
 SmtAtom
+SmtMaps
 
 SatParser
 ZchaffParser