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/linear-set2.bpl b/Test/og/linear-set2.bpl
index 93ede868..81d30521 100644
--- a/Test/og/linear-set2.bpl
+++ b/Test/og/linear-set2.bpl
@@ -20,8 +20,8 @@ function {:inline} {:linear "x"} XCollector(xs: [X]bool) : [X]bool
   xs

 }

 

-var {:layer 1} x: int;

-var {:layer 1} l: X;

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

+var {:layer 0,1} l: X;

 const nil: X;

 

 procedure Split({:linear_in "x"} xls: [X]bool) returns ({:linear "x"} xls1: [X]bool, {:linear "x"} xls2: [X]bool);