diff --git a/tests/issues/issue664.icry b/tests/issues/issue664.icry
new file mode 100644
index 000000000..4e28f411f
--- /dev/null
+++ 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
new file mode 100644
index 000000000..1d827d329
--- /dev/null
+++ 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.