1 files changed, 29 insertions, 0 deletions
diff --git a/Chalice/tests/predicates/test3.chalice b/Chalice/tests/predicates/test3.chalice
new file mode 100644
index 00000000..2a364fee
--- /dev/null
+++ b/Chalice/tests/predicates/test3.chalice
@@ -0,0 +1,29 @@
+class Unsound
+{
+  var value:int;
+  
+  predicate inv { acc(value) }
+  
+  function get():int
+    requires inv;
+  {
+    unfolding inv in value
+  }
+  
+  method set(newval:int)
+    requires inv;
+    ensures inv && get()==newval;
+  {
+    unfold inv;
+    value:=newval;
+    fold inv;
+  }
+  
+  method test()
+    requires inv;
+  {
+    call set(3);
+    call set(4);
+    // at this point, Chalice used to be able to prove false
+  }
+}
+\ No newline at end of file