more refactoring in stratified inlining

1 files changed, 5 insertions, 5 deletions

diff --git a/Test/stratifiedinline/bar7.bpl b/Test/stratifiedinline/bar7.bpl
index b28777bd..41cf612e 100644
--- a/Test/stratifiedinline/bar7.bpl
+++ b/Test/stratifiedinline/bar7.bpl
@@ -1,7 +1,7 @@
 var i: int;

 var m: int;

 

-procedure {:inline 1} foo()

+procedure foo()

 modifies i;

 {

   if (i < 20) {

@@ -10,7 +10,7 @@ modifies i;
   }

 }

 

-procedure {:inline 1} bar1(j: int) 

+procedure bar1(j: int) 

 modifies i;

 {

   if (j < 2*m) 

@@ -20,7 +20,7 @@ modifies i;
   }

 }

 

-procedure {:inline 1} bar2(j: int) 

+procedure bar2(j: int) 

 modifies i;

 {

   if (j < m) {

@@ -29,7 +29,7 @@ modifies i;
   }

 }

 

-procedure main() 

+procedure {:entrypoint} main() 

 modifies i;

 {

   i := 0;

@@ -39,5 +39,5 @@ modifies i;
     call bar1(0);

     call bar2(0);

   }

-  assert i < 10;

+  assume !(i < 10);

 }
\ No newline at end of file