diff options
| author | QGarchery <QGarchery@users.noreply.github.com> | 2019-02-12 10:32:49 +0100 |
|---|---|---|
| committer | ckeller <ckeller@users.noreply.github.com> | 2019-02-12 10:32:49 +0100 |
| commit | 769c2054cc14af50e70a38b0d2340ae6170863e0 (patch) | |
| tree | d8ea9b89f915d195cbd0ddd4d73520df6c9706ea /unit-tests | |
| parent | 9e1615b8bdd080f2331bce6b62f5f243950e43d7 (diff) | |
| download | smtcoq-769c2054cc14af50e70a38b0d2340ae6170863e0.tar.gz smtcoq-769c2054cc14af50e70a38b0d2340ae6170863e0.zip | |
equalities on array and bv types (#34)
Diffstat (limited to 'unit-tests')
| -rw-r--r-- | unit-tests/Tests_lfsc.v | 20 |
1 files changed, 9 insertions, 11 deletions
diff --git a/unit-tests/Tests_lfsc.v b/unit-tests/Tests_lfsc.v index 48d2d2b..05a9fb4 100644 --- a/unit-tests/Tests_lfsc.v +++ b/unit-tests/Tests_lfsc.v @@ -46,12 +46,11 @@ Local Open Scope bv_scope. smt. Qed. - (* TODO: will be ok when symmetry of equality is back for verit *) - (* Goal forall (bv1 bv2: bitvector 4), *) - (* bv1 = bv2 <-> bv2 = bv1. *) - (* Proof. *) - (* smt. *) - (* Qed. *) + Goal forall (bv1 bv2: bitvector 4), + bv1 = bv2 <-> bv2 = bv1. + Proof. + smt. + Qed. End BV. @@ -689,11 +688,10 @@ Section A_BV_EUF_LIA_PR. smt. Qed. - (* TODO: will be ok when symmetry of equality is back for verit *) - (* Goal forall (a b: farray Z Z), a = b <-> b = a. *) - (* Proof. *) - (* smt. *) - (* Qed. *) + Goal forall (a b: farray Z Z), a = b <-> b = a. + Proof. + smt. + Qed. End A_BV_EUF_LIA_PR. |