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