Add regression test for issues #1093 and #1094.

GaloisInc · Mar 2, 2021 · 5ff4f5b · 5ff4f5b
1 parent 4735117
commit 5ff4f5b
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 0 deletions.
diff --git a/tests/issues/issue1093.icry b/tests/issues/issue1093.icry
@@ -0,0 +1,4 @@
+:set prover=z3
+:prove \(xs:[12][0]) -> reverse (reverse xs) == xs
+:prove \(xs:[0]) (ys:[0]) -> xs == ys
+:prove \(xs:[0]) (ys:[0]) (zs:[0]) -> (xs # ys) # zs == xs # (ys # zs)
diff --git a/tests/issues/issue1093.icry.stdout b/tests/issues/issue1093.icry.stdout
@@ -0,0 +1,4 @@
+Loading module Cryptol
+Q.E.D.
+Q.E.D.
+Q.E.D.