From ce1c2de044c91624370411e23acab13b0381949b Mon Sep 17 00:00:00 2001
From: mikebarnett <unknown>
Date: Wed, 15 Jul 2009 21:03:41 +0000
Subject: Initial set of files.

---
 Test/test2/Axioms.bpl | 29 +++++++++++++++++++++++++++++
 1 file changed, 29 insertions(+)
 create mode 100644 Test/test2/Axioms.bpl

(limited to 'Test/test2/Axioms.bpl')

diff --git a/Test/test2/Axioms.bpl b/Test/test2/Axioms.bpl
new file mode 100644
index 00000000..4fe7a8a7
--- /dev/null
+++ b/Test/test2/Axioms.bpl
@@ -0,0 +1,29 @@
+const Seven: int;
+axiom Seven == 7;
+
+function inc(int) returns (int);
+axiom (forall j: int :: inc(j) == j+1);
+
+procedure P()
+{
+  start:
+    assert 4 <= Seven;
+    assert Seven < inc(Seven);
+    assert inc(5) + inc(inc(2)) == Seven + 3;
+    return;
+}
+
+procedure Q()
+{
+  start:
+    assert inc(5) + inc(inc(2)) == Seven;  // error
+    return;
+}
+
+function inc2(x:int) returns(int) { x + 2 }
+
+procedure ExpandTest()
+{
+  var q:int;
+  assert inc(inc(q)) == inc2(q);
+}
-- 
cgit v1.2.3