cryptol/tests/issues/issue1210.icry

mirror of https://github.com/GaloisInc/cryptol.git synced 2024-09-19 01:49:11 +03:00
:l issue1210.cry
:check
:set prover=sbv-z3
:prove
:set prover=w4-z3
:prove
Add a test case for issue #1210 This bug was fixed in What4 via https://github.com/GaloisInc/what4/pull/127 which was included in What4 version 1.2. Fixes #1210 2021-06-17 21:55:45 +03:00			`:l issue1210.cry`
			`:check`
			`:set prover=sbv-z3`
			`:prove`
			`:set prover=w4-z3`
			`:prove`