Chalice: exhale spec statement post condition in refinement block translation; tag global coupling assertions (bug fix)

1 files changed, 11 insertions, 1 deletions

diff --git a/Chalice/refinements/Counter.chalice b/Chalice/refinements/Counter.chalice
index 16cd8473..f2184a2d 100644
--- a/Chalice/refinements/Counter.chalice
+++ b/Chalice/refinements/Counter.chalice
@@ -49,7 +49,12 @@ class Counter1 refines Counter0 {
   refines dec() 
   {
     this.z := this.z + 1;
-  }       
+  }      
+
+  refines magic() returns (c: Cell)
+  {
+    c := new Cell;
+  } 
 }
 
 class Cell {var n: int}
@@ -82,6 +87,11 @@ class Counter2 refines Counter0 {
   {
     this.b.n := this.b.n + 1;
   }
+
+  refines magic() returns (c: Cell)
+  {
+    c := a;
+  }
 }
 
 class Client {