diff options
author | Chantal Keller <Chantal.Keller@lri.fr> | 2016-04-29 02:25:12 +0200 |
---|---|---|
committer | Chantal Keller <Chantal.Keller@lri.fr> | 2016-04-29 02:25:12 +0200 |
commit | 640bf0dda4a4880aeb525d1460dc91f5041aa626 (patch) | |
tree | 68dfa3afc15c76979364cab6fe10c06f16d9d842 /unit-tests | |
parent | d734e4eae47b0b7f13626053663d236faa7f69e6 (diff) | |
download | smtcoq-640bf0dda4a4880aeb525d1460dc91f5041aa626.tar.gz smtcoq-640bf0dda4a4880aeb525d1460dc91f5041aa626.zip |
Possibility to embed any Coq proof in certificates (not tested yet)
Diffstat (limited to 'unit-tests')
-rw-r--r-- | unit-tests/Tests_verit.v | 60 |
1 files changed, 30 insertions, 30 deletions
diff --git a/unit-tests/Tests_verit.v b/unit-tests/Tests_verit.v index e63bbaf..b5edddd 100644 --- a/unit-tests/Tests_verit.v +++ b/unit-tests/Tests_verit.v @@ -135,153 +135,153 @@ End Checker_Let2. Section Sat0. Parse_certif_verit t_i0 t_func0 t_atom0 t_form0 root0 used_roots0 trace0 "sat0.smt2" "sat0.vtlog". - Compute Euf_Checker.checker t_i0 t_func0 t_atom0 t_form0 root0 used_roots0 trace0. + Compute @Euf_Checker.checker t_i0 t_func0 t_atom0 t_form0 root0 used_roots0 trace0. End Sat0. Section Sat1. Parse_certif_verit t_i1 t_func1 t_atom1 t_form1 root1 used_roots1 trace1 "sat1.smt2" "sat1.vtlog". - Compute Euf_Checker.checker t_i1 t_func1 t_atom1 t_form1 root1 used_roots1 trace1. + Compute @Euf_Checker.checker t_i1 t_func1 t_atom1 t_form1 root1 used_roots1 trace1. End Sat1. Section Sat2. Parse_certif_verit t_i2 t_func2 t_atom2 t_form2 root2 used_roots2 trace2 "sat2.smt2" "sat2.vtlog". - Compute Euf_Checker.checker t_i2 t_func2 t_atom2 t_form2 root2 used_roots2 trace2. + Compute @Euf_Checker.checker t_i2 t_func2 t_atom2 t_form2 root2 used_roots2 trace2. End Sat2. Section Sat3. Parse_certif_verit t_i3 t_func3 t_atom3 t_form3 root3 used_roots3 trace3 "sat3.smt2" "sat3.vtlog". - Compute Euf_Checker.checker t_i3 t_func3 t_atom3 t_form3 root3 used_roots3 trace3. + Compute @Euf_Checker.checker t_i3 t_func3 t_atom3 t_form3 root3 used_roots3 trace3. End Sat3. Section Sat4. Parse_certif_verit t_i4 t_func4 t_atom4 t_form4 root4 used_roots4 trace4 "sat4.smt2" "sat4.vtlog". - Compute Euf_Checker.checker t_i4 t_func4 t_atom4 t_form4 root4 used_roots4 trace4. + Compute @Euf_Checker.checker t_i4 t_func4 t_atom4 t_form4 root4 used_roots4 trace4. End Sat4. Section Sat5. Parse_certif_verit t_i5 t_func5 t_atom5 t_form5 root5 used_roots5 trace5 "sat5.smt2" "sat5.vtlog". - Compute Euf_Checker.checker t_i5 t_func5 t_atom5 t_form5 root5 used_roots5 trace5. + Compute @Euf_Checker.checker t_i5 t_func5 t_atom5 t_form5 root5 used_roots5 trace5. End Sat5. Section Sat6. Parse_certif_verit t_i6 t_func6 t_atom6 t_form6 root6 used_roots6 trace6 "sat6.smt2" "sat6.vtlog". - Compute Euf_Checker.checker t_i6 t_func6 t_atom6 t_form6 root6 used_roots6 trace6. + Compute @Euf_Checker.checker t_i6 t_func6 t_atom6 t_form6 root6 used_roots6 trace6. End Sat6. Section Sat7. Parse_certif_verit t_i7 t_func7 t_atom7 t_form7 root7 used_roots7 trace7 "sat7.smt2" "sat7.vtlog". - Compute Euf_Checker.checker t_i7 t_func7 t_atom7 t_form7 root7 used_roots7 trace7. + Compute @Euf_Checker.checker t_i7 t_func7 t_atom7 t_form7 root7 used_roots7 trace7. End Sat7. Section Sat8. Parse_certif_verit t_i8 t_func8 t_atom8 t_form8 root8 used_roots8 trace8 "sat8.smt2" "sat8.vtlog". - Compute Euf_Checker.checker t_i8 t_func8 t_atom8 t_form8 root8 used_roots8 trace8. + Compute @Euf_Checker.checker t_i8 t_func8 t_atom8 t_form8 root8 used_roots8 trace8. End Sat8. Section Sat9. Parse_certif_verit t_i9 t_func9 t_atom9 t_form9 root9 used_roots9 trace9 "sat9.smt2" "sat9.vtlog". - Compute Euf_Checker.checker t_i9 t_func9 t_atom9 t_form9 root9 used_roots9 trace9. + Compute @Euf_Checker.checker t_i9 t_func9 t_atom9 t_form9 root9 used_roots9 trace9. End Sat9. (* Section Sat10. Parse_certif_verit t_i10 t_func10 t_atom10 t_form10 root10 used_roots10 trace10 "sat10.smt2" "sat10.vtlog". - Compute Euf_Checker.checker t_i10 t_func10 t_atom10 t_form10 root10 used_roots10 trace10. + Compute @Euf_Checker.checker t_i10 t_func10 t_atom10 t_form10 root10 used_roots10 trace10. End Sat10. *) Section Sat11. Parse_certif_verit t_i11 t_func11 t_atom11 t_form11 root11 used_roots11 trace11 "sat11.smt2" "sat11.vtlog". - Compute Euf_Checker.checker t_i11 t_func11 t_atom11 t_form11 root11 used_roots11 trace11. + Compute @Euf_Checker.checker t_i11 t_func11 t_atom11 t_form11 root11 used_roots11 trace11. End Sat11. Section Sat12. Parse_certif_verit t_i12 t_func12 t_atom12 t_form12 root12 used_roots12 trace12 "sat12.smt2" "sat12.vtlog". - Compute Euf_Checker.checker t_i12 t_func12 t_atom12 t_form12 root12 used_roots12 trace12. + Compute @Euf_Checker.checker t_i12 t_func12 t_atom12 t_form12 root12 used_roots12 trace12. End Sat12. Section Hole4. Parse_certif_verit t_i_hole4 t_func_hole4 t_atom_hole4 t_form_hole4 root_hole4 used_roots_hole4 trace_hole4 "hole4.smt2" "hole4.vtlog". - Compute Euf_Checker.checker t_i_hole4 t_func_hole4 t_atom_hole4 t_form_hole4 root_hole4 used_roots_hole4 trace_hole4. + Compute @Euf_Checker.checker t_i_hole4 t_func_hole4 t_atom_hole4 t_form_hole4 root_hole4 used_roots_hole4 trace_hole4. End Hole4. Section Uf1. Parse_certif_verit t_i_uf1 t_func_uf1 t_atom_uf1 t_form_uf1 root_uf1 used_roots_uf1 trace_uf1 "uf1.smt2" "uf1.vtlog". - Compute Euf_Checker.checker t_i_uf1 t_func_uf1 t_atom_uf1 t_form_uf1 root_uf1 used_roots_uf1 trace_uf1. + Compute @Euf_Checker.checker t_i_uf1 t_func_uf1 t_atom_uf1 t_form_uf1 root_uf1 used_roots_uf1 trace_uf1. End Uf1. Section Uf2. Parse_certif_verit t_i_uf2 t_func_uf2 t_atom_uf2 t_form_uf2 root_uf2 used_roots_uf2 trace_uf2 "uf2.smt2" "uf2.vtlog". - Compute Euf_Checker.checker t_i_uf2 t_func_uf2 t_atom_uf2 t_form_uf2 root_uf2 used_roots_uf2 trace_uf2. + Compute @Euf_Checker.checker t_i_uf2 t_func_uf2 t_atom_uf2 t_form_uf2 root_uf2 used_roots_uf2 trace_uf2. End Uf2. Section Uf3. Parse_certif_verit t_i_uf3 t_func_uf3 t_atom_uf3 t_form_uf3 root_uf3 used_roots_uf3 trace_uf3 "uf3.smt2" "uf3.vtlog". - Compute Euf_Checker.checker t_i_uf3 t_func_uf3 t_atom_uf3 t_form_uf3 root_uf3 used_roots_uf3 trace_uf3. + Compute @Euf_Checker.checker t_i_uf3 t_func_uf3 t_atom_uf3 t_form_uf3 root_uf3 used_roots_uf3 trace_uf3. End Uf3. Section Uf4. Parse_certif_verit t_i_uf4 t_func_uf4 t_atom_uf4 t_form_uf4 root_uf4 used_roots_uf4 trace_uf4 "uf4.smt2" "uf4.vtlog". - Compute Euf_Checker.checker t_i_uf4 t_func_uf4 t_atom_uf4 t_form_uf4 root_uf4 used_roots_uf4 trace_uf4. + Compute @Euf_Checker.checker t_i_uf4 t_func_uf4 t_atom_uf4 t_form_uf4 root_uf4 used_roots_uf4 trace_uf4. End Uf4. Section Uf5. Parse_certif_verit t_i_uf5 t_func_uf5 t_atom_uf5 t_form_uf5 root_uf5 used_roots_uf5 trace_uf5 "uf5.smt2" "uf5.vtlog". - Compute Euf_Checker.checker t_i_uf5 t_func_uf5 t_atom_uf5 t_form_uf5 root_uf5 used_roots_uf5 trace_uf5. + Compute @Euf_Checker.checker t_i_uf5 t_func_uf5 t_atom_uf5 t_form_uf5 root_uf5 used_roots_uf5 trace_uf5. End Uf5. Section Uf6. Parse_certif_verit t_i_uf6 t_func_uf6 t_atom_uf6 t_form_uf6 root_uf6 used_roots_uf6 trace_uf6 "uf6.smt2" "uf6.vtlog". - Compute Euf_Checker.checker t_i_uf6 t_func_uf6 t_atom_uf6 t_form_uf6 root_uf6 used_roots_uf6 trace_uf6. + Compute @Euf_Checker.checker t_i_uf6 t_func_uf6 t_atom_uf6 t_form_uf6 root_uf6 used_roots_uf6 trace_uf6. End Uf6. Section Uf7. Parse_certif_verit t_i_uf7 t_func_uf7 t_atom_uf7 t_form_uf7 root_uf7 used_roots_uf7 trace_uf7 "uf7.smt2" "uf7.vtlog". - Compute Euf_Checker.checker t_i_uf7 t_func_uf7 t_atom_uf7 t_form_uf7 root_uf7 used_roots_uf7 trace_uf7. + Compute @Euf_Checker.checker t_i_uf7 t_func_uf7 t_atom_uf7 t_form_uf7 root_uf7 used_roots_uf7 trace_uf7. End Uf7. Section Lia1. Parse_certif_verit t_i_lia1 t_func_lia1 t_atom_lia1 t_form_lia1 root_lia1 used_roots_lia1 trace_lia1 "lia1.smt2" "lia1.vtlog". - Compute Euf_Checker.checker t_i_lia1 t_func_lia1 t_atom_lia1 t_form_lia1 root_lia1 used_roots_lia1 trace_lia1. + Compute @Euf_Checker.checker t_i_lia1 t_func_lia1 t_atom_lia1 t_form_lia1 root_lia1 used_roots_lia1 trace_lia1. End Lia1. Section Lia2. Parse_certif_verit t_i_lia2 t_func_lia2 t_atom_lia2 t_form_lia2 root_lia2 used_roots_lia2 trace_lia2 "lia2.smt2" "lia2.vtlog". - Compute Euf_Checker.checker t_i_lia2 t_func_lia2 t_atom_lia2 t_form_lia2 root_lia2 used_roots_lia2 trace_lia2. + Compute @Euf_Checker.checker t_i_lia2 t_func_lia2 t_atom_lia2 t_form_lia2 root_lia2 used_roots_lia2 trace_lia2. End Lia2. Section Lia3. Parse_certif_verit t_i_lia3 t_func_lia3 t_atom_lia3 t_form_lia3 root_lia3 used_roots_lia3 trace_lia3 "lia3.smt2" "lia3.vtlog". - Compute Euf_Checker.checker t_i_lia3 t_func_lia3 t_atom_lia3 t_form_lia3 root_lia3 used_roots_lia3 trace_lia3. + Compute @Euf_Checker.checker t_i_lia3 t_func_lia3 t_atom_lia3 t_form_lia3 root_lia3 used_roots_lia3 trace_lia3. End Lia3. Section Lia4. Parse_certif_verit t_i_lia4 t_func_lia4 t_atom_lia4 t_form_lia4 root_lia4 used_roots_lia4 trace_lia4 "lia4.smt2" "lia4.vtlog". - Compute Euf_Checker.checker t_i_lia4 t_func_lia4 t_atom_lia4 t_form_lia4 root_lia4 used_roots_lia4 trace_lia4. + Compute @Euf_Checker.checker t_i_lia4 t_func_lia4 t_atom_lia4 t_form_lia4 root_lia4 used_roots_lia4 trace_lia4. End Lia4. Section Lia5. Parse_certif_verit t_i_lia5 t_func_lia5 t_atom_lia5 t_form_lia5 root_lia5 used_roots_lia5 trace_lia5 "lia5.smt2" "lia5.vtlog". - Compute Euf_Checker.checker t_i_lia5 t_func_lia5 t_atom_lia5 t_form_lia5 root_lia5 used_roots_lia5 trace_lia5. + Compute @Euf_Checker.checker t_i_lia5 t_func_lia5 t_atom_lia5 t_form_lia5 root_lia5 used_roots_lia5 trace_lia5. End Lia5. Section Lia6. Parse_certif_verit t_i_lia6 t_func_lia6 t_atom_lia6 t_form_lia6 root_lia6 used_roots_lia6 trace_lia6 "lia6.smt2" "lia6.vtlog". - Compute Euf_Checker.checker t_i_lia6 t_func_lia6 t_atom_lia6 t_form_lia6 root_lia6 used_roots_lia6 trace_lia6. + Compute @Euf_Checker.checker t_i_lia6 t_func_lia6 t_atom_lia6 t_form_lia6 root_lia6 used_roots_lia6 trace_lia6. End Lia6. Section Lia7. Parse_certif_verit t_i_lia7 t_func_lia7 t_atom_lia7 t_form_lia7 root_lia7 used_roots_lia7 trace_lia7 "lia7.smt2" "lia7.vtlog". - Compute Euf_Checker.checker t_i_lia7 t_func_lia7 t_atom_lia7 t_form_lia7 root_lia7 used_roots_lia7 trace_lia7. + Compute @Euf_Checker.checker t_i_lia7 t_func_lia7 t_atom_lia7 t_form_lia7 root_lia7 used_roots_lia7 trace_lia7. End Lia7. (* Section Let1. Parse_certif_verit t_i_let1 t_func_let1 t_atom_let1 t_form_let1 root_let1 used_roots_let1 trace_let1 "let1.smt2" "let1.vtlog". - Compute Euf_Checker.checker t_i_let1 t_func_let1 t_atom_let1 t_form_let1 root_let1 used_roots_let1 trace_let1. + Compute @Euf_Checker.checker t_i_let1 t_func_let1 t_atom_let1 t_form_let1 root_let1 used_roots_let1 trace_let1. End Let1. Section Let2. Parse_certif_verit t_i_let2 t_func_let2 t_atom_let2 t_form_let2 root_let2 used_roots_let2 trace_let2 "let2.smt2" "let2.vtlog". - Compute Euf_Checker.checker t_i_let2 t_func_let2 t_atom_let2 t_form_let2 root_let2 used_roots_let2 trace_let2. + Compute @Euf_Checker.checker t_i_let2 t_func_let2 t_atom_let2 t_form_let2 root_let2 used_roots_let2 trace_let2. End Let2. *) |