diff options
| author | Chantal Keller <Chantal.Keller@lri.fr> | 2016-04-26 00:30:35 +0200 |
|---|---|---|
| committer | Chantal Keller <Chantal.Keller@lri.fr> | 2016-04-26 00:30:35 +0200 |
| commit | 9f9699c8134ed0ded42aad64e00cfb9f0a60c914 (patch) | |
| tree | 2e34b34bf43380bfbdcf6e57fd41cc5773b0b3c6 /unit-tests | |
| parent | 5ebe1f1c3684609dc0c2f360cf4d86486795ab54 (diff) | |
| download | smtcoq-9f9699c8134ed0ded42aad64e00cfb9f0a60c914.tar.gz smtcoq-9f9699c8134ed0ded42aad64e00cfb9f0a60c914.zip | |
- Solved the Coq 8.5 problem relating to declaring section variables
- Correct equality check of atoms and formulas for processing congruence closure
Diffstat (limited to 'unit-tests')
| -rw-r--r-- | unit-tests/Tests_verit.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/unit-tests/Tests_verit.v b/unit-tests/Tests_verit.v index 2be8752..53cb9fb 100644 --- a/unit-tests/Tests_verit.v +++ b/unit-tests/Tests_verit.v @@ -134,8 +134,8 @@ End Checker_Let2. Section Sat0. - 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. + 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. End Sat0. Section Sat1. @@ -287,7 +287,7 @@ End Let2. Section Theorem_Sat0. - Time Verit_Theorem theorem_sat1 "sat0.smt2" "sat0.vtlog". + Time Verit_Theorem theorem_sat0 "sat0.smt2" "sat0.vtlog". End Theorem_Sat0. Section Theorem_Sat1. |