1 files changed, 609 insertions, 99 deletions

diff --git a/src/trace/smtCommands.ml b/src/trace/smtCommands.ml
index 27b8210..58793b6 100644
--- a/src/trace/smtCommands.ml
+++ b/src/trace/smtCommands.ml
@@ -1,13 +1,9 @@
 (**************************************************************************)
 (*                                                                        *)
 (*     SMTCoq                                                             *)
-(*     Copyright (C) 2011 - 2016                                          *)
+(*     Copyright (C) 2011 - 2019                                          *)
 (*                                                                        *)
-(*     Michaël Armand                                                     *)
-(*     Benjamin Grégoire                                                  *)
-(*     Chantal Keller                                                     *)
-(*                                                                        *)
-(*     Inria - École Polytechnique - Université Paris-Sud                 *)
+(*     See file "AUTHORS" for the list of authors                         *)
 (*                                                                        *)
 (*   This file is distributed under the terms of the CeCILL-C licence     *)
 (*                                                                        *)
@@ -38,7 +34,53 @@ let cchecker_b = gen_constant euf_checker_modules "checker_b"
 let cchecker_eq_correct =
   gen_constant euf_checker_modules "checker_eq_correct"
 let cchecker_eq = gen_constant euf_checker_modules "checker_eq"
-let cZeqbsym = gen_constant z_modules "eqb_sym"
+let csetup_checker_step_debug =
+  gen_constant euf_checker_modules "setup_checker_step_debug"
+let cchecker_step_debug = gen_constant euf_checker_modules "checker_step_debug"
+let cstep = gen_constant euf_checker_modules "step"
+let cchecker_debug = gen_constant euf_checker_modules "checker_debug"
+
+let cname_step = gen_constant euf_checker_modules "name_step"
+
+let cName_Res = gen_constant euf_checker_modules "Name_Res"
+let cName_Weaken= gen_constant euf_checker_modules "Name_Weaken"
+let cName_ImmFlatten= gen_constant euf_checker_modules "Name_ImmFlatten"
+let cName_CTrue= gen_constant euf_checker_modules "Name_CTrue"
+let cName_CFalse = gen_constant euf_checker_modules "Name_CFalse"
+let cName_BuildDef= gen_constant euf_checker_modules "Name_BuildDef"
+let cName_BuildDef2= gen_constant euf_checker_modules "Name_BuildDef2"
+let cName_BuildProj = gen_constant euf_checker_modules "Name_BuildProj"
+let cName_ImmBuildDef= gen_constant euf_checker_modules "Name_ImmBuildDef"
+let cName_ImmBuildDef2= gen_constant euf_checker_modules "Name_ImmBuildDef2"
+let cName_ImmBuildProj = gen_constant euf_checker_modules "Name_ImmBuildProj"
+let cName_EqTr = gen_constant euf_checker_modules "Name_EqTr"
+let cName_EqCgr = gen_constant euf_checker_modules "Name_EqCgr"
+let cName_EqCgrP= gen_constant euf_checker_modules "Name_EqCgrP"
+let cName_LiaMicromega = gen_constant euf_checker_modules "Name_LiaMicromega"
+let cName_LiaDiseq= gen_constant euf_checker_modules "Name_LiaDiseq"
+let cName_SplArith= gen_constant euf_checker_modules "Name_SplArith"
+let cName_SplDistinctElim = gen_constant euf_checker_modules "Name_SplDistinctElim"
+let cName_BBVar= gen_constant euf_checker_modules "Name_BBVar"
+let cName_BBConst= gen_constant euf_checker_modules "Name_BBConst"
+let cName_BBOp= gen_constant euf_checker_modules "Name_BBOp"
+let cName_BBNot= gen_constant euf_checker_modules "Name_BBNot"
+let cName_BBNeg= gen_constant euf_checker_modules "Name_BBNeg"
+let cName_BBAdd= gen_constant euf_checker_modules "Name_BBAdd"
+let cName_BBConcat= gen_constant euf_checker_modules "Name_BBConcat"
+let cName_BBMul= gen_constant euf_checker_modules "Name_BBMul"
+let cName_BBUlt= gen_constant euf_checker_modules "Name_BBUlt"
+let cName_BBSlt= gen_constant euf_checker_modules "Name_BBSlt"
+let cName_BBEq= gen_constant euf_checker_modules "Name_BBEq"
+let cName_BBDiseq= gen_constant euf_checker_modules "Name_BBDiseq"
+let cName_BBExtract= gen_constant euf_checker_modules "Name_BBExtract"
+let cName_BBZextend= gen_constant euf_checker_modules "Name_BBZextend"
+let cName_BBSextend= gen_constant euf_checker_modules "Name_BBSextend"
+let cName_BBShl= gen_constant euf_checker_modules "Name_BBShl"
+let cName_BBShr= gen_constant euf_checker_modules "Name_BBShr"
+let cName_RowEq= gen_constant euf_checker_modules "Name_RowEq"
+let cName_RowNeq= gen_constant euf_checker_modules "Name_RowNeq"
+let cName_Ext= gen_constant euf_checker_modules "Name_Ext"
+let cName_Hole= gen_constant euf_checker_modules "Name_Hole"
 
 (* Given an SMT-LIB2 file and a certif, build the corresponding objects *)
 
@@ -50,42 +92,40 @@ let compute_roots roots last_root =
 
   let rec find_root i root = function
     | [] -> assert false
-    | t::q -> if Form.equal t root then (i,q) else find_root (i+1) root q in
+    | t::q -> if Form.equal t root then i else find_root (i+1) root q in
 
-  let rec used_roots acc i roots r =
+  let rec used_roots acc r =
     if isRoot r.kind then
       match r.value with
         | Some [root] ->
