another fix requested by Chris

verification is performed now for all created layers

36 files changed, 53 insertions, 34 deletions

diff --git a/Test/civl/DeviceCache.bpl.expect b/Test/civl/DeviceCache.bpl.expect
index c4cf5ccf..129e60e2 100644
--- a/Test/civl/DeviceCache.bpl.expect
+++ b/Test/civl/DeviceCache.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 30 verified, 0 errors
+Boogie program verifier finished with 39 verified, 0 errors
diff --git a/Test/civl/FlanaganQadeer.bpl.expect b/Test/civl/FlanaganQadeer.bpl.expect
index 00ddb38b..76a9a2bf 100644
--- a/Test/civl/FlanaganQadeer.bpl.expect
+++ b/Test/civl/FlanaganQadeer.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 4 verified, 0 errors
+Boogie program verifier finished with 8 verified, 0 errors
diff --git a/Test/civl/Program1.bpl.expect b/Test/civl/Program1.bpl.expect
index 41374b00..00ddb38b 100644
--- a/Test/civl/Program1.bpl.expect
+++ b/Test/civl/Program1.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 2 verified, 0 errors
+Boogie program verifier finished with 4 verified, 0 errors
diff --git a/Test/civl/Program2.bpl.expect b/Test/civl/Program2.bpl.expect
index a9949f2e..9823d44a 100644
--- a/Test/civl/Program2.bpl.expect
+++ b/Test/civl/Program2.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 3 verified, 0 errors
+Boogie program verifier finished with 6 verified, 0 errors
diff --git a/Test/civl/Program3.bpl.expect b/Test/civl/Program3.bpl.expect
index a9949f2e..9823d44a 100644
--- a/Test/civl/Program3.bpl.expect
+++ b/Test/civl/Program3.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 3 verified, 0 errors
+Boogie program verifier finished with 6 verified, 0 errors
diff --git a/Test/civl/Program4.bpl.expect b/Test/civl/Program4.bpl.expect
index a9949f2e..9823d44a 100644
--- a/Test/civl/Program4.bpl.expect
+++ b/Test/civl/Program4.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 3 verified, 0 errors
+Boogie program verifier finished with 6 verified, 0 errors
diff --git a/Test/civl/Program5.bpl.expect b/Test/civl/Program5.bpl.expect
index fde7e712..4bcb1071 100644
--- a/Test/civl/Program5.bpl.expect
+++ b/Test/civl/Program5.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 18 verified, 0 errors
+Boogie program verifier finished with 21 verified, 0 errors
diff --git a/Test/civl/StoreBuffer.bpl.expect b/Test/civl/StoreBuffer.bpl.expect
index 8c74fe2e..1931ffd2 100644
--- a/Test/civl/StoreBuffer.bpl.expect
+++ b/Test/civl/StoreBuffer.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 17 verified, 0 errors
+Boogie program verifier finished with 27 verified, 0 errors
diff --git a/Test/civl/akash.bpl.expect b/Test/civl/akash.bpl.expect
index 00ddb38b..76a9a2bf 100644
--- a/Test/civl/akash.bpl.expect
+++ b/Test/civl/akash.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 4 verified, 0 errors
+Boogie program verifier finished with 8 verified, 0 errors
diff --git a/Test/civl/alloc.bpl.expect b/Test/civl/alloc.bpl.expect
index f08c6e00..4bcb1071 100644
--- a/Test/civl/alloc.bpl.expect
+++ b/Test/civl/alloc.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 12 verified, 0 errors
+Boogie program verifier finished with 21 verified, 0 errors
diff --git a/Test/civl/bar.bpl.expect b/Test/civl/bar.bpl.expect
index 810c93bf..be6722fe 100644
--- a/Test/civl/bar.bpl.expect
+++ b/Test/civl/bar.bpl.expect
@@ -10,4 +10,4 @@ Execution trace:
     (0,0): anon00
     (0,0): inline$Impl_YieldChecker_PC_1$0$L0
 
-Boogie program verifier finished with 3 verified, 2 errors
+Boogie program verifier finished with 8 verified, 2 errors
diff --git a/Test/civl/chris2.bpl.expect b/Test/civl/chris2.bpl.expect
index ddb8537e..f3b66f4a 100644
--- a/Test/civl/chris2.bpl.expect
+++ b/Test/civl/chris2.bpl.expect
@@ -15,4 +15,4 @@ Execution trace:
 Execution trace:
     (0,0): this_A
 
