GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-11-09 17:15:06 +03:00
Code Issues Projects Releases Wiki Activity

Generalize CheckEnum test case to include :prove commands

Browse Source
This commit is contained in:
Ryan Scott 2024-01-25 15:06:35 -05:00
parent dd6313c07b
commit 82526569eb
4 changed files with 26 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
tests/enum/CheckEnum.icry
View File

@ -1,2 +0,0 @@
:l CheckEnum.cry
:check

0
tests/enum/CheckEnum.cry → tests/enum/CheckProveEnum.cry
View File

10
tests/enum/CheckProveEnum.icry Normal file
View File

@ -0,0 +1,10 @@
:l CheckProveEnum.cry
:set prover-stats=off
:check
:set prover=sbv-z3
:prove
:set prover=w4-z3
:prove

16
tests/enum/CheckEnum.icry.stdout → tests/enum/CheckProveEnum.icry.stdout
View File

@ -13,3 +13,19 @@ Expected test coverage: 0.15% (100 of 65539 values)
property letterRotateProp Using exhaustive testing.
Testing... Passed 3 tests.
Q.E.D.
:prove maybeMapProp
Q.E.D.
:prove eitherMapProp
Q.E.D.
:prove fooMapProp
Q.E.D.
:prove letterRotateProp
Q.E.D.
:prove maybeMapProp
Q.E.D.
:prove eitherMapProp
Q.E.D.
:prove fooMapProp
Q.E.D.
:prove letterRotateProp
Q.E.D.