-           let (j,roots') = find_root i root roots in
-           used_roots (j::acc) (j+1) roots' (next r)
+           let j = find_root 0 root roots in
+           used_roots (j::acc) (next r)
         | _ -> assert false
-    else
-      acc in
+    else acc
+  in
 
-  used_roots [] 0 roots !r
+  used_roots [] !r
 
 
-let interp_uf ta tf c =
+let interp_uf t_i ta tf c =
   let rec interp = function
     | [] -> Lazy.force cfalse
-    | [l] -> Form.interp_to_coq (Atom.interp_to_coq ta) tf l
-    | l::c -> mklApp corb [|Form.interp_to_coq (Atom.interp_to_coq ta) tf l; interp c|] in
+    | [l] -> Form.interp_to_coq (Atom.interp_to_coq t_i ta) tf l
+    | l::c -> mklApp corb [|Form.interp_to_coq (Atom.interp_to_coq t_i ta) tf l; interp c|] in
   interp c
 
-let interp_conseq_uf (prem, concl) =
+let interp_conseq_uf t_i (prem, concl) =
   let ta = Hashtbl.create 17 in
   let tf = Hashtbl.create 17 in
   let rec interp = function
-    | [] -> mklApp cis_true [|interp_uf ta tf concl|]
-    | c::prem -> Term.mkArrow (mklApp cis_true [|interp_uf ta tf c|]) (interp prem) in
+    | [] -> mklApp cis_true [|interp_uf t_i ta tf concl|]
+    | c::prem -> Term.mkArrow (mklApp cis_true [|interp_uf t_i ta tf c|]) (interp prem) in
   interp prem
 
 
 let print_assm ty =
-  let rec fix rf x = rf (fix rf) x in
-  let pr = fix Ppconstr.modular_constr_pr Pp.mt Structures.ppconstr_lsimpleconstr in
-  Printf.printf "WARNING: assuming the following hypothesis:\n%s\n\n" (Pp.string_of_ppcmds (pr (Structures.constrextern_extern_constr ty)));
-  flush stdout
+  Format.printf "WARNING: assuming the following hypothesis:\n%s\n@."
+    (string_coq_constr ty)
 
 
 let parse_certif t_i t_func t_atom t_form root used_root trace (rt, ro, ra, rf, roots, max_id, confl) =
@@ -107,7 +147,8 @@ let parse_certif t_i t_func t_atom t_form root used_root trace (rt, ro, ra, rf,
   let ct_form = Term.mkConst (declare_constant t_form (DefinitionEntry ce2, IsDefinition Definition)) in
 
   (* EMPTY LEMMA LIST *)
-  let (tres, last_root, cuts) = SmtTrace.to_coq (fun i -> mkInt (Form.to_lit i)) interp_conseq_uf (certif_ops (Some [|ct_i; ct_func; ct_atom; ct_form|])) confl None in
+  let (tres, last_root, cuts) = SmtTrace.to_coq (fun i -> mkInt (Form.to_lit i))
+      (interp_conseq_uf ct_i) (certif_ops (Some [|ct_i; ct_func; ct_atom; ct_form|])) confl None in
   List.iter (fun (v,ty) ->
     let _ = Structures.declare_new_variable v ty in
     print_assm ty
@@ -140,8 +181,8 @@ let parse_certif t_i t_func t_atom t_form root used_root trace (rt, ro, ra, rf,
 
 (* Given an SMT-LIB2 file and a certif, build the corresponding theorem *)
 
-let interp_roots roots =
-  let interp = Form.interp_to_coq (Atom.interp_to_coq (Hashtbl.create 17)) (Hashtbl.create 17) in
+let interp_roots t_i roots =
+  let interp = Form.interp_to_coq (Atom.interp_to_coq t_i (Hashtbl.create 17)) (Hashtbl.create 17) in
   match roots with
     | [] -> Lazy.force ctrue
     | f::roots -> List.fold_left (fun acc f -> mklApp candb [|acc; interp f|]) (interp f) roots
@@ -163,7 +204,9 @@ let theorem name (rt, ro, ra, rf, roots, max_id, confl) =
   let t_form = snd (Form.interp_tbl rf) in
 
   (* EMPTY LEMMA LIST *)
-  let (tres,last_root,cuts) = SmtTrace.to_coq (fun i -> mkInt (Form.to_lit i)) interp_conseq_uf (certif_ops (Some [|v 4(*t_i*); v 3(*t_func*); v 2(*t_atom*); v 1(* t_form *)|])) confl None in
+  let (tres,last_root,cuts) = SmtTrace.to_coq (fun i -> mkInt (Form.to_lit i))
+      (interp_conseq_uf t_i)
+      (certif_ops (Some [|v 4(*t_i*); v 3(*t_func*); v 2(*t_atom*); v 1(* t_form *)|])) confl None in
   List.iter (fun (v,ty) ->
     let _ = Structures.declare_new_variable v ty in
     print_assm ty
@@ -185,10 +228,10 @@ let theorem name (rt, ro, ra, rf, roots, max_id, confl) =
     List.iter (fun j -> res.(!i) <- mkInt (Form.to_lit j); incr i) roots;
     Structures.mkArray (Lazy.force cint, res) in
 
-  let theorem_concl = mklApp cis_true [|mklApp cnegb [|interp_roots roots|]|] in
+  let theorem_concl = mklApp cnot [|mklApp cis_true [|interp_roots t_i roots|]|] in
   let theorem_proof_cast =
     Term.mkCast (
-        Term.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_eqb|],
+        Term.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_compdec|],
         Term.mkLetIn (ntfunc, t_func, mklApp carray [|mklApp ctval [|v 1(* t_i *)|]|],
         Term.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|],
         Term.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|],
@@ -197,13 +240,13 @@ let theorem name (rt, ro, ra, rf, roots, max_id, confl) =
         Term.mkLetIn (nd, rootsCstr, mklApp carray [|Lazy.force cint|],
         mklApp cchecker_correct
                [|v 7 (*t_i*); v 6 (*t_func*); v 5 (*t_atom*); v 4 (*t_form*); v 1 (*d*); v 2 (*used_roots*); v 3 (*c*);
-	         vm_cast_true
+	         vm_cast_true_no_check
 	           (mklApp cchecker [|v 7 (*t_i*); v 6 (*t_func*); v 5 (*t_atom*); v 4 (*t_form*); v 1 (*d*); v 2 (*used_roots*); v 3 (*c*)|])|]))))))),
         Term.VMcast,
         theorem_concl)
   in
   let theorem_proof_nocast =
-        Term.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_eqb|],
+        Term.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_compdec|],
         Term.mkLetIn (ntfunc, t_func, mklApp carray [|mklApp ctval [|v 1(* t_i *)|]|],
         Term.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|],
         Term.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|],