-Boogie program verifier finished with 1 verified, 4 errors
+Boogie program verifier finished with 2 verified, 4 errors
diff --git a/Test/civl/chris6.bpl b/Test/civl/chris6.bpl
new file mode 100644
index 00000000..a0aecf1e
--- /dev/null
+++ b/Test/civl/chris6.bpl
@@ -0,0 +1,14 @@
+// RUN: %boogie -noinfer -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+procedure{:extern}{:yields}{:layer 1,2} P1();
+  requires{:layer 1} false;
+  ensures{:atomic} |{ A: return true; }|;
+
+procedure{:yields}{:layer 2,3} P2()
+  ensures{:atomic} |{ A: return true; }|;
+{
+  assert{:layer 1} false;
+  yield;
+  call P1();
+  yield;
+}
diff --git a/Test/civl/chris6.bpl.expect b/Test/civl/chris6.bpl.expect
new file mode 100644
index 00000000..229e4e10
--- /dev/null
+++ b/Test/civl/chris6.bpl.expect
@@ -0,0 +1,5 @@
+chris6.bpl(10,3): Error BP5001: This assertion might not hold.
+Execution trace:
+    chris6.bpl(10,3): anon0
+
+Boogie program verifier finished with 1 verified, 1 error
diff --git a/Test/civl/civl-paper.bpl.expect b/Test/civl/civl-paper.bpl.expect
index 11d204a8..bd1df2f9 100644
--- a/Test/civl/civl-paper.bpl.expect
+++ b/Test/civl/civl-paper.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 35 verified, 0 errors
+Boogie program verifier finished with 45 verified, 0 errors
diff --git a/Test/civl/foo.bpl.expect b/Test/civl/foo.bpl.expect
index 41e30691..44a93860 100644
--- a/Test/civl/foo.bpl.expect
+++ b/Test/civl/foo.bpl.expect
@@ -5,4 +5,4 @@ Execution trace:
     foo.bpl(14,3): inline$Incr_1$0$A
     (0,0): inline$Impl_YieldChecker_PC_1$0$L0
 
-Boogie program verifier finished with 4 verified, 1 error
+Boogie program verifier finished with 9 verified, 1 error
diff --git a/Test/civl/ghost.bpl.expect b/Test/civl/ghost.bpl.expect
index 9823d44a..76a9a2bf 100644
--- a/Test/civl/ghost.bpl.expect
+++ b/Test/civl/ghost.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 6 verified, 0 errors
+Boogie program verifier finished with 8 verified, 0 errors
diff --git a/Test/civl/linear-set.bpl.expect b/Test/civl/linear-set.bpl.expect
index 00ddb38b..76a9a2bf 100644
--- a/Test/civl/linear-set.bpl.expect
+++ b/Test/civl/linear-set.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 4 verified, 0 errors
+Boogie program verifier finished with 8 verified, 0 errors
diff --git a/Test/civl/linear-set2.bpl.expect b/Test/civl/linear-set2.bpl.expect
index 00ddb38b..76a9a2bf 100644
--- a/Test/civl/linear-set2.bpl.expect
+++ b/Test/civl/linear-set2.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 4 verified, 0 errors
+Boogie program verifier finished with 8 verified, 0 errors
diff --git a/Test/civl/lock-introduced.bpl.expect b/Test/civl/lock-introduced.bpl.expect
index f08c6e00..8c74fe2e 100644
--- a/Test/civl/lock-introduced.bpl.expect
+++ b/Test/civl/lock-introduced.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 12 verified, 0 errors
+Boogie program verifier finished with 17 verified, 0 errors
diff --git a/Test/civl/lock.bpl.expect b/Test/civl/lock.bpl.expect
index 3e6d423a..76a9a2bf 100644
--- a/Test/civl/lock.bpl.expect
+++ b/Test/civl/lock.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 5 verified, 0 errors
+Boogie program verifier finished with 8 verified, 0 errors
diff --git a/Test/civl/lock2.bpl.expect b/Test/civl/lock2.bpl.expect
index 3e6d423a..76a9a2bf 100644
--- a/Test/civl/lock2.bpl.expect
+++ b/Test/civl/lock2.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 5 verified, 0 errors
+Boogie program verifier finished with 8 verified, 0 errors
diff --git a/Test/civl/multiset.bpl.expect b/Test/civl/multiset.bpl.expect
index 0a77c517..63682bb4 100644
--- a/Test/civl/multiset.bpl.expect
+++ b/Test/civl/multiset.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 78 verified, 0 errors
+Boogie program verifier finished with 85 verified, 0 errors
diff --git a/Test/civl/new1.bpl.expect b/Test/civl/new1.bpl.expect
index 41374b00..00ddb38b 100644
--- a/Test/civl/new1.bpl.expect
+++ b/Test/civl/new1.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 2 verified, 0 errors
+Boogie program verifier finished with 4 verified, 0 errors
diff --git a/Test/civl/one.bpl.expect b/Test/civl/one.bpl.expect
index 37fad75c..41374b00 100644
--- a/Test/civl/one.bpl.expect
+++ b/Test/civl/one.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 1 verified, 0 errors
+Boogie program verifier finished with 2 verified, 0 errors
diff --git a/Test/civl/par-incr.bpl.expect b/Test/civl/par-incr.bpl.expect
index 00ddb38b..3e3dc54b 100644
--- a/Test/civl/par-incr.bpl.expect
+++ b/Test/civl/par-incr.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 4 verified, 0 errors
+Boogie program verifier finished with 7 verified, 0 errors
diff --git a/Test/civl/parallel1.bpl.expect b/Test/civl/parallel1.bpl.expect
index 889ee4f2..fa974099 100644
--- a/Test/civl/parallel1.bpl.expect
+++ b/Test/civl/parallel1.bpl.expect
@@ -5,4 +5,4 @@ Execution trace:
     parallel1.bpl(14,3): inline$Incr_1$0$A
     (0,0): inline$Impl_YieldChecker_PC_1$0$L0
 
