diff options
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. |