@@ -238,7 +281,9 @@ let checker (rt, ro, ra, rf, roots, max_id, confl) =
   let t_form = snd (Form.interp_tbl rf) in
 
   (* EMPTY LEMMA LIST *)
-  let (tres,last_root,cuts) = SmtTrace.to_coq (fun i -> mkInt (Form.to_lit i)) interp_conseq_uf (certif_ops (Some [|v 4(*t_i*); v 3(*t_func*); v 2(*t_atom*); v 1(* t_form *)|])) confl None in
+  let (tres,last_root,cuts) = SmtTrace.to_coq (fun i -> mkInt (Form.to_lit i))
+      (interp_conseq_uf t_i)
+      (certif_ops (Some [|v 4(*t_i*); v 3(*t_func*); v 2(*t_atom*); v 1(* t_form *)|])) confl None in
   List.iter (fun (v,ty) ->
     let _ = Structures.declare_new_variable v ty in
     print_assm ty
@@ -261,7 +306,7 @@ let checker (rt, ro, ra, rf, roots, max_id, confl) =
     Structures.mkArray (Lazy.force cint, res) in
 
   let tm =
-   Term.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_eqb|],
+   Term.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_compdec|],
    Term.mkLetIn (ntfunc, t_func, mklApp carray [|mklApp ctval [|v 1(* t_i *)|]|],
    Term.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|],
    Term.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|],
@@ -275,10 +320,256 @@ let checker (rt, ro, ra, rf, roots, max_id, confl) =
     (if Term.eq_constr res (Lazy.force CoqTerms.ctrue) then
         "true" else "false")
 
