Link equality on uninterpreted sorts with SMT equality (#86)

Equality is now treated from uninterpreted sorts, which makes them usable with tactics!
Closes #17
Closes #78

18 files changed, 683 insertions, 290 deletions

diff --git a/examples/Example.v b/examples/Example.v
index 2d48776..628811c 100644
--- a/examples/Example.v
+++ b/examples/Example.v
@@ -111,8 +111,9 @@ Proof.
 Qed.
 
 
-(*Some examples of using verit with lemmas. Use <verit H1 .. Hn>
-  to temporarily add the lemmas H1 .. Hn to the verit environment. *)
+(* Some examples of using verit with lemmas. Use <verit H1 .. Hn> to
+   temporarily add the lemmas H1 .. Hn to the verit environment.
+ *)
 
 Lemma const_fun_is_eq_val_0 :
   forall f : Z -> Z,
@@ -134,6 +135,7 @@ Section With_lemmas.
 End With_lemmas.
 
 (* Instantiating a lemma with multiple quantifiers *)
+
 Section NonLinear.
   Lemma distr_right_inst a b (mult : Z -> Z -> Z) :
     (forall x y z, mult (x + y)  z =? mult x z + mult y z) ->
@@ -207,8 +209,22 @@ Proof.
   smt.
 Qed.
 
+Goal forall (a b: farray Z Z) (v w x y z t: Z)
+            (r s: bitvector 4)
+            (f: Z -> Z)
+            (g: farray Z Z -> Z)
+            (h: bitvector 4 -> Z),
+    a[x <- v] = b /\ a[y <- w] = b ->
+    a[z <- w] = b /\ a[t <- v] = b ->
+    r = s -> v < x + 10 /\ v > x - 5 ->
+    ~ (g a = g b) \/ f (h r) = f (h s).
+Proof.
+  smt.
+Qed.
+
+
 (* All tactics have a "no_check" variant that is faster but, in case of
-  failure, it will only fail at Qed *)
+   failure, it will only fail at Qed *)
 
 Goal forall (bv1 bv2 bv3: bitvector 4),
     bv1 = #b|0|0|0|0|  /\
@@ -219,16 +235,6 @@ Proof.
   smt_no_check.
 Qed.
 
-(* From cvc4_bool : Uncaught exception Not_found *)
-(* Goal forall (a b c d: farray Z Z), *)
-(*     b[0 <- 4] = c  -> *)
-(*     d = b[0 <- 4][1 <- 4]  -> *)
-(*     a = d[1 <- b[1]]  -> *)
-(*     a = c. *)
-(* Proof. *)
-(*   smt. *)
-(* Qed. *)
-
 Goal forall (a b: farray Z Z) (v w x y z t: Z)
             (r s: bitvector 4)
             (f: Z -> Z)
@@ -239,7 +245,7 @@ Goal forall (a b: farray Z Z) (v w x y z t: Z)
     r = s -> v < x + 10 /\ v > x - 5 ->
     ~ (g a = g b) \/ f (h r) = f (h s).
 Proof.
-  smt.
+  smt_no_check.
 Qed.
 
 
@@ -332,46 +338,51 @@ Open Scope Z_scope.
 (** Now more insightful examples. The first one automatically proves
     properties in group theory. **)
 
-Section group.
-  Variable op : Z -> Z -> Z.
-  Variable inv : Z -> Z.
-  Variable e : Z.
+Section Group.
+  Variable G : Type.
+  (* We suppose that G has a decidable equality *)
+  Variable HG : CompDec G.
+  Variable op : G -> G -> G.
+  Variable inv : G -> G.
+  Variable e : G.
+
+  Local Notation "a ==? b" := (@eqb_of_compdec G HG a b) (at level 60).
 
   (* We can prove automatically that we have a group if we only have the
      "left" versions of the axioms of a group *)
   Hypothesis associative :
-    forall a b c : Z, op a (op b c) =? op (op a b) c.
+    forall a b c : G, op a (op b c) ==? op (op a b) c.
   Hypothesis inverse :
-    forall a : Z, (op (inv a) a =? e).
+    forall a : G, op (inv a) a ==? e.
   Hypothesis identity :
-    forall a : Z, (op e a =? a).
-  Add_lemmas associative identity inverse.
+    forall a : G, op e a ==? a.
+  Add_lemmas associative inverse identity.
 
   (* The "right" version of inverse *)
   Lemma inverse' :
-    forall a : Z, (op a (inv a) =? e).
+    forall a : G, op a (inv a) ==? e.
   Proof. smt. Qed.
 
   (* The "right" version of identity *)
   Lemma identity' :
-    forall a : Z, (op a e =? a).
+    forall a : G, op a e ==? a.
   Proof. smt inverse'. Qed.
 
   (* Some other interesting facts about groups *)
   Lemma unique_identity e':
-    (forall z, op e' z =? z) -> e' =? e.
+    (forall z, op e' z ==? z) -> e' ==? e.
   Proof. intros pe'; smt pe'. Qed.
 
   Lemma simplification_right x1 x2 y:
-      op x1 y =? op x2 y -> x1 =? x2.
+      op x1 y ==? op x2 y -> x1 ==? x2.
   Proof. intro H. smt_no_check H inverse'. Qed.
 
   Lemma simplification_left x1 x2 y:
-      op y x1 =? op y x2 -> x1 =? x2.
+      op y x1 ==? op y x2 -> x1 ==? x2.
   Proof. intro H. smt_no_check H inverse'. Qed.
 
   Clear_lemmas.
-End group.
+End Group.
 
 
 (* A full example coming from CompCert, slightly revisited.
@@ -380,20 +391,23 @@ End group.
  *)
 Section CompCert.
 
-  Definition block := Z.
+  Variable block : Set.
+  Hypothesis eq_block : CompDec block.
+  Local Notation "a ==? b" := (@eqb_of_compdec block eq_block a b) (at level 60).
+
   Variable mem: Set.
-  Variable dec_mem : CompDec mem.
+  Hypothesis dec_mem : CompDec mem.
   Variable alloc_block: mem -> Z -> Z -> block.
   Variable alloc_mem: mem -> Z -> Z -> mem.
   Variable valid_block: mem -> block -> bool.
 
   Hypothesis alloc_valid_block_1:
     forall m lo hi b,
-      valid_block (alloc_mem m lo hi) b ---> ((b =? (alloc_block m lo hi)) || valid_block m b).
+      valid_block (alloc_mem m lo hi) b ---> ((b ==? (alloc_block m lo hi)) || valid_block m b).
 
   Hypothesis alloc_valid_block_2:
     forall m lo hi b,
-      ((b =? (alloc_block m lo hi)) || valid_block m b) ---> valid_block (alloc_mem m lo hi) b.
+      ((b ==? (alloc_block m lo hi)) || valid_block m b) ---> valid_block (alloc_mem m lo hi) b.
 
   Hypothesis alloc_not_valid_block:
     forall m lo hi,
@@ -402,13 +416,13 @@ Section CompCert.
   Lemma alloc_valid_block_inv m lo hi b :
     valid_block m b -> valid_block (alloc_mem m lo hi) b.
   Proof.
-    intro H. unfold block in *. verit alloc_valid_block_2 H.
+    intro H. verit alloc_valid_block_2 H.
   Qed.
 
   Lemma alloc_not_valid_block_2 m lo hi b' :
-    valid_block m b' -> b' =? (alloc_block m lo hi) = false.
+    valid_block m b' -> b' ==? (alloc_block m lo hi) = false.
   Proof.
-    intro H. unfold block in *. verit alloc_not_valid_block H.
+    intro H. verit alloc_not_valid_block H.
   Qed.
 
 End CompCert.
diff --git a/src/PropToBool.v b/src/PropToBool.v
index 393f835..a9cbded 100644
--- a/src/PropToBool.v
+++ b/src/PropToBool.v
@@ -18,16 +18,12 @@ Import BVList.BITVECTOR_LIST.
 Ltac prop2bool :=
   repeat
     match goal with
-    | [ |- forall _ : bitvector _, _] => intro
-    | [ |- forall _ : farray _ _, _] => intro
-    | [ |- forall _ : _ -> _, _] => intro
-    | [ |- forall _ : Z, _] => intro
-    | [ |- forall _ : bool, _] => intro
-    | [ |- forall _ : Type, _] => intro
-    | [ p: (CompDec ?t) |-  context[ forall _ : ?t, _ ] ] => intro
+    | [ |- forall _ : ?t, _ ] =>
+      lazymatch type of t with
+      | Prop => fail
+      | _ => intro
+      end
 
-    | [ |- forall t : Type, CompDec t -> _  ] => intro
-    | [ |- CompDec _ -> _  ] => intro
     | [ |- context[ bv_ultP _ _ ] ] => rewrite <- bv_ult_B2P
     | [ |- context[ bv_sltP _ _ ] ] => rewrite <- bv_slt_B2P
     | [ |- context[ Z.lt _ _ ] ] => rewrite <- Z.ltb_lt
@@ -36,22 +32,24 @@ Ltac prop2bool :=
     | [ |- context[ Z.ge _ _ ] ] => rewrite Z.ge_le_iff; rewrite <- Z.leb_le
     | [ |- context[ Z.eq _ _ ] ] => rewrite <- Z.eqb_eq
 
-    | [ p: (CompDec ?t) |- context[ @Logic.eq ?t _ _ ] ] =>
-      pose proof p as p0;
-      rewrite (@compdec_eq_eqb _ p0);
-      destruct p0;
-      try exact p
-
-    | [ Eqb : (EqbType ?ty)  |- _ ] => destruct Eqb; simpl
-
-    | [ |- context[ @Logic.eq (bitvector _) _ _ ] ] =>
-      rewrite <- bv_eq_reflect
-
-    | [ |- context[ @Logic.eq (farray _ _) _ _ ] ] =>
-      rewrite <- equal_iff_eq
-
-    | [ |- context[ @Logic.eq Z _ _ ] ] =>
-      rewrite <- Z.eqb_eq
+    | [ |- context[ @Logic.eq ?t _ _ ] ] =>
+      lazymatch t with
+      | bitvector _ => rewrite <- bv_eq_reflect
+      | farray _ _ => rewrite <- equal_iff_eq
+      | Z => rewrite <- Z.eqb_eq
+      | bool => fail
+      | _ =>
+        lazymatch goal with
+        | [ p: (CompDec t) |- _ ] =>
+          rewrite (@compdec_eq_eqb _ p)
+        | _ =>
+          let p := fresh "p" in
+          assert (p:CompDec t);
+          [ auto with typeclass_instances
+          | rewrite (@compdec_eq_eqb _ p)
+          ]
+        end
+      end
 
     | [ |- context[?G0 = true \/ ?G1 = true ] ] =>
       rewrite (@reflect_iff (G0 = true \/ G1 = true) (orb G0 G1));
diff --git a/src/QInst.v b/src/QInst.v
index 724a482..bb2cfd1 100644
--- a/src/QInst.v
+++ b/src/QInst.v
@@ -11,7 +11,7 @@
 
 
 Require Import Bool ZArith.
-Require Import State.
+Require Import State SMT_classes.
 
 
 (** Handling quantifiers with veriT **)
@@ -47,28 +47,72 @@ 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 : Z) := (a =? b)%Z.
-Ltac all_rew :=
+Lemma eqb_of_compdec_sym (A:Type) (HA:CompDec A) (a b:A) :
+  eqb_of_compdec HA b a = eqb_of_compdec HA a b.
+Proof.
+  destruct (@eq_dec _ (@Decidable _ HA) a b) as [H|H].
+  - now rewrite H.
+  - case_eq (eqb_of_compdec HA a b).
+    + now rewrite <- !(@compdec_eq_eqb _ HA).
+    + intros _. case_eq (eqb_of_compdec HA b a); auto.
+      intro H1. elim H. symmetry. now rewrite compdec_eq_eqb.
+Qed.
+
+Definition hidden_eq_Z (a b : Z) := (a =? b)%Z.
+Definition hidden_eq_U (A:Type) (HA:CompDec A) (a b : A) := eqb_of_compdec HA a b.
+Ltac apply_sym_hyp T :=
+  repeat match T with
+         | context [ (?A =? ?B)%Z] =>
+           change (A =? B)%Z with (hidden_eq_Z A B) in T
+         end;
+  repeat match T with
+         | context [ @eqb_of_compdec ?A ?HA ?a ?b ] =>
+           change (eqb_of_compdec HA a b) with (hidden_eq_U A HA a b) in T
+         end;
+  repeat match T with
+         | context [ hidden_eq_Z ?A ?B] =>
+           replace (hidden_eq_Z A B) with (B =? A)%Z in T;
+           [ | now rewrite Z.eqb_sym]
+         end;
+  repeat match T with
+         | context [ hidden_eq_U ?A ?HA ?a ?b] =>
+           replace (hidden_eq_U A HA a b) with (eqb_of_compdec HA b a) in T;
+           [ | now rewrite eqb_of_compdec_sym]
+         end.
+Ltac apply_sym_goal :=
+  repeat match goal with
+         | [ |- context [ (?A =? ?B)%Z] ] =>
+           change (A =? B)%Z with (hidden_eq_Z A B)
+         end;
   repeat match goal with
-         | [ |- context [ (?A =? ?B)%Z]] =>
-           change (A =? B)%Z with (hidden_eq A B)
+         | [ |- context [ @eqb_of_compdec ?A ?HA ?a ?b ] ] =>
+           change (eqb_of_compdec HA a b) with (hidden_eq_U A HA a b)
          end;
   repeat match goal with
-         | [ |- context [ hidden_eq ?A ?B] ] =>
-           replace (hidden_eq A B) with (B =? A)%Z;
+         | [ |- context [ hidden_eq_Z ?A ?B] ] =>
+           replace (hidden_eq_Z A B) with (B =? A)%Z;
            [ | now rewrite Z.eqb_sym]
+         end;
+  repeat match goal with
+         | [ |- context [ hidden_eq_U ?A ?HA ?a ?b] ] =>
+           replace (hidden_eq_U A HA a b) with (eqb_of_compdec HA b a);
+           [ | now rewrite eqb_of_compdec_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);
+       intro H;
+       try apply H;
+       try (apply_sym_goal; apply H);
+       try (apply_sym_hyp H; apply H);
+       try (apply_sym_goal; apply_sym_hyp H; 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);
+       end
+      );
   auto.
 
 
