Merge from LFSC (#26)

* Showing models as coq counter examples in tactic without constructing coq terms

* also read models when calling cvc4 with a file (deactivated because cvc4 crashes)

* Show counter examples with variables in the order they are quantified in the Coq goal

* Circumvent issue with ocamldep

* fix issue with dependencies

* fix issue with dependencies

* Translation and OCaml support for extract, zero_extend, sign_extend

* Show run times of components

* print time on stdout instead

* Tests now work with new version (master) of CVC4

* fix small printing issue

* look for date on mac os x

* proof of valid_check_bbShl: some cases to prove.

* full proof of "left shift checker".

*  full proof of "rigth shift checker".

* Support translation of terms bvlshr, bvshl but LFSC rules do not exists at the moment
Bug fix for bitvector extract (inverted arguments)

* Typo

* More modularity on the format of traces depending on the version of coq

* More straightforward definitions in Int63Native_standard

* Use the Int31 library with coq-8.5

* Use the most efficient operations of Int31

* Improved performance with coq-8.5

* Uniform treatment of sat and smt tactics

* Hopefully solved the problem with universes for the tactic

* Updated the installation instructions

* Holes for unsupported bit blasting rules

* Cherry-picking from smtcoq/smtcoq

* bug fix hole for bitblast

* Predefined arrays are not required anymore

* fix issue with coq bbT and bitof construction from ocaml

* bug fix in smtAtom for uninterpreted functions
fix verit test file

* fix issue with smtlib2 extract parsing

* It looks like we still need the PArray function instances for some examples (see vmcai_bytes.smt2)

* Solver specific reification:
Each solver has a list of supported theories which is passed to Atom.of_coq, this function creates uninterpreted functions / sorts for unsupported features.

* show counter-examples with const_farray instead of const for constant array definitions

* Vernacular commands to debug checkers.
Verit/Lfsc_Checker_Debug will always fail, reporting the first proof step of the certificate that failed be checked

* Update INSTALL.md

* show smtcoq proof when converting

* (Hopefully) repared the universes problems

* Corrected a bug with holes in proofs

* scripts for tests:
create a folder "work" under "lfsc/tests/", locate the benchmarks there.
create a folder "results" under "lfsc/tests/work/" in which you'll find the results of ./cvc4tocoq.

* make sure to give correct path for your benchs...

* Checker for array extensionality modulo symmetry of equality

* fix oversight with bitvectors larger than 63 bits

* some printing functions for smt2 ast

* handle smtlib2 files with more complicated equivalence with (= ... )

* revert: ./cvc4tocoq does not output lfsc proofs...

* bug fix one input was ignored

* Don't show verit translation of LFSC proof if environment variable DONTSHOWVERIT is set
(e.g. put export DONTSHOWVERIT="" in your .bashrc or .bashprofile)

* Also sort names of introduced variables when showing counter-example

* input files for which SMTCoq retuns false.

* input files for which SMTCoq retuns false.

* use debug checker for debug file

* More efficient debug checker

* better approximate number of failing step of certificate in debug checker

* fix mistake in ml4

* very first attempt to support goals in Prop

* bvs: comparison predicates in Prop and their <-> proofs with the ones in bool
farrays: equality predicate in Prop and its <-> proof with the one in bool.

* unit, Bool, Z, Pos: comparison and equality predicates in Prop.

* a typo fixed.

* an example of array equality in  Prop (converted into Bool by hand)...
TODO: enhance the search space of cvc4 tactic.

* first version of cvc4' tactic: "solves" the goals in Prop.
WARNING: supports only bv and array goals and might not be complete
TODO: add support for lia goals

* cvc4' support for lia
WARNING: might not be complete!

* small fix in cvc4' and some variations of examples

* small fix + support for goals in Bool and Bool = true + use of solve tactical
WARNING: does not support UF and INT63 goals in Prop

* cvc4': better arrangement

* cvc4': Prop2Bool by context search...

* cvc4': solve tactial added -> do not modify unsolved goals.

* developer documentation for the smtcoq repo

* cvc4': rudimentary support for uninterpreted function goals in Prop.

* cvc4': support for goals with Leibniz equality...
WARNING: necessary use of "Grab Existential Variables." to instantiate variable types for farrays!

* cvc4': Z.lt adapted + better support from verit...

* cvc4': support for Z.le, Z.ge, Z.gt.

* Try arrays with default value (with a constructor for constant arrays), but extensionality is not provable

* cvc4': support for equality over uninterpreted types

* lfsc demo: goals in Coq's Prop.

* lfsc demo: goals in Bool.

* Fix issue with existential variables generated by prop2bool.
- prop2bool tactic exported by SMTCoq
- remove useless stuff

* update usage and installation instructions

* Update INSTALL.md

* highlighting

* the tactic: bool2prop.

* clean up

* the tactic smt: very first version.

* smt: return unsolved goals in Prop.

* Show when a certificate cannot be checked when running the tactic instead of at Qed

* Tactic improvements
- Handle negation/True/False in prop/bool conversions tactic.
- Remove alias for farray (this caused problem for matching on this type in tactics).
- Tactic `smt` that combines cvc4 and veriT.
- return subgoals in prop

* test change header

* smt: support for negated goals + some reorganization.

* conflicts resolved + some reorganization.

* a way to solve the issue with ambiguous coercions.

* reorganization.

* small change.

* another small change.

* developer documentation of the tactics.

* developer guide: some improvements.

* developer guide: some more improvements.

* developer guide: some more improvements.

* developer guide: some more improvements.

* pass correct environment for conversion + better error messages

* cleaning

* ReflectFacts added.

* re-organizing developers' guide.

* re-organizing developers' guide.

* re-organizing developers' guide.

* removing unused maps.

* headers.

* artifact readme getting started...

* first attempt

* second...

* third...

* 4th...

* 5th...

* 6th...

* 7th...

* 8th...

* 9th...

* 10th...

* 11th...

* 12th...

* 13th...

* 14th...

* 15th...

* 16th...

* 17th...

* Update artifact.md

Use links to lfsc repository like in the paper

* 18th...

* 19th...

* 20th...

* 21st...

* 22nd...

* 23rd...

* 24th...

* 25th...

* 26th...

* 27th...

* 28th...

* Update artifact.md

Small reorganization

* minor edits

* More minor edits

* revised description of tactics

* Final pass

* typo

* name changed: artifact-readme.md

* file added...

* passwd chaged...

* links...

* removal

* performance statement...

* typos...

* the link to the artifact image updated...

* suggestions by Guy...

* aux files removed...

* clean-up...

* clean-up...

* some small changes...

* small fix...

* additional information on newly created files after running cvc4tocoq script...

* some small fix...

* another small fix...

* typo...

* small fix...

* another small fix...

* fix...

* link to the artifact image...

* We do not want to force vm_cast for the Theorem commands

* no_check variants of the tactics

* TODO: a veriT test does not work anymore

* Compiles with both versions of Coq

* Test of the tactics in real conditions

* Comment on this case study

* an example for the FroCoS paper.

* Fix smt tactic that doesn't return cvc4's subgoals

* readme modifications

* readme modifications 2

* small typo in readme.

* small changes in readme.

* small changes in readme.

* typo in readme.

* Sync with https://github.com/LFSC/smtcoq

* Port to Coq 8.6

* README

* README

* INSTALL

* Missing file

* Yves' proposition for installation instructions

* Updated link to CVC4

* Compiles again with native-coq

* Compiles with both versions of Coq

* Command to bypass typechecking when generating a zchaff theorem

* Solved bug on cuts from Hole

* Counter-models for uninterpreted sorts (improves issue #13)

* OCaml version note (#15)

* update .gitignore

* needs OCaml 4.04.0

* Solving merge issues (under progress)

* Make SmtBtype compile

* Compilation of SmtForm under progress

* Make SmtForm compile

* Make SmtCertif compile

* Make SmtTrace compile

* Make SatAtom compile

* Make smtAtom compile

* Make CnfParser compile

* Make Zchaff compile

* Make VeritSyntax compile

* Make VeritParser compile

* Make lfsc/tosmtcoq compile

* Make smtlib2_genconstr compile

* smtCommand under progress

* smtCommands and verit compile again

* lfsc compiles

* ml4 compiles

* Everything compiles

* All ZChaff unit tests and most verit unit tests (but taut5 and un_menteur) go through

* Most LFSC tests ok; some fail due to the problem of verit; a few fail due to an error "Not_found" to investigate

* Authors and headings

* Compiles with native-coq

* Typo

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))