From f1f3d32ba043c0468dd04dfcfa7ac02c3fa1876c Mon Sep 17 00:00:00 2001
From: qadeer <unknown>
Date: Thu, 15 Aug 2013 12:38:35 -0700
Subject: inlining is now done in rhs of assignments for codeexprs added more
 regressions

---
 Test/inline/Answer       |  6 +++---
 Test/inline/codeexpr.bpl | 26 +++++++++++++++++++++++++-
 2 files changed, 28 insertions(+), 4 deletions(-)

(limited to 'Test/inline')

diff --git a/Test/inline/Answer b/Test/inline/Answer
index d1666e03..f08209e3 100644
--- a/Test/inline/Answer
+++ b/Test/inline/Answer
@@ -6,11 +6,11 @@ Execution trace:
 
 Boogie program verifier finished with 1 verified, 1 error
 -------------------- codeexpr.bpl --------------------
-codeexpr.bpl(35,5): Error BP5001: This assertion might not hold.
+codeexpr.bpl(40,5): Error BP5001: This assertion might not hold.
 Execution trace:
-    codeexpr.bpl(34,7): anon0
+    codeexpr.bpl(39,7): anon0
 
-Boogie program verifier finished with 3 verified, 1 error
+Boogie program verifier finished with 5 verified, 1 error
 -------------------- test1.bpl --------------------
 
 procedure Main();
diff --git a/Test/inline/codeexpr.bpl b/Test/inline/codeexpr.bpl
index bd57329f..67728ea5 100644
--- a/Test/inline/codeexpr.bpl
+++ b/Test/inline/codeexpr.bpl
@@ -5,6 +5,11 @@ procedure {:inline 1} bar() returns (l: bool)
   l := g;
 }
 
+procedure {:inline 1} baz() returns (l: bool)
+{
+  call l := bar();
+}
+
 procedure A1() 
 modifies g;
 {
@@ -33,4 +38,23 @@ modifies g;
 {
     g := true;
     assert |{ var l: bool; A: call l := bar(); return !l; }|;
-}
\ No newline at end of file
+}
+
+procedure A5() 
+modifies g;
+{
+    var m: bool;
+
+    g := true;
+    m := |{ var l: bool; A: call l := bar(); return l; }|;
+    assert m;
+}
+
+procedure A6() 
+modifies g;
+{
+    g := true;
+    assert |{ var l: bool; A: call l := baz(); return l; }|;
+    assert (exists p: bool :: |{ var l: bool; A: call l := baz(); return l; }|);
+    assert (forall p: bool :: |{ var l: bool; A: call l := baz(); return l; }|);
+}
-- 
cgit v1.2.3