+let count_used confl =
+  let cpt = ref 0 in
+  let rec count c =
+    incr cpt;
+    (* if c.used = 1 then incr cpt; *)
+    match c.prev with
+    | None -> !cpt
+    | Some c -> count c
+  in
+  count confl
+
+
+let checker_debug (rt, ro, ra, rf, roots, max_id, confl) =
+  let nti = mkName "t_i" in
+  let ntfunc = mkName "t_func" in
+  let ntatom = mkName "t_atom" in
+  let ntform = mkName "t_form" in
+  let nc = mkName "c" in
+  let nused_roots = mkName "used_roots" in
+  let nd = mkName "d" in
+
+  let v = Term.mkRel in
+
+  let t_i = make_t_i rt in
+  let t_func = make_t_func ro (v 1 (*t_i*)) in
+  let t_atom = Atom.interp_tbl ra in
+  let t_form = snd (Form.interp_tbl rf) in
+
+  let (tres,last_root,cuts) = SmtTrace.to_coq (fun i -> mkInt (Form.to_lit i))
+      (interp_conseq_uf t_i)
+      (certif_ops (Some [|v 4(*t_i*); v 3(*t_func*);
+                          v 2(*t_atom*); v 1(* t_form *)|])) confl None in
+  List.iter (fun (v,ty) ->
+    let _ = Structures.declare_new_variable v ty in
+    print_assm ty
+  ) cuts;
+
+  let certif =
+    mklApp cCertif [|v 4(*t_i*); v 3(*t_func*); v 2(*t_atom*); v 1(* t_form *);
+                     mkInt (max_id + 1); tres;mkInt (get_pos confl)|] in
+
+  let used_roots = compute_roots roots last_root in
+  let used_rootsCstr =
+    let l = List.length used_roots in
+    let res = Array.make (l + 1) (mkInt 0) in
+    let i = ref (l-1) in
+    List.iter (fun j -> res.(!i) <- mkInt j; decr i) used_roots;
+    mklApp cSome [|mklApp carray [|Lazy.force cint|];
+                   Structures.mkArray (Lazy.force cint, res)|] in
+  let rootsCstr =
+    let res = Array.make (List.length roots + 1) (mkInt 0) in
+    let i = ref 0 in
+    List.iter (fun j -> res.(!i) <- mkInt (Form.to_lit j); incr i) roots;
+    Structures.mkArray (Lazy.force cint, res) in
+
+  let tm =
+   Term.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_compdec|],
+   Term.mkLetIn (ntfunc, t_func,
+                 mklApp carray [|mklApp ctval [|v 1(* t_i *)|]|],
+   Term.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|],
+   Term.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|],
+   Term.mkLetIn (nc, certif, mklApp ccertif [|v 4 (*t_i*); v 3 (*t_func*);
+                                              v 2 (*t_atom*); v 1 (*t_form*)|],
+   Term.mkLetIn (nused_roots, used_rootsCstr,
+                 mklApp coption [|mklApp carray [|Lazy.force cint|]|],
+   Term.mkLetIn (nd, rootsCstr, mklApp carray [|Lazy.force cint|],
+   mklApp cchecker_debug [|v 7 (*t_i*); v 6 (*t_func*); v 5 (*t_atom*);
+       v 4 (*t_form*); v 1 (*d*); v 2 (*used_roots*); v 3 (*c*)|]))))))) in
+
+  let res = Vnorm.cbv_vm (Global.env ()) tm
+      (mklApp coption
+         [|mklApp cprod
+             [|Lazy.force cnat; Lazy.force cname_step|]|]) in
+
+  match Term.decompose_app res with
+  | c, _ when Term.eq_constr c (Lazy.force cNone) ->
+    Structures.error ("Debug checker is only meant to be used for certificates \
+                       that fail to be checked by SMTCoq.")
+  | c, [_; n] when Term.eq_constr c (Lazy.force cSome) ->
+    (match Term.decompose_app n with
+     | c, [_; _; cnb; cn] when Term.eq_constr c (Lazy.force cpair) ->
+       let n = fst (Term.decompose_app cn) in
+       let name =
+         if Term.eq_constr n (Lazy.force cName_Res ) then "Res"
+         else if Term.eq_constr n (Lazy.force cName_Weaken) then "Weaken"
+         else if Term.eq_constr n (Lazy.force cName_ImmFlatten) then "ImmFlatten"
+         else if Term.eq_constr n (Lazy.force cName_CTrue) then "CTrue"
+         else if Term.eq_constr n (Lazy.force cName_CFalse ) then "CFalse"
+         else if Term.eq_constr n (Lazy.force cName_BuildDef) then "BuildDef"
+         else if Term.eq_constr n (Lazy.force cName_BuildDef2) then "BuildDef2"
+         else if Term.eq_constr n (Lazy.force cName_BuildProj ) then "BuildProj"
+         else if Term.eq_constr n (Lazy.force cName_ImmBuildDef) then "ImmBuildDef"
+         else if Term.eq_constr n (Lazy.force cName_ImmBuildDef2) then "ImmBuildDef2"
+         else if Term.eq_constr n (Lazy.force cName_ImmBuildProj ) then "ImmBuildProj"
+         else if Term.eq_constr n (Lazy.force cName_EqTr ) then "EqTr"
+         else if Term.eq_constr n (Lazy.force cName_EqCgr ) then "EqCgr"
+         else if Term.eq_constr n (Lazy.force cName_EqCgrP) then "EqCgrP"
+         else if Term.eq_constr n (Lazy.force cName_LiaMicromega ) then "LiaMicromega"
+         else if Term.eq_constr n (Lazy.force cName_LiaDiseq) then "LiaDiseq"
+         else if Term.eq_constr n (Lazy.force cName_SplArith) then "SplArith"
+         else if Term.eq_constr n (Lazy.force cName_SplDistinctElim ) then "SplDistinctElim"
+         else if Term.eq_constr n (Lazy.force cName_BBVar) then "BBVar"
+         else if Term.eq_constr n (Lazy.force cName_BBConst) then "BBConst"
+         else if Term.eq_constr n (Lazy.force cName_BBOp) then "BBOp"
+         else if Term.eq_constr n (Lazy.force cName_BBNot) then "BBNot"
+         else if Term.eq_constr n (Lazy.force cName_BBNeg) then "BBNeg"
+         else if Term.eq_constr n (Lazy.force cName_BBAdd) then "BBAdd"
+         else if Term.eq_constr n (Lazy.force cName_BBConcat) then "BBConcat"
+         else if Term.eq_constr n (Lazy.force cName_BBMul) then "BBMul"
+         else if Term.eq_constr n (Lazy.force cName_BBUlt) then "BBUlt"
+         else if Term.eq_constr n (Lazy.force cName_BBSlt) then "BBSlt"
+         else if Term.eq_constr n (Lazy.force cName_BBEq) then "BBEq"
+         else if Term.eq_constr n (Lazy.force cName_BBDiseq) then "BBDiseq"
+         else if Term.eq_constr n (Lazy.force cName_BBExtract) then "BBExtract"
+         else if Term.eq_constr n (Lazy.force cName_BBZextend) then "BBZextend"
+         else if Term.eq_constr n (Lazy.force cName_BBSextend) then "BBSextend"
+         else if Term.eq_constr n (Lazy.force cName_BBShl) then "BBShl"
+         else if Term.eq_constr n (Lazy.force cName_BBShr) then "BBShr"
+         else if Term.eq_constr n (Lazy.force cName_RowEq) then "RowEq"
+         else if Term.eq_constr n (Lazy.force cName_RowNeq) then "RowNeq"
+         else if Term.eq_constr n (Lazy.force cName_Ext) then "Ext"
+         else if Term.eq_constr n (Lazy.force cName_Hole) then "Hole"
+         else string_coq_constr n
+       in
+       let nb = mk_nat cnb + List.length roots + (confl.id + 1 - count_used confl) in
+       Structures.error ("Step number " ^ string_of_int nb ^
+                         " (" ^ name ^ ") of the certificate likely failed.")
+     | _ -> assert false
+    )
+  | _ -> assert false
+
+
+
+let rec of_coq_list cl =
+  match Term.decompose_app cl with
+  | c, _ when Term.eq_constr c (Lazy.force cnil) -> []
+  | c, [_; x; cr] when Term.eq_constr c (Lazy.force ccons) ->
+    x :: of_coq_list cr
+  | _ -> assert false
+
+
+let checker_debug_step t_i t_func t_atom t_form root used_root trace
+    (rt, ro, ra, rf, roots, max_id, confl) =
+
+  let t_i' = make_t_i rt in
+  let ce5 = Structures.mkUConst t_i' in
+  let ct_i = Term.mkConst (declare_constant t_i
+                             (DefinitionEntry ce5, IsDefinition Definition)) in
+
+  let t_func' = make_t_func ro ct_i in
+  let ce6 = Structures.mkUConst t_func' in
+  let ct_func =
+    Term.mkConst (declare_constant t_func
+                    (DefinitionEntry ce6, IsDefinition Definition)) in
+
+  let t_atom' = Atom.interp_tbl ra in
+  let ce1 = Structures.mkUConst t_atom' in
+  let ct_atom =
+    Term.mkConst (declare_constant t_atom
+                    (DefinitionEntry ce1, IsDefinition Definition)) in
+
+  let t_form' = snd (Form.interp_tbl rf) in
+  let ce2 = Structures.mkUConst t_form' in
+  let ct_form =
+    Term.mkConst (declare_constant t_form
+                    (DefinitionEntry ce2, IsDefinition Definition)) in
+
+  let (tres, last_root, cuts) = SmtTrace.to_coq (fun i -> mkInt (Form.to_lit i))
+      (interp_conseq_uf ct_i)
+      (certif_ops (Some [|ct_i; ct_func; ct_atom; ct_form|])) confl None in
+  List.iter (fun (v,ty) ->
+    let _ = Structures.declare_new_variable v ty in
+    print_assm ty
+  ) cuts;
+
+  let used_roots = compute_roots roots last_root in
+  let croots =
+    let res = Array.make (List.length roots + 1) (mkInt 0) in
+    let i = ref 0 in
+    List.iter (fun j -> res.(!i) <- mkInt (Form.to_lit j); incr i) roots;
+    Structures.mkArray (Lazy.force cint, res) in
+  let cused_roots =
+    let l = List.length used_roots in
+    let res = Array.make (l + 1) (mkInt 0) in
+    let i = ref (l-1) in
+    List.iter (fun j -> res.(!i) <- mkInt j; decr i) used_roots;
+    mklApp cSome [|mklApp carray [|Lazy.force cint|];
+                   Structures.mkArray (Lazy.force cint, res)|] in
+  let ce3 = Structures.mkUConst croots in
+  let _ = declare_constant root
+      (DefinitionEntry ce3, IsDefinition Definition) in
+  let ce3' = Structures.mkUConst cused_roots in
+  let _ = declare_constant used_root
+      (DefinitionEntry ce3', IsDefinition Definition) in
+
+  let certif =
+    mklApp cCertif [|ct_i; ct_func; ct_atom; ct_form; mkInt (max_id + 1);
+                     tres;mkInt (get_pos confl)|] in
+  let ce4 = Structures.mkUConst certif in
+  let _ = declare_constant trace
+      (DefinitionEntry ce4, IsDefinition Definition) in
+
+  let setup =
+   mklApp csetup_checker_step_debug
+     [| ct_i; ct_func; ct_atom; ct_form; croots; cused_roots; certif |] in
+
+  let setup = Vnorm.cbv_vm (Global.env ()) setup
+      (mklApp cprod
+         [|Lazy.force cState_S_t;
+           mklApp clist [|mklApp cstep
+                            [|ct_i; ct_func; ct_atom; ct_form|]|]|]) in
+
+  let s, steps = match Term.decompose_app setup with
+    | c, [_; _; s; csteps] when Term.eq_constr c (Lazy.force cpair) ->
+      s, of_coq_list csteps
+    | _ -> assert false
+  in
+
+  let cpt = ref (List.length roots) in
+  let debug_step s step =
+    incr cpt;
+    Format.eprintf "%d@." !cpt;
+    let tm =
+      mklApp cchecker_step_debug
+        [| ct_i; ct_func; ct_atom; ct_form; s; step |] in
+
+    let res =
+      Vnorm.cbv_vm (Global.env ()) tm
+          (mklApp cprod [|Lazy.force cState_S_t; Lazy.force cbool|]) in
+
+    match Term.decompose_app res with
+    | c, [_; _; s; cbad] when Term.eq_constr c (Lazy.force cpair) ->
+      if not (mk_bool cbad) then s
+      else Structures.error ("Step number " ^ string_of_int !cpt ^
+                             " (" ^ string_coq_constr
+                               (fst (Term.decompose_app step)) ^ ")" ^
+                             " of the certificate likely failed." )
+    | _ -> assert false
+  in
+
+  List.fold_left debug_step s steps |> ignore;
+
+  Structures.error ("Debug checker is only meant to be used for certificates \
+                     that fail to be checked by SMTCoq.")
+
+
 
 (* Tactic *)
 
-let build_body rt ro ra rf l b (max_id, confl) find =
+let build_body rt ro ra rf l b (max_id, confl) vm_cast find =
   let nti = mkName "t_i" in
   let ntfunc = mkName "t_func" in
   let ntatom = mkName "t_atom" in
@@ -291,34 +582,49 @@ let build_body rt ro ra rf l b (max_id, confl) find =
   let t_func = Structures.lift 1 (make_t_func ro (v 0 (*t_i - 1*))) in
   let t_atom = Atom.interp_tbl ra in
   let t_form = snd (Form.interp_tbl rf) in
-  let (tres,_,cuts) = SmtTrace.to_coq Form.to_coq interp_conseq_uf (certif_ops (Some [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|])) confl find in
+  let (tres,_,cuts) = SmtTrace.to_coq Form.to_coq
+      (interp_conseq_uf t_i)
+      (certif_ops
+         (Some [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|]))
+      confl find
+  in
   let certif =
-    mklApp cCertif [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*); mkInt (max_id + 1); tres;mkInt (get_pos confl)|] in
+    mklApp cCertif
+      [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*);
+        mkInt (max_id + 1); tres;mkInt (get_pos confl)|] in
 
