From 30181ba4213413c32459d0f0de2ec77ed939c2dd Mon Sep 17 00:00:00 2001
From: qadeer <unknown>
Date: Fri, 10 Sep 2010 07:42:17 +0000
Subject: added an optimization to extract loops so that only loop targets are
 treated as output variables of the extracted procedure.

---
 Test/lazyinline/Answer  |  2 +-
 Test/lazyinline/foo.bpl | 17 ++++++++++++++++-
 2 files changed, 17 insertions(+), 2 deletions(-)

(limited to 'Test')

diff --git a/Test/lazyinline/Answer b/Test/lazyinline/Answer
index 423695a5..ecb258a2 100644
--- a/Test/lazyinline/Answer
+++ b/Test/lazyinline/Answer
@@ -64,5 +64,5 @@ Boogie program verifier finished with 1 verified, 0 errors
 -----
 ----- Running regression test foo.bpl
 
-Boogie program verifier finished with 1 verified, 0 errors
+Boogie program verifier finished with 2 verified, 0 errors
 -----
diff --git a/Test/lazyinline/foo.bpl b/Test/lazyinline/foo.bpl
index 80b7b7b2..bd45258a 100644
--- a/Test/lazyinline/foo.bpl
+++ b/Test/lazyinline/foo.bpl
@@ -12,4 +12,19 @@ ensures g == 2;
     x := x - 1;
   }
   assert x == 2;
-}
\ No newline at end of file
+}
+
+procedure B(j: int) returns (x: int)
+{
+  var i: int;
+  var y: int;
+
+  y := 0;
+  i := 0;
+  x := j;
+  while (i < 100) {
+     x := x + 1 + y;
+     i := i + 1;
+  }
+  assert y == 0;
+}
-- 
cgit v1.2.3