Test case for issue #639

GaloisInc · Dec 10, 2020 · 5d75123 · 5d75123
1 parent 7376dfb
commit 5d75123
Show file tree

Hide file tree

Showing 4 changed files with 21 additions and 0 deletions.
diff --git a/tests/issues/Issue639_C.cry b/tests/issues/Issue639_C.cry
@@ -0,0 +1,2 @@
+module Issue639_C where
+  import Issue639_M (f)
diff --git a/tests/issues/Issue639_M.cry b/tests/issues/Issue639_M.cry
@@ -0,0 +1,3 @@
+module Issue639_M where
+  f (a:Bit) = True
+  property p a = f a == a
diff --git a/tests/issues/issue639.icry b/tests/issues/issue639.icry
@@ -0,0 +1,4 @@
+:m Issue639_C
+:check
+:prove
+:sat
diff --git a/tests/issues/issue639.icry.stdout b/tests/issues/issue639.icry.stdout
@@ -0,0 +1,12 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module Issue639_M
+Loading module Issue639_C
+property Issue639_M::p Using exhaustive testing.
+Testing... Issue639_M::p False = False
+:prove Issue639_M::p
+	Counterexample
+Issue639_M::p False = False
+:sat Issue639_M::p
+	Satisfiable
+Issue639_M::p True = True