-  let proof_cast =
-    Term.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_eqb|],
-    Term.mkLetIn (ntfunc, t_func, mklApp carray [|mklApp ctval [|v 1 (*t_i*)|]|],
+  let add_lets t =
+    Term.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_compdec|],
+    Term.mkLetIn (ntfunc, t_func, mklApp carray [|mklApp ctval [|v 1(*t_i*)|]|],
     Term.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|],
     Term.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|],
-    Term.mkLetIn (nc, certif, mklApp ccertif [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|],
-    mklApp cchecker_b_correct
-      [|v 5 (*t_i*);v 4 (*t_func*);v 3 (*t_atom*); v 2 (*t_form*); l; b; v 1 (*certif*);
-	vm_cast_true (mklApp cchecker_b [|v 5 (*t_i*);v 4 (*t_func*);v 3 (*t_atom*); v 2 (*t_form*); l; b; v 1 (*certif*)|])|])))))
+    Term.mkLetIn (nc, certif, mklApp ccertif
+             [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|],
+    t))))) in
+
+  let cbc =
+    add_lets
+      (mklApp cchecker_b [|v 5 (*t_i*);v 4 (*t_func*);v 3 (*t_atom*);
+                           v 2 (*t_form*); l; b; v 1 (*certif*)|])
+    |> vm_cast
   in
+
+  let proof_cast =
+    add_lets
+      (mklApp cchecker_b_correct
+         [|v 5 (*t_i*);v 4 (*t_func*);v 3 (*t_atom*); v 2 (*t_form*);
+           l; b; v 1 (*certif*); cbc |]) in
+
   let proof_nocast =
-    Term.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_eqb|],
-    Term.mkLetIn (ntfunc, t_func, mklApp carray [|mklApp ctval [|v 1 (*t_i*)|]|],
-    Term.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|],
-    Term.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|],
-    Term.mkLetIn (nc, certif, mklApp ccertif [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|],
-    mklApp cchecker_b_correct
-      [|v 5 (*t_i*);v 4 (*t_func*);v 3 (*t_atom*); v 2 (*t_form*); l; b; v 1 (*certif*)|])))))
-  in
+    add_lets
+      (mklApp cchecker_b_correct
+         [|v 5 (*t_i*);v 4 (*t_func*);v 3 (*t_atom*); v 2 (*t_form*);
+           l; b; v 1 (*certif*)|]) in
 
   (proof_cast, proof_nocast, cuts)
 
 
