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/z3api/boog17.bpl | 25 +++++++++++++++++++++++++
 1 file changed, 25 insertions(+)
 create mode 100644 Test/z3api/boog17.bpl

(limited to 'Test/z3api/boog17.bpl')

diff --git a/Test/z3api/boog17.bpl b/Test/z3api/boog17.bpl
new file mode 100644
index 00000000..6f886f49
--- /dev/null
+++ b/Test/z3api/boog17.bpl
@@ -0,0 +1,25 @@
+const unique g : int;
+axiom(g != 0);
+
+const unique PINT4_name:name;
+
+function PLUS(a:int, a_size:int, b:int) returns (int);
+axiom(forall a:int, a_size:int, b:int :: {PLUS(a,a_size,b)} PLUS(a,a_size,b) == a + a_size * b);
+
+function HasType(v:int, t:name) returns (bool);
+
+
+procedure  main ( ) returns ($result.main$11.5$1$:int) {
+  var p : int;
+
+start:
+  assume(HasType(p, PINT4_name));
+  goto label_3;
+
+label_3:
+  goto label_4;
+
+label_4:
+  p := PLUS(g, 4, 55) ;
+  assert(HasType(p, PINT4_name));
+}
\ No newline at end of file
-- 
cgit v1.2.3