GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-11-11 08:37:35 +03:00
Code Issues Projects Releases Wiki Activity

Use sbv version 7.7. Fixes #486.

Browse Source 
Also add regression test for #486.
This commit is contained in:
Brian Huffman 2018-04-30 09:54:26 -07:00
parent 42e89b11ae
commit 62dfa1d58f
3 changed files with 9 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
cryptol.cabal
View File

@ -58,7 +58,7 @@ library
pretty >= 1.1,
process >= 1.2,
random >= 1.0.1,
sbv >= 7.0,
sbv >= 7.7,
simple-smt >= 0.7.1,
strict,
text >= 1.1,
@ -262,5 +262,5 @@ benchmark cryptol-bench
, deepseq
, directory
, filepath
, sbv >= 7.0
, sbv >= 7.7
, text

3
tests/issues/issue486.icry Normal file
View File

@ -0,0 +1,3 @@
:prove \(x:Integer) -> x ^^ integer`{0} == integer`{1}
:prove \(x:Integer) -> x ^^ integer`{1} == x
:prove \(x:Integer) -> x ^^ integer`{5} == x * x * x * x * x

4
tests/issues/issue486.icry.stdout Normal file
View File

@ -0,0 +1,4 @@
Loading module Cryptol
Q.E.D.
Q.E.D.
Q.E.D.