diff options
| -rw-r--r-- | unit-tests/Tests.v | 42 |
1 files changed, 21 insertions, 21 deletions
diff --git a/unit-tests/Tests.v b/unit-tests/Tests.v index 5f75204..d011cdb 100644 --- a/unit-tests/Tests.v +++ b/unit-tests/Tests.v @@ -535,13 +535,13 @@ Section Checker_Lia7. Verit_Checker "lia7.smt2" "lia7.vtlog". End Checker_Lia7. -(* Section Checker_Let1. *) -(* Verit_Checker "let1.smt2" "let1.vtlog". *) -(* End Checker_Let1. *) +Section Checker_Let1. + Verit_Checker "let1.smt2" "let1.vtlog". +End Checker_Let1. -(* Section Checker_Let2. *) -(* Verit_Checker "let2.smt2" "let2.vtlog". *) -(* End Checker_Let2. *) +Section Checker_Let2. + Verit_Checker "let2.smt2" "let2.vtlog". +End Checker_Let2. Section Sat1. @@ -679,15 +679,15 @@ Section 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. *) -(* End Let1. *) +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. +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. *) -(* End Let2. *) +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. +End Let2. Section Theorem_Sat1. @@ -798,13 +798,13 @@ Section Theorem_Lia7. Time Verit_Theorem theorem_lia7 "lia7.smt2" "lia7.vtlog". End Theorem_Lia7. -(* Section Theorem_Let1. *) -(* Time Verit_Theorem theorem_let1 "let1.smt2" "let1.vtlog". *) -(* End Theorem_Let1. *) +Section Theorem_Let1. + Time Verit_Theorem theorem_let1 "let1.smt2" "let1.vtlog". +End Theorem_Let1. -(* Section Theorem_Let2. *) -(* Time Verit_Theorem theorem_let2 "let2.smt2" "let2.vtlog". *) -(* End Theorem_Let2. *) +Section Theorem_Let2. + Time Verit_Theorem theorem_let2 "let2.smt2" "let2.vtlog". +End Theorem_Let2. (* verit tactic *) @@ -1215,7 +1215,7 @@ Goal forall b, Proof. verit. Qed. -(* Ne marche pas car la coercion is_true inclut le [let in] +(* Does not work since the [is_true] coercion includes [let in] Goal forall b, let a := b in a || (negb a). |