]> matita.cs.unibo.it Git - fireball-separation.git/commitdiff
Failing case found
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 18 Jul 2017 13:38:27 +0000 (15:38 +0200)
committeracondolu <andrea.condoluci@unibo.it>
Mon, 28 May 2018 09:10:57 +0000 (11:10 +0200)
(cherry picked from commit 42eb14bc4443ce5a9bb893654db97a9c41486f06)

ocaml/problems/bugs [new file with mode: 0644]

diff --git a/ocaml/problems/bugs b/ocaml/problems/bugs
new file mode 100644 (file)
index 0000000..2cea8d3
--- /dev/null
@@ -0,0 +1,12 @@
+$! randomly generated test
+D ((((z b) (w v)) (v. (v z))) (a. (v y)))
+C (((((((b b) (a. (y v))) (a. (b. (b b)))) (w. (x. (a (y v))))) (((w v) z) (v. (((y v) v) ((z b) (w v)))))) ((((y v) v) (z. (y. (w. (b b))))) (y. (w. (b b))))) ((y (y. (c v))) w))
+C ((((((b b) (a. (y v))) (a. (b. (b b)))) ((((w v) z) (v. (((y v) v) ((z b) (w v))))) (y (y. (c v))))) (b. a)) (((z b) (w v)) y))
+C ((((((b b) (a. (y v))) (a. (b. (b b)))) (w. (x. (a (y v))))) (((w v) z) (v. (((y v) v) ((z b) (w v)))))) ((((y v) v) (z. (y. (w. (b b))))) (y. (w. (b b)))))
+C ((((((y v) v) ((z b) (w v))) c) c) (((((z b) (w v)) (v. (v z))) (a. (v x))) v))
+C (((((b b) (a. (y v))) (a. (b. (b b)))) ((((w v) z) (v. (((y v) v) ((z b) (w v))))) (y (y. (c v))))) (b. a))
+N ((((((b b) (a. (y v))) (a. (b. (b b)))) ((((w v) z) (v. (((y v) v) ((z b) (w v))))) (y (y. (c v))))) (b. a)) (((c (w v)) ((w v) z)) (c w))) Z
+N ((((((b b) (a. (y v))) (a. (b. (b b)))) ((((w v) z) (v. (((y v) v) ((z b) (w v))))) (y (y. (c v))))) (b. a)) (c. (((c v) ((c w) (b. a))) (v. (c. (w. b)))))) Z
+N ((((((w v) z) (v. (((y v) v) ((z b) (w v))))) (y (y. (c v)))) (y. (c. ((((y v) v) (z. (y. (w. (b b))))) (((z b) (w v)) (v. (v z))))))) (z. (y. (b. a)))) Z
+N (((((b b) (a. (y v))) (a. (b. (b b)))) ((((w v) z) (v. (((y v) v) ((z b) (w v))))) (y (y. (c v))))) (((y v) v) ((z b) (w v)))) Z
+N (((((b b) (a. (y v))) (a. (b. (b b)))) (((w v) z) (y. (c v)))) (y. (c. c))) Z