2 files changed, 85 insertions, 0 deletions
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