cleaned up the OG code

enabled it to be always on

26 files changed, 117 insertions, 101 deletions

diff --git a/Test/linear/typecheck.bpl b/Test/linear/typecheck.bpl
index ebd3d07d..973a1c88 100644
--- a/Test/linear/typecheck.bpl
+++ b/Test/linear/typecheck.bpl
@@ -20,7 +20,7 @@ procedure C()
 

 function f(X): X;

 

-procedure D()

+procedure {:yields} D()

 {

     var {:linear "D"} a: X;

     var {:linear "D"} x: X;

@@ -66,7 +66,7 @@ procedure E({:linear "D"} a: X, {:linear "D"} b: X) returns ({:linear "D"} c: X,
     c := a;

 }

 

-procedure F({:linear "D"} a: X) returns ({:linear "D"} c: X);

+procedure {:yields} {:stable} F({:linear "D"} a: X) returns ({:linear "D"} c: X);

 

 var{:linear "x"} g:int;

 

@@ -81,22 +81,22 @@ modifies g;
   g := r;

 }

 

-procedure I({:linear ""} x:int) returns({:linear ""} x':int)

+procedure {:yields} {:stable} I({:linear ""} x:int) returns({:linear ""} x':int)

 {

   x' := x;

 }

 

-procedure J()

+procedure {:yields} {:stable} J()

 {

 }

 

-procedure P1({:linear ""} x:int) returns({:linear ""} x':int)

+procedure {:yields} P1({:linear ""} x:int) returns({:linear ""} x':int)

 {

   call x' := I(x) | J();

   call x' := I(x');

 }

 

-procedure P2({:linear ""} x:int) returns({:linear ""} x':int)

+procedure {:yields} P2({:linear ""} x:int) returns({:linear ""} x':int)

 {

   call x' := I(x);

   call x' := I(x') | J();

diff --git a/Test/og/Answer b/Test/og/Answer
index d663de9a..1d516066 100644
--- a/Test/og/Answer
+++ b/Test/og/Answer
@@ -1,36 +1,36 @@
 

 -------------------- foo.bpl --------------------

-foo.bpl(13,3): Error BP5001: This assertion might not hold.

+foo.bpl(14,3): Error BP5001: This assertion might not hold.

 Execution trace:

-    foo.bpl(5,5): anon0

+    foo.bpl(6,5): anon0

     (0,0): inline$Impl_YieldChecker_PC$0$L0

 

-Boogie program verifier finished with 3 verified, 1 error

+Boogie program verifier finished with 4 verified, 1 error

 

 -------------------- bar.bpl --------------------

-bar.bpl(12,3): Error BP5001: This assertion might not hold.

+bar.bpl(13,3): Error BP5001: This assertion might not hold.

 Execution trace:

-    bar.bpl(5,5): anon0

+    bar.bpl(6,5): anon0

     (0,0): inline$Impl_YieldChecker_PC$0$L0

-bar.bpl(12,3): Error BP5001: This assertion might not hold.

+bar.bpl(13,3): Error BP5001: This assertion might not hold.

 Execution trace:

-    bar.bpl(17,5): anon0

+    bar.bpl(23,5): anon0

     (0,0): inline$Impl_YieldChecker_PC$0$L0

 

-Boogie program verifier finished with 2 verified, 2 errors

+Boogie program verifier finished with 3 verified, 2 errors

 

 -------------------- one.bpl --------------------

 

 Boogie program verifier finished with 2 verified, 0 errors

 

 -------------------- parallel1.bpl --------------------

-parallel1.bpl(9,3): Error BP5001: This assertion might not hold.

+parallel1.bpl(10,1): Error BP5001: This assertion might not hold.

 Execution trace:

-    parallel1.bpl(5,5): anon0

+    parallel1.bpl(6,5): anon0

     (0,0): inline$Proc_YieldChecker_PC$0$L0

-parallel1.bpl(13,3): Error BP5001: This assertion might not hold.

+parallel1.bpl(14,3): Error BP5001: This assertion might not hold.

 Execution trace:

-    parallel1.bpl(5,5): anon0

+    parallel1.bpl(6,5): anon0

     (0,0): inline$Impl_YieldChecker_PC$0$L0

 

 Boogie program verifier finished with 3 verified, 2 errors

@@ -100,10 +100,10 @@ Boogie program verifier finished with 2 verified, 0 errors
 Boogie program verifier finished with 2 verified, 0 errors

 

 -------------------- async.bpl --------------------

-async.bpl(13,1): Error BP5001: This assertion might not hold.

+async.bpl(14,1): Error BP5001: This assertion might not hold.

 Execution trace:

-    async.bpl(6,3): anon0

-    async.bpl(6,3): anon0$1

+    async.bpl(7,3): anon0

+    async.bpl(7,3): anon0$1

     (0,0): inline$Proc_YieldChecker_P$1$L0

 

 Boogie program verifier finished with 1 verified, 1 error

diff --git a/Test/og/DeviceCacheSimplified.bpl b/Test/og/DeviceCacheSimplified.bpl
index d231e17c..32fb25b7 100644
--- a/Test/og/DeviceCacheSimplified.bpl
+++ b/Test/og/DeviceCacheSimplified.bpl
@@ -5,7 +5,7 @@ function {:inline} Inv(ghostLock: X, currsize: int, newsize: int) : (bool)
     currsize <= newsize && (ghostLock == nil <==> currsize == newsize)

 }

 

-procedure YieldToReadCache({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X)

+procedure {:yields} YieldToReadCache({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X)

 requires tid' != nil;

 requires Inv(ghostLock, currsize, newsize);

 ensures Inv(ghostLock, currsize, newsize);

@@ -19,7 +19,7 @@ ensures tid == tid';
     assert tid != nil;

 }

 

-procedure YieldToUpdateCache({:linear "tid"} tid': X, i: int) returns ({:linear "tid"} tid: X)

+procedure {:yields} YieldToUpdateCache({:linear "tid"} tid': X, i: int) returns ({:linear "tid"} tid: X)

 requires tid' != nil;

 requires Inv(ghostLock, currsize, newsize);

 requires ghostLock == tid';

@@ -56,7 +56,7 @@ modifies lock;
 requires lock == tid;

 ensures lock == nil;

 

-procedure Read ({:linear "tid"} tid': X, start : int, size : int) returns (bytesread : int)

+procedure {:yields} Read ({:linear "tid"} tid': X, start : int, size : int) returns (bytesread : int)

 requires tid' != nil;

 requires 0 <= start && 0 <= size;

 requires Inv(ghostLock, currsize, newsize);

@@ -120,7 +120,7 @@ COPY_TO_BUFFER:
     }

 }

 

-procedure thread({:linear "tid"} tid': X)

+procedure {:yields} {:stable} thread({:linear "tid"} tid': X)

 requires tid' != nil;

 requires Inv(ghostLock, currsize, newsize);

 {

@@ -133,7 +133,7 @@ requires Inv(ghostLock, currsize, newsize);
     call bytesread := Read(tid, start, size);

 }

 

-procedure {:entrypoint} main()

+procedure {:entrypoint} {:yields} main()

 requires currsize == 0 && newsize == 0 && ghostLock == nil && lock == nil;

 {

     var {:linear "tid"} tid: X;

diff --git a/Test/og/FlanaganQadeer.bpl b/Test/og/FlanaganQadeer.bpl
index 434d1f14..5985b6d6 100644
--- a/Test/og/FlanaganQadeer.bpl
+++ b/Test/og/FlanaganQadeer.bpl
@@ -7,7 +7,7 @@ var x: int;
 procedure Allocate() returns ({:linear "tid"} xls: X);

 ensures xls != nil;

 

-procedure {:entrypoint} main()

+procedure {:entrypoint} {:yields} main()

 {

     var {:linear "tid"} tid: X;

     var val: int;

@@ -20,7 +20,7 @@ procedure {:entrypoint} main()
     }

 }

 

-procedure foo({:linear "tid"} tid': X, val: int)

+procedure {:yields} {:stable} foo({:linear "tid"} tid': X, val: int)

 requires tid' != nil;

 {

     var {:linear "tid"} tid: X;

@@ -36,7 +36,7 @@ requires tid' != nil;
     l := nil;

 }

 

-procedure Yield({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X)

+procedure {:yields} Yield({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X)

 requires tid' != nil;

 ensures tid == tid';

 ensures old(l) == tid ==> old(l) == l && old(x) == x;

diff --git a/Test/og/akash.bpl b/Test/og/akash.bpl
index f8c32022..eaa820b9 100644
--- a/Test/og/akash.bpl
+++ b/Test/og/akash.bpl
@@ -12,7 +12,7 @@ ensures xls == mapconstbool(true);
 var g: int;

 var h: int;

 

-procedure A({:linear "tid"} tid_in: int) returns ({:linear "tid"} tid_out: int) 

+procedure {:yields} A({:linear "tid"} tid_in: int) returns ({:linear "tid"} tid_out: int) 

 {

     var {:linear "1"} x: [int]bool;

     var {:linear "2"} y: [int]bool;

@@ -40,7 +40,7 @@ procedure A({:linear "tid"} tid_in: int) returns ({:linear "tid"} tid_out: int)
     async call C(tid_child, y);

 }

 

-procedure B({:linear "tid"} tid_in: int, {:linear "1"} x_in: [int]bool) 

+procedure {:yields} {:stable} B({:linear "tid"} tid_in: int, {:linear "1"} x_in: [int]bool) 

 requires x_in != mapconstbool(false);

 {

     var {:linear "tid"} tid_out: int;

@@ -55,7 +55,7 @@ requires x_in != mapconstbool(false);
     g := 2;

 }

 

-procedure C({:linear "tid"} tid_in: int, {:linear "2"} y_in: [int]bool) 

+procedure {:yields} {:stable} C({:linear "tid"} tid_in: int, {:linear "2"} y_in: [int]bool) 

 requires y_in != mapconstbool(false);

 {

     var {:linear "tid"} tid_out: int;

diff --git a/Test/og/async.bpl b/Test/og/async.bpl
index 15f89bae..32f609bc 100644
--- a/Test/og/async.bpl
+++ b/Test/og/async.bpl
@@ -1,7 +1,8 @@
 var x: int;

 var y: int;

 

-procedure {:entrypoint} foo() 

+procedure {:entrypoint} {:yields} foo()

+modifies x, y; 

 {

   assume x == y;

   x := x + 1;

@@ -9,7 +10,7 @@ procedure {:entrypoint} foo()
   y := y + 1;

 }

 

-procedure P()

+procedure {:yields} {:stable} P()

 requires x != y;

 {

   assert x != y;

diff --git a/Test/og/bar.bpl b/Test/og/bar.bpl
index 8c4586d3..920fc32c 100644
--- a/Test/og/bar.bpl
+++ b/Test/og/bar.bpl
@@ -1,30 +1,36 @@
 var g:int;

 

-procedure PB()

+procedure {:yields} {:stable} PB()

+modifies g;

 {

   g := g + 1;

 }

 

-procedure PC()

-  ensures g == old(g);

+procedure {:yields} PC()

+ensures g == old(g);

 {

   yield;

   assert g == old(g);

 }

 

-procedure PD()

+procedure {:yields} {:stable} PE()

+{

+  call PC();

+}

+

+procedure {:yields} {:stable} PD()

 {

   g := 3;

   call PC();

   assert g == 3;

 }

 

-procedure{:entrypoint} Main2()

+procedure{:entrypoint} {:yields} Main2()

 {

-  while (true)

+  while (*)

   {

     async call PB();

-    async call PC();

+    async call PE();

     async call PD();

   }

 }

diff --git a/Test/og/foo.bpl b/Test/og/foo.bpl
index 776a165d..831d2b97 100644
--- a/Test/og/foo.bpl
+++ b/Test/og/foo.bpl
@@ -1,31 +1,37 @@
 var g:int;

 

-procedure PB()

+procedure {:yields} {:stable} PB()

+modifies g;

 {

   g := g + 1;

 }

 

-procedure PC()

-  ensures g == 3;

+procedure {:yields} PC()

+ensures g == 3;

 {

   g := 3;

   yield;

   assert g == 3;

 }

 

-procedure PD()

+procedure {:yields} {:stable} PE()

+{

+  call PC();

+}

+

+procedure {:yields} {:stable} PD()

 {

   call PC();

   assert g == 3;

   yield;

 }

 

-procedure{:entrypoint} Main()

+procedure {:entrypoint} {:yields} Main()

 {

-  while (true)

+  while (*)

   {

     async call PB();

-    async call PC();

+    async call PE();

     async call PD();

   }

 }

diff --git a/Test/og/linear-set.bpl b/Test/og/linear-set.bpl
index c2f792ef..96aca741 100644
--- a/Test/og/linear-set.bpl
+++ b/Test/og/linear-set.bpl
@@ -21,7 +21,7 @@ ensures xls == MapOr(xls1, xls2) && xls1 != None() && xls2 != None();
 

 procedure Allocate() returns ({:linear "tid"} xls: [X]bool);

 

-procedure {:entrypoint} main({:linear "tid"} tidls': [X]bool, {:linear "x"} xls': [X]bool) 

+procedure {:entrypoint} {:yields} main({:linear "tid"} tidls': [X]bool, {:linear "x"} xls': [X]bool) 

 requires tidls' != None() && xls' == All();

 {

     var {:linear "tid"} tidls: [X]bool;

@@ -46,7 +46,7 @@ requires tidls' != None() && xls' == All();
     async call thread(lsChild, xls2);

 }

 

-procedure thread({:linear "tid"} tidls': [X]bool, {:linear "x"} xls': [X]bool)

+procedure {:yields} {:stable} thread({:linear "tid"} tidls': [X]bool, {:linear "x"} xls': [X]bool)

 requires tidls' != None() && xls' != None();

 {

     var {:linear "x"} xls: [X]bool;

diff --git a/Test/og/linear-set2.bpl b/Test/og/linear-set2.bpl
index ac4a2e21..565cc82b 100644
--- a/Test/og/linear-set2.bpl
+++ b/Test/og/linear-set2.bpl
@@ -23,7 +23,7 @@ ensures xls == MapOr(xls1, xls2) && xls1 != None() && xls2 != None();
 procedure Allocate() returns ({:linear "tid"} xls: X);

 ensures xls != nil;

 

-procedure {:entrypoint} main({:linear "tid"} tidls': X, {:linear "x"} xls': [X]bool) 

+procedure {:entrypoint}  {:yields} main({:linear "tid"} tidls': X, {:linear "x"} xls': [X]bool) 

 requires tidls' != nil && xls' == All();

 {

     var {:linear "tid"} tidls: X;

@@ -46,7 +46,7 @@ requires tidls' != nil && xls' == All();
     async call thread(lsChild, xls2);

 }

 

-procedure thread({:linear "tid"} tidls': X, {:linear "x"} xls': [X]bool)

+procedure {:yields} {:stable} thread({:linear "tid"} tidls': X, {:linear "x"} xls': [X]bool)

 requires tidls' != nil && xls' != None();

 {

     var {:linear "x"} xls: [X]bool;

diff --git a/Test/og/new1.bpl b/Test/og/new1.bpl
index 472e64c6..6ebb9cf1 100644
--- a/Test/og/new1.bpl
+++ b/Test/og/new1.bpl
@@ -9,7 +9,7 @@ modifies Permissions;
 requires Permissions == mapconstbool(true);

 ensures xls == mapconstbool(true) && Permissions == mapconstbool(false);

 

-procedure PB({:linear "Perm"} permVar_in:[int]bool)

+procedure {:yields} {:stable} PB({:linear "Perm"} permVar_in:[int]bool)

 requires permVar_in[0] && g == 0;

 {

   var {:linear "Perm"} permVar_out: [int]bool;

@@ -26,7 +26,8 @@ requires permVar_in[0] && g == 0;
   assert g == 1;

 }

 

-procedure{:entrypoint} Main()

+procedure{:entrypoint} {:yields} Main()

+modifies g, Permissions;

 requires Permissions == mapconstbool(true);

 {

   var {:linear "Perm"} permVar_out: [int]bool;

diff --git a/Test/og/one.bpl b/Test/og/one.bpl
index 806a4178..2a63d60d 100644
--- a/Test/og/one.bpl
+++ b/Test/og/one.bpl
@@ -1,11 +1,12 @@
 var x:int;

 

 procedure A()

+modifies x;

 {

   x := x;

 }

 

-procedure B()

+procedure {:yields} B()

 {

   x := 5;

   yield;

diff --git a/Test/og/parallel1.bpl b/Test/og/parallel1.bpl
index cb3502b4..ecddc9fc 100644
--- a/Test/og/parallel1.bpl
+++ b/Test/og/parallel1.bpl
@@ -1,26 +1,27 @@
 var g:int;

 

-procedure PB()

+procedure {:yields} {:stable} PB()

+modifies g;

 {

   g := g + 1;

 }

 

-procedure PC()

-  ensures g == 3;

+procedure {:yields} {:stable} PC()

+ensures g == 3;

 {

   g := 3;

   yield;

   assert g == 3;

 }

 

-procedure PD()

+procedure {:yields} {:stable} PD()

 {

   call PC();

   assert g == 3;

   yield;

 }

 

-procedure{:entrypoint} Main()

+procedure {:entrypoint} {:yields} Main()

 {

   while (true)

   {

diff --git a/Test/og/parallel2.bpl b/Test/og/parallel2.bpl
index 116612cb..b963fe72 100644
--- a/Test/og/parallel2.bpl
+++ b/Test/og/parallel2.bpl
@@ -2,7 +2,7 @@ var a:[int]int;
 

 procedure Allocate() returns ({:linear "tid"} xls: int);

 

-procedure {:entrypoint} main() 

+procedure {:entrypoint} {:yields} main() 

 {

     var {:linear "tid"} i: int;

     var {:linear "tid"} j: int;

@@ -12,7 +12,7 @@ procedure {:entrypoint} main()
     call i := u(i) | j := u(j);

 }

 

-procedure t({:linear "tid"} i': int) returns ({:linear "tid"} i: int)

+procedure {:yields} {:stable} t({:linear "tid"} i': int) returns ({:linear "tid"} i: int)

 {

     i := i';

 

@@ -21,7 +21,7 @@ procedure t({:linear "tid"} i': int) returns ({:linear "tid"} i: int)
     assert a[i] == 42;

 }

 

-procedure u({:linear "tid"} i': int) returns ({:linear "tid"} i: int) 

+procedure {:yields} {:stable} u({:linear "tid"} i': int) returns ({:linear "tid"} i: int) 

 {

     i := i';

 

@@ -30,7 +30,7 @@ procedure u({:linear "tid"} i': int) returns ({:linear "tid"} i: int)
     assert a[i] == 42;

 }

 

-procedure Yield({:linear "tid"} i': int) returns ({:linear "tid"} i: int)

+procedure {:yields} Yield({:linear "tid"} i': int) returns ({:linear "tid"} i: int)

 ensures i == i';

 ensures old(a)[i] == a[i];

 {

diff --git a/Test/og/parallel3.bpl b/Test/og/parallel3.bpl
index a99a5eb8..f34efc6d 100644
--- a/Test/og/parallel3.bpl
+++ b/Test/og/parallel3.bpl
@@ -1,7 +1,7 @@
-procedure {:entrypoint} main() 

+procedure {:entrypoint} {:yields} main() 

 {

     call A() | B();

 }

 

-procedure A() {}

-procedure B() {}

+procedure {:yields} {:stable} A() {}

+procedure {:yields} {:stable} B() {}

diff --git a/Test/og/parallel4.bpl b/Test/og/parallel4.bpl
index 8f78fdc5..c07975ca 100644
--- a/Test/og/parallel4.bpl
+++ b/Test/og/parallel4.bpl
@@ -2,7 +2,7 @@ var a:int;
 

 procedure Allocate() returns ({:linear "tid"} xls: int);

 

-procedure {:entrypoint} main() 

+procedure {:entrypoint} {:yields} main() 

 {

   var {:linear "tid"} i: int;

   var {:linear "tid"} j: int;

@@ -11,7 +11,7 @@ procedure {:entrypoint} main()
   call i := t(i) | j := t(j);

 }

 

-procedure t({:linear "tid"} i': int) returns ({:linear "tid"} i: int)

+procedure {:yields} {:stable} t({:linear "tid"} i': int) returns ({:linear "tid"} i: int)

 {

   i := i';

   call Yield();

@@ -19,7 +19,7 @@ procedure t({:linear "tid"} i': int) returns ({:linear "tid"} i: int)
   a := a + 1;

 }

 

-procedure Yield()

+procedure {:yields} Yield()

 {

   yield;

 }

diff --git a/Test/og/parallel5.bpl b/Test/og/parallel5.bpl
index c583cb3c..eda8ef44 100644
--- a/Test/og/parallel5.bpl
+++ b/Test/og/parallel5.bpl
@@ -2,7 +2,7 @@ var a:[int]int;
 

 procedure Allocate() returns ({:linear "tid"} xls: int);

 

-procedure {:entrypoint} main() 

+procedure {:entrypoint} {:yields} main() 

 {

     var {:linear "tid"} i: int;

     var {:linear "tid"} j: int;

@@ -12,7 +12,7 @@ procedure {:entrypoint} main()
     call i := u(i) | j := u(j);

 }

 

-procedure t({:linear "tid"} i': int) returns ({:linear "tid"} i: int)

+procedure {:yields} {:stable} t({:linear "tid"} i': int) returns ({:linear "tid"} i: int)

 {

     i := i';

 

@@ -21,7 +21,7 @@ procedure t({:linear "tid"} i': int) returns ({:linear "tid"} i: int)
     assert a[i] == 42;

 }

 

-procedure u({:linear "tid"} i': int) returns ({:linear "tid"} i: int) 

+procedure {:yields} {:stable} u({:linear "tid"} i': int) returns ({:linear "tid"} i: int) 

 {

     i := i';

 

@@ -30,7 +30,7 @@ procedure u({:linear "tid"} i': int) returns ({:linear "tid"} i: int)
     assert a[i] == 42;

 }

 

-procedure Yield({:linear "tid"} i': int) returns ({:linear "tid"} i: int)

+procedure {:yields} {:stable} Yield({:linear "tid"} i': int) returns ({:linear "tid"} i: int)

 ensures i == i';

 ensures old(a)[i] == a[i];

 {

diff --git a/Test/og/parallel6.bpl b/Test/og/parallel6.bpl
index dba3eb2b..32f6e4bf 100644
--- a/Test/og/parallel6.bpl
+++ b/Test/og/parallel6.bpl
@@ -1,2 +1,2 @@
-procedure A();

-procedure C() { async call A(); }

+procedure {:yields} {:stable} A();

+procedure {:yields} C() { async call A(); }

diff --git a/Test/og/parallel7.bpl b/Test/og/parallel7.bpl
index 79c92196..7a4018df 100644
--- a/Test/og/parallel7.bpl
+++ b/Test/og/parallel7.bpl
@@ -1,3 +1,3 @@
-procedure A();

-procedure B();

-procedure C() { call A() | B(); }

+procedure {:yields} {:stable} A();

+procedure {:yields} {:stable} B();

+procedure {:yields} C() { call A() | B(); }

diff --git a/Test/og/perm.bpl b/Test/og/perm.bpl
index 78889868..ad4123f9 100644
--- a/Test/og/perm.bpl
+++ b/Test/og/perm.bpl
@@ -7,7 +7,7 @@ procedure Split({:linear "Perm"} xls: [int]bool) returns ({:linear "Perm"} xls1:
   ensures xls == ch_mapunion(xls1, xls2) && xls1 != ch_mapconstbool(false) && xls2 != ch_mapconstbool(false);

 

 

-procedure {:entrypoint} mainE({:linear "Perm"} permVar_in: [int]bool)

+procedure {:entrypoint} {:yields} mainE({:linear "Perm"} permVar_in: [int]bool)

    free requires permVar_in == ch_mapconstbool(true);

    free requires permVar_in[0];

   modifies x;

@@ -28,7 +28,7 @@ procedure {:entrypoint} mainE({:linear "Perm"} permVar_in: [int]bool)
     async call foo(permVarOut2);

 }

 

-procedure foo({:linear "Perm"} permVar_in: [int]bool) 

+procedure {:yields} {:stable} foo({:linear "Perm"} permVar_in: [int]bool) 

   free requires permVar_in != ch_mapconstbool(false);

   free requires permVar_in[1];

   requires x == 0;

diff --git a/Test/og/runtest.bat b/Test/og/runtest.bat
index 5915a206..1325e476 100644
--- a/Test/og/runtest.bat
+++ b/Test/og/runtest.bat
@@ -6,12 +6,12 @@ set BGEXE=..\..\Binaries\Boogie.exe
 for %%f in (foo.bpl bar.bpl one.bpl parallel1.bpl parallel3.bpl) do (

   echo.

   echo -------------------- %%f --------------------

-  %BGEXE% %* /nologo /noinfer /doModSetAnalysis /OwickiGries:OwickiGriesDesugared.bpl %%f

+  %BGEXE% %* /nologo /noinfer %%f

 )

 

 for %%f in (linear-set.bpl linear-set2.bpl FlanaganQadeer.bpl DeviceCacheSimplified.bpl parallel2.bpl parallel4.bpl parallel5.bpl parallel6.bpl parallel7.bpl akash.bpl t1.bpl new1.bpl perm.bpl async.bpl) do (

   echo.

   echo -------------------- %%f --------------------

-  %BGEXE% %* /nologo /noinfer /typeEncoding:m /useArrayTheory /doModSetAnalysis /OwickiGries:OwickiGriesDesugared.bpl %%f

+  %BGEXE% %* /nologo /noinfer /typeEncoding:m /useArrayTheory %%f

 )

 

diff --git a/Test/og/t1.bpl b/Test/og/t1.bpl
index 28ae5b89..84ed3a35 100644
--- a/Test/og/t1.bpl
+++ b/Test/og/t1.bpl
@@ -12,7 +12,7 @@ ensures xls == mapconstbool(true);
 var g: int;

 var h: int;

 

-procedure A({:linear "tid"} tid_in: int) returns ({:linear "tid"} tid_out: int) 

+procedure {:yields} A({:linear "tid"} tid_in: int) returns ({:linear "tid"} tid_out: int) 

 {

     var {:linear "1"} x: [int]bool;

     var {:linear "2"} y: [int]bool;

@@ -45,7 +45,7 @@ procedure A({:linear "tid"} tid_in: int) returns ({:linear "tid"} tid_out: int)
     async call C(tid_child, y);

 }

 

-procedure B({:linear "tid"} tid_in: int, {:linear "1"} x_in: [int]bool) 

+procedure {:yields} {:stable} B({:linear "tid"} tid_in: int, {:linear "1"} x_in: [int]bool) 

 requires x_in != mapconstbool(false);

 {

     var {:linear "tid"} tid_out: int;

@@ -56,7 +56,7 @@ requires x_in != mapconstbool(false);
     g := 1;

 }

 

-procedure C({:linear "tid"} tid_in: int, {:linear "2"} y_in: [int]bool) 

+procedure {:yields} {:stable} C({:linear "tid"} tid_in: int, {:linear "2"} y_in: [int]bool) 

 requires y_in != mapconstbool(false);

 {

     var {:linear "tid"} tid_out: int;

diff --git a/Test/test0/Answer b/Test/test0/Answer
index 8c7ce4c7..f92dd1dc 100644
--- a/Test/test0/Answer
+++ b/Test/test0/Answer
@@ -123,8 +123,8 @@ axiom (forall x: int :: {:xname "hello"} {:weight 5} {:ValueFunc f(x + 1)} { f(x
 Boogie program verifier finished with 0 verified, 0 errors

 

 Boogie program verifier finished with 0 verified, 0 errors

-Arrays1.bpl(11,11): Error: command assigns to a global variable that is not in the enclosing method's modifies clause: Q

-Arrays1.bpl(14,15): Error: command assigns to a global variable that is not in the enclosing method's modifies clause: Q

+Arrays1.bpl(11,11): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: Q

+Arrays1.bpl(14,15): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: Q

 2 type checking errors detected in Arrays1.bpl

 Types0.bpl(6,18): error: expected identifier before ':'

 Types0.bpl(6,12): error: expecting an identifier as parameter name

diff --git a/Test/test1/Answer b/Test/test1/Answer
index 70b7ea80..e1a36ad9 100644
--- a/Test/test1/Answer
+++ b/Test/test1/Answer
@@ -1,20 +1,20 @@
 Frame0.bpl(10,11): Error: undeclared identifier: a

 Frame0.bpl(12,11): Error: undeclared identifier: b

 2 name resolution errors detected in Frame0.bpl

-Frame1.bpl(16,7): Error: command assigns to a global variable that is not in the enclosing method's modifies clause: g1

+Frame1.bpl(16,7): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: g1

 Frame1.bpl(17,6): Error: command assigns to an immutable variable: a

-Frame1.bpl(22,4): Error: command assigns to a global variable that is not in the enclosing method's modifies clause: g1

+Frame1.bpl(22,4): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: g1

 Frame1.bpl(23,4): Error: command assigns to an immutable variable: a

 Frame1.bpl(27,12): Error: command assigns to an immutable variable: hh

-Frame1.bpl(28,12): Error: command assigns to a global variable that is not in the enclosing method's modifies clause: h0

+Frame1.bpl(28,12): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: h0

 Frame1.bpl(30,7): Error: command assigns to an immutable variable: hh

-Frame1.bpl(31,7): Error: command assigns to a global variable that is not in the enclosing method's modifies clause: h0

+Frame1.bpl(31,7): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: h0

 Frame1.bpl(33,4): Error: command assigns to an immutable variable: hh

-Frame1.bpl(34,4): Error: command assigns to a global variable that is not in the enclosing method's modifies clause: h0

-Frame1.bpl(55,4): Error: command assigns to a global variable that is not in the enclosing method's modifies clause: g0

-Frame1.bpl(68,4): Error: command assigns to a global variable that is not in the enclosing method's modifies clause: g0

-Frame1.bpl(68,4): Error: command assigns to a global variable that is not in the enclosing method's modifies clause: g1

-Frame1.bpl(68,4): Error: command assigns to a global variable that is not in the enclosing method's modifies clause: h0

+Frame1.bpl(34,4): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: h0

+Frame1.bpl(55,4): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: g0

+Frame1.bpl(68,4): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: g0

+Frame1.bpl(68,4): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: g1

+Frame1.bpl(68,4): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: h0

 Frame1.bpl(84,15): Error: mismatched type of in-parameter in implementation MismatchedTypes: x

 Frame1.bpl(89,15): Error: mismatched type of in-parameter in implementation MismatchedTypes: x (named y in implementation)

 16 type checking errors detected in Frame1.bpl

@@ -107,7 +107,7 @@ UpdateExprTyping.bpl(36,28): Error: right-hand side in map store with wrong type
 UpdateExprTyping.bpl(38,27): Error: right-hand side in map store with wrong type: ref (expected: int)

 UpdateExprTyping.bpl(39,27): Error: right-hand side in map store with wrong type: int (expected: ref)

 12 type checking errors detected in UpdateExprTyping.bpl

-MapsTypeErrors.bpl(26,6): Error: command assigns to a global variable that is not in the enclosing method's modifies clause: m

+MapsTypeErrors.bpl(26,6): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: m

 MapsTypeErrors.bpl(32,2): Error: mismatched types in assignment command (cannot assign int to []int)

 MapsTypeErrors.bpl(33,3): Error: mismatched types in assignment command (cannot assign []int to int)

 MapsTypeErrors.bpl(39,3): Error: mismatched types in assignment command (cannot assign bool to int)

diff --git a/Test/test15/Answer b/Test/test15/Answer
index 7f20ab7a..502d7db5 100644
--- a/Test/test15/Answer
+++ b/Test/test15/Answer
@@ -121,11 +121,11 @@ Execution trace:
     CaptureState.bpl(24,5): anon3

 *** MODEL

 $mv_state_const -> 6

-%lbl%@293 -> false

+%lbl%@294 -> false

 %lbl%+112 -> true

 %lbl%+114 -> true

 %lbl%+118 -> true

-%lbl%+148 -> true

+%lbl%+149 -> true

 boolType -> T@T!val!2

 F -> T@U!val!2

 FieldNameType -> T@T!val!4

diff --git a/Test/test20/Answer b/Test/test20/Answer
index 5e4481ca..4127471b 100644
--- a/Test/test20/Answer
+++ b/Test/test20/Answer
@@ -177,7 +177,7 @@ ProcParamReordering.bpl(15,15): Error: mismatched number of type parameters in p
 2 type checking errors detected in ProcParamReordering.bpl

 ParallelAssignment.bpl(17,2): Error: mismatched types in assignment command (cannot assign bool to int)

 ParallelAssignment.bpl(18,4): Error: invalid type for argument 0 in map assignment: bool (expected: int)

-ParallelAssignment.bpl(20,4): Error: command assigns to a global variable that is not in the enclosing method's modifies clause: z

+ParallelAssignment.bpl(20,4): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: z

 3 type checking errors detected in ParallelAssignment.bpl

 ParallelAssignment2.bpl(9,7): Error: number of left-hand sides does not match number of right-hand sides

 ParallelAssignment2.bpl(10,9): Error: variable a is assigned more than once in parallel assignment