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

Add a test case for issue725

Browse Source
This commit is contained in:
Rob Dockins 2020-05-22 14:44:02 -07:00 committed by robdockins
parent 06584f4d10
commit c1b641c420
2 changed files with 23 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

14
tests/issues/issue725.icry Normal file
View File

@ -0,0 +1,14 @@
:set show-examples = no
:set prover-stats=no
:set prover=z3
:prove \(n:Integer, p : Bit) -> p ==> (x != x where x = 2 ^^ 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)
:sat \(a:[8], b:[8]) -> a == ~zero /\ a@b == False
:prove \(a:[8], b:[8]) -> a == zero ==> a@b == False

9
tests/issues/issue725.icry.stdout Normal file
View File

@ -0,0 +1,9 @@
Loading module Cryptol
operation can not be supported on symbolic values: integer exponentiation
Unsatisfiable
Counterexample
operation can not be supported on symbolic values: integer exponentiation
Unsatisfiable
Counterexample