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

diff --git a/Test/og/multiset.bpl b/Test/og/multiset.bpl
index 0f56dd7e..308e4b8b 100644
--- a/Test/og/multiset.bpl
+++ b/Test/og/multiset.bpl
@@ -6,10 +6,10 @@ const unique null : int;
 const unique nil: X;

 const unique done: X;

 

-var elt : [int]int;

-var valid : [int]bool;

-var lock : [int]X;

-var owner : [int]X;

+var {:layer 0} elt : [int]int;

+var {:layer 0} valid : [int]bool;

+var {:layer 0} lock : [int]X;

+var {:layer 0} owner : [int]X;

 const max : int;

 

 function {:builtin "MapConst"} MapConstBool(bool) : [X]bool;