From 769c2054cc14af50e70a38b0d2340ae6170863e0 Mon Sep 17 00:00:00 2001 From: QGarchery Date: Tue, 12 Feb 2019 10:32:49 +0100 Subject: equalities on array and bv types (#34) --- unit-tests/Tests_lfsc.v | 20 +++++++++----------- 1 file changed, 9 insertions(+), 11 deletions(-) (limited to 'unit-tests') 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. -- cgit