1 files changed, 34 insertions, 0 deletions
diff --git a/Chalice/refinements/AngelicExec.chalice b/Chalice/refinements/AngelicExec.chalice
new file mode 100644
index 00000000..06ab9c83
--- /dev/null
+++ b/Chalice/refinements/AngelicExec.chalice
@@ -0,0 +1,34 @@
+class A0 {
+  method m(b: bool) {
+    var x;
+    if (b) {
+      var x [0 <= x && x < 3];
+    } else {
+      x := 1;
+    }
+  }
+}
+
+class B0 refines A0 {
+  refines m(b: bool) {
+    var x := 1;
+  }
+}
+
+class A1 refines A0 {
+  transforms m(b: bool) {
+    _
+    if { 
+      replaces * by {x := 1;}
+    } else {
+      *
+    }
+    _
+  }
+}
+
+class A2 refines A1 {
+  refines m(b: bool) {
+    var x := 1;
+  }
+}