3 files changed, 56 insertions, 0 deletions
diff --git a/Test/stratifiedinline/Answer b/Test/stratifiedinline/Answer
index 6e23c098..77b00b19 100644
--- a/Test/stratifiedinline/Answer
+++ b/Test/stratifiedinline/Answer
@@ -484,3 +484,24 @@ Execution trace:
 
 Boogie program verifier finished with 0 verified, 1 error
 -----
+----- Running regression test bar11.bpl
+bar11.bpl(31,1): Error BP5003: A postcondition might not hold on this return path.
+bar11.bpl(26,1): Related location: This is the postcondition that might not hold.
+Execution trace:
+    bar11.bpl(30,3): anon0
+    Inlined call to procedure foo begins
+        bar11.bpl(15,3): anon0
+        value = 0
+        Inlined call to procedure bar begins
+            bar11.bpl(8,5): anon0
+            value = 1
+        Inlined call to procedure bar ends
+        Inlined call to procedure bar begins
+            bar11.bpl(8,5): anon0
+            value = 2
+        Inlined call to procedure bar ends
+        value = 2
+    Inlined call to procedure foo ends
+
+Boogie program verifier finished with 0 verified, 1 error
+-----
diff --git a/Test/stratifiedinline/bar11.bpl b/Test/stratifiedinline/bar11.bpl
new file mode 100644
index 00000000..baad27a1
--- /dev/null
+++ b/Test/stratifiedinline/bar11.bpl
@@ -0,0 +1,32 @@
+var x: int;
+var y: int;
+procedure boogie_si_record_int(x:int);
+
+procedure {:inline 1} bar()
+modifies y;
+{
+  y := y + 1;
+  call boogie_si_record_int(y);
+}
+
+procedure {:inline 1} foo() 
+modifies x, y;
+{
+  call boogie_si_record_int(x);
+  x := x + 1;
+  call bar();
+  call bar();
+  x := x + 1;
+  call boogie_si_record_int(x);
+}
+
+procedure main()
+requires x == 0;
+requires x == y;
+ensures x != y;
+modifies x, y;
+{
+
+  call foo();
+}
+
diff --git a/Test/stratifiedinline/runtest.bat b/Test/stratifiedinline/runtest.bat
index d731d605..3ba74096 100644
--- a/Test/stratifiedinline/runtest.bat
+++ b/Test/stratifiedinline/runtest.bat
@@ -31,4 +31,7 @@ echo -----
 echo ----- Running regression test bar10.bpl
 %BGEXE% %* /noinfer /stratifiedInline:1 /nonUniformUnfolding bar10.bpl
 echo -----
+echo ----- Running regression test bar11.bpl
+%BGEXE% %* /noinfer /stratifiedInline:1 bar11.bpl
+echo -----