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, 1 insertions, 1 deletions

diff --git a/Test/og/Program4.bpl b/Test/og/Program4.bpl
index 61d4fcdc..0228adc9 100644
--- a/Test/og/Program4.bpl
+++ b/Test/og/Program4.bpl
@@ -13,7 +13,7 @@ function {:inline} {:linear "tid"} TidSetCollector(x: [Tid]bool) : [Tid]bool
   x

 }

 

-var {:layer 1} a:[Tid]int;

+var {:layer 0,1} a:[Tid]int;

 

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