From cfd809c669908fd5c00344901e4d146308860f49 Mon Sep 17 00:00:00 2001
From: akashlal <unknown>
Date: Mon, 21 Oct 2013 19:52:19 +0530
Subject: And a test case

---
 Test/stratifiedinline/Answer      | 7 +++++++
 Test/stratifiedinline/bar12.bpl   | 8 ++++++++
 Test/stratifiedinline/runtest.bat | 3 +++
 3 files changed, 18 insertions(+)
 create mode 100644 Test/stratifiedinline/bar12.bpl

(limited to 'Test/stratifiedinline')

diff --git a/Test/stratifiedinline/Answer b/Test/stratifiedinline/Answer
index dd5344e8..d2600aad 100644
--- a/Test/stratifiedinline/Answer
+++ b/Test/stratifiedinline/Answer
@@ -502,3 +502,10 @@ Execution trace:
 
 Boogie program verifier finished with 0 verified, 1 error
 -----
+----- Running regression test bar12.bpl
+(0,0): Error BP5001: This assertion might not hold.
+Execution trace:
+    bar12.bpl(6,4): anon0
+
+Boogie program verifier finished with 0 verified, 1 error
+-----
diff --git a/Test/stratifiedinline/bar12.bpl b/Test/stratifiedinline/bar12.bpl
new file mode 100644
index 00000000..863f9dc0
--- /dev/null
+++ b/Test/stratifiedinline/bar12.bpl
@@ -0,0 +1,8 @@
+function {:inline} f(a:bool) : bool { true }
+
+procedure {:entrypoint} main()
+{
+  var x: int;
+   assume f(x >= 0);
+  assume x >= 0;
+}
diff --git a/Test/stratifiedinline/runtest.bat b/Test/stratifiedinline/runtest.bat
index 07261c4d..d4b9c811 100644
--- a/Test/stratifiedinline/runtest.bat
+++ b/Test/stratifiedinline/runtest.bat
@@ -34,4 +34,7 @@ echo -----
 echo ----- Running regression test bar11.bpl
 %BGEXE% %* /stratifiedInline:1 /vc:i bar11.bpl
 echo -----
+echo ----- Running regression test bar12.bpl
+%BGEXE% %* /stratifiedInline:1 /vc:i bar12.bpl
+echo -----
 
-- 
cgit v1.2.3