Add regression test for #664.

GaloisInc · Nov 27, 2019 · 67fc367 · 67fc367
1 parent 56f2638
commit 67fc367
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 0 deletions.
diff --git a/tests/issues/issue664.icry b/tests/issues/issue664.icry
@@ -0,0 +1,3 @@
+let ashr x y = if head x then ~ (~ x >> y) else x >> y
+:exhaust \(x : [8]) (y : [8]) -> x >>$ y == ashr x y
+:prove \(x : [8]) (y : [8]) -> x >>$ y == ashr x y
diff --git a/tests/issues/issue664.icry.stdout b/tests/issues/issue664.icry.stdout
@@ -0,0 +1,5 @@
+Loading module Cryptol
+Using exhaustive testing.
+Testing... Passed 65536 tests.
+Q.E.D.
+Q.E.D.