1. made variable introduction layer explicit in the test cases

2. if a single layer is specified for a global variable, that layer is the introduction layer

1 files changed, 2 insertions, 2 deletions

diff --git a/Test/og/t1.bpl b/Test/og/t1.bpl
index 305f1ed1..b2f02bda 100644
--- a/Test/og/t1.bpl
+++ b/Test/og/t1.bpl
@@ -27,8 +27,8 @@ ensures {:layer 1} xls == mapconstbool(true);
 procedure Allocate_2() returns ({:linear "2"} xls: [int]bool);

 ensures {:layer 1} xls == mapconstbool(true);

 

-var {:layer 1} g: int;

-var {:layer 1} h: int;

+var {:layer 0,1} g: int;

+var {:layer 0,1} h: int;

 

 procedure {:yields} {:layer 0,1} SetG(val:int);

 ensures {:atomic} |{A: g := val; return true; }|;