-let build_body_eq rt ro ra rf l1 l2 l (max_id, confl) find =
+let build_body_eq rt ro ra rf l1 l2 l (max_id, confl) vm_cast find =
   let nti = mkName "t_i" in
   let ntfunc = mkName "t_func" in
   let ntatom = mkName "t_atom" in
@@ -331,28 +637,39 @@ let build_body_eq rt ro ra rf l1 l2 l (max_id, confl) find =
   let t_func = Structures.lift 1 (make_t_func ro (v 0 (*t_i*))) in
   let t_atom = Atom.interp_tbl ra in
   let t_form = snd (Form.interp_tbl rf) in
-  let (tres,_,cuts) = SmtTrace.to_coq Form.to_coq interp_conseq_uf (certif_ops (Some [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|])) confl find in
+  let (tres,_,cuts) = SmtTrace.to_coq Form.to_coq
+      (interp_conseq_uf t_i)
+      (certif_ops (Some [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|])) confl find in
   let certif =
     mklApp cCertif [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*); mkInt (max_id + 1); tres;mkInt (get_pos confl)|] in
 
-  let proof_cast =
-    Term.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_eqb|],
-    Term.mkLetIn (ntfunc, t_func, mklApp carray [|mklApp ctval [|v 1 (*t_i*)|]|],
+  let add_lets t =
+    Term.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_compdec|],
+    Term.mkLetIn (ntfunc, t_func, mklApp carray [|mklApp ctval [|v 1(*t_i*)|]|],
     Term.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|],
     Term.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|],
-    Term.mkLetIn (nc, certif, mklApp ccertif [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|],
-    mklApp cchecker_eq_correct
-      [|v 5 (*t_i*);v 4 (*t_func*);v 3 (*t_atom*); v 2 (*t_form*); l1; l2; l; v 1 (*certif*);
-	vm_cast_true (mklApp cchecker_eq [|v 5 (*t_i*);v 4 (*t_func*);v 3 (*t_atom*); v 2 (*t_form*); l1; l2; l; v 1 (*certif*)|])|])))))
+    Term.mkLetIn (nc, certif, mklApp ccertif
+             [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|],
+    t))))) in
+
+  let ceqc =
+    add_lets
+      (mklApp cchecker_eq [|v 5 (*t_i*);v 4 (*t_func*);v 3 (*t_atom*);
+                            v 2 (*t_form*); l1; l2; l; v 1 (*certif*)|])
+      |> vm_cast
+  in
+
+  let proof_cast =
+    add_lets
+      (mklApp cchecker_eq_correct
+         [|v 5 (*t_i*);v 4 (*t_func*);v 3 (*t_atom*); v 2 (*t_form*);
+           l1; l2; l; v 1 (*certif*); ceqc|])
   in
   let proof_nocast =
-    Term.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_eqb|],
-    Term.mkLetIn (ntfunc, t_func, mklApp carray [|mklApp ctval [|v 1 (*t_i*)|]|],
-    Term.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|],
-    Term.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|],
-    Term.mkLetIn (nc, certif, mklApp ccertif [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|],
-    mklApp cchecker_eq_correct
-      [|v 5 (*t_i*);v 4 (*t_func*);v 3 (*t_atom*); v 2 (*t_form*); l1; l2; l; v 1 (*certif*)|])))))
+    add_lets
+      (mklApp cchecker_eq_correct
+         [|v 5 (*t_i*);v 4 (*t_func*);v 3 (*t_atom*); v 2 (*t_form*);
+           l1; l2; l; v 1 (*certif*)|])
   in
 
   (proof_cast, proof_nocast, cuts)
@@ -366,23 +683,23 @@ let get_arguments concl =
   | _ -> failwith ("Verit.tactic: can only deal with equality over bool")
 
 
