Initial set of files.

1 files changed, 16 insertions, 0 deletions

diff --git a/Test/test2/Implies.bpl b/Test/test2/Implies.bpl
new file mode 100644
index 00000000..3034f973
--- /dev/null
+++ b/Test/test2/Implies.bpl
@@ -0,0 +1,16 @@
+

+const a:bool;

+const b:bool;

+const c:bool;

+const d:bool;

+

+function f(int) returns (bool);

+axiom (forall x:int :: f(x) <== x >= 0);

+

+procedure P() {

+  assert (a ==> (b ==> c) ==> d) == (d <== (c <== b) <== a);

+  assert (a ==> b ==> c) == (c <== (a ==> b));     // error

+

+  assert f(23);

+  assert f(-5);                                    // error

+}
\ No newline at end of file