diff --git a/src/lfsc/tosmtcoq.ml b/src/lfsc/tosmtcoq.ml
index 6382e9e..0719803 100644
--- a/src/lfsc/tosmtcoq.ml
+++ b/src/lfsc/tosmtcoq.ml
@@ -244,7 +244,7 @@ let rec term_smtcoq_old t =
       | 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
-        Form.Atom (Atom.mk_eq ra (Atom.type_of h1) h1 h2)
+        Form.Atom (Atom.mk_eq_sym 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 ->
diff --git a/src/smtlib2/smtlib2_genConstr.ml b/src/smtlib2/smtlib2_genConstr.ml
index f938671..3df6a92 100644
--- a/src/smtlib2/smtlib2_genConstr.ml
+++ b/src/smtlib2/smtlib2_genConstr.ml
@@ -101,8 +101,7 @@ let declare_sort_from_name rt s =
   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
+  let res = SmtBtype.of_coq_compdec rt cons_t compdec_var in
   SmtMaps.add_btype s res;
   res
 
@@ -190,7 +189,7 @@ let make_root ra rf t =
       | "=", [a;b] ->
         (match make_root_term a, make_root_term b with
          | Atom a', Atom b' when Atom.type_of a' <> Tbool ->
-           Atom (Atom.mk_eq ra (Atom.type_of a') a' b')
+           Atom (Atom.mk_eq_sym ra (Atom.type_of a') a' b')
          | _ -> Form (Form.get rf (Fapp (Fiff, [|make_root a; make_root b|])))
         )
       | "<", [a;b] ->
diff --git a/src/trace/smtAtom.ml b/src/trace/smtAtom.ml
index 121e705..62cbe99 100644
--- a/src/trace/smtAtom.ml
+++ b/src/trace/smtAtom.ml
@@ -12,7 +12,24 @@
 
 open SmtMisc
 open CoqTerms
-open SmtBtype
+
+
+(** Hashing functions on Btypes *)
+
+module HashBtype = Hashtbl.Make(SmtBtype.HashedBtype)
+
+module HashedBtypePair : Hashtbl.HashedType
+       with type t = SmtBtype.btype * SmtBtype.btype = struct
+  type t = SmtBtype.btype * SmtBtype.btype
+
+  let equal (t1,s1) (t2,s2) =
+    SmtBtype.HashedBtype.equal t1 t2 && SmtBtype.HashedBtype.equal s1 s2
+
+  let hash (t,s) =
+    ((SmtBtype.HashedBtype.hash t) lsl 3) land (SmtBtype.HashedBtype.hash s)
+end
+
+module HashBtypePair = Hashtbl.Make(HashedBtypePair)
 
 
 (** Operators *)
@@ -43,7 +60,7 @@ type bop =
    | BO_Zle
    | BO_Zge
    | BO_Zgt
-   | BO_eq of btype
+   | BO_eq of SmtBtype.btype
    | BO_BVand of int
    | BO_BVor of int
    | BO_BVxor of int
@@ -54,20 +71,20 @@ type bop =
    | BO_BVconcat of int * int
    | BO_BVshl of int
    | BO_BVshr of int
-   | BO_select of btype * btype
-   | BO_diffarray of btype * btype
+   | BO_select of SmtBtype.btype * SmtBtype.btype
+   | BO_diffarray of SmtBtype.btype * SmtBtype.btype
 
 
 type top =
-  | TO_store of btype * btype
+  | TO_store of SmtBtype.btype * SmtBtype.btype
 
 
 type nop =
-  | NO_distinct of btype
+  | NO_distinct of SmtBtype.btype
 
 type op_def = {
-    tparams : btype array;
-    tres : btype;
+    tparams : SmtBtype.btype array;
+    tres : SmtBtype.btype;
     op_val : Structures.constr }
 
 type index = Index of int
@@ -97,9 +114,9 @@ module Op =
       | CO_BV bv -> mklApp cCO_BV [|mk_bv_list bv; mkN (List.length bv)|]
 
     let c_type_of = function
-      | CO_xH -> Tpositive
-      | CO_Z0 -> TZ
-      | CO_BV bv -> TBV (List.length bv)
+      | CO_xH -> SmtBtype.Tpositive
+      | CO_Z0 -> SmtBtype.TZ
+      | CO_BV bv -> SmtBtype.TBV (List.length bv)
 
     let interp_cop = function
       | CO_xH -> Lazy.force cxH
@@ -120,20 +137,20 @@ module Op =
       | UO_BVsextn (s, n) -> mklApp cUO_BVsextn [|mkN s; mkN n|]
 
     let u_type_of = function
-      | UO_xO | UO_xI -> Tpositive
-      | UO_Zpos | UO_Zneg | UO_Zopp -> TZ
-      | UO_BVbitOf _ -> Tbool
-      | UO_BVnot s | UO_BVneg s -> TBV s
-      | UO_BVextr (_, n, _) -> TBV n
-      | UO_BVzextn (s, n) | UO_BVsextn (s, n) -> TBV (s + n)
+      | UO_xO | UO_xI -> SmtBtype.Tpositive
+      | UO_Zpos | UO_Zneg | UO_Zopp -> SmtBtype.TZ
+      | UO_BVbitOf _ -> SmtBtype.Tbool
+      | UO_BVnot s | UO_BVneg s -> SmtBtype.TBV s
+      | UO_BVextr (_, n, _) -> SmtBtype.TBV n
+      | UO_BVzextn (s, n) | UO_BVsextn (s, n) -> SmtBtype.TBV (s + n)
 
     let u_type_arg = function
-      | UO_xO | UO_xI | UO_Zpos | UO_Zneg -> Tpositive
-      | UO_Zopp -> TZ
-      | UO_BVbitOf (s,_) -> TBV s
-      | UO_BVnot s | UO_BVneg s -> TBV s
-      | UO_BVextr (_, _, s) -> TBV s
-      | UO_BVzextn (s, _) | UO_BVsextn (s, _) -> TBV s
+      | UO_xO | UO_xI | UO_Zpos | UO_Zneg -> SmtBtype.Tpositive
+      | UO_Zopp -> SmtBtype.TZ
+      | UO_BVbitOf (s,_) -> SmtBtype.TBV s
+      | UO_BVnot s | UO_BVneg s -> SmtBtype.TBV s
+      | UO_BVextr (_, _, s) -> SmtBtype.TBV s
+      | UO_BVzextn (s, _) | UO_BVsextn (s, _) -> SmtBtype.TBV s
 
 
     let interp_uop = function
@@ -149,37 +166,37 @@ module Op =
       | UO_BVzextn (s, n) -> mklApp cbv_zextn [|mkN s; mkN n|]
       | UO_BVsextn (s, n) -> mklApp cbv_sextn [|mkN s; mkN n|]
 
-    let eq_tbl = Hashtbl.create 17
-    let select_tbl = Hashtbl.create 17
-    let store_tbl = Hashtbl.create 17
-    let diffarray_tbl = Hashtbl.create 17
+    let eq_tbl = HashBtype.create 17
+    let select_tbl = HashBtypePair.create 17
+    let store_tbl = HashBtypePair.create 17
+    let diffarray_tbl = HashBtypePair.create 17
 
     let eq_to_coq t =
-      try Hashtbl.find eq_tbl t
+      try HashBtype.find eq_tbl t
       with Not_found ->
 	let op = mklApp cBO_eq [|SmtBtype.to_coq t|] in
-	Hashtbl.add eq_tbl t op;
+	HashBtype.add eq_tbl t op;
 	op
 
     let select_to_coq ti te =
-      try Hashtbl.find select_tbl (ti, te)
+      try HashBtypePair.find select_tbl (ti, te)
       with Not_found ->
         let op = mklApp cBO_select [|SmtBtype.to_coq ti; SmtBtype.to_coq te|] in
-        Hashtbl.add select_tbl (ti, te) op;
+        HashBtypePair.add select_tbl (ti, te) op;
         op
 
     let store_to_coq ti te =
-      try Hashtbl.find store_tbl (ti, te)
+      try HashBtypePair.find store_tbl (ti, te)
       with Not_found ->
         let op = mklApp cTO_store [|SmtBtype.to_coq ti; SmtBtype.to_coq te|] in
-        Hashtbl.add store_tbl (ti, te) op;
+        HashBtypePair.add store_tbl (ti, te) op;
         op
 
     let diffarray_to_coq ti te =
-      try Hashtbl.find diffarray_tbl (ti, te)
+      try HashBtypePair.find diffarray_tbl (ti, te)
       with Not_found ->
         let op = mklApp cBO_diffarray [|SmtBtype.to_coq ti; SmtBtype.to_coq te|] in
-        Hashtbl.add diffarray_tbl (ti, te) op;
+        HashBtypePair.add diffarray_tbl (ti, te) op;
         op
 
     let b_to_coq = function
@@ -205,25 +222,25 @@ module Op =
       | BO_diffarray (ti, te) -> diffarray_to_coq ti te
 
     let b_type_of = function
-      | BO_Zplus | BO_Zminus | BO_Zmult -> TZ
+      | BO_Zplus | BO_Zminus | BO_Zmult -> SmtBtype.TZ
       | BO_Zlt | BO_Zle | BO_Zge | BO_Zgt | BO_eq _
-      | BO_BVult _ | BO_BVslt _ -> Tbool
+      | BO_BVult _ | BO_BVslt _ -> SmtBtype.Tbool
       | BO_BVand s | BO_BVor s | BO_BVxor s | BO_BVadd s | BO_BVmult s
-      | BO_BVshl s | BO_BVshr s -> TBV s
-      | BO_BVconcat (s1, s2) -> TBV (s1 + s2)
+      | BO_BVshl s | BO_BVshr s -> SmtBtype.TBV s
+      | BO_BVconcat (s1, s2) -> SmtBtype.TBV (s1 + s2)
       | BO_select (_, te) -> te
       | BO_diffarray (ti, _) -> ti
 
     let b_type_args = function
       | BO_Zplus | BO_Zminus | BO_Zmult
-      | BO_Zlt | BO_Zle | BO_Zge | BO_Zgt -> (TZ,TZ)
+      | BO_Zlt | BO_Zle | BO_Zge | BO_Zgt -> (SmtBtype.TZ,SmtBtype.TZ)
       | BO_eq t -> (t,t)
       | BO_BVand s | BO_BVor s | BO_BVxor s | BO_BVadd s | BO_BVmult s
       | BO_BVult s | BO_BVslt s | BO_BVshl s | BO_BVshr s ->
-        (TBV s,TBV s)
-      | BO_BVconcat (s1, s2) -> (TBV s1, TBV s2)
-      | BO_select (ti, te) -> (TFArray (ti, te), ti)
-      | BO_diffarray (ti, te) -> (TFArray (ti, te), TFArray (ti, te))
+        (SmtBtype.TBV s,SmtBtype.TBV s)
+      | BO_BVconcat (s1, s2) -> (SmtBtype.TBV s1, SmtBtype.TBV s2)
+      | BO_select (ti, te) -> (SmtBtype.TFArray (ti, te), ti)
+      | BO_diffarray (ti, te) -> (SmtBtype.TFArray (ti, te), SmtBtype.TFArray (ti, te))
 
 
     (* let interp_ieq t_i t =
@@ -270,14 +287,15 @@ module Op =
 
 
     let interp_eq t_i = function
-      | TZ -> Lazy.force ceqbZ
-      | Tbool -> Lazy.force ceqb
-      | Tpositive -> Lazy.force ceqbP
-      | TBV s -> mklApp cbv_eq [|mkN s|]
-      | Tindex i ->
-        mklApp ceqb_of_compdec [|mklApp cte_carrier [|i.hval|];
-                                 mklApp cte_compdec [|i.hval|]|]
-      | TFArray (ti, te) -> interp_eqarray t_i ti te
+      | SmtBtype.TZ -> Lazy.force ceqbZ
+      | SmtBtype.Tbool -> Lazy.force ceqb
+      | SmtBtype.Tpositive -> Lazy.force ceqbP
+      | SmtBtype.TBV s -> mklApp cbv_eq [|mkN s|]
+      | SmtBtype.Tindex i ->
+         let compdec = SmtBtype.indexed_type_compdec i in
+         mklApp ceqb_of_compdec [|mklApp cte_carrier [|compdec|];
+                                  mklApp cte_compdec [|compdec|]|]
+      | SmtBtype.TFArray (ti, te) -> interp_eqarray t_i ti te
 
 
 
@@ -307,10 +325,10 @@ module Op =
       | TO_store (ti, te) -> store_to_coq ti te
 
     let t_type_of = function
-      | TO_store (ti, te) -> TFArray (ti, te)
+      | TO_store (ti, te) -> SmtBtype.TFArray (ti, te)
 
     let t_type_args = function
-      | TO_store (ti, te) -> TFArray (ti, te), ti, te
+      | TO_store (ti, te) -> SmtBtype.TFArray (ti, te), ti, te
 
     let interp_top t_i = function
       | TO_store (ti, te) -> interp_store t_i ti te
@@ -320,7 +338,7 @@ module Op =
       | NO_distinct t -> mklApp cNO_distinct [|SmtBtype.to_coq t|]
 
     let n_type_of = function
-      | NO_distinct _ -> Tbool
+      | NO_distinct _ -> SmtBtype.Tbool
 
     let n_type_args = function
       | NO_distinct ty -> ty
@@ -362,7 +380,7 @@ module Op =
 
     let interp_tbl tval mk_Tval reify =
       let t = Array.make (reify.count + 1)
-	        (mk_Tval [||] Tbool (Lazy.force ctrue)) in
+	        (mk_Tval [||] SmtBtype.Tbool (Lazy.force ctrue)) 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
@@ -381,6 +399,11 @@ module Op =
          | Invalid_argument _ -> false)
       | _ -> op1 == op2
 
+    let c_hash = function
+      | CO_xH -> 1
+      | CO_Z0 -> 2
+      | CO_BV l -> 3 + (List.fold_left (fun acc b -> if b then 2*acc+1 else 2*acc) 0 l)
+
     let u_equal op1 op2 =
       match op1,op2 with
       | UO_xO, UO_xO
@@ -397,9 +420,22 @@ module Op =
       | UO_BVsextn (s1, n1), UO_BVsextn (s2, n2) -> s1 == s2 && n1 == n2
       | _ -> false
 
+    let u_hash = function
+      | UO_xO -> 0
+      | UO_xI -> 1
+      | UO_Zpos -> 2
+      | UO_Zneg -> 3
+      | UO_Zopp -> 4
+      | UO_BVbitOf (s,n) -> (n land s) lxor 5
+      | UO_BVnot s -> s lxor 6
+      | UO_BVneg s -> s lxor 7
+      | UO_BVextr (s, n0, n1) -> (s land n0 land n1) lxor 8
+      | UO_BVzextn (s, n) -> (s land n) lxor 9
+      | UO_BVsextn (s, n) -> (s land n) lxor 10
+
     let b_equal op1 op2 =
       match op1,op2 with
-        | BO_eq t1, BO_eq t2 -> SmtBtype.equal t1 t2
+        | BO_eq t1, BO_eq t2 -> SmtBtype.HashedBtype.equal t1 t2
         | BO_BVand n1, BO_BVand n2 -> n1 == n2
         | BO_BVor n1, BO_BVor n2 -> n1 == n2
         | BO_BVxor n1, BO_BVxor n2 -> n1 == n2
@@ -412,17 +448,45 @@ module Op =
         | BO_BVshr n1, BO_BVshr n2 -> n1 == n2
         | BO_select (ti1, te1), BO_select (ti2, te2)
         | BO_diffarray (ti1, te1), BO_diffarray (ti2, te2) ->
-          SmtBtype.equal ti1 ti2 && SmtBtype.equal te1 te2
+           HashedBtypePair.equal (ti1, te1) (ti2, te2)
         | _ -> op1 == op2
 
+    let b_hash = function
+      | BO_Zplus -> 1
+      | BO_Zminus -> 2
+      | BO_Zmult -> 3
+      | BO_Zlt -> 4
+      | BO_Zle -> 5
+      | BO_Zge -> 6
+      | BO_Zgt -> 7
+      | BO_eq ty -> ((SmtBtype.HashedBtype.hash ty) lsl 6) lxor 8
+      | BO_BVand s -> s lxor 9
+      | BO_BVor s -> s lxor 10
+      | BO_BVxor s -> s lxor 11
+      | BO_BVadd s -> s lxor 12
+      | BO_BVmult s -> s lxor 13
+      | BO_BVult s -> s lxor 14
+      | BO_BVslt s -> s lxor 15
+      | BO_BVconcat (s1,s2) -> (s1 land s2) lxor 16
+      | BO_BVshl s -> s lxor 17
+      | BO_BVshr s -> s lxor 18
+      | BO_select (ti, te) -> ((HashedBtypePair.hash (ti, te)) lsl 6) lxor 19
+      | BO_diffarray (ti, te) -> ((HashedBtypePair.hash (ti, te)) lsl 6) lxor 20
+
     let t_equal op1 op2 =
       match op1,op2 with
         | TO_store (ti1, te1), TO_store (ti2, te2) ->
-          SmtBtype.equal ti1 ti2 && SmtBtype.equal te1 te2
+          SmtBtype.HashedBtype.equal ti1 ti2 && SmtBtype.HashedBtype.equal te1 te2
+
+    let t_hash = function
+      | TO_store (ti, te) -> HashedBtypePair.hash (ti, te)
 
     let n_equal op1 op2 =
       match op1,op2 with
-      | NO_distinct t1, NO_distinct t2 -> SmtBtype.equal t1 t2
+      | NO_distinct t1, NO_distinct t2 -> SmtBtype.HashedBtype.equal t1 t2
+
+    let n_hash = function
+      | NO_distinct t -> SmtBtype.HashedBtype.hash t
 
     let i_equal (i1, _) (i2, _) = i1 = i2
 
@@ -554,14 +618,14 @@ module HashedAtom =
       | _, _ -> false
 
     let hash = function
-      |	Acop op -> ((Hashtbl.hash op) lsl 3) lxor 1
+      |	Acop op -> ((Op.c_hash op) lsl 3) lxor 1
       | Auop (op,h) ->
-         (( (h.index lsl 3) + (Hashtbl.hash op)) lsl 3) lxor 2
+         (( (h.index lsl 3) + (Op.u_hash op)) lsl 3) lxor 2
       | Abop (op,h1,h2) ->
-        (((( (h1.index lsl 2) + h2.index) lsl 3) + Hashtbl.hash op) lsl 3) lxor 3
+        (((( (h1.index lsl 2) + h2.index) lsl 3) + Op.b_hash op) lsl 3) lxor 3
       | Atop (op,h1,h2,h3) ->
         (((( ((h1.index lsl 2) + h2.index) lsl 3) + h3.index) lsl 4
-          + Hashtbl.hash op) lsl 4) lxor 4
+          + Op.t_hash op) lsl 4) lxor 4
       | Anop (op, args) ->
           let hash_args =
             match Array.length args with
@@ -570,7 +634,7 @@ module HashedAtom =
             | 2 -> args.(1).index lsl 2 + args.(0).index
             | _ -> args.(2).index lsl 4 + args.(1).index lsl 2 + args.(0).index
           in
-          (hash_args lsl 5 + (Hashtbl.hash op) lsl 3) lxor 4
+          (hash_args lsl 5 + (Op.n_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 =
@@ -607,8 +671,8 @@ module Atom =
       | Anop (op,_) -> Op.n_type_of op
       | Aapp (op,_) -> Op.i_type_of op
 
-    let is_bool_type h = SmtBtype.equal (type_of h) Tbool
-    let is_bv_type h = match type_of h with | TBV _ -> true | _ -> false
+    let is_bool_type h = SmtBtype.HashedBtype.equal (type_of h) SmtBtype.Tbool
+    let is_bv_type h = match type_of h with | SmtBtype.TBV _ -> true | _ -> false
 
 
     let rec compute_int = function
@@ -782,9 +846,9 @@ module Atom =
 
       let check_one t h =
         let th = type_of h in
-        if SmtBtype.equal t th then
+        if SmtBtype.HashedBtype.equal t th then
           h
-        else if t == TZ && th == Tpositive then
+        else if t == SmtBtype.TZ && th == SmtBtype.Tpositive then
           (* Special case: the SMT solver cannot distinguish Z from
              positive, we have to add the injection back *)
           get reify (Auop(UO_Zpos, h))
@@ -822,7 +886,8 @@ module Atom =
       a
 
 
-    let mk_eq reify ?declare:(decl=true) ty h1 h2 =
+    (* Identifies two equalities modulo symmetry *)
+    let mk_eq_sym reify ?declare:(decl=true) ty h1 h2 =
       let op = BO_eq ty in
       try
         HashAtom.find reify.tbl (Abop (op, h1, h2))
@@ -841,23 +906,23 @@ module Atom =
           | _ -> failwith "opp not on Z" in
         get reify na
 
-    let rec hash_hatom ra' {index = _; hval = a} =
+    let rec hash_hatom ra_quant {index = _; hval = a} =
       match a with
-      | Acop cop -> get ra' a
-      | Auop (uop, ha) -> get ra' (Auop (uop, hash_hatom ra' ha))
+      | Acop cop -> get ra_quant a
+      | Auop (uop, ha) -> get ra_quant (Auop (uop, hash_hatom ra_quant ha))
       | Abop (bop, ha1, ha2) ->
-         let new_ha1 = hash_hatom ra' ha1 in
-         let new_ha2 = hash_hatom ra' ha2 in
+         let new_ha1 = hash_hatom ra_quant ha1 in
+         let new_ha2 = hash_hatom ra_quant ha2 in
          begin match bop with
-         | BO_eq ty -> mk_eq ra' ty new_ha1 new_ha2
-         | _ -> get ra' (Abop (bop, new_ha1, new_ha2)) end
+         | BO_eq ty -> mk_eq_sym ra_quant ty new_ha1 new_ha2
+         | _ -> get ra_quant (Abop (bop, new_ha1, new_ha2)) end
       | Atop (top, ha1, ha2, ha3) ->
-         let new_ha1 = hash_hatom ra' ha1 in
-         let new_ha2 = hash_hatom ra' ha2 in
-         let new_ha3 = hash_hatom ra' ha3 in
-         get ra' (Atop (top, new_ha1, new_ha2, new_ha3))
+         let new_ha1 = hash_hatom ra_quant ha1 in
+         let new_ha2 = hash_hatom ra_quant ha2 in
+         let new_ha3 = hash_hatom ra_quant ha3 in
+         get ra_quant (Atop (top, new_ha1, new_ha2, new_ha3))
       | Anop _ -> assert false
-      | Aapp (op, arr) -> get ra' (Aapp (op, Array.map (hash_hatom ra') arr))
+      | Aapp (op, arr) -> get ra_quant (Aapp (op, Array.map (hash_hatom ra_quant) arr))
 
     let copy {count=c; tbl=t} = {count = c; tbl = HashAtom.copy t}
 
