From 3718f4836a0a5d80b07f2e9f41cacbebbf7958fe Mon Sep 17 00:00:00 2001
From: qadeer <unknown>
Date: Sun, 6 Feb 2011 06:13:47 +0000
Subject: implemented /UseUnsatCoreForInlining option for use in stratified
 inlining

---
 Test/stratifiedinline/bar7.bpl | 43 ++++++++++++++++++++++++++++++++++++++++++
 Test/stratifiedinline/bar8.bpl | 42 +++++++++++++++++++++++++++++++++++++++++
 2 files changed, 85 insertions(+)
 create mode 100644 Test/stratifiedinline/bar7.bpl
 create mode 100644 Test/stratifiedinline/bar8.bpl

(limited to 'Test/stratifiedinline')

diff --git a/Test/stratifiedinline/bar7.bpl b/Test/stratifiedinline/bar7.bpl
new file mode 100644
index 00000000..747510de
--- /dev/null
+++ b/Test/stratifiedinline/bar7.bpl
@@ -0,0 +1,43 @@
+var i: int;
+var m: int;
+
+procedure {:inline 1} foo()
+modifies i;
+{
+  if (i < 80) {
+      i := i + 1;
+      call foo();
+  }
+}
+
+procedure {:inline 1} bar1(j: int) 
+modifies i;
+{
+  if (j < 2*m) 
+  {
+    i := i + 1;
+    call bar1(j+1);
+  }
+}
+
+procedure {:inline 1} bar2(j: int) 
+modifies i;
+{
+  if (j < m) {
+    i := i - 1;
+    call bar2(j+1);
+  }
+}
+
+procedure main() 
+modifies i;
+{
+  i := 0;
+  if (*) {
+    call foo();
+  } else {
+    call bar1(0);
+    call bar2(0);
+  }
+  assert i < 10;
+}
\ No newline at end of file
diff --git a/Test/stratifiedinline/bar8.bpl b/Test/stratifiedinline/bar8.bpl
new file mode 100644
index 00000000..d447e3a7
--- /dev/null
+++ b/Test/stratifiedinline/bar8.bpl
@@ -0,0 +1,42 @@
+var i: int;
+var m: int;
+
+procedure {:inline 1} foo() 
+modifies i;
+{
+  if (i < 80) {
+      i := i + 1;
+      call foo();
+  }
+}
+
+procedure {:inline 1} bar1(j: int) 
+modifies i;
+{
+  if (j < 2*m) {
+    i := i + 1;
+    call bar1(j+1);
+  }
+}
+
+procedure {:inline 1} bar2(j: int) 
+modifies i;
+{
+  if (j < m) {
+    i := i - 2;
+    call bar2(j+1);
+  }
+}
+
+procedure main()
+modifies i;
+{
+  i := 0;
+  if (*) {
+    call foo();
+  } else {
+    call bar1(0);
+    call bar2(0);
+  }
+  assert i < 10;
+}
\ No newline at end of file
-- 
cgit v1.2.3