Simpler tests in simple_test.ml + Added diverging tests in simple.1

[fireball-separation.git] / ocaml / problems / simple.1

diff --git a/ocaml/problems/simple.1 b/ocaml/problems/simple.1
new file mode 100644 (file)
index 0000000..d3e9213
--- /dev/null
+++ b/ocaml/problems/simple.1
@@ -0,0 +1,11 @@
+$! simple: C diverges\r
+D v0 (x. x) (v1 (x. y. y v2)) (x. y. v1 v3)\r
+C v4 (v1 v5 v2 v1 (x. v1 x v2) (v0 (v1 v3) (v1 v5 v2) (v6 v2 (x. y. v0 (v1 v3)) (v3 v2 (x. v1 v3))))) (v1 (x. y. y v2) (v5 v5) (x. v5) (v0 (v1 v3) (v1 v5 v2)) (x. y. v0 (v1 v3))) (v6 v2 (x. y. v0 (v1 v3)) (v3 v2 (x. v1 v3)) (v7 (v0 (v1 v3) (v1 v5 v2))) (v1 v3)) (v1 (x. y. y v2) (v5 v5) (x. v5) (x. v8) (x. x v2) (x. v1 v5 v2)) (v1 (x. y. y v2) (v5 v5) (x. v5) (x. v8) (x. x v2) (x. v5) (x. y. z. v8))\r
+\r
+$! simple: C diverges in pure (1)\r
+D v0 v1 (x. y. z. v2 (y (v3 v4))) (v5 (x. v6))\r
+C v7 (v0 v1 (v5 v8 (x. y. v6)) (x. v2) (x. x (y. v1)) (x. v5 v8 v0) (x. v8 (v3 v4))) (v0 v1 (v5 v8 (x. y. v6)) (x. v2) (x. x (y. v1)) (v5 v8 v0) (x. x (y. v2 (v8 (y v4))) (x (y. v2 (v8 (y v4)))))) (v8 (v3 v4) (v5 v8 (x. y. v6) (v8 (v3 v4)) (v5 v8 (x. y. v6) (v8 (v3 v4))) (v5 (x. v6 (v6 (y. v2 (x (y v4))))))) (v5 v8 (x. y. v6) (v8 (v3 v4)) (v5 v8 (x. y. v6) (v8 (v3 v4))) (v5 (x. v6 (v6 (y. v2 (x (y v4)))))) (v8 (v3 v4) (v5 v8 (x. y. v6) (v8 (v3 v4)) (v5 v8 (x. y. v6) (v8 (v3 v4))) (v5 (x. v6 (v6 (y. v2 (x (y v4))))))))) (v0 v1 (v5 v8 (x. y. v6)) (x. v2) (x. x (y. v1)) (v5 v8 v0)) (v0 v1 (v5 v8 (x. y. v6)) (v8 (v3 v4)) (v5 v8)) (x. v6 (y. v2 (v8 (y v4))) (v8 (v3 v4)) (x (v0 x (v5 v8 (y. z. v6)) (v8 (v3 v4)))))) (v0 v1 (v5 v8 (x. y. v6)) (x. v2) (x. x (y. v1)) (x. v5 v8 v0) (x. v8 (v3 v4)) v4) (v0 v1 (v5 v8 (x. y. v6)) (x. v2) (x. x (y. v1)) (x. v5 v8 v0) (x. v8 (v3 v4)) (x. y. v6))\r
+\r
+$! simple: C diverges in pure (2)\r
+D v0 (v0 v1 (v0 v2) (v3 v4) v0 (v0 v1 (v0 v2) (v3 v4)) (x. v0 v2 (v0 v1 (v0 v2))) (v5 (v0 v1 (v0 v2) (v3 v4) v0 v1))) (x. v0 v1 v6 (v7 (v2 v5) (v0 v2)) (y. x v4 (v0 v1)))\r
+C v8 (v0 v1 (v0 v2) (v3 v4) v0 (v0 v1 (v0 v2) (v3 v4)) (x. v0 v2 (v0 v1 (v0 v2))) (v5 (v0 v1 (v0 v2) (v3 v4) v0 v1))) (v0 v1 (v0 v2) (v3 v4) v0 (v0 v1 (v0 v2) (v3 v4)) (x. v0 v2 (v0 v1 (v0 v2))) (v2 v5 (x. v0 v1 (v0 x) (v3 v4) v0 v1 v4))) (v0 v1 (v0 v2) (v3 v4) v0 (v3 v4) (x. y. v0) (v0 v1 (v0 v2) (v3 v4)) (v2 v5 (v0 v1 (v0 v2) (v3 v4) v0 v1 (v3 v4 (v0 v1)) (v2 (v0 v2 (v0 v1 (v0 v2)) v2))))) (v0 v1 (v0 v2) (v3 v4) v0 (v0 v1 (v0 v2) (v3 v4)) (x. v0 v2 (v0 v1 (v0 v2))) (v5 (v0 v1 (v0 v2) (v3 v4) v0 v1)) (x. y. z. v0 v1 (v0 v2) (v3 z))) (v0 v1 (v0 v2) (v3 v4) v0 (v0 v1 (v0 v2) (v3 v4)) (x. v0 v2 (v0 v1 (v0 v2))) (v5 (v0 v1 (v0 v2) (v3 v4) v0 v1)) (x. y. z. v0 v1 (v0 v2) (v3 z)) (v0 v1 (v0 v2) (v3 v4) v0 v1 (v3 v4 (v0 v1)) (v2 (v0 v2 (v0 v1 (v0 v2)) v2))))\r