diff options
| author | Chantal Keller <Chantal.Keller@inria.fr> | 2019-02-07 19:40:56 +0100 |
|---|---|---|
| committer | Chantal Keller <Chantal.Keller@inria.fr> | 2019-02-07 19:40:56 +0100 |
| commit | d813320d18db7c065cb8fda0cdc5785045d1a6c8 (patch) | |
| tree | 3a3219d486e9949640d22023336342ef6d265397 /unit-tests | |
| parent | 296e3c78c2d56f0e08d654cb473f86f5b24375f4 (diff) | |
| download | smtcoq-d813320d18db7c065cb8fda0cdc5785045d1a6c8.tar.gz smtcoq-d813320d18db7c065cb8fda0cdc5785045d1a6c8.zip | |
PR #28 solves some problems in the tests of the "smt" tactics
Diffstat (limited to 'unit-tests')
| -rw-r--r-- | unit-tests/Tests_lfsc.v | 26 |
1 files changed, 12 insertions, 14 deletions
diff --git a/unit-tests/Tests_lfsc.v b/unit-tests/Tests_lfsc.v index 2f74ac2..48d2d2b 100644 --- a/unit-tests/Tests_lfsc.v +++ b/unit-tests/Tests_lfsc.v @@ -114,14 +114,13 @@ Section EUF. smt. Qed. - (* TODO: will be ok when symmetry of equality is back for verit *) - (* Goal forall *) - (* (x y: Z) *) - (* (f: Z -> Z), *) - (* (f x) = (f y) -> (f y) = (f x). *) - (* Proof. *) - (* smt. *) - (* Qed. *) + Goal forall + (x y: Z) + (f: Z -> Z), + (f x) = (f y) -> (f y) = (f x). + Proof. + smt. + Qed. Goal forall @@ -155,11 +154,10 @@ End EUF. Section LIA. - (* TODO: will be ok when symmetry of equality is back for verit *) - (* Goal forall (a b: Z), a = b <-> b = a. *) - (* Proof. *) - (* smt. *) - (* Qed. *) + Goal forall (a b: Z), a = b <-> b = a. + Proof. + smt. + Qed. Goal forall (x y: Z), (x >= y) -> (y < x) \/ (x = y). Proof. @@ -693,7 +691,7 @@ Section A_BV_EUF_LIA_PR. (* TODO: will be ok when symmetry of equality is back for verit *) (* Goal forall (a b: farray Z Z), a = b <-> b = a. *) - (* Proof. *) + (* Proof. *) (* smt. *) (* Qed. *) |