GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-12-24 16:31:34 +03:00
Code Issues Projects Releases Wiki Activity

Post-merge test suite fixups

Browse Source
This commit is contained in:
Rob Dockins 2020-05-26 17:45:42 -07:00
parent 23f22bbab7
commit 066cbd492e
2 changed files with 4 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
tests/issues/issue723.icry.stdout
View File

@ -12,9 +12,9 @@ Loading module Main
assuming
• fin k
the following constraints hold:
• k >= n`908
• k >= n`923
arising from
matching types
at issue723.cry:7:17--7:19
where
n`908 is signature variable 'n' at issue723.cry:1:6--1:7
n`923 is signature variable 'n' at issue723.cry:1:6--1:7

4
tests/issues/issue725.icry
View File

@ -3,12 +3,12 @@
:set prover=z3
:prove \(n:Integer, p : Bit) -> p ==> (x != x where x = 2 ^^ n)
:prove \(n:Integer, p : Bit) -> p ==> (x != x where x = (2 : Integer) ^^ n)
:sat \(a:[8], b:[8]) -> a == ~zero /\ a@b == False
:prove \(a:[8], b:[8]) -> a == zero ==> a@b == False
:set prover=w4-z3
:prove \(n:Integer, p : Bit) -> p ==> (x != x where x = 2 ^^ n)
:prove \(n:Integer, p : Bit) -> p ==> (x != x where x = (2 : Integer) ^^ n)
:sat \(a:[8], b:[8]) -> a == ~zero /\ a@b == False
:prove \(a:[8], b:[8]) -> a == zero ==> a@b == False