-Boogie program verifier finished with 3 verified, 1 error
+Boogie program verifier finished with 7 verified, 1 error
diff --git a/Test/civl/parallel2.bpl.expect b/Test/civl/parallel2.bpl.expect
index 3e6d423a..12041afe 100644
--- a/Test/civl/parallel2.bpl.expect
+++ b/Test/civl/parallel2.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 5 verified, 0 errors
+Boogie program verifier finished with 10 verified, 0 errors
diff --git a/Test/civl/parallel4.bpl.expect b/Test/civl/parallel4.bpl.expect
index 2d4c8148..baf228c8 100644
--- a/Test/civl/parallel4.bpl.expect
+++ b/Test/civl/parallel4.bpl.expect
@@ -3,4 +3,4 @@ Execution trace:
     parallel4.bpl(29,5): anon0
     (0,0): anon01
 
-Boogie program verifier finished with 3 verified, 1 error
+Boogie program verifier finished with 7 verified, 1 error
diff --git a/Test/civl/parallel5.bpl.expect b/Test/civl/parallel5.bpl.expect
index 3e6d423a..12041afe 100644
--- a/Test/civl/parallel5.bpl.expect
+++ b/Test/civl/parallel5.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 5 verified, 0 errors
+Boogie program verifier finished with 10 verified, 0 errors
diff --git a/Test/civl/perm.bpl.expect b/Test/civl/perm.bpl.expect
index 41374b00..00ddb38b 100644
--- a/Test/civl/perm.bpl.expect
+++ b/Test/civl/perm.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 2 verified, 0 errors
+Boogie program verifier finished with 4 verified, 0 errors
diff --git a/Test/civl/t1.bpl.expect b/Test/civl/t1.bpl.expect
index fcef7e58..27a208d4 100644
--- a/Test/civl/t1.bpl.expect
+++ b/Test/civl/t1.bpl.expect
@@ -6,4 +6,4 @@ Execution trace:
     t1.bpl(25,21): inline$SetG_1$0$A
     (0,0): inline$Impl_YieldChecker_A_1$0$L1
 
-Boogie program verifier finished with 4 verified, 1 error
+Boogie program verifier finished with 9 verified, 1 error
diff --git a/Test/civl/termination2.bpl.expect b/Test/civl/termination2.bpl.expect
index 37fad75c..41374b00 100644
--- a/Test/civl/termination2.bpl.expect
+++ b/Test/civl/termination2.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 1 verified, 0 errors
+Boogie program verifier finished with 2 verified, 0 errors
diff --git a/Test/civl/ticket.bpl.expect b/Test/civl/ticket.bpl.expect
index b072912b..dc45a0ee 100644
--- a/Test/civl/ticket.bpl.expect
+++ b/Test/civl/ticket.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 16 verified, 0 errors
+Boogie program verifier finished with 24 verified, 0 errors
diff --git a/Test/civl/treiber-stack.bpl.expect b/Test/civl/treiber-stack.bpl.expect
index 9823d44a..76a9a2bf 100644
--- a/Test/civl/treiber-stack.bpl.expect
+++ b/Test/civl/treiber-stack.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 6 verified, 0 errors
+Boogie program verifier finished with 8 verified, 0 errors
diff --git a/Test/civl/wsq.bpl.expect b/Test/civl/wsq.bpl.expect
index a9949f2e..9823d44a 100644
--- a/Test/civl/wsq.bpl.expect
+++ b/Test/civl/wsq.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 3 verified, 0 errors
+Boogie program verifier finished with 6 verified, 0 errors