diff options
| author | Chantal Keller <Chantal.Keller@lri.fr> | 2016-09-28 15:33:17 +0200 |
|---|---|---|
| committer | Chantal Keller <Chantal.Keller@lri.fr> | 2016-09-28 15:33:17 +0200 |
| commit | b3f7d3361fac0d1771e6ea3eb277ad858ce38760 (patch) | |
| tree | fdf80fcee557857bf70912f2b98831a53b3be8ad /unit-tests | |
| parent | 73e19ad0aac3cbd472b8add74594bbc158fce334 (diff) | |
| download | smtcoq-b3f7d3361fac0d1771e6ea3eb277ad858ce38760.tar.gz smtcoq-b3f7d3361fac0d1771e6ea3eb277ad858ce38760.zip | |
Hopefully solved the problem with universes for the tactic
Diffstat (limited to 'unit-tests')
| -rw-r--r-- | unit-tests/Tests_verit.v | 17 | ||||
| -rw-r--r-- | unit-tests/Tests_zchaff.v | 10 |
2 files changed, 27 insertions, 0 deletions
diff --git a/unit-tests/Tests_verit.v b/unit-tests/Tests_verit.v index ccc2714..54916fa 100644 --- a/unit-tests/Tests_verit.v +++ b/unit-tests/Tests_verit.v @@ -4,6 +4,16 @@ Require Import Bool PArray Int63 List ZArith. Local Open Scope int63_scope. +(* First a tactic, to test the universe computation in an empty + environment. *) + +Lemma check_univ (x1: bool): + (x1 && (negb x1)) = false. +Proof. + verit. +Qed. + + (* veriT vernacular commands *) Section Checker_Sat0. @@ -912,3 +922,10 @@ Goal forall (P:Z -> Z -> bool) x y z, Proof. verit. Qed. + + +(* + Local Variables: + coq-load-path: ((rec "../src" "SMTCoq")) + End: +*) diff --git a/unit-tests/Tests_zchaff.v b/unit-tests/Tests_zchaff.v index fe973f8..106e25d 100644 --- a/unit-tests/Tests_zchaff.v +++ b/unit-tests/Tests_zchaff.v @@ -4,6 +4,16 @@ Require Import Bool PArray Int63 List ZArith. Local Open Scope int63_scope. +(* First a tactic, to test the universe computation in an empty + environment. *) + +Lemma check_univ (x1: bool): + (x1 && (negb x1)) = false. +Proof. + zchaff. +Qed. + + (* zChaff vernacular commands *) Time Zchaff_Checker "sat1.cnf" "sat1.zlog". |