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/test15/ModelTest.bpl | 10 ++++++++++
 1 file changed, 10 insertions(+)
 create mode 100644 Test/test15/ModelTest.bpl

(limited to 'Test/test15/ModelTest.bpl')

diff --git a/Test/test15/ModelTest.bpl b/Test/test15/ModelTest.bpl
new file mode 100644
index 00000000..6f03d0bd
--- /dev/null
+++ b/Test/test15/ModelTest.bpl
@@ -0,0 +1,10 @@
+procedure M (s : ref, r : ref) {
+  var  i : int, j : int;
+  i := 0 + 1;
+  j := i + 1;
+  j := j + 1;
+  j := j + 1;
+  assert i == j;
+  assert s == r;
+}
+type ref;
-- 
cgit v1.2.3