@@ -908,11 +973,12 @@ module Atom =
       | CCBVzextn
       | CCBVshl
       | CCBVshr
-      | CCeqb
-      | CCeqbP
-      | CCeqbZ
-      | CCeqbBV
-      | CCeqbA
+      | CCeqb                   (* Equality on bool *)
+      | CCeqbP                  (* Equality on positive *)
+      | CCeqbZ                  (* Equality on Z *)
+      | CCeqbBV                 (* Equality on bit vectors *)
+      | CCeqbA                  (* Equality on arrays *)
+      | CCeqbU                  (* Equality on uninterpreted types *)
       | CCselect
       | CCdiff
       | CCstore
@@ -962,7 +1028,7 @@ module Atom =
       (* | CCeqbBV -> SL.singleton LBitvectors *)
       (* | CCeqbA -> SL.singleton LArrays *)
 
-      | CCeqbP | CCeqbZ | CCeqbBV | CCeqbA
+      | CCeqbP | CCeqbZ | CCeqbBV | CCeqbA | CCeqbU
       | CCunknown | CCunknown_deps _  -> SL.singleton LUF
 
 
@@ -994,7 +1060,7 @@ module Atom =
 
 
     let op_tbl () =
-      let tbl = Hashtbl.create 29 in
+      let tbl = Hashtbl.create 40 in
       let add (c1,c2) = Hashtbl.add tbl (Lazy.force c1) c2 in
       List.iter add
 	[ cxH,CCxH; cZ0,CCZ0; cof_bits, CCBV;
@@ -1007,7 +1073,7 @@ module Atom =
           cbv_add, CCBVadd; cbv_mult, CCBVmult;
           cbv_ult, CCBVult; cbv_slt, CCBVslt; cbv_concat, CCBVconcat;
           cbv_shl, CCBVshl; cbv_shr, CCBVshr;
-          ceqb,CCeqb; ceqbP,CCeqbP; ceqbZ, CCeqbZ; cbv_eq, CCeqbBV;
+          ceqb,CCeqb; ceqbP,CCeqbP; ceqbZ, CCeqbZ; cbv_eq, CCeqbBV; ceqb_of_compdec, CCeqbU;
           cselect, CCselect; cdiff, CCdiff;
           cstore, CCstore;
           cequalarray, CCeqbA;
@@ -1030,7 +1096,7 @@ module Atom =
       Hashtbl.find op_coq_terms
 
 
-    let of_coq ?hash:(hash=false) rt ro reify known_logic env sigma c =
+    let of_coq ?eqsym:(eqsym=false) rt ro reify known_logic env sigma c =
       let op_tbl = Lazy.force op_tbl in
       let get_cst c =
 	try
@@ -1073,11 +1139,12 @@ module Atom =
         | CCBVsextn -> mk_bvsextn args
         | CCBVshl -> mk_bop_bvshl args
         | CCBVshr -> mk_bop_bvshr args
-        | CCeqb -> mk_teq Tbool args
-        | CCeqbP -> mk_teq Tpositive args
-        | CCeqbZ -> mk_teq TZ args
+        | CCeqb -> mk_teq SmtBtype.Tbool args
+        | CCeqbP -> mk_teq SmtBtype.Tpositive args
+        | CCeqbZ -> mk_teq SmtBtype.TZ args
         | CCeqbA -> mk_bop_farray_equal args
         | CCeqbBV -> mk_bop_bveq args
+        | CCeqbU -> mk_bop_ueq args
         | CCselect -> mk_bop_select args
         | CCdiff -> mk_bop_diff args
         | CCstore -> mk_top_store args
@@ -1135,13 +1202,20 @@ module Atom =
         | _ -> assert false
 
       and mk_teq ty args =
-        if hash then match args with
+        if eqsym then match args with
                   | [a1; a2] -> let h1 = mk_hatom a1 in
                                 let h2 = mk_hatom a2 in
-                                mk_eq reify ty h1 h2
+                                mk_eq_sym reify ty h1 h2
                   | _ -> failwith "unexpected number of arguments for mk_teq"
         else mk_bop (BO_eq ty) args
 
+      and mk_bop_ueq args =
+        match args with
+          | t::compdec::args ->
+             let ty = SmtBtype.of_coq_compdec rt t compdec in
+             mk_teq ty args
+          | _ -> failwith "unexpected number of arguments for mk_bop_ueq"
+
       and mk_bop op = function
         | [a1;a2] ->
            let h1 = mk_hatom a1 in
@@ -1219,7 +1293,7 @@ module Atom =
       and mk_bop_bveq = function
         | [s;a1;a2] when SL.mem LBitvectors known_logic ->
           let s' = mk_bvsize s in
-          mk_teq (TBV s') [a1;a2]
+          mk_teq (SmtBtype.TBV s') [a1;a2]
         (* We still want to interpret bv equality as uninterpreted
            smtlib2 equality if the solver doesn't support bitvectors *)
         | [s;a1;a2] ->
@@ -1252,7 +1326,7 @@ module Atom =
         | [ti;te;_;_;_;_;_;a;b] when SL.mem LArrays known_logic ->
           let ti' = SmtBtype.of_coq rt known_logic ti in
           let te' = SmtBtype.of_coq rt known_logic te in
-          mk_teq (TFArray (ti', te')) [a; b]
+          mk_teq (SmtBtype.TFArray (ti', te')) [a; b]
         (* We still want to interpret array equality as uninterpreted
            smtlib2 equality if the solver doesn't support arrays *)
         | [ti;te;ord_ti;_;_;_;inh_te;a;b] ->
diff --git a/src/trace/smtAtom.mli b/src/trace/smtAtom.mli
index f076cb8..17a0cd0 100644
--- a/src/trace/smtAtom.mli
+++ b/src/trace/smtAtom.mli
@@ -140,7 +140,7 @@ module Atom :
       val print_atoms : reify_tbl -> string -> unit
 
       (** Given a coq term, build the corresponding atom *)
-      val of_coq : ?hash:bool -> SmtBtype.reify_tbl -> Op.reify_tbl ->
+      val of_coq : ?eqsym:bool -> SmtBtype.reify_tbl -> Op.reify_tbl ->
         reify_tbl -> SmtMisc.logic -> Environ.env -> Evd.evar_map -> Structures.constr -> t
 
       val get_coq_term_op : int -> Structures.constr
@@ -159,7 +159,7 @@ module Atom :
       (* Generation of atoms *)
       val hatom_Z_of_int : reify_tbl -> int -> t
       val hatom_Z_of_bigint : reify_tbl -> Big_int.big_int -> t
-      val mk_eq : reify_tbl -> ?declare:bool -> btype -> t -> t -> t
+      val mk_eq_sym : reify_tbl -> ?declare:bool -> btype -> t -> t -> t
       val mk_lt : reify_tbl -> ?declare:bool -> t -> t -> t
       val mk_le : reify_tbl -> ?declare:bool -> t -> t -> t
       val mk_gt : reify_tbl -> ?declare:bool -> t -> t -> t
diff --git a/src/trace/smtBtype.ml b/src/trace/smtBtype.ml
index 948acaa..3c4cd53 100644
--- a/src/trace/smtBtype.ml
+++ b/src/trace/smtBtype.ml
@@ -15,11 +15,28 @@ open CoqTerms
 
 (** Syntaxified version of Coq type *)
 
-type indexed_type = Structures.constr gen_hashed
-
-let dummy_indexed_type i = {index = i; hval = Structures.mkProp}
+type uninterpreted_type =
+  (* Uninterpreted type for which a CompDec is already known
+     The constr is of type typ_compdec
+   *)
+  | CompDec of Structures.constr
+  (* Uninterpreted type for which the knowledge of a CompDec is delayed
+     until either:
+     - one is used
+     - we have reached the end of the process and we generate a new one
+       via a cut
+     The constr is of type Type
+   *)
+  | Delayed of Structures.constr
+
+type indexed_type = uninterpreted_type gen_hashed
+
+let dummy_indexed_type i = {index = i; hval = Delayed (Structures.mkProp)}
 let indexed_type_index i = i.index
-let indexed_type_hval i = i.hval
+let indexed_type_compdec i =
+  match i.hval with
+    | CompDec compdec -> compdec
+    | Delayed _ -> assert false
 
 type btype =
   | TZ
@@ -39,14 +56,26 @@ let index_to_coq i =
     interp
 
 let indexed_type_of_int i =
-  {index = i; hval = index_to_coq i }
-
-let rec equal t1 t2 =
-  match t1,t2 with
-    | Tindex i, Tindex j -> i.index == j.index
-    | TBV i, TBV j -> i == j
-    | TFArray (ti, te), TFArray (ti', te') -> equal ti ti' && equal te te'
-    | _ -> t1 == t2
+  {index = i; hval = Delayed (index_to_coq i) }
+
+module HashedBtype : Hashtbl.HashedType with type t = btype = struct
+  type t = btype
+
+  let rec equal t1 t2 =
+    match t1,t2 with
+      | Tindex i, Tindex j -> i.index == j.index
+      | TBV i, TBV j -> i == j
+      | TFArray (ti, te), TFArray (ti', te') -> equal ti ti' && equal te te'
+      | _ -> t1 == t2
+
+  let rec hash = function
+    | TZ -> 1
+    | Tbool -> 2
+    | Tpositive -> 3
+    | TBV s -> s lxor 4
+    | TFArray (t1, t2) -> ((((hash t1) lsl 3) land (hash t2)) lsl 3) lxor 5
+    | Tindex i -> (i.index lsl 3) lxor 6
+end
 
 let rec to_coq = function
   | TZ -> Lazy.force cTZ
@@ -103,10 +132,24 @@ let get_coq_type_op = Hashtbl.find op_coq_types
 
 let interp_tbl reify =
   let t = Array.make (reify.count + 1) (Lazy.force cunit_typ_compdec) in
-  let set _ = function
-    | Tindex it -> t.(it.index) <- it.hval
-    | _ -> () in
-  Hashtbl.iter set reify.tbl;
+  let set c bt =
+    match bt with
+      | Tindex it ->
+         (match it.hval with
+            | CompDec compdec -> t.(it.index) <- compdec; Some bt
+            | Delayed ty ->
+               let n = string_of_int (List.length reify.cuts) in
+               let compdec_name = Structures.mkId ("CompDec"^n) in
+               let compdec_var = Structures.mkVar compdec_name in
+               let compdec_type = mklApp cCompDec [| ty |] in
+               reify.cuts <- (compdec_name, compdec_type) :: reify.cuts;
+               let ce = mklApp cTyp_compdec [|ty; compdec_var|] in
+               t.(it.index) <- ce;
+               Some (Tindex {index = it.index; hval = CompDec ce})
+         )
+      | _ -> Some bt
+  in
+  Hashtbl.filter_map_inplace set reify.tbl;
   Structures.mkArray (Lazy.force ctyp_compdec, t)
 
 
@@ -139,7 +182,11 @@ let rec interp t_i = function
   | Tbool -> Lazy.force cbool
   | Tpositive -> Lazy.force cpositive
   | TBV n -> mklApp cbitvector [|mkN n|]
-  | Tindex c -> mklApp cte_carrier [|c.hval|]
+  | Tindex c ->
+     (match c.hval with
+        | CompDec t -> mklApp cte_carrier [|t|]
+        | Delayed _ -> assert false
+     )
   (* | TFArray _ as t -> interp_t t_i t *)
   | TFArray (ti,te) ->
      mklApp cfarray [| interp t_i ti; interp t_i te;
@@ -150,14 +197,25 @@ let interp_to_coq reify t = interp (make_t_i reify) t
 
 let get_cuts reify = reify.cuts
 
-let declare reify t typ_compdec =
-  (* TODO: allows to have only typ_compdec *)
+let declare reify t typ_uninterpreted_type =
   assert (not (Hashtbl.mem reify.tbl t));
-  let res = Tindex {index = reify.count; hval = typ_compdec} in
+  let res = Tindex {index = reify.count; hval = typ_uninterpreted_type} in
   Hashtbl.add reify.tbl t res;
   reify.count <- reify.count + 1;
   res
 
+let declare_compdec reify t compdec =
+  let ce = mklApp cTyp_compdec [|t; compdec|] in
+  let ty = declare reify t (CompDec ce) in
+  (match ty with Tindex h -> Hashtbl.add op_coq_types h.index t | _ -> assert false);
+  ty
+
+let declare_delayed reify t delayed =
+  let ty = declare reify t (Delayed delayed) in
+  (match ty with Tindex h -> Hashtbl.add op_coq_types h.index t | _ -> assert false);
+  ty
+
+
 exception Unknown_type of btype
 
 let check_known ty known_logic =
@@ -175,24 +233,29 @@ let rec compdec_btype reify = function
        [|interp_to_coq reify ti; interp_to_coq reify te;
          compdec_btype reify ti; compdec_btype reify te|]
   | Tindex i ->
-     let c, args = Structures.decompose_app i.hval in
-     if Structures.eq_constr c (Lazy.force cTyp_compdec) then
-       match args with
-         | [_; tic] -> tic
-         | _ -> assert false
-     else assert false
+     (match i.hval with
+        | CompDec compdec ->
+           let c, args = Structures.decompose_app compdec in
+           if Structures.eq_constr c (Lazy.force cTyp_compdec) then
+             match args with
+               | [_; tic] -> tic
+               | _ -> assert false
+           else assert false
+        | _ -> assert false
+     )
 
 
 let declare_and_compdec reify t ty =
   try Hashtbl.find reify.unsup_tbl ty
   with Not_found ->
     let res =
-      declare reify t (mklApp cTyp_compdec [|t; compdec_btype reify ty|])
+      declare reify t (CompDec (mklApp cTyp_compdec [|t; compdec_btype reify ty|]))
     in
     Hashtbl.add reify.unsup_tbl ty res;
     res
 
 
+
 let rec of_coq reify known_logic t =
   try
     let c, args = Structures.decompose_app t in
@@ -220,16 +283,27 @@ let rec of_coq reify known_logic t =
     else
       try Hashtbl.find reify.tbl t
       with Not_found ->
-        let n = string_of_int (List.length reify.cuts) in
-        let compdec_name = Structures.mkId ("CompDec"^n) in
-        let compdec_var = Structures.mkVar compdec_name in
-        let compdec_type = mklApp cCompDec [| t |]in
-        reify.cuts <- (compdec_name, compdec_type) :: reify.cuts;
-        let ce = mklApp cTyp_compdec [|t; compdec_var|] in
-        let ty = declare reify t ce in
-        (match ty with Tindex h -> Hashtbl.add op_coq_types h.index t | _ -> assert false);
-        ty
+        declare_delayed reify t t
 
   with Unknown_type ty ->
     try Hashtbl.find reify.tbl t
     with Not_found -> declare_and_compdec reify t ty
+
+
+let of_coq_compdec reify t compdec =
+  try
+    let ty = Hashtbl.find reify.tbl t in
+    match ty with
+      | Tindex i ->
+         (match i.hval with
+            | CompDec _ -> ty
+            | Delayed _ ->
+               Hashtbl.remove reify.tbl t;
+               let ce = mklApp cTyp_compdec [|t; compdec|] in
+               let res = Tindex {index = i.index; hval = CompDec ce} in
+               Hashtbl.add reify.tbl t res;
+               res
+         )
+      | _ -> assert false
+  with Not_found ->
+    declare_compdec reify t compdec
diff --git a/src/trace/smtBtype.mli b/src/trace/smtBtype.mli
index 5d45ca4..5710cf3 100644
--- a/src/trace/smtBtype.mli
+++ b/src/trace/smtBtype.mli
@@ -13,11 +13,11 @@
 open SmtMisc
 
 
-type indexed_type = Structures.constr gen_hashed
+type indexed_type
 
 val dummy_indexed_type: int -> indexed_type
 val indexed_type_index : indexed_type -> int
-val indexed_type_hval : indexed_type -> Structures.constr
+val indexed_type_compdec : indexed_type -> Structures.constr
 
 type btype =
   | TZ
@@ -27,9 +27,9 @@ type btype =
   | TFArray of btype * btype
   | Tindex of indexed_type
 
-val indexed_type_of_int : int -> Structures.constr SmtMisc.gen_hashed
+val indexed_type_of_int : int -> indexed_type
 
-val equal : btype -> btype -> bool
+module HashedBtype : Hashtbl.HashedType with type t = btype
 
 val to_coq : btype -> Structures.constr
 
@@ -39,9 +39,8 @@ type reify_tbl
 
 val create : unit -> reify_tbl
 
-val declare : reify_tbl -> Structures.constr -> Structures.constr -> btype
-
 val of_coq : reify_tbl -> logic -> Structures.constr -> btype
+val of_coq_compdec : reify_tbl -> Structures.constr -> Structures.constr -> btype
 
 val get_coq_type_op : int -> Structures.constr
 
diff --git a/src/trace/smtCommands.ml b/src/trace/smtCommands.ml
index e64a131..6bd4829 100644
--- a/src/trace/smtCommands.ml
+++ b/src/trace/smtCommands.ml
@@ -672,18 +672,18 @@ let get_arguments concl =
   | _ -> failwith ("Verit.tactic: can only deal with equality over bool")
 
 
-let make_proof call_solver env rt ro ra' rf' l ls_smtc =
+let make_proof call_solver env rt ro ra_quant rf_quant l ls_smtc =
   let root = SmtTrace.mkRootV [l] in
-  call_solver env rt ro ra' rf' (root,l) ls_smtc
+  call_solver env rt ro ra_quant rf_quant (root,l) ls_smtc
 (* TODO: not generic anymore, the "lemma" part is currently specific to veriT *)
 
-(* <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_coq_lemma> reifies the given coq lemma, so we can then easily print it in a
+ .smt2 file. We need the reify tables to correctly recognize free 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 solver_logic clemma =
+let of_coq_lemma rt ro ra_quant rf_quant env sigma solver_logic 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 =
@@ -703,20 +703,20 @@ let of_coq_lemma rt ro ra' rf' env sigma solver_logic clemma =
          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' solver_logic env_lemma sigma)
-                   rf' core_f in
+  let core_smt = Form.of_coq (Atom.of_coq ~eqsym:true rt ro ra_quant solver_logic env_lemma sigma)
+                   rf_quant core_f in
   match forall_args with
     [] -> core_smt
-  | _ -> Form.get rf' (Fapp (Fforall forall_args, [|core_smt|]))
+  | _ -> Form.get rf_quant (Fapp (Fforall forall_args, [|core_smt|]))
 
-let core_tactic call_solver solver_logic rt ro ra rf ra' rf' vm_cast lcpl lcepl env sigma concl =
+let core_tactic call_solver solver_logic rt ro ra rf ra_quant rf_quant vm_cast 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 (Structures.retyping_get_type_of env sigma) lcpl in
 
-  let lsmt  = List.map (of_coq_lemma rt ro ra' rf' env sigma solver_logic) lcl in
+  let lsmt  = List.map (of_coq_lemma rt ro ra_quant rf_quant env sigma solver_logic) lcl in
   let l_pl_ls = List.combine (List.combine lcl lcpl) lsmt in
 
   let lem_tbl : (int, Structures.constr * Structures.constr) Hashtbl.t =
@@ -727,7 +727,7 @@ let core_tactic call_solver solver_logic rt ro ra rf ra' rf' vm_cast lcpl lcepl
   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
+    let re_hash hf = Form.hash_hform (Atom.hash_hatom ra_quant) rf_quant hf in
     match cl.value with
     | Some [l] ->
        let hl = re_hash l in
@@ -742,24 +742,24 @@ let core_tactic call_solver solver_logic rt ro ra rf ra' rf' vm_cast lcpl lcepl
 
   let (body_cast, body_nocast, cuts) =
     if ((Structures.eq_constr b (Lazy.force ctrue)) ||
-        (Structures.eq_constr b (Lazy.force cfalse))) then
+        (Structures.eq_constr b (Lazy.force cfalse))) then (
       let l = Form.of_coq (Atom.of_coq rt ro ra solver_logic env sigma) rf a in
+      let _ = Form.of_coq (Atom.of_coq ~eqsym:true rt ro ra_quant solver_logic env sigma) rf_quant a in
       let nl = if (Structures.eq_constr b (Lazy.force ctrue)) then Form.neg l else l in
-      let _ = Form.of_coq (Atom.of_coq ~hash:true rt ro ra' solver_logic env sigma) rf' a in
       let lsmt = Form.flatten rf nl :: lsmt in
-      let max_id_confl = make_proof call_solver env rt ro ra' rf' nl lsmt in
+      let max_id_confl = make_proof call_solver env rt ro ra_quant rf_quant nl lsmt in
       build_body rt ro ra rf (Form.to_coq l) b max_id_confl (vm_cast env) (Some find_lemma)
-    else
+    ) else (
       let l1 = Form.of_coq (Atom.of_coq rt ro ra solver_logic env sigma) rf a in
-      let _ = Form.of_coq (Atom.of_coq ~hash:true rt ro ra' solver_logic env sigma) rf' a in
+      let _ = Form.of_coq (Atom.of_coq ~eqsym:true rt ro ra_quant solver_logic env sigma) rf_quant a in
       let l2 = Form.of_coq (Atom.of_coq rt ro ra solver_logic env sigma) rf b in
-      let _ = Form.of_coq (Atom.of_coq ~hash:true rt ro ra' solver_logic env sigma) rf' b in
+      let _ = Form.of_coq (Atom.of_coq ~eqsym:true rt ro ra_quant solver_logic env sigma) rf_quant b in
       let l = Form.get rf (Fapp(Fiff,[|l1;l2|])) in
       let nl = Form.neg l in
       let lsmt = Form.flatten rf nl :: lsmt in
-      let max_id_confl = make_proof call_solver env rt ro ra' rf' nl lsmt in
+      let max_id_confl = make_proof call_solver env rt ro ra_quant rf_quant nl lsmt in
       build_body_eq rt ro ra rf (Form.to_coq l1) (Form.to_coq l2)
-        (Form.to_coq nl) max_id_confl (vm_cast env) (Some find_lemma) in
+        (Form.to_coq nl) max_id_confl (vm_cast env) (Some find_lemma) ) in
 
       let cuts = (SmtBtype.get_cuts rt) @ cuts in
 
@@ -773,10 +773,10 @@ let core_tactic call_solver solver_logic rt ro ra rf ra' rf' vm_cast lcpl lcepl
        (Structures.vm_cast_no_check body_cast))
 
 
-let tactic call_solver solver_logic rt ro ra rf ra' rf' vm_cast lcpl lcepl =
+let tactic call_solver solver_logic rt ro ra rf ra_quant rf_quant vm_cast lcpl lcepl =
   Structures.tclTHEN
     Tactics.intros
-    (Structures.mk_tactic (core_tactic call_solver solver_logic rt ro ra rf ra' rf' vm_cast lcpl lcepl))
+    (Structures.mk_tactic (core_tactic call_solver solver_logic rt ro ra rf ra_quant rf_quant vm_cast lcpl lcepl))
 
 
 (**********************************************)
diff --git a/src/trace/smtForm.ml b/src/trace/smtForm.ml
index 12aef5a..4e11709 100644
--- a/src/trace/smtForm.ml
+++ b/src/trace/smtForm.ml
@@ -472,7 +472,7 @@ module Make (Atom:ATOM) =
       mk_hform c
 
 
-    let hash_hform hash_hatom rf' hf =
+    let hash_hform hash_hatom rf_quant hf =
       let rec mk_hform = function
         | Pos hp -> Pos (mk_hpform hp)
         | Neg hp -> Neg (mk_hpform hp)
@@ -482,7 +482,7 @@ module Make (Atom:ATOM) =
             | Fapp (fop, arr) -> Fapp (fop, Array.map mk_hform arr)
             | FbbT (a, l) -> FbbT (hash_hatom a, List.map mk_hform l)
         in
-        match get rf' new_hv with Pos x | Neg x -> x in
+        match get rf_quant new_hv with Pos x | Neg x -> x in
       mk_hform hf
 
 
diff --git a/src/verit/verit.ml b/src/verit/verit.ml
index 39f60c0..fbc04e3 100644
--- a/src/verit/verit.ml
+++ b/src/verit/verit.ml
@@ -55,7 +55,7 @@ open SmtCertif
  *   done;
  *   Format.fprintf fmt "@."; close_out out_channel *)
 
-let import_trace ra' rf' filename first lsmt =
+let import_trace ra_quant rf_quant filename first lsmt =
   let chan = open_in filename in
   let lexbuf = Lexing.from_channel chan in
   let confl_num = ref (-1) in
@@ -78,7 +78,7 @@ let import_trace ra' rf' filename first lsmt =
        close_in chan;
        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
+       let re_hash = Form.hash_hform (Atom.hash_hatom ra_quant) rf_quant in
        begin match first with
        | None -> ()
        | Some _ ->
@@ -114,10 +114,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 ra_quant = VeritSyntax.ra_quant in
+  let rf_quant = VeritSyntax.rf_quant in
   let roots = Smtlib2_genConstr.import_smtlib2 rt ro ra rf fsmt in
-  let (max_id, confl) = import_trace ra' rf' fproof None [] in
+  let (max_id, confl) = import_trace ra_quant rf_quant fproof None [] in
   (rt, ro, ra, rf, roots, max_id, confl)
 
 
@@ -169,7 +169,7 @@ let export out_channel rt ro lsmt =
 
 exception Unknown
 
-let call_verit _ rt ro ra' rf' first lsmt =
+let call_verit _ rt ro ra_quant rf_quant first lsmt =
   let (filename, outchan) = Filename.open_temp_file "verit_coq" ".smt2" in
   export outchan rt ro lsmt;
   close_out outchan;
@@ -206,7 +206,7 @@ let call_verit _ rt ro ra' rf' first lsmt =
   try
     if exit_code <> 0 then Structures.warning "verit-non-zero-exit-code" ("Verit.call_verit: command " ^ command ^ " exited with code " ^ string_of_int exit_code);
     raise_warnings_errors ();
-    let res = import_trace ra' rf' logfilename (Some first) lsmt in
+    let res = import_trace ra_quant rf_quant logfilename (Some first) lsmt in
     close_in win; Sys.remove wname; res
   with x -> close_in win; Sys.remove wname;
             match x with
@@ -223,8 +223,8 @@ let tactic_gen vm_cast lcpl lcepl =
   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
-  SmtCommands.tactic call_verit verit_logic rt ro ra rf ra' rf' vm_cast lcpl lcepl
+  let ra_quant = VeritSyntax.ra_quant in
+  let rf_quant = VeritSyntax.rf_quant in
+  SmtCommands.tactic call_verit verit_logic rt ro ra rf ra_quant rf_quant vm_cast lcpl lcepl
 let tactic = tactic_gen vm_cast_true
 let tactic_no_check = tactic_gen (fun _ -> vm_cast_true_no_check)
diff --git a/src/verit/veritParser.mly b/src/verit/veritParser.mly
index 08c5cb3..c46b7c3 100644
--- a/src/verit/veritParser.mly
+++ b/src/verit/veritParser.mly
@@ -272,7 +272,7 @@ term:   /* returns a bool * (SmtAtom.Form.pform or SmtAtom.hatom), the boolean i
   | 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, 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 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_sym 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 }
diff --git a/src/verit/veritSyntax.ml b/src/verit/veritSyntax.ml
index b1a6304..422c6f5 100644
--- a/src/verit/veritSyntax.ml
+++ b/src/verit/veritSyntax.ml
@@ -555,7 +555,7 @@ let init_index lsmt re_hash =
               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"
+              failwith "Input not found: log available in /tmp/input_not_found.log"
 
 let qf_to_add lr =
   let is_forall l = match Form.pform l with
@@ -570,8 +570,8 @@ let qf_to_add lr =
 
 let ra = Atom.create ()
 let rf = Form.create ()
-let ra' = Atom.create ()
-let rf' = Form.create ()
+let ra_quant = Atom.create ()
+let rf_quant = Form.create ()
 
 let hlets : (string, Form.atom_form_lit) Hashtbl.t = Hashtbl.create 17
 
@@ -586,6 +586,6 @@ let clear () =
   clear_solver ();
   Atom.clear ra;
   Form.clear rf;
-  Atom.clear ra';
-  Form.clear rf';
+  Atom.clear ra_quant;
+  Form.clear rf_quant;
   Hashtbl.clear hlets
diff --git a/src/verit/veritSyntax.mli b/src/verit/veritSyntax.mli
index 7a325a6..bd98ba6 100644
--- a/src/verit/veritSyntax.mli
+++ b/src/verit/veritSyntax.mli
@@ -52,8 +52,8 @@ val qf_to_add : SmtAtom.Form.t SmtCertif.clause list -> (SmtAtom.Form.t SmtCerti
 
 val ra : SmtAtom.Atom.reify_tbl
 val rf : SmtAtom.Form.reify
-val ra' : SmtAtom.Atom.reify_tbl
-val rf' : SmtAtom.Form.reify
+val ra_quant : SmtAtom.Atom.reify_tbl
+val rf_quant : SmtAtom.Form.reify
 
 val hlets : (string, Form.atom_form_lit) Hashtbl.t
 
diff --git a/src/versions/standard/Tactics_standard.v b/src/versions/standard/Tactics_standard.v
index 95b92d6..4162f13 100644
--- a/src/versions/standard/Tactics_standard.v
+++ b/src/versions/standard/Tactics_standard.v
@@ -29,11 +29,11 @@ Tactic Notation "verit_bool_no_check" constr_list(h) :=
 Ltac zchaff          := prop2bool; zchaff_bool; bool2prop.
 Ltac zchaff_no_check := prop2bool; zchaff_bool_no_check; bool2prop.
 
-Tactic Notation "verit" constr_list(h) := prop2bool; verit_bool h; bool2prop.
-Tactic Notation "verit_no_check" constr_list(h) := prop2bool; verit_bool_no_check h; bool2prop.
+Tactic Notation "verit" constr_list(h) := prop2bool; [ .. | verit_bool h; bool2prop ].
+Tactic Notation "verit_no_check" constr_list(h) := prop2bool; [ .. | verit_bool_no_check h; bool2prop ].
 
-Ltac cvc4            := prop2bool; cvc4_bool; bool2prop.
-Ltac cvc4_no_check   := prop2bool; cvc4_bool_no_check; bool2prop.
+Ltac cvc4            := prop2bool; [ .. | cvc4_bool; bool2prop ].
+Ltac cvc4_no_check   := prop2bool; [ .. | cvc4_bool_no_check; bool2prop ].
 
 
 (* Ltac smt := prop2bool; *)
@@ -53,8 +53,8 @@ Ltac cvc4_no_check   := prop2bool; cvc4_bool_no_check; bool2prop.
 (*               end; *)
 (*             bool2prop. *)
 
-Tactic Notation "smt" constr_list(h) := (prop2bool; try verit_bool h; cvc4_bool; try verit_bool h; bool2prop).
-Tactic Notation "smt_no_check" constr_list(h) := (prop2bool; try verit_bool_no_check h; cvc4_bool_no_check; try verit_bool_no_check h; bool2prop).
+Tactic Notation "smt" constr_list(h) := (prop2bool; [ .. | try verit_bool h; cvc4_bool; try verit_bool h; bool2prop ]).
+Tactic Notation "smt_no_check" constr_list(h) := (prop2bool; [ .. | try verit_bool_no_check h; cvc4_bool_no_check; try verit_bool_no_check h; bool2prop]).
 
 
 
diff --git a/unit-tests/Tests_lfsc_tactics.v b/unit-tests/Tests_lfsc_tactics.v
index 387ed21..feb1d7e 100644
--- a/unit-tests/Tests_lfsc_tactics.v
+++ b/unit-tests/Tests_lfsc_tactics.v
@@ -716,7 +716,7 @@ Section A_BV_EUF_LIA_PR.
     smt.
   Admitted.
 
-  (* The original issue (unvalid) *)
+  (* The original issue (invalid) *)
   Goal forall (x: bitvector 1), bv_subt (bv_shl #b|0| x) #b|0| = #b|0|.
   Proof using.
     smt.
@@ -755,6 +755,94 @@ Section group.
 End group.
 
 
+Section EqualityOnUninterpretedType1.
+  Variable A : Type.
+  Hypothesis HA : CompDec A.
+
+  Goal forall (f : A -> Z) (a b : A), a = b -> f a = f b.
+  Proof. cvc4. Qed.
+
+  Goal forall (f : A -> Z) (a b : A), a = b -> f a = f b.
+  Proof. smt. Qed.
+End EqualityOnUninterpretedType1.
+
+Section EqualityOnUninterpretedType2.
+  Variable A B : Type.
+  Hypothesis HA : CompDec A.
+  Hypothesis HB : CompDec B.
+
+  Goal forall (f : A -> Z) (a b : A), a = b -> f a = f b.
+  Proof. cvc4. Qed.
+
+  Goal forall (f : A -> Z) (a b : A), a = b -> f a = f b.
+  Proof. smt. Qed.
+
+  Goal forall (f : Z -> B) (a b : Z), a = b -> f a = f b.
+  Proof. cvc4. Qed.
+
+  Goal forall (f : Z -> B) (a b : Z), a = b -> f a = f b.
+  Proof. smt. Qed.
+
+  Goal forall (f : A -> B) (a b : A), a = b -> f a = f b.
+  Proof. cvc4. Qed.
+
+  Goal forall (f : A -> B) (a b : A), a = b -> f a = f b.
+  Proof. smt. Qed.
+End EqualityOnUninterpretedType2.
+
+Section EqualityOnUninterpretedType3.
+  Variable A B : Type.
+
+  Goal forall (f : A -> Z) (a b : A), a = b -> f a = f b.
+  Proof. cvc4. Abort.
+
+  Goal forall (f : A -> Z) (a b : A), a = b -> f a = f b.
+  Proof. smt. Abort.
+
+  Goal forall (f : Z -> B) (a b : Z), a = b -> f a = f b.
+  Proof. cvc4. Abort.
+
+  Goal forall (f : Z -> B) (a b : Z), a = b -> f a = f b.
+  Proof. smt. Abort.
+
+  Goal forall (f : A -> B) (a b : A), a = b -> f a = f b.
+  Proof. cvc4. Abort.
+
+  Goal forall (f : A -> B) (a b : A), a = b -> f a = f b.
+  Proof. smt. Abort.
+
+  Goal forall (f : A -> A -> B) (a b c d : A), a = b -> c = d -> f a c = f b d.
+  Proof. cvc4. Abort.
+
+  Goal forall (f : A -> A -> B) (a b c d : A), a = b -> c = d -> f a c = f b d.
+  Proof. smt. Abort.
+End EqualityOnUninterpretedType3.
+
+
+Section Issue17.
+
+  Variable A : Type.
+  Variable cd : CompDec A.
+
+  Goal forall (a:A), a = a.
+  Proof. smt. Qed.
+
+End Issue17.
+
+
+(* TODO *)
+(* From cvc4_bool : Uncaught exception Not_found *)
+(* Goal forall (a b c d: farray Z Z), *)
+(*     b[0 <- 4] = c  -> *)
+(*     d = b[0 <- 4][1 <- 4]  -> *)
+(*     a = d[1 <- b[1]]  -> *)
+(*     a = c. *)
+(* Proof. *)
+(*   smt. *)
+(* Qed. *)
+
+
+
 (*
    Local Variables:
    coq-load-path: ((rec "../src" "SMTCoq"))
diff --git a/unit-tests/Tests_verit_tactics.v b/unit-tests/Tests_verit_tactics.v
index da7cb5a..2121ba2 100644
--- a/unit-tests/Tests_verit_tactics.v
+++ b/unit-tests/Tests_verit_tactics.v
@@ -499,20 +499,16 @@ Proof using.
   verit.
 Qed.
 
-(* TODO: fails with native-coq: "compilation error"
 Goal forall (i j:int),
     (i == j) && (negb (i == j)) = false.
 Proof using.
-  verit.
-  exact int63_compdec.
+  verit. auto with typeclass_instances.
 Qed.
 
 Goal forall i j, (i == j) || (negb (i == j)).
 Proof using.
-  verit.
-  exact int63_compdec.
+  verit. auto with typeclass_instances.
 Qed.
-*)
 
 
 (* Congruence in which some premises are REFL *)
@@ -707,27 +703,24 @@ End mult3.
 (* End mult. *)
 
 Section implicit_transform.
-  Variable f : Z -> bool.
-  Variable a1 a2 : Z.
+  Variable A : Type.
+  Variable HA : CompDec A.
+  Variable f : A -> bool.
+  Variable a1 a2 : A.
   Hypothesis f_const : forall b, implb (f b) (f a2).
   Hypothesis f_a1 : f a1.
   Add_lemmas f_const f_a1.
 
   Lemma implicit_transform :
     f a2.
-  Proof using f_const f_a1. verit. Qed.
+  Proof using HA f_const f_a1. verit. Qed.
 
   Clear_lemmas.
 End implicit_transform.
 
 Section list.
-  Variable Zlist : Type.
-  Hypothesis dec_Zlist : CompDec Zlist.
-  Variable nil : Zlist.
-  Variable cons : Z -> Zlist -> Zlist.
-  Variable inlist : Z -> Zlist -> bool.
-
-  Infix "::" := cons.
+  Hypothesis dec_Zlist : CompDec (list Z).
+  Variable inlist : Z -> (list Z) -> bool.
 
   Hypothesis in_eq : forall a l, inlist a (a :: l).
   Hypothesis in_cons : forall a b l, implb (inlist a l) (inlist a (b::l)).
@@ -765,9 +758,6 @@ Section list.
   (*   inlist 12 (11::13::(-12)::1::nil). *)
   (*   verit. (*returns unknown*) *)
 
-  Variable append : Zlist -> Zlist -> Zlist.
-  Infix "++" := append.
-
   Hypothesis in_or_app : forall a l1 l2,
       implb (orb (inlist a l1) (inlist a l2))
             (inlist a (l1 ++ l2)).
@@ -819,7 +809,7 @@ Section list.
 End list.
 
 
-Section group.
+Section GroupZ.
   Variable op : Z -> Z -> Z.
   Variable inv : Z -> Z.
   Variable e : Z.
@@ -832,20 +822,54 @@ Section group.
     forall a : Z, (op a (inv a) =? e) && (op (inv a) a =? e).
   Add_lemmas associative identity inverse.
 
-  Lemma unique_identity e':
+  Lemma unique_identity_Z e':
     (forall z, op e' z =? z) -> e' =? e.
   Proof using associative identity inverse. intros pe'. verit pe'. Qed.
 
-  Lemma simplification_right x1 x2 y:
+  Lemma simplification_right_Z x1 x2 y:
       op x1 y =? op x2 y -> x1 =? x2.
   Proof using associative identity inverse. intro H. verit H. Qed.
 
-  Lemma simplification_left x1 x2 y:
+  Lemma simplification_left_Z x1 x2 y:
       op y x1 =? op y x2 -> x1 =? x2.
   Proof using associative identity inverse. intro H. verit H. Qed.
 
   Clear_lemmas.
-End group.
+End GroupZ.
+
+
+Section Group.
+  Variable G : Type.
+  Variable HG : CompDec G.
+  Variable op : G -> G -> G.
+  Variable inv : G -> G.
+  Variable e : G.
+
+  Notation "a ==? b" := (@eqb_of_compdec G HG a b) (at level 60).
+
+  Hypothesis associative :
+    forall a b c : G, op a (op b c) ==? op (op a b) c.
+  Hypothesis identity :
+    forall a : G, (op e a ==? a) && (op a e ==? a).
+  Hypothesis inverse :
+    forall a : G, (op a (inv a) ==? e) && (op (inv a) a ==? e).
+  Add_lemmas associative identity inverse.
+
+  Lemma unique_identity e':
+    (forall z, op e' z ==? z) -> e' ==? e.
+  Proof using associative identity inverse. intros pe'. verit pe'. Qed.
+
+  Lemma simplification_right x1 x2 y:
+      op x1 y ==? op x2 y -> x1 ==? x2.
+  Proof using associative identity inverse. intro H. verit H. Qed.
+
+  Lemma simplification_left x1 x2 y:
+      op y x1 ==? op y x2 -> x1 ==? x2.
+  Proof using associative identity inverse. intro H. verit H. Qed.
+
+  Clear_lemmas.
+End Group.
+
 
 Section Linear1.
   Variable f : Z -> Z.
@@ -996,11 +1020,90 @@ Proof using.
 Qed.
 
 
-Section Polymorphism.
+Section AppliedPolymorphicTypes1.
   Goal forall (f : option Z -> Z) (a b : Z),
       implb (Z.eqb a b) (Z.eqb (f (Some a)) (f (Some b))).
   Proof. verit. auto with typeclass_instances. Qed.
 
   Goal forall (f : option Z -> Z) (a b : Z), a = b -> f (Some a) = f (Some b).
   Proof. verit. auto with typeclass_instances. Qed.
-End Polymorphism.
+End AppliedPolymorphicTypes1.
+
+
+Section EqualityOnUninterpretedType1.
+  Variable A : Type.
+  Hypothesis HA : CompDec A.
+
+  Goal forall (f : A -> Z) (a b : A), a = b -> f a = f b.
+  Proof. verit. Qed.
+End EqualityOnUninterpretedType1.
+
+Section EqualityOnUninterpretedType2.
+  Variable A B : Type.
+  Hypothesis HA : CompDec A.
+  Hypothesis HB : CompDec B.
+
+  Goal forall (f : A -> Z) (a b : A), a = b -> f a = f b.
+  Proof. verit. Qed.
+
+  Goal forall (f : Z -> B) (a b : Z), a = b -> f a = f b.
+  Proof. verit. Qed.
+
+  Goal forall (f : A -> B) (a b : A), a = b -> f a = f b.
+  Proof. verit. Qed.
+End EqualityOnUninterpretedType2.
+
+Section EqualityOnUninterpretedType3.
+  Variable A B : Type.
+
+  Goal forall (f : A -> Z) (a b : A), a = b -> f a = f b.
+  Proof. verit. Abort.
+
+  Goal forall (f : Z -> B) (a b : Z), a = b -> f a = f b.
+  Proof. verit. Abort.
+
+  Goal forall (f : A -> B) (a b : A), a = b -> f a = f b.
+  Proof. verit. Abort.
+
+  Goal forall (f : A -> A -> B) (a b c d : A), a = b -> c = d -> f a c = f b d.
+  Proof. verit. Abort.
+End EqualityOnUninterpretedType3.
+
+
+Section AppliedPolymorphicTypes2.
+  Variable list : Type -> Type.
+  Variable append : forall A : Type, list A -> list A -> list A.
+  Arguments append {A} _ _.
+  Local Notation "l1 +++ l2" := (append l1 l2) (at level 60).
+
+  Variable B : Type.
+  Variable HlB : CompDec (list B).
+
+  Goal forall l1 l2 l3 l4 : list B,
+      l1 +++ (l2 +++ (l3 +++ l4)) = l1 +++ (l2 +++ (l3 +++ l4)).
+  Proof. verit. Qed.
+
+  Hypothesis append_assoc_B :
+    forall l1 l2 l3 : list B, eqb_of_compdec HlB (l1 +++ (l2 +++ l3)) ((l1 +++ l2) +++ l3) = true.
+  (* TODO: make it possible to apply prop2bool to hypotheses *)
+  (* Hypothesis append_assoc_B : *)
+  (*   forall l1 l2 l3 : list B, l1 +++ (l2 +++ l3) = (l1 +++ l2) +++ l3. *)
+
+  (* The hypothesis is not used *)
+  Goal forall l1 l2 l3 l4 : list B,
+      l1 +++ (l2 +++ (l3 +++ l4)) = l1 +++ (l2 +++ (l3 +++ l4)).
+  Proof. verit append_assoc_B. Qed.
+
+  (* The hypothesis is used *)
+  Goal forall l1 l2 l3 l4 : list B,
+      l1 +++ (l2 +++ (l3 +++ l4)) = ((l1 +++ l2) +++ l3) +++ l4.
+  Proof. verit append_assoc_B. Qed.
+End AppliedPolymorphicTypes2.
+
+
+Section Issue78.
+
+  Goal forall (f : option Z -> Z) (a  b : Z), Some a = Some b -> f (Some a) = f (Some b).
+  Proof. verit. Qed.
+
+End Issue78.