-let make_proof call_solver rt ro rf ra' rf' l' ls_smtc=
-  let fl' = Form.flatten rf' l' in
+let make_proof call_solver env rt ro ra' rf' l' ls_smtc =
   let root = SmtTrace.mkRootV [l'] in
-  call_solver rt ro ra' rf' (Some (root, l')) (fl'::ls_smtc)
+  call_solver env rt ro ra' rf' (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 the lemma. We also need to make sure to leave unchanged the tables because
  the new objects may contain bound (by forall of the lemma) variables. *)
 exception Axiom_form_unsupported
-              
-let of_coq_lemma rt ro ra' rf' env sigma clemma =
+
+let of_coq_lemma rt ro ra' rf' 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 =
     let fmap r = let n, t = Structures.destruct_rel_decl r in
-                 string_of_name n, SmtBtype.of_coq rt t in
+                 string_of_name n, SmtBtype.of_coq rt solver_logic t in
     List.map fmap rel_context in
   let f, args = Term.decompose_app qf_lemma in
   let core_f =
@@ -397,19 +714,20 @@ let of_coq_lemma rt ro ra' rf' env sigma 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' env_lemma sigma)
+  let core_smt = Form.of_coq (Atom.of_coq ~hash:true rt ro ra' solver_logic env_lemma sigma)
                    rf' core_f in
   match forall_args with
     [] -> core_smt
   | _ -> Form.get rf' (Fapp (Fforall forall_args, [|core_smt|]))
 
-let core_tactic call_solver rt ro ra rf ra' rf' lcpl lcepl env sigma concl =
+let core_tactic call_solver solver_logic rt ro ra rf ra' rf' 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 (Retyping.get_type_of env sigma) lcpl in
 
-  let lsmt  = List.map (of_coq_lemma rt ro ra' rf' env sigma) lcl in
+  let lsmt  = List.map (of_coq_lemma rt ro ra' rf' env sigma solver_logic) lcl in
   let l_pl_ls = List.combine (List.combine lcl lcpl) lsmt in
 
   let lem_tbl : (int, Term.constr * Term.constr) Hashtbl.t =
@@ -418,7 +736,7 @@ let core_tactic call_solver rt ro ra rf ra' rf' lcpl lcepl env sigma concl =
     Hashtbl.add lem_tbl (Form.index ls) (l, pl) in
 
   List.iter new_ref l_pl_ls;
-  
+
   let find_lemma cl =
     let re_hash hf = Form.hash_hform (Atom.hash_hatom ra') rf' hf in
     match cl.value with
@@ -427,39 +745,231 @@ let core_tactic call_solver rt ro ra rf ra' rf' lcpl lcepl env sigma concl =
        begin try Hashtbl.find lem_tbl (Form.index hl)
              with Not_found ->
                let oc = open_out "/tmp/find_lemma.log" in
-               List.iter (fun u -> Printf.fprintf oc "%s\n"
-                                     (VeritSyntax.string_hform u)) lsmt;
-               Printf.fprintf oc "\n%s\n" (VeritSyntax.string_hform hl);
+               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;
                flush oc; close_out oc; failwith "find_lemma" end
       | _ -> failwith "unexpected form of root" in
-  
+
   let (body_cast, body_nocast, cuts) =
-    if ((Term.eq_constr b (Lazy.force ctrue)) || (Term.eq_constr b (Lazy.force cfalse))) then
-      let l = Form.of_coq (Atom.of_coq rt ro ra env sigma) rf a in
-      let l' = Form.of_coq (Atom.of_coq ~hash:true rt ro ra' env sigma) rf' a in
-      let l' = if (Term.eq_constr b (Lazy.force ctrue)) then Form.neg l' else l' in
-      let max_id_confl = make_proof call_solver rt ro rf ra' rf' l' lsmt in
-      build_body rt ro ra rf (Form.to_coq l) b max_id_confl (Some find_lemma)
+    if ((Term.eq_constr b (Lazy.force ctrue)) ||
+        (Term.eq_constr b (Lazy.force cfalse))) then
+      let l = Form.of_coq (Atom.of_coq rt ro ra solver_logic env sigma) rf a in
+      let l' = Form.of_coq (Atom.of_coq ~hash:true rt ro ra' solver_logic env sigma) rf' a in
+      let l' =
+        if (Term.eq_constr b (Lazy.force ctrue)) then Form.neg l' else l' in
+      let max_id_confl = make_proof call_solver env rt ro ra' rf' l' lsmt in
+      build_body rt ro ra rf (Form.to_coq l) b max_id_confl (vm_cast env) (Some find_lemma)
     else
-      let l1 = Form.of_coq (Atom.of_coq rt ro ra env sigma) rf a in
-      let l2 = Form.of_coq (Atom.of_coq rt ro ra env sigma) rf b in
+      let l1 = Form.of_coq (Atom.of_coq rt ro ra solver_logic env sigma) rf a in
+      let l2 = Form.of_coq (Atom.of_coq rt ro ra solver_logic env sigma) rf b in
       let l = Form.neg (Form.get rf (Fapp(Fiff,[|l1;l2|]))) in
-      let l1' = Form.of_coq (Atom.of_coq ~hash:true rt ro ra' env sigma) rf' a in
-      let l2' = Form.of_coq (Atom.of_coq ~hash:true rt ro ra' env sigma) rf' b in
+      let l1' = Form.of_coq (Atom.of_coq ~hash:true rt ro ra' solver_logic env sigma) rf' a in
+      let l2' = Form.of_coq (Atom.of_coq ~hash:true rt ro ra' solver_logic env sigma) rf' b in
       let l' = Form.neg (Form.get rf' (Fapp(Fiff,[|l1';l2'|]))) in
-      let max_id_confl = make_proof call_solver rt ro rf ra' rf' l' lsmt in
-      build_body_eq rt ro ra rf (Form.to_coq l1) (Form.to_coq l2) (Form.to_coq l) max_id_confl (Some find_lemma) in
+      let max_id_confl = make_proof call_solver env rt ro ra' rf' l' lsmt in
+      build_body_eq rt ro ra rf (Form.to_coq l1) (Form.to_coq l2)
+        (Form.to_coq l) max_id_confl (vm_cast env) (Some find_lemma) in
 
-  let cuts = SmtBtype.get_cuts rt @ cuts in
+      let cuts = (SmtBtype.get_cuts rt) @ cuts in
 
   List.fold_right (fun (eqn, eqt) tac ->
-      Structures.tclTHENLAST (Structures.assert_before (Names.Name eqn) eqt) tac)
-    cuts
+      Structures.tclTHENLAST
+        (Structures.assert_before (Names.Name eqn) eqt)
+        tac
+    ) cuts
     (Structures.tclTHEN
        (Structures.set_evars_tac body_nocast)
        (Structures.vm_cast_no_check body_cast))
 
-let tactic call_solver rt ro ra rf ra' rf' lcpl lcepl =
+
+let tactic call_solver solver_logic rt ro ra rf ra' rf' vm_cast lcpl lcepl =
   Structures.tclTHEN
     Tactics.intros
