added an optimization to extract loops so that only loop targets are treated as output variables of the extracted procedure.

2 files changed, 17 insertions, 2 deletions

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;

+}