1 files changed, 20 insertions, 0 deletions
diff --git a/Chalice/tests/permission-model/predicate_error4.chalice b/Chalice/tests/permission-model/predicate_error4.chalice
new file mode 100644
index 00000000..0726e349
--- /dev/null
+++ b/Chalice/tests/permission-model/predicate_error4.chalice
@@ -0,0 +1,20 @@
+class Cell {
+  var x: int;
+  
+  // --- some predicates ---
+  
+  predicate write1 { acc(x) } // full permission in a predicate
+  predicate write2 { acc(x,10) } // 10%
+  predicate read1 { rd(x) } // fractional read permission
+  predicate read2 { rd*(x) } // starred fractional read permission
+  predicate read3 { rd(x,1) } // counting permission (1 epsilon)
+  
+  // --- invalid permission scaling ---
+  
+  method error()
+    requires rd(read3);
+  {
+    unfold rd(read3); // ERROR: scaling epsilons is not possible
+  }
+  
+}