-    (Structures.mk_tactic (core_tactic call_solver rt ro ra rf ra' rf' lcpl lcepl))
+    (Structures.mk_tactic (core_tactic call_solver solver_logic rt ro ra rf ra' rf' vm_cast lcpl lcepl))
+
+
+(**********************************************)
+(* Show solver models as Coq counter-examples *)
+(**********************************************)
+
+
+open SExpr
+open Smtlib2_genConstr
+open Format
+
+
+let string_index_of_constr env i cf =
+  try
+    let s = string_coq_constr cf in
+    let nc = Environ.named_context env in
+    let nd = Environ.lookup_named (Names.id_of_string s) env in
+    let cpt = ref 0 in
+    (try List.iter (fun n -> incr cpt; if n == nd then raise Exit) nc
+     with Exit -> ());
+    s, !cpt
+  with _ -> string_coq_constr cf, -i
+
+
+let vstring_i env i =
+  let cf = SmtAtom.Atom.get_coq_term_op i in
+  if Term.isRel cf then
+    let dbi = Term.destRel cf in
+    let s =
+      Environ.lookup_rel dbi env
+      |> Structures.get_rel_dec_name
+      |> function
+      | Names.Name id -> Names.string_of_id id
+      | Names.Anonymous -> "?" in
+    s, dbi
+  else
+    string_index_of_constr env i cf
+
+
+let sstring_i env i v =
+  let tf = SmtBtype.get_coq_type_op i in
+  let (s, idx) = string_index_of_constr env i tf in
+  (s^"#"^v, idx)
+
+
+let smt2_id_to_coq_string env t_i ra rf name =
+  try
+    let l = String.split_on_char '_' name in
+    match l with
+      | ["op"; i] -> vstring_i env (int_of_string i)
+      | ["@uc"; "Tindex"; i; j] -> sstring_i env (int_of_string i) j
+      | _ -> raise Not_found
+  with _ -> (name, 0)
+
+
+let op_to_coq_string op = match op with
+  | "=" | "+" | "-" | "*" | "/" -> op
+  | "or" -> "||"
+  | "and" -> "&&"
+  | "xor" -> "xorb"
+  | "=>" -> "implb"
+  | _ -> op
+
+
+let coq_bv_string s =
+  let rec aux acc = function
+    | true :: r -> aux (acc ^ "|1") r
+    | false :: r -> aux (acc ^ "|0") r
+    | [] -> "#b" ^ acc ^ "|"
+  in
+  if String.length s < 3 ||
+     not (s.[0] = '#' && s.[1] = 'b') then failwith "not bv";
+  aux "" (parse_smt2bv s)
+
+
+let is_bvint bs =
+  try Scanf.sscanf bs "bv%s" (fun s ->
+      try ignore (Big_int.big_int_of_string s); true
+      with _ -> false)
+  with _ -> false
+
+
+let rec smt2_sexpr_to_coq_string env t_i ra rf =
+  let open SExpr in function
+  | Atom "true" -> "true"
+  | Atom "false" -> "false"
+  | Atom s ->
+    (try ignore (int_of_string s); s
+     with Failure _ ->
+     try coq_bv_string s
+     with Failure _ ->
+     try fst (smt2_id_to_coq_string env t_i ra rf s)
+     with _ -> s)
+  | List [Atom "as"; Atom "const"; _] -> "const_farray"
+  | List [Atom "as"; s; _] -> smt2_sexpr_to_coq_string env t_i ra rf s
+  | List [Atom "_"; Atom bs; Atom s] when is_bvint bs ->
+    Scanf.sscanf bs "bv%s" (fun i ->
+        coq_bv_string (bigint_bv (Big_int.big_int_of_string i)
+                         (int_of_string s)))
+  | List [Atom "-"; Atom _ as s] ->
+    sprintf "-%s"
+      (smt2_sexpr_to_coq_string env t_i ra rf s)
+  | List [Atom "-"; s] ->
+    sprintf "(- %s)"
+      (smt2_sexpr_to_coq_string env t_i ra rf s)
+  | List [Atom (("+"|"-"|"*"|"/"|"or"|"and"|"=") as op); s1; s2] ->
+    sprintf "%s %s %s"
+      (smt2_sexpr_to_coq_string env t_i ra rf s1)
+      (op_to_coq_string op)
+      (smt2_sexpr_to_coq_string env t_i ra rf s2)
+  | List [Atom (("xor"|"=>"|"") as op); s1; s2] ->
+    sprintf "(%s %s %s)"
+      (op_to_coq_string op)
+      (smt2_sexpr_to_coq_string env t_i ra rf s1)
+      (smt2_sexpr_to_coq_string env t_i ra rf s2)
+  | List [Atom "select"; a; i] ->
+    sprintf "%s[%s]"
+      (smt2_sexpr_to_coq_string env t_i ra rf a)
+      (smt2_sexpr_to_coq_string env t_i ra rf i)
+  | List [Atom "store"; a; i; v] ->
+    sprintf "%s[%s <- %s]"
+      (smt2_sexpr_to_coq_string env t_i ra rf a)
+      (smt2_sexpr_to_coq_string env t_i ra rf i)
+      (smt2_sexpr_to_coq_string env t_i ra rf v)
+  | List [Atom "ite"; c; s1; s2] ->
+    sprintf "if %s then %s else %s"
+      (smt2_sexpr_to_coq_string env t_i ra rf c)
+      (smt2_sexpr_to_coq_string env t_i ra rf s1)
+      (smt2_sexpr_to_coq_string env t_i ra rf s2)
+  | List l ->
+    sprintf "(%s)"
+      (String.concat " " (List.map (smt2_sexpr_to_coq_string env t_i ra rf) l))
+
+
+let str_contains s1 s2 =
+  let re = Str.regexp_string s2 in
+  try ignore (Str.search_forward re s1 0); true
+  with Not_found -> false
+
+let lambda_to_coq_string l s =
+  Format.sprintf "fun %s => %s"
+    (String.concat " "
+       (List.map (function
+            | List [Atom v; _] ->
+              if str_contains s v then v else "_"
+            | _ -> assert false) l))
+    s
+
+type model =
+  | Fun of ((string * int) * string)
+  | Sort
+
+let model_item env rt ro ra rf =
+  let t_i = make_t_i rt in
+  function
+  | List [Atom "define-fun"; Atom n; List []; _; expr] ->
+     Fun (smt2_id_to_coq_string env t_i ra rf n,
+           smt2_sexpr_to_coq_string env t_i ra rf expr)
+
+  | List [Atom "define-fun"; Atom n; List l; _; expr] ->
+     Fun (smt2_id_to_coq_string env t_i ra rf n,
+           lambda_to_coq_string l
+             (smt2_sexpr_to_coq_string env t_i ra rf expr))
+
+  | List [Atom "declare-sort"; Atom n; _] ->
+     Sort
+
+  | l ->
+     (* let out = open_out_gen [Open_append] 700 "/tmp/test.log" in
+      * let outf = Format.formatter_of_out_channel out in
+      * SExpr.print outf l; pp_print_flush outf ();
+      * close_out out; *)
+     Structures.error ("Could not reconstruct model")
+
+
+let model env rt ro ra rf = function
+  | List (Atom "model" :: l) ->
+     List.fold_left (fun acc m -> match model_item env rt ro ra rf m with Fun m -> m::acc | Sort -> acc) [] l
+     |> List.sort (fun ((_ ,i1), _) ((_, i2), _) -> i2 - i1)
+  | _ -> Structures.error ("No model")
+
+
+let model_string env rt ro ra rf s =
+  String.concat "\n"
+    (List.map (fun ((x, _) ,v) -> Format.sprintf "%s := %s" x v)
+       (model env rt ro ra rf s))