From 1f38d2d252aaac3d55191e6c3dad46ecffdfee2c Mon Sep 17 00:00:00 2001
From: Rustan Leino <unknown>
Date: Tue, 1 Mar 2016 15:37:54 -0800
Subject: Revised the $Is and $IsAlloc axioms for arrow terms.  It is now
 possible to derived these predicates.  More things can now be verified
 (including the problem reported in Issue #49).

---
 Test/hofs/OneShot.dfy      | 9 ++++-----
 Test/hofs/VectorUpdate.dfy | 2 +-
 2 files changed, 5 insertions(+), 6 deletions(-)

(limited to 'Test')

diff --git a/Test/hofs/OneShot.dfy b/Test/hofs/OneShot.dfy
index 286be898..e920530a 100644
--- a/Test/hofs/OneShot.dfy
+++ b/Test/hofs/OneShot.dfy
@@ -10,16 +10,15 @@ method OneShot() {
   var i : Ref<int>;
   i := new Ref;
 
-  g := () -> true;
-
+  g := () reads i -> true;  // using a (deprecated) one-shot arrow here means "g" acquires
+                           // a precondition that says it can only be applied in this heap
   assert g();
 
   i.val := i.val + 1; // heap changes
 
   if * {
-    assert g();         // should fail
+    assert g();         // error: precondition violation
   } else {
-    assert !g();        // should fail
+    assert !g();        // error: precondition violation
   }
 }
-
diff --git a/Test/hofs/VectorUpdate.dfy b/Test/hofs/VectorUpdate.dfy
index ca6b20b3..6fb25a87 100644
--- a/Test/hofs/VectorUpdate.dfy
+++ b/Test/hofs/VectorUpdate.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:3 "%s" > "%t"
+// RUN: %dafny /compile:3 /autoTriggers:1 "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 // this is a rather verbose version of the VectorUpdate method
-- 